# These are lecture notes from my Computer Science course. For learning about functional programming, in particular Haskell, I recommend Programming in Haskell.

## Show in detail…

If you’re required to show that something holds for a set of given functions, use certain base cases. For example in the 08-09 paper you are given some boolean algebra laws and asked to show that another law holds for all expressions. For that, you use 3 cases of True, False, and undefined (_|_) for one of the values.

## List induction

Here’s an example of list induction from the practicals:

Prove by list induction that (++) is associative. That is, prove that the following equation holds for any lists xs, ys and zs.

``xs ++ (ys ++ zs) = (xs ++ ys) ++ zs``

First, the definition of `++`:

``````[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)``````

`++` is pattern matched on the first argument, so the base case is where this argument == `[]`, so apply this to the equation at the top:

``````[] ++ (ys ++ zs) = ([] ++ ys) ++ zs
by definition:
ys ++ zs = ys ++ zs``````

Now for the inductive proof:

``````xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
(x:xs) ++ (ys ++ zs) = (x:xs ++ ys) ++ zs
unfold:
x : (xs ++ (ys ++ zs)) = x : ((xs ++ ys) ++ zs)
due to inductive hypothesis this can be written:
x : (xs ++ (ys ++ zs)) = x : (xs ++ (ys ++ zs))``````

Don’t forget the undefined clause:

``````_|_ ++ (ys ++ zs) = (_|_ ++ ys) ++ zs
strict matching:
_|_ = _|_ ++ zs
_|_ = _|_``````
This entry was posted in fun, lecture. Bookmark the permalink.