Structural Induction and Induction Hypothesis in Haskell

Question

I am trying to prove 'ns' with the statement below using structual induction. All lists 'ns' are of type [Int] and all 'm' are of type Int.

foldl (+) m ns = m + (sum ns)

Definitions:

sum :: [Int] -> Int         -- summation of an Int list
sum []     = 0              -- s.1
sum (x:xs) = x + (sum xs)   -- s.2

foldl :: (a -> b -> a) -> a -> [b] -> a    -- fold left
foldl _ s []     = s                       -- fl.1
foldl f s (x:xs) = foldl f (f s x) xs      -- fl.2

It would be grateful if someone can help me out on this.

Any thoughts of your own? Anything you've tried? Surely, you have been given some example on how this kind of proof looks in general. — leftaroundabout
It seems that your code uses the my_ prefix inconsistently. You should edit your question to remove them all, I guess. — chi

András Kovács András Kovács · Accepted Answer · 2015-01-20T20:27:22

We would like to prove that for all ns and m, foldl (+) m ns = m + sum ns. We shall proceed by induction on ns. In other words, we prove that the property holds for the empty list, and holds for n:ns whenever it holds for ns.

First, let's see the empty list, and let m be an arbitrary number. Our goal is to prove foldl (+) m [] = m + sum []. There are many ways to do this, but we will proceed by transforming the left side of the equation into the right side by equational reasoning.

foldl (+) m []  -- by definition of foldl
m               -- by right identity of addition
m + 0           -- by the definition of sum
m + sum []      -- QED

Now for the (:) case. Let our list be n:ns. Suppose that the property holds for ns for any m (this is the induction hypothesis). Our goal is to prove foldl (+) m (n:ns) = m + sum (n:ns). Again, we use equational reasoning.

foldl (+) m (n:ns)    -- by the definition of foldl
foldl (+) (m + n) ns  -- by the induction hypothesis, applied to (m + n)
(m + n) + sum ns      -- by associativity of addition
m + (n + sum ns)      -- by the definition of sum
m + sum (n:ns)        -- QED

And we're done.

A common issue among new students of proof writing is that they're not sure if what they're doing actually makes sense, and this makes them nervous. I recommend taking a look at proof assistants such as Agda or Coq. They are excellent for building proof-writing skill. As a small example of Agda, the above proof can be written very similarly there, with some syntactic differences:

-- imports omitted

prop : forall m ns → foldl (_+_) m ns ≡ m + sum ns

prop m [] = begin
  foldl (_+_) m []     ≡⟨⟩ 
  m                    ≡⟨ sym $ +-right-identity m ⟩
  m + 0                ≡⟨⟩
  m + sum []           ∎

prop m (x ∷ ns) = begin 
  foldl _+_ m (x ∷ ns)     ≡⟨⟩
  foldl _+_ (m + x) ns     ≡⟨ prop (m + x) ns ⟩  
  (m + x) + sum ns         ≡⟨ +-assoc m x (sum ns) ⟩ 
  m + (x + sum ns)         ≡⟨⟩
  m + sum (x ∷ ns)         ∎

Structural Induction and Induction Hypothesis in Haskell

1 Answers