Lean における等号の証明パターン¶
Lean の等号 a = b は Eq a b という型です．
つまり「a = b を証明する」とは，型 Eq a b の証明項を構成することです．
ただし，数学で一言で「等しい」と言うものが，Lean ではいくつかの層に分かれます．
| レベル | 数学での状況 | Lean での姿 | 典型的な証明方法 |
|---|---|---|---|
| 定義的な等しさ | 定義から同じ | definitional equality | rfl，change，dsimp |
| 命題的な等しさ | 補題や仮定で等しい | propositional equality, Eq |
rw，calc，exact h |
| 自動化された等式証明 | 正規化すれば同じ | Eq の証明を tactic が作る |
simp，decide，grind |
| 外延的な等しさ | 点ごと・元ごと・成分ごとに同じ | extensional equality | funext，ext |
| 命題外延性 | 論理的に同値な命題を等しい命題として扱う | propositional extensionality | propext |
| 商での等しさ | 同値な代表元を商では同じと見る | quotient equality | Quot.sound |
この表のうち，最初の definitional equality だけは Lean の項として直接書く命題ではありません．
これは Lean のカーネルが内部で判断する「計算と定義展開により同じ式である」という関係です．
両辺が定義的に等しければ，rfl によって命題的等号 a = b の証明を作れます．
逆に，h : a = b があるからといって，a と b が定義的に等しいとは限りません．
この環境の自然数の加法では，n + 0 は定義を展開すると n になり，rfl で閉じます．
一方，0 + n = n は数学的には同じくらい基本的な等式ですが，変数 n が具体的に 0 か Nat.succ k か分からない状態では計算が進みません．
したがって，これは一般には definitional equality ではなく，定理として証明する propositional equality です．
simp で閉じるからといって，その等式が definitional equality であるとは限りません．
simp は定義展開だけでなく，Nat.zero_add のような単純化補題を使って Eq の証明を作ります．
decide や grind も同様に，判定手続きや推論によって証明を生成する tactic であり，単に rfl で閉じているわけではない場合があります．
交換法則のような等式も，数学的には明らかでも定義を展開するだけでは同じ式になりません．
この場合は，Nat.add_comm のような定理を使って Eq 型の証明項を構成します．
example (a b : Nat) : a + b = b + a := by
exact Nat.add_comm a b
example (a b c : Nat) : a + (b + c) = b + (a + c) := by
calc
a + (b + c) = (a + b) + c := by
rw [Nat.add_assoc]
_ = (b + a) + c := by
rw [Nat.add_comm a b]
_ = b + (a + c) := by
rw [Nat.add_assoc]
等式は書き換えにも使います．
rw [h] は，証明項 h : a = b を使って，ゴール中の a を b に置き換えます．
example (a b : Nat) (h : a = b) : a.succ = b.succ := by
rw [h]
example (a b c : Nat) (h : a = b) : a + c = b + c := by
rw [h]
example (a b c : Nat) (h : a = b) : b + c = a + c := by
rw [← h]
同じことを，合同性の補題 congrArg を使って証明することもできます．
これは「等しい入力に同じ関数を適用すれば，結果も等しい」という原理です．
少し先の話ですが，型の等号と同型・同値も区別します．
数学では「同型な対象を同じと思う」と言うことがありますが，Lean では α = β と α ≃ β は別の主張です．
等号 h : α = β があれば cast h により項を移送できますが，これは同値や同型を与えることとは違います．
定義的な等しさ由来の cast は計算で消えやすく，funext や ext から来る非自明な等号は，証明上は便利でも計算上は扱いが重くなることがあります．
命題外延性 propext や商型 Quot による等号は，次の advanced 節で扱います．
ここで重要なのは，すべての「等しい」が同じ理由で証明されるわけではない，という点です．
rfl は Lean が計算で同じだと分かる等号です．
rw，simp，calc は，補題や仮定から Eq の証明を作って使います．
funext や ext は，点ごと・元ごと・成分ごとの一致から全体の等式を作ります．
propext や Quot.sound は，標準的な数学を Lean で扱うための追加原理と結びついています．
証明が通らないときは，まず「これは定義的な等しさで閉じたいのか，補題による等式なのか，外延性で成分ごとに示すべき等式なのか，advanced な原理に由来する等式なのか」を切り分けると，次に使う tactic が選びやすくなります．