<div dir="ltr">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.<div><br></div><div style>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.</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Apr 20, 2013 at 12:53 AM, Yasuyuki Ogawa <span dir="ltr"><<a href="mailto:lost_dog@nifty.com" target="_blank">lost_dog@nifty.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi! I'm studying Agda with CPDT, and now reading<br>
"Infinite Data and Proofs" section.<br>
<br>
(<a href="http://adam.chlipala.net/cpdt/html/Coinductive.html" target="_blank">http://adam.chlipala.net/cpdt/html/Coinductive.html</a>)<br>
<br>
But I can't prove a following infinite proof...<br>
In CPDT, this requires StreamEq, so I tried it but<br>
I couldn't. Can anyone help me?<br>
<br>
zeros : Stream N<br>
zeros = cons 0 (# zeros)<br>
<br>
ones : Stream N<br>
ones = cons 1 (# ones)<br>
<br>
map : forall {A B} -> (A -> B) -> Stream A -> Stream B<br>
map f (cons x xs) = cons (f x) (# map f (b xs))<br>
<br>
ones' : Stream N<br>
ones' = map suc zeros<br>
<br>
theorem-ones-eq : ones == ones'<br>
theorem-ones-eq = ?<br>
<br>
Thank you!<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>