The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

Hi,

Your lemma actually shows the equivalence with the inductive versions
of the predicates.

The direct proof goes through all right for me (I do not think it is a  
question
of Coq versions, but this is with 8.2beta) :


CoInductive a:nat->Prop := a1: a O | a2: forall n, a n -> a (S (S (S  
(S n)))).
CoInductive b : nat->Prop := b1: b O | b2: forall n, b n -> b (S (S n)).
Goal forall n, a n -> b n.

cofix chr.
intros [|p].
 intros; constructor.
inversion 1.
constructor; constructor.
apply chr.
assumption.
Qed.

Le 18 juin 08 à 11:35, Razvan Voicu a écrit :

> Hi,
>
> Consider the following toy example:
>
> CoInductive a:nat->Prop := a1: a O | a2: forall n, a n -> a (S (S (S  
> (S n)))).
> Coinductive b:nat->Prop := b1: b O | b2: forall n, b n -> b (S (S n)).
> Goal forall n, a n -> b n.
>
> I can't use elim for coinductive definitions. So the only solution I  
> found was to prove this auxilliary lemma:
>
> Lemma L: forall n, a n -> n=O \/ exists m, (S (S (S (S m))))=n /\ a  
> m. (* easily proven using cofix and destruct*)
>
> I have the following questions:
>
> 1) Is there a more straightforward way to prove the above goal,  
> without the auxilliary theorem?
>
> 2) In fact, the auxilliary theorem might be useful in a lot of other  
> situations, so I may want to define and prove this type of lemma for  
> each of my inductive/coinductive definitions. Is there some sort of  
> scripting tool that would allow me to program a macro or procedure  
> whose parameter would be a, and which would automate the process of  
> generating this type of lemma and its proof?
>
> Thanks in advance,
>
> Razvan