[Agda] Confused about rewriting

[Ulf Norell]

The problem is that at the point you invoke the rewrite the goal isn't (*),
but

  ∃[ m₁ ] (suc (suc (m + (m + 0))) ≡ m₁ + (m₁ + 0))   (**)

with a fresh variable m₁ in the right-hand side.

/ Ulf


On Sun, Mar 18, 2018 at 1:15 AM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> 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/20180318/9ef18bd2/attachment.html>