The Coq mailing list

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

Correction of my previous post: I have a proof, your lemma is not
provable:
No where it is said that A is inhabited (only wf(X) ensures it, but it
is BELOW the "exists w"); so at least, try to prove:

 Lemma wfExStr: forall X : Tree, wf(X) -> exists w,
 elem w X.

and not:

 Lemma wfExStr: forall X : Tree, exists w,
 wf(X)->  elem w X.

or assume that A is inhabited (and probably consider using excluded
middle).

Here are two developpements (with the "corrected" version).
Of course I used axioms.
For the first developpement, I did a specific axiom;
for the second, I used classical choice axiom (which allows to get
around the problem of requiring an "informative coinductive" to build a
"non-informative inductive").

I don't know if "choice axiom" belongs to the scary solutions, Adam
spoke of.

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

>>>>>>>>>>>>>>>
CoInductive elem2 : Tree -> Prop :=
  el2: forall X X' : Tree, forall a : A,
    derv a X X' ->
    elem2 X' ->
    elem2 X.

CoInductive sim: forall T s, elem s T -> elem2 T -> Prop :=
  SIM: forall w X X' a (da: derv a X X') (next: elem w X') (next2:
elem2 X'), sim (el da next) (el2 da next2).

(* The following axiom seems harmless, but quite specific *)
Axiom extraction: forall T e2, exists s, exists e:elem s T, sim e e2.

Lemma wfExStr: forall X : Tree, wf(X) -> exists w,
 elem w X.
 Proof.
 intros X wfX.
 cut (elem2 X).
  intros H; case (extraction H) as [w [K L]].
  now exists w.
 revert X wfX; cofix; intros X [f Heq [a [X' HaX']] wfX_].
 split with X' a.
  split.
  rewrite Heq.
  simpl.
  assumption.
 apply wfExStr.
 exact (wfX_ _ _ HaX').
Qed.
<<<<<<<<<<<<<<<
Require Import ClassicalChoice.

Lemma select:
 exists f: forall T, wf T -> (A*{T: Tree|wf(T)}),
 forall T wfT, let (a, HT') := f T wfT in
               let (T', _) := HT' in
               dervaux a T = Some T'.
 Proof.
 case (choice (fun (T:{T: Tree | wf(T)}) (p: A*{T: Tree|wf(T)}) =>
               let (T, _) := T in
               let (a, HT') := p in
               let (T', _) := HT' in
               dervaux a T = Some T')).
  intros [T [f Heq [a [T' HaT']] next]].
  rewrite Heq; clear Heq.
  now exists (a, exist (fun T => _) T' (next _ _ HaT')).
 intros f Hf.
 exists (fun T wfT => f (exist _ T wfT)).
 intros T wfT.
 exact (Hf (exist _ T wfT)).
Qed.

Definition wfExStr: forall X : Tree, wf(X) -> exists w,
 elem w X.
 Proof.
 case select as [sel Hsel].
 set (str := cofix str X wfX: Stream A :=
             let (a, next) := sel X wfX in
             let (X', wfX') := next in
             Cons a (str X' wfX')).
 assert (forall X wfX, (let (a, b) := str X wfX in Cons a b) = str X
wfX). now intros X wfX; destruct (str X wfX).
 intros X wfX; exists (str X wfX).
 revert X wfX; cofix.
 intros X wfX.
 case H; simpl.
 generalize (Hsel X wfX).
 destruct (sel X wfX).
 destruct s.
 fold str.
 split with x.
  now split.
 apply wfExStr.
Qed.
>>>>>>>>>>>>>>>>>>>>>
Le Sat, 26 Feb 2011 00:11:41 +0100,
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 a écrit :

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