[Agda] Infinite proofs

[Daniel Peebles]

You can't prove them equal in Agda, and you probably shouldn't be able to
in Coq either (it breaks subject reduction) but you can anyway.

The usual solution is to define a custom equivalence relation
(bisimulation) that's also coinductive and indexed by your stream, and then
to use that instead of equality. If we had a fancier notion of equality,
this would work, but with plain old intensional equality and nothing else,
it shouldn't be possible.


On Sat, Apr 20, 2013 at 12:53 AM, Yasuyuki Ogawa <lost_dog at nifty.com> wrote:

> Hi! I'm studying Agda with CPDT, and now reading
> "Infinite Data and Proofs" section.
>
> (http://adam.chlipala.net/cpdt/html/Coinductive.html)
>
> But I can't prove a following infinite proof...
> In CPDT, this requires StreamEq, so I tried it but
> I couldn't. Can anyone help me?
>
> zeros : Stream N
> zeros = cons 0 (# zeros)
>
> ones : Stream N
> ones = cons 1 (# ones)
>
> map : forall {A B} -> (A -> B) -> Stream A -> Stream B
> map f (cons x xs) = cons (f x) (# map f (b xs))
>
> ones' : Stream N
> ones' = map suc zeros
>
> theorem-ones-eq : ones == ones'
> theorem-ones-eq = ?
>
> Thank you!
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130420/d959537a/attachment.html