Link Search Menu Expand Document

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]