On Wed, May 19, 2010 at 01:12:16PM +0000, R J wrote:

Is this how a rigorous Haskeller would lay out the proofs of the following theorems? This is Bird 1.4.6. (i) Theorem: (*) x = (* x) Proof: (*) x = {definition of partial application} \y -> x * y = {commutativity of "*"} \y -> y * x = {definition of "(* x)"} (* x) (ii) Theorem: (+) x = (x +) Proof: (+) x = {definition of partial application} \y -> x + y = {definition of "(x +)"} (x +)

I would put each step and each {reason} on a separate line (or perhaps there is something wrong with the way your mail client handles newlines?) but other than that these look good.

(iii) Theorem: (-) x /= (- x) Proof: (-) x = {definition of partial application} \y -> x - y /= {definition of prefix negation, which is not a section} (- x)

This is not a proof. To prove an inequality like this you should simply give a counterexample. -Brent