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]