The Coq mailing list

[Dimiter Milushev <Dimiter.Milushev AT cs.kuleuven.be>]

Cedric,
thank you very much! I owe you ;)

On Wed, Mar 9, 2011 at 12:30 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> Le Tue, 8 Mar 2011 13:47:08 +0100,
>Â dimiter.milushev AT cs.kuleuven.be
>  a écrit :
>
> I have rewritten some minor parts to have simpler (but equivalent and
> keeping the same signature) definitions, but if you understand the
> proof, you should be able to have one with your definitions.
>
> The "Critical" proof has been completely rewritten, without trying to
> follow the one you did, so you may get lost, and some of your
> technical facilities may become useless, or may be used to simplify my
> proof.
>
>>>>>>>>>>>>>>>>>>>>>>>>
> Require Import Coq.Lists.Streams.
> Set Implicit Arguments.
> Require Import Setoid.
>
> Parameter A : Set.
> Parameter f : A -> A.
>
> CoInductive Tree : Set :=
>  | Node : (A -> option Tree) -> Tree.
>
> Inductive inhabited (f : A -> option Tree) : Prop :=
> inhabited_intro: forall a t, f a = Some t -> inhabited f.
>
> CoInductive wf: Tree -> Prop :=
>  wftree : forall f,
>  inhabited f
>  -> (forall a ta, f a = Some ta -> wf ta)
>  -> wf (Node f).
>
> Inductive derv (a: A): Tree -> Tree -> Prop :=
>  derva : forall (f: A -> option Tree) (tx : Tree),
>  f a = Some tx -> derv a (Node f) tx.
>
> Lemma wfsubtree : forall t a ta, wf t -> derv a t ta -> wf ta.
> Proof.
> Admitted.
>
> CoInductive elem : Stream A -> Tree -> Prop :=
>  el: forall w : Stream A, forall X X' : Tree, forall a : A,
>  derv a X X' ->
>  elem w X' ->
>  elem (Cons a w) X.
>
> (* Some Helpers *)
> Lemma elem_cons: forall (X Xa: Tree) (a : A) (w : Stream A), derv a X
> Xa -> (elem (Cons a w) X <-> elem w Xa).
> Proof.
> Admitted.
>
> Lemma elem2derv : forall a w X,
>  elem (Cons a w) X -> exists Xa, derv a X Xa.
> Proof.
> Admitted.
>
> CoInductive IPP : Tree -> Tree -> Prop :=
>  Tpp : forall X Y,
>  (forall a : A, forall Xa, derv a X Xa
>    -> (exists Yb, derv (f a) Y Yb /\ IPP Xa Yb))
>    -> IPP X Y.
>
> Definition fIPP (P :Tree -> Tree -> Prop) (X Y : Tree) : Prop :=
>  (forall a : A, forall Xa, derv a X Xa
>    -> (exists Yb, derv (f a) Y Yb /\ P Xa Yb)).
>
> Lemma IPPunfold : forall X Y, IPP X Y <-> fIPP IPP X Y.
> Proof.
> Admitted.
>
> CoFixpoint fl (s : Stream A) : Stream A:=
>  match s with Cons h t => Cons (f h) (fl t) end.
>
> Definition wfHP (X:Tree) (Y:Tree) : Prop:=
> wf X -> wf Y -> forall x, elem x X -> elem (fl x) Y.
>
> (* Technicalities to get the proofs done *)
> Definition SS (s : Stream A) :=
>  match s with
>  | Cons x t => Cons x t
>  end.
>
> Lemma SSid : forall s:Stream A, s = SS s.
> Proof.
>  intros.
>  destruct s.
>  reflexivity.
> Qed.
>
> Lemma Crucial : forall X Y : Tree, forall x,
>  wf X -> wf Y -> IPP X Y ->  elem x X -> elem (fl x) Y.
> Proof.
>  intros.
>  revert X x H2 Y H1 H H0.
>  cofix CoindHyp.
>  intros _ _ [s X X' a Ha Hs].
>  intros Y HIPP; revert X Y HIPP Ha.
>  intros _ _ [X Y H] Ha.
>  generalize (H a X' Ha); clear H.
>  intros [Y' [Ha' HIPP]] wfX wfY.
>  cut (Cons (f a) (fl s) = fl (Cons a s)).
>  intros [].
>  split with Y'; auto.
>  cut (forall A A' a, derv a A A' -> wf A -> wf A').
>   intro H.
>   apply CoindHyp with X'; auto.
>    clear -wfX Ha H.
>    exact (H X X' a Ha wfX).
>   clear -wfY Ha' H.
>   exact (H Y Y' (f a) Ha' wfY).
>  clear.
>  intros _ _ a [f A'].
>  intros Heq H.
>  inversion_clear H.
>  exact (H1 a A' Heq).
>  clear.
>  change (let (b, c) := fl (Cons a s) in Cons b c = fl (Cons a s)).
>  destruct (fl (Cons a s)).
>  split.
> Qed.
>
>
>