形式化证明(Lean)

如果相等需要为对称性、传递性、合同性等分别设立公理,可信内核就会随着关于 $=$ 的每条新事实而膨胀。从一个消去子推出所有这些性质,才能让内核保持很小。

固定 $a$。我们想要一个函数,对任意 $b$,把 $h : a = b$ 变成 $b = a$ 的证明。用动机(motive)$C(y, h) := (y = a)$ 来使用 $\mathsf{Eq.rec}$——这是一族由点 $y$ 及连接 $a$ 到 $y$ 的证明 $h$ 索引的命题。

消去子要求提供基础情形 $C(a, \mathrm{refl}\,a)$ 的证明,即 $a = a$;我们提供 $\mathrm{refl}\,a$ 本身。这是合法的,因为基础情形总是在起点 $a$ 处由 $\mathrm{refl}$ 索引。

于是 $\mathsf{Eq.rec}$ 对每个 $y$ 与每个 $h : a = y$ 返回 $C(y,h) = (y = a)$ 的证明。代入 $y := b,\ h := h$:我们恰好得到 $b = a$ 的证明。

把它打包为 $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$,就得到类型为 $\mathrm{Eq.symm} : a = b \to b = a$ 的项。内核仅通过将这个应用与 $\mathsf{Eq.rec}$ 的类型签名匹配就能接受它——在内核层面完全不需要对"对称性"这一概念进行推理。

把等式串联起来($a=b=c$ 因而 $a=c$)几乎在每个证明中都会用到;如果这是一条公理而不是一个可推导的项,内核就必须信任该公理,而不能通过计算来验证它。

固定 $a,b$ 及 $h_1 : a = b$。给定任意 $c$ 上的 $h_2 : b = c$,我们想要 $a = c$ 的证明。用动机 $C(y, h) := (a = y)$(由点 $y$ 及连接 $b$ 到 $y$ 的证明 $h$ 索引)对 $h_2$ 使用 $\mathsf{Eq.rec}$。

所需的基础情形是 $C(b, \mathrm{refl}\,b)$,即 $a = b$——恰好就是 $h_1$。所以 $h_1$ 就是提供给 $\mathsf{Eq.rec}$ 的基础情形证明。

于是 $\mathsf{Eq.rec}$ 对每个 $c$ 与每个 $h_2 : b = c$ 给出 $C(c, h_2) = (a = c)$ 的证明,这正是我们想要的。

所以 $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ 的类型是 $\mathrm{Eq.trans} : a = b \to b = c \to a = c$。注意它与对称性共享的模式:两个证明都是通过选取合适的动机 $C$,沿着一个相等关系"传输"一个事实,而真正的计算工作则交给内核对 $\mathrm{refl}$ 上 $\mathsf{Eq.rec}$ 的固定归约规则来完成。