Inductive Types I: Natural Numbers

Constants and definitions

First we need a way to add named objects to the kernel. Terms gain constants $c$:

A signature $\Sigma$ lists the constants. Each entry either declares a constant with its type, written $c : C$, or also gives it a body, written $c : C \mathrel{:=} t$. Entries with a body are definitions. For example, $\Nat : \Sort{1}$ below is a declaration, and $\add$ later in this chapter is a definition. Before an entry is added, its type is checked to be a type in the empty context, and its body, if any, is checked against that type, as Lean does for each def.

The signature is used in two ways. First, a constant has the type the signature gives it:

where $(c : C) \in \Sigma$ covers both declarations and definitions. Second, a definition can be unfolded: the constant is replaced by its body. This computation step is called delta-reduction:

For example, $\add\;2\;1 \deltared (\tLam{m}{\Nat}{\tLam{n}{\Nat}{\cdots}})\;2\;1$, after which beta-reduction continues. A declared constant without a body, such as $\Nat$ or $\zero$, never delta-reduces. Like beta, the step may be applied to any subterm.

Constants are not variables: they are never bound, so $\FV(c) = \emptyset$ and substitution leaves them unchanged. Reduction now consists of beta, delta, and the iota-rules introduced below, and definitional equality (Chapter 12) is taken with respect to all three.

Natural numbers

In Lean, the natural numbers are declared as

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

The declaration says that every natural number is built in one of two ways: it is $\zero$, or it is $\suc\;n$, the successor of a natural number $n$. For example, $2$ is $\suc\;(\suc\;\zero)$. In our kernel the declaration adds three constants without bodies:

$\zero$ and $\suc$ are called constructors. They build values but never compute: $\suc\;(\suc\;\zero)$ is already in normal form, and it is the number $2$. We write $0, 1, 2, \ldots$ for $\zero$, $\suc\;\zero$, $\suc\;(\suc\;\zero)$, and so on.

We now have numbers, but no way to compute with them: addition must distinguish $\zero$ from $\suc\;n$, while our terms can only pass an argument along, not inspect it.

Computing: addition

How should addition be defined? By recursion on the second argument:

Look at the shape of this definition. For a fixed $m$, the function $\add\;m$ is determined by two pieces of data: its value on $\zero$, which is $m$, and a way to turn its value $r$ on $k$ into its value on $\suc\;k$, which is $\suc\;r$. Every function $f : \Nat \to C$ defined by recursion of this kind, called structural recursion, has the same shape:

for some $z : C$ and $s : \Nat \to C \to C$. The step function $s$ receives both $k$ and the result $f\;k$ of the recursive call. So we add one constant that builds $f$ from $z$ and $s$, once and for all:

together with two computation rules, called iota-rules, which are the equations above:

Addition is now an ordinary, non-recursive definition:

We write $m + n$ for $\add\;m\;n$. The kernel computes $2 + 1$ with delta, beta, and iota steps only. The explorer below is the kernel doing that, one head step at a time, with the $\add$ definition loaded.

def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n

Each row is one head step: the highlighted part is the redex, and the next row shows what it became. Change the numerals, or try add Nat.zero n with the context n : Nat to see the recursor get stuck.

Other functions follow the same pattern. Doubling, with $\mathit{double}\;(\suc\;k) = \suc\;(\suc\;(\mathit{double}\;k))$, is

and $\mathit{double}\;2 \to \suc\;(\suc\;(\mathit{double}\;1)) \to \suc^4\;(\mathit{double}\;0) \to \suc^4\;\zero = 4$.

No new recursion mechanism is needed. The constants of the inductive type, together with $\mathsf{rec}_C$ and its two rules, are enough to express every structurally recursive function on $\Nat$. And unlike general recursion, this one always terminates: each iota-step removes one $\suc$ from the argument.

Proving: induction

Now consider proofs. To prove that a property $P\;n$ holds for every $n$, where $P : \Nat \to \Sort{0}$, mathematics uses induction: prove the base case $P\;\zero$, and the step $\tPi{k}{\Nat}{P\;k \to P\;(\suc\;k)}$, whose argument $P\;k$ is the induction hypothesis.

Through Curry-Howard, a proof of $\tPi{n}{\Nat}{P\;n}$ is a function $f$ that takes $n$ and returns a proof of $P\;n$. How do we build such an $f$ from $\mathit{base} : P\;\zero$ and $\mathit{step}$? For $3$, the proof is $\mathit{step}\;2\;(\mathit{step}\;1\;(\mathit{step}\;0\;\mathit{base}))$, and in general

This is a structurally recursive function again, with exactly the shape of $\add$ above: $z = \mathit{base}$ and $s = \mathit{step}$. Induction is recursion that returns proofs.

There is one difference: $\add$ has the same result type $C$ for every $n$, whereas a proof has a type that depends on $n$, such as $f\;\zero : P\;\zero$ and $f\;1 : P\;1$. Because the type of $\mathsf{rec}_C$ mentions a fixed $C$, it cannot express induction as it stands.

One recursor for both

Putting the two cases side by side shows what to generalize.

The left column is the special case of the right column in which $P\;n$ is the same type $C$ for every $n$. So we take the right column, with $P$ replaced by an arbitrary function $M : \Nat \to \Sort{u}$ that gives the type of the result for each $n$. This function is called the motive. The result is the recursor $\NatRec{u}$ of Figure 7.1. Its arguments are the motive, one minor premise for each constructor, and finally the number $n$ to recurse on, called the major premise. Its iota-rules are those of $\mathsf{rec}_C$. As in Lean, where the recursor is Nat.rec.{u}, there is one recursor for each universe level; since we have no universe polymorphism, the level is a subscript.

The one recursor does both jobs, depending on the motive.

Recursion. With the constant motive $\tLam{\_}{\Nat}{C}$ at level $1$, the type of $\NatRec{1}\;(\tLam{\_}{\Nat}{C})$ is convertible to the type of $\mathsf{rec}_C$. So $\mathsf{rec}_C$ is just $\NatRec{1}\;(\tLam{\_}{\Nat}{C})$, and from now on

which is the definition in examples/zero-add.leanmini.

Induction. With a predicate $M : \Nat \to \Sort{0}$ at level $0$, the type of $\NatRec{0}$ is the induction principle

Here the choice of $\imax$ in T-Pi is essential. The conclusion $\tPi{n}{\Nat}{M\;n}$ has type $\Sort{\imax(1, 0)} = \Sort{0}$, so "$M\;n$ for every $n$" is a proposition although $\Nat$ lives in $\Sort{1}$. With $\max$ instead, it would live in $\Sort{1}$, and statements about numbers would not be propositions at all.

The type of $\NatRec{u}$ is not arbitrary: it can be read off the declaration of $\Nat$. There is one minor premise per constructor. Each minor premise takes the constructor's arguments, plus one induction hypothesis for each argument whose type is $\Nat$ itself (a recursive argument), and returns the motive applied to the constructor. $\zero$ has no arguments, so its case is just $M\;\zero$; $\suc$ has one recursive argument $n$, so its case is $\tPi{n}{\Nat}{M\;n \to M\;(\suc\;n)}$. Chapter 8 applies this recipe to more and more general declarations.

Try it

The kernel starts with $\Nat$ and its recursors already declared (Kernel::standard in src/kernel.rs). The script below defines addition and asks the kernel to confirm that $2 + 1$ and $3$ are definitionally equal, which rfl does by computing both sides. Try changing three to Nat.succ three and see the kernel refuse.

def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n
def one : Nat := Nat.succ Nat.zero
def two : Nat := Nat.succ one
def three : Nat := Nat.succ two
# Both sides compute to succ (succ (succ zero)), so refl proves this.
goal Eq Nat (add two one) three
rfl
qed

The Eq in the goal is the equality type, declared in Chapter 9. For now, read Eq Nat a b as "$a = b$" and rfl as "both sides compute to the same thing".

Exercises

def mul : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) Nat.zero (fun (k : Nat) => fun (r : Nat) => add m r) n