Inductive types and proof by induction

Proofs by induction are ubiquitous throughout mathematics, providing an axiomatic tool for proving universal statements about recursively defined mathematical objects through two steps: proving base cases and showing preservation under construction from substructures. Of course, Lean provides ample machinery to write inductive proofs. Let’s take a look!

A basic example: Peano’s axiom of induction

Let us consider a basic inductive proof of the form most probably encounter first in their mathematics education: In order to prove that a statement (we call it motive in Lean proofs) motive : (n : Nat) → Prop about a natural number holds for all natural numbers n, it suffices to prove that it holds for n = 0, and that given a proof that it holds for some n : Nat we can derive that it also holds for n + 1, according to Peano’s axiom of induction. The induction tactic makes it straightforward to write such a proof in Lean, as done in this example taken from mathlib about the binomial coefficient:

example (n : Nat) : choose n 2 = n * (n - 1) / 2 := by induction' n with n ih · simp · rw [Nat.triangle_succ n] rw [Nat.choose, ih] simp [Nat.add_comm]

We actually used the induction' variant of the tactic that allowed us to assign the names n and ih to the induction variable and hypothesis. If we look at the goals the tactic produced here, we see that we are required to provide proofs for the base case 0 and the induction step:

2 goals case zero ⊢ Nat.choose 0 2 = 0 * (0 - 1) / 2 case succ n : Nat ih : n.choose 2 = n * (n - 1) / 2 ⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2

Inductive Types and Recursors

That was smooth enough! However, many proofs by induction we encounter don’t follow the exact structure given by Peano’s axiom, or are not even about natural numbers. To formalise such proofs in Lean, we take a more abstract, structural view of induction, as a general method for proving statements of the form \(∀ a \in A, P(a)\), where \(A\) is some domain and \(P(a)\) is some proposition about elements of \(A\).

What do we require of \(A\) so we can make inductive proofs about its members? Each element \(a \in A\) needs to be representable as either an instance of some base cases, or constructed from other elements of \(A\) that are “smaller” than \(a\), meaning that they are closer than \(a\) to some base case according to a (partial) ordering on \(A\). In type theory, the domains of universal quantifications are types, and we say a type \(A\) is an inductive type if each of its members is generated from finite compositions of a finite number of constructors.¹

In Lean, they are defined by using the keyword inductive. Inductive types are so expressive that apart from type universes and dependent function types, all Lean types are inductive types, even though that fact is hiding underneath a thick layer of syntactic sugar. We’ve already encountered a prominent example of an inductive type with Nat, which is defined through one constant constructor zero and one recursive constructor succ:

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

We see that by definition, all natural numbers in Lean are either 0 or n + 1 for some natural number n, which means it suffices to prove a statement for those two cases to prove it for all of Nat. When we define any inductive type in Lean, this principle (called the recursor or eliminator of the type) is automatically derived from the definition and accessible in the .rec field. Looking at what it came up with for our definition of Nat through #print Nat.rec, we get something that looks suspiciously like Peano’s axiom:

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

Different Induction Principles

The induction tactic is just a shortcut that allows us to choose the current goal as motive, creating goals for the constructor arguments, and handling variable naming. By default, it uses the recursor of the induction variable’s type as an induction principle specifying the shape of the generated proof though we can influence that choice through the using keyword. We can easily verify that the previous example remains valid when we explicitly demand Nat.rec to be used through induction' n using Nat.rec with n ih.

Mathlib provides a collection of alternative induction principles on Nat for frequently occuring proof techniques:

Induction Principle	Description
twoStepInduction	Uses hypotheses for n and n - 1 to prove for n + 1
strong_induction_on	Proves for n + 1 using all m < n + 1
le_induction	Proves for numbers above a bound
decreasingInduction	Proves for numbers below a bound
diag_induction	Proves using diagonal arguments with two parameters

We can in fact easily reformulate the proof of our previous example using strong_induction_on. Note that it requires us to manually separate out the base case:

example (n : Nat) : choose n 2 = n * (n - 1) / 2 := by induction' n using Nat.strong_induction_on with k ik by_cases h : k = 0 · simp [h] · obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h rw [Nat.triangle_succ n] rw [Nat.choose, ik n (Nat.lt_succ_self n)] simp [Nat.add_comm]

Let us also consider a slightly more complex example using le_induction. Looking at the signature of this induction principle through #print le_induction, we see that the form of the motive we can prove with this principle is P : (n : Nat) → m ≤ n → Prop, and that we need to prove the statement for the lower bound m (P m ⋯ in the signature), as well as for the induction step P n hmn → P (n + 1) ⋯) for all n within the bound:

>> theorem Nat.le_induction : ∀ {m : Nat} {P : (n : Nat) → m ≤ n → Prop}, P m ⋯ → (∀ (n : Nat) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) → ∀ (n : Nat) (hmn : m ≤ n), P n hmn ...

The following easy example from mathlib, establishing that

\[\sum_{m = k}^{n} {m \choose k} = {n + 1 \choose k + 1},\]

demonstrates how to use le_induction, with the induction' tactic now invoked using two induction parameters as required by the motive P in the le_induction principle.

example (n k : Nat) (h : n ≥ k) : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1) := by induction' n, h using le_induction with n _ ih · simp · rw [← Ico_insert_right (by omega), sum_insert (by simp), show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)]

Writing Your Own Principles

Now what happens if we want to prove a universal statement about a motive that’s more intricate than the simple unary predicate that we get from the recursor? We likely could, in theory, reduce it to nested induction using only type recursors on some obtuse inductive type, but there is a much nicer way.

As we have seen, the recursor of an inductive type \(A\) is a function from a proposition over a variable (the motive, itself a function mapping from \(A\) to Prop), and one argument for each constructor, to a proof of the motive under universal quantification over \(A\). The induction tactic can in fact use any function in place of the recursor, as long as it

• binds a variable for motive : (t₀ : T₀) → ... → (tₙ : Tₙ) → Sort*,
• binds variables (t₀ : T₀), …, (tₙ : Tₙ), and
• has motive t₀ ... tₙ as the result type.

The function can also bind other variables and the induction tactic will create a separate goal for each of them. It expects as input one bound variable for each t_i, and will result in a proof universally quantified over all those variables.

While this is such a general tactic I hesitate to call the resulting proofs “by induction” for all input principles, we can use it to generate proofs using nonstandard induction (not even necessarily over an inductively defined type!) by specifying an induction principle where the cases correspond to proofs about base cases and inductive steps.

We can look at an example from mathlib again: the two-step induction principle on the naturals, deriving the next case from the two previous ones.

def twoStepInduction {P : ℕ → Sort*} (zero : P 0) (one : P 1) (more : ∀ n, P n → P (n + 1) → P (n + 2)) : ∀ a, P a | 0 => zero | 1 => one | _ + 2 => more _ (twoStepInduction zero one more _) (twoStepInduction zero one more _)

We observe the motive, here called P, the bound variable a and the result type P a. The remaining bound variables, zero, one, and more, will each get a seperate case when we use this with the induction tactic, requiring us to prove P 0, P 1 and ∀ n, P n → P (n + 1) → P (n + 2) respectively. All that was needed to write this induction principle was proving that given those three things, we can infer ∀ a, P a.

1. Constructors are functions whose codomain is \(A\). They need to adhere to certain restrictions to maintain consistency. ↩