Behind the curtain
Nat is not alone. Inductive constructions can model a vast amount of mathematics.
We can create the propositions True and False using them.
inductive False : Prop where
inductive True : Prop where
| intro As you can see both False and True are more basic than Nat. With False you have no ways of building it. With True, you have exactly one: intro.
When building a function f : Nat → α, recursion told us we needed to specify a value of f for each way we construct a Nat: one for zero and one for each succ n. What does recursion look like here?
theorem False.elim {p : Prop} (no : False) : p := no.rec False.elim allows us to prove anything from a proof of a False. Why? Because when using recursion on False, there is nothing to recurse over. This is exactly the same reasoning that exhibits a function $\varnothing \to X$ for any set. (The match syntax expects terms so the proof uses the recursor rec underlying it.)
We can also build And and Or using inductive types.
inductive And (p q : Prop) : Prop where
| intro (left : p) (right : q)
inductive Or (p q : Prop) : Prop where
| inl (h : p)
| inr (h : q) Here are proofs of And.left and And.right.
theorem And.left {p q: Prop} (h : And p q) : p :=
match h with
| intro left _ => left
theorem And.right {p q: Prop} (h : And p q) : q :=
match h with
| intro _ right => right Or.elim becomes just another name for recursion.
theorem Or.elim {p q r : Prop} (h : Or p q) (h₁ : p → r)
(h₂ : q → r) : r :=
match h with
| inl h => h₁ h
| inr h => h₂ h We can also model existential propositions using inductive types.
inductive Exists {α : Type} (P : α → Prop) : Prop where
| intro (a : α) (h : P a)
theorem Exists.elim {α : Type} {p : Prop} {P : α → Prop}
(e : Exists P) (h : ∀ a, P a → p) : p :=
match e with
| intro a h' => h a h' Even equality fits into a inductive construction.
inductive Eq {α : Type} : α → α → Prop where
| refl (a : α) : Eq a a
theorem Eq.symm {α : Type} (a a' : α) (h : Eq a a') : Eq a' a := by
match h with
| refl a => exact Eq.refl a As we know from shopping, lists are also built recursively.
inductive List (α : Type) where
| nil
| cons (a : α) (as : List α) We start with an empty list nil and we build via cons our list by adding one thing, a:α, at a time.
def ShoppingList : List String :=
List.cons "nuts" (List.cons "cottage cheese"
(List.cons "grapes" List.nil))As this is cumbersome, Lean allows for familiar notation for lists.
def ShoppingList : List String :=
["nuts","cottage cheese","grapes"]We have the [] for the empty list and a::as to append a to the list as.
We can build useful functions on List using recursion
def Length {α : Type} (l : List α) : Nat :=
match l with
| [] => 0
| _::as => 1 + Length as
def Join {α : Type} (l₁ l₂ : List α) : List α :=
match l₁ with
| [] => l₂
| a::as => a :: Join as l₂ And we can prove results, like the additivity of length, under join.
theorem join_add_len {α : Type} {l₁ l₂ : List α} :
Length (Join l₁ l₂) = Length l₁ + Length l₂ := by
match l₁ with
| [] => simp [Length,Join]
| a::as => simp[Length]; rw [join_add_len,Nat.add_assoc]