The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.