Lean's Inductive Types

Inductive types in Lean allow for conservative extensions of the core theory (the calculus of inductive constructions) by adding new freely generated types. Here “conservative” is a term of art: it means that our additions do not “increase the power” of the underlying theory by adding new axioms; instead, they extend the language in a way designed to preserve consistency.

But how does this work internally? What exactly is added to the logical theory when we write inductive ...? This post answers that question using natural numbers as the running example. Suppose we declare a Nat type as follows:

namespace MyNat

  inductive Nat : Type
  | zero : Nat
  | succ : Nat → Nat

end MyNat

When we do this, Lean adds constructors, or “introduction rules”:

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

These let us construct (or ‘introduce’) Nat values. For example, the value for 1 is introduced as Nat.succ Nat.zero : Nat.

But we also need to deconstruct or (‘eliminate’) a Nat value. Lean adds a “recursor” Nat.rec for this, whose type can be printed using #check Nat.rec:

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

Spelling this out, we have:

1. A dependent function motive assigning to each Nat value n some type denoted motive n.
2. A base case - a value zero of type motive Nat.zero
3. An inductive case - a function succ mapping a value of type motive a to a value motive (Nat.succ a)

With these three arguments applied, we’re left with a function of type (t : Nat) → motive t. This is a dependent function type mapping each nat value to a result whose type depends on the value.

A motivating proof-shaped use is ∀ n, n = n. In Lean, proving this means constructing a term of that type. Nat.rec is exactly the induction/recursion principle that lets us build such terms by giving: 1. a value at zero, and 2. a way to extend a value at a to one at succ a.

Together, the constructors (introduction rules) and recursor (elimination rule) form the core logical/computational content of an inductive declaration. However, Lean also automatically derives a couple useful utilities.

Helpers: casesOn and noConfusion

In addition to rec, lean adds a special case: Nat.casesOn, which lets us do a ‘shallow match’ of cases, without recursing.

-- casesOn
#check Nat.casesOn
-- MyNat.Nat.casesOn.{u} {motive : Nat → Sort u} (t : Nat) (zero : motive Nat.zero) (succ : (a : Nat) → motive a.succ) :
  motive t

As a quick aside, note that if you try to add a case to Nat with the same name as one of these automatically added functions, you will get an error! E.g., adding

inductive Nat : Type
| zero : Nat
| casesOn : Nat -- will cause an error
| succ : Nat → Nat

… will cause an error like this:

error: (kernel) constant has already been declared 'MyNat.Nat.casesOn'

A more important helper is Nat.noConfusion. This is a theorem that says if t = t', then:

1. Matching constructors imply equal arguments
2. Different constructors are impossible

In table form:

Note that noConfusion is purely a helper: we could write it by hand, but it’s both tedious and mechanically derivable, so Lean gives it to us automatically. How does this work? Let’s examine Nat.noConfusion by #checking it first.

-- #check Nat.noConfusion
MyNat.Nat.noConfusion.{u} {P : Sort u} {t t' : Nat} (eq : t = t') : Nat.noConfusionType P t t'

This isn’t particularly helpful until we examine the definition of noConfusionType. Informally, it unpacks as the following case analysis:

More precisely, when we #print Nat.noConfusionType, we get this nested case analysis which first unpacks t, then t' within each branch. I’ve indented the #print for easier reading:

@[reducible] protected def MyNat.Nat.noConfusionType.{u} : Sort u → Nat → Nat → Sort u :=
    fun P t t' =>
        Nat.casesOn t
            (Nat.casesOn t'
                (P → P)
                fun a => P
            )
            (fun a => Nat.casesOn t'
                        P
                        (fun a_1 => (a = a_1 → P) → P)
            )

Finally, Lean also automatically adds an injectivity helper Nat.succ.inj as a useful special case proof that Succ(a) = Succ(a') ⇒ a = a'.