5. Lists: Working with Structured Data
import LF.Induction import LF.UsingLean
namespace Lists
5.1. Pairs of Numbers
An inductive definition of pairs of numbers. It has just one constructor, taking two arguments:
inductive NatProd where
| pair (n1 n2 : Nat)
#check (NatProd.pair 3 5)
I would have expected us to have namespace NatProd here when defining
the following functions, so we don't need qualifiers. We've already
fully explained namespaces back in Basics. Some of the text below
mentions using the NatProd prefix specifically, but I think you can
drop it and it will still work.
Functions for extracting the first and second components of a pair can then be defined by pattern matching.
def NatProd.fst (p : NatProd) : Nat :=
match p with
| .pair x _ => x
def NatProd.snd (p : NatProd) : Nat :=
match p with
| .pair _ y => y
Defining these functions with the NatProd type name qualifying their names
allows us to use them with . notation:
example : (NatProd.pair 3 5).fst = 3 := ⊢ (NatProd.pair 3 5).fst = 3 All goals completed! 🐙
A nicer notation for pairs:
example : (⟨3, 5⟩ : NatProd).fst = 3 := ⊢ (NatProd.pair 3 5).fst = 3 All goals completed! 🐙
The anonymous constructor can be used both in expressions and in pattern matches.
def NatProd.fst' (p : NatProd) : Nat :=
match p with
| ⟨x, _⟩ => x
def NatProd.snd' (p : NatProd) : Nat :=
match p with
| ⟨_, y⟩ => y
def NatProd.swap (p : NatProd) : NatProd :=
⟨snd p, fst p⟩
To expose the structure of a pair, use cases (or destructuring).
theorem surjective_pairing : ∀ p : NatProd,
p = ⟨p.fst, p.snd⟩ := ⊢ ∀ (p : NatProd), p = NatProd.pair p.fst p.snd
n:Natm:Nat⊢ NatProd.pair n m = NatProd.pair (NatProd.pair n m).fst (NatProd.pair n m).snd; All goals completed! 🐙
theorem surjective_pairing_cases (p : NatProd) :
p = ⟨p.fst, p.snd⟩ := p:NatProd⊢ p = NatProd.pair p.fst p.snd
n1✝:Natn2✝:Nat⊢ NatProd.pair n1✝ n2✝ = NatProd.pair (NatProd.pair n1✝ n2✝).fst (NatProd.pair n1✝ n2✝).snd; All goals completed! 🐙
5.1.1. Structures
Lean's structure is shorthand for a single-constructor
inductive with the accessors auto-generated.
structure NatProd' where
fst : Nat
snd : Nat
#check (NatProd'.mk 3 5)
example : (NatProd'.mk 3 5).fst = 3 := ⊢ { fst := 3, snd := 5 }.fst = 3 All goals completed! 🐙
example : (⟨3, 5⟩ : NatProd').fst = 3 := ⊢ { fst := 3, snd := 5 }.fst = 3 All goals completed! 🐙
5.2. Lists of Numbers
An inductive definition of lists of numbers:
inductive NatList : Type where
| nil
| cons (n : Nat) (l : NatList)
By convention, we place the operations (functions) of an inductive type inside the namespace implicitly created by that type's definition.
namespace NatList
Some notation for lists to make our lives easier: :: as an
infix cons operator and square brackets as an "outfix" notation.
List syntax
We first define :: as right-associative notation for cons,
and then define list notation as a macro,
allowing us to write [1, 2] instead of 1 :: 2 :: [].
The unexpander reverses the macro, translating list syntax back to
cons syntax.
scoped infixr:65 (priority := high) " :: " => cons
scoped macro (priority := high) "[" elems:term,* "]" : term => do
elems.getElems.foldrM (``(cons $(⟨·⟩) $(⟨·⟩))) (← ``(nil))
@[scoped app_unexpander nil]
def unexpandNil : Lean.PrettyPrinter.Unexpander
| `($_) => `([])
@[scoped app_unexpander cons]
def unexpandCons : Lean.PrettyPrinter.Unexpander
| `($_ $x []) => `([$x])
| `($_ $x [$xs,*]) => `([$x, $xs,*])
| _ => throw ()
Now these all mean exactly the same thing:
def mylist1 : NatList := 1 :: (2 :: (3 :: []))
def mylist2 : NatList := 1 :: 2 :: 3 :: []
def mylist3 : NatList := [1, 2, 3]
Some useful list-manipulation functions...
Let's define some functions on lists.
5.2.1. Replicate
def replicate (n count : Nat) : NatList :=
match count with
| 0 => []
| count' + 1 => n :: replicate n count'
Some simple facts about replication:
theorem replicate_zero (n : Nat) : replicate n 0 = [] := n:Nat⊢ replicate n 0 = [] All goals completed! 🐙
theorem replicate_succ (n count : Nat) :
replicate n (count + 1) = n :: replicate n count := n:Natcount:Nat⊢ replicate n (count + 1) = n :: replicate n count All goals completed! 🐙
5.2.2. Length
def length (l : NatList) : Nat :=
match l with
| [] => 0
| _ :: t => (length t) + 1
Some simple facts about list lengths:
theorem length_nil : [].length = 0 := ⊢ [].length = 0 All goals completed! 🐙
theorem length_cons (n : Nat) (l : NatList) :
(n :: l).length = l.length + 1 := n:Natl:NatList⊢ (n :: l).length = l.length + 1 All goals completed! 🐙
5.2.3. Append
def append (l₁ l₂ : NatList) : NatList :=
match l₁ with
| [] => l₂
| h :: t => h :: append t l₂
5.2.4. Type Classes and Overloading Notation
Lean overloads notation like ++ via type classes: registering an
HAppend instance lets ++ mean append for NatList.
instance : HAppend NatList NatList NatList where
hAppend := append
Now l₁ ++ l₂ means append l₁ l₂ within NatList.
Some simple facts about appending lists:
theorem nil_append (l : NatList) : [] ++ l = l := l:NatList⊢ [] ++ l = l All goals completed! 🐙
theorem cons_append (n : Nat) (l₁ l₂ : NatList) :
(n :: l₁) ++ l₂ = n :: (l₁ ++ l₂) := n:Natl₁:NatListl₂:NatList⊢ (n :: l₁) ++ l₂ = n :: l₁ ++ l₂ All goals completed! 🐙
example : [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5] := ⊢ [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5] All goals completed! 🐙
example : [] ++ [4, 5] = [4, 5] := ⊢ [] ++ [4, 5] = [4, 5] All goals completed! 🐙
example : [1, 2, 3] ++ [] = [1, 2, 3] := ⊢ [1, 2, 3] ++ [] = [1, 2, 3] All goals completed! 🐙
BEq.refl : (a == a) = true is worth knowing by name.
5.2.5. Head and Tail
def head (default : Nat) (l : NatList) : Nat :=
match l with
| [] => default
| h :: _ => h
Basic theorems about how head behaves:
theorem head_cons (h x : Nat) (t : NatList) : (h :: t).head x = h := h:Natx:Natt:NatList⊢ head x (h :: t) = h All goals completed! 🐙
theorem head_nil (x : Nat) : [].head x = x := x:Nat⊢ head x [] = x All goals completed! 🐙
def tail (l : NatList) : NatList :=
match l with
| [] => []
| _ :: t => t
Basic theorems about how tail behaves:
theorem tail_cons (h : Nat) (t : NatList) : (h :: t).tail = t := h:Natt:NatList⊢ (h :: t).tail = t All goals completed! 🐙
theorem tail_nil : [].tail = [] := ⊢ [].tail = [] All goals completed! 🐙
5.2.6. Exercises
The exercises below are kind of massive, with many parts. Is that really what we want, rather than separating out the graded parts into separate exercises?
5.2.7. Counting
5.2.8. Membership
5.2.9. Removal
5.2.10. Included
5.3. Reasoning About Lists
As with numbers, some proofs about list functions need only rewriting.
...and some need case analysis.
theorem tail_length_pred (l : NatList) :
l.length.pred = l.tail.length := l:NatList⊢ l.length.pred = l.tail.length
cases l with
⊢ [].length.pred = [].tail.length ⊢ Nat.pred 0 = 0; All goals completed! 🐙
n:Natl':NatList⊢ (n :: l').length.pred = (n :: l').tail.length n:Natl':NatList⊢ (l'.length + 1).pred = l'.length; All goals completed! 🐙
Usually, though, interesting theorems about lists require induction for their proofs. We'll see how to do this next.
5.3.1. Induction on Lists
Lean generates an induction principle for every inductive
definition, including lists. We can use the induction tactic on
lists to prove things like the associativity of list-append...
theorem append_assoc (l₁ l₂ l₃ : NatList) :
(l₁ ++ l₂) ++ l₃ = l₁ ++ (l₂ ++ l₃) := l₁:NatListl₂:NatListl₃:NatList⊢ l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃)
induction l₁ with
l₂:NatListl₃:NatList⊢ [] ++ l₂ ++ l₃ = [] ++ (l₂ ++ l₃)
All goals completed! 🐙
l₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ (n :: l₁') ++ l₂ ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃)
All goals completed! 🐙
For comparison, here is an informal proof of the same theorem.
Theorem: For all lists l₁, l₂, and l₃,
(l₁ ++ l₂) ++ l₃ = l₁ ++ (l₂ ++ l₃).
Proof: By induction on l₁.
-
First, suppose
l₁ = []. We must show
([] ++ l₂) ++ l₃ = [] ++ (l₂ ++ l₃),
which follows directly from the definition of append.
-
Next, suppose
l₁ = n :: l₁', which gives us the following inductive hypothesis.
(l₁' ++ l₂) ++ l₃ = l₁' ++ (l₂ ++ l₃)
We must show
((n :: l₁') ++ l₂) ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃).
By the definition of append, this follows from
n :: ((l₁' ++ l₂) ++ l₃) = n :: (l₁' ++ (l₂ ++ l₃)),
which is immediate from the induction hypothesis. QED.
5.3.1.1. Generalizing Statements
Sometimes statements need to be generalized to prove them by induction:
theorem replicate_append_fail (c n : Nat) :
replicate n c ++ replicate n c = replicate n (c + c) := c:Natn:Nat⊢ replicate n c ++ replicate n c = replicate n (c + c)
induction c with
n:Nat⊢ replicate n 0 ++ replicate n 0 = replicate n (0 + 0) All goals completed! 🐙
n:Natc':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ replicate n (c' + 1) ++ replicate n (c' + 1) = replicate n (c' + 1 + (c' + 1))
-- Now we seem to be stuck.
-- The `ih` only works for `c' + c'`,
-- but we need `c' + 1 + (c' + 1)`.
A generalization that gives a stronger induction hypothesis:
theorem replicate_append_general (c₁ c₂ n : Nat) :
replicate n c₁ ++ replicate n c₂ = replicate n (c₁ + c₂) := c₁:Natc₂:Natn:Nat⊢ replicate n c₁ ++ replicate n c₂ = replicate n (c₁ + c₂)
induction c₁ with
c₂:Natn:Nat⊢ replicate n 0 ++ replicate n c₂ = replicate n (0 + c₂)
All goals completed! 🐙
c₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ replicate n (c1' + 1) ++ replicate n c₂ = replicate n (c1' + 1 + c₂)
All goals completed! 🐙
Then, we can use this more general theorem to prove the original goal:
theorem replicate_append (c n : Nat) :
replicate n c ++ replicate n c = replicate n (c + c) := c:Natn:Nat⊢ replicate n c ++ replicate n c = replicate n (c + c)
All goals completed! 🐙
5.3.1.2. Reversing a List
A more interesting example of induction over lists:
def reverse (l : NatList) : NatList :=
match l with
| [] => []
| h :: t => t.reverse ++ [h]
theorem reverse_nil : [].reverse = [] := ⊢ [].reverse = [] All goals completed! 🐙
theorem reverse_cons (h : Nat) (t : NatList) : (h :: t).reverse = t.reverse ++ [h] := h:Natt:NatList⊢ (h :: t).reverse = t.reverse ++ [h] All goals completed! 🐙
example : [1, 2, 3].reverse = [3, 2, 1] := ⊢ [1, 2, 3].reverse = [3, 2, 1] All goals completed! 🐙
example : [].reverse = [] := ⊢ [].reverse = [] All goals completed! 🐙
Let's try to prove ∀ l : NatList, length (reverse l) = length l.
example (l : NatList) :
l.reverse.length = l.length := l:NatList⊢ l.reverse.length = l.length
induction l with
⊢ [].reverse.length = [].length All goals completed! 🐙
n:Natl':NatListih:l'.reverse.length = l'.length⊢ (n :: l').reverse.length = (n :: l').length
-- Now we seem to be stuck: the goal involves `++`,
-- but we don't have any useful equations
-- in either the immediate context or in the global
-- environment!
theorem length_append_succ (l : NatList) (n : Nat) :
(l.reverse ++ [n]).length = l.reverse.length + 1 := l:NatListn:Nat⊢ (l.reverse ++ [n]).length = l.reverse.length + 1
induction l with
n:Nat⊢ ([].reverse ++ [n]).length = [].reverse.length + 1
All goals completed! 🐙
n:Natm:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ ((m :: l').reverse ++ [n]).length = (m :: l').reverse.length + 1
-- `ih` not applicable
theorem append_length_succ (l : NatList) (n : Nat) :
(l ++ [n]).length = l.length + 1 := l:NatListn:Nat⊢ (l ++ [n]).length = l.length + 1
induction l with
n:Nat⊢ ([] ++ [n]).length = [].length + 1 All goals completed! 🐙
n:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ ((m :: l') ++ [n]).length = (m :: l').length + 1
All goals completed! 🐙
Now we can prove the main theorem.
theorem length_reverse (l : NatList) :
l.reverse.length = l.length := l:NatList⊢ l.reverse.length = l.length
induction l with
⊢ [].reverse.length = [].length All goals completed! 🐙
n:Natl':NatListih:l'.reverse.length = l'.length⊢ (n :: l').reverse.length = (n :: l').length
All goals completed! 🐙
We can also prove a more general form that gives the
length of any two appended lists. We could use this theorem rather
than append_length_succ to help prove length_reverse.
theorem length_append (l₁ l₂ : NatList) :
(l₁ ++ l₂).length = l₁.length + l₂.length := l₁:NatListl₂:NatList⊢ (l₁ ++ l₂).length = l₁.length + l₂.length
All goals completed! 🐙
To prove the following theorem, which tactics will we need besides
intro, rw, and rfl?
(A) none
(B) cases
(C) induction on n
(D) induction on l
(E) can't be done with the tactics we've seen.
example (n : Nat) (l : NatList) :
replicate n 0 = l → l.length = 0
What about the next one?
example (n m : Nat) : (replicate n m).length = m
To prove the following theorem, which tactics will we need besides
intro, rw, and rfl?
(A) none
(B) cases
(C) induction on n
(D) induction on m
(E) can't be done with the tactics we've seen.
5.3.2. List Exercises, Part 1
5.3.3. List Exercises, Part 2
open NatList
5.4. Options
Suppose we'd like a function to retrieve the nth element
of a list. What to do if the list is too short?
def nthBad (l : NatList) (n : Nat) : Nat :=
match l with
| [] => 42
| a :: l' => match n with
| 0 => a
| n' + 1 => nthBad l' n'
The solution: return a NatOption.
end NatList
inductive NatOption : Type where
| some (n : Nat)
| none
namespace NatList
def nth? (l : NatList) (n : Nat) : NatOption :=
match l with
| [] => .none
| a :: l' => match n with
| 0 => .some a
| n' + 1 => nth? l' n'
example : nth? [4, 5, 6, 7] 0 = .some 4 := ⊢ [4, 5, 6, 7].nth? 0 = NatOption.some 4 All goals completed! 🐙
example : nth? [4, 5, 6, 7] 3 = .some 7 := ⊢ [4, 5, 6, 7].nth? 3 = NatOption.some 7 All goals completed! 🐙
example : nth? [4, 5, 6, 7] 9 = .none := ⊢ [4, 5, 6, 7].nth? 9 = NatOption.none All goals completed! 🐙
def NatOption.elim (d : Nat) (o : NatOption) : Nat :=
match o with
| .some n => n
| .none => d
theorem NatOption.elim_none (d : Nat) : elim d .none = d := d:Nat⊢ elim d NatOption.none = d All goals completed! 🐙
theorem NatOption.elim_some (d₁ d₂ : Nat) : elim d₁ (.some d₂) = d₂ := d₁:Natd₂:Nat⊢ elim d₁ (NatOption.some d₂) = d₂ All goals completed! 🐙
end NatList
5.5. Partial Maps
As a final illustration of how data structures can be defined in Lean, here is a simple partial map data type, analogous to the map or dictionary data structures found in most programming languages.
First, we define a new type MyId to serve as the "keys" of our
partial maps.
structure MyId where
val : Nat
Internally, a MyId is just a number. Introducing a separate type
by wrapping each Nat makes definitions more readable and gives us
flexibility to change representations later if we want to.
We'll also need an equality test for MyIds:
def MyId.beq (x₁ x₂ : MyId) : Bool :=
x₁.val == x₂.val
theorem MyId.beq_refl (x : MyId) : MyId.beq x x = true := x:MyId⊢ x.beq x = true
All goals completed! 🐙
Now we define the type of partial maps:
inductive PartialMap : Type where
| empty : PartialMap
| record (i : MyId) (n : Nat) (m : PartialMap) : PartialMap
namespace PartialMap
The update function overrides the entry for a given key in a
partial map by shadowing it with a new one (or simply adds a new
entry if the given key is not already present).
def update (d : PartialMap) (x : MyId) (value : Nat) : PartialMap :=
record x value d
We can define functions on PartialMaps by pattern matching.
def find (x : MyId) (d : PartialMap) : NatOption :=
match d with
| empty => .none
| record y n d' =>
bif MyId.beq x y then .some n
else find x d'
Is the following claim true or false?
∀ (d : PartialMap) (x : MyId) (n : Nat),
-----------------------------------------
find x (update d x n) = .some n(A) True (B) False (C) Not sure
Is the following claim true or false?
∀ (d : PartialMap) (x y : MyId) (o : Nat)
(h : MyId.beq x y = false),
-----------------------------------------
find x (update d y o) = find x d(A) True (B) False (C) Not sure
end PartialMap
end Lists