<div dir="ltr">Thanks, Ulf. I see---the problem is that the rewrite happens before m1 is instantiated to (suc m). So, is the proof that worked the best one, or is there a neater way to do it? Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 18 March 2018 at 04:16, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>The problem is that at the point you invoke the rewrite the goal isn't (*), but<br><br>  ∃[ m₁ ] (suc (suc (m + (m + 0))) ≡ m₁ + (m₁ + 0))   (**)<br><br>with a fresh variable m₁ in the right-hand side.<br><br></div>/ Ulf<br><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Sun, Mar 18, 2018 at 1:15 AM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">Attached find a program that gives two proofs that if n is even, then there exists an m such that n equals 2*m.  Or rather, a proof and a non-proof. The equation I need to prove is<div><br></div><div><div>  suc (suc (m + (m + 0))) ≡ suc (m + suc (m + 0))      (*)</div><div><div><br></div><div>If I use<div><br></div><div>  sym (+-suc m (m + 0)) : suc (m + (m + 0)) ≡ m + suc (m + 0)</div><div><br></div><div>to rewrite then it works perfectly, rewriting the lhs of (*). But if I remove the sym then it fails to work, even though it should rewrite the rhs of (*). What am I doing wrong?</div><div><br></div><div>Cheers, -- P</div><div><div><br></div><div><br clear="all"><div><div class="m_2837295858144990846m_-1222012575685472962gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
</div></div></div></div></div></div>
<br></div></div>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>