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