The Coq mailing list

[Dimiter Milushev <dimiter.milushev AT googlemail.com>]

Hi all and thanks a lot for the help so far.
I have a continuation of my previous question.

In the following development, the main goal is to prove Lemma EndIt.
To that end lemmas OtherHalf and ShortHalf  can be used.
We have tried several approaches,
but always get an error similar to the one shown at the end of proof
attempt for Lemma ShortHalf.
(The admitted Lemmas are omitted for readability, the only problem is
with Lemma ShortHalf)

We have a paper proof that Lemma EndIt holds, i.e. we believe that it
is correct.
Are we doing something conceptually wrong here?

I would greatly appreciate any suggestions.
Greetins,
Dimiter

>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
Require Import Coq.Lists.Streams.
Set Implicit Arguments.
Require Import Setoid.

Parameter A : Set.
Parameter f : A -> A.

CoInductive c : Stream A -> Stream A -> Prop :=
  | C0 : forall h1 h2 t1 t2,
    c t1 t2 -> h2 = f(h1) -> c (Cons h1 t1) (Cons h2 t2).

CoInductive Tree : Set :=
  | Node : (A -> option Tree) -> Tree.

Definition inhabited (f : A -> option Tree) : Prop :=
  exists a : A, exists t : Tree, f a = Some t.

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

Definition dervaux (a : A) (t: Tree): option Tree :=
  match t with Node f => f a end.

Inductive derv : A -> Tree -> Tree -> Prop :=
  derva : forall (a : A) (t tx : Tree),
    dervaux a t = Some tx -> derv a t 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 derv_det : forall a X Xa Xa', derv a X Xa -> derv a X Xa' -> Xa = Xa'.
Proof.
Admitted.


Lemma derv_ex_all_prop : forall a X P,
  (exists Xa, (derv a X Xa /\ P a X Xa))
    -> forall Xa, derv a X Xa -> P a X Xa.
Proof.
Admitted.

Lemma elem2derv : forall a w X,
  elem (Cons a w) X -> exists Xa, derv a X Xa.
Proof.
Admitted.

Lemma f2derv: forall X Xa a f0,
  X = Node f0 -> f0 a = Some Xa -> derv a X Xa.
Proof.
Admitted.


Lemma wfExDerv: forall X,
  wf(X) -> exists a, exists Xa, derv a X Xa.
Proof.
Admitted.


(*Contribution by Auger*)
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; destruct (extraction H) as [w [K L]].
 now exists w.
 revert X wfX; cofix; intros X [f1 Heq [a [X' HaX']] wfX_].
 split with X' a.
 split.
 rewrite Heq.
 simpl.
 assumption.
 apply wfExStr.
 exact (wfX_ _ _ HaX').
 Qed.
(*End Contributions by Auger*)

Lemma derv2elem: forall a X Xa,
wf(X) -> derv a X Xa -> exists w, elem w Xa.
Proof.
Admitted.


Definition HP (X:Tree)  (Y: Tree) : Prop :=
      forall x: Stream A, (elem x X) ->  exists y: (Stream A), (elem y
Y) /\ (c x y).

CoInductive IPP : Tree -> Tree -> Prop :=
  Tpp : forall X Y,
   (forall a : A, forall Xa, derv a X Xa
      -> (exists b : A, b = f(a) /\ exists Yb, derv b 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 b : A, b = f(a) /\ exists Yb, derv b 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.


Axiom A2: forall X Y x, wfHP X Y -> elem x X -> exists y, y = fl(x) /\ elem y 
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 ShortHalf : forall X Y : Tree, forall x,
  wf X -> wf Y -> IPP X Y ->  elem x X -> elem (fl x) Y.
Proof.
  cofix.
  intros.
  destruct x.
  apply IPPunfold in H1.
  unfold fIPP in H1.
  assert (elem (Cons a x) X); auto.
  apply elem2derv in H2.
  destruct H2 as [Xa H4].
  destruct H1 with (a := a) (Xa := Xa); auto.
  destruct H2 as [H5 [Yb [H6 H7]]].
  rewrite H5 in H6.
  assert (wf Xa); try apply wfsubtree with (t := X) (a := a) (ta := Xa); auto.
  assert (wf Yb); try (rewrite <- H5 in H6;  apply wfsubtree with (t
:= Y) (a := x0) (ta := Yb);   auto).
  replace (fl (Cons a x)) with (SS (fl (Cons a x))).
  unfold fl.
  unfold SS.
  fold fl.
  apply elem_cons with (w := fl x) in H6.
  apply H6.
  apply ShortHalf with (X := Xa) (Y := Yb); auto.
  apply elem_cons with (w := x) in H4.
  tauto.
  rewrite SSid.
  auto.
Admitted.

(*
Qed. At end of above proof results in following error:

Sub-expression "let H6 :=
                  eq_ind x1 (fun x0 : A => derv x0 Y Yb) H9 (f a) H6 in
                let H2 := wfsubtree H H4 in
                let H8 :=
                  let H7 := eq_ind_r (fun a : A => derv a Y Yb) H6 H6 in
                  wfsubtree H0 H7 in
                Morphisms.reflexive_proper elem (fl (Cons a x0))
                  (SS (fl (Cons a x0))) (SSid (fl (Cons a x0))) Y Y
                  (Morphisms.eq_proper_proxy Tree Y)
                  (let H7 := elem_cons (fl x0) H6 in
                   let H9 := match H7 with
                             | conj _ x0 => x0
                             end in
                   H9
                     (ShortHalf Xa Yb x0 H2 H8 H10
                        (let H4 := elem_cons x0 H4 in
                         and_ind
                           (fun (H10 : elem (Cons a x0) X -> elem x0 Xa)
                              (H11 : elem x0 Xa -> elem (Cons a x0) X) =>
                            and_ind
                              (fun
                                 (_ : elem (Cons (f a) (fl x0)) Y ->
                                      elem (fl x0) Yb)
                                 (_ : elem (fl x0) Yb ->
                                      elem (Cons (f a) (fl x0)) Y) =>
                               let H13 := H10 H3 in let H14 := H11 H13 in H13)
                              H7) H4)))" not in guarded form (should be a
constructor, an abstraction, a match, a cofix or a recursive
call).
Recursive definition is:
"fun (X Y : Tree) (x : Stream A) (H : wf X) (H0 : wf Y)
   (H1 : IPP X Y) (H2 : elem x X) =>
 match x as s return (elem s X -> elem (fl s) Y) with
 | Cons a x0 =>
     fun H3 : elem (Cons a x0) X =>
     let H4 :=
       fun X0 Y0 : Tree => match IPPunfold X0 Y0 with
                           | conj x1 _ => x1
                           end in
     let H5 := H4 X Y H1 in
     let H6 := H3 in
     let H7 := elem2derv H3 in
     match H7 with
     | ex_intro Xa H8 =>
         let e := H5 in
         match e a Xa H8 with
         | ex_intro x1 (conj H10 (ex_intro Yb (conj H13 H14))) =>
             let H15 :=
               eq_ind x1 (fun x2 : A => derv x2 Y Yb) H13 (f a) H10 in
             let H16 := wfsubtree H H8 in
             let H17 :=
               let H17 := eq_ind_r (fun a0 : A => derv a0 Y Yb) H15 H10 in
               wfsubtree H0 H17 in
             Morphisms.reflexive_proper elem (fl (Cons a x0))
               (SS (fl (Cons a x0))) (SSid (fl (Cons a x0))) Y Y
               (Morphisms.eq_proper_proxy Tree Y)
               (let H18 := elem_cons (fl x0) H15 in
                let H19 := match H18 with
                           | conj _ x3 => x3
                           end in
                H19
                  (ShortHalf Xa Yb x0 H16 H17 H14
                     (let H20 := elem_cons x0 H8 in
                      and_ind
                        (fun (H21 : elem (Cons a x0) X -> elem x0 Xa)
                           (H22 : elem x0 Xa -> elem (Cons a x0) X) =>
                         and_ind
                           (fun
                              (_ : elem (Cons (f a) (fl x0)) Y ->
                                   elem (fl x0) Yb)
                              (_ : elem (fl x0) Yb ->
                                   elem (Cons (f a) (fl x0)) Y) =>
                            let H25 := H21 H6 in let H26 := H22 H25 in H25)
                           H18) H20)))
         end
     end
 end H2".
*)


Lemma OtherHalf : forall X Y : Tree,
  wf X -> wf Y -> IPP X Y -> wfHP X Y.
Proof.
Admitted.


Lemma EndIt : forall X Y : Tree,
  wf X -> wf Y -> IPP X Y -> HP X Y.
Proof.
Admitted.
 >>>>>>>>>>>>>>>>>>>>

On Sun, Feb 27, 2011 at 6:58 PM, Dimiter Milushev
<Dimiter.Milushev AT cs.kuleuven.be>
 wrote:
> Thanks a lot for your competent opinions and extremely fast response!
> All the replies made me think and learn something new.
> I really appreciate the your help.!
>
> Special thanks to Cedric!
>
> Greetings,
> Dimiter
>
> 2011/2/26 AUGER Cedric 
>Â <Cedric.Auger AT lri.fr>:
>> Le Sat, 26 Feb 2011 01:18:28 +0100,
>> Pierre-Marie Pédrot 
>>Â <pierremarie.pedrot AT ens-lyon.fr>
>>  a écrit :
>>
>>> On 26/02/2011 00:11, AUGER Cedric wrote:
>>> > 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."
>>>
>>> If A is countable, you can still retrieve some information through the
>>> coutable epsilon principle, as not being of the form « None » is
>>> decidable, thus proving it without any other change whatsoever.
>>
>> There are always some alternative workaround I miss…
>>
>>>
>>> If you put Stream in Prop, though I am not sure, I think you are still
>>> going to face some problems and you will need to use some weaker form
>>> of the choice axiom (looks a lot like dependent choice in this case).
>>>
>>
>> I don't think we require dependent choice in this case, but of course
>> you will lack the Stream library, and won't be able to make functions
>> from Stream in Prop to any Type.
>>
>>> Otherwise, placing inhabited in Type should be sufficient since this
>>> is the only point where you need to retrieve a witness (the other
>>> properties are not really informative), and you can even show
>>> existence of your stream in Type (with sig) instead of in Prop (with
>>> ex).
>>
>> Not sure, as inhabited is accessed via wf which is in Prop.
>>
>>>
>>> PMP
>>>
>>
>>
>