tactics 設計

tactics パッケージは、ユーザーがゴールを後ろ向きに、より単純なゴールへ還元して証明できるようにするが、すべての定理は依然としてカーネルによって前向きに構築される。このページでは、定理変換器としてのタクティクの LCF 的な見方、QED が各ステップの前向き部分をクロージャではなくデータとして記録する方法、そして誤ったタクティクが証明を失敗させることはあっても誤って成功させることは決してない理由を説明する。

設計目標

意味が自然演繹と一致する、ゴール指向のステップ(intro、split、left、right、apply、exact、assumption)を提供する。
ユーザーが述べたゴールそのものに対するカーネルの Thm を生成するか、理由と失敗したゴールの位置とともに失敗する。
権限を持たない。このパッケージは定理を構築するために logic とカーネルの関数を呼び出すだけである。

数学的背景

定理変換器としてのタクティク

LCF では、ゴールはまだ証明すべきシーケント $\Gamma \vdash c$ であり、タクティクは関数である

\mathsf{tac} : \mathit{goal} \to \mathit{goal}^{*} \times (\mathit{thm}^{*} \to \mathit{thm})

それはサブゴール $g_1, \dots, g_n$ と正当化 $j$ を返す。タクティクが有効であるとは、 $g_1, \dots, g_n$ を証明する定理 $t_1, \dots, t_n$ に対して、定理 $j(t_1, \dots, t_n)$ が元のゴールを証明することである。¹1 M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF, LNCS 78, 1979. シーケント $\Gamma' \vdash c'$ がゴール $\Gamma \vdash c$ を証明するとは、 $c' \equiv_\alpha c$ かつ $\Gamma' \subseteq \Gamma$ であることをいう。証明の実行とは、ゴールが残らなくなるまでタクティクを適用し、葉を閉じる定理から出発して、正当化を下から上へ合成することである。

重要な性質は、有効性が正しさの問題であって健全性の問題ではないことである。正当化はカーネル規則を呼び出すことによってのみ定理を構築できる。タクティクが無効なら、その正当化は別のゴールの定理を生成するか失敗するかであり、偽の定理を生成することはできない。したがって LCF は有効性を最後に検査し、QED も同じことを行う。

QED のステップの正当化

以下の各ステップは有効なタクティクであり、正当化は右の列のカーネル導出である。

ステップ	ゴール	サブゴール	正当化
`intro h`	$\Gamma \vdash a \Rightarrow b$	$\Gamma, a \vdash b$	$t \mapsto$ $t$ から $a$ を解消する(含意導入)
`split`	$\Gamma \vdash a \wedge b$	$\Gamma \vdash a$ , $\Gamma \vdash b$	$(t_1, t_2) \mapsto$ 連言導入
`left`	$\Gamma \vdash a \vee b$	$\Gamma \vdash a$	$t \mapsto$ 左側での選言導入
`right`	$\Gamma \vdash a \vee b$	$\Gamma \vdash b$	$t \mapsto$ 右側での選言導入
`apply h`, $h : a \Rightarrow b \in \Gamma$	$\Gamma \vdash b$	$\Gamma \vdash a$	$t \mapsto$ $\{a \Rightarrow b\} \vdash a \Rightarrow b$ との modus ponens
`exact h`, `assumption`	$\Gamma \vdash c$ , $c \in \Gamma$	なし	ASSUME $c$ を $\Gamma$ に弱化したもの
`exact n`	$\Gamma \vdash c$	なし	$n$ に対するカタログの定理を $\Gamma$ に弱化したもの

各行の有効性は、logic 設計で導出した対応する自然演繹の規則である。含意に対する intro では、サブゴールは仮定の中に $a$ を持つので、含意導入がそれを解消でき、結果の仮定は再び $\Gamma$ となる。

intro x は、HOL における $\forall y.\,P$ のエンコーディングである $(\lambda y.\,P) = (\lambda y.\,\top)$ の形のゴールにも適用される。サブゴールは新しい変数 $x'$ に対する $\Gamma \vdash P[x'/y]$ であり、正当化は次のとおりである。

\frac{\dfrac{\Gamma \vdash P \qquad \vdash \top}{\Gamma \vdash P = \top}\;\textsf{DEDUCT\_ANTISYM\_RULE}}{\Gamma \vdash (\lambda x'.\,P) = (\lambda x'.\,\top)}\;\textsf{ABS}

ここで ABS は $x' \notin \mathrm{FV}(\Gamma)$ を必要とする。そのため、リプレイの束縛変数は、ゴール、そのローカル、その仮定に対して新しいものが選ばれる。

設計判断

データとしての正当化

問題。 LCF は正当化をクロージャとして表現する。クロージャは検査できないので、証明のどこで失敗したかを報告できず、構築された文脈全体を捕捉してしまう。

選択。 保留中のゴールは、正当化をデータとして持つ。含意の接頭辞(解消すべき仮定)、PendingRefine の値の精緻化チェーン(取り消すべき後ろ向きの apply と量化子のステップ)、SplitRole(連言の左半分か右半分か)、OrContext(選言のどちら側が選ばれたか)である。ゴールが閉じると、finish_goal_evidence がこのデータを解釈する。精緻化チェーンをリプレイし、次に選言を包み、連言の半分を併合し、含意の接頭辞を解消し、最後に量化子のステップを取り消す。

理由。 このデータはクロージャの脱関数化された形である。各コンストラクタは上の表の 1 つの正当化に対応し、インタプリタがそれらを適用する。診断のために検査でき、不変であり、2 つの証明状態が構造を安全に共有できる。

閉じるたびにリプレイし、ルートで検査する

問題。 前向きのリプレイをまさに最後まで待つと、証明の早い段階での無効なステップは ps_qed で初めて報告され、原因から遠く離れてしまう。

選択。 証拠は、ゴールが閉じた時点で直ちにリプレイされる。split の前半は、その定理を後半の SplitRole に保存し、後半が閉じたときに両者が併合される。最後のゴールが閉じると、定理がルートのゴールと比較される。β 正規化の後、その仮定はルートの仮定と一対一で一致し、その結論はルートの結論に等しくなければならない。いずれも α 同値を除く。その場合にのみ最終定理として保存される。

理由。 失敗はそれを引き起こしたステップで現れる。最後の比較はまさに LCF の有効性検査であり、すべてのステップが有効なら常に成功し、そうでないステップがあれば、ユーザーは誤った主張の定理ではなく ProofSynthesisUnavailable を得る。

2 つの名前空間、1 つの順序

exact n と apply n は、n をまず intro が導入したローカルの中から、次に logic パッケージのカタログ名の中から探す。ローカルは常に優先され、カタログ名にフォールバックすることはない。そのため truth という名前のローカルが定理 truth と取り違えられることはない。カタログはステップのモードで参照される。exact はゴールを直接閉じられる名前のみを、apply は含意である名前のみを使う。誤ったモードで使われた名前は、未知の名前ではなく不一致として報告される。

hole ステップは無い

穴のある証明は証明ではない。tactics 層にはゴールを開いたままにするステップが無いので、完了したふりをする状態を生成できない。hole はフロントエンドの概念である。prover は hole で停止し、その時点のゴールとともに未完了の証明を報告する。

正しさと不変条件

健全性。 すべての定理は logic とカーネルの関数で構築される。tactics 層は Thm を構築できない。ここにバグがあっても、証明は失敗するか誤ったエラーを報告するだけで、偽の定理で成功することはない。
ルートへの忠実性。 証明状態が最終定理を持つのは、その定理が、β 正規形と α 同値を除いて、ちょうどルートの仮定のもとでルートのゴールを証明する場合に限る。
ゴールの順序。 新しいサブゴールは、残りのゴールの前に順番に置かれる。Split が左半分の定理を右半分に保存することと合わせて、これにより prover の分岐ブロックが依拠する左から右への評価が実現する。
分岐パス。 各保留中のゴールは、ルートからの選択のパスを記録する。Split は 1 または 2 を追加し、Left と Right は 1 を追加する。prover と CLI は失敗時にこのパスを出力する。
永続性。 ps_apply は引数を決して変更しない。失敗したステップの後も、以前の状態を使い続けられる。

却下した代替案

正当化にクロージャを使う。 書くのは簡単だが、診断には不透明で、テストもしにくい。
定理を ps_qed でのみ構築する。 カーネル呼び出しは減るが、エラーが原因から遠く離れて現れる。
exact から apply への暗黙のフォールバック。 名前が含意であるとき exact が黙って後ろ向きのステップを始めるようにすると、スクリプトは読みにくく、エラーの位置は特定しにくくなる。モードは別々である。
メタ変数。 Isabelle や Lean のように、ゴールの一部を後で埋めるために残しておくには、単一化と、カーネル内の不完全な定理の概念が必要になる。同梱サブセットはそれを必要としない。

境界

命題のステップのみ、および全称量化子の HOL エンコーディングに対する intro。書き換えも、選言の場合分けも、帰納法も無い。
証明探索は無く、すべてのステップはユーザーが与える。assumption と apply imp_elim は現在の仮定のみを探索する。
解析も分岐ブロックのスケジュールも行わない。どちらも prover が行う。
hole も部分的な定理も無い。

M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF, LNCS 78, 1979. シーケント $\Gamma' \vdash c'$ がゴール $\Gamma \vdash c$ を証明するとは、 $c' \equiv_\alpha c$ かつ $\Gamma' \subseteq \Gamma$ であることをいう。 ↩