Equality Is an Inductive Type Too

The declaration

In Lean, equality is declared as

inductive Eq {A : Sort u} (a : A) : A -> Prop where
  | refl : Eq a a

For $a, b : A$, the type $\Eq{u}\;A\;a\;b$ is the proposition that $a$ and $b$ are equal; when $A$ is $\Nat$ we write it $a = b$. In the terms of Chapter 8, $A$ and $a$ are parameters and $b$ is an index:

The only constructor $\refl{u}$ has no fields, and its index term is $a$: it can only prove equations whose two sides are the same $a$. So $\Eq{}$ is an inductive family like $\mathsf{Vec}$, not a single type. The left side is fixed by the parameter; the right side varies, and the constructor pins it to the left side.

The recursor: transport

Informally, the recursor of $\Eq{}$ says: if $a = b$, then whatever holds of $a$ holds of $b$. This is Leibniz's principle, and in its most common form it reads

Given a property $M$ of elements of $A$, evidence $m : M\;a$, and a proof $h$ that $a = b$, it returns evidence of $M\;b$. We say that it transports $m$ along $h$. Its computation rule says that transporting along $\refl{}$ does nothing:

The version the general recipe of Chapter 8 generates is slightly more general, and $\EqRec{}$ is a definition built from it.

For example, suppose $P : \Nat \to \Sort{0}$, $a, b : \Nat$, $h : a = b$, and $\mathit{pa} : P\;a$. Choosing the motive $M = P$ gives

This one line is the logical content of rewriting: a fact about $a$ becomes a fact about $b$. The rw tactic of Chapter 10 builds such terms automatically.

Definitional versus propositional equality

There are now two notions of equality, and keeping them apart is essential to understanding how a proof assistant behaves.

• Definitional equality $\conv$ is decided by the kernel, by computation. It is a judgment about terms, not a type; no proof object is involved.
• Propositional equality $\Eq{}$ is a type. Its proofs are terms, and finding one may require real reasoning, such as induction.

The constructor $\refl{}$ connects them: by T-Conv, $\refl{u}\;A\;a : \Eq{u}\;A\;a\;b$ whenever $a \conv b$. So every definitional equality yields a propositional one for free. The converse fails, and the standard example is the two halves of $n + 0 = n$ and $0 + n = n$. With the definition of $\add$ from Chapter 7 and $s$ its step function,

so $\refl{1}\;\Nat\;n : n + 0 = n$, and Lean proves this by rfl. In contrast,

is stuck: $n$ is a variable, and the iota-rules fire only on $\zero$ and $\suc$. So $0 + n = n$ is not provable by $\refl{}$ and needs induction.

The reduction explorer shows both computations with $n$ as a variable in the context. The first reaches $n$; the second stops with the recursor waiting for a constructor it will never get.

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 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 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

# n + 0 = n holds by computation: the recursor sees the constructor zero.
goal forall (n : Nat), Eq Nat (add n Nat.zero) n
intro n
rfl
qed

# 0 + n = n does not: the recursor is stuck on the variable n.
goal forall (n : Nat), Eq Nat (add Nat.zero n) n
intro n
rfl

Example: proving 0 + n = n

We prove $\tPi{n}{\Nat}{0 + n = n}$ by induction, using $\NatRec{0}$ with the motive $M_0 = \tLam{n}{\Nat}{0 + n = n}$.

Base. We need $M_0\;0$, which is convertible to $0 + 0 = 0$. Since $0 + 0$ computes to $0$, the term $\refl{1}\;\Nat\;0$ works.

Step. Given $k : \Nat$ and $\mathit{ih} : 0 + k = k$, we need $M_0\;(\suc\;k)$, that is, $0 + \suc\;k = \suc\;k$. By the second iota-rule, $0 + \suc\;k$ computes to $\suc\;(0 + k)$, so it suffices to prove $\suc\;(0 + k) = \suc\;k$. We start from $\refl{1}\;\Nat\;(\suc\;(0 + k))$, a proof of $\suc\;(0+k) = \suc\;(0+k)$, and transport it along $\mathit{ih}$ with the motive $N = \tLam{b}{\Nat}{\suc\;(0 + k) = \suc\;b}$, which replaces the second $0 + k$ by $k$:

The proof is

The kernel checks it with Algorithm 5.1. Each argument is checked against the corresponding part of the type of $\NatRec{0}$, instantiated with $M_0$, and every comparison succeeds after normalization. Here is the complete term, submitted to the kernel in one piece. The non-dependent recursor is defined first, as in Figure 9.1.

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

# Eq.ndrec at levels (1, 0): transport a proof of M a along a = b to M b.
def ndrec : forall (A : Sort 1), forall (a : A), forall (M : A -> Sort 0), M a -> forall (b : A), Eq A a b -> M b := fun (A : Sort 1) => fun (a : A) => fun (M : A -> Sort 0) => fun (m : M a) => fun (b : A) => fun (h : Eq A a b) => Eq.rec0 A a (fun (b' : A) => fun (_h : Eq A a b') => M b') m b h

goal forall (n : Nat), Eq Nat (add Nat.zero n) n
exact Nat.rec0 (fun (n : Nat) => Eq Nat (add Nat.zero n) n) (Eq.refl Nat Nat.zero) (fun (k : Nat) => fun (ih : Eq Nat (add Nat.zero k) k) => ndrec Nat (add Nat.zero k) (fun (b : Nat) => Eq Nat (Nat.succ (add Nat.zero k)) (Nat.succ b)) (Eq.refl Nat (Nat.succ (add Nat.zero k))) k ih)
qed

Writing such terms by hand is tedious, and finding the right motive is the hard part: the motive $N$ had to mention $b$ in exactly one of the two places where $0 + k$ occurs. Tactics (Chapter 10) automate both the bookkeeping and the choice of motive.

Changes to the kernel

Little changed to get from propositional logic to arithmetic with equality. $\Infer$ gained a case for constants, which looks up the type in $\Sigma$ (T-Const). $\Check$ is unchanged. Only $\Whnf$, and through it $\IsDefEq$, learned the new delta- and iota-steps. Chapter 12 shows how a single $\Whnf$ handles every inductive type, and Chapter 14 discusses what inductive types change in the metatheory.

Exercises

goal forall (a : Nat), forall (b : Nat), Eq Nat a b -> Eq Nat b a
exact fun (a : Nat) => fun (b : Nat) => fun (h : Eq Nat a b) => ndrec Nat a (fun (x : Nat) => Eq Nat x a) (Eq.refl Nat a) b h
qed