The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Herman,

there is a systematic way to address situations like this - Nils Anders 
Danielsson has recently written a paper about this (at PAR 10), see
http://www.cs.nott.ac.uk/~nad/publications/danielsson-productivity.pdf
The examples are in Agda but hopefully they can be translated to Coq. 

Cheers,
Thorsten

On 21 Oct 2010, at 17:18, Herman Geuvers wrote:

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