09 Jun 2025

[ inductive definitions ] The previous post discussed the simplest sort of definitions, those that are essentially abbreviations. An inductive definition is conceptionally quite different. The simplest example is to say that a natural number can be either 0 or the successor of another natural number, and that there are no other natural numbers. This last minimality property is the basis for mathematical induction, for it implies that if some property holds for 0 and is preserved as we move from a natural number to its successor, then all natural numbers have been accounted for. Inductive definitions are a natural way to specify recursive datatypes such as lists and trees, programming language semantics, inference systems and much else. Proof by induction corresponds (respectively) to structural induction, induction on program executions, induction over derivations. Proofs involving inductive definitions are often easy, with automation taking care of most of the work.

A tiny example

The very simplest example of an inductive definition would be the natural numbers themselves, but most proof assistants treat recursive datatypes as a separate, highly specialised case. Instead, let’s look at the Isabelle equivalent of the Prolog program to append two lists:

append([],X,X).
append([X|Y],Z,[X|W]) :- append(Y,Z,W).

In case you don’t know Prolog, this defines a ternary relation, append. The first two arguments are the lists to be joined and the third argument is the result. In Prolog, you do not define functions but rather relations that specify how the output is derived from the inputs.1 The first clause is for joining an empty list, while the second joins a list with head X and tail Y to some other list, Z.

This Prolog code is easily expressed in Isabelle. For this example, let’s conform to the Prolog convention that variables begin with capital letters. Isabelle is even capable of reasoning using a proof strategy related to Prolog’s. Note, however, that the Isabelle definition itself is simply mathematics and does not model Prolog’s depth-first execution model (not to mention its broken treatment of unification).

inductive Append :: "['a list, 'a list, 'a list] ⇒ bool" where
Append_Nil:  "Append [] X X"
| Append_Cons: "Append Y Z W ⟹ Append (X#Y) Z (X#W)"

Let’s prove that Append, although written as a relation, is actually functional (single-valued). Note that the induction appeals to the specific induction rule for Append, namely Append.induct.

lemma Append_function: "⟦Append X Y Z; Append X Y Z'⟧ ⟹ Z' = Z"
proof (induction arbitrary: Z' rule: Append.induct)
show "⋀Y Z'. Append [] Y Z' ⟹ Z' = Y"
using Append.cases by blast
show "⋀X Y W A Z'. ⟦⋀Z'. Append X Y Z' ⟹ Z'=W; Append (A#X) Y Z'⟧
⟹ Z' = A#W"
by (metis Append.cases list.inject neq_Nil_conv)
qed

Here I deliberately avoid Isar’s concise syntax for induction to highlight the two cases that must be proved. In the base case, we need to show that Append behaves like a function when its first argument is []; in the induction step, the first argument is X and we can assume the induction hypothesis that Append behaves like a function when its first argument is X (where X is fixed and local to this case).

Both proofs appeal to case analysis on the definition, namely Append.cases. This is a common feature of proofs involving inductive definitions, and invites the use of a technique called rule inversion: creating new simplification rules to handle special cases of the inductively defined predicate. For example, if the first argument is the empty list then the second and third arguments must be equal. And if the first argument is a list with head X, then the third argument will also have head X and a tail obtained through Append.

inductive_simps Append_Nil_simp [simp]: "Append [] X Y"
inductive_simps Append_Cons_simp [simp]: "Append (X#Y) Z V"

Isabelle automatically generates these and similar facts by instantiating and then simplifying the relevant case analysis rule: you merely need to specify the special case you are interested in, which will become the left-hand side of the new rewrite rule. If you set up rule inversion skilfully and integrate it with simplification, the combination can be extremely powerful. The proof above becomes only slightly simpler (the metis call needs just one argument, Append_Cons_simp), but the following similar theorem now gets a one-line proof:

lemma Append_function2: "⟦Append X Y Z; Append X Y' Z⟧ ⟹ Y' = Y"
by (induction rule: Append.induct) auto

The lemma below expresses that append is associative. It again has a one line proof, thanks to our special simplification rules. (Otherwise, the proof is a mess.)

lemma Append_assoc: "⟦Append T U V; Append V W X; Append U W Y⟧ ⟹ Append T Y X"
by (induction arbitrary: X rule: Append.induct) (auto simp: Append_function)

Naturally, the append function @ is already provided by Isabelle’s list library, and it’s time to prove that the Append relation coincides with this function. In other words, the Prolog program really computes list append.

We prove this in two directions. First, the third argument of Append can only be the list computed by @. As before, I’ve written out the base case and induction step explicitly.

lemma Append_imp_append: "Append X Y Z ⟹ Z = X@Y"
proof (induction rule: Append.induct)
show "⋀Y. Y = [] @ Y"
by simp
show "⋀X Y Z A. Z = X@Y ⟹ A # Z = (A # X) @ Y"
by simp
qed

It’s vital to note that the property above would also be satisfied if Append X Y Z was always false. To complete the equivalence proof, it’s essential to show that Append is true given suitable arguments. This proof is by list induction. The induction rule Append.induct is not applicable because it requires some instance of Append X Y Z as a fact or assumption.

lemma Append_append: "Append X Y (X@Y)"
proof (induction X)
show "Append [] Y ([] @ Y)"
by (auto simp: Append.intros)
show "⋀A X. Append X Y (X @ Y) ⟹ Append (A # X) Y ((A # X) @ Y)"
by (auto simp: Append.intros)
qed

I’ve again written out the inductions in great detail to reveal what has to be proved. In fact, these theorems have one-line proofs.

lemma "Append X Y Z ⟹ Z = X@Y"
by (induction rule: Append.induct) auto

lemma "Append X Y (X@Y)"
by (induction X) (auto simp: Append.intros)

The equivalence between Append and list append is now trivial:

lemma Append_iff_append: "Append X Y Z ⟷ Z = X@Y"
using Append_append Append_imp_append by blast

And with this fact available, it’s now trivial to prove things that might be quite tricky otherwise, such as this one:

lemma Append_function1: "⟦Append X Y Z; Append X' Y Z⟧ ⟹ X' = X"
by (simp add: Append_iff_append)

And here’s a secret: most of the theorems proved at the stop of this example become trivial using Append_iff_append. Most inductive definitions don’t correspond to functions (what would be the point?), but it’s often possible to prove general theorems relating the arguments, from which more specific properties follow without further use of induction.

What an inductive definition means mathematically

The inductive definition of a logical calculus may contain introduction rules such as these:

• if $A\to B$ and $A$ are theorems then so is $B$

• if $\neg\neg A$ is a theorem then so is $A$

• $x=x$ is a theorem Note that the preconditions, if any, of an introduction rule may refer to the relation being defined, but only positively. We cannot have a rule containing a negative reference, such as this:

• if $A$ is not a theorem then $\neg A$ is a theorem The problem with that is how to establish a negative precondition in the first place. Mathematically speaking, an inductive definition has to be monotone. There is always a construction of finite depth establishing any particular instance of the inductively defined relation. (Even if the precondition involves a universal quantifier, it will still be well behaved!) Precoditions not referring to the relation being defined can be anything, and can even refer negatively to an inductive relation to defined earlier.

In mathematics (and in Isabelle), an inductive definition carves out a distinguished subset of something we have already. An inference system distinguishes a given set of formulas as theorems; the full set of formulas was already available. The semantics of a programming language is defined on configurations involving a fragment of program syntax combined with information about the program state, distinguishing those state transitions allowed by the language; the syntax and state space had been defined previously.

Even when we define the set of natural numbers in terms of zero and successor, we need to have defined zero and successors already. In set theory, zero is the empty set and the successor of $n$ is $n \cup {n}$; The axiom of infinity guarantees the existence of a set closed under these, and the minimality property can be obtained by a least fixed-point construction, ultimately a set intersection. The situation is similar in higher-order logic. However, dependent-typed theories — such as used in Lean — need the concept of inductive definition to be primitive to the formalism itself.

Documentation is available in Section 3.5 of Programming and Proving. For those of you interested in the full abstract theory of inductive definitions, Peter Aczel’s chapter (also here) in the Handbook of Mathematical Logic is the ultimate account.

And there are plenty of examples right here on this blog.

In fact, Prolog does not force us to distinguish inputs from outputs. But that’s another story. ↩