The Coq mailing list

[Hongjin Liang <lianghongjin AT gmail.com>]

Hi all,

I defined a coinductive property and tried to prove a lemma about it. When I applied the hypothesis, the proof violates the guarded condition. But if I wrote the same hypothesis as a case in the coinductive definition, then I can complete the proof. I'm not familiar with coq, but I'm really curious about the reasons behind the results and hope somebody could help me. My code is given below (it itself does not have special meanings). 

*****************************************************************************

CoInductive LList : Set :=

    LNil : LList

  | LCons : nat -> LList -> LList. 

CoInductive my_Inf : LList -> Prop :=

    My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l. 

  

Hypothesis foo : forall l, my_Inf l -> my_Inf (LCons 0 l). 

Lemma foo_test :  forall l, my_Inf l. 

Proof. 

  cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded. 

------------------------------------------------------------------------------------------------

The error message: 

Recursive definition of H is ill-formed.

In environment

H : forall l : LList, my_Inf l

l : LList

Sub-_expression_ "foo l (H l)" not in guarded form (should be a constructor, an

abstraction, a match, a cofix or a recursive call).

Recursive definition is: "fun l : LList => My_Inf_Lcons l (foo l (H l))".

*****************************************************************************

Then I merged the coinductive definition my_Inf and the hypothesis foo to be a new coinductive definition: 

CoInductive my_Inf : LList -> Prop :=

    My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l

  | foo : forall l, my_Inf l -> my_Inf (LCons 0 l). 

Lemma foo_test :  forall l, my_Inf l. 

Proof. 

  cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded. 

Qed.

The proof is completed and foo_test is defined. 

*****************************************************************************

I'm really curious about the differences between the above two ways to define and prove coinductive properties. Could anyone give me some hints about the reasons behind the results please? Thanks a lot!

- Hongjin