Building things from constructors

Technical version: Inductive types and recursors

Most of the things Lean reasons about (numbers, lists, trees, true and false) are made in one way: by naming a few rules for making values and declaring that nothing else counts. This page explains that idea, how Lean takes such values apart again, and the principle of recursion that Lean derives from the rules.

A type given by its rules

The natural numbers 0, 1, 2, 3, ... can be described by two rules. Zero is a natural number. If n is a natural number, so is the next one after n, its successor. Every natural number is reached from zero by applying the second rule some finite number of times, and nothing else is a natural number.

Lean's own definition says exactly this. Asked to print it,

#print Nat

Lean 4.34.1 answers:

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

A type defined this way is an inductive type. Its rules are its constructors: here Nat.zero, which needs nothing, and Nat.succ, which takes one natural number and makes the next. Three is Nat.succ (Nat.succ (Nat.succ Nat.zero)), and the numeral 3 names the same number. The values of an inductive type are exactly the ones its constructors make; it has no others.

This is not one device among many. Functions, universes and quotient types are built into Lean; every other type is an inductive type or is defined from functions, universes and inductive types.

Lists and trees

The same pattern makes a list. A list is either empty, or a first item followed by a list. Asked for #print List, Lean shows its own definition of lists in the same form:

inductive List.{u} : Type u → Type u
number of parameters: 1
constructors:
List.nil : {α : Type u} → List α
List.cons : {α : Type u} → α → List α → List α

The letter α stands for the type of the items, so the one definition gives lists of numbers, lists of words and lists of lists. The list [1, 2] is cons of 1 onto cons of 2 onto the empty list nil.

A tree with numbers at its branch points takes two rules of the same kind, and the size of a tree is a short definition on top of them:

inductive Tree where
  | leaf : Tree
  | node : Tree → Nat → Tree → Tree

def Tree.size : Tree → Nat
  | leaf       => 0
  | node l _ r => l.size + 1 + r.size

#eval (Tree.node (Tree.node Tree.leaf 5 Tree.leaf) 7 Tree.leaf).size

A leaf carries nothing. A node carries a left tree, a number and a right tree. Because a constructor may take values of the very type being defined, a few lines describe trees of every finite size. The #eval line asks for the size of a tree with two nodes, and Lean prints 2.

Taking values apart

To use a value of an inductive type, a definition asks which constructor made it and what was put into it. This is pattern matching. The definition of Tree.size above has one line per constructor: a leaf has size zero, and a node has the sizes of its two subtrees plus one for itself.

Lean checks that every constructor is covered. A definition that forgets one is refused:

def isZero : Nat → Bool
  | 0 => true

Lean answers Missing cases: and shows the shape left unhandled, (Nat.succ _): a number made by the successor rule, with anything at all inside. The check is possible because a natural number can only have come from one of the two rules. A definition that handles both handles every number.

The recursion principle

From the constructors alone, Lean derives one more thing: a recursion principle, also called the type's recursor. For the natural numbers, #check Nat.rec prints:

Nat.rec.{u} {motive : Nat → Sort u} (zero : motive Nat.zero) (succ : (n : Nat) → motive n → motive n.succ) (t : Nat) :
  motive t

In plain words: to produce something for every natural number t, supply what it is for zero, and a way to obtain it for the successor of n from n and from what it is for n. The word motive names the thing being produced, which may be different for each number. The recursor then delivers it for every number, because every number is zero followed by finitely many successors.

The recursion principle does two jobs, and the Lean Language Reference describes it in both roles. As computation, it defines functions: Lean translates the structurally recursive functions of [[Lean theorem prover/Explainers/Functions that always finish|functions that always finish]] into uses of it, and that is how the Lean kernel knows they end. As logic, where the thing produced for each number is a proof, it is proof by induction: prove a statement for zero, show that it passes from each number to the next, and it holds for all of them. Induction, as the machine sees it follows that second job.

Every inductive type has a recursor, with one case per constructor. The type Bool of true and false has two constructors that take nothing, and #check Bool.rec shows that its recursor asks for one answer for false and one for true. That is a choice between two cases and nothing more.

Structures: the one-constructor case

Often a value is several things kept together: a point is an x and a y. A structure is an inductive type with exactly one constructor, whose arguments are called its fields.

structure Point where
  x : Nat
  y : Nat

#eval (Point.mk 3 4).y
#print Point

The #eval line prints 4. The #print line lists the fields Point.x and Point.y and the single constructor Point.mk (x y : Nat) : Point. For structures, Lean adds conveniences: a function that reads each field, a way to write values by field name, and a way to extend one structure with another. These add no power. Everything a structure does could be done with a one-constructor inductive type, and the reference manual says so.

What the idea gives

Defining a type by its constructors fixes three things at once. How to make its values is the list of constructors. How to take them apart is pattern matching, which Lean checks for completeness. How to reason about all of them is the recursion principle, which Lean derives without being told, and which serves both to define functions and as the principle of induction.

Next

• Induction, as the machine sees it: the recursion principle used for proofs.
• Inductive types and recursors: the technical treatment.