[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/

[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

Post by 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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[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/

Post by 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

Post by 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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

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.)

[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/

Post by Nils Anders Danielsson

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
∃-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