Inductive Types II: The General Recipe

More constructors: trees

$\Nat$ has two constructors, and only one of them has a recursive argument. Consider a type with three:

inductive Tree where
  | leaf   : Tree
  | node   : Tree -> Tree
  | branch : Tree -> Tree -> Tree

For example, $\mathsf{branch}\;(\mathsf{node}\;\mathsf{leaf})\;\mathsf{leaf}$ is a tree built from four constructors. To build $M\;t$ for every tree $t$, where $M : \mathsf{Tree} \to \Sort{v}$, the recipe of Chapter 7 asks for one case per constructor, and each argument of type $\mathsf{Tree}$ contributes one induction hypothesis:

The recursor takes the motive, the three cases, and a tree:

where the dots stand for the types of $m_{\mathsf{node}}$ and $m_{\mathsf{branch}}$. Compared with $\NatRec{v}$, only the number of cases and the number of hypotheses per case have changed. Writing $R$ for the partial application $\mathsf{Tree.rec}_v\;M\;m_{\mathsf{leaf}}\;m_{\mathsf{node}}\;m_{\mathsf{branch}}$, the iota-rules are

Each rule selects the case for the constructor at the head of the major premise, and fills each hypothesis with a recursive call on the corresponding subtree. For example, with $M = \tLam{\_}{\mathsf{Tree}}{\Nat}$ and the cases

$R$ counts the constructors of a tree:

With $M$ a predicate ($v = 0$), the same recursor is structural induction on trees. In general, a type with $n$ constructors gets a recursor with $n$ minor premises $m_1, \ldots, m_n$, and the kernel needs no code specific to the type: it only needs to know, for each constructor, which case to pick and which arguments to recurse on.

Here is that tree as the kernel sees it. Each box is a constructor application; the recursive fields hang below it, and the line at the bottom of each box is the recursor case that handles it, with $(R\;l)$ and $(R\;r)$ the induction hypotheses computed by recursive calls. Type another tree to see its cases.

inductive Tree : Sort 1 where
  | leaf
  | node (t : Tree)
  | branch (l : Tree) (r : Tree)

inductive Tree : Sort 1 where
  | leaf
  | node (t : Tree)
  | branch (l : Tree) (r : Tree)

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 four : Nat := Nat.succ (Nat.succ (Nat.succ one))

# The minor premise for branch takes l, r, then the two induction hypotheses.
def count : Tree -> Nat := fun (t : Tree) => Tree.rec1 (fun (_t : Tree) => Nat) one (fun (t : Tree) => fun (i : Nat) => Nat.succ i) (fun (l : Tree) => fun (r : Tree) => fun (i : Nat) => fun (j : Nat) => Nat.succ (add i j)) t

goal Eq Nat (count (Tree.branch (Tree.node Tree.leaf) Tree.leaf)) four
rfl
qed

Parameters: lists

A list of numbers is either empty or a number in front of a list of numbers, so we could declare a type $\mathsf{ListNat}$ with constructors $\mathsf{nil}$ and $\mathsf{cons} : \Nat \to \mathsf{ListNat} \to \mathsf{ListNat}$. But then lists of trees would need another declaration, $\mathsf{ListTree}$, with the same constructors and a separate recursor, and so on for every element type. It is better to make the element type an argument of the type itself:

inductive List (A : Sort 1) where
  | nil  : List A
  | cons : A -> List A -> List A

Now $\mathsf{List}\;\Nat$ and $\mathsf{List}\;\mathsf{Tree}$ are two instances of one declaration. The declaration adds

The constructors take $A$ as an explicit first argument. For example, the one-element list $[5]$ is $\mathsf{cons}\;\Nat\;5\;(\mathsf{nil}\;\Nat)$. Within one list, $A$ never changes: the tail of $\mathsf{cons}\;A\;a\;\mathit{as}$ is again a $\mathsf{List}\;A$. An argument of the type that stays the same in every constructor and every recursive argument is called a parameter. Because it never changes, the recursor can take it once, before the motive, and treat it as fixed:

Apart from the leading $A$, this is the recipe of Chapter 7 once more: $\mathsf{cons}$ has two arguments, of which only $\mathit{as}$ is recursive, so its case gets one induction hypothesis. The rules ignore the parameter $A'$ stored in the constructor; in a well-typed term it is convertible to $A$. For example, the length of a list is

A list value carries the parameter $A$ in every constructor, which the tree below shows next to each box: the parameter is repeated, the fields differ.

inductive List (A : Sort 1) : Sort 1 where
  | nil
  | cons (head : A) (tail : List A)

inductive List (A : Sort 1) : Sort 1 where
  | nil
  | cons (head : A) (tail : List A)

def length : forall (A : Sort 1), List A -> Nat := fun (A : Sort 1) => fun (xs : List A) => List.rec1 A (fun (_xs : List A) => Nat) Nat.zero (fun (head : A) => fun (tail : List A) => fun (r : Nat) => Nat.succ r) xs

# length [0, 0] = 2
goal Eq Nat (length Nat (List.cons Nat Nat.zero (List.cons Nat Nat.zero (List.nil Nat)))) (Nat.succ (Nat.succ Nat.zero))
rfl
qed

Indices: vectors

A $\mathsf{List}\;\Nat$ may have any length. What if we want the length to be part of the type, so that $\mathsf{Vec}\;\Nat\;0$ and $\mathsf{Vec}\;\Nat\;2$ are different types?

inductive Vec (A : Sort 1) : Nat -> Sort 1 where
  | vnil  : Vec A 0
  | vcons : (n : Nat) -> A -> Vec A n -> Vec A (succ n)

The element type $A$ is still a parameter. The length is not: $\mathsf{vnil}$ has length $0$, and $\mathsf{vcons}$ takes a vector of length $n$ and returns one of length $\suc\;n$. An argument of the type that may differ between constructors, and between a constructor and its recursive arguments, is called an index. The constructors are

Because an index varies, the recursor cannot fix it in advance. Instead, the motive takes it as an argument, $M : \tPi{n}{\Nat}{\mathsf{Vec}\;A\;n \to \Sort{v}}$, and the case for $\mathsf{vcons}$ is

The induction hypothesis is about a vector of length $n$, read off the type $\mathsf{Vec}\;A\;n$ of the recursive argument, and the conclusion is about one of length $\suc\;n$, read off the result type of the constructor. The script examples/generic-vec.leanmini (Appendix E) declares this type and checks a small term that uses it.

The general recipe

This section states the procedure for a single inductive type with parameters and indices. Mutual and nested inductive types, which Lean also supports, are out of scope.

The procedure also answers a question that T-Const leaves open. A constant without a body is an assumption: T-Const would accept $c : \tPi{P}{\Sort{0}}{P}$ just as readily as $\zero : \Nat$, and with it the system would be inconsistent. The constants generated below are not arbitrary assumptions. They are instances of a fixed schema, the inductive types of the Calculus of Inductive Constructions, whose consistency is known [Werner 1994].

Telescopes. We write $(\vec{x} : \vec{A})$ for a sequence of bindings $(x_1 : A_1) \cdots (x_k : A_k)$ in which each $A_i$ may mention $x_1, \ldots, x_{i-1}$; $\tPi{\vec{x}}{\vec{A}}{B}$ for $\tPi{x_1}{A_1}{\cdots\,\tPi{x_k}{A_k}{B}}$; and $f\;\vec{x}$ for $f\;x_1 \cdots x_k$. The length of $\vec{x}$ is $|\vec{x}|$. In the code, a telescope is a Context, and telescope(binders, tail) in src/term.rs builds the nested $\Pi$.

Declarations. A declaration introduces a type former $I$ and constructors $c_1, \ldots, c_n$:

The parameters $\vec{p}$ are shared by all constructors and appear unchanged in every result type. The indices $\vec{\imath}$ may differ between constructors: the index terms $\vec{t}_j$ may mention $\vec{p}$ and the constructor's own arguments $\vec{a}$, which are called its fields. For the examples so far, with the leading $\Pi$ over the parameters omitted from the constructor types:

Acceptance. The kernel accepts a declaration only if the following four conditions hold.

1. The type of $I$ is a type in the current signature.
2. With $I$ added to the signature, each constructor type is a type, and it ends in $I\;\vec{p}\;\vec{t}_j$, where $\vec{p}$ are exactly the parameters in order and $I$ does not occur in $\vec{t}_j$.
3. Strict positivity. Each field type either does not mention $I$, or has the form $\tPi{\vec{y}}{\vec{B}}{I\;\vec{p}\;\vec{s}}$ where $I$ occurs neither in $\vec{B}$ nor in $\vec{s}$. A field of the second form is recursive.
4. Universes. If $u \ge 1$, each field type lies in some $\Sort{w}$ with $w \le u$. If $u = 0$, there is no condition.

Condition 2 lets the recursor treat the parameters uniformly. Condition 3 rules out declarations such as

inductive Bad where
  | mk : (Bad -> False) -> Bad

whose field mentions Bad to the left of an arrow. Case analysis on Bad would let one define $f : \mathsf{Bad} \to \mathsf{False}$ by $f\;(\mathsf{mk}\;g) = g\;(\mathsf{mk}\;g)$. Then $f\;(\mathsf{mk}\;f)$ is a closed term of type $\mathsf{False}$, and it reduces to itself, so it has no normal form. For a type $\mathsf{Tree}$ under declaration, some field types and their status are:

A field of type $\Nat \to \mathsf{Tree}$ is a tree with infinitely many children, one for each number; the recursor can still recurse into each child $a_k\;n$. A field of type $\mathsf{Tree} \to \Nat$ consumes trees instead of containing them, and it is the shape that makes Bad paradoxical.

Condition 4 prevents a type from containing a larger universe. Without it, a declaration $T : \Sort{1}$ with a constructor $\mathsf{mk} : \Sort{1} \to T$ would place a copy of all of $\Sort{1}$ inside $\Sort{1}$, which is the self-containment that Chapter 13 shows to be inconsistent. For $u = 0$ no condition is needed, because $\Sort{0}$ is impredicative.

The recursor. For an accepted declaration, the kernel generates a recursor $I.\mathsf{rec}_v$ for each admissible level $v$ (see below):

The parameters come first and stay fixed, as for lists; the motive takes the indices and the element, as for vectors. The minor premise $C_j$ asks for the case of constructor $c_j$: given its fields and an induction hypothesis for each recursive field, build $M$ for $c_j$ applied to those fields:

The final arguments are the indices and the element $x$ itself, the major premise.

The rules. For each constructor, the kernel generates one iota-rule, which applies the minor premise to the fields and to the induction hypotheses, computed by recursive calls:

The major premise is at position $|\vec{p}| + 1 + n + |\vec{\imath}|$ (counting from zero), the constructor has $|\vec{p}|$ parameters and $|\vec{a}|$ fields, and in a well-typed redex $\vec{p}\,'$ is convertible to $\vec{p}$, so the rule ignores it, as the rules for lists ignore $A'$. For $\Nat$, $\mathsf{Tree}$, $\mathsf{List}$, and $\mathsf{Vec}$ the procedure produces exactly the recursors and rules of this chapter and the last, and the recursor types agree with the ones Lean 4 generates, up to the names of bound variables and implicit arguments.

Eliminating from propositions. If $u \ge 1$, the recursor is generated for every level $v$. If $u = 0$, so that $I$ is a proposition, the recursor is generated only for $v = 0$, unless $I$ is a subsingleton: it has at most one constructor, and each field either is a proof (its type lies in $\Sort{0}$) or occurs among the index terms $\vec{t}_j$. The restriction keeps data from depending on which proof of a proposition was given. For example, $P \vee Q$ has two constructors, so a function from proofs of $P \vee Q$ into $\Nat$ could return $0$ for one and $1$ for the other, and a proof would carry computational information. Lean's Or.rec and Exists.rec therefore eliminate only into Prop, while And.rec and Eq.rec eliminate into every universe: And has one constructor whose fields are proofs, and Eq (Chapter 9) has one constructor with no fields.

So the kernel's rules stay fixed while the signature grows: one generic procedure turns each declaration into signature entries, and a single reduction function runs their rules (Chapter 12).

In the code

The heart of the generator is short enough to read in full. Compare it with the formula for $C_j$.

/// C_j = Pi (as : As_j). Pi (hs : Hs_j). M ts_j (c_j ps as)
fn minor_premise_type(info: &InductiveInfo, j: usize, constructor: &ConstructorInfo) -> Term {
    // c_j ps as
    let constructor_application = apps(
        const_term(&constructor.name),
        info.params.iter().chain(constructor.fields.iter()).map(|(name, _)| var(name)),
    );
    // (as : As_j) followed by (hs : Hs_j)
    let mut minor_premise_binders = constructor.fields.clone();
    for (k, recursive_field) in constructor.recursive_fields.iter().enumerate() {
        minor_premise_binders.push((
            format!("{INDUCTION_HYPOTHESIS_PREFIX}{j}_{k}"),
            induction_hypothesis_type(constructor, recursive_field),
        ));
    }
    telescope(&minor_premise_binders, apply_motive(&constructor.result_indices, constructor_application))
}

The kernel never special-cases $\Nat$. Kernel::standard in src/kernel.rs declares $\Nat$ and $\mathsf{Eq}$ by calling add_inductive with the same InductiveSpec a user script would produce, so Figure 7.1 is generated, not hard-coded, and the tests in src/inductive/tests.rs check that the generated types agree with the hand-written ones.

Exercises