[Agda] Confused about rewriting

[Philip Wadler]

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

  suc (suc (m + (m + 0))) ≡ suc (m + suc (m + 0))      (*)

If I use

  sym (+-suc m (m + 0)) : suc (m + (m + 0)) ≡ m + suc (m + 0)

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?

Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/cbf68af1/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: RewriteWTF.agda
Type: application/octet-stream
Size: 1253 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/cbf68af1/attachment.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/cbf68af1/attachment.ksh>