The Coq mailing list

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

Le Fri, 22 Oct 2010 14:11:38 +0200,
Herman Geuvers 
<herman AT cs.ru.nl>
 a écrit :

I sent some patch suggestions to your developpement.

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

Tactic Notation "cosimpl" ident(A) := (simpl; fold (@zip A); fold
(@even A)).
(* this is not a very convenient notation as you need to give the
 * type; maybe some improvement can be done
 *)

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

(* I may be wrong, the cofixpoint is meant to be some producting
 * process; in your proof script, the head is well produced;
 * but the tail has no production guarantee, since it is obtained by
 * rewritting.
 *
 * consider:
 * Parameter A: Type.
 * Parameter f: Stream A -> Stream A.
 * CoFixpoint fid (s: Stream A) := hd s :: (f (fid (tl s))).
 *
 * Coq is not very happy with this definition.
 *
 * Maybe that an axiom of the form:
 * "forall A (f: Stream A -> Stream A) B (g: B -> A),
 *  exists Recfg: Stream B -> Stream A,
 *  forall (s: Stream B), Recfg s = (g (hd s))::(f (Recfg (tl s)))"
 * can save you…
 *)


Lemma even_zip_using_ext : forall (s t: Stream A), even (zip s t) == s.
Proof.
 (* if you first introduce s and t, then using "coinduction" will block
  * you since s and t will be fixed
  * (generated hypothesis will be "even (zip s t) == s" for not yet
  * destroyed s and t)
  *)
 coinduction H; destruct s; destruct t.
  auto.
 cosimpl A. (* this notation is to be improved *)
 apply H.
Qed.
(* by the way do you know the "Guarded." instruction?
 * If not, it can be very usefull; take a look in the manual.
 *
 * by the way2, is there a trick to make it available in
 * in a tactic?
 * Having a [Notation Tactic "guard" tactic(t) := (t; Guarded).]
 * could be handy.
 *)

(* The rest of the file can be solved the same way without using
 * rewriting; for these examples, rewritting is not very natural;
 * maybe you can provide better examples?
 *)