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