tactics 教程

本教程使用 tactics 包手动驱动证明状态：陈述一个目标，逐步应用步骤，中途查看待证目标，最后收集内核定理。这就是 prover 对每个证明脚本所做的事，只是没有解析和调度。

快速开始

在 moon.pkg 中导入这些包：

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

用 intro 和 exact 证明 $\vdash p \Rightarrow p$ ：

fn goal_of(st : @kernel.KernelState, locals : Array[String], src : String) -> @tactics.Goal {
  let mut env = @parser.empty_parse_env()
  for name in locals {
    env = @parser.parse_env_push_local(env, name, @kernel.bool_ty())
  }
  let g = @parser.parse_goal_with_env(st, env, src).unwrap()
  @tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g))
}

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p"], "⊢ p -> p"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_exact("h")).unwrap()
  let th = @tactics.ps_qed(ps).unwrap()
  inspect(@kernel.thm_hyp_count(th), content="0")
}

goal_of 是本页通篇使用的小辅助函数：它声明布尔局部变量并解析一个目标。每一步都接受内核状态和序言，因为它可能调用内核规则。

日常任务

观察目标的变化

每一步之后，ps_current_goal 和 ps_current_local_hyps 显示剩下的内容：

test "watch" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["x"], "⊢ x -> x ∧ x"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // the goal is now  x ⊢ x ∧ x  with the local h : x
  let g = @tactics.ps_current_goal(ps).unwrap()
  inspect(@tactics.goal_hyp_count(g), content="1")
  assert_eq(@tactics.ps_current_local_hyps(ps).map(@tactics.local_hyp_name), ["h"])
  // split leaves two goals, x and x, on branches 1 and 2
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_split()).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="2")
  assert_eq(@tactics.ps_current_branch_path(ps), [1])
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_exact("h"), @tactics.step_exact("h")]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

这就是 examples/demo_and.qed 中的脚本 demo_and，一步一步地执行。

使用目录定理

exact 和 apply 也接受 logic 包目录中的定理名称。合取的交换律使用上下文中的合取：

test "and_comm" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "⊢ p ∧ q -> q ∧ p"))
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_intro("h"),
    @tactics.step_split(),
    @tactics.step_exact("and_elim_r"), // q, from p ∧ q in context
    @tactics.step_exact("and_elim_l"), // p, from p ∧ q in context
  ]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

用 `apply` 反向工作

当蕴含 $a \Rightarrow b$ 可用时，apply 把目标 $b$ 替换为 $a$ 。这是语料用例 t2， $\vdash p \wedge q \Rightarrow p$ ：

test "apply" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "⊢ p ∧ q -> p"))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // and_elim_l as an implication: from p ∧ q infer p, so the goal becomes p ∧ q
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_apply("and_elim_l")).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="1")
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_exact("h")).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
}

选择析取的一侧

left 和 right 选定某一侧。这是语料用例 t4， $p \vdash p \vee q$ ：

test "left" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_init(goal_of(st, ["p", "q"], "p ⊢ p ∨ q"))
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_left(), @tactics.step_assumption()]).unwrap()
  inspect(@tactics.ps_qed(ps) is Ok(_), content="true")
  // choosing the wrong side leaves a goal that cannot be closed
  let wrong = @tactics.ps_apply(st, pre, @tactics.ps_init(goal_of(st, ["p", "q"], "p ⊢ p ∨ q")), @tactics.step_right()).unwrap()
  let stuck = @tactics.ps_apply(st, pre, wrong, @tactics.step_assumption())
  inspect(stuck is Err(@tactics.GoalShapeMismatch(_)), content="true")
}

读懂错误

不适用的步骤会带着原因失败；先前的状态保持不变，可以再次使用：

test "errors" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let ps = @tactics.ps_apply(st, pre, @tactics.ps_init(goal_of(st, ["x"], "⊢ x -> x ∨ x")), @tactics.step_intro("h")).unwrap()
  let ps_left = @tactics.ps_apply(st, pre, ps, @tactics.step_left()).unwrap()
  // `truth` proves T, not x
  match @tactics.ps_apply(st, pre, ps_left, @tactics.step_exact("truth")) {
    Err(@tactics.GoalShapeMismatch(msg)) => inspect(msg, content="exact witness does not directly close current goal")
    _ => fail("expected a goal-shape mismatch")
  }
  // `or_intro_l` cannot be used with exact, only with apply
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_exact("or_intro_l")) is Err(@tactics.GoalShapeMismatch(_)), content="true")
  inspect(@tactics.ps_qed(ps) is Err(@tactics.UnsolvedGoals), content="true")
}

第一个失败是用户手册中的 bad_branch 示例；prover 会连同步骤编号和分支路径一起报告它。

进一步使用

用你自己的定理关闭目标。 ps_close_current_with_th(state, pre, ps, th) 用别处构建的定理（例如用 logic 包构建）关闭当前目标；它会检查该定理是否适配目标。

单独处理一个分支。 ps_isolate_pending_at(ps, i) 为待证目标 i 生成一个全新的证明状态。prover 用它单独运行 { ... } 分支块，因此某个分支内部的失败只针对该分支报告。

证明量化目标。 对于 HOL 编码的 $\forall x.\,P$ 的目标，即 $(\lambda x.\,P) = (\lambda x.\,\top)$ ，intro x 去掉量词，重放时用 ABS 重建它。脚本中用 forall 书写的目标则以不同方式处理，作为自由变量；见 parser 设计。

让 prover 来做。 prover 教程从文本脚本运行相同的步骤，并增加了结构化诊断和未完成证明。

常见陷阱

忘记序言。 含 T、F 或目录名称的目标，需要在传给每一步的状态中执行 install_prop_prelude。
以为 exact 会开启反向步骤。 exact 要么关闭目标，要么失败。对于 or_intro_l 这样的蕴含，请使用 apply。
被遮蔽的局部变量。 与目录定理同名的局部变量会隐藏该定理：在 intro truth 之后，exact truth 指向的是局部变量。
情形分析。 没有使用假设中析取的步骤；logic 设计解释了原因。
以为 ps_qed 会重新检查。 根检查在最后一个目标关闭时运行；ps_qed 只报告结果或 UnsolvedGoals。

后续步骤

tactics API 列出每个函数和重放上下文类型。
tactics 设计解释了论证 (justification)，以及为何无效步骤不可能产生错误的定理。
prover 教程从脚本运行相同的证明。