Functional proofs (Haskell)

21
votes

I failed at reading RWH; and not one to quit, I ordered Haskell: The Craft of Functional Programming. Now I'm curious about these functional proofs on page 146. Specifically I'm trying to prove 8.5.1 sum (reverse xs) = sum xs. I can do some of the induction proof but then I get stuck..

HYP:

sum ( reverse xs ) = sum xs

BASE:

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

INDUCTION:

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

So now I'm just trying ot prove that Left sum ( reverse xs ++ [x] ) is equal to Right x + sum xs, but that isn't too far off from where I started sum ( reverse (x:xs) ) = sum (x:xs).

I'm not quite sure why this needs to be proved, it seems totally reasonable to use the symbolic proof of reverse x:y:z = z:y:x (by defn), and because + is commutative (arth) then reverse 1+2+3 = 3+2+1,

4
haskellfunctional-programmingproof
There's a song that goes like "addition is commutative, right!" It applies to this situation. – jrockway
@jrockway, thanks for the downvote leave it to you drop by with a negative vote and a side-tracking remark. – Evan Carroll
"it seems totally reasonable to use the symbolic proof of reverse x:y:z = z:y:x (by defn), and because + is commutative (arth) then reverse 1+2+3 = 3+2+1." Well, this gives you a proof for lists of length 3, but not for any other lengths. – Alexey Romanov
@jrockway: New Math, by Tom Lehrer. "And you know why four plus minus one plus ten is fourteen minus one? 'Cause addition is commutative, right." – Antal Spector-Zabusky
Yup. Thought the reference was too obscure even for this crowd :) – jrockway

4 Answers

24
votes
sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

However, there are underlying assumptions of associativity and commutativity that are not strictly warranted and this will not work properly for a number of numerical types such as Float and Double where those assumptions are violated.

Lemma: sum (xs ++ ys) == sum xs + sum ys given the associativity of (+)

Proof:

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum
6
votes

Basically you need to show that

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

which then easily leads to 

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

The problem is to show that sum distributes over list concatenation.

4
votes

Use the definition of a sum to break up (sum reverse xs ++[x]) into x + sum(reverse(xs)), and using your inductive hypothesis you know sum(reverse(xs)) = sum(xs). But I agree, induction is overkill for a problem like this.

3
votes

Here's where I think you're stuck. You need to prove a lemma that says

sum (xs ++ ys) == sum xs + sum ys

To prove this law you will have to assume that addition is associative, which is true only for integers and rationals.

Then, you will also need to assume that addition is commutative, which is true for integers and rationals but also for floats.

Digression: The style of your proofs looks very strange to me. I think you will have an easier time writing these kinds of proofs if you use the style in Graham Hutton's book.