Skip to Content.
Sympa Menu

coq-club - [Coq-Club] make coinductive types and hypotheses work together

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] make coinductive types and hypotheses work together


chronological Thread 
  • From: Hongjin Liang <lianghongjin AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] make coinductive types and hypotheses work together
  • Date: Sun, 7 Aug 2011 14:40:55 +0800

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



Archive powered by MhonArc 2.6.16.

Top of Page