Foundations: what an inductive type gives you

Types have types

Every term has a type, and every type is itself a term with a type. The types of types are the universes Sort u:

Nat : Type

Type : Type 1

Prop : Type

Prop is Sort 0, Type is Sort 1, and Type u is Sort (u + 1). The hierarchy exists because Type : Type would be inconsistent (Girard's paradox), so each universe lives in the next one up. Definitions can be universe polymorphic: List takes a universe parameter, so List Nat and List Type are both fine.

List : Type u_1 → Type u_1

List Type : Type 1

Prop is the special case. A term p : Prop is a proposition, and a term h : p is a proof of it. Two facts about Prop matter for everything below:

• Impredicativity. A ∀ over any type still lands in Prop. The statement "for every type α, α → α is inhabited" quantifies over Type, but it is itself a Prop, not a Type 1.

• Proof irrelevance. Any two proofs of the same proposition are definitionally equal. The kernel never distinguishes them, so rfl proves it.

(α : Type) → α → α : Type 1

That output was a surprise worth recording. Lean prints the statement back as a dependent function type, (α : Type) → α → α, and puts it in Type 1, not Prop. The body α → α is a Type, so this is a type of polymorphic functions, not a proposition. Impredicativity applies only when the body is a proposition:

∀ (α : Type), α = α : Prop

The rule is that (x : A) → B lives in Sort (imax u v), where A : Sort u and B : Sort v. imax u 0 = 0, so a Prop body always gives a Prop. Otherwise imax u v = max u v.

What inductive adds

Here is a small inductive type, declared in its own namespace so it does not clash with the standard library:

That declaration adds much more than Tree, Tree.leaf and Tree.node. On Lean 4.32 it adds 24 constants. I listed them with a small metaprogram that filters the environment for names starting with Tree. Only four come from the kernel: the type, its two constructors and the recursor Tree.rec. Lean's front end derives the rest from the recursor:

• Tree.casesOn and Tree.recOn: case analysis without inductive hypotheses, and the recursor with the tree argument moved first.

• Tree.noConfusion, Tree.node.inj and Tree.node.injEq: constructors are distinct and injective. The kernel does not know this. It is proved from the recursor.

• Tree.below and Tree.brecOn: used to compile structural recursion (see the last section).

• Tree._sizeOf_1 and the sizeOf_spec lemmas: a size measure used by well-founded recursion.

• Tree.ctorIdx, Tree.ctorElim and the per-constructor elim functions, used by the code generator and by tactics.

The recursor is the important one. Its type is the induction principle:

@Demo.Tree.rec : {motive : Demo.Tree → Sort u_1} →
  motive Demo.Tree.leaf →
    ((a : Demo.Tree) → (a_1 : Nat) → (a_2 : Demo.Tree) → motive a → motive a_2 → motive (a.node a_1 a_2)) →
      (t : Demo.Tree) → motive t

Read it left to right:

• The motive says what we are computing or proving for each tree. Because it returns Sort u_1 for an arbitrary universe u_1, the same recursor builds both data (motive := fun _ => Nat) and proofs (motive := fun t => P t).

• There is one minor premise per constructor. The node case gets the constructor's arguments plus one inductive hypothesis for each recursive argument: motive a and motive a_2.

• The result is a function from every tree t to motive t.

The recursor also comes with computation rules, which the kernel uses when it reduces terms. Tree.rec l n Tree.leaf reduces to l, and Tree.rec l n (Tree.node a x b) reduces to n a x b (Tree.rec l n a) (Tree.rec l n b). That is all the kernel knows about Tree.

code generator does not support recursor `Demo.Tree.rec` yet, consider using 'match ... with' and/or structural recursion

Prop restricts the recursor

Inductive types can also live in Prop. Or is one:

@Or.rec : ∀ {a b : Prop} {motive : a ∨ b → Prop},
  (∀ (h : a), motive ⋯) → (∀ (h : b), motive ⋯) → ∀ (t : a ∨ b), motive t

(The ⋯ hides proof terms, here Or.inl h and Or.inr h. Lean elides proofs in output by default; set_option pp.proofs true shows them.)

Compare this to Tree.rec. The motive returns Prop, not Sort u_1. You can use a proof of a ∨ b to prove another proposition, but not to compute data. If you could, you could write a function that returns true for proofs made with Or.inl and false for proofs made with Or.inr. Proof irrelevance says any two proofs of True ∨ True are equal, so that function would have to return the same value on both, and Lean would be inconsistent.

Lean enforces this when you try:

Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Or.casesOn` can only eliminate into `Prop`

motive:True ∨ True → Sort ?u.3h_1:(h : True) → motive ⋯h_2:(h : True) → motive ⋯h✝:True ∨ True⊢ motive h✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

The important line is the second one. The pattern-match compiler tried to build the function from Or.casesOn, whose motive must return Prop, but Bool is a Type.

The exception is subsingleton elimination. An inductive proposition may eliminate into any Sort when it has at most one constructor and every argument of that constructor is either a proof or appears in the result type. And, True, False and Eq qualify. False.rec eliminating into any type is what makes absurd possible, and Eq.rec eliminating into any type is what lets you transport data along an equation:

@Eq.rec : {α : Sort u_2} →
  {a : α} → {motive : (a_1 : α) → a = a_1 → Sort u_1} → motive a ⋯ → {a_1 : α} → (t : a = a_1) → motive a_1 t

False.rec : (motive : False → Sort u_1) → (t : False) → motive t

Note the motive of Eq.rec. It depends on the right-hand side and on the proof of equality. Proofs about Eq that look trivial (Eq.symm, Eq.subst, congruence) are all applications of this one recursor.

How match becomes a recursor

Most functions are written with pattern matching and recursion:

The kernel has no match and no recursion, so the elaborator has to translate this into something like sumRec. It does that in two steps.

First, the pattern match is compiled into an auxiliary matcher function, Demo.Tree.sum.match_1, built from casesOn.

Second, the recursion has to be justified. Lean first tries structural recursion: every recursive call must be on a direct subterm of the argument. Here l and r are subterms of .node l x r, so it succeeds. #print shows the definition the kernel actually checked:

def Demo.Tree.sum : Demo.Tree → Nat :=
fun x => Demo.Tree.brecOn x Demo.Tree.sum._f

There is no recursion left. Tree.brecOn is a variant of the recursor that hands each case a table, Tree.below, holding the results for every smaller subtree. The body you wrote became the helper Demo.Tree.sum._f, and each recursive call l.sum became a lookup in that table. That is why inductive generated below and brecOn.

The compiler, by contrast, compiles your match and recursive calls directly, which is why #eval Demo.example1.sum works when #eval of sumRec did not:

6

Both definitions reduce in the kernel on concrete inputs:

The second line is worth pausing on. The two functions were written differently, one with match and one with Tree.rec directly, but on a concrete tree they reduce to the same numeral, so rfl proves them equal. To prove them equal for every tree, you need induction, which means using the recursor:

The show step works because both sides of the node case unfold, by the computation rules, to exactly the expression written there. induction chose the motive fun t => t.sum = t.sumRec and handed us the two minor premises, with ihl and ihr as the inductive hypotheses.

When structural recursion fails, for example when the recursive call is on n / 2, Lean falls back to well-founded recursion. That builds the function from WellFounded.fix and needs a termination proof. Such definitions do not reduce by rfl the way structural ones do. That is the subject of the Programming part of the series.

What I took away

• The kernel's view of an inductive type is small: the type, its constructors, one recursor and its computation rules. Everything else is derived.

• Universes stop Type : Type, and imax is the rule that makes a ∀ with a Prop body a Prop.

• A proof of an inductive proposition can only be used to prove other propositions, unless the type qualifies for subsingleton elimination.

• match and recursion are elaborator features. They compile to casesOn and brecOn, which are built from the recursor.

• The kernel and the compiler are separate. A recursor application type-checks and reduces, but it does not compile.

Sources

• Theorem Proving in Lean 4, chapters on inductive types and on induction and recursion.

• Lean language reference: the sections on universes and on inductive types, including the rules for subsingleton elimination.

• Mario Carneiro, The Type Theory of Lean (master's thesis, 2019), for the formal rules behind imax and the recursor.