相等也是归纳类型

声明

在 Lean 中，相等的声明是

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

对 $a, b : A$，类型 $\Eq{u}\;A\;a\;b$ 是“$a$ 与 $b$ 相等”这一命题；当 $A$ 是 $\Nat$ 时我们把它写作 $a = b$。用第 8 章的术语说，$A$ 和 $a$ 是参数，$b$ 是索引：

唯一的构造子 $\refl{u}$ 没有字段，它的索引项是 $a$：它只能证明两边是同一个 $a$ 的等式。所以 $\Eq{}$ 像 $\mathsf{Vec}$ 一样是归纳族，而不是单个类型。左边由参数固定；右边可变，而构造子把它钉在左边上。

递归子：传输

非形式地说，$\Eq{}$ 的递归子表示：若 $a = b$，则凡对 $a$ 成立者对 $b$ 也成立。 这是莱布尼茨原理，其最常见的形式是

给定 $A$ 的元素的一个性质 $M$、证据 $m : M\;a$ 和 $a = b$ 的证明 $h$，它返回 $M\;b$ 的证据，我们说它沿着 $h$ 传输 $m$。它的计算规则说，沿着 $\refl{}$ 传输什么也不做：

第 8 章的通用方法生成的版本略为一般，$\EqRec{}$ 是由它构造出的一个定义。

例如，设 $P : \Nat \to \Sort{0}$，$a, b : \Nat$，$h : a = b$，$\mathit{pa} : P\;a$。取 motive $M = P$，得到

这一行就是重写的逻辑内容：关于 $a$ 的事实变成关于 $b$ 的事实。第 10 章的 rw 策略会自动构造这样的项。

定义相等与命题相等

现在有了两种相等概念，区分它们是理解证明助手行为的关键。

• 定义相等 $\conv$ 由内核通过计算来判定。它是关于项的判断，不是类型；不涉及任何证明对象。
• 命题相等 $\Eq{}$ 是一个类型，它的证明是项，而找到一个证明可能需要真正的推理，例如归纳。

构造子 $\refl{}$ 把二者联系起来：由 T-Conv，只要 $a \conv b$，就有 $\refl{u}\;A\;a : \Eq{u}\;A\;a\;b$。所以每个定义相等都免费给出一个命题相等，但反之不成立，标准的例子是 $n + 0 = n$ 和 $0 + n = n$ 这两半。采用第 7 章 $\add$ 的定义，并记 $s$ 为它的步骤函数，

所以 $\refl{1}\;\Nat\;n : n + 0 = n$，Lean 用 rfl 证明它。相反，

是卡住的：$n$ 是变量，而 ι 规则只在 $\zero$ 和 $\suc$ 上触发。所以 $0 + n = n$ 不能用 $\refl{}$ 证明，需要归纳。

归约浏览器展示了这两个计算，其中 $n$ 是上下文中的变量。第一个到达 $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

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 由计算成立：递归子看到的是构造子 zero。
goal forall (n : Nat), Eq Nat (add n Nat.zero) n
intro n
rfl
qed

# 0 + n = n 则不然：递归子卡在变量 n 上。
goal forall (n : Nat), Eq Nat (add Nat.zero n) n
intro n
rfl

示例：证明 0 + n = n

我们用归纳证明 $\tPi{n}{\Nat}{0 + n = n}$，使用 $\NatRec{0}$ 和 motive $M_0 = \tLam{n}{\Nat}{0 + n = n}$。

基础情形。 我们需要 $M_0\;0$，它可转换为 $0 + 0 = 0$。由于 $0 + 0$ 计算为 $0$，项 $\refl{1}\;\Nat\;0$ 即可。

归纳步骤。 给定 $k : \Nat$ 和 $\mathit{ih} : 0 + k = k$，我们需要 $M_0\;(\suc\;k)$，即 $0 + \suc\;k = \suc\;k$。由第二条 ι 规则，$0 + \suc\;k$ 计算为 $\suc\;(0 + k)$，所以只需证明 $\suc\;(0 + k) = \suc\;k$。我们从 $\refl{1}\;\Nat\;(\suc\;(0 + k))$ 出发，它是 $\suc\;(0+k) = \suc\;(0+k)$ 的证明，然后用 motive $N = \tLam{b}{\Nat}{\suc\;(0 + k) = \suc\;b}$ 沿着 $\mathit{ih}$ 传输它，这把第二个 $0 + k$ 替换为 $k$：

证明为

内核用算法 5.1 检查它：每个参数都对照 $\NatRec{0}$ 的类型中以 $M_0$ 实例化后的相应部分进行检查，每次比较都在规范化之后成功。下面是完整的项，一次性提交给内核，其中非依赖递归子先定义，如图 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

# 层级 (1, 0) 的 Eq.ndrec：沿着 a = b 把 M a 的证明传输到 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

手写这样的项很繁琐，而找到正确的 motive 才是难点：motive $N$ 必须恰好在 $0 + k$ 出现的两处之一提及 $b$。策略（第 10 章）把记账工作和 motive 的选择都自动化了。

内核的变化

从命题逻辑走到带相等的算术，内核改动很少：$\Infer$ 增加了常量的情形，它在 $\Sigma$ 中查找类型（T-Const）；$\Check$ 没有变化；只有 $\Whnf$，以及经由它的 $\IsDefEq$，学会了新的 δ 步骤和 ι 步骤。第 12 章展示单个 $\Whnf$ 如何处理每一种归纳类型，第 14 章讨论归纳类型给元理论带来的变化。

练习

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