The Coq mailing list

["Razvan Voicu" <razvan AT comp.nus.edu.sg>]

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