The Coq mailing list

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

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.