prover チュートリアル

このチュートリアルでは、prover パッケージで MoonBit から定理スクリプトを実行し、3 種類の結果、すなわち証明された定理、構造化された失敗、未完了の証明を読む。スクリプトはすべて examples/ と回帰コーパスから取ったものなので、示す出力はテストが検査するものと同じである。

クイックスタート

moon.pkg でカーネルと prover をインポートする。

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

最小のスクリプト examples/truth_file.qed を実行する。

test "quick start" {
  let st = @kernel.empty_kernel_state()
  let src = "theorem truth_file : ⊢ T := by exact truth"
  match @prover.prove_theorem_script_detailed(st, src, @prover.default_prover_options()) {
    Proved(ok) => {
      inspect(ok.theorem_name, content="truth_file")
      inspect(@kernel.thm_hyp_count(ok.thm), content="0")
    }
    _ => fail("expected a proof")
  }
}

default_prover_options() は命題論理のプレリュードをインストールするため、空の状態で T とカタログ定理 truth が使える。結果の thm はカーネルの定理である。

日常的な作業

束縛子と分岐ブロックを使って証明する

ヘッダの束縛子はゴールのローカルを宣言する。split の後の分岐ブロックは、それぞれの半分を別々に証明する。次は examples/and_comm.qed である。

test "and_comm" {
  let src =
    #|theorem and_comm (p : bool) (q : bool) : ⊢ p ∧ q -> q ∧ p := by
    #|  intro h
    #|  split { exact and_elim_r } { exact and_elim_l }
  let r = @prover.prove_theorem_script(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Ok((_, th)) else { fail("expected a proof") }
  inspect(@kernel.thm_hyp_count(th), content="0")
}

prove_theorem_script は Ok((state, thm)) またはエラーを返す。定理だけに関心のある呼び出し側向けである。

失敗の位置を特定する

ステップが失敗すると、結果はどのステップが、どの分岐で、どのゴールとローカルのもとで失敗したかを示す。次は examples/bad_branch.qed である。

test "failure" {
  let src =
    #|theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
    #|  intro h
    #|  left { exact truth }
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Failed(f) else { fail("expected a failure") }
  inspect(f.kind is Tactic, content="true")
  inspect(f.detail, content="GoalShapeMismatch(exact witness does not directly close current goal)")
  assert_eq(f.step_index, Some(3))
  assert_eq(f.branch_path, [1])
  assert_eq(f.step_src, Some("exact truth"))
  assert_eq(f.local_hyps.map(h => h.name), ["h"])
}

ステップ 3 は（intro h と left の後の）exact truth であり、left ブロックの分岐 1 にある。その時点のゴールは x であり、truth はこれを証明しない。

未完了の証明を報告する

hole は証明の欠落箇所を示す。prover はそこで止まり、hole が表すゴールを報告する。定理は生成されない。次は examples/unfinished_branch.qed である。

test "unfinished" {
  let src =
    #|theorem unfinished_branch (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by
    #|  intro h
    #|  right { right { hole h1 } }
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Unfinished(u) else { fail("expected an unfinished proof") }
  assert_eq(u.hole_name, Some("h1"))
  assert_eq(u.branch_path, [1, 1])
  inspect(u.detail, content="proof contains an unfinished hole")
  inspect(@tactics.goal_hyp_count(u.current_goal), content="1")
}

current_goal は $x \vdash x$ である。hole を exact h で埋めれば証明は完了する。

ファイル全体を検査する

prove_theorem_file_results_detailed はファイルのすべての定理を検査し、失敗や hole の後も続行する。次は examples/multi_with_hole.qed である。

test "file" {
  let src =
    #|theorem before_hole : ⊢ T := by exact truth
    #|qed
    #|
    #|theorem unfinished_demo (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by
    #|  intro h
    #|  right { right { hole h1 } }
    #|qed
    #|
    #|theorem after_hole : ⊢ T := by exact truth
    #|qed
  let r = @prover.prove_theorem_file_results_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is FileChecked(report) else { fail("expected a report") }
  let names = report.items.map(item => match item {
    ProverItemProved(ok) => "ok " + ok.theorem_name
    ProverItemFailed(f) => "error " + f.detail
    ProverItemUnfinished(u) => "unfinished " + u.theorem_name
  })
  assert_eq(names, ["ok before_hole", "unfinished unfinished_demo", "ok after_hole"])
}

さらに進む

自分の状態に対して実行する。 @prover.prover_options(false) を渡すとプレリュードを省略し、用意した状態、たとえばカーネルを通じて追加の定数を宣言した状態に対して実行できる。プレリュードがなければ T は未知であり、実行は Sig 診断で失敗する。

test "no prelude" {
  let src = "theorem t : ⊢ T := by exact truth"
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.prover_options(false))
  guard r is Failed(f) else { fail("expected a failure") }
  inspect(f.kind is Sig, content="true")
  inspect(f.detail, content="UnknownConst")
}

コーパスを使う。 positive_corpus_cases() とその仲間の関数は、テストが実行するスクリプトをその期待される結果とともに返す。これらはすぐに使える例の集まりであり、prover の上に構築するものの回帰テストスイートでもある。

結果を描画する。 cmd パッケージは、これらの結果をコマンドラインツールの ok、error[...]、warning[unfinished] 行に変換する。同じテキストが必要なら、その描画関数を再利用すること。

よくある落とし穴

• hole から定理を期待する。 Unfinished の結果には定理がなく、prove_theorem_script はそれをエラーとして返す。
• 前の定理を引用する。 ファイル内で先に証明された定理は後の定理からは使えない。使えるのはカタログ名だけである。
• 定理の間の qed を忘れる。 複数の定理を含むファイルでは、最後のもの以外の各定理の後に qed 行が必要であり、ないとファイルのパースが失敗する。
• ゴール内の自由な名前。 ゴール内の名前は、ヘッダの束縛子、状態の定数、またはプレリュードの T/F でなければならない。変数には (x : bool) のような束縛子を使うこと。
• 項の内側の素の forall。 forall はゴールの先頭でのみ受け付けられる。

次のステップ

• prover API には、すべての結果フィールドとコーパスの型が列挙されている。
• prover 設計は、結果が 3 種類ある理由と、分岐ブロックがどうスケジュールされるかを説明する。
• ユーザーマニュアルにはサポート表とコーパスの例の完全な一覧があり、構文ガイドはスクリプトのリファレンスである。
• cmd チュートリアルは、同じスクリプトをコマンドラインから実行する。