The Coq mailing list

[dimiter.milushev AT cs.kuleuven.be]

Hello,

Firstly, apologies for sending off an earlier less structured version of this
question.

Now, as a followup of a previous question I have isolated the main problem:
applying the coinduction hypothesis in the following lemma:

Lemma Crucial : forall X Y : Tree, forall x,
 wf X -> wf Y -> IPP X Y ->  elem x X -> elem (fl x) Y

where wf, IPP, elem are all coinductive predicates,
and fl applies a function to a stream in pointwise manner.

The Coq development is given below, and the error produced is:

Sub-expression "H14
                (let H4 := elem_cons x0 H6 in
                 let H3 :=
                   (fun lemma : elem (Cons a x0) X <-> elem x0 Xa =>
                    subrelation_id_morphism iff_impl_subrelation
                      (elem (Cons a x0) X) (elem x0 Xa) lemma) H4 H3 in
                 Crucial Xa Yb x0 (wfsubtree H H6)
                   (let H6 :=
                      eq_ind_r (fun a : A => derv a Y Yb)
                        (eq_ind x1 (fun x0 : A => derv x0 Y Yb) H11
                           (f a) H8) H8 in
                    wfsubtree H0 H6) H12 H3)" not in guarded form (should
be a constructor, an abstraction, a match, a cofix or a recursive call).

My only guess is that the call to CoindHyp might not be properly guarded.
But it could be that I'm doing coinduction over two data types at the same
time,
and Coq does not recognise this.

In principle, is it possible to do such proofs in Coq?

Any help will be appreciated.

Greetings,
Dimiter


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

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

(* 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.
 cofix CoindHyp.
 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 elem_cons with (w := x) in H4.
 rewrite H4 in H3.
 apply  CoindHyp with (X := Xa) (Y := Yb); auto.
 Guarded.
Sub-expression "H14
                (let H4 := elem_cons x0 H6 in
                 let H3 :=
                   (fun lemma : elem (Cons a x0) X <-> elem x0 Xa =>
                    subrelation_id_morphism iff_impl_subrelation
                      (elem (Cons a x0) X) (elem x0 Xa) lemma) H4 H3 in
                 Crucial Xa Yb x0 (wfsubtree H H6)
                   (let H6 :=
                      eq_ind_r (fun a : A => derv a Y Yb)
                        (eq_ind x1 (fun x0 : A => derv x0 Y Yb) H11
                           (f a) H8) H8 in
                    wfsubtree H0 H6) H12 H3)" not in guarded form (should
be a constructor, an abstraction, a match, a cofix or a recursive call).

>>>>>>>>>>>>>>>>>