tactics 设计

tactics 包让用户通过把目标归约为更简单的目标来向后证明，而每个定理仍由内核向前构建。本页解释把策略视为定理变换器的 LCF 观点、QED 如何把每一步的向前部分记录为数据而非闭包，以及为何不正确的策略可以使证明失败，却绝不会使证明错误地成功。

设计目标

提供含义与自然演绎相符的面向目标的步骤（intro、split、left、right、apply、exact、assumption）。
为用户所陈述的目标精确地产生内核 Thm，否则带着原因和失败目标的位置而失败。
不持有权限：该包只调用 logic 和内核函数来构建定理。

数学背景

作为定理变换器的策略

在 LCF 中，目标是尚待证明的相继式 $\Gamma \vdash c$ ，策略是一个函数

\mathsf{tac} : \mathit{goal} \to \mathit{goal}^{*} \times (\mathit{thm}^{*} \to \mathit{thm})

它返回子目标 $g_1, \dots, g_n$ 和一个论证 (justification) $j$ 。当对证明 $g_1, \dots, g_n$ 的任意定理 $t_1, \dots, t_n$ ，定理 $j(t_1, \dots, t_n)$ 都证明原目标时，该策略是有效的。¹1 M. Gordon, R. Milner, C. Wadsworth，Edinburgh LCF，LNCS 78，1979。当 $c' \equiv_\alpha c$ 且 $\Gamma' \subseteq \Gamma$ 时，相继式 $\Gamma' \vdash c'$ 证明目标 $\Gamma \vdash c$ 。运行证明就是不断应用策略直至没有目标剩下，然后自底向上组合论证，从关闭叶子的定理开始。

关键性质在于，有效性是正确性问题，而不是可靠性问题。论证只能通过调用内核规则来构建定理。如果策略无效，其论证产生的是另一个目标的定理，或者失败；它不可能产生假定理。因此 LCF 在最后检查有效性，QED 也这样做。

QED 各步骤的论证

下面每一步都是有效的策略；论证是右列中的内核推导。

步骤	目标	子目标	论证
`intro h`	$\Gamma \vdash a \Rightarrow b$	$\Gamma, a \vdash b$	$t \mapsto$ 从 $t$ 中解除 $a$ （蕴含引入）
`split`	$\Gamma \vdash a \wedge b$	$\Gamma \vdash a$ , $\Gamma \vdash b$	$(t_1, t_2) \mapsto$ 合取引入
`left`	$\Gamma \vdash a \vee b$	$\Gamma \vdash a$	$t \mapsto$ 左侧析取引入
`right`	$\Gamma \vdash a \vee b$	$\Gamma \vdash b$	$t \mapsto$ 右侧析取引入
`apply h`, $h : a \Rightarrow b \in \Gamma$	$\Gamma \vdash b$	$\Gamma \vdash a$	$t \mapsto$ 带 $\{a \Rightarrow b\} \vdash a \Rightarrow b$ 的肯定前件 (modus ponens)
`exact h`, `assumption`	$\Gamma \vdash c$ , $c \in \Gamma$	无	ASSUME $c$ ，弱化到 $\Gamma$
`exact n`	$\Gamma \vdash c$	无	$n$ 对应的目录定理，弱化到 $\Gamma$

每一行的有效性就是相应的自然演绎规则，已在 logic 设计中推导。对蕴含上的 intro，子目标的假设中含有 $a$ ，因此蕴含引入可以解除它，结果的假设重新成为 $\Gamma$ 。

intro x 也适用于形如 $(\lambda y.\,P) = (\lambda y.\,\top)$ 的目标，这是 HOL 对 $\forall y.\,P$ 的编码。子目标是对新变量 $x'$ 的 $\Gamma \vdash P[x'/y]$ ，论证为

\frac{\dfrac{\Gamma \vdash P \qquad \vdash \top}{\Gamma \vdash P = \top}\;\textsf{DEDUCT\_ANTISYM\_RULE}}{\Gamma \vdash (\lambda x'.\,P) = (\lambda x'.\,\top)}\;\textsf{ABS}

其中 ABS 需要 $x' \notin \mathrm{FV}(\Gamma)$ ，这就是为什么重放绑定子要相对目标、其局部变量及其假设选取为新的。

设计决策

作为数据的论证

问题。 LCF 把论证表示为闭包。闭包无法被检查，所以不能报告证明在何处失败，并且会捕获其构建时的整个上下文。

选择。 待处理目标把其论证作为数据携带：一个蕴含前缀（待解除的假设）、一条由 PendingRefine 值组成的细化链（待撤销的向后 apply 和量词步骤）、一个 SplitRole（合取的左半或右半）和一个 OrContext（选择了析取的哪一侧）。目标关闭时，finish_goal_evidence 解释该数据：它重放细化链，然后包装析取、合并合取的两半、解除蕴含前缀，最后撤销量词步骤。

原因。 这些数据是闭包的去函数化形式：每个构造子对应上表中的一个论证，解释器负责应用它们。它可以为诊断而被检查，是不可变的，两个证明状态可以安全地共享结构。

每次关闭时重放，在根处检查

问题。 如果向前重放等到最后才进行，证明早期的无效步骤只会在 ps_qed 处被报告，离其原因很远。

选择。 证据在目标一关闭时就被重放。split 的前半把其定理存放在后半的 SplitRole 中；后半关闭时，两者被合并。最后一个目标关闭时，将定理与根目标比较：经 β 规范化后，其假设必须与根假设一一对应，其结论必须等于根结论，两者均按 α 等价。只有这样，它才会被存为最终定理。

原因。 失败出现在导致它的那一步，而最终比较正是 LCF 的有效性检查：如果每一步都有效，它总会成功；如果某一步无效，用户得到的是 ProofSynthesisUnavailable，而不是一个错误命题的定理。

两个名字空间，一种顺序

exact n 和 apply n 先在 intro 引入的局部变量中查找 n，然后在 logic 包的目录名称中查找。局部变量总是胜出，且绝不回退到目录名称，因此名为 truth 的局部变量不会被误认为定理 truth。目录按该步骤的模式查询：exact 只使用能直接关闭目标的名称，apply 只使用属于蕴含的名称。在错误模式下使用的名称会被报告为不匹配，而不是未知名称。

没有 hole 步骤

有缺口的证明不是证明。策略层没有让目标保持未关闭的步骤，因此它不会产生假装已完成的状态。hole 是前端的概念：证明器在 hole 处停止，并报告未完成证明及该处的目标。

正确性与不变量

可靠性。 每个定理都由 logic 和内核函数构建；策略层无法构造 Thm。这里的缺陷会使证明失败或报告错误的错误，但绝不会以假定理成功。
根的保真。 证明状态只有在某定理在 β 范式与 α 等价意义下证明根目标，且恰好带有根假设时，才拥有最终定理。
目标顺序。 新的子目标按顺序放在其余目标之前。再加上 Split 把左半的定理存入右半，就给出了证明器分支块所依赖的从左到右求值。
分支路径。 每个待处理目标记录从根开始的选择路径：Split 追加 1 或 2，Left 和 Right 追加 1。证明器和 CLI 在失败时打印此路径。
持久性。 ps_apply 从不修改其参数；失败的步骤会让之前的状态保持可用。

被否决的替代方案

用闭包表示论证。 写起来更简单，但对诊断不透明，也更难测试。
仅在 ps_qed 构建定理。 内核调用更少，但错误会在远离其原因之处出现。
隐式的 exact 到 apply 回退。 当名称是蕴含时让 exact 悄悄开始向后一步，会使脚本更难阅读、错误更难定位。这两种模式是分开的。
元变量。 像 Isabelle 或 Lean 那样把目标的一部分留待以后填充，需要合一和内核中不完整定理的概念。已发布子集不需要它。

边界

只有命题步骤，外加对 HOL 全称量词编码的 intro。没有重写，没有对析取的情形分析，没有归纳。
没有证明搜索：每一步都由用户给出。assumption 和 apply imp_elim 只搜索当前假设。
不解析，也不调度分支块；这两者都由 prover 完成。
没有 hole，也没有部分定理。

M. Gordon, R. Milner, C. Wadsworth，Edinburgh LCF，LNCS 78，1979。当 $c' \equiv_\alpha c$ 且 $\Gamma' \subseteq \Gamma$ 时，相继式 $\Gamma' \vdash c'$ 证明目标 $\Gamma \vdash c$ 。 ↩