证明助理与内核检查

双向检查与 elaboration ​

双向类型检查理路双向类型检查Bidirectional type checking · Bidirectional typing把类型综合与给定类型下的检查分开，并用局部注解连接两种方向的算法化类型判断。把可综合项与需给定期望类型的项分开，有助于在 core language 中保持判定性。用户省略的隐式参数、类型类实例和 coercion 由 elaborator 填补。

例如用户写交换律证明的 tactic 脚本，elaborator 可能生成包含等式消去子的长 proof term。内核检查后者，而不是信任 tactic 日志。

elaboration 若产生 metavariable 未解决，系统必须拒绝或显式把它转成 assumption；静默当作任意证明会形成漏洞。

overloading 与 type class search 可以选出不同实例。例如同一个 + 可能是自然数、整数或矩阵运算；elaborated term 决定实际定理。打印 surface statement 不足以复核隐式实例，关键位置应能展开。

双向检查不必推断所有类型，用户 annotation 是可接受输入；elaborator 的便利失败不代表 core term 不存在，也不代表定理不可证。

定义相等与归约 ​

内核常需判断 $A$ 与 $B$ 是否 definitionally equal，通过 $\beta ,\delta ,\iota ,\zeta$ 等归约或 normalization-by-evaluation。这个等价不是用户证明的 propositional equality。

不受控展开可能不终止，因此核心递归定义需结构递归、well-founded recursion 或 termination certificate。接受任意一般递归会让 conversion 检查失去一致性/可判定基础。

universe inconsistency、非正归纳定义和 quotient 实现也是内核高风险面，不能用“Curry–Howard 所以自动正确”跳过。

归纳类型的严格正性检查会拒绝含构造子 $\mathsf{bad}:(D\to \mathrm{False})\to D$ 的这类定义：构造子的参数类型 $D\to \mathrm{False}$ 在箭头左侧使用了 $D$，使消去时可能把被分析对象重新传给内部函数，破坏归纳依据。递归定义则需要单独保证终止；若系统允许将非计算证明声明为 opaque，定义相等检查也应遵守相应的不可展开约定。

proof irrelevance、propositional extensionality 和 univalence 对 definitional equality 的地位随系统不同。把某系统中的公理等同当另一系统的计算规则，会改变内核和可执行内容。

外部求解器证书 ​

SAT/SMT、CAS 或自动定理证明器可作为 oracle。一种缩小可信边界的方式是让外部工具输出 proof certificate，再由内核内反射程序或独立 checker 验证。

若只把求解器 unsat 返回值转成定理，则求解器和翻译器都进入可信基。proof-producing 并非自动完整：证书格式可能不覆盖所有理论或预处理步骤。

SAT DRAT/LRAT 证书可由小 checker 重放 clause addition 与 deletion；SMT 理论 lemma 还需各理论 checker。预处理若消去变量，证书必须连接原公式，不能只证明简化后公式 UNSAT。

反射 tactic 可在内核中证明一个 verified checker 的正确性，然后通过计算检查大证书；此时还需信任内核求值和 extracted/native computation 的连接方式。

一个带编号的 RUP 重放片段 ​

把上述原则落实为一个有限检查器。输入 $F_0$ 是CNF公式理路CNF 可满足性问题CNF satisfiability · CNF-SAT给定有限个命题子句的合取，判定是否存在同时满足全部子句的布尔赋值。，变量集合 $V$ 有限，文字为 $v$ 或 $\mathrm{\neg }v$。每个子句先去重，作为有限集合保存；本教学片段拒绝同时含 $v,\mathrm{\neg }v$ 的重言子句，允许空子句。原子句按输入顺序获得正编号 $1,\dots ,m$，内容相同的两个子句也可以有不同编号。

检查状态是活动映射 $D:\mathrm{ID}\rightharpoonup \mathrm{Clause}$ 与永久已用编号集合 $U$。初始化 $D(i)=C_i$（$1\le i\le m$），$U=\{1,\dots ,m\}$，从而原始编号也永久保留。证书只含两种逻辑记录：

Add(new_id, clause, ordered_hints)
Delete(ids)

Add 的编号必须是未在 $U$ 中出现过的正整数，子句只能使用 $V$ 中的变量。提示都是正的活动子句编号；这里不实现 LRAT 中负提示表示的 RAT 分支。Delete 的编号必须互异且全部活动，删除后从 $D$ 移除，但不从 $U$ 移除。此处给出的是 RUP/AT 的 LRAT 式编号与提示机制，不声称该逻辑记录语法是完整 LRAT 文件格式。[4, §§3–4]

检查一次 Add(k,C,[h_1,...,h_r]) 时，新建局部部分赋值 $\rho$，使 $C$ 中每个文字为假。因为已拒绝互补文字，这些假设不会互相矛盾。按单位传播理路单元传播Unit propagation · Boolean constraint propagation · BCP在部分赋值下反复满足单位子句，并记录传播原因直至达到不动点或发现冲突。规则顺序访问每个 $D(h_i)$，不能替换成求解器另外搜索到的子句：

1. 若编号不活动，拒绝；若该子句已有真文字，也拒绝这条不适用的提示。
2. 删除已为假的文字。剩下至少两个未赋值文字时，它不是单位传播，拒绝。
3. 恰剩一个文字 $\ell$ 时，把 $\ell$ 赋为真，再处理下一提示。
4. 剩余为空时得到冲突；要求这正是最后一条提示，否则拒绝多余提示。若提示用尽仍无冲突，也拒绝。

只有这一轮成功，才把 $C$ 加入 $D(k)$ 和编号加入 $U$。每个 Add 都从新的 $\rho$ 开始，不能把上一次反证假设或传播赋值带入下一次。扫描有限提示及有限子句必定结束；资源预算不足时可以返回未完成，不能返回接受。

检查器顺序验证全部记录，并要求最后一条是成功添加空子句的 Add。仅通过若干非空子句的检查不算 UNSAT。若原公式已经含空子句，也可用其编号作为唯一冲突提示添加一个新的空子句。永久编号不复用、拒绝重言子句、冲突必须位于提示末尾以及最后记录的要求，都是本页明确的简化约定，而非声称所有 LRAT 工具都必须采用的限制。

四个原子句与一个可重放的反驳 ​

取

在空赋值下没有单位子句。下面的记录不需要检查器自行决定对哪个变量分支：

Add(5, [a],     [1,2])
Add(6, [not a], [3,4])
Delete([1,2,3,4])
Add(7, [],      [5,6])

第二轮必须重新令 $a=1$，而不能沿用第一轮的 $a=0,b=1$。删除后活动映射只有 5、6，第三轮仍可重放；原始公式 $F_0$ 作为整个证书的待证对象没有被修改。每一行提示的单位或冲突状态都可手工检查，最后接受的是原始四子句不可满足。

坏证书会在哪一步被拒绝 ​

• 只提交 Add(5,[a],[1,2]) 后结束：这一轮冲突仅说明 $F_0\models a$；没有最后的空子句记录，整体拒绝。
• 直接提交 Add(5,[],[1,2])：空候选没有反证假设，提示1中两个文字均未赋值，第一步就拒绝。
• 删除1–4后提交 Add(7,[],[1,2])：提示1已不活动，拒绝；不能从缓存中复活删除的子句。
• 把已删除编号1用于新的 Add：即便内容能被证明，也违反永久编号新鲜性；否则同一提示编号会在日志不同位置代表不同对象。
• 把单位子句保存为未去重的列表并按出现次数数剩余项，会把 $a\vee a$ 误当成非单位；规范化必须先于传播。相反，$a\vee \mathrm{\neg }a$ 在本片段的语法检查处明确拒绝，不把它的互相矛盾反证假设当作普通传播结果。

删除所有原子句得到的空子句集是可满足的，不是空子句；单独的删除记录永远不能使检查器宣布 UNSAT。

从提示正确性到原公式不可满足 ​

先证明一次 RUP 检查的局部引理：若在活动公式 $D$ 下，令候选 $C$ 的所有文字为假后，指定提示产生冲突，则 $D\models C$。

反证假定存在总赋值 $\alpha$ 同时满足 $D$ 和 $\mathrm{\neg }C$。初始部分赋值 $\rho$ 与 $\alpha$ 相容。每个单位提示的其他文字已经为假，而 $\alpha$ 必须满足这个活动子句，所以唯一剩余文字在 $\alpha$ 下为真；扩展 $\rho$ 后仍与 $\alpha$ 相容。对提示数归纳，最后的冲突子句在 $\alpha$ 下全部为假，违背 $\alpha \models D$。因此这样的总赋值不存在，即 $D\models C$。检查器拒绝已满足提示、非单位提示和不可用编号，正是为了使这条逐步强制论证成立。

全程保持的全局不变量是

初始每条活动子句都属于 $F_0$，所以成立。通过 Add 时，局部引理给出 $D\models C$，而全局不变量给出 $F_0\models D$，由蕴涵传递得到 $F_0\models C$。删除只是移除一些需满足的结论，不会破坏剩余子句仍被 $F_0$ 蕴涵的事实。最后一条成功加入空子句，便得到 $F_0\models \mathrm{\perp }$。

这也解释删除为什么不需要“被删子句已由其他活动子句推出”的证明：删除可以减弱活动公式，影响后续哪些提示可用，却不会让原公式失去蕴涵当前活动子句的性质。删除会使某些本来可重放的后续证书失效，检查器应拒绝失效证书。

该证明针对 RUP 子集：每次添加都是逻辑后果。完整 RAT 可以添加只保持可满足性而非原式蕴涵的子句，必须采用更一般的不变量和检查分支，不能直接沿用这里的蕴涵证明。本文不声称每个 UNSAT 输入都能靠原有单位传播一步完成，也不声称这个简化检查器覆盖完整 LRAT 格式。

独立检查缩小了求解器的可信职责，但仍需正确解析原公式与证书，维护编号、文字符号和局部赋值。若上游把程序性质错误编码为 CNF，可靠重放也只能证明那份 CNF 不可满足。输入编码的语义对应与证书重放是两项独立责任。

失败边界与复现 ​

证明助理检查的是形式陈述。若定理编码漏掉前提、数据结构不对应实现或使用了不希望的公理，内核仍会正确接受这个被错误建模的目标；发布物因此应同时给出陈述、axiom inventory 和与实现之间的解释。

名称解析决定常量实际指向哪个定义。Unicode homoglyph 或未展开的短名可能让屏幕上相似的陈述引用不同对象，审阅工具应能显示 fully qualified names，不能把视觉相似当作身份相同。

缓存的“已检查”结果必须由内容哈希绑定系统版本、依赖库和 opaque/transparent 等选项。定理发布应保存可重建源并在干净环境重新检查；只保存 tactic transcript，无法保证未来同名 tactic 仍生成同一 proof term。

代码生成或 extraction 会引入编译器、运行时与语义保持的新信任链；内核证明源函数满足规范，不自动证明生成的机器代码等价。类似地，巨大归约或证书可能造成拒绝服务，资源上限可以返回失败或 unknown，却绝不能在超限时默认接受。