The Coq mailing list

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

Dear all,

We are trying to prove a number of basic results over streams in Coq, 
typically staring from results that are standard in (infinitary) term 
rewriting, like defining zip, even and odd and showing that
   zip (even s)(odd s) == s
Here, == is the coinductively defined equality over streams, EqSt in the 
standard library.

To make this all smooth and to be able to automate these proofs, we 
would like to use Setoid Rewriting.
Now, it is straightforward to declare == as an equivalence relation 
that  is a congruence wrt functions like zip and even.
Then one can go and do rewriting in proofs, but the proofs can't be 
saved, becuase -- according to Coq's mechanism -- they are not guarded.

Has anyone encountered this situation before and found a solution?

One thing I have tried is to just assume that == is Leibniz equality on 
streams, so one can use the rewrite tactic itself.

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

That doesn't help either, because the final proof of a statement 
involving == will not be guarded still.

For specific functions, like zip even and odd, there is always a way 
around the problem, by unfolding its definition and doing case analysis. 
However, we would like to find a generic method. (Possibly by assuming 
an axiom.)

Thanks

--
Herman Geuvers