class InductiveTypeConstructor:
def __init__(self, name: str, type_: Term):
self.name = name
self.type_ = type_
def __repr__(self):
return f"Constructor({self.name}: {self.type_})"
class InductiveType:
def __init__(self, name: str, params: List[Variable], indices: List[Variable],
returnType: Term, constructors: List[InductiveTypeConstructor]):
self.name = name
self.params = params
self.indices = indices
self.returnType = returnType
self.constructors = constructors
def __repr__(self):
return f"Inductive {self.name}"
Introduction
To introduce more complex notions into our type system, we need induction.
Induction will allow us both to define more complex objects, and also to prove entire families of theorems (even infinitely many) at the same time.
This post is a sequel to several earlier posts about proofs and reasoning. I recommend reading those posts first.
Background
Induction over the natural numbers is the most well-known type of induction. In induction over the natural numbers, to prove a theorem we need to prove that the theorem holds in two different cases.
Suppose we want to show that a theorem is true for any natural number. Then we need to prove the following two sub-theorems:
Base case: Prove that a theorem holds for case \(n = 0\).
Inductive case: Prove that if a theorem holds for case \(n = k\), then the theorem also holds for \(n = k + 1\).
For example, suppose we wanted to prove that the sum of the first \(n\) natural numbers is \(n(n+1)/2\).
Base Case: It’s true for \(n = 0\).
\[ \sum_{s=0}^0 s = 0*(0+1)/2 = 0 \]
Inductive Case:
Suppose we have:
\[ S(k) = \sum_{s=0}^k s = k(k+1)/2 \]
Then:
\[ \begin{align*} \sum_{s=0}^{k+1} s &= (k + 1) + S(k) \\[0.5em] &= (k + 1) + \frac{k(k + 1)}{2} \\[0.5em] &= \frac{2(k + 1)}{2} + \frac{k(k + 1)}{2} \\[0.5em] &= \frac{(k + 2)(k + 1)}{2} \\ &= \frac{((k + 1) + 1)(k + 1)}{2} \\ &= S(k + 1) \end{align*} \]
There’s also structural induction: for any recursively-defined data structure, if we prove the theorem for any base case of the structure, and we prove the theorem for each dependent case, then we prove the theorem. For example, you can have induction indexed by paths through binary tree.
Suppose we have some root node of a tree, and we have two operators, \(left\) and \(right\). We want to show that the theorem is true given any path from the root. That is, any sequence of \(left\) and \(right\) applied to \(root\). These theorems look like \(left(root)\) or \(right(root)\) or \(left(left(right(left(root))))\), etc.
To prove this family of theorems, we need to prove three sub-theorems:
Base case: Prove that a theorem holds for the root case.
Left: Prove that if a theorem holds for case \(parent\), then it holds for the \(left(parent)\) case.
Right: Prove that if a theorem holds for the \(parent\) case, then it holds for the \(right(parent)\) case.
For example, suppose we start with \(0\). We want to prove that any sequence of adding \(1\) and multiplying by \(2\) is greater than or equal to 0 (think of these as \(L(x) = x + 1\) and \(R(x) = 2x\)).
For example, \(L(R(L(R(R(L(0)))))) \geq 0\) is an example expression, but there are an infinite number of similar expressions. How do we prove all of them?
We can simplify if we see that each expression corresponds to a node on a binary tree. Each node contains a number. The left child’s number is “add \(1\)” to parent. The right child’s number is “multiply by \(2\)” on the parent.
Base Case: \(0 \geq 0\). We have an implicit assumption that the empty expression is \(0\), but we could adapt the proof to other starting numbers.
Left Inductive Case: Suppose we have an integer \(n \geq 0\). Then \(n + 1 \geq 0\)
Right Inductive Case: Suppose we have an integer \(n \geq 0\). Then \(2n \geq 0\).
Therefore, the theorem holds for any such sequence of operations \(L\) and \(R\).
Some inductive types are even simpler. For example, simple case expressions or equality may be represented as inductive types. So: how do we implement induction in code?
Inductive Types
We have two separate constructs, the constructors for the inductive types, and the InductiveType class itself.
The InductiveType class has five different fields:
name: a string identifies the inductive type.
params: These are the parameters that the type takes. For instance, if we’re defining a List type, it might have a parameter to describe type of elements it contains (e.g. List[Int]).
indices: Similar to parameters but vary between different constructors. For example, in a fixed-length list length could be an index that changes with each constructor.
returnType: This specifies what universe the inductive type lives in. For example,
Natlives inSet, because it’s a collection of objects we can compute with.constructors: Ways to build values of this type. The natural numbers have two constructors: a zero constructor and a successor constructor. A tree type has root, left, and right as constructors.
To actually define the inductive type, call define_inductive:
def form_inductive_type(inductive: InductiveType) -> Term:
result = inductive.returnType
# Add indices
for index in reversed(inductive.indices):
result = ProductType(index.term_, index.type_, result)
# Add parameters
for param in reversed(inductive.params):
result = ProductType(param.term_, param.type_, result)
return result
def define_inductive(env: Environment, inductive: InductiveType) -> Environment:
# First add the type itself
inductive_type = form_inductive_type(inductive)
env = w_global_def(env,
Constant(inductive.name),
Hypothesis(env, Constant(inductive.name), inductive_type))
# Then add each constructor
for constructor in inductive.constructors:
env = w_global_def(env,
Constant(constructor.name),
Hypothesis(env, Constant(constructor.name), constructor.type_))
# Generate and add elimination principles
env = add_elimination_principles(env, inductive)
return envThis also adds all of the constructors and elimination principles to the environment.
Elimination Principles
The actual machinery that operates the inductive types is the elimination principles. To prove a theorem over Nat, we need to prove a base case and an inductive case in order to prove the theorem for all of Nat. This is the essence of the elimination principle for Nat: given input types for each constructor, it produces a type for the overall theorem. However, there are many more inductive types than just Nat, we need an algorithm to automatically produce the elimination principle given a definition.
def add_elimination_principles(env: Environment, inductive: InductiveType) -> Environment:
# Create the motive
P = Variable(f"P_{inductive.name}")
motive_type = build_motive_type(inductive)
env = w_local_assum(env, P, Hypothesis(env, motive_type, Type()))
# For each constructor, generate its elimination case
cases = []
for constructor in inductive.constructors:
case_type = build_constructor_case(env, constructor, inductive, P)
case_var = Variable(f"case_{constructor.name}")
env = w_local_assum(env, case_var, Hypothesis(env, case_type, Type()))
cases.append((case_var, case_type))
# Build the final eliminator type
eliminator_type = build_eliminator_type(inductive, P, cases)
# Add the eliminator to the environment
rect_name = f"{inductive.name}_rect"
env = w_global_def(env,
Constant(rect_name),
Hypothesis(env, Constant(rect_name), eliminator_type))
return envThere’s a few substeps in here. We need to create the motive, then generate an elimination case for each constructor, then finally build the eliminator type. Let’s look at each step in turn.
Motives
The motive is what we want to prove about every value of the type. For example, for the natural numbers, this would be something like \(\mathbb{N} \to \text{Type}\): we want to construct a type for the natural numbers. The type might represent, say, a proposition \(P\) we want to prove for natural numbers (could be \(P(n)\) is even, could be \(P(n) > 0\), etc.).
The motive is more complex if the types have parameters or indices. For example, equality motive takes a type \(A\) and two element \(x\) and \(y\), and the propositions we might want to prove would concern the equality of those elements of type \(A\).
In more detail, for equality, we should get back something like: P_eq: ∀(A: Type)(x: A)(y: A), eq A x y -> Type
def build_motive_type(inductive: InductiveType) -> Term:
result = inductive.returnType
target = Constant(inductive.name)
for param in inductive.params:
target = Application(target, param.term_)
for index in inductive.indices:
target = Application(target, index.term_)
x = Variable(f"x_{inductive.name}")
result = ProductType(x, target, result)
# Add bindings for indices in reverse order
for index in reversed(inductive.indices):
result = ProductType(index.term_, index.type_, result)
# Add bindings for parameters in reverse order
for param in reversed(inductive.params):
result = ProductType(param.term_, param.type_, result)
return resultThe algorithmic steps are basically iterating through and binding all parameters and indices.
Constructor Cases
A constructor is any way to introduce the elements of a give type. For example, in Nat, we either introduce the zero element (\(O\)), which takes no arguments, or we use the successor constructor (\(S\)), which takes a natural number and returns a new natural number (intuitively, the input natural plus one).
The constructor cases tell us how to prove the motive holds for each constructor. For example, for Nat, we need to prove \(P(O)\) for the zero case, we need to prove that for any \(n\), if \(P(n)\) holds then \(P(S(n))\) holds.
def build_constructor_case(env: Environment,
constructor: InductiveTypeConstructor,
inductive: InductiveType,
motive: Variable) -> Term:
def process_type(t: Term) -> Term:
match t:
case ProductType(var, domain, codomain):
is_recursive = (isinstance(domain, Constant) and
domain.name == inductive.name)
if is_recursive:
# Add inductive hypothesis
ih = Application(motive, var)
return ProductType(var, domain,
ProductType(Variable(f"ih_{var.name}"), ih,
process_type(codomain)))
return ProductType(var, domain, process_type(codomain))
case _:
return Application(motive, t)
return process_type(constructor.type_)As you can see above, need to apply the motive to the term. However, if the term is a product type, we need to pass through all the bound variables.
If the term is recursively defined (for example, the successor function for Nat is defined from Nat to Nat, so it’s defined recursively) we need to pass through all the bound variables and construct
Eliminators
Finally, we tie everything together. Given a motive \(P\), proofs for each constructor case, and a target value of the inductive type, you call the eliminator to produce a proof that the motive holds for that target value.
def build_eliminator_type(inductive: InductiveType,
motive: Variable,
cases: List[tuple[Variable, Term]]) -> Term:
# Start with motive application to target
target = Variable(f"target_{inductive.name}")
result = Application(motive, target)
target_type = Constant(inductive.name)
for param in inductive.params + inductive.indices:
target_type = Application(target_type, param.term_)
# Add target
result = ProductType(target, target_type, result)
# Add case hypotheses
for case_var, case_type in reversed(cases):
result = ProductType(case_var, case_type, result)
# Add motive
motive_type = build_motive_type(inductive)
result = ProductType(motive, motive_type, result)
# Add parameters and indices
for param in reversed(inductive.params + inductive.indices):
result = ProductType(param.term_, param.type_, result)
return result Now we can automatically generate the eliminators. In the next section we will define some inductive types and look at the eliminators.
Inductive Definitions
Let’s take a look at some simple inductive types.
Equals
Here we check if two variables \(x\) and \(y\) of type \(A\) are equal.
def define_equality(env: Environment, type_: Type) -> Environment:
A = Variable("A")
x = Variable("x")
y = Variable("y")
# eq_refl : ∀ (A : Type) (x : A), eq A x x
eq1 = Constant("eq")
eq2 = Application(eq1, A)
eq3 = Application(eq2, x)
eq4 = Application(eq3, x)
prod1 = ProductType(x, A, eq4)
refl_type = ProductType(A, type_, prod1)
equality = InductiveType(
name="eq",
params=[DefinedVariableHolder(A, type_)],
indices=[DefinedVariableHolder(x, type_), DefinedVariableHolder(y, type_)],
returnType=Prop(),
constructors=[InductiveTypeConstructor("eq_refl", refl_type)]
)
return define_inductive(env, equality)Here’s the printed \(eq_{rect}\) type.
Constant(eq_rect):(Set->(Set->(Set->∀P_eq:((Set->(Set->(Constant(eq) Var(A):Set)))->Type(0)),(∀A:Set,∀x:Var(A),(Var(P_eq) (((Constant(eq) Var(A)) Var(x)) Var(x)))->∀target_eq:Constant(eq),(Var(P_eq) Var(target_eq))))))
Complicated. What does this do? Given 3 sets (\(A\), \(x\), \(y\)), and a proposition (\(P_{eq}\)) that takes two sets \(x\) and \(y\) and returns a type, we return a new function.
The new function says that if you have function/proof that takes sets \(A\) and \(x\) and shows \(P_{eq}\) in the reflective case, then you can produce the target equality proof.
For example, suppose we want to prove that if \(x = y\), then \(y = x\). We define \(A\), \(x\), \(y\) as variables, and provide \(P_{eq}\) (which is \(x = y\) in this case). We get back a function that takes a proof that \(P_{eq}\) holds if \(x = x\), and we can return a proof that \(P_{eq}\) is true for any equality of \(A\), \(x\), \(y\).
If that is confusing, we will see it in code shortly.
Nat
The natural numbers. Note the two constructors.
def define_nat(env: Environment) -> Environment:
nat_type = InductiveType(
name="nat",
params=[],
indices=[],
returnType=Set(),
constructors=[
InductiveTypeConstructor("O", Constant("nat")),
InductiveTypeConstructor("S",
ProductType(Variable("n"), Constant("nat"), Constant("nat")))
]
)
return define_inductive(env, nat_type)Here’s the natural number eliminator. ∀P_nat:(Constant(nat)->Type(0)),((Var(P_nat) Constant(nat))->((Constant(nat)->((Var(P_nat) Var(n))->(Var(P_nat) Constant(nat))))->∀target_nat:Constant(nat),(Var(P_nat) Var(target_nat))))
Given \(P_{nat}\), a theorem about some natural numbers, we get a new function.
The new function takes as a input theorem on \(nat\) (the zero value) and a theorem about the successor function. Then it returns the theorem for the naturals. This corresponds to our earlier example of induction over the naturals.
Basic Proofs
Let’s look at some proofs.
\(0 = 0\)
def prove_zero_eq_zero() -> Hypothesis:
env = w_empty()
env = define_nat(env)
env = define_equality(env, Set())
nat_hyp = const(env, Constant("nat"))
zero_hyp = const(env, Constant("O"))
refl_hyp = const(env, Constant("eq_refl"))
nat_app = app(env, refl_hyp, nat_hyp)
proof = app(env, nat_app, zero_hyp)
return proofThis is trivial, just an application of nat and eq.
\(\forall k\in \mathbb{N}, k + 0 = k\)
Caveat Lector: I am not confident that this code is correct.
Here I attempt to prove that for any natural number \(n\), \(n + 0 = n\).
def prove_plus_zero() -> Hypothesis:
env = w_empty()
env, _ = define_nat(env)
env, _ = define_equality(env, Set())
env = add_plus(env)
n = Variable("n")
nat_hyp = const(env, Constant("nat"))
zero_hyp = const(env, Constant("O"))
succ_hyp = const(env, Constant("S"))
plus_hyp = const(env, Constant("plus"))
nat_rect_hyp = const(env, Constant("nat_rect"))
eq = const(env, Constant('eq'))
# Base case
zero_plus_zero = app(env, app(env, plus_hyp, zero_hyp), zero_hyp)
eq_nat = app(env, eq, nat_hyp)
eq_nat_0 = app(env, eq_nat, zero_hyp)
eq_0_eq_0plus0 = app(env, eq_nat_0, zero_plus_zero)
# Step case
k = Variable("k")
env = w_local_assum(env, k, nat_hyp)
hyp_k = var(env, k)
k_plus_zero = app(env, app(env, plus_hyp, hyp_k), zero_hyp)
sk_plus_zero = app(env, succ_hyp, k_plus_zero)
sk = app(env, succ_hyp, hyp_k)
eq_nat_sk = app(env, eq_nat, sk)
eq_sk_skplus0 = app(env, eq_nat_sk, sk_plus_zero)
# Motive
n = Variable("n")
env = w_local_assum(env, n, nat_hyp)
n_hyp = var(env, n)
n_plus_zero = app(env, app(env, plus_hyp, n_hyp), zero_hyp)
eq_nat_n = app(env, eq_nat, n_hyp)
motive_body = app(env, eq_nat_n, n_plus_zero)
product_hyp = prod_set(env, n, nat_hyp, motive_body)
motive = lam(env, n, product_hyp, motive_body) # This lam has issues in type_equal
# motive = lam_auto(env, n, nat_hyp, motive_body) # Alternative using lam_auto
# Use nat_rect
with_motive = app(env, nat_rect_hyp, motive) # This application has issues in type_equal
with_base = app(env, with_motive, eq_0_eq_0plus0) # Apply base case
thm = app(env, with_base, eq_sk_skplus0) # Apply step case
final = app(env, thm, hyp_k)
return finalAs you can see, there’s a few main steps.
Setup: I unpack all the definitions into the environment.
Getting the base case (\(0 + 0 = 0\))
Getting the step case (\(S(k + 0) = S(k)\))
Generating the motive (In this case, \(\forall n\in \mathbb{N}, n = n + 0\))
Then, we apply nat_rect to each element, to generate the theorem.
One we have thm, we can specialize it to any \(k \in \mathbb{N}\), as shown1.
Next Steps
We’ve now managed to implement basic induction, and prove a trivial theorem.
If you’re following the game plan, we are through the first four steps, and partway through the fifth.
Next, to prove more non-trivial theorems, we’re going to need to implement a match construct. We may also need to deal more with minutiae of conversions between types, such as sort hierarchies, subtyping, singleton elimination, etc.
Changelog
01-15-2025 - Added a non-trivial proof example.
Footnotes
Note that, though I think the final output is correct, there appear to be some issues running the type_equals checks in my typing_rules code. I wanted to get a non-trivial example of an inductive proof down stat, but I’ll come back and correct this once I’ve figured out what the problem is.↩︎