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.