The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

A long time ago when I did some coinduction in Coq, this threw me
off-guard, too.  Then I realized it was just Coq's way of making sure
that I wasn't writing down nonsense, which is what I would have been
doing if I had tried to do such a proof on paper.

One obvious way to proceed is to write a corecursive function from
your tree to the witness of the existential quantifier, and state your
lemma in terms of that function.  At least, that usually worked for
me.

 - Aaron

On Fri, Feb 25, 2011 at 4:19 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
>Â dimiter.milushev AT cs.kuleuven.be
>  wrote:
>>
>> I am trying to do some very basic coinductive proofs in Coq,
>> but I get stuck and am not able to use the cofix tactic in lemma wfExStr
>> below.
>> [...]
>>
>> CoInductive wf (t : Tree) : Prop :=
>>   wftree : forall f,
>>   t = Node f
>>   ->  inhabited f
>>   ->  (forall a ta, f a = Some ta ->  wf ta)
>>   ->  wf t.
>>
>> [...]
>>
>> Lemma wfExStr: forall X : Tree, exists w,
>> wf(X)->  elem w X.
>>
>
> This is a variant of a standard question about coinduction in Coq.  Last
> time someone asked it, I said it was impossible to prove such theorems.
>  That is, coinduction can only be used to build values of coinductive types,
> and you are trying to build a value of an inductive type (via [exists]),
> with a coinductive value nested inside.
>
> Last time, however, someone suggested some scary (to me) solution that uses
> a very non-constructive axiom (if I remember correctly).  Someone else may
> repeat the suggestion again soon.
>