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;  l = cons 1 nil // Different list with one element;  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.