等式も帰納型である

宣言

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$ の証拠を返す。$m$ を $h$ に沿って輸送（transport）する、という。その計算規則は、$\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 で証明する。対照的に、

は行き詰まる（stuck）。$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$ を証明すれば足りる。$\suc\;(0+k) = \suc\;(0+k)$ の証明 $\refl{1}\;\Nat\;(\suc\;(0 + k))$ から出発し、motive $N = \tLam{b}{\Nat}{\suc\;(0 + k) = \suc\;b}$ で $\mathit{ih}$ に沿って輸送する。この motive は二つ目の $0 + k$ を $k$ に置き換える。

証明は次のとおりである。

カーネルはこれをアルゴリズム 5.1 で検査し、各引数は、$M_0$ でインスタンス化した $\NatRec{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: M a の証明を a = b に沿って 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