The natural numbers and reduction rules

Lean and its type theory — chapter 1

The natural numbers

Nat is an inductive type, generated by two constructors:

Nat.zero : Nat
Nat.succ : Nat → Nat

Every natural number is a finite tower of them: 2 is Nat.succ (Nat.succ Nat.zero). Numerals are notation.

Peano, 1889

A zero, a successor, and induction.
Dedekind gave the same analysis in 1888.
Induction is not a third constructor: it is the recursor, generated together with the type.

What was a list of axioms in 1889 is a type declaration here.

The recursor `Nat.rec`

Constructors build a value, the recursor consumes one. For a fixed type C:

Nat.rec : C → (Nat → C → C) → Nat → C

Nat.rec base step is the function f : Nat → C with f 0 = base and f (n + 1) = step n (f n).

Pattern matching, cases and induction compile down to Nat.rec.

`Nat.rec` computes

On a constructor, the recursor picks the matching case:

Nat.rec base step Nat.zero
  ⟶ base
Nat.rec base step (Nat.succ n)
  ⟶ step n (Nat.rec base step n)

Numerals such as 2 are put into constructor form first.

Example: `myDouble`

def step (_ j : Nat) : Nat := j + 2

def myDouble (n : Nat) : Nat :=
  Nat.rec 0 step n

--   myDouble 2
-- ⟶ Nat.rec 0 step 2           -- unfold myDouble
-- ⟶ step 1 (Nat.rec 0 step 1)  -- 2 = succ 1
-- ⟶ Nat.rec 0 step 1 + 2       -- unfold step
-- ⟶ step 0 (Nat.rec 0 step 0) + 2  -- 1 = succ 0
-- ⟶ Nat.rec 0 step 0 + 2 + 2   -- unfold step
-- ⟶ 0 + 2 + 2  ⟶  4            -- zero case, add
example : myDouble 2 = 4 := rfl

Definitional equality and `rfl`

Terms reduce: (fun x => x + 1) 4 becomes 5.
a ≡ b, definitionally equal: both reduce to a common form.
The kernel treats them as interchangeable (conversion).
Propositional equality a = b is a Prop and may need a proof.

rfl proves exactly a definitional equality.

The reduction rules

Rule	What it does	Example
α	rename a bound variable	`fun x => x` and `fun y => y`
β	apply a function	`(fun x => x + 1) 4 ⟶ 4 + 1`
η	`fun x => f x` equals `f`	`fun x => f x ⟶ f`
δ	unfold a definition	`twice 3 ⟶ 2 * 3`
ι	recursor on a constructor	`Nat.rec base step (n+1) ⟶ …`
ζ	substitute a `let`	`let x := 4; x + x ⟶ 4 + 4`

Rule

What it does

Example

rename a bound variable

fun x => x and fun y => y

apply a function

(fun x => x + 1) 4 ⟶ 4 + 1

fun x => f x equals f

fun x => f x ⟶ f

unfold a definition

twice 3 ⟶ 2 * 3

recursor on a constructor

Nat.rec base step (n+1) ⟶ …

substitute a let

let x := 4; x + x ⟶ 4 + 4

Names from Church's lambda calculus, 1930s.

What `rfl` sees: `α β η`

-- α: the bound name does not matter
example : (fun x : Nat => x)
    = (fun y : Nat => y) := rfl

-- β: apply a function
example : (fun x => x + 1) 4 = 5 := rfl

-- η: a function equals its expansion
example (f : Nat → Nat) :
    (fun x => f x) = f := rfl

What `rfl` sees: `δ ι ζ`

-- δ: unfold a definition
def twice (n : Nat) : Nat := 2 * n
example : twice 3 = 6 := rfl

-- ι: recursor on a constructor
example (b : Nat) (s : Nat → Nat → Nat) :
    Nat.rec (motive := fun _ => Nat)
      b s 0 = b := rfl

-- ζ: substitute a `let`
example : (let x := 4; x + x) = 8 := rfl

rfl is far stronger than "syntactically identical".

When `rfl` fails

Addition recurses on its second argument.

example (n : Nat) : n + 0 = n := rfl

example (n : Nat) : 0 + n = n := rflType mismatch
  rfl
has type
  ?m.9 = ?m.9
but is expected to have type
  0 + n = n

0 + n is stuck: with n a variable there is no constructor for the recursor to fire on.

Induction instead

example (n : Nat) : 0 + n = n := byn:Nat⊢ 0 + n = n
  induction n with
  | zero =>zero⊢ 0 + 0 = 0 rflAll goals completed! 🐙
  | succ k ih =>succk:Natih:0 + k = k⊢ 0 + (k + 1) = k + 1
      rw [Nat.add_succ,succk:Natih:0 + k = k⊢ (0 + k).succ = k + 1 ihsucck:Natih:0 + k = k⊢ k.succ = k + 1]All goals completed! 🐙

rw [ih] alone fails: 0 + k only appears after the ι step 0 + succ k ⟶ succ (0 + k), which Nat.add_succ performs.

How far reduction goes

δ fires freely for @[reducible], on demand for def, never for @[irreducible].
Reduction stops at weak head normal form: the outermost constructor or binder, no further.
On the terms that occur in practice this terminates, so rfl gives an answer.

In general definitional equality is undecidable: the checker is sound but incomplete.

Bool

Two constructors without arguments: true, false. Bool.rec : C → C → Bool → C is if-then-else, false case first.

example : (bif true then "Hi"
    else "Salut") = "Hi" := rfl

example (b : Bool) :
    (bif b then "Hi" else "Salut")
      = Bool.rec "Salut" "Hi" b := byb:Bool⊢ (bif b then "Hi" else "Salut") = Bool.rec "Salut" "Hi" b
  cases bfalse⊢ (bif false then "Hi" else "Salut") = Bool.rec "Salut" "Hi" falsetrue⊢ (bif true then "Hi" else "Salut") = Bool.rec "Salut" "Hi" true <;>false⊢ (bif false then "Hi" else "Salut") = Bool.rec "Salut" "Hi" falsetrue⊢ (bif true then "Hi" else "Salut") = Bool.rec "Salut" "Hi" true rflAll goals completed! 🐙

For a variable b, rfl alone is stuck, as for 0 + n.

Pattern matching

Instead of calling the recursor, write one line per constructor. Lean translates it back into Bool.rec.

def myNot : Bool → Bool
  | false => true
  | true  => false

`True`

Prop is no inductive type: it is a primitive of the kernel, Sort 0. True has one constructor, no argument.

example : True := True.intro
example : True := trivial
example : True := by⊢ True trivialAll goals completed! 🐙

trivial is a name for that constructor; the tactic of the same name tries it, plus rfl and assumption.

True.rec : C → True → C

One case, so nothing to learn from a proof of True.

`False`

No constructors, so no term can be built. The recursor has no case argument, so the result may be of any type: ex falso quodlibet.

False.rec  : (motive : False → Sort u) →
               (t : False) → motive t
False.elim : {C : Sort u} → False → C
False.elim h := False.rec (fun _ => C) h

False.elim is False.rec with a constant motive, which Lean reads off the goal:

example (h : False) : 0 = 1 :=
  False.rec (fun _ => 0 = 1) h
example (h : False) : 0 = 1 := False.elim h

No constructors, so no term — exactly what a proposition without a proof should look like.

Same thing or not? Same principle, two constants. False.rec is the recursor the kernel generates; False.elim is an ordinary definition on top of it (#print False.elim shows the line on the slide). Two differences, both about convenience:

The motive is explicit in False.rec and must be written out. False.elim takes a plain type C instead, implicitly, so Lean fills it in from the goal. Plain False.rec h is an error — Lean reads h as the motive.
The motive of False.rec may depend on the proof t. False.elim throws that away. For False it costs nothing, there is no proof to depend on.

Why the motive is explicit here and implicit for Bool.rec: there are no case values for Lean to infer it from. The chapter has it in a box.

In practice students write h.elim, exfalso, or cases h, never False.rec.

`False` and consistency

One proof of False proves every proposition.
A system with False inhabited is contradictory: it no longer tells the provable from the false.

False must stay empty.

Summary

Nat: two constructors and the recursor Nat.rec.
Six reduction rules α β η δ ι ζ generate definitional equality.
rfl checks it; a variable in recursive position gets stuck, then use induction or cases.
Bool, True, False: two, one and no constructors.