In this post, we will explore an inductive data structure as a type for lists of elements. We define two recursive functions that can be applied to lists of this type; namely, an operation to append two lists and an operation to reverse a list. With these definitions, we set out to mathematically prove a number of properties that should hold for these functions by means of induction.

A list is a data structure of a collection of elements in a certain order. A list can be defined in multiple ways. One way is to define a list as being an element (the “head” of the list) followed by another list (the “tail” of the list). Inductively, this could be formalized as follows:

Inductive list a := cons a list | nil.

This means that a list l with elements of type a is either cons x tail, with x of type a and with tail of type list a, or l is the empty list nil. Let’s look at some example lists with elements of the whole numbers.

// Empty list; []
l = nil

// List with one element; [1]
l = cons 1 nil

// Different list with one element; [2]
l = cons 2 nil

// List with two elements; [1,2]
l = cons 1 (cons 2 nil)

// List with three elements; [1,2,3]
l = cons 1 (cons 2 (cons 3 nil))

Note that because we have lists of integers, following our definition the list l is of type list integer.

Multiple list operations can be defined, such as append and reverse. We defined our list inductively, and so it would make sense to define these operations inductively (also known as recursively) as well. Because of our neat data structure and operations, we should then be able to prove that certain properties of the operations hold.

Let’s first define append. By appending two lists, we create a new list where the elements in the first list are followed by the elements in the second. This can easily be defined as follows:

Function append : (list a) (list a) -> (list a)
append (nil) (k)            = k.
append (cons head tail) (k) = cons head (append tail k).

Thus, our function append is a function that takes two parameters of type list a and returns something of type list a. We defined it in two steps: if the first list is empty (nil), we return the second list. If the first list is not empty, we create a new list with the same head as the first, and with as tail the second list appended to the tail of the first list. Note that the parentheses around nil, k, and cons head tail in the above definition are optional; I added them for clarity. Let’s append the lists [1,2,3] and [4,5]:

append (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))
= cons 1 (append (cons 2 (cons 3 nil)) (cons 4 (cons 5 nil))) 
= cons 1 (cons 2 (append (cons 3 nil) (cons 4 (cons 5 nil))))
= cons 1 (cons 2 (cons 3 (append (nil) (cons 4 (cons 5 nil)))))
= cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil)))).

We want to prove that the following properties of this function hold:

Lemma append_nil   = forall (l : list a), append l nil = l.
Lemma append_assoc = forall (k : list a, l : list a, m : list a), 
                         append (append k l) m = append k (append l m).

With the first lemma we state that the result of appending a list and an empty list is equal to the first list. With the second lemma we state that first appending lists k and l, and then appending m to the result is equal to appending the result of appending l and m to k.

Proof of the First Lemma

Let’s prove the first lemma. We will prove that the lemma is true with induction on l.

First, consider l = nil. Thus,

append l nil 
= append nil nil // First rule of append:
= nil
= l.

Thus, for l = nil we have append l nil = l, and so the property holds.

Now, we assume that the property holds for the list tail. Thus, append tail nil = tail. Consider l = cons head tail.

append l nil
= append (cons head tail) nil // Second rule of append:
= cons head (append tail nil) // Inductive assumption:
= cons head tail
= l.

As such, if the property holds for tail we have append (cons head tail) nil = cons head tail for any arbitrary head. Thus, with structural induction on l, we have shown that the first lemma holds for all finite lists.

Proof of the Second Lemma

Now, we will prove the second lemma. We will again prove this by induction.

First, consider arbitrary l and m, with k = nil.

append (append k l) m
= append (append nil l) m // First rule of append:
= append l m              // First rule of append (reversed):
= append nil (append l m)
= append k (append l m).

Thus, with k = nil the property holds. Now, we assume the property holds for some list tail. Thus, append (append tail l) m = append tail (append l m). Consider k = cons head tail.

append (append k l) m
= append (append (cons head tail) l) m // Second rule of append:
= append (cons head (append tail l)) m // Second rule of append:
= cons head (append (append tail l) m) // Inductive assumption:
= cons head (append tail (append l m)) // Second rule of append (reversed):
= append (cons head tail) (append l m)
= append k (append l m).

As such, if the property holds for tail we have append ((cons head tail) l) m = append (cons head tail) (append l m) for any arbitrary head. So, the property holds for cons head tail as well. We have shown, with structural induction on k, that the second lemma holds for all lists.

Reversing Lists

Now, we define a new operation; reverse.

Function reverse : (list a) -> (list a)
reverse nil = nil.
reverse (cons head tail) = append (reverse tail) (cons head nil)

Let’s take the reverse of the list [1,2,3]:

reverse (cons 1 (cons 2 (cons 3 nil)))
= append (reverse (cons 2 (cons 3 nil))) (cons 1 nil)
= append (append (reverse (cons 3 nil)) (cons 2 nil)) (cons 1 nil)
= append (append (append (reverse nil) (cons 3 nil)) (cons 2 nil)) (cons 1 nil)
= append (append (append nil (cons 3 nil)) (cons 2 nil)) (cons 1 nil)
= append (append (cons 3 nil) (cons 2 nil)) (cons 1 nil)
= append (cons 3 (cons 2 nil)) (cons 1 nil)
= cons 3 (cons 2 (cons 1 nil)). // [3,2,1]

Now, we want to prove that the following property of our reversal and append functions hold:

Lemma reverse_append = forall (l : list a, m : list a),
                           reverse (append l m) = append (reverse m) (reverse l).

This lemma states that reversing the result of appending lists l and m is equal to appending the reversals of lists m and l. We will prove this by induction on l. First, consider l = nil.

reverse (append l m)
= reverse (append nil m) // First rule of append:
= reverse m              // Reverse use of our first lemma
                         // append m nil = append m:
= append (reverse m) nil // First rule of reverse (reversed):
= append (reverse m) (reverse nil)
= append (reverse m) (reverse l).

Thus, with l = nil the property holds. Now, assume the property holds for tail; thus, reverse (append tail m) = append (reverse m) (reverse tail). Consider l = cons head tail.

reverse (append l m)
= reverse (append (cons head tail) m) // Second rule of append:
= reverse (cons head (append tail m)) // Second rule of reverse:
= append (reverse (append tail m)) (cons head nil) 
// Inductive assumption:
= append (append (reverse m) (reverse tail)) (cons head nil)
// Use of second lemma:
= append (reverse m) (append (reverse tail) (cons head nil))
// Second rule of reverse (reversed):
= append (reverse m) (reverse (cons head tail))
= append (reverse m) (reverse l).

As such, if the property holds for tail, we have reverse (append (cons head tail) m) = append (reverse m) (reverse (cons head tail)) for any arbitrary head. Thus, the property also holds for cons head tail. So, with structural induction on l, the property holds for all lists.