Functional proofs (Haskell)

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.

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.

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.

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