Philip Wadler

2018-03-18 00:15:05 UTC

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/

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/