[Agda] Confused about rewriting

[Philip Wadler]

Thanks, Nils! I had spotted that I should avoid 2 * m + 1 and instead write
1 + 2 *m, but not that 1 + m * 2 eliminates the need for my lemma. 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 20 March 2018 at 07:53, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2018-03-18 13:46, Philip Wadler wrote:
>
>> So, is the proof that worked the best one, or is there a neater way to
>> do it?
>>
>
> I suggest that you replace "2 * m" with "m * 2". Then the following
> proof works:
>
>   ∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ m * 2)
>   ∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + m * 2)
>
>   ∃-even even-zero    = zero , refl
>   ∃-even (even-suc o) = map suc (cong suc) (∃-odd  o)
>   ∃-odd  (odd-suc  e) = map id  (cong suc) (∃-even e)
>
> (The map function here comes from Data.Product.)
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180320/ec2ad13d/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180320/ec2ad13d/attachment.ksh>