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..
sum ( reverse xs ) = sum xs
sum ( reverse [] ) = sum []
Left = sum ( [] ) (reverse.1)
= 0 (sum.1)
Right = 0 (sum.1)
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,
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