logic API

logic パッケージ (Luna-Flow/QED/logic) は、カーネルの上に置かれた検査済みヘルパ層である。命題結合子をカーネルの定義として定義し、結合子の項を構築・認識し、基本規則から命題規則を導出し、exact と apply が理解する定理名のカタログを保持する。依存先は kernel のみで、自前の権限は持たない。返される定理はすべてカーネル規則によって生成されたものであるため、ここにバグがあっても証明が失敗することはあり得るが、偽の定理が得られることはない。

すべての関数は純粋である。定理を生成する関数は Result[@kernel.Thm, @kernel.LogicError] を返し、何も見つからない可能性のあるヘルパは Option を返す。定義の背後にある論理はlogic の設計で説明しており、ウォークスルーは logic チュートリアルにある。

このページの式では、 $\top$ は定数 T、 $\bot$ は定数 F を表し、 $p \wedge q$ 、 $p \Rightarrow q$ 、 $\neg p$ 、 $p \vee q$ はそれぞれ prop_mk_and、prop_mk_imp、prop_mk_not、prop_mk_or が構築する結合子の項を表す。

プレリュード

`PropPrelude`

PropPrelude は命題プレリュードの定数を名指し、その規則名を列挙する。

pub struct PropPrelude {
  truth_name : String
  false_name : String
  imp_name : String
  not_name : String
  and_name : String
  or_name : String
  rules : Array[PropRule]
}

このパッケージのほとんどの関数は、状態内でどの定数を探すかを知るために PropPrelude を受け取る。

`PropRule`

PropRule は前提の数を伴う、名前付きの命題規則である。

pub struct PropRule {
  name : String
  premise_count : Int
}

`default_prop_prelude`

default_prop_prelude は QED のあらゆる箇所で使われるプレリュードを返す。定数は T、F、imp、not、and、or、規則は imp_intro、imp_elim、and_intro、and_elim_l、and_elim_r、or_intro_l、or_intro_r である。

pub fn default_prop_prelude() -> PropPrelude

`install_prop_prelude`

install_prop_prelude は、DefOK ゲートを通じて 6 個のプレリュード定数をカーネル状態に定義する。

pub fn install_prop_prelude(@kernel.KernelState) -> Result[@kernel.KernelState, @kernel.SigError]

これは冪等である。すでに正準の定義を持つ定数はそのまま保たれる。同名で宣言のみされている、または異なる定義を持つ定数は DefinitionAlreadyExists で拒否され、異なる型を持つものは ConstTypeConflict で拒否される。空の状態では 6 個の DefOK 証明書が追加される。

`prop_prelude_rule_count`、`prop_prelude_rule_at` と `prop_prelude_has_rule`

これらの関数は、プレリュードの規則リストを読み出す。

pub fn prop_prelude_rule_count(PropPrelude) -> Int
pub fn prop_prelude_rule_at(PropPrelude, Int) -> PropRule?
pub fn prop_prelude_has_rule(PropPrelude, String) -> Bool

`prop_truth_name` と `prop_false_name`

これらの関数は、真と偽の定数の名前を返す。

pub fn prop_truth_name(PropPrelude) -> String
pub fn prop_false_name(PropPrelude) -> String

test "prelude" {
  let pre = @logic.default_prop_prelude()
  inspect(@logic.prop_prelude_rule_count(pre), content="7")
  inspect(@logic.prop_prelude_has_rule(pre, "and_intro"), content="true")
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  inspect(@kernel.ks_extension_cert_count(st), content="6")
  // installing again changes nothing
  let st2 = @logic.install_prop_prelude(st).unwrap()
  inspect(@kernel.ks_extension_cert_count(st2), content="6")
  // a placeholder constant named `and` blocks the prelude
  let bool = @kernel.bool_ty()
  let and_ty = @kernel.fun_ty(bool, @kernel.fun_ty(bool, bool))
  let squatted = @kernel.ks_add_const(@kernel.empty_kernel_state(), "and", and_ty).unwrap()
  inspect(@logic.install_prop_prelude(squatted) is Err(_), content="true")
}

結合子の項

`prop_mk_and`、`prop_mk_imp`、`prop_mk_not` と `prop_mk_or`

これらの関数は結合子の項を構築する。返されるのは定数の適用ではなく、定義の右辺を引数に適用した基底形である。

pub fn prop_mk_and(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn prop_mk_imp(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn prop_mk_not(@kernel.KernelState, PropPrelude, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn prop_mk_or(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

形は次のとおりである

\begin{aligned} p \wedge q &:= (\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t) \\ p \Rightarrow q &:= (p \wedge q) = p \\ \neg p &:= p \Rightarrow \bot_0 \\ p \vee q &:= \neg p \Rightarrow q \end{aligned}

ここで $t$ は真の項 $(\lambda x.\,x) = (\lambda x.\,x)$ 、 $\bot_0$ は logic_prop_false_term による偽の項である。引数が命題でない場合は NotBoolTerm、型が不正な場合は TypeMismatch で失敗する。プレリュードがインストールされている必要はない。

`prop_dest_and`、`prop_dest_imp`、`prop_dest_not` と `prop_dest_or`

これらの関数は結合子の項を認識してその引数を返し、認識できなければ None を返す。

pub fn prop_dest_and(@kernel.KernelState, PropPrelude, @kernel.Term) -> (@kernel.Term, @kernel.Term)?
pub fn prop_dest_imp(@kernel.KernelState, PropPrelude, @kernel.Term) -> (@kernel.Term, @kernel.Term)?
pub fn prop_dest_not(@kernel.KernelState, PropPrelude, @kernel.Term) -> @kernel.Term?
pub fn prop_dest_or(@kernel.KernelState, PropPrelude, @kernel.Term) -> (@kernel.Term, @kernel.Term)?

基底形を受理し、さらに、状態がその正準の定義定理を持つ場合にはプレリュード定数の適用も受理する。名前が正しくてもその定義を持たない定数は認識されないため、見せかけの定数が結合子として通ることはない。

`logic_prop_truth_term` と `logic_prop_false_term`

これらの関数は、真と偽の基底項を返す。すなわち $(\lambda x.\,x) = (\lambda x.\,x)$ と $(\lambda p.\,p) = (\lambda p.\,t)$ であり、後者は HOL の符号化における $\forall p.\,p$ である。

pub fn logic_prop_truth_term() -> @kernel.Term
pub fn logic_prop_false_term() -> @kernel.Term

test "connectives" {
  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 imp = @logic.prop_mk_imp(st, pre, p, q).unwrap()
  let (a, b) = @logic.prop_dest_imp(st, pre, imp).unwrap()
  inspect(@kernel.term_to_string(a) + " -> " + @kernel.term_to_string(b), content="Var(p : bool) -> Var(q : bool)")
  // p -> q is the equation (p ∧ q) = p
  let (lhs, _) = @kernel.dest_eq(imp).unwrap()
  inspect(@kernel.term_alpha_eq(lhs, @logic.prop_mk_and(st, pre, p, q).unwrap()), content="true")
  // connectives only take propositions
  let x = @kernel.mk_var("x", @kernel.mk_tyvar("A"))
  inspect(@logic.prop_mk_and(st, pre, p, x) is Err(@kernel.NotBoolTerm), content="true")
}

定義定理

`logic_prop_def_imp`、`logic_prop_def_not`、`logic_prop_def_and` と `logic_prop_def_or`

これらの関数は、状態から結合子定数の定義定理を返す。例えば $\vdash \mathit{and} = \lambda p\,q.\,p \wedge q$ である。

pub fn logic_prop_def_imp(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.SigError]
pub fn logic_prop_def_not(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.SigError]
pub fn logic_prop_def_and(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.SigError]
pub fn logic_prop_def_or(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.SigError]

プレリュードがインストールされていない場合は UnknownConst で失敗する。

`logic_bool_false_def_thm`

logic_bool_false_def_thm は F の定義定理を返す。

pub fn logic_bool_false_def_thm(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.SigError]

`logic_prop_def_lhs` と `logic_prop_def_rhs`

これらの関数は、等式の定理(典型的には定義)の両辺を返す。

pub fn logic_prop_def_lhs(@kernel.Thm) -> Result[@kernel.Term, @kernel.LogicError]
pub fn logic_prop_def_rhs(@kernel.Thm) -> Result[@kernel.Term, @kernel.LogicError]

`logic_prop_unfold_head`

logic_prop_unfold_head(state, th_def, th) は、th の結論の先頭の定数をその定義で置き換える。 $\vdash c = \lambda \bar x.\,b$ と $\Gamma \vdash c\,\bar a$ から $\Gamma \vdash (\lambda \bar x.\,b)\,\bar a$ を導出し、先頭の β 冗長式は logic_beta_normalize_eq によって簡約される。

pub fn logic_prop_unfold_head(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

先頭は定義された定数であり、引数は高々 2 個でなければならない。そうでなければ関数は AlphaMismatch または TypeMismatch で失敗する。簡約されるのは先頭にある冗長式のみである。引数が 1 個なら $(\lambda x.\,b)\,a$ がそのような冗長式であり、結果は $b[a/x]$ となる。引数が 2 個なら先頭は $((\lambda x\,y.\,b)\,a_1)\,a_2$ であり、その関数部は抽象ではないため、結論は簡約されないままとなる。基底形に到達するには logic_normalize_prop_beta を適用する。

`logic_prop_unfold_imp`、`logic_prop_unfold_not`、`logic_prop_unfold_and` と `logic_prop_unfold_or`

これらの関数は、1 つの結合子定数の定義を用いた logic_prop_unfold_head である。logic_prop_unfold_not は $\Gamma \vdash \mathit{not}\,p$ を基底形の $\Gamma \vdash \neg p$ に変える。引数が 2 個の形は、上述の未簡約の適用を返す。

pub fn logic_prop_unfold_imp(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_unfold_not(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_unfold_and(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_unfold_or(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

test "unfold" {
  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)
  // {and p q} |- and p q, with `and` the prelude constant
  let and_c = @kernel.ks_mk_const(st, "and").unwrap()
  let and_pq = @kernel.mk_comb(@kernel.mk_comb(and_c, p), q)
  let th = @logic.logic_assume(st, and_pq).unwrap()
  let unfolded = @logic.logic_prop_unfold_and(st, pre, th).unwrap()
  // the definition is substituted, but (λp q. ...) p q is not yet reduced
  let basis = @logic.prop_mk_and(st, pre, p, q).unwrap()
  inspect(@kernel.term_alpha_eq(@kernel.thm_concl(unfolded).unwrap(), basis), content="false")
  let reduced = @logic.logic_normalize_prop_beta(st, unfolded).unwrap()
  inspect(@kernel.term_alpha_eq(@kernel.thm_concl(reduced).unwrap(), basis), content="true")
}

カーネル規則のラッパ

これらの関数は、対応するカーネル規則をそのまま呼び出す。上位層がステップごとにカーネルへ直接触れずに logic に依存できるようにするために存在する。

`logic_refl`、`logic_assume`、`logic_add_assum` と `logic_trans`

pub fn logic_refl(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_assume(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_add_assum(@kernel.KernelState, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_trans(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

これらは refl_checked、assume_checked、add_assum_checked、trans_checked である。

`logic_mk_comb_rule`、`logic_abs_rule` と `logic_beta_rule`

pub fn logic_mk_comb_rule(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_abs_rule(@kernel.KernelState, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_beta_rule(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

これらは mk_comb_rule_checked、abs_rule_checked、beta_rule_checked である。

`logic_eq_mp` と `logic_deduct_antisym`

pub fn logic_eq_mp(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_deduct_antisym(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

これらは eq_mp_checked と deduct_antisym_rule_checked である。

`logic_inst_type` と `logic_inst`

pub fn logic_inst_type(@kernel.KernelState, Array[(String, @kernel.HolType)], @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_inst(@kernel.KernelState, Array[(@kernel.Term, @kernel.Term)], @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

これらは inst_type と inst_checked である。

拡張のラッパ

これらの関数は、カーネルの拡張ゲートと監査リーダをそのまま呼び出す。

`logic_register_typedef` と `logic_typedef_contract`

pub fn logic_register_typedef(@kernel.KernelState, String, Array[String], String, @kernel.Term, @kernel.Thm) -> Result[@kernel.KernelState, @kernel.SigError]
pub fn logic_typedef_contract(@kernel.KernelState, String) -> Result[(@kernel.Thm, @kernel.Thm, @kernel.Thm), @kernel.SigError]

これらは ks_register_type_definition (TypeDefOK) と ks_typedef_contract である。

`logic_specify_const`

pub fn logic_specify_const(@kernel.KernelState, String, @kernel.HolType, @kernel.Term, @kernel.Thm) -> Result[(@kernel.KernelState, @kernel.Thm), @kernel.SigError]

これは ks_specify_const (SpecOK) である。

`logic_register_ind_infinity_anchor` と `logic_ind_infinity_anchor`

pub fn logic_register_ind_infinity_anchor(@kernel.KernelState, @kernel.Thm) -> Result[@kernel.KernelState, @kernel.SigError]
pub fn logic_ind_infinity_anchor(@kernel.KernelState) -> Result[@kernel.Thm, @kernel.SigError]

これらは ks_register_ind_infinity_axiom と ks_ind_infinity_axiom である。

`logic_extension_cert_count`、`logic_extension_cert_at` と `logic_conservative_replay_ok`

pub fn logic_extension_cert_count(@kernel.KernelState) -> Int
pub fn logic_extension_cert_at(@kernel.KernelState, Int) -> (@kernel.ExtensionGate, Array[String], String)?
pub fn logic_conservative_replay_ok(@kernel.KernelState, @kernel.KernelState, @kernel.Thm) -> Bool

これらは ks_extension_cert_count、ks_extension_cert_at、ks_conservative_replay_ok である。

等式のツール

`logic_eq_sym`

logic_eq_sym は等式の対称性を導出する。 $\Gamma \vdash s = t$ から $\Gamma \vdash t = s$ を証明する。

pub fn logic_eq_sym(@kernel.KernelState, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

導出には REFL、MK_COMB を 2 回、EQ_MP を用いる。カーネルチュートリアルでは同じ規則を段階的に構築している。前提が等式でない場合は NotAnEquality で失敗する。

`logic_eq_mp_bool`

logic_eq_mp_bool は、2 番目の前提が命題であることを明示的に検査する EQ_MP である。

pub fn logic_eq_mp_bool(@kernel.KernelState, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_apply_fun_eq` と `logic_apply_fun_eq2`

これらの関数は、関数等式の両辺を引数に適用する。 $\Gamma \vdash f = g$ から $\Gamma \vdash f\,a = g\,a$ 、または $\Gamma \vdash f\,a\,b = g\,a\,b$ を証明する。

pub fn logic_apply_fun_eq(@kernel.KernelState, @kernel.Thm, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_apply_fun_eq2(@kernel.KernelState, @kernel.Thm, @kernel.Term, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_beta_normalize_eq` と `logic_normalize_prop_beta`

logic_beta_normalize_eq は、等式の右辺が β 冗長式である限り、その先頭の β 冗長式を簡約する。 $\Gamma \vdash s = t$ から $\Gamma \vdash s = t'$ を証明する。logic_normalize_prop_beta は定理の結論をより徹底的に簡約する。(抽象の内側ではなく)適用のスパイン上にある最左最外の冗長式を、最大 512 ステップまで繰り返し簡約し、 $\Gamma \vdash c$ から $\Gamma \vdash c'$ を証明する。

pub fn logic_beta_normalize_eq(@kernel.KernelState, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_normalize_prop_beta(@kernel.KernelState, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

どちらも BETA、MK_COMB、TRANS のステップを連鎖させるため、結果は書き換えられた項ではなくカーネル定理である。

`logic_beta_nf_bool_term` と `logic_beta_nf_bool_term_deep`

これらの関数は、 $\vdash t = t'$ を証明して $t'$ を返すことで、命題の β 正規形を計算する。deep 版は、上限の範囲内で不動点に達するまで繰り返す。

pub fn logic_beta_nf_bool_term(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn logic_beta_nf_bool_term_deep(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

タクティク層はこれらを用いて、完成した定理をそのゴールと β 同値の範囲で比較する。

命題の定理

これらの関数は、カーネル規則と結合子の定義から、命題論理の自然演繹規則を導出する。

`logic_prop_truth_thm` と `logic_prop_truth_const_thm`

logic_prop_truth_thm は REFL によって真の項 $\vdash (\lambda x.\,x) = (\lambda x.\,x)$ を証明する。logic_prop_truth_const_thm は、定数 T の定義を用いて $\vdash \top$ を証明する。

pub fn logic_prop_truth_thm(@kernel.KernelState) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_truth_const_thm(@kernel.KernelState, PropPrelude) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_and_intro_thm`、`logic_prop_and_elim_l_thm` と `logic_prop_and_elim_r_thm`

これらの関数は、連言の導入と除去である。

pub fn logic_prop_and_intro_thm(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_and_elim_l_thm(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_and_elim_r_thm(@kernel.KernelState, PropPrelude, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

\frac{\Gamma \vdash p \quad \Delta \vdash q}{\Gamma \cup \Delta \vdash p \wedge q} \qquad \frac{\Gamma \vdash p \wedge q}{\Gamma \vdash p} \qquad \frac{\Gamma \vdash p \wedge q}{\Gamma \vdash q}

`logic_prop_imp_intro_thm`、`logic_prop_imp_elim_thm` と `logic_prop_imp_refl`

logic_prop_imp_intro_thm(state, pre, p, th) は仮定 p を解消する。logic_prop_imp_elim_thm はモーダスポネンスである。logic_prop_imp_refl は $\vdash p \Rightarrow p$ を証明する。

pub fn logic_prop_imp_intro_thm(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_imp_elim_thm(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_imp_refl(@kernel.KernelState, PropPrelude, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

\frac{\Gamma \vdash q \quad p \in \Gamma}{\Gamma \setminus \{p\} \vdash p \Rightarrow q} \qquad \frac{\Gamma \vdash p \Rightarrow q \quad \Delta \vdash p}{\Gamma \cup \Delta \vdash q} \qquad \frac{}{\vdash p \Rightarrow p}

p が th の仮定でない場合、logic_prop_imp_intro_thm は失敗する。2 番目の定理が前件を証明しない場合、logic_prop_imp_elim_thm は失敗する。

`logic_prop_not_elim` と `logic_prop_ex_falso_thm`

logic_prop_not_elim は、命題とその否定から偽を導く。logic_prop_ex_falso_thm(state, pre, th_false, q) は、偽から任意の命題 q を導く。

pub fn logic_prop_not_elim(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_ex_falso_thm(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

\frac{\Gamma \vdash \neg p \quad \Delta \vdash p}{\Gamma \cup \Delta \vdash \bot_0} \qquad \frac{\Gamma \vdash \bot_0 \quad q : \mathit{bool}}{\Gamma \vdash q}

`logic_prop_or_intro_l_thm` と `logic_prop_or_intro_r_thm`

これらの関数は選言の導入である。logic_prop_or_intro_l_thm(state, pre, th_p, q) は $p$ から $p \vee q$ を証明し、logic_prop_or_intro_r_thm(state, pre, p, th_q) は $q$ から $p \vee q$ を証明する。

pub fn logic_prop_or_intro_l_thm(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_or_intro_r_thm(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

選言の除去は存在しない。 $p \vee q := \neg p \Rightarrow q$ では排中律が必要になるが、プレリュードはそれを導出しないためである。これについてはlogic の設計で説明している。

test "natural deduction" {
  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 th_p = @logic.logic_assume(st, p).unwrap()
  let th_q = @logic.logic_assume(st, q).unwrap()
  // {p, q} |- p ∧ q, then {p, q} |- q
  let th_pq = @logic.logic_prop_and_intro_thm(st, pre, th_p, th_q).unwrap()
  let th_r = @logic.logic_prop_and_elim_r_thm(st, pre, th_pq).unwrap()
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_r).unwrap()), content="Var(q : bool)")
  // discharge p: {q} |- p -> p ∧ q
  let th_imp = @logic.logic_prop_imp_intro_thm(st, pre, p, th_pq).unwrap()
  inspect(@kernel.thm_hyp_count(th_imp), content="1")
  // modus ponens gives back {p, q} |- p ∧ q
  let th_mp = @logic.logic_prop_imp_elim_thm(st, pre, th_imp, th_p).unwrap()
  inspect(@kernel.thm_hyp_count(th_mp), content="2")
  // |- p -> p
  let th_refl = @logic.logic_prop_imp_refl(st, pre, p).unwrap()
  inspect(@kernel.thm_hyp_count(th_refl), content="0")
  // |- T, for the prelude constant T
  let th_t = @logic.logic_prop_truth_const_thm(st, pre).unwrap()
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_t).unwrap()), content="Const(T#1 : bool)")
}

test "negation and disjunction" {
  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 th_p = @logic.logic_assume(st, p).unwrap()
  let th_not_p = @logic.logic_assume(st, @logic.prop_mk_not(st, pre, p).unwrap()).unwrap()
  // {¬p, p} |- ⊥, and from ⊥ anything follows
  let th_false = @logic.logic_prop_not_elim(st, pre, th_not_p, th_p).unwrap()
  let th_q = @logic.logic_prop_ex_falso_thm(st, pre, th_false, q).unwrap()
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_q).unwrap()), content="Var(q : bool)")
  // {p} |- p ∨ q
  let th_or = @logic.logic_prop_or_intro_l_thm(st, pre, th_p, q).unwrap()
  inspect(
    @kernel.term_alpha_eq(@kernel.thm_concl(th_or).unwrap(), @logic.prop_mk_or(st, pre, p, q).unwrap()),
    content="true",
  )
}

リプレイヘルパ

タクティク層は、カーネルのステップをリプレイすることでゴールを閉じる。これらのヘルパは、定理をゴールのシーケントに過不足なく合わせる。

`logic_prop_assume`

logic_prop_assume は、リプレイのコードが使う名前で呼べる logic_assume である。

pub fn logic_prop_assume(@kernel.KernelState, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_strengthen_to_hyps`

logic_prop_strengthen_to_hyps(state, hyps, th) は、弱化によって hyps のうち不足している仮定を th に追加し、結果の仮定がちょうど hyps であることを検査する。

pub fn logic_prop_strengthen_to_hyps(@kernel.KernelState, Array[@kernel.Term], @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

th が hyps の外に仮定を持つ場合は失敗する。弱化は仮定を追加できるが、取り除くことはできない。

`logic_prop_close_hypothesis` と `logic_prop_ensure_sequent`

logic_prop_close_hypothesis(state, hyps, c) は、c が hyps の 1 つであるとき、シーケント $\mathit{hyps} \vdash c$ を証明する。logic_prop_ensure_sequent(state, hyps, c, th) は、th が c を結論とすることを検査し、仮定をちょうど hyps にして返す。

pub fn logic_prop_close_hypothesis(@kernel.KernelState, Array[@kernel.Term], @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_ensure_sequent(@kernel.KernelState, Array[@kernel.Term], @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_discharge_imp_prefix`

logic_prop_discharge_imp_prefix(state, pre, [a1, ..., an], th) は、仮定 $a_n, \dots, a_1$ を順に解消し、 $\Gamma \vdash q$ を $\Gamma \setminus \{a_1, \dots, a_n\} \vdash a_1 \Rightarrow \dots \Rightarrow a_n \Rightarrow q$ に変える。

pub fn logic_prop_discharge_imp_prefix(@kernel.KernelState, PropPrelude, Array[@kernel.Term], @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_replay_imp_elim_backward` と `logic_prop_replay_imp_elim_backward_thm`

これらの関数は、後ろ向きの apply ステップを完了させる。ゴールの仮定、含意 $a \Rightarrow b$ (仮定の項として、または定理として)、および $a$ の証明を与えると、ゴールの仮定とちょうど同じ仮定の下で $b$ を証明する。

pub fn logic_prop_replay_imp_elim_backward(@kernel.KernelState, PropPrelude, Array[@kernel.Term], @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_replay_imp_elim_backward_thm(@kernel.KernelState, PropPrelude, Array[@kernel.Term], @kernel.Thm, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_replay_and_elim_l` と `logic_prop_replay_and_elim_r`

これらの関数は連言を除去し、結果が期待される項であることを検査する。

pub fn logic_prop_replay_and_elim_l(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_replay_and_elim_r(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_merge_conjunction`

logic_prop_merge_conjunction(state, pre, th_a, th_b, and_term) は連言を導入し、それが and_term であることを検査する。split はこれを用いて 2 つの分岐を結合する。

pub fn logic_prop_merge_conjunction(@kernel.KernelState, PropPrelude, @kernel.Thm, @kernel.Thm, @kernel.Term) -> Result[@kernel.Thm, @kernel.LogicError]

`logic_prop_or_wrap_left` と `logic_prop_or_wrap_right`

これらの関数は、左または右の分岐から選言を導入し、それが期待される選言であることを β 正規形の範囲で検査する。left と right がこれらを使う。

pub fn logic_prop_or_wrap_left(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]
pub fn logic_prop_or_wrap_right(@kernel.KernelState, PropPrelude, @kernel.Term, @kernel.Term, @kernel.Thm) -> Result[@kernel.Thm, @kernel.LogicError]

引数は、選言全体、もう一方の分岐、および選ばれた分岐の証明である。

test "replay helpers" {
  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)
  // close the goal  p, q |- p  from the hypothesis p
  let th = @logic.logic_prop_close_hypothesis(st, [p, q], p).unwrap()
  inspect(@kernel.thm_hyp_count(th), content="2")
  // a theorem with an extra hypothesis cannot be fitted to a smaller sequent
  let th_pq = @logic.logic_prop_and_intro_thm(
    st,
    pre,
    @logic.logic_assume(st, p).unwrap(),
    @logic.logic_assume(st, q).unwrap(),
  ).unwrap()
  inspect(@logic.logic_prop_strengthen_to_hyps(st, [p], th_pq) is Err(_), content="true")
}

定理カタログ

カタログは、証明スクリプトが exact と apply で使える定理名の唯一のリストである。

`PropTheoremClass` と `PropTheoremEntry`

PropTheoremEntry はカタログの名前を記述するもので、前提の数と、exact および apply がそれをどう使えるかを持つ。PropTheoremClass は、その名前がゴールをどのように閉じるかを表す。

pub enum PropTheoremClass {
  DirectClose
  ImplicationBacked
  ContextDerived
}

pub struct PropTheoremEntry {
  name : String
  premise_count : Int
  exact_class : PropTheoremClass?
  apply_class : PropTheoremClass?
}

DirectClose はゴールをそのまま閉じる(truth、imp_refl、eq_refl)。ContextDerived は、仮定とローカルの中にある事実を用いてゴールを閉じる(コンテキスト中の連言からの and_elim_l)。ImplicationBacked はゴールを含意の前提に変える(apply or_intro_l)。クラスが None の場合、その名前はそのモードでは利用できない。

名前	前提の数	`exact`	`apply`
`imp_refl`	0	`DirectClose`	なし
`truth`	0	`DirectClose`	なし
`and_elim_l`	1	`ContextDerived`	`ImplicationBacked`
`and_elim_r`	1	`ContextDerived`	`ImplicationBacked`
`and_intro`	2	`ContextDerived`	なし
`not_elim`	2	`ContextDerived`	なし
`ex_falso`	1	`ContextDerived`	なし
`or_intro_l`	1	なし	`ImplicationBacked`
`or_intro_r`	1	なし	`ImplicationBacked`
`imp_elim`	2	`ContextDerived`	なし
`eq_refl`	0	`DirectClose`	なし
`eq_sym`	1	`ContextDerived`	`ImplicationBacked`
`eq_mp`	2	`ContextDerived`	なし

`logic_prop_theorem_count`、`logic_prop_theorem_at` と `logic_prop_theorem_entry`

これらの関数は、インデックスまたは名前でカタログを読み出す。

pub fn logic_prop_theorem_count() -> Int
pub fn logic_prop_theorem_at(Int) -> PropTheoremEntry?
pub fn logic_prop_theorem_entry(String) -> PropTheoremEntry?

`logic_prop_named_theorem`

logic_prop_named_theorem(state, pre, name, goal) は、与えられたゴールの結論に対する DirectClose の名前の定理を構築する。その名前がそのゴールを閉じない場合は None を返す。

pub fn logic_prop_named_theorem(@kernel.KernelState, PropPrelude, String, @kernel.Term) -> @kernel.Thm?

`logic_prop_context_theorem` と `logic_prop_context_apply_theorem`

logic_prop_context_theorem(state, pre, name, pool, goal) は、pool 内の事実から ContextDerived の名前の定理を構築し、使用した事実も併せて返す。logic_prop_context_apply_theorem は、ImplicationBacked の名前の含意定理を、新たなゴールとなる前件とともに構築する。

pub fn logic_prop_context_theorem(@kernel.KernelState, PropPrelude, String, Array[@kernel.Term], @kernel.Term) -> (@kernel.Thm, @kernel.Term)?
pub fn logic_prop_context_apply_theorem(@kernel.KernelState, PropPrelude, String, Array[@kernel.Term], @kernel.Term) -> (@kernel.Thm, @kernel.Term)?

解決結果

以下のリゾルバは、これらの型のいずれかを返す。KnownButUnavailable とその各バリアントは、その名前がカタログにはあるが、このモードではこのゴールに適用できないことを意味する。タクティク層はこれを未知の名前としてではなく、ゴール形状または apply の不一致として報告する。

pub enum PropApplyTheoremResolution {
  Applicable(@kernel.Thm, @kernel.Term)
  KnownButUnavailable
}

pub enum PropExactTheoremResolution {
  ExactApplicable(@kernel.Thm)
  ExactKnownButUnavailable
}

pub enum PropExactWitness {
  ExactLocalAlias(String)
  ExactDirectTheorem(String, @kernel.Thm)
  ExactContextTheorem(String, @kernel.Thm, Array[@kernel.Term])
}

pub enum PropExactWitnessResolution {
  ExactWitnessApplicable(PropExactWitness)
  ExactWitnessKnownButUnavailable
}

pub enum PropRefResolution {
  LocalFact(@kernel.Term)
  NamedTheorem(@kernel.Thm)
  ContextDerived(@kernel.Thm, @kernel.Term)
}

`logic_prop_resolve_exact_witness`

logic_prop_resolve_exact_witness(state, pre, locals, hyps, goal, name) は exact の引数を解決する。ローカル名が最初に検索され、見つかった場合はカタログ名にフォールバックすることはない。それが有効な仮定でありゴールと等しい場合にのみ適用可能となる。そうでなければ、カタログを exact モードで参照する。ローカルにもカタログにもない名前には None を返す。

pub fn logic_prop_resolve_exact_witness(@kernel.KernelState, PropPrelude, Array[(String, @kernel.Term)], Array[@kernel.Term], @kernel.Term, String) -> PropExactWitnessResolution?

`logic_prop_resolve_exact_theorem` と `logic_prop_resolve_apply_theorem`

これらの関数は、ローカルを見ずに、事実のプールに対してカタログ名を exact または apply モードで解決する。None はその名前がカタログにないことを意味する。

pub fn logic_prop_resolve_exact_theorem(@kernel.KernelState, PropPrelude, Array[@kernel.Term], @kernel.Term, String) -> PropExactTheoremResolution?
pub fn logic_prop_resolve_apply_theorem(@kernel.KernelState, PropPrelude, Array[@kernel.Term], @kernel.Term, String) -> PropApplyTheoremResolution?

`logic_prop_resolve_ref`

logic_prop_resolve_ref はモードを混在させる旧来のリゾルバであり、テストとタクティク以外の呼び出し元のために残されている。ProofState と prover はモード別のリゾルバを用いる。

pub fn logic_prop_resolve_ref(@kernel.KernelState, PropPrelude, Array[(String, @kernel.Term)], Array[@kernel.Term], @kernel.Term, String) -> PropRefResolution?

test "catalog" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  inspect(@logic.logic_prop_theorem_count(), content="13")
  let e = @logic.logic_prop_theorem_entry("or_intro_l").unwrap()
  inspect(e.exact_class is None && e.apply_class is Some(@logic.ImplicationBacked), content="true")
  let t = @kernel.ks_mk_const(st, "T").unwrap()
  // `exact truth` closes the goal T
  let r = @logic.logic_prop_resolve_exact_theorem(st, pre, [], t, "truth")
  inspect(r is Some(@logic.ExactApplicable(_)), content="true")
  // `apply truth` is known but not usable: truth is not an implication
  let r2 = @logic.logic_prop_resolve_apply_theorem(st, pre, [], t, "truth")
  inspect(r2 is Some(@logic.KnownButUnavailable), content="true")
  // an unknown name resolves to nothing
  inspect(@logic.logic_prop_resolve_apply_theorem(st, pre, [], t, "nope") is None, content="true")
}

logic API

プレリュード

PropPrelude

PropRule

default_prop_prelude

install_prop_prelude

prop_prelude_rule_count、prop_prelude_rule_at と prop_prelude_has_rule

prop_truth_name と prop_false_name

結合子の項

prop_mk_and、prop_mk_imp、prop_mk_not と prop_mk_or

prop_dest_and、prop_dest_imp、prop_dest_not と prop_dest_or

logic_prop_truth_term と logic_prop_false_term

定義定理

logic_prop_def_imp、logic_prop_def_not、logic_prop_def_and と logic_prop_def_or

logic_bool_false_def_thm

logic_prop_def_lhs と logic_prop_def_rhs

logic_prop_unfold_head

logic_prop_unfold_imp、logic_prop_unfold_not、logic_prop_unfold_and と logic_prop_unfold_or

カーネル規則のラッパ

logic_refl、logic_assume、logic_add_assum と logic_trans

logic_mk_comb_rule、logic_abs_rule と logic_beta_rule

logic_eq_mp と logic_deduct_antisym

logic_inst_type と logic_inst

拡張のラッパ

logic_register_typedef と logic_typedef_contract

logic_specify_const

logic_register_ind_infinity_anchor と logic_ind_infinity_anchor

logic_extension_cert_count、logic_extension_cert_at と logic_conservative_replay_ok

等式のツール

logic_eq_sym

logic_eq_mp_bool

logic_apply_fun_eq と logic_apply_fun_eq2

logic_beta_normalize_eq と logic_normalize_prop_beta

logic_beta_nf_bool_term と logic_beta_nf_bool_term_deep