[Haskell-cafe] Proof format

[Brent Yorgey]

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