Structural Induction - Example

Example

Consider the following property of lists:

length (L ++ M) = length L + length M

Here ++ denotes the list concatenation operation, and L and M are lists.

In order to prove this, we need definitions for length and for the concatenation operation. Let (h:t) denote a list whose head (first element) is h and whose tail (list of remaining elements) is t, and let denote the empty list. The definitions for length and the concatenation operation are:

length = 0 length (h:t) = 1 + length t ++ list = list (h:t) ++ list = h : (t ++ list)

Our proposition P(l) is that EQ is true for all lists M when L is l. We want to show that P(l) is true for all lists l. We will prove this by structural induction on lists.

First we will prove that P is true; that is, EQ is true for all lists M when L happens to be the empty list . Consider EQ:

length (L ++ M) = length L + length M length ( ++ M) = length + length M length M = length + length M (by APP1) length M = 0 + length M (by LEN1)

So this part of the theorem is proved; EQ is true for all M, when L is, because the left-hand side and the right-hand side are equal.

Now we will prove P(l) when l is a nonempty list. Since l is nonempty, it has a head item, x, and a tail list, xs, so we can express it as (x:xs). The induction hypothesis is that EQ is true for all values of M when L is xs:

length (xs ++ M) = length xs + length M (hypothesis)

We would like to show that if this is the case, then EQ is also true for all values of M when L is a list x:xs whose tail is xs. We proceed as before:

length (L ++ M) = length L + length M length ((x:xs)++ M) = length (x:xs) + length M length (x:(xs ++ M)) = length (x:xs) + length M (by APP2) 1 + length (xs ++ M) = length (x:xs) + length M (by LEN2) 1 + length (xs ++ M) = 1 + length xs + length M (by LEN2) length (xs ++ M) = length xs + length M

As this is just the induction hypothesis, we are done.