タクティク: 対話的に証明項を組み立てる

Lean では、第 9 章の定理は次のように証明される。

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]

各タクティクは、証明項の一部を組み立てる小さなプログラムであり、カーネルの外側で動く。その出力はふつうの項であり、カーネルは他の項と同じようにアルゴリズム 5.1 でそれを検査する。

ゴールと証明状態

ゴール（goal）$\goal{\Gamma}{\hole{m}}{T}$ は、文脈 $\Gamma$ における型 $T$ の項を求める。ホール（hole）$\hole{m}$ はまだ見つかっていない項を表し、Lean ではこれをメタ変数と呼ぶ。証明状態（proof state）は、ゴールのリストと、ホールを含みうる項である部分的な証明項を合わせたものである。

$T$ を証明するには、部分項 $\hole{0}$ と唯一のゴール $\goal{\cdot}{\hole{0}}{T}$ から始める。タクティクは最初のゴール $\goal{\Gamma}{\hole{m}}{T}$ に対して働き、$\hole{m}$ に、新鮮なホールを含みうる項を割り当て、そのゴールを新鮮なホールごとに一つの新しいゴールで置き換える。ゴールが残っていなければ部分項にホールはなく、カーネルがそれを $T$ に対して検査する。ホールは束縛子の下に置かれることがあり、$\tLam{x}{A}{\hole{1}}$ の $\hole{1}$ がそうで、それを埋める項はその束縛変数を使ってよい。ゴールがそれぞれ自分の文脈を持つのはそのためである。

各タクティクは、新鮮な各ホールがのちにそのゴールの述べる型の項で埋められると仮定したうえで、自分の割り当てが $\Gamma$ において型 $T$ を持つことを保証しなければならない。これを $\goal{\Gamma}{\hole{m}}{T} \leadsto \text{new goals}$ と書き、続けて割り当てを書く。

最初の例

スクリプト examples/identity.leanmini は第 1 章の冒頭の例を証明し、下のエクスプローラはそれを一コマンドずつ実行する。

goal forall (P : Sort 0), P -> P
intro P
intro p
exact p
qed

ボタンか矢印キーで一歩ずつ進めてほしい。中央のパネルは各コマンドの後のゴールのリスト、右のパネルは部分的な証明項で、現在のゴールに対応するホールが強調されている。三つのパネルは常に一致する。タクティクがホールに項を割り当てるからこそ、ゴールが変わる。

ゴールのリストだけでは足りない。intro p のあと、ゴール $P$ は、その解が二つの $\lambda$ で包まれなければならないことを覚えておらず、部分項がそれを記録する。

基本的なタクティク

intro x。 $T$ が $\Pi$ 型に正規化されるとき、このタクティクはその引数を文脈に移す。

割り当てが正しい型を持つことは T-Lam による。名前 $x$ は $\dom(\Gamma)$ に含まれていてはならず、さもないと新しい仮定が既存の仮定をシャドーイングし、カーネルが不健全になる（第 11 章）。本書の intro はそのような名前を「binder name already in context」というメッセージで拒否するが、Lean は名前を付け替える。

exact t。 このタクティクは、与えられた項でゴールを閉じる。

その前に自分で $\Check(\Gamma, t, T)$ を実行する。型の正しくない $t$ はどのみち最後にカーネルが拒否するので、早めに検査するのは、よりよいエラーメッセージのためでしかない。

apply f。 $f$ が型 $A_1 \to \cdots \to A_n \to B$ を持ち $B \conv T$ であるとき、このタクティクは引数を新しいゴールとして残す。

割り当ては T-App を $n$ 回使って型 $B$ を持ち、T-Conv により型 $T$ を持つ。$f$ の型が依存 $\Pi$ のときは、後ろの $A_i$ と $B$ が前の引数に言及するので、タクティクは $B$ を $T$ と照合してそれらの引数を見つけなければならない。Lean はこれを単一化で行い、メタ変数について解くが、本書の制限版は非依存の矢印しか扱わず、それ以外は「dependent apply requires elaboration/unification」と報告する。（$n = 0$ のとき、つまり $f$ の型がすでに $T$ と変換可能なら、apply f は exact f と同じに振る舞う。）

たとえば、第 6 章の二つ目の演習だった含意の推移性は、結論から逆向きに進められる。

goal forall (P : Sort 0), forall (Q : Sort 0), forall (R : Sort 0), (P -> Q) -> (Q -> R) -> P -> R
intro P
intro Q
intro R
intro f
intro g
intro p
apply g
apply f
exact p
qed

六回の intro のあと、ゴールは $\goal{\Gamma}{\hole{6}}{R}$ で、$\Gamma = P, Q, R : \Sort{0},\; f : P \to Q,\; g : Q \to R,\; p : P$ である。型 $R$ の仮定はないので exact では閉じられないが、$g$ は $R$ で終わる。apply g は $\hole{6} \mathrel{:=} g\;\hole{7}$ を割り当て、$\hole{7} : Q$ を残す。同様に apply f は $\hole{7} \mathrel{:=} f\;\hole{8}$ を割り当てて $\hole{8} : P$ を残し、これを exact p が閉じる。得られる項の本体は $g\;(f\;p)$ である。二つのタクティクの違いに注意してほしい。$g$ の型は $Q \to R$ であって $R$ ではないので exact g は失敗する一方、apply g は、$g$ に足りない引数を新しいゴールに変える。

change T'。 このタクティクは、ゴールを定義的に等しいものに置き換える。

ただし $T'$ は型で、$T' \conv T$ でなければならない。項には何も加えず、ゴールの表示の仕方を変えるだけであり、それを正当化するのは T-Conv である。change が必要なのは、rw（後述）が部分項を α 同値までしか探さないからであり、計算してはじめて現れる部分項は、まず change で露出させなければならない。本章末尾の例がそうである。

rfl。 $T$ が $\Eq{u}\;A\;a\;b$ に正規化され $a \conv b$ であるとき、このタクティクはゴールを閉じる。

割り当ての型は $\Eq{u}\;A\;a\;a$ で、これはゴールと変換可能なので、rfl が証明するのは、定義的等価で成り立つ等式そのものである（第 9 章）。

帰納法

$n : \Nat$ を $\Gamma$ の変数とし、$\Gamma \vdash T : \Sort{u}$ とする。タクティク induction n は、ゴールの中の $n$ を抽象化して motive を作り、構成子ごとに一つのゴールを生成する。

motive を $M = \tLam{z}{\Nat}{\subst{T}{n}{z}}$ とすると、$\NatRec{u}\;M$ の型は $M\;\zero$ と $\tPi{k}{\Nat}{M\;k \to M\;(\suc\;k)}$ を求め、結果の型は $M\;n$ であり、これらは β により、二つのゴールの型および $T$ と変換可能である。この構成が正しいのは、名前が新鮮で、レベル $u$ が正しく、他のどの仮定も $n$ に言及しないときに限る。

• motive が $n$ ではなく新鮮な名前 $z$ を束縛するのは、$n$ がすでに $\Gamma$ にあり、$\tLam{n}{\Nat}{T}$ と書くとそれをシャドーイングしてしまい、第 11 章の落とし穴にはまるからである。同様に $k$ と $\mathit{ih}$ も新鮮でなければならない。（本書の実装では、motive の変数を ind_x、n が使われているときの後者の構成子のフィールドを k、仮定を ih と名付ける。）
• motive のレベル $u$ はゴールの型から来るもので、$\InferSort$ で求める。命題なら $0$ であり、$\NatRec{0}$ が帰納法である。
• 他の仮定が $n$ に言及しているとき、たとえば $h : n = 2$ があるとき、新しいゴールには元の $n$ についての $h$ が残ったままで、$\mathit{ih}$ はそれについて何も言わず、ゴールは正しいが証明できないかもしれない。Lean の induction はそのような仮定をまずゴールの中に戻し（リバートし）、motive の一部にする一方、本書の実装では、後続の仮定が $n$ に言及しないことを要求し、そうでなければ「induction: revert dependent hypotheses first」と報告する。

この実装は $\Nat$ に固有のものではなく、添字を持たない任意の帰納型で動く。シグネチャから再帰子の型を読み、構成子ごとに小前提を一つずつ剥がし、それぞれを、構成子のフィールドと帰納法の仮定を文脈に持つゴールに変える。スクリプト examples/generic-list.leanmini は、ユーザーが宣言したリスト型に対してこれを使う。

書き換え

$h : \Eq{u}\;A\;a\;b$ とし、ゴール $T$ を命題とする。タクティク rw h は、ゴールの中の $a$ を $b$ に三段階で置き換える。

1. 抽象化。 新鮮な $x$ を選び、$T$ の中の $a$ のすべての出現を $x$ で置き換えたものを $C$ とする。出現は変換ではなく α 同値までで探す。$a$ の自由変数を束縛する束縛子の下にある出現は、そこでは別のものを指すので飛ばす。
2. motive の検査。 $\Gamma, x : A \vdash C : \Sort{0}$ を検査する。これは後述のとおり失敗しうる。
3. 項の構築。 新しいゴールは $\subst{C}{x}{b}$、つまり $a$ を $b$ に置き換えたゴールである。
   $$\goal{\Gamma}{\hole{m}}{T} \;\leadsto\; \goal{\Gamma}{\hole{1}}{\subst{C}{x}{b}}, \qquad \hole{m} \mathrel{:=} \EqRec{u,0}\;A\;a\;(\tLam{x}{A}{C \to T})\;(\tLam{p}{T}{p})\;b\;h\;\hole{1}.$$

この割り当てが型 $T$ を持つことを見るために、motive を $N = \tLam{x}{A}{C \to T}$ と書く。$\subst{C}{x}{a} = T$ なので、項 $N\;a$ は $T \to T$ と変換可能で、恒等関数 $\tLam{p}{T}{p}$ がその型を持つ。$h$ に沿って輸送すると $N\;b$ が得られ、これは $\subst{C}{x}{b} \to T$ と変換可能であり、それを $\hole{1}$ に適用すれば $T$ になる。Lean は同じ発想から Eq.mpr (congrArg (fun x => C) h) という別の項を組み立て、さらに新しいゴールを rfl で閉じることも試みるが、本書の実装ではそれを明示的な rfl に任せ、二つの段階がスクリプト上で見えるようにしている。

motive の型が正しくないとき。 $a$ を抽象化するとゴールが壊れることがある。$\Gamma = n : \Nat,\; h : n = 2,\; q : n = 0$ とし、証明 $q$ についての主張であるゴール $\Eq{0}\;(n = 0)\;q\;q$ に rw h を実行したとしよう。$n$ を抽象化すると $C = \Eq{0}\;(x = 0)\;q\;q$ となるが、$q$ の型は $n = 0$ であって $x = 0$ ではなく、$q$ 自身は抽象化できないので、これは型が正しくない。段階 2 が失敗し、Lean も同じ状況を「motive is not type correct」と報告する。段階 2 がなければ、タクティクはカーネルに拒否される項を生成し、それは健全性には無害だが、ユーザーの役には立たない。

例: タクティクによる 0 + n = n

本書の体系では、第 9 章の証明は次のスクリプトになり、これは examples/zero-add.leanmini に $\add$ の定義を含めたものである（スクリプトでは $0 + n$ を add Nat.zero 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
goal forall (n : Nat), Eq Nat (add Nat.zero n) n
intro n
induction n
rfl
change Eq Nat (Nat.succ (add Nat.zero k)) (Nat.succ k)
rw ih
rfl
qed

部分項が育っていく様子を見てほしい。induction n が二つのホールを持つ $\NatRec{0}$ を挿入し、rfl が最初のホールを埋め、change は項には触れずゴールだけを書き換え、rw ih が輸送を挿入して最後の rfl のためのホールを一つ残す。change の行を消してスクリプトを適用すると、rw が左辺を見つけられずに失敗するのが分かる。

# 第二引数に関する再帰による加法:
#   add m zero     = m
#   add m (succ k) = succ (add m k)
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

# add zero n = n は定義的ではないので、n に関する帰納法が要る。
goal forall (n : Nat), Eq Nat (add Nat.zero n) n
intro n
induction n
# 基底ケース: add zero zero は zero に簡約される。
rfl
# ステップケース: add zero (succ k) を succ (add zero k) に展開し、ih を使う。
change Eq Nat (Nat.succ (add Nat.zero k)) (Nat.succ k)
rw ih
rfl
qed

この項は、第 9 章で手書きしたものと二箇所で異なる。intro のために $\tLam{n}{\Nat}{\ldots\;n}$ で始まることと、ステップが rw の組み立てた motive を使うことである。どちらも同じ命題の証明であり、カーネルはどちらを受け取っても構わない。プレイグラウンドで change の行を消し、rw が出すエラーを読んでみてほしい。

なぜタクティクを信頼する必要がないのか

カーネルが最終的な項を検査するので、体系が健全であるためにタクティクが正しい必要はない。バグのあるタクティクは、失敗するか、型の正しくない項を生成してカーネルに拒否されるかのどちらかであり、偽の定理をカーネルに受理させることはできない。exact の $\Check$ や rw の motive の検査など、タクティク自身が行う検査は、エラーを早く分かりやすく報告するためにあるにすぎない。

したがって体系の信頼すべき部分は小さく、アルゴリズム 5.1、第 III 部の簡約関数と比較関数、そして第 8 章のシグネチャ構築手続きであり、src/proof.rs と src/syntax.rs の中身はすべてその外側にある。

Lean のタクティク基盤は、ここで素描したものよりはるかに豊かで、単一化で解かれるメタ変数、暗黙の引数を補い 0 + n のような記法を展開するエラボレータ、依存する仮定をリバートし添字付きの族も扱う induction、そして simp のような自動化がある。これらはすべて信頼されない側にあり、Lean のカーネルも本書のものと同じく、完成した項しか見ない [de Moura and Ullrich 2021]。

演習