[Agda] Confused about rewriting

[Philip Wadler]

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

.   \ 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/

On 18 March 2018 at 04:16, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/210a042f/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/210a042f/attachment.ksh>