tactics チュートリアル

このチュートリアルでは、tactics パッケージで証明状態を手で動かす。ゴールを述べ、ステップを一つずつ適用し、その合間に保留中のゴールを確認し、最後にカーネルの定理を受け取る。これは prover が各証明スクリプトに対して行うことから、パースとスケジューリングを除いたものである。

クイックスタート

moon.pkg でパッケージをインポートする。

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/logic",
  "Luna-Flow/QED/parser",
  "Luna-Flow/QED/tactics",
}

intro と exact で $\vdash p \Rightarrow p$ を証明する。

fn goal_of(st : @kernel.KernelState, locals : Array[String], src : String) -> @tactics.Goal {
  let mut env = @parser.empty_parse_env()
  for name in locals {
    env = @parser.parse_env_push_local(env, name, @kernel.bool_ty())
  }
  let g = @parser.parse_goal_with_env(st, env, src).unwrap()
  @tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g))
}

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p"], "⊢ p -> p"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_exact("h")).unwrap()
  let th = @tactics.ps_qed(ps).unwrap()
  inspect(@kernel.thm_hyp_count(th), content="0")
}

goal_of はこのページ全体で使う小さな補助関数で、ブール型のローカルを宣言してゴールをパースする。各ステップはカーネル規則を呼ぶ可能性があるため、カーネル状態とプレリュードを受け取る。

日常的な作業

ゴールの変化を観察する

各ステップの後、ps_current_goal と ps_current_local_hyps が残りを示す。

test "watch" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["x"], "⊢ x -> x ∧ x"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // the goal is now  x ⊢ x ∧ x  with the local h : x
  let g = @tactics.ps_current_goal(ps).unwrap()
  inspect(@tactics.goal_hyp_count(g), content="1")
  assert_eq(@tactics.ps_current_local_hyps(ps).map(@tactics.local_hyp_name), ["h"])
  // split leaves two goals, x and x, on branches 1 and 2
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_split()).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="2")
  assert_eq(@tactics.ps_current_branch_path(ps), [1])
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_exact("h"), @tactics.step_exact("h")]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

これは examples/demo_and.qed のスクリプト demo_and をステップごとに追ったものである。

カタログの定理を使う

exact と apply は、logic パッケージのカタログにある定理名も受け付ける。連言の可換性の証明では、文脈にある連言を使う。

test "and_comm" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "⊢ p ∧ q -> q ∧ p"))
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_intro("h"),
    @tactics.step_split(),
    @tactics.step_exact("and_elim_r"), // q, from p ∧ q in context
    @tactics.step_exact("and_elim_l"), // p, from p ∧ q in context
  ]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

`apply` で後ろ向きに進む

apply は、含意 $a \Rightarrow b$ が利用できるとき、ゴール $b$ を $a$ に置き換える。次はコーパスのケース t2、 $\vdash p \wedge q \Rightarrow p$ である。

test "apply" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "⊢ p ∧ q -> p"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // and_elim_l as an implication: from p ∧ q infer p, so the goal becomes p ∧ q
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_apply("and_elim_l")).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="1")
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_exact("h")).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

選言の一方を選ぶ

left と right は一方の側に確定する。次はコーパスのケース t4、 $p \vdash p \vee q$ である。

test "left" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "p ⊢ p ∨ q"))
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_left(), @tactics.step_assumption()]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
  // choosing the wrong side leaves a goal that cannot be closed
  let wrong = @tactics.ps_apply(st, pre, @tactics.ps_init(goal_of(st, ["p", "q"], "p ⊢ p ∨ q")), @tactics.step_right()).unwrap()
  let stuck = @tactics.ps_apply(st, pre, wrong, @tactics.step_assumption())
  inspect(stuck is Err(@tactics.GoalShapeMismatch(_)), content="true")
}

エラーを読む

合わないステップは理由を伴って失敗する。直前の状態は変わらず、再び使える。

test "errors" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_apply(st, pre, @tactics.ps_init(goal_of(st, ["x"], "⊢ x -> x ∨ x")), @tactics.step_intro("h")).unwrap()
  let ps_left = @tactics.ps_apply(st, pre, ps, @tactics.step_left()).unwrap()
  // `truth` proves T, not x
  match @tactics.ps_apply(st, pre, ps_left, @tactics.step_exact("truth")) {
    Err(@tactics.GoalShapeMismatch(msg)) => inspect(msg, content="exact witness does not directly close current goal")
    _ => fail("expected a goal-shape mismatch")
  }
  // `or_intro_l` cannot be used with exact, only with apply
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_exact("or_intro_l")) is Err(@tactics.GoalShapeMismatch(_)), content="true")
  inspect(@tactics.ps_qed(ps) is Err(@tactics.UnsolvedGoals), content="true")
}

最初の失敗はユーザーマニュアルの bad_branch の例であり、prover はこれをステップ番号と分岐パスとともに報告する。

さらに進む

自分の定理でゴールを閉じる。 ps_close_current_with_th(state, pre, ps, th) は、たとえば logic パッケージなど別の場所で構築した定理で現在のゴールを閉じる。定理がゴールに合うことは検査される。

一つの分岐を切り離して扱う。 ps_isolate_pending_at(ps, i) は、保留中のゴール i のための新しい証明状態を作る。prover はこれを使って { ... } 分岐ブロックを単独で実行するため、ある分岐の内側の失敗はその分岐に対してのみ報告される。

量化されたゴールを証明する。 HOL における $\forall x.\,P$ の符号化、すなわち $(\lambda x.\,P) = (\lambda x.\,\top)$ の形のゴールに対しては、intro x が量化子を外し、リプレイが ABS でそれを再構築する。スクリプトで forall を使って書かれたゴールは、自由変数として別の扱いを受ける。parser 設計を参照。

prover に任せる。 prover チュートリアルは、同じステップをテキストのスクリプトから実行し、構造化された診断と未完了の証明を加える。

よくある落とし穴

プレリュードを忘れる。 T、F、またはカタログ名を含むゴールには、各ステップに渡す状態に install_prop_prelude が必要である。
exact で後ろ向きのステップを始められると思い込む。 exact はゴールを閉じるか、失敗するかのどちらかである。or_intro_l のような含意には apply を使うこと。
シャドーイングされたローカル。 カタログの定理と同じ名前のローカルはその定理を隠す。intro truth の後では、exact truth はローカルを指す。
場合分け。 仮定にある選言を使うステップは存在しない。その理由は logic 設計が説明している。
ps_qed が再検査すると思い込む。 ルートの検査は最後のゴールが閉じたときに実行される。ps_qed は結果か UnsolvedGoals を報告するだけである。

次のステップ

tactics API には、すべての関数とリプレイコンテキストの型が列挙されている。
tactics 設計は、正当化と、不正なステップが偽の定理を生成しえない理由を説明する。
prover チュートリアルは、同じ証明をスクリプトから実行する。