Lists
The first exercises involve lists. Let α : Type* be any type. Then the new type List α has terms that are lists with elements of type α.
This list type is defined inductively using two constructors. The first one is List.nil, also denoted as []. It can be considered the empty list. The second one is List.cons, also denoted as ::.
The following table summarize what the types of these constructor terms.
| Constructor term | Type |
|---|---|
| List.nil [] |
List α |
| List.cons :: |
α → List α → List α |
The inductive definition of lists says that every term of type List α is either [] or a :: as, with a : α and as : List α.
For example, if we have a, b: α, then [] is a term of type List α by the inductive construction. Also, b :: [] is a type of List α, because it has the form b :: as with as = [] a term of List α. Continuing this pattern, we see that a :: b :: [] is a term of List α.
Note that we can use short hand notation [a, b] = a :: b :: [].
For proving theorems about list, the tactic induction' will be helpful. For a list as, we can handle the two different cases (as = [] and as = a::tail) separately as
induction' a with a tail ih
· -- give the proof when as = []
· -- give the proof when as = a::tail, with ih the induction hypothesis (the theorem applied to tail)
Binary trees
Similarly to lists, the inductive type BinTree also has two possible formats. The first one is empty, which is just an empty binary tree. The second format is node l r, where node is of type BinTree → BinTree → BinTree.
Hence, the function node creates a new binary tree by connecting a left tree (the first argument) and a right tree (the second argument) together at a new node. We can again use the induction' tactic for proofs about binary trees. For example, if we want to prove theorem about a binary tree t, then we can use
induction' t with l r hl hr
· -- give the proof when t = empty
· -- give the proof when t = node l r, with hl a proof that the theorem holds for l and hr a proof the the theorem holds for r.
Next week
Next week, we will finish chapter 6 (discrete mathematics) and start with chapter 7 (structures).