#3 Functional Programming: Induction over list

Hi everyone! Welcome to the series where I'll be teaching you how to program in Haskell (functional programming part) and how to prove your programs.

Today I'll be talking again about Lists, since list are really important in Haskell.

Today we'll look at how to proove your program that uses recursion over list. Feel free to ask question, since this part is close to mathematics.

We want to proove some properties of our program.

Induction

What is induction exactly? We have for example proof by induction over the natural numbers for some statement P(n), where we prove first P(0) and then we can assume that P(n) holds. Next we have to show that P(n+1) holds. And then we can say that P(n) holds for every n.

Basically Induction over lists looks like this:

Proof by induction: prove P(xs) for all xs in in [T]
Base case: prove P([]) (emptylist)
Step case: prove P(x:xs) under assumption P(xs) for an arbitrary xs::[T] and x::T
- Induction hypothesis: xs :: [T], x::T and P(xs)
- To prove P(x : xs)

Let's go straight to an example:

sumList [] = 0

sumList (x:xs) = x + (sumList xs)





double [] = []

double (x:xs) = (2*x) : (double xs)

Proof by induction:
P(xs) := ( (sumList (double xs) = 2 * (sumList xs) )

We want to prove that the sum of the list times two is the same as the every element times two and the summed. Above you see the definition with which we'll work. P(xs) is simply what we want to show. (the whole equation)

Base case: prove P([])
sumList (double []) = sumList [] = 0
2 * sumList [] = 2 * 0 = 0
since both are 0, we can say that P([]) is true since 0=0
Step case: P(xs) -> P(x : xs). Let x :: Int and xs :: [Int] be arbitray.
- Induction hypothesis:
  sumList (double xs) = 2 * sumList xs
- To prove:
  sumList (double (x : xs)) = 2 * sumList (x : xs)
  
  sumList (double (x : xs)) = sumList ((2 · x) : double xs)
  = 2 · x + sumList (double xs) = 2 · x + 2 · sumList xs
  = 2 · (x + sumList xs) = 2 · (sumList (x : xs))

The first we did is we used the definition of double. Then we used the definition of sumList. Then we finally could use our induction hypothesis so we could change the form. General Rule: At one point you'll have to use the induction hypothesis.

I hope you enjoyed this quick tutorial on Inductions. Next time we'll dig deeper into types, higher-order functions and some awesome examples. Stay tuned.

If you enjoyed this, take a look at the other tutorials on Functional Programming!

Cheers!