証明支援系による形式証明(Lean)

対称性、推移性、合同性などのために等号ごとに別の公理が必要だとすれば、信頼されたカーネルは $=$ に関する新しい事実ごとに肥大化してしまう。すべてを一つの除去子から導くことでカーネルを小さく保てる。

$a$ を固定する。任意の $b$ について $h : a = b$ を受け取り $b = a$ の証明を返す関数が欲しい。モチーフ $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}$ に対するカーネルの固定された還元規則に委ねている。