证明助理与内核检查

双向检查与 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。

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

失败边界与复现 ​

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

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

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

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