The Coq mailing list

[Herman Geuvers <herman AT cs.ru.nl>]

Dear all,

To clarify my mail, I append a small Coq file indicating what I am 
trying to prove.

NB. I know that the Lemma even_zip can be proved in a different way, so 
the point of this file is not that I am stuck with even_zip.
I am interested in using  the setoid rewriting or the standard rewrite 
(using Leibniz eq) for streams. This is a kind of minimal file where 
this feature occurs and Coq doesn't accept my proof because of the 
guardedness constraint.
(So maybe the answer is: You can't use (setoid) rewriting in Coq for 
this purpose.)

Thanks

Herman Geuvers
=====================================

Set Implicit Arguments.
Require Import Streams.
Require Export Setoid.
Require Export Relation_Definitions.

Infix "::" := Cons (at level 60, right associativity) : richstream_scope.
Infix "==" := EqSt (at level 60) : richstream_scope.
Ltac coinduction proof :=
 cofix proof; intros; constructor;
  [ clear proof | try (apply proof; clear proof) ].
Open Scope richstream_scope.

Section Zip.
Variable A: Type.

CoFixpoint zip(s: Stream A)(t: Stream A) : Stream A  :=
 match s with
   | x :: xs => x :: (zip t xs)
 end.

CoFixpoint even(s: Stream A) := hd s :: (even (tl(tl s))).

End Zip.

Section Congruence.
Variable A:Type.

Axiom ext : forall s t :Stream A, s == t -> s = t.

Lemma leib : forall s t :Stream A, s = t -> s == t.
Proof.
intros s t Heq; rewrite Heq; apply EqSt_reflex.
Qed.

Lemma congruence : forall f : Stream A -> Stream A, forall s t :Stream A,
 s == t -> f s == f t.
(* Impossible without ext *)
Proof.
intros f s t H. rewrite (ext H). apply EqSt_reflex.
Qed.
(* This works, because we don't do the proof by coinduction, but
  by the property of Leibiz equality *)

Lemma even_zip_using_ext : forall (s t: Stream A), even (zip s t) == s.
Proof.
intros s t.
coinduction H; destruct s; destruct t.
auto.
rewrite (ext H). apply EqSt_reflex.
(* Proof completed, but not guarded *)
Abort.

End Congruence.

Section EquivRel.

Add Parametric Relation A : (Stream A) (@EqSt A)
reflexivity proved by (@EqSt_reflex A)
symmetry proved by (sym_EqSt (A:=A))
transitivity proved by (trans_EqSt (A:=A))
as stream_eq.

Add Parametric Morphism A : (@zip A) with
signature (@EqSt A) ==> (@EqSt A) ==> (@EqSt A)
as stream_zip.
Admitted.

Add Parametric Morphism A : (@tl A) with
signature (@EqSt A) ==> (@EqSt A)
as stream_tl.
Proof.
intros s t Heq; case Heq; auto.
Qed.


Add Parametric Morphism A : (@even A) with
signature (@EqSt A) ==> (@EqSt A)
as stream_even.
Admitted.

Lemma even_zip : forall (A:Type)(s t: Stream A), even (zip s t) == s.
Proof.
intro A.
coinduction H; destruct s; auto.
rewrite H.
reflexivity.
(* Qed. ? Not Guarded *)
Abort.


Lemma even_zip' : forall (A:Type)(s t: Stream A), even (zip s t) == s.
Proof.
intro A.
coinduction H; destruct s; auto.
apply congruence.
apply H.
(* Qed. ? Not Guarded *)
Abort.

End EquivRel.