证明助理与内核检查

从判断到证明对象 ​

在形式系统公理库形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。中，目标是建立判断 $\mathrm{\Gamma }⊢t:A$ 或命题的可推导性公理库句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。。证明助理让用户交互构造证明项 $t$，内核独立检查它是否满足推理规则。

典型管线为

$$\text{surface term}\stackrel{elaboration}{\to }\text{core proof term}\stackrel{kernel}{\to }\text{accepted/rejected}.$$

tactic、搜索、重写和自动化只负责产生候选证明项；若最终项由内核重新检查，自动化 bug 最多导致失败或生成被拒项，不应让假定理通过。

以函数蕴含为例，证明 $A\to A$ 的 core term 是

$$\lambda x:A.x,$$

内核在上下文 $x:A$ 下综合出项 $x$ 的类型为 $A$，再由函数引入规则检查 lambda 类型。这个小轨迹展示“证明”是规则可检查对象，而非 tactic 输出的一句成功消息。

若命题使用 classical axiom、choice 或 quotient，证明仍可检查，但逻辑基础随已声明常量扩展；输出 axiom inventory 才能说明结论依赖。

小可信内核原则 ​

LCF 风格把 theorem 设为抽象类型，只有少数内核推理函数能创建其值。其他程序通过组合这些函数工作，不能伪造 theorem。

依赖类型系统常直接检查 proof term。内核可信基包含 parser/core syntax、reduction、conversion、universe 约束和递归/positivity 检查；“内核很小”不等于只有类型检查主循环几行代码。

若插件能绕过抽象类型、unsafe cast 或直接注入公理，信任边界随之扩大。系统报告应列出 axioms 和 admitted goals。

parser 把用户文本变成语法树，名称解析决定常量指向哪个定义。名称混淆或 Unicode homoglyph 可让屏幕上相似定理实际引用不同对象；内核检查内部标识，审阅工具需忠实显示 fully qualified names。

构建系统若信任预编译 .olean/.vo 等工件的校验标志而不核对内容哈希，也会扩大可信基。缓存命中必须绑定编译器、依赖和选项。

双向检查与 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 所以自动正确”跳过。

归纳类型 positivity 防止定义类似 $D=(D\to False)\to D$ 的负递归，从而导出悖论。termination checker 保证递归计算归约；若用 opaque theorem 封装非计算证明，conversion 又不应随意展开它。

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。

代码生成/extraction 从证明项产生程序时，运行时和编译器正确性是另一条信任链。内核证明函数满足规范，不自动证明生成的机器代码保持语义。

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

失败边界与复现 ​

证明助理检查的是形式陈述。若定理编码漏掉前提、数据结构不对应实现或使用了不希望的公理，内核仍会正确接受错误目标的证明。

构建应记录系统版本、依赖库和 opaque/transparent 设置。核心定义变化会使旧 proof term 失去类型；缓存的“已检查”结果需由内容哈希绑定。

资源上，内核检查也可能遭遇巨大归约或证书造成拒绝服务。限制时间/内存可以返回失败或 unknown，却不能在超限时默认接受；性能防护不能改变逻辑判定方向。

定理发布应保存可重建源、锁定依赖，并在干净环境重新内核检查。只保存 tactic transcript 而缺少库版本，未来无法判断同名 tactic 是否生成同一 proof term。

参考资料

• Robin Milner, “LCF: A Way of Doing Proofs with a Machine,” MFCS, 1979, pp. 146–159。
• Thierry Coquand and Gérard Huet, “The Calculus of Constructions,” Information and Computation 76, 1988, pp. 95–120。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016, Chs. 5–10。