coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
- To: Herman Geuvers <herman AT cs.ru.nl>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Equational Reasoning over streams
- Date: Thu, 21 Oct 2010 17:23:18 +0100
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
>
>
- [Coq-Club] recursive Ltac definitions, Aaron Bohannon
- [Coq-Club] Re: recursive Ltac definitions,
Aaron Bohannon
- [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams, Thorsten Altenkirch
- Re: [Coq-Club] Equational Reasoning over streams,
David Leduc
- Re: [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams, AUGER Cedric
- Re: [Coq-Club] Equational Reasoning over streams,
Keiko Nakata
- Re: [Coq-Club] Equational Reasoning over streams, David Leduc
- Re: [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams,
David Leduc
- Re: [Coq-Club] Equational Reasoning over streams, Thorsten Altenkirch
- [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] recursive Ltac definitions, Adam Chlipala
- [Coq-Club] Re: recursive Ltac definitions,
Aaron Bohannon
Archive powered by MhonArc 2.6.16.