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 构造的联结词项。

前奏（Prelude）

`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 闸门在内核状态中定义这六个前奏常量。

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

它是幂等的：已经恰好具有规范定义的常量会被保留。同名但仅被声明、或定义不同的常量会被拒绝并报 DefinitionAlreadyExists，类型不同的则报 ConstTypeConflict。在空状态上，它会添加六个 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$ ，头部的 β-redex 由 logic_beta_normalize_eq 收缩。

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

头部必须是被定义的常量，且至多应用于两个参数；否则函数失败并报 AlphaMismatch 或 TypeMismatch。只收缩恰在头部的 redex。给定一个参数时， $(\lambda x.\,b)\,a$ 就是这样的 redex，结果为 $b[a/x]$ ；给定两个参数时，头部是 $((\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`

这些函数是带某个联结词常量定义的 logic_prop_unfold_head。logic_prop_unfold_not 把 $\Gamma \vdash \mathit{not}\,p$ 变为基础形式的 $\Gamma \vdash \neg p$ ；两个参数的形式返回上述未归约的应用。

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 和 EQ_MP；内核教程逐步构造了同一条规则。当前提不是等式时，失败并报 NotAnEquality。

`logic_eq_mp_bool`

logic_eq_mp_bool 是 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`

只要等式右端是 β-redex，logic_beta_normalize_eq 就收缩其头部 redex：由 $\Gamma \vdash s = t$ 证明 $\Gamma \vdash s = t'$ 。logic_normalize_prop_beta 对定理结论的归约更彻底：它沿应用脊反复收缩最左最外的 redex（不进入抽象之下），至多 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]

tactics 层用它们在 β 等价意义下比较已完成的定理与其目标。

命题定理

这些函数从内核规则和联结词定义推导出命题逻辑的自然演绎规则。

`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 是肯定前件式（modus ponens）；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 失败。当第二个定理没有证明前件时，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",
  )
}

重放辅助函数

tactics 层通过重放内核步骤来关闭目标。这些辅助函数使定理恰好适配目标相继式。

`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`

当 c 是 hyps 之一时，logic_prop_close_hypothesis(state, hyps, c) 证明相继式 $\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 用它合并其两个分支。

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 及其变体表示该名字在目录中，但在此模式下不适用于该目标；tactics 层把这报告为目标形状或 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

前奏（Prelude）

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