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
_|_ = _|_