logic チュートリアル

このチュートリアルでは、logic パッケージを使って命題論理の定理を前向きに証明する。結合子をインストールし、論理式を構築し、自然演繹の規則を組み合わせて連言の可換性のような証明を作る。各ステップはカーネルの定理を返すため、ここで構築するものは、tactics 層が証明スクリプトの裏で構築するものとまったく同じである。

クイックスタート

moon.pkg でカーネルと logic パッケージをインポートする。

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

命題論理のプレリュードをカーネル状態にインストールし、 $\vdash \top$ を証明する。

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let th = @logic.logic_prop_truth_const_thm(st, pre).unwrap()
  inspect(@kernel.thm_to_string(th), content="[] |- Const(T#1 : bool)")
}

#1 は定数 T の同一性であり、プレリュードが最初に宣言する定数である。install_prop_prelude は T、F、and、imp、not、or をカーネルの定義ゲートを通じて定義する。default_prop_prelude() はそれらの名前の記録であり、パッケージのすべての関数がこれを受け取る。

日常的な作業

論理式を構築する

結合子のビルダーは命題を受け取って項を返す。引数が型 bool であることを検査する。

test "formulas" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let q = @kernel.mk_var("q", @kernel.bool_ty())
  let p_and_q = @logic.prop_mk_and(st, pre, p, q).unwrap()
  let p_or_q = @logic.prop_mk_or(st, pre, p, q).unwrap()
  // the destructors recover the parts
  let (l, r) = @logic.prop_dest_and(st, pre, p_and_q).unwrap()
  inspect(@kernel.term_to_string(l) + ", " + @kernel.term_to_string(r), content="Var(p : bool), Var(q : bool)")
  inspect(@logic.prop_dest_or(st, pre, p_or_q) is Some(_), content="true")
  // a disjunction is not a conjunction
  inspect(@logic.prop_dest_and(st, pre, p_or_q) is None, content="true")
}

各結合子は等号まで展開された定義であるため、項は大きくなる。出力するのではなく、term_alpha_eq で比較し、prop_dest_* 関数で分解すること。

連言の可換性を証明する

$p \wedge q$ を仮定し、分解し、逆順に組み立て直して、仮定を解消する。

test "and commutes" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let q = @kernel.mk_var("q", @kernel.bool_ty())
  let p_and_q = @logic.prop_mk_and(st, pre, p, q).unwrap()
  let h = @logic.logic_assume(st, p_and_q).unwrap() // {p ∧ q} |- p ∧ q
  let th_p = @logic.logic_prop_and_elim_l_thm(st, pre, h).unwrap() // {p ∧ q} |- p
  let th_q = @logic.logic_prop_and_elim_r_thm(st, pre, h).unwrap() // {p ∧ q} |- q
  let th_qp = @logic.logic_prop_and_intro_thm(st, pre, th_q, th_p).unwrap() // {p ∧ q} |- q ∧ p
  let th = @logic.logic_prop_imp_intro_thm(st, pre, p_and_q, th_qp).unwrap() // |- p ∧ q -> q ∧ p
  inspect(@kernel.thm_hyp_count(th), content="0")
  let goal = @logic.prop_mk_imp(st, pre, p_and_q, @logic.prop_mk_and(st, pre, q, p).unwrap()).unwrap()
  inspect(@kernel.term_alpha_eq(@kernel.thm_concl(th).unwrap(), goal), content="true")
}

これは prover チュートリアルのスクリプト and_comm が証明する定理であり、tactic 層は同じ呼び出しを行う。

含意を連鎖させる

モーダスポネンスは logic_prop_imp_elim_thm である。 $p \Rightarrow q$ 、 $q \Rightarrow r$ 、 $p$ から $r$ を導出する。

test "chain" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let r = @kernel.mk_var("r", bool)
  let pq = @logic.logic_assume(st, @logic.prop_mk_imp(st, pre, p, q).unwrap()).unwrap()
  let qr = @logic.logic_assume(st, @logic.prop_mk_imp(st, pre, q, r).unwrap()).unwrap()
  let th_p = @logic.logic_assume(st, p).unwrap()
  let th_q = @logic.logic_prop_imp_elim_thm(st, pre, pq, th_p).unwrap()
  let th_r = @logic.logic_prop_imp_elim_thm(st, pre, qr, th_q).unwrap()
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_r).unwrap()), content="Var(r : bool)")
  inspect(@kernel.thm_hyp_count(th_r), content="3")
  // modus ponens needs the antecedent, not some other fact
  inspect(@logic.logic_prop_imp_elim_thm(st, pre, qr, th_p) is Err(_), content="true")
}

否定と偽を使う

$\neg p$ は $p \Rightarrow \bot$ であるため、 $p$ の証明と $\neg p$ の証明から $\bot$ が得られ、 $\bot$ からは何でも導かれる。

test "contradiction" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let goal = @kernel.mk_var("anything", bool)
  let th_p = @logic.logic_assume(st, p).unwrap()
  let th_np = @logic.logic_assume(st, @logic.prop_mk_not(st, pre, p).unwrap()).unwrap()
  let th_f = @logic.logic_prop_not_elim(st, pre, th_np, th_p).unwrap()
  let th = @logic.logic_prop_ex_falso_thm(st, pre, th_f, goal).unwrap()
  inspect(@kernel.term_to_string(@kernel.thm_concl(th).unwrap()), content="Var(anything : bool)")
}

カタログ名を調べる

証明スクリプトは定理を名前で引用する。どの名前が存在し、どのモードで使えるかはカタログが示す。

test "catalog" {
  let names = []
  for i in 0..<@logic.logic_prop_theorem_count() {
    let e = @logic.logic_prop_theorem_at(i).unwrap()
    if e.apply_class is Some(_) {
      names.push(e.name)
    }
  }
  // the names `apply` accepts
  inspect(names.join(" "), content="and_elim_l and_elim_r or_intro_l or_intro_r eq_sym")
}

さらに進む

定理をゴールに合わせる。 後ろ向き証明には、仮定がゴールの仮定とちょうど一致する定理が必要である。logic_prop_ensure_sequent(state, hyps, concl, th) は結論を検査し、th をちょうど hyps まで弱化する。th がゴールの提供しないものに依存していれば失敗する。tactics 層はゴールを閉じるたびにこれを呼ぶ。

正規化する。 結合子定数を展開すると β-redex が残る。logic_normalize_prop_beta はそれをカーネルのステップで簡約する。

test "unfold and normalise" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let not_c = @kernel.ks_mk_const(st, "not").unwrap()
  let th = @logic.logic_assume(st, @kernel.mk_comb(not_c, p)).unwrap() // {not p} |- not p
  let unfolded = @logic.logic_prop_unfold_not(st, pre, th).unwrap() // {not p} |- ¬p
  let concl = @kernel.thm_concl(unfolded).unwrap()
  inspect(@kernel.term_alpha_eq(concl, @logic.prop_mk_not(st, pre, p).unwrap()), content="true")
}

理論を拡張する。 拡張ラッパー（logic_specify_const、logic_register_typedef）は、この層に属する名前で提供されたカーネルのゲートである。上位層はこれらを呼ぶことで、カーネルのゲート関数を直接インポートせずに済む。

欠けている規則に注意する。 選言除去は存在しない。その理由は logic 設計が説明している。選言は logic_prop_or_intro_l_thm か logic_prop_or_intro_r_thm で証明し、選言による場合分けを必要とする設計は避けること。

よくある落とし穴

プレリュードを忘れる。 ビルダーはどの状態でも動作するが、logic_prop_truth_const_thm、logic_prop_def_* 関数、および結合子定数の認識には、先に install_prop_prelude が必要である。
結合子の名前を横取りする。 正規の定義なしにすでに and を宣言している状態にはプレリュードを入れられない。install_prop_prelude はそれを拒否する。
存在しない仮定を解消する。 logic_prop_imp_intro_thm(state, pre, p, th) は、p が th の仮定に含まれていることを必要とする。空虚な含意が欲しい場合は、先に logic_add_assum で弱化すること。
二項結合子を展開した後に基本形を期待する。 logic_prop_unfold_and、_imp、_or は $(\lambda p\,q.\,\dots)\,a\,b$ を簡約せずに残す。logic_normalize_prop_beta を呼ぶこと。
エラーコンストラクタを字面どおりに読む。 補助関数の失敗は TypeMismatch のような汎用のカーネルエラーで報告される。補助関数が失敗したら、前提の形を確認すること。

次のステップ

logic API には、リプレイ補助関数を含むすべての関数が列挙されている。
logic 設計は、各規則をカーネル規則から導出する。
tactics チュートリアルは、これらの規則をゴールから後ろ向きに使う。