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)

Note to developers (Mike Hicks @mwhicks1)

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 := 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 snd_fst_is_swap (p : NatProd) :
    (⟨p.snd, p.fst⟩ : NatProd) = p.swap := byp:NatProd⊢ NatProd.pair p.snd p.fst = p.swap
  solution!
    cases ppairn1✝:Natn2✝:Nat⊢ NatProd.pair (NatProd.pair n1✝ n2✝).snd (NatProd.pair n1✝ n2✝).fst = (NatProd.pair n1✝ n2✝).swap; rflAll goals completed! 🐙

Exercise★(fst_swap_is_snd) (Optional)

theorem fst_swap_is_snd (p : NatProd) :
    p.swap.fst = p.snd := byp:NatProd⊢ p.swap.fst = p.snd
  solution!
    cases ppairn1✝:Natn2✝:Nat⊢ (NatProd.pair n1✝ n2✝).swap.fst = (NatProd.pair n1✝ n2✝).snd; rflAll 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🔗

Note to developers (Michael Hicks @mwhicks1)

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?

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 nonZeros (l : NatList) : NatList := solution!(
  match l with
  | [] => []
  | 0 :: t => nonZeros t
  | h :: t => h :: nonZeros t
)

The following lemmas should hold about your definition.

theorem nonZeros_cons_zero (t : NatList) :
    nonZeros (0 :: t) = nonZeros t := solution!(byt:NatList⊢ (0 :: t).nonZeros = t.nonZeros rflAll goals completed! 🐙)

theorem nonZeros_nil :
    nonZeros [] = [] := solution!(by⊢ [].nonZeros = [] rflAll goals completed! 🐙)

theorem nonZeros_cons_nonZero (h : Nat) (t : NatList) :
    nonZeros ((h + 1) :: t) = (h + 1) :: nonZeros t := solution!(byh:Natt:NatList⊢ ((h + 1) :: t).nonZeros = (h + 1) :: t.nonZeros rflAll goals completed! 🐙)

theorem test_nonZeros : nonZeros [0, 1, 0] = [1] := by⊢ [0, 1, 0].nonZeros = [1]
  solution!
    rw [nonZeros_cons_zero⊢ [1, 0].nonZeros = [1]]⊢ [1, 0].nonZeros = [1]
    rw [nonZeros_cons_nonZero⊢ (0 + 1) :: [0].nonZeros = [1]]⊢ (0 + 1) :: [0].nonZeros = [1]
    rw [nonZeros_cons_zero⊢ (0 + 1) :: [].nonZeros = [1]]⊢ (0 + 1) :: [].nonZeros = [1]
    rw [nonZeros_nil⊢ [0 + 1] = [1]]All 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 oddMembers (l : NatList) : NatList := solution!(
  match l with
  | [] => []
  | h :: t => bif h.odd then h :: oddMembers t else oddMembers t)

theorem oddMembers_nil :
    oddMembers [] = [] := solution!(by⊢ [].oddMembers = [] rflAll goals completed! 🐙)

theorem oddMembers_cons (h : Nat) (t : NatList) :
    oddMembers (h :: t) =
      bif h.odd then h :: oddMembers t else oddMembers t :=
  solution!(byh:Natt:NatList⊢ (h :: t).oddMembers = bif h.odd then h :: t.oddMembers else t.oddMembers rflAll goals completed! 🐙)

theorem 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
  solution!
    rw [oddMembers_cons,n:Natl:NatListh:n.odd = true⊢ (bif n.odd then n :: l.oddMembers else l.oddMembers) = n :: l.oddMembers h,n:Natl:NatListh:n.odd = true⊢ (bif true then n :: l.oddMembers else l.oddMembers) = n :: l.oddMembers Bool.cond_truen:Natl:NatListh:n.odd = true⊢ n :: l.oddMembers = n :: l.oddMembers]All goals completed! 🐙

theorem 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
  solution!
    rw [oddMembers_cons,n:Natl:NatListh:n.odd = false⊢ (bif n.odd then n :: l.oddMembers else l.oddMembers) = l.oddMembers h,n:Natl:NatListh:n.odd = false⊢ (bif false then n :: l.oddMembers else l.oddMembers) = l.oddMembers Bool.cond_falsen:Natl:NatListh:n.odd = false⊢ l.oddMembers = l.oddMembers]All 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.

example : oddMembers [1, 2] = [1] := solution!(by⊢ [1, 2].oddMembers = [1] rflAll goals completed! 🐙)

theorem test_oddMembers : oddMembers [0, 1, 2, 3, 0] = [1, 3] := solution!(by⊢ [0, 1, 2, 3, 0].oddMembers = [1, 3] rflAll goals completed! 🐙)

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

def countOddMembers (l : NatList) : Nat := solution!(
  (oddMembers l).length)

example : countOddMembers [0, 1, 2, 3, 0] = 2 := solution!(by⊢ [0, 1, 2, 3, 0].countOddMembers = 2 rflAll goals completed! 🐙)

theorem test_countOddMembers1 : countOddMembers [0, 2, 4] = 0 := solution!(by⊢ [0, 2, 4].countOddMembers = 0 rflAll goals completed! 🐙)

theorem test_countOddMembers2 : countOddMembers [] = 0 := solution!(by⊢ [].countOddMembers = 0 rflAll goals completed! 🐙)

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 alternate (l₁ l₂ : NatList) : NatList := solution!(
  match l₁, l₂ with
  | [], _ => l₂
  | _, [] => l₁
  | h₁ :: t₁, h₂ :: t₂ => h₁ :: h₂ :: alternate t₁ t₂)

theorem test_alternate1 :
    alternate [1, 2, 3] [4, 5, 6] = [1, 4, 2, 5, 3, 6] := solution!(by⊢ [1, 2, 3].alternate [4, 5, 6] = [1, 4, 2, 5, 3, 6] rflAll goals completed! 🐙)

theorem test_alternate2 :
    alternate [1] [4, 5, 6] = [1, 4, 5, 6] := solution!(by⊢ [1].alternate [4, 5, 6] = [1, 4, 5, 6] rflAll goals completed! 🐙)

theorem test_alternate3 :
    alternate [1, 2, 3] [4] = [1, 4, 2, 3] := solution!(by⊢ [1, 2, 3].alternate [4] = [1, 4, 2, 3] rflAll goals completed! 🐙)

theorem test_alternate4 :
    alternate [] [20, 30] = [20, 30] := solution!(by⊢ [].alternate [20, 30] = [20, 30] rflAll goals completed! 🐙)

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 count (n : Nat) (l : NatList) : Nat := solution!(
  match l with
  | [] => 0
  | h :: t => bif n == h then count n t + 1 else count n t)

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

theorem count_nil (n : Nat) : count n [] = 0 := solution!(byn:Nat⊢ count n [] = 0 rflAll goals completed! 🐙)

theorem count_cons_def (n h : Nat) (t : NatList) :
    count n (h :: t) =
      bif n == h then count n t + 1 else count n t := solution!(byn:Nath:Natt:NatList⊢ count n (h :: t) = bif n == h then count n t + 1 else count n t rflAll goals completed! 🐙)

theorem 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
  solution!
    rw [count_cons_def,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif n₁ == n₂ then count n₁ t + 1 else count n₁ t) = count n₁ t + 1 h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif true then count n₁ t + 1 else count n₁ t) = count n₁ t + 1 `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_truen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ count n₁ t + 1 = count n₁ t + 1]All goals completed! 🐙

theorem 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
  solution!
    rw [count_cons_def,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif n₁ == n₂ then count n₁ t + 1 else count n₁ t) = count n₁ t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif false then count n₁ t + 1 else count n₁ t) = count n₁ t `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falsen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ count n₁ t = count n₁ t]All 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! 🐙

example : count 2 [2, 2] = 2 := solution!(by⊢ count 2 [2, 2] = 2 rflAll goals completed! 🐙)

theorem test_count1 : count 1 [1, 1, 4] = 2 := solution!(by⊢ count 1 [1, 1, 4] = 2 rflAll goals completed! 🐙)

theorem test_count2 : count 5 [1, 1, 4] = 0 := solution!(by⊢ count 5 [1, 1, 4] = 0 rflAll goals completed! 🐙)

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.

example : count 1 [1, 2, 3, 1, 4, 1] = 3 := solution!(by⊢ count 1 [1, 2, 3, 1, 4, 1] = 3 rflAll goals completed! 🐙)
example : count 6 [1, 2, 3, 1, 4, 1] = 0 := solution!(by⊢ count 6 [1, 2, 3, 1, 4, 1] = 0 rflAll goals completed! 🐙)

5.2.8. Membership🔗

Exercise★(membership)

def member (n : Nat) (l : NatList) : Bool := solution!(
  match l with
  | [] => false
  | h :: t => bif n == h then true else member n t)

theorem member_nil (n : Nat) : member n [] = false := solution!(byn:Nat⊢ member n [] = false rflAll goals completed! 🐙)

theorem 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
  solution!
    rw [member,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif n₁ == n₂ then true else member n₁ t) = true h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif true then true else member n₁ t) = true `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_truen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ true = true]All goals completed! 🐙

theorem 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
  solution!
    rw [member,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif n₁ == n₂ then true else member n₁ t) = member n₁ t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif false then true else member n₁ t) = member n₁ t `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falsen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ member n₁ t = member n₁ t]All goals completed! 🐙

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

example : member 2 [1] = false := solution!(by⊢ member 2 [1] = false rflAll goals completed! 🐙)

theorem test_member1 : member 1 [1, 4, 1] = true := solution!(by⊢ member 1 [1, 4, 1] = true rflAll goals completed! 🐙)

theorem test_member2 : member 2 [1, 4, 1] = false := solution!(by⊢ member 2 [1, 4, 1] = false rflAll goals completed! 🐙)

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 removeOne (n : Nat) (l : NatList) : NatList := solution!(
  match l with
  | [] => nil
  | h :: t => bif n == h then t else h :: removeOne n t)

theorem removeOne_nil (n : Nat) : removeOne n nil = nil := solution!(byn:Nat⊢ removeOne n [] = [] rflAll goals completed! 🐙)

theorem 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
  solution!
    rw [removeOne,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif n₁ == n₂ then t else n₂ :: removeOne n₁ t) = t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif true then t else n₂ :: removeOne n₁ t) = t `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_truen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ t = t]All goals completed! 🐙

theorem 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
  solution!
    rw [removeOne,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif n₁ == n₂ then t else n₂ :: removeOne n₁ t) = n₂ :: removeOne n₁ t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif false then t else n₂ :: removeOne n₁ t) = n₂ :: removeOne n₁ t `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falsen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ n₂ :: removeOne n₁ t = n₂ :: removeOne n₁ t]All 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! 🐙

example : count 5 (removeOne 5 [1, 5, 4]) = 0 := solution!(by⊢ count 5 (removeOne 5 [1, 5, 4]) = 0 rflAll goals completed! 🐙)

theorem test_removeOne1 : count 4 (removeOne 5 [4, 5, 1, 4]) = 2 := solution!(by⊢ count 4 (removeOne 5 [4, 5, 1, 4]) = 2 rflAll goals completed! 🐙)

theorem test_removeOne2 : count 5 (removeOne 5 [1, 5, 5, 4]) = 1 := solution!(by⊢ count 5 (removeOne 5 [1, 5, 5, 4]) = 1 rflAll goals completed! 🐙)

Exercise★★★(removeAll) (Optional)

def removeAll (n : Nat) (l : NatList) : NatList := solution!(
  match l with
  | [] => []
  | h :: t => bif n == h then removeAll n t else h :: removeAll n t)

theorem removeAll_nil (n : Nat) : removeAll n [] = [] := solution!(byn:Nat⊢ removeAll n [] = [] rflAll goals completed! 🐙)

theorem 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
  solution!
    rw [removeAll,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif n₁ == n₂ then removeAll n₁ t else n₂ :: removeAll n₁ t) = removeAll n₁ t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ (bif true then removeAll n₁ t else n₂ :: removeAll n₁ t) = removeAll n₁ t `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_truen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = true⊢ removeAll n₁ t = removeAll n₁ t]All goals completed! 🐙

theorem 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
  solution!
    rw [removeAll,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif n₁ == n₂ then removeAll n₁ t else n₂ :: removeAll n₁ t) = n₂ :: removeAll n₁ t h,n₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ (bif false then removeAll n₁ t else n₂ :: removeAll n₁ t) = n₂ :: removeAll n₁ t `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falsen₁:Natn₂:Natt:NatListh:(n₁ == n₂) = false⊢ n₂ :: removeAll n₁ t = n₂ :: removeAll n₁ t]All 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! 🐙

example : count 5 (removeAll 5 [5, 5]) = 0 := solution!(by⊢ count 5 (removeAll 5 [5, 5]) = 0 rflAll goals completed! 🐙)

theorem test_removeAll1 : count 4 (removeAll 5 [4, 5, 4]) = 2 := solution!(by⊢ count 4 (removeAll 5 [4, 5, 4]) = 2 rflAll goals completed! 🐙)

theorem test_removeAll2 : count 5 (removeAll 5 [2, 5, 5, 5, 1]) = 0 := solution!(by⊢ count 5 (removeAll 5 [2, 5, 5, 5, 1]) = 0 rflAll goals completed! 🐙)

5.2.10. Included🔗

                    Exercise★★★(included) (Optional)
def included (l₁ l₂ : NatList) : Bool := solution!(
  match l₁ with
  | [] => true
  | h :: t => member h l₂ && included t (removeOne h l₂))
theorem included_nil (l₂ : NatList) : included nil l₂ = true := solution!(byl₂:NatList⊢ [].included l₂ = true rflAll goals completed! 🐙)
theorem 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₂)
  solution!
    rw [included,n:Natl₁:NatListl₂:NatListh:member n l₂ = true⊢ (member n l₂ && l₁.included (removeOne n l₂)) = l₁.included (removeOne n l₂) h,n:Natl₁:NatListl₂:NatListh:member n l₂ = true⊢ (true && l₁.included (removeOne n l₂)) = l₁.included (removeOne n l₂) Bool.true_andn:Natl₁:NatListl₂:NatListh:member n l₂ = true⊢ l₁.included (removeOne n l₂) = l₁.included (removeOne n l₂)]All goals completed! 🐙

theorem 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
  solution!
    rw [included,n:Natl₁:NatListl₂:NatListh:member n l₂ = false⊢ (member n l₂ && l₁.included (removeOne n l₂)) = false h,n:Natl₁:NatListl₂:NatListh:member n l₂ = false⊢ (false && l₁.included (removeOne n l₂)) = false Bool.false_andn:Natl₁:NatListl₂:NatListh:member n l₂ = false⊢ false = false]All 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! 🐙

example : included [1, 1] [2, 1, 4, 1] = true := solution!(by⊢ [1, 1].included [2, 1, 4, 1] = true rflAll goals completed! 🐙)
theorem test_included1 : included [1, 2] [2, 1, 4, 1] = true := solution!(by⊢ [1, 2].included [2, 1, 4, 1] = true rflAll goals completed! 🐙)

theorem test_included2 : included [1, 2, 2] [2, 1, 4, 1] = false := solution!(by⊢ [1, 2, 2].included [2, 1, 4, 1] = false rflAll goals completed! 🐙)

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
  workinclass!
    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 append_nil (l : NatList) :
    l ++ [] = l := byl:NatList⊢ l ++ [] = l
  solution!
    induction l with
    | nil =>nil⊢ [] ++ [] = [] rw [nil_appendnil⊢ [] = []]All goals completed! 🐙
    | cons n l' ih =>consn:Natl':NatListih:l' ++ [] = l'⊢ (n :: l') ++ [] = n :: l'
      rw [cons_append,consn:Natl':NatListih:l' ++ [] = l'⊢ n :: l' ++ [] = n :: l' ihconsn:Natl':NatListih:l' ++ [] = l'⊢ n :: l' = n :: l']All goals completed! 🐙

theorem reverse_append (l₁ l₂ : NatList) :
   (l₁ ++ l₂).reverse = l₂.reverse ++ l₁.reverse := byl₁:NatListl₂:NatList⊢ (l₁ ++ l₂).reverse = l₂.reverse ++ l₁.reverse
  solution!
    induction l₁ with
    | nil =>nill₂:NatList⊢ ([] ++ l₂).reverse = l₂.reverse ++ [].reverse rw [nil_append,nill₂:NatList⊢ l₂.reverse = l₂.reverse ++ [].reverse reverse_nil,nill₂:NatList⊢ l₂.reverse = l₂.reverse ++ [] append_nilnill₂:NatList⊢ l₂.reverse = l₂.reverse]All goals completed! 🐙
    | cons x l₁' ih =>consl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ ((x :: l₁') ++ l₂).reverse = l₂.reverse ++ (x :: l₁').reverse
      rw [cons_append,consl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ (x :: l₁' ++ l₂).reverse = l₂.reverse ++ (x :: l₁').reverse reverse_cons,consl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ (l₁' ++ l₂).reverse ++ [x] = l₂.reverse ++ (x :: l₁').reverse ih,consl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ l₂.reverse ++ l₁'.reverse ++ [x] = l₂.reverse ++ (x :: l₁').reverse reverse_cons,consl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ l₂.reverse ++ l₁'.reverse ++ [x] = l₂.reverse ++ (l₁'.reverse ++ [x]) append_assocconsl₂:NatListx:Natl₁':NatListih:(l₁' ++ l₂).reverse = l₂.reverse ++ l₁'.reverse⊢ l₂.reverse ++ (l₁'.reverse ++ [x]) = l₂.reverse ++ (l₁'.reverse ++ [x])]All goals completed! 🐙

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

theorem reverse_involutive (l : NatList) :
    l.reverse.reverse = l := byl:NatList⊢ l.reverse.reverse = l
  solution!
    induction l with
    | nil =>nil⊢ [].reverse.reverse = [] rw [reverse_nil,nil⊢ [].reverse = [] reverse_nilnil⊢ [] = []]All goals completed! 🐙
    | cons n l' ih =>consn:Natl':NatListih:l'.reverse.reverse = l'⊢ (n :: l').reverse.reverse = n :: l'
      rw [reverse_cons,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ (l'.reverse ++ [n]).reverse = n :: l' reverse_append,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ [n].reverse ++ l'.reverse.reverse = n :: l' ihconsn:Natl':NatListih:l'.reverse.reverse = l'⊢ [n].reverse ++ l' = n :: l']consn:Natl':NatListih:l'.reverse.reverse = l'⊢ [n].reverse ++ l' = n :: l'
      rw [reverse_cons,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ [].reverse ++ [n] ++ l' = n :: l' reverse,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ [] ++ [n] ++ l' = n :: l' nil_append,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ [n] ++ l' = n :: l' cons_append,consn:Natl':NatListih:l'.reverse.reverse = l'⊢ n :: [] ++ l' = n :: l' nil_appendconsn:Natl':NatListih:l'.reverse.reverse = l'⊢ n :: l' = n :: l']All 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 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
  solution!
    rw [append_assoc,l₁:NatListl₂:NatListl₃:NatListl4:NatList⊢ l₁ ++ (l₂ ++ (l₃ ++ l4)) = l₁ ++ l₂ ++ (l₃ ++ l4) append_assocl₁:NatListl₂:NatListl₃:NatListl4:NatList⊢ l₁ ++ (l₂ ++ (l₃ ++ l4)) = l₁ ++ (l₂ ++ (l₃ ++ l4))]All goals completed! 🐙

An exercise about your implementation of nonZeros:

theorem nonZeros_append (l₁ l₂ : NatList) :
    nonZeros (l₁ ++ l₂) = (nonZeros l₁) ++ (nonZeros l₂) := byl₁:NatListl₂:NatList⊢ (l₁ ++ l₂).nonZeros = l₁.nonZeros ++ l₂.nonZeros
  solution!
    induction l₁ with
    | nil =>nill₂:NatList⊢ ([] ++ l₂).nonZeros = [].nonZeros ++ l₂.nonZeros rw [nonZeros_nil,nill₂:NatList⊢ ([] ++ l₂).nonZeros = [] ++ l₂.nonZeros nil_append,nill₂:NatList⊢ l₂.nonZeros = [] ++ l₂.nonZeros nil_appendnill₂:NatList⊢ l₂.nonZeros = l₂.nonZeros]All goals completed! 🐙
    | cons n l₁' ih =>consl₂:NatListn:Natl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ ((n :: l₁') ++ l₂).nonZeros = (n :: l₁').nonZeros ++ l₂.nonZeros
      cases n with
      | zero =>cons.zerol₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ ((0 :: l₁') ++ l₂).nonZeros = (0 :: l₁').nonZeros ++ l₂.nonZeros
        rw [nonZeros_cons_zero,cons.zerol₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ ((0 :: l₁') ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros ← ih,cons.zerol₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ ((0 :: l₁') ++ l₂).nonZeros = (l₁' ++ l₂).nonZeros cons_append,cons.zerol₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ (0 :: l₁' ++ l₂).nonZeros = (l₁' ++ l₂).nonZeros nonZeros_cons_zerocons.zerol₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZeros⊢ (l₁' ++ l₂).nonZeros = (l₁' ++ l₂).nonZeros]All goals completed! 🐙
      | succ n' =>cons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ (((n' + 1) :: l₁') ++ l₂).nonZeros = ((n' + 1) :: l₁').nonZeros ++ l₂.nonZeros
        rw [cons_append,cons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ ((n' + 1) :: l₁' ++ l₂).nonZeros = ((n' + 1) :: l₁').nonZeros ++ l₂.nonZeros nonZeros_cons_nonZero,cons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ (n' + 1) :: (l₁' ++ l₂).nonZeros = ((n' + 1) :: l₁').nonZeros ++ l₂.nonZeros nonZeros_cons_nonZero,cons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ (n' + 1) :: (l₁' ++ l₂).nonZeros = ((n' + 1) :: l₁'.nonZeros) ++ l₂.nonZeros ih,cons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ (n' + 1) :: l₁'.nonZeros ++ l₂.nonZeros = ((n' + 1) :: l₁'.nonZeros) ++ l₂.nonZeros cons_appendcons.succl₂:NatListl₁':NatListih:(l₁' ++ l₂).nonZeros = l₁'.nonZeros ++ l₂.nonZerosn':Nat⊢ (n' + 1) :: l₁'.nonZeros ++ l₂.nonZeros = (n' + 1) :: l₁'.nonZeros ++ l₂.nonZeros]All 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 beq (l₁ l₂ : NatList) : Bool := solution!(
  match l₁, l₂ with
  | [], [] => true
  | h₁ :: t₁, h₂ :: t₂ => (h₁ == h₂) && beq t₁ t₂
  | _, _ => false)

theorem beq_nil : beq [] [] = true := solution!(by⊢ [].beq [] = true rflAll goals completed! 🐙)

theorem 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₂
  solution!
    rw [beq,h₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = true⊢ (h₁ == h₂ && t₁.beq t₂) = t₁.beq t₂ h,h₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = true⊢ (true && t₁.beq t₂) = t₁.beq t₂ Bool.true_andh₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = true⊢ t₁.beq t₂ = t₁.beq t₂]All goals completed! 🐙

theorem 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
  solution!
    rw [beq,h₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = false⊢ (h₁ == h₂ && t₁.beq t₂) = false h,h₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = false⊢ (false && t₁.beq t₂) = false Bool.false_andh₁:Nath₂:Natt₁:NatListt₂:NatListh:(h₁ == h₂) = false⊢ false = false]All goals completed! 🐙

example : beq [] [] = true := solution!(by⊢ [].beq [] = true rflAll goals completed! 🐙)
example : beq [1, 2, 3] [1, 2, 3] = true := solution!(by⊢ [1, 2, 3].beq [1, 2, 3] = true rflAll goals completed! 🐙)
example : beq [1, 2, 3] [1, 2, 4] = false := by⊢ [1, 2, 3].beq [1, 2, 4] = false
  solution!
    rw [beq_cons_same _ _ _ _ rfl⊢ [2, 3].beq [2, 4] = false]⊢ [2, 3].beq [2, 4] = false
    rw [beq_cons_same _ _ _ _ rfl⊢ [3].beq [4] = false]⊢ [3].beq [4] = false
    rw [beq_cons_diff _ _ _ _ rfl⊢ false = false]All goals completed! 🐙

theorem beq_refl (l : NatList) :
    beq l l = true := byl:NatList⊢ l.beq l = true
  solution!
    induction l with
    | nil =>nil⊢ [].beq [] = true rw [beq_nilnil⊢ true = true]All goals completed! 🐙
    | cons n l' ih =>consn:Natl':NatListih:l'.beq l' = true⊢ (n :: l').beq (n :: l') = true
      rw [beq_cons_same _ _ _ _ (BEq.refl n)consn:Natl':NatListih:l'.beq l' = true⊢ l'.beq l' = true]consn:Natl':NatListih:l'.beq l' = true⊢ l'.beq l' = true
      exact ihAll 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 count_member_nonZero (l : NatList) :
    Nat.ble 1 (count 1 (1 :: l)) = true := byl:NatList⊢ Nat.ble 1 (count 1 (1 :: l)) = true
  solution!
    rw [count_cons_samel:NatList⊢ Nat.ble 1 (count 1 l + 1) = truehl:NatList⊢ (1 == 1) = true]l:NatList⊢ Nat.ble 1 (count 1 l + 1) = truehl:NatList⊢ (1 == 1) = true <;>l:NatList⊢ Nat.ble 1 (count 1 l + 1) = truehl:NatList⊢ (1 == 1) = true rflAll 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 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
  solution!
    induction l with
    | nil =>nil⊢ (count 0 (removeOne 0 [])).ble (count 0 []) = true
      rw [removeOne_nil,nil⊢ (count 0 []).ble (count 0 []) = true count_nilnil⊢ Nat.ble 0 0 = true]nil⊢ Nat.ble 0 0 = true
      rflAll goals completed! 🐙
    | cons n s' ih =>consn:Nats':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = true⊢ (count 0 (removeOne 0 (n :: s'))).ble (count 0 (n :: s')) = true
      cases n with
      | zero =>cons.zeros':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = true⊢ (count 0 (removeOne 0 (0 :: s'))).ble (count 0 (0 :: s')) = true
        rw [removeOne_cons_same _ _ _ rfl,cons.zeros':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = true⊢ (count 0 s').ble (count 0 (0 :: s')) = true count_cons_same _ _ _ rfl,cons.zeros':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = true⊢ (count 0 s').ble (count 0 s' + 1) = true ble_self_succcons.zeros':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = true⊢ true = true]All goals completed! 🐙
      | succ n' =>cons.succs':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = truen':Nat⊢ (count 0 (removeOne 0 ((n' + 1) :: s'))).ble (count 0 ((n' + 1) :: s')) = true
        rw [removeOne_cons_diff _ _ _ rfl,cons.succs':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = truen':Nat⊢ (count 0 ((n' + 1) :: removeOne 0 s')).ble (count 0 ((n' + 1) :: s')) = true count_cons_diff _ _ _ rfl,cons.succs':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = truen':Nat⊢ (count 0 (removeOne 0 s')).ble (count 0 ((n' + 1) :: s')) = true count_cons_diff _ _ _ rflcons.succs':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = truen':Nat⊢ (count 0 (removeOne 0 s')).ble (count 0 s') = true]cons.succs':NatListih:(count 0 (removeOne 0 s')).ble (count 0 s') = truen':Nat⊢ (count 0 (removeOne 0 s')).ble (count 0 s') = true
        exact ihAll 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!)

theorem count_append (l₁ l₂ : NatList) (n : Nat) :
    count n (l₁ ++ l₂) = (count n l₁) + (count n l₂) := byl₁:NatListl₂:NatListn:Nat⊢ count n (l₁ ++ l₂) = count n l₁ + count n l₂
  induction l₁ with
  | nil =>nill₂:NatListn:Nat⊢ count n ([] ++ l₂) = count n [] + count n l₂
    rw [nil_append,nill₂:NatListn:Nat⊢ count n l₂ = count n [] + count n l₂ count_nil,nill₂:NatListn:Nat⊢ count n l₂ = 0 + count n l₂ Nat.zero_addnill₂:NatListn:Nat⊢ count n l₂ = count n l₂]All goals completed! 🐙
  | cons h s1' ih =>consl₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂⊢ count n ((h :: s1') ++ l₂) = count n (h :: s1') + count n l₂
    rw [cons_appendconsl₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂⊢ count n (h :: s1' ++ l₂) = count n (h :: s1') + count n l₂]consl₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂⊢ count n (h :: s1' ++ l₂) = count n (h :: s1') + count n l₂
    cases hv : (n == h) with
    | false =>cons.falsel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = false⊢ count n (h :: s1' ++ l₂) = count n (h :: s1') + count n l₂
      rw [count_cons_diff _ _ _ hv,cons.falsel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = false⊢ count n (s1' ++ l₂) = count n (h :: s1') + count n l₂ count_cons_diff _ _ _ hvcons.falsel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = false⊢ count n (s1' ++ l₂) = count n s1' + count n l₂]cons.falsel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = false⊢ count n (s1' ++ l₂) = count n s1' + count n l₂
      exact ihAll goals completed! 🐙
    | true =>cons.truel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = true⊢ count n (h :: s1' ++ l₂) = count n (h :: s1') + count n l₂
      rw [count_cons_same _ _ _ hv,cons.truel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = true⊢ count n (s1' ++ l₂) + 1 = count n (h :: s1') + count n l₂ count_cons_same _ _ _ hv,cons.truel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = true⊢ count n (s1' ++ l₂) + 1 = count n s1' + 1 + count n l₂ Nat.succ_add,cons.truel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = true⊢ count n (s1' ++ l₂) + 1 = (count n s1' + count n l₂).succ ← ihcons.truel₂:NatListn:Nath:Nats1':NatListih:count n (s1' ++ l₂) = count n s1' + count n l₂hv:(n == h) = true⊢ count n (s1' ++ l₂) + 1 = (count n (s1' ++ l₂)).succ]All goals completed! 🐙

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 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₂
  solution!
    intro n₁ n₂ hf:Nat → NathInv:∀ (n : Nat), n = f (f n)n₁:Natn₂:Nath:f n₁ = f n₂⊢ n₁ = n₂
    rw [hInv n₁,f:Nat → NathInv:∀ (n : Nat), n = f (f n)n₁:Natn₂:Nath:f n₁ = f n₂⊢ f (f n₁) = n₂ hInv n₂,f:Nat → NathInv:∀ (n : Nat), n = f (f n)n₁:Natn₂:Nath:f n₁ = f n₂⊢ f (f n₁) = f (f n₂) hf:Nat → NathInv:∀ (n : Nat), n = f (f n)n₁:Natn₂:Nath:f n₁ = f n₂⊢ f (f n₂) = f (f n₂)]All 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 reverse_injective (l₁ l₂ : NatList)
    (h : l₁.reverse = l₂.reverse) : l₁ = l₂ := byl₁:NatListl₂:NatListh:l₁.reverse = l₂.reverse⊢ l₁ = l₂
  solution!
    rw [← reverse_involutive l₁,l₁:NatListl₂:NatListh:l₁.reverse = l₂.reverse⊢ l₁.reverse.reverse = l₂ ← reverse_involutive l₂,l₁:NatListl₂:NatListh:l₁.reverse = l₂.reverse⊢ l₁.reverse.reverse = l₂.reverse.reverse hl₁:NatListl₂:NatListh:l₁.reverse = l₂.reverse⊢ l₂.reverse.reverse = l₂.reverse.reverse]All 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 head? (l : NatList) : NatOption := solution!(
  match l with
  | [] => .none
  | h :: _ => .some h)

example : head? [] = .none := solution!(by⊢ [].head? = NatOption.none rflAll goals completed! 🐙)
theorem test_head?1 : head? [1] = .some 1 := solution!(by⊢ [1].head? = NatOption.some 1 rflAll goals completed! 🐙)
theorem test_head?2 : head? [5, 6] = .some 5 := solution!(by⊢ [5, 6].head? = NatOption.some 5 rflAll goals completed! 🐙)

theorem head?_nil : head? [] = .none := solution!(by⊢ [].head? = NatOption.none rflAll goals completed! 🐙)

theorem head?_cons (h : Nat) (t : NatList) : head? (h :: t) = .some h := solution!(byh:Natt:NatList⊢ (h :: t).head? = NatOption.some h rflAll goals completed! 🐙)

Exercise★(option_elim_head?) (Optional)

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

theorem 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?
  solution!
    cases l with
    | nil =>nildefault:Nat⊢ head default [] = NatOption.elim default [].head? rw [head?_nil,nildefault:Nat⊢ head default [] = NatOption.elim default NatOption.none NatOption.elim_none,nildefault:Nat⊢ head default [] = default head_nilnildefault:Nat⊢ default = default]All goals completed! 🐙
    | cons n l' =>consdefault:Natn:Natl':NatList⊢ head default (n :: l') = NatOption.elim default (n :: l').head?
      rw [head_cons,consdefault:Natn:Natl':NatList⊢ n = NatOption.elim default (n :: l').head? head?_cons,consdefault:Natn:Natl':NatList⊢ n = NatOption.elim default (NatOption.some n) NatOption.elim_someconsdefault:Natn:Natl':NatList⊢ n = n]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

Exercise★(MyId.beq_refl)

theorem MyId.beq_refl (x : MyId) : MyId.beq x x = true := byx:MyId⊢ x.beq x = true
  solution!
    rw [beq,x:MyId⊢ (x.val == x.val) = true BEq.reflx:MyId⊢ true = 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

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

example (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
  rw [update,d:PartialMapx:MyIdn:Nat⊢ find x (record x n d) = NatOption.some n find,d:PartialMapx:MyIdn:Nat⊢ (bif x.beq x then NatOption.some n else find x d) = NatOption.some n MyId.beq_refl,d:PartialMapx:MyIdn:Nat⊢ (bif true then NatOption.some n else find x d) = NatOption.some n Bool.cond_trued:PartialMapx:MyIdn:Nat⊢ NatOption.some n = NatOption.some n]All goals completed! 🐙

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

example (d : PartialMap) (x y : MyId) (o : Nat)
    (h : MyId.beq x y = false) :
    find x (update d y o) = find x d := byd:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x (d.update y o) = find x d
  rw [update,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x (record y o d) = find x d find,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ (bif x.beq y then NatOption.some o else find x d) = find x d h,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ (bif false then NatOption.some o else find x d) = find x d Bool.cond_falsed:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x d = find x d]All goals completed! 🐙

Exercise★(update_eq)

theorem 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
  solution!
    rw [update,d:PartialMapx:MyIdn:Nat⊢ find x (record x n d) = NatOption.some n find,d:PartialMapx:MyIdn:Nat⊢ (bif x.beq x then NatOption.some n else find x d) = NatOption.some n MyId.beq_refl,d:PartialMapx:MyIdn:Nat⊢ (bif true then NatOption.some n else find x d) = NatOption.some n `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_trued:PartialMapx:MyIdn:Nat⊢ NatOption.some n = NatOption.some n]All goals completed! 🐙

Exercise★(update_neq)

theorem 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
  solution!
    intro hd:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x (d.update y o) = find x d
    rw [update,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x (record y o d) = find x d find,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ (bif x.beq y then NatOption.some o else find x d) = find x d h,d:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ (bif false then NatOption.some o else find x d) = find x d `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falsed:PartialMapx:MyIdy:MyIdo:Nath:x.beq y = false⊢ find x d = find x d]All goals completed! 🐙

end PartialMap

end Lists

Source revision: e85fe77, committed 2026-10-06 21:16 UTC