The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 25 Feb 2011 16:49:01 -0500,
Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 a écrit :

> 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.
> >
> 

I am not sure of what I am saying, but I think it is not provable:
the only way you have to prove something like that is to do some
coinduction over some coinductive structure at some place, then
converting it to a "Stream A" as Aaron said, so you can give this
witness; but the problem is that "Stream A" is informative; and what
you have is "X", which is informative, but not enough to allow you to
build such a stream, and "wf(X)" which is non-informative (as in
Prop), so you cannot use it to build a "Stream A".

As Adam said, you can use some axioms.
Another work around is to make "wf" informative (in Type).
Its dual workaround is to put "Stream A" as non informative
"CoInductive PStream A: Prop := Pstream: A -> PStream A -> PStream A."

Some other remarks (not very pertinent):

"Definition derv (a : A) (t tx : Tree) := dervaux a t = Some tx."
is simpler to me than using an inductive type.

"CoInductive wf: tree -> Prop :=
  wftree : forall f,
  -> inhabited f
  -> (forall a ta, f a = Some ta -> wf ta)
  -> wf (Node f)."
skips the "t=Node f".