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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
