5. Lists: Working with Structured Data🔗

import LF.Induction
import LF.UsingLean

This chapter introduces basic data structures and functions for working with them. We place all these definitions in the Lists namespace to avoid name clashes with Lean's standard library and with definitions from other chapters.

namespace Lists

5.1. Pairs of Numbers🔗

In an inductive type definition, each constructor can take any number of arguments — none (as with true and 0), one (as with Nat.succ), or more than one (as with Playground.Nibble and the following):

inductive NatProd where
  | pair (n1 n2 : Nat)

This declaration can be read: "The one and only way to construct a pair of numbers is by applying the constructor NatProd.pair to two arguments of type Nat."

NatProd.pair 3 5 : NatProd#check (NatProd.pair 3 5)

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 := by⊢ (NatProd.pair 3 5).fst = 3 rflAll goals completed! 🐙

Since pairs will be used heavily in what follows, it will be convenient to write them with angle-bracket notation ⟨n, m⟩ instead of NatProd.pair n m. This notation is built into Lean and is called "anonymous constructor syntax". It is available for any inductive type with a single constructor, as long as the expected type is declared or can be inferred from the context.

example : (⟨3, 5⟩ : NatProd).fst = 3 := by⊢ (NatProd.pair 3 5).fst = 3 rflAll 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⟩

Note that pattern-matching on a pair (with angle brackets: ⟨x, y⟩) is not to be confused with the "multiple pattern" syntax (with no brackets: x, y) that we have seen previously. The above examples illustrate pattern matching on a pair with elements x and y, whereas, for example, the definition of sub for subtracting two Nats performs pattern matching on the values n and m:

def sub (n m : Nat) : Nat :=
  match n, m with
  | 0,        _        => 0
  | .succ _,  0        => n
  | .succ n', .succ m' => sub n' m'

The distinction is minor, but it is worth understanding that they are not the same. For instance, the following definitions are ill-formed:

def bad_fst (p : NatProd) : Nat :=
  match p with
  | Too many patterns in match alternative: Expected 1, but found 2:
  x, yx, y => x

Too many patterns in match alternative: Expected 1, but found 2:
  x, y

def bad_sub (n m : Nat) : Nat :=
  match n, m with
  | Invalid `⟨...⟩` notation: The expected type `Nat` has more than one constructor

Note: This notation can only be used when the expected type is an inductive type with a single constructorNot enough patterns in match alternative: Expected 2, but found 1:
  ⟨0, .(_)⟩⟨0,        _⟩        => 0
  | ⟨.succ _,  0⟩        => n
  | ⟨.succ n', .succ m'⟩ => sub n' m'

Invalid `⟨...⟩` notation: The expected type `Nat` has more than one constructor

Note: This notation can only be used when the expected type is an inductive type with a single constructor

As with the multi-argument match n, m with style used above in sub, matching jointly on several values can combine what would otherwise be several separate cases into a single match arm. This means the simplification rules we define for such a function may not always match one-to-one with the cases of its match construct.

A property like p = ⟨p.fst, p.snd⟩ can be proved by exposing the structure of the pair, either with cases or by destructuring in intro.

theorem surjective_pairing : ∀ p : NatProd,
    p = ⟨p.fst, p.snd⟩ := by⊢ ∀ (p : NatProd), p = NatProd.pair p.fst p.snd
  intro ⟨n, m⟩n:Natm:Nat⊢ NatProd.pair n m = NatProd.pair (NatProd.pair n m).fst (NatProd.pair n m).snd; rflAll goals completed! 🐙

theorem surjective_pairing_cases (p : NatProd) :
    p = ⟨p.fst, p.snd⟩ := byp:NatProd⊢ p = NatProd.pair p.fst p.snd
  cases ppairn1✝:Natn2✝:Nat⊢ NatProd.pair n1✝ n2✝ = NatProd.pair (NatProd.pair n1✝ n2✝).fst (NatProd.pair n1✝ n2✝).snd; rflAll goals completed! 🐙

Notice that, unlike the behavior of cases on Nats, where it generates two subgoals, cases generates just one subgoal here. That's because NatProds can only be constructed in one way.

Exercise★(snd_fst_is_swap)

theorem declaration uses `sorry`snd_fst_is_swap (p : NatProd) :
    (⟨p.snd, p.fst⟩ : NatProd) = p.swap := byp:NatProd⊢ NatProd.pair p.snd p.fst = p.swap
  sorryAll goals completed! 🐙

Exercise★(fst_swap_is_snd) (Optional)

theorem declaration uses `sorry`fst_swap_is_snd (p : NatProd) :
    p.swap.fst = p.snd := byp:NatProd⊢ p.swap.fst = p.snd
  sorryAll goals completed! 🐙

5.1.1. Structures🔗

Lean also provides a convenient way to define inductive structures like pairs that have a single constructor but multiple ways to access their data, using the structure keyword. The definition of NatProd' below is equivalent to the NatProd definition from earlier, except that Lean automatically generates the fst and snd accessors.

structure NatProd' where
  fst : Nat
  snd : Nat

{ fst := 3, snd := 5 } : NatProd'#check (NatProd'.mk 3 5)
example : (NatProd'.mk 3 5).fst = 3 := by⊢ { fst := 3, snd := 5 }.fst = 3 rflAll goals completed! 🐙
example : (⟨3, 5⟩ : NatProd').fst = 3 := by⊢ { fst := 3, snd := 5 }.fst = 3 rflAll goals completed! 🐙

5.2. Lists of Numbers🔗

Generalizing the definition of pairs, we can describe the type of lists of numbers like this: "A list is either the empty list or else a pair of a number and another list."

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

As with pairs, it is useful to give lists a symbolic notation. The following declarations allow us to use :: as an infix cons operator and square brackets as an "outfix" notation for constructing lists.

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]

Let's define some functions on lists.

5.2.1. Replicate🔗

Our first is the replicate function, which takes a number n and a count and returns a list of length count in which every element is n.

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 = [] := byn:Nat⊢ replicate n 0 = [] rflAll goals completed! 🐙

theorem replicate_succ (n count : Nat) :
  replicate n (count + 1) = n :: replicate n count := byn:Natcount:Nat⊢ replicate n (count + 1) = n :: replicate n count rflAll goals completed! 🐙

5.2.2. Length🔗

The length function calculates the length of a list.

def length (l : NatList) : Nat :=
  match l with
  | [] => 0
  | _ :: t => (length t) + 1

Some simple facts about list lengths:

theorem length_nil : [].length = 0 := by⊢ [].length = 0 rflAll goals completed! 🐙

theorem length_cons (n : Nat) (l : NatList) :
  (n :: l).length = l.length + 1 := byn:Natl:NatList⊢ (n :: l).length = l.length + 1 rflAll goals completed! 🐙

5.2.3. Append🔗

The append function appends (concatenates) two lists.

def append (l₁ l₂ : NatList) : NatList :=
  match l₁ with
  | [] => l₂
  | h :: t => h :: append t l₂

5.2.4. Type Classes and Overloading Notation🔗

In Lean, notation like ++, ==, and + is not hardwired to particular definitions, which is the way we have been defining notation so far. Instead, Lean defines this notation using type classes — a mechanism that lets us overload operations for different types.

We'll learn more about type classes in chapter Typeclasses. For now, the key idea is just this: a type class is like a Java-style interface, and an instance is an implementation of that interface for a particular type. We associate notation with a particular type class member, and then instances of that typeclass inherit the notation for that member.

For example, ++ is defined via the HAppend type class's hAppend member. Any type that provides an HAppend instance gets to use ++ for its implementation of hAppend. Lean's built-in List already has such an instance (using List.append for hAppend), but since we've defined our own append function, we can register it as the ++ operator within our namespace:

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 := byl:NatList⊢ [] ++ l = l rflAll goals completed! 🐙

theorem cons_append (n : Nat) (l₁ l₂ : NatList) :
  (n :: l₁) ++ l₂ = n :: (l₁ ++ l₂) := byn:Natl₁:NatListl₂:NatList⊢ (n :: l₁) ++ l₂ = n :: l₁ ++ l₂ rflAll goals completed! 🐙

example : [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5] := by⊢ [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5] rflAll goals completed! 🐙
example : [] ++ [4, 5] = [4, 5] := by⊢ [] ++ [4, 5] = [4, 5] rflAll goals completed! 🐙
example : [1, 2, 3] ++ [] = [1, 2, 3] := by⊢ [1, 2, 3] ++ [] = [1, 2, 3] rflAll goals completed! 🐙

The equality test == on Nats is another example: it comes from the BEq ("boolean equality") type class. One small but handy fact about it, which several proofs below will need, is that == is reflexive:

BEq.refl : ∀ (a : Nat), (a == a) = true#check (BEq.refl (α := Nat))

BEq.refl : ∀ (a : Nat), (a == a) = true

5.2.5. Head and Tail🔗

The head function returns the first element (the "head") of the list, while tail returns everything but the first element (the "tail"). Since the empty list has no first element, we pass a default value to be returned in that case.

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 := byh:Natx:Natt:NatList⊢ head x (h :: t) = h rflAll goals completed! 🐙

theorem head_nil (x : Nat) : [].head x = x := byx:Nat⊢ head x [] = x rflAll 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 := byh:Natt:NatList⊢ (h :: t).tail = t rflAll goals completed! 🐙

theorem tail_nil : [].tail = [] := by⊢ [].tail = [] rflAll goals completed! 🐙

And some examples:

example : head 0 [1, 2, 3] = 1 := by⊢ head 0 [1, 2, 3] = 1 rw [head_cons⊢ 1 = 1]All goals completed! 🐙
example : head 0 [] = 0 := by⊢ head 0 [] = 0 rw [head_nil⊢ 0 = 0]All goals completed! 🐙
example : [1, 2, 3].tail = [2, 3] := by⊢ [1, 2, 3].tail = [2, 3] rw [tail_cons⊢ [2, 3] = [2, 3]]All goals completed! 🐙

Quiz

What does the following function do?

def foo (n : Nat) : NatList :=
  match n with
  | 0 => []
  | n' + 1 => (n' + 1) :: foo n'

5.2.6. Exercises🔗

Exercise★★(list_funs)

Complete the definitions of nonZeros, oddMembers, and countOddMembers below. Have a look at the lemmas and examples to understand what these functions should do.

def declaration uses `sorry`nonZeros (l : NatList) : NatList := sorry

The following lemmas should hold about your definition.

theorem declaration uses `sorry`nonZeros_cons_zero (t : NatList) :
    nonZeros (0 :: t) = nonZeros t := sorry

theorem declaration uses `sorry`nonZeros_nil :
    nonZeros [] = [] := sorry

theorem declaration uses `sorry`nonZeros_cons_nonZero (h : Nat) (t : NatList) :
    nonZeros ((h + 1) :: t) = (h + 1) :: nonZeros t := sorry

theorem declaration uses `sorry`test_nonZeros : nonZeros [0, 1, 0] = [1] := by⊢ [0, 1, 0].nonZeros = [1]
  sorryAll goals completed! 🐙

The next definition uses bif, Lean's conditional for boolean tests. The expression bif b then x else y evaluates to x when b is true and to y when b is false. Its characterizing lemmas are cond_true and cond_false.

theorem Bool.cond_true {α} (x y : α) : (bif true then x else y) = x := byα:Sort u_1x:αy:α⊢ (bif true then x else y) = x
  rflAll goals completed! 🐙

theorem Bool.cond_false {α} (x y : α) : (bif false then x else y) = y := byα:Sort u_1x:αy:α⊢ (bif false then x else y) = y
  rflAll goals completed! 🐙

def declaration uses `sorry`oddMembers (l : NatList) : NatList := sorry

theorem declaration uses `sorry`oddMembers_nil :
    oddMembers [] = [] := sorry

theorem declaration uses `sorry`oddMembers_cons (h : Nat) (t : NatList) :
    oddMembers (h :: t) =
      bif h.odd then h :: oddMembers t else oddMembers t :=
  sorry

theorem declaration uses `sorry`oddMembers_cons_odd (n : Nat) (l : NatList)
    (h : n.odd = true) :
    oddMembers (n :: l) = n :: oddMembers l := byn:Natl:NatListh:n.odd = true⊢ (n :: l).oddMembers = n :: l.oddMembers
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`oddMembers_cons_not_odd (n : Nat) (l : NatList)
    (h : n.odd = false) :
    oddMembers (n :: l) = oddMembers l := byn:Natl:NatListh:n.odd = false⊢ (n :: l).oddMembers = l.oddMembers
  sorryAll goals completed! 🐙

Now, we can prove that oddMembers [1, 2] returns [1] using the lemmas:

example : oddMembers [1, 2] = [1] := by⊢ [1, 2].oddMembers = [1]
  rw [oddMembers_cons_odd⊢ 1 :: [2].oddMembers = [1]h⊢ Nat.odd 1 = true]⊢ 1 :: [2].oddMembers = [1]h⊢ Nat.odd 1 = true
  ·⊢ 1 :: [2].oddMembers = [1] rw [oddMembers_cons_not_odd⊢ 1 :: [].oddMembers = [1]h⊢ Nat.odd 2 = false]⊢ 1 :: [].oddMembers = [1]h⊢ Nat.odd 2 = false
    ·⊢ 1 :: [].oddMembers = [1] rw [oddMembers_nil⊢ [1] = [1]]All goals completed! 🐙
    ·h⊢ Nat.odd 2 = false rw [Nat.odd_defh⊢ (!Nat.even 2) = false]h⊢ (!Nat.even 2) = false
      rw [Nat.even_succ,h⊢ (!!Nat.even 1) = false Nat.even_succ,h⊢ (!!!Nat.even 0) = false Nat.even_zeroh⊢ (!!!true) = false]h⊢ (!!!true) = false
      rw [Bool.not_true,h⊢ (!!false) = false Bool.not_false,h⊢ (!true) = false Bool.not_trueh⊢ false = false]All goals completed! 🐙
  ·h⊢ Nat.odd 1 = true rw [Nat.odd,h⊢ (!Nat.even 1) = true Nat.even_succ,h⊢ (!!Nat.even 0) = true Nat.even_zeroh⊢ (!!true) = true]h⊢ (!!true) = true
    rw [Bool.not_true,h⊢ (!false) = true Bool.not_falseh⊢ true = true]All goals completed! 🐙

This gets verbose pretty fast; however, we can use rfl to deal with subgoals such as Nat.odd 2 = false:

example : oddMembers [1, 2] = [1] := by⊢ [1, 2].oddMembers = [1]
  rw [oddMembers_cons_odd⊢ 1 :: [2].oddMembers = [1]h⊢ Nat.odd 1 = true]⊢ 1 :: [2].oddMembers = [1]h⊢ Nat.odd 1 = true
  ·⊢ 1 :: [2].oddMembers = [1] rw [oddMembers_cons_not_odd⊢ 1 :: [].oddMembers = [1]h⊢ Nat.odd 2 = false]⊢ 1 :: [].oddMembers = [1]h⊢ Nat.odd 2 = false
    ·⊢ 1 :: [].oddMembers = [1] rw [oddMembers_nil⊢ [1] = [1]]All goals completed! 🐙
    ·h⊢ Nat.odd 2 = false rflAll goals completed! 🐙
  ·h⊢ Nat.odd 1 = true rflAll goals completed! 🐙

In fact, as the entire proof is just plain computation, it can be done with a single rfl. This is possible because all of the elements and lists are concrete — there are no variables involved.

declaration uses `sorry`example : oddMembers [1, 2] = [1] := sorry

theorem declaration uses `sorry`test_oddMembers : oddMembers [0, 1, 2, 3, 0] = [1, 3] := sorry

For the next problem, countOddMembers, we encourage you to implement it using already-defined functions, rather than recursion.

def declaration uses `sorry`countOddMembers (l : NatList) : Nat := sorry

declaration uses `sorry`example : countOddMembers [0, 1, 2, 3, 0] = 2 := sorry

theorem declaration uses `sorry`test_countOddMembers1 : countOddMembers [0, 2, 4] = 0 := sorry

theorem declaration uses `sorry`test_countOddMembers2 : countOddMembers [] = 0 := sorry

Exercise★★★(alternate) (Advanced)

Complete the following definition of alternate, which interleaves two lists into one, alternating between elements taken from the first list and elements from the second.

Hint: there are natural ways of writing alternate that fail to satisfy Lean's requirement that all recursive definitions be structurally recursive, as mentioned in Basics. If you encounter this difficulty, consider pattern matching against both lists at the same time.

def declaration uses `sorry`alternate (l₁ l₂ : NatList) : NatList := sorry

theorem declaration uses `sorry`test_alternate1 :
    alternate [1, 2, 3] [4, 5, 6] = [1, 4, 2, 5, 3, 6] := sorry

theorem declaration uses `sorry`test_alternate2 :
    alternate [1] [4, 5, 6] = [1, 4, 5, 6] := sorry

theorem declaration uses `sorry`test_alternate3 :
    alternate [1, 2, 3] [4] = [1, 4, 2, 3] := sorry

theorem declaration uses `sorry`test_alternate4 :
    alternate [] [20, 30] = [20, 30] := sorry

5.2.7. Counting🔗

Exercise★(counting)

Define a count function for NatLists that counts the number of times an element n appears in the list.

def declaration uses `sorry`count (n : Nat) (l : NatList) : Nat := sorry

Now prove these lemmas, which should hold about your definition.

theorem declaration uses `sorry`count_nil (n : Nat) : count n [] = 0 := sorry

theorem declaration uses `sorry`count_cons_def (n h : Nat) (t : NatList) :
    count n (h :: t) =
      bif n == h then count n t + 1 else count n t := sorry

theorem declaration uses `sorry`count_cons_same (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = true) :
    count n₁ (n₂ :: t) = count n₁ t + 1 := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ count n₁ (n₂ :: t) = count n₁ t + 1
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`count_cons_diff (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = false) :
    count n₁ (n₂ :: t) = count n₁ t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ count n₁ (n₂ :: t) = count n₁ t
  sorryAll goals completed! 🐙

example : count 1 [1] = 1 := by⊢ count 1 [1] = 1
  rw [count_cons_same _ _ _ rfl⊢ count 1 [] + 1 = 1]⊢ count 1 [] + 1 = 1
  rw [count_nil⊢ 0 + 1 = 1]All goals completed! 🐙

declaration uses `sorry`example : count 2 [2, 2] = 2 := sorry

theorem declaration uses `sorry`test_count1 : count 1 [1, 1, 4] = 2 := sorry

theorem declaration uses `sorry`test_count2 : count 5 [1, 1, 4] = 0 := sorry

Again, all these proofs could be completed with just rfl, because the proof is computationally straightforward — compute both sides of the equality and check whether they are the same.

declaration uses `sorry`example : count 1 [1, 2, 3, 1, 4, 1] = 3 := sorry
declaration uses `sorry`example : count 6 [1, 2, 3, 1, 4, 1] = 0 := sorry

5.2.8. Membership🔗

Exercise★(membership)

def declaration uses `sorry`member (n : Nat) (l : NatList) : Bool := sorry

theorem declaration uses `sorry`member_nil (n : Nat) : member n [] = false := sorry

theorem declaration uses `sorry`member_cons_same (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = true) :
    member n₁ (n₂ :: t) = true := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ member n₁ (n₂ :: t) = true
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`member_cons_diff (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = false) :
    member n₁ (n₂ :: t) = member n₁ t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ member n₁ (n₂ :: t) = member n₁ t
  sorryAll goals completed! 🐙

example : member 1 [1] = true := by⊢ member 1 [1] = true
  rw [member_cons_same _ _ _ rfl⊢ true = true]All goals completed! 🐙

declaration uses `sorry`example : member 2 [1] = false := sorry

theorem declaration uses `sorry`test_member1 : member 1 [1, 4, 1] = true := sorry

theorem declaration uses `sorry`test_member2 : member 2 [1, 4, 1] = false := sorry

5.2.9. Removal🔗

Exercise★★★(removeOne)

Here are some more NatList functions for you to practice with.

When removeOne is applied to a list without the number to remove, it should return the same list unchanged.

def declaration uses `sorry`removeOne (n : Nat) (l : NatList) : NatList := sorry

theorem declaration uses `sorry`removeOne_nil (n : Nat) : removeOne n nil = nil := sorry

theorem declaration uses `sorry`removeOne_cons_same (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = true) :
    removeOne n₁ (n₂ :: t) = t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ removeOne n₁ (n₂ :: t) = t
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`removeOne_cons_diff (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = false) :
    removeOne n₁ (n₂ :: t) = n₂ :: removeOne n₁ t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ removeOne n₁ (n₂ :: t) = n₂ :: removeOne n₁ t
  sorryAll goals completed! 🐙

example : removeOne 5 [1, 5, 4] = [1, 4] := by⊢ removeOne 5 [1, 5, 4] = [1, 4]
  rw [removeOne_cons_diff _ _ _ rfl⊢ 1 :: removeOne 5 [5, 4] = [1, 4]]⊢ 1 :: removeOne 5 [5, 4] = [1, 4]
  rw [removeOne_cons_same _ _ _ rfl⊢ [1, 4] = [1, 4]]All goals completed! 🐙

declaration uses `sorry`example : count 5 (removeOne 5 [1, 5, 4]) = 0 := sorry

theorem declaration uses `sorry`test_removeOne1 : count 4 (removeOne 5 [4, 5, 1, 4]) = 2 := sorry

theorem declaration uses `sorry`test_removeOne2 : count 5 (removeOne 5 [1, 5, 5, 4]) = 1 := sorry

Exercise★★★(removeAll) (Optional)

def declaration uses `sorry`removeAll (n : Nat) (l : NatList) : NatList := sorry

theorem declaration uses `sorry`removeAll_nil (n : Nat) : removeAll n [] = [] := sorry

theorem declaration uses `sorry`removeAll_cons_same (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = true) :
    removeAll n₁ (n₂ :: t) = removeAll n₁ t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ removeAll n₁ (n₂ :: t) = removeAll n₁ t
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`removeAll_cons_diff (n₁ n₂ : Nat) (t : NatList)
  (h : (n₁ == n₂) = false) :
    removeAll n₁ (n₂ :: t) = n₂ :: removeAll n₁ t := byn₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ removeAll n₁ (n₂ :: t) = n₂ :: removeAll n₁ t
  sorryAll goals completed! 🐙

example : count 5 (removeAll 5 [5, 1]) = 0 := by⊢ count 5 (removeAll 5 [5, 1]) = 0
  rw [removeAll_cons_same _ _ _ rfl⊢ count 5 (removeAll 5 [1]) = 0]⊢ count 5 (removeAll 5 [1]) = 0
  rw [removeAll_cons_diff _ _ _ rfl⊢ count 5 (1 :: removeAll 5 []) = 0]⊢ count 5 (1 :: removeAll 5 []) = 0
  rw [removeAll_nil⊢ count 5 [1] = 0]⊢ count 5 [1] = 0
  rw [count_cons_diff _ _ _ rfl⊢ count 5 [] = 0]⊢ count 5 [] = 0
  rw [count_nil⊢ 0 = 0]All goals completed! 🐙

declaration uses `sorry`example : count 5 (removeAll 5 [5, 5]) = 0 := sorry

theorem declaration uses `sorry`test_removeAll1 : count 4 (removeAll 5 [4, 5, 4]) = 2 := sorry

theorem declaration uses `sorry`test_removeAll2 : count 5 (removeAll 5 [2, 5, 5, 5, 1]) = 0 := sorry

5.2.10. Included🔗

                    Exercise★★★(included) (Optional)
def declaration uses `sorry`included (l₁ l₂ : NatList) : Bool := sorry
theorem declaration uses `sorry`included_nil (l₂ : NatList) : included nil l₂ = true := sorry
theorem declaration uses `sorry`included_cons_member (n : Nat) (l₁ l₂ : NatList)
  (h : member n l₂ = true) :
    included (cons n l₁) l₂ = included l₁ (removeOne n l₂) := byn:Natl₁:NatListl₂:NatListh:member n l₂ = true⊢ (n :: l₁).included l₂ = l₁.included (removeOne n l₂)
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`included_cons_nonmember (n : Nat) (l₁ l₂ : NatList)
  (h : member n l₂ = false) :
    included (cons n l₁) l₂ = false := byn:Natl₁:NatListl₂:NatListh:member n l₂ = false⊢ (n :: l₁).included l₂ = false
  sorryAll goals completed! 🐙
example : included [1] [2, 1] = true := by⊢ [1].included [2, 1] = true
  rw [included_cons_member⊢ [].included (removeOne 1 [2, 1]) = trueh⊢ member 1 [2, 1] = true]⊢ [].included (removeOne 1 [2, 1]) = trueh⊢ member 1 [2, 1] = true
  ·⊢ [].included (removeOne 1 [2, 1]) = true exact included_nil _All goals completed! 🐙
  ·h⊢ member 1 [2, 1] = true rw [member_cons_diff _ _ _ rflh⊢ member 1 [1] = true]h⊢ member 1 [1] = true
    rw [member_cons_same _ _ _ rflh⊢ true = true]All goals completed! 🐙

declaration uses `sorry`example : included [1, 1] [2, 1, 4, 1] = true := sorry
theorem declaration uses `sorry`test_included1 : included [1, 2] [2, 1, 4, 1] = true := sorry

theorem declaration uses `sorry`test_included2 : included [1, 2, 2] [2, 1, 4, 1] = false := sorry

5.3. Reasoning About Lists🔗

As with numbers, simple facts about list-processing functions can sometimes be proved entirely by cases and rewriting, as shown for the following theorem.

theorem tail_length_pred (l : NatList) :
    l.length.pred = l.tail.length := byl:NatList⊢ l.length.pred = l.tail.length
  cases l with
  | nil       =>nil⊢ [].length.pred = [].tail.length rw [tail_nil,nil⊢ [].length.pred = [].length length_nilnil⊢ Nat.pred 0 = 0]nil⊢ Nat.pred 0 = 0; rflAll goals completed! 🐙
  | cons n l' =>consn:Natl':NatList⊢ (n :: l').length.pred = (n :: l').tail.length rw [tail_cons,consn:Natl':NatList⊢ (n :: l').length.pred = l'.length length_consconsn:Natl':NatList⊢ (l'.length + 1).pred = l'.length]consn:Natl':NatList⊢ (l'.length + 1).pred = l'.length; rflAll goals completed! 🐙

Here, the nil case works because we've chosen to define tail [] = []. Notice that the cons case introduces two names, n and l', corresponding to the fact that the cons constructor for lists takes two arguments (the head and tail of the list it is constructing).

Usually, though, interesting theorems about lists require induction for their proofs. We'll see how to do this next.

(Micro-Sermon: As we get deeper into this material, simply reading proof scripts will not help you very much. Rather, it is important to step through the details of each one using Lean and think about what each step achieves. Otherwise it is more or less guaranteed that the exercises will make no sense when you get to them. 'Nuff said.)

5.3.1. Induction on Lists🔗

Proofs by induction over datatypes like NatList are a little less familiar than standard natural number induction, but the idea is equally simple. Each inductive declaration defines a set of data values that can be built up using the declared constructors. For example, a boolean can be either true or false; a number can be either 0 or else Nat.succ applied to another number; and a list can be either [] or else :: applied to a number and a list. Moreover, applications of the declared constructors to one another are the only possible shapes that elements of an inductively defined set can have.

This last fact directly gives rise to a way of reasoning about inductively defined sets: a number is either 0 or else it is Nat.succ applied to some smaller number; a list is either [] or else it is :: applied to some number and some smaller list; etc. Thus, if we have in mind some proposition P that mentions a list l and we want to argue that P holds for all lists, we can reason as follows:

First, show that P is true of l when l is [].
Then show that P is true of l when l is n :: l' for some number n and some smaller list l', assuming that P is true for l'.

Since larger lists can always be broken down into smaller ones, eventually reaching [], these two arguments together establish the truth of P for all lists l.

Here's a concrete example:

theorem append_assoc (l₁ l₂ l₃ : NatList) :
    (l₁ ++ l₂) ++ l₃ = l₁ ++ (l₂ ++ l₃) := byl₁:NatListl₂:NatListl₃:NatList⊢ l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃)
  induction l₁ with
  | nil =>nill₂:NatListl₃:NatList⊢ [] ++ l₂ ++ l₃ = [] ++ (l₂ ++ l₃)
    rw [nil_append,nill₂:NatListl₃:NatList⊢ l₂ ++ l₃ = [] ++ (l₂ ++ l₃) nil_appendnill₂:NatListl₃:NatList⊢ l₂ ++ l₃ = l₂ ++ l₃]All goals completed! 🐙
  | cons n l₁' ih =>consl₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ (n :: l₁') ++ l₂ ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃)
    rw [cons_append,consl₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ (n :: l₁' ++ l₂) ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃) cons_append,consl₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ n :: l₁' ++ l₂ ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃) cons_append,consl₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ n :: l₁' ++ l₂ ++ l₃ = n :: l₁' ++ (l₂ ++ l₃) ihconsl₂:NatListl₃:NatListn:Natl₁':NatListih:l₁' ++ l₂ ++ l₃ = l₁' ++ (l₂ ++ l₃)⊢ n :: l₁' ++ (l₂ ++ l₃) = n :: l₁' ++ (l₂ ++ l₃)]All goals completed! 🐙

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🔗

In some situations, it is necessary to generalize a statement in order to prove it by induction. Intuitively, the reason is that a more general statement also yields a more general (stronger) induction hypothesis. While the following statement is true, we cannot prove it directly:

theorem replicate_append_fail (c n : Nat) :
    replicate n c ++ replicate n c = replicate n (c + c) := byc:Natn:Nat⊢ replicate n c ++ replicate n c = replicate n (c + c)
  induction c with
  | zero =>zeron:Nat⊢ replicate n 0 ++ replicate n 0 = replicate n (0 + 0) rw [replicate_zero,zeron:Nat⊢ [] ++ [] = [] nil_appendzeron:Nat⊢ [] = []]All goals completed! 🐙
  | succ c' ih unsolved goals
succn c':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ n :: replicate n c' ++ (n :: replicate n c') = replicate n (c' + 1 + (c' + 1))=>
    rw [replicate_succ,succn:Natc':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ (n :: replicate n c') ++ (n :: replicate n c') = replicate n (c' + 1 + (c' + 1)) cons_appendsuccn:Natc':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ n :: replicate n c' ++ (n :: replicate n c') = replicate n (c' + 1 + (c' + 1))]succn:Natc':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ n :: replicate n c' ++ (n :: replicate n c') = replicate n (c' + 1 + (c' + 1))succn: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)`.

unsolved goals
succn c':Natih:replicate n c' ++ replicate n c' = replicate n (c' + c')⊢ n :: replicate n c' ++ (n :: replicate n c') = replicate n (c' + 1 + (c' + 1))

To get a more general induction hypothesis, we can generalize:

theorem replicate_append_general (c₁ c₂ n : Nat) :
    replicate n c₁ ++ replicate n c₂ = replicate n (c₁ + c₂) := byc₁:Natc₂:Natn:Nat⊢ replicate n c₁ ++ replicate n c₂ = replicate n (c₁ + c₂)
  induction c₁ with
  | zero =>zeroc₂:Natn:Nat⊢ replicate n 0 ++ replicate n c₂ = replicate n (0 + c₂)
    rw [replicate_zero,zeroc₂:Natn:Nat⊢ [] ++ replicate n c₂ = replicate n (0 + c₂) Nat.zero_add,zeroc₂:Natn:Nat⊢ [] ++ replicate n c₂ = replicate n c₂ nil_appendzeroc₂:Natn:Nat⊢ replicate n c₂ = replicate n c₂]All goals completed! 🐙
  | succ c1' ih =>succc₂: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₂)
    rw [Nat.add_right_comm,succc₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ replicate n (c1' + 1) ++ replicate n c₂ = replicate n (c1' + c₂ + 1) replicate_succ,succc₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ (n :: replicate n c1') ++ replicate n c₂ = replicate n (c1' + c₂ + 1) replicate_succ,succc₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ (n :: replicate n c1') ++ replicate n c₂ = n :: replicate n (c1' + c₂) cons_append,succc₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ n :: replicate n c1' ++ replicate n c₂ = n :: replicate n (c1' + c₂) ihsuccc₂:Natn:Natc1':Natih:replicate n c1' ++ replicate n c₂ = replicate n (c1' + c₂)⊢ n :: replicate n (c1' + c₂) = n :: replicate n (c1' + 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) := byc:Natn:Nat⊢ replicate n c ++ replicate n c = replicate n (c + c)
  exact replicate_append_general c c nAll goals completed! 🐙

5.3.1.2. Reversing a List🔗

For a slightly more involved example of inductive proof over lists, suppose we use append to define a list-reversing function reverse:

def reverse (l : NatList) : NatList :=
  match l with
  | [] => []
  | h :: t => t.reverse ++ [h]

theorem reverse_nil : [].reverse = [] := by⊢ [].reverse = [] rflAll goals completed! 🐙

theorem reverse_cons (h : Nat) (t : NatList) : (h :: t).reverse = t.reverse ++ [h] := byh:Natt:NatList⊢ (h :: t).reverse = t.reverse ++ [h] rflAll goals completed! 🐙

example : [1, 2, 3].reverse = [3, 2, 1] := by⊢ [1, 2, 3].reverse = [3, 2, 1] rflAll goals completed! 🐙

example : [].reverse = [] := by⊢ [].reverse = [] rflAll goals completed! 🐙

Let's prove that reversing a list does not change its length. Our first attempt gets stuck in the successor case...

example (l : NatList) :
    l.reverse.length = l.length := byl:NatList⊢ l.reverse.length = l.length
  induction l with
  | nil =>nil⊢ [].reverse.length = [].length rw [reverse_nilnil⊢ [].length = [].length]All goals completed! 🐙
  | cons n l' ih unsolved goals
consn:Natl':NatListih:l'.reverse.length = l'.length⊢ (l'.reverse ++ [n]).length = (n :: l').length=>
    rw [reverse_consconsn:Natl':NatListih:l'.reverse.length = l'.length⊢ (l'.reverse ++ [n]).length = (n :: l').length]consn:Natl':NatListih:l'.reverse.length = l'.length⊢ (l'.reverse ++ [n]).length = (n :: l').lengthconsn: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!

unsolved goals
consn:Natl':NatListih:l'.reverse.length = l'.length⊢ (l'.reverse ++ [n]).length = (n :: l').length

A first attempt to make progress would be to prove exactly the statement that we are missing at this point. But this attempt will fail because the induction hypothesis is not general enough.

theorem length_append_succ (l : NatList) (n : Nat) :
    (l.reverse ++ [n]).length = l.reverse.length + 1 := byl:NatListn:Nat⊢ (l.reverse ++ [n]).length = l.reverse.length + 1
  induction l with
  | nil =>niln:Nat⊢ ([].reverse ++ [n]).length = [].reverse.length + 1
    rw [reverse_nil,niln:Nat⊢ ([] ++ [n]).length = [].length + 1 nil_append,niln:Nat⊢ [n].length = [].length + 1 length_cons,niln:Nat⊢ [].length + 1 = [].length + 1 length_nilniln:Nat⊢ 0 + 1 = 0 + 1]All goals completed! 🐙
  | cons m l' ih unsolved goals
consn m:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ (l'.reverse ++ [m] ++ [n]).length = (l'.reverse ++ [m]).length + 1=>
    rw [reverse_consconsn:Natm:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ (l'.reverse ++ [m] ++ [n]).length = (l'.reverse ++ [m]).length + 1]consn:Natm:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ (l'.reverse ++ [m] ++ [n]).length = (l'.reverse ++ [m]).length + 1consn:Natm:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ ((m :: l').reverse ++ [n]).length = (m :: l').reverse.length + 1
    -- `ih` not applicable

unsolved goals
consn m:Natl':NatListih:(l'.reverse ++ [n]).length = l'.reverse.length + 1⊢ (l'.reverse ++ [m] ++ [n]).length = (l'.reverse ++ [m]).length + 1

It turns out that the above lemma is more specific than it needs to be. We can strengthen the lemma to work not only on reversed lists but on general lists.

theorem append_length_succ (l : NatList) (n : Nat) :
    (l ++ [n]).length = l.length + 1 := byl:NatListn:Nat⊢ (l ++ [n]).length = l.length + 1
  induction l with
  | nil =>niln:Nat⊢ ([] ++ [n]).length = [].length + 1 rw [nil_append,niln:Nat⊢ [n].length = [].length + 1 length_consniln:Nat⊢ [].length + 1 = [].length + 1]All goals completed! 🐙
  | cons m l' ih =>consn:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ ((m :: l') ++ [n]).length = (m :: l').length + 1
    rw [cons_append,consn:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ (m :: l' ++ [n]).length = (m :: l').length + 1 length_cons,consn:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ (l' ++ [n]).length + 1 = (m :: l').length + 1 ih,consn:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ l'.length + 1 + 1 = (m :: l').length + 1 length_consconsn:Natm:Natl':NatListih:(l' ++ [n]).length = l'.length + 1⊢ l'.length + 1 + 1 = l'.length + 1 + 1]All goals completed! 🐙

Now we can prove the main theorem.

theorem length_reverse (l : NatList) :
    l.reverse.length = l.length := byl:NatList⊢ l.reverse.length = l.length
  induction l with
  | nil =>nil⊢ [].reverse.length = [].length rw [reverse_nilnil⊢ [].length = [].length]All goals completed! 🐙
  | cons n l' ih =>consn:Natl':NatListih:l'.reverse.length = l'.length⊢ (n :: l').reverse.length = (n :: l').length
    rw [reverse_cons,consn:Natl':NatListih:l'.reverse.length = l'.length⊢ (l'.reverse ++ [n]).length = (n :: l').length append_length_succ,consn:Natl':NatListih:l'.reverse.length = l'.length⊢ l'.reverse.length + 1 = (n :: l').length ih,consn:Natl':NatListih:l'.reverse.length = l'.length⊢ l'.length + 1 = (n :: l').length length_consconsn:Natl':NatListih:l'.reverse.length = l'.length⊢ l'.length + 1 = l'.length + 1]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 := byl₁:NatListl₂:NatList⊢ (l₁ ++ l₂).length = l₁.length + l₂.length
  induction l₁ with
  | nil =>nill₂:NatList⊢ ([] ++ l₂).length = [].length + l₂.length rw [nil_append,nill₂:NatList⊢ l₂.length = [].length + l₂.length length_nil,nill₂:NatList⊢ l₂.length = 0 + l₂.length Nat.zero_addnill₂:NatList⊢ l₂.length = l₂.length]All goals completed! 🐙
  | cons n l₁' ih =>consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ ((n :: l₁') ++ l₂).length = (n :: l₁').length + l₂.length
    rw [cons_append,consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ (n :: l₁' ++ l₂).length = (n :: l₁').length + l₂.length length_cons,consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ (l₁' ++ l₂).length + 1 = (n :: l₁').length + l₂.length ih,consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ l₁'.length + l₂.length + 1 = (n :: l₁').length + l₂.length length_cons,consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ l₁'.length + l₂.length + 1 = l₁'.length + 1 + l₂.length Nat.succ_addconsl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).length = l₁'.length + l₂.length⊢ l₁'.length + l₂.length + 1 = (l₁'.length + l₂.length).succ]All goals completed! 🐙

For comparison, here are informal proofs of these two theorems, length_append and length_reverse.

Theorem: For all lists l₁ and l₂,

(l₁ ++ l₂).length = l₁.length + l₂.length.

Proof: By induction on l₁.

First, suppose l₁ = []. We must show

([] ++ l₂).length = [].length + l₂.length,

which follows directly from the definitions of length, ++, and +.

Next, suppose l₁ = n :: l₁', with

(l₁' ++ l₂).length = l₁'.length + l₂.length

We must show

((n :: l₁') ++ l₂).length = (n :: l₁').length + l₂.length.

This follows directly from the definitions of length and ++ together with the induction hypothesis. QED.

Theorem: For all lists l, l.reverse.length = l.length.

Proof: By induction on l.

First, suppose l = []. We must show

[].reverse.length = [].length,

which follows directly from the definitions of length and reverse.

Next, suppose l = n :: l', with

l'.reverse.length = l'.length

We must show

(n :: l').reverse.length = (n :: l').length.

By the definition of reverse, this follows from

(l'.reverse ++ [n]).length = l'.length + 1,

which, by the previous lemma, is the same as

l'.reverse.length + [n].length = l'.length + 1.

This follows directly from the induction hypothesis and the definition of length. QED.

The style of these proofs is rather long-winded and pedantic. After reading a couple like this, we might find it easier to follow proofs that give fewer details (which we can easily work out in our own minds or on scratch paper if necessary) and just highlight the non-obvious steps. In this more compressed style, the above proof might look like this:

Theorem: For all lists l, l.reverse.length = l.length.

Proof: First observe, by a straightforward induction on l₁, that (l₁ ++ l₂).length = l₁.length + l₂.length for any l₁ and l₂. The main property then follows by induction on l, using the observation together with the induction hypothesis in the case where l = n' :: l'. QED.

Which style is preferable in a given situation depends on the sophistication of the expected audience and how similar the proof at hand is to ones that they will already be familiar with. The more pedantic style is a good default for our present purposes because we're trying to be very clear about the details.

5.3.2. List Exercises, Part 1🔗

Exercise★★★(list_exercises)

More practice with lists:

theorem declaration uses `sorry`append_nil (l : NatList) :
    l ++ [] = l := byl:NatList⊢ l ++ [] = l
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`reverse_append (l₁ l₂ : NatList) :
   (l₁ ++ l₂).reverse = l₂.reverse ++ l₁.reverse := byl₁:NatListl₂:NatList⊢ (l₁ ++ l₂).reverse = l₂.reverse ++ l₁.reverse
  sorryAll goals completed! 🐙

An involution is a function that is its own inverse. That is, applying the function twice yields the original input.

theorem declaration uses `sorry`reverse_involutive (l : NatList) :
    l.reverse.reverse = l := byl:NatList⊢ l.reverse.reverse = l
  sorryAll goals completed! 🐙

There is a short solution to the next one. If you find yourself getting tangled up, step back and try to look for a simpler way.

theorem declaration uses `sorry`append_assoc4 (l₁ l₂ l₃ l4 : NatList) :
    l₁ ++ (l₂ ++ (l₃ ++ l4)) = ((l₁ ++ l₂) ++ l₃) ++ l4 := byl₁:NatListl₂:NatListl₃:NatListl4:NatList⊢ l₁ ++ (l₂ ++ (l₃ ++ l4)) = l₁ ++ l₂ ++ l₃ ++ l4
  sorryAll goals completed! 🐙

An exercise about your implementation of nonZeros:

theorem declaration uses `sorry`nonZeros_append (l₁ l₂ : NatList) :
    nonZeros (l₁ ++ l₂) = (nonZeros l₁) ++ (nonZeros l₂) := byl₁:NatListl₂:NatList⊢ (l₁ ++ l₂).nonZeros = l₁.nonZeros ++ l₂.nonZeros
  sorryAll goals completed! 🐙

Exercise★★(beq)

Fill in the definition of beq, which compares lists of numbers for equality. Prove that beq l l yields true for every list l.

def declaration uses `sorry`beq (l₁ l₂ : NatList) : Bool := sorry

theorem declaration uses `sorry`beq_nil : beq [] [] = true := sorry

theorem declaration uses `sorry`beq_cons_same (h₁ h₂ : Nat) (t₁ t₂ : NatList)
  (h : (h₁ == h₂) = true) :
    beq (h₁ :: t₁) (h₂ :: t₂) = beq t₁ t₂ := byh₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = true⊢ (h₁ :: t₁).beq (h₂ :: t₂) = t₁.beq t₂
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`beq_cons_diff (h₁ h₂ : Nat) (t₁ t₂ : NatList)
  (h : (h₁ == h₂) = false) :
    beq (h₁ :: t₁) (h₂ :: t₂) = false := byh₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = false⊢ (h₁ :: t₁).beq (h₂ :: t₂) = false
  sorryAll goals completed! 🐙

declaration uses `sorry`example : beq [] [] = true := sorry
declaration uses `sorry`example : beq [1, 2, 3] [1, 2, 3] = true := sorry
declaration uses `sorry`example : beq [1, 2, 3] [1, 2, 4] = false := by⊢ [1, 2, 3].beq [1, 2, 4] = false
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`beq_refl (l : NatList) :
    beq l l = true := byl:NatList⊢ l.beq l = true
  sorryAll goals completed! 🐙

5.3.3. List Exercises, Part 2🔗

open NatList

Here are a couple of little theorems to prove about your definition above.

Exercise★(count_member_nonZero)

theorem declaration uses `sorry`count_member_nonZero (l : NatList) :
    Nat.ble 1 (count 1 (1 :: l)) = true := byl:NatList⊢ Nat.ble 1 (count 1 (1 :: l)) = true
  sorryAll goals completed! 🐙

The following lemma about Nat.ble might help you in the next exercise (it will also be useful in later chapters).

theorem ble_self_succ (n : Nat) :
    Nat.ble n (n + 1) = true := byn:Nat⊢ n.ble (n + 1) = true
  induction n with
  | zero       =>zero⊢ Nat.ble 0 (0 + 1) = true rflAll goals completed! 🐙
  | succ n' ih =>succn':Natih:n'.ble (n' + 1) = true⊢ (n' + 1).ble (n' + 1 + 1) = true rw [Nat.blesuccn':Natih:n'.ble (n' + 1) = true⊢ n'.ble (n' + 1) = true]succn':Natih:n'.ble (n' + 1) = true⊢ n'.ble (n' + 1) = true; exact ihAll goals completed! 🐙

Exercise★★★(remove_does_not_increase_count) (Advanced)

theorem declaration uses `sorry`remove_does_not_increase_count (l : NatList) :
    Nat.ble (count 0 (removeOne 0 l)) (count 0 l) = true := byl:NatList⊢ (count 0 (removeOne 0 l)).ble (count 0 l) = true
  sorryAll goals completed! 🐙

Exercise★★★(count_append) (Optional, Manually graded)

Write down an interesting theorem count_append about lists involving the functions count and append, and prove it. (You may find that the difficulty of the proof depends on how you defined count!)

Exercise★★★(involutive_injective) (Advanced)

Prove that every involution is injective.

Involutions were defined above in reverse_involutive. An injective function is one-to-one: it maps distinct inputs to distinct outputs, without any collisions.

theorem declaration uses `sorry`involutive_injective (f : Nat → Nat)
  (hInv : ∀ n : Nat, n = f (f n)) :
    (∀ n₁ n₂ : Nat, f n₁ = f n₂ → n₁ = n₂) := byf:Nat → NathInv:∀ (n : Nat), n = f (f n)⊢ ∀ (n₁ n₂ : Nat), f n₁ = f n₂ → n₁ = n₂
  sorryAll goals completed! 🐙

Exercise★★(reverse_injective) (Advanced)

Prove that reverse is injective. Do not prove this by induction — that would be hard. Instead, reuse the same proof technique that you used for involutive_injective. (But: Don't try to use that exercise directly as a lemma: the types are not the same!)

theorem declaration uses `sorry`reverse_injective (l₁ l₂ : NatList)
    (h : l₁.reverse = l₂.reverse) : l₁ = l₂ := byl₁:NatListl₂:NatListh:l₁.reverse = l₂.reverse⊢ l₁ = l₂
  sorryAll goals completed! 🐙

5.4. Options🔗

Suppose we want to write a function that returns the nth element of some list. If we give it type NatList → Nat → Nat, then we'll have to choose some number to return when 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'

This solution is not so good, since in some cases this default value of 42 could appear in the input list, and thus will not clearly indicate that n was greater than the length of the list. A better alternative is to change the return type to include an error value as a possible outcome. We call this new type NatOption.

end NatList

inductive NatOption : Type where
  | some (n : Nat)
  | none

namespace NatList

We can then change the above definition of nthBad to return NatOption.none when the list is too short and some a when the list has enough members and a appears at position n. We call this new function nth? to indicate that it may result in an error.

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 := by⊢ [4, 5, 6, 7].nth? 0 = NatOption.some 4 rflAll goals completed! 🐙
example : nth? [4, 5, 6, 7] 3 = .some 7 := by⊢ [4, 5, 6, 7].nth? 3 = NatOption.some 7 rflAll goals completed! 🐙
example : nth? [4, 5, 6, 7] 9 = .none := by⊢ [4, 5, 6, 7].nth? 9 = NatOption.none rflAll goals completed! 🐙

The function below pulls the Nat out of a NatOption, returning a supplied default in the none case.

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 := byd:Nat⊢ elim d NatOption.none = d rflAll goals completed! 🐙

theorem NatOption.elim_some (d₁ d₂ : Nat) : elim d₁ (.some d₂) = d₂ := byd₁:Natd₂:Nat⊢ elim d₁ (NatOption.some d₂) = d₂ rflAll goals completed! 🐙

Exercise★★(head?)

Using the same idea, fix the head function from earlier so we don't have to pass a default element for the nil case.

def declaration uses `sorry`head? (l : NatList) : NatOption := sorry

declaration uses `sorry`example : head? [] = .none := sorry
theorem declaration uses `sorry`test_head?1 : head? [1] = .some 1 := sorry
theorem declaration uses `sorry`test_head?2 : head? [5, 6] = .some 5 := sorry

Exercise★(option_elim_head?) (Optional)

This exercise relates your new head? to the old head.

theorem declaration uses `sorry`option_elim_head? (l : NatList) (default : Nat) :
    head default l = NatOption.elim default (head? l) := byl:NatListdefault:Nat⊢ head default l = NatOption.elim default l.head?
  sorryAll 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

Exercise★(MyId.beq_refl)

theorem declaration uses `sorry`MyId.beq_refl (x : MyId) : MyId.beq x x = true := byx:MyId⊢ x.beq x = true
  sorryAll goals completed! 🐙

Now we define the type of partial maps:

inductive PartialMap : Type where
  | empty : PartialMap
  | record (i : MyId) (n : Nat) (m : PartialMap) : PartialMap

This declaration can be read: "There are two ways to construct a PartialMap: either using the constructor empty to represent an empty partial map, or applying the constructor record to a key, a value, and an existing PartialMap to construct a PartialMap with an additional key-to-value mapping."

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

Last, the find function searches a PartialMap for a given key. It returns none if the key was not found and some val if the key was associated with val. If the same key is mapped to multiple values, find will return the first one it encounters.

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'

Quiz

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

Quiz

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

Exercise★(update_eq)

theorem declaration uses `sorry`update_eq (d : PartialMap) (x : MyId) (n : Nat) :
    find x (update d x n) = .some n := byd:PartialMapx:MyIdn:Nat⊢ find x (d.update x n) = NatOption.some n
  sorryAll goals completed! 🐙

Exercise★(update_neq)

theorem declaration uses `sorry`update_neq (d : PartialMap) (x y : MyId) (o : Nat) :
    MyId.beq x y = false → find x (update d y o) = find x d := byd:PartialMapx:MyIdy:MyIdo:Nat⊢ x.beq y = false → find x (d.update y o) = find x d
  sorryAll goals completed! 🐙

end PartialMap

end Lists

Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC