Luna Flow
简体中文

logic 教程

本教程使用 logic 包向前证明命题定理：安装联结词，构造公式，并把自然演绎规则组合成证明，例如合取的交换律。每一步都返回内核定理，所以你在这里构建的，正是 tactics 层在证明脚本背后所构建的。

快速开始

在 moon.pkg 中导入内核和 logic 包：

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

把命题序言 (prelude) 安装到内核状态中，然后证明 ⊢⊤\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∧qp \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⇒qp \Rightarrow q、q⇒rq \Rightarrow r 和 pp，推出 rr：

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")
}

使用否定与假

¬p\neg p 即 p⇒⊥p \Rightarrow \bot，所以 pp 的证明和 ¬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 层每次关闭目标时都会调用它。

规范化。 展开联结词常量会留下 β 可约式。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 会留下未归约的 (λp q. … ) a b(\lambda p\,q.\,\dots)\,a\,b；请调用 logic_normalize_prop_beta。
  • 按字面理解错误构造子。 辅助函数的失败以通用的内核错误报告，如 TypeMismatch。辅助函数失败时，请检查前提的形状。

后续步骤