交互式定理证明器中的证明项与依赖类型

1. 我们先从一个简单概念开始：在交互式定理证明器（如Coq、Agda、Lean）中，用户通过编写证明脚本来构造定理的证明。但证明器的核心实际上并不直接记录这些脚本步骤，而是将每一步证明指令转化为一个被称为“证明项”的内部数学对象。证明项是一个类型良好的lambda项，其类型就是所要证明的命题本身。例如，命题“A → A”的证明项可以是 λ (x:A). x，这个项的类型是“A → A”。

2. 为了理解证明项如何与命题对应，需要依赖“Curry-Howard同构”（你已学过）。这个原理指出，命题对应类型，而该命题的证明则对应一个具有该类型的项。在构造逻辑/类型论的框架下，证明一个命题就是构造一个该类型的项。例如，命题“A ∧ B → A”对应类型是“A × B → A”，其证明项可以是 λ (p: A × B). fst p，其中 fst 是取二元组第一分量的函数。

3. 然而，简单的简单类型lambda演算不足以表达所有数学命题。为了表达“对于所有自然数n，P(n)成立”这样的全称命题，我们需要依赖类型。在依赖类型系统中，类型可以依赖于项。例如，“Vec A n”表示长度为n的A类型元素的向量，这里类型“Vec A n”依赖于项n（一个自然数）。全称命题“∀ n:ℕ, P(n)”对应的类型是“Π n:ℕ, P(n)”，这是一个依赖乘积类型（Π-类型），其项是一个函数，对于每个输入n，返回一个类型为P(n)的项（即P(n)的证明）。

4. 在交互式定理证明器中，当你使用策略（tactic）进行证明时，底层系统实际上是在后台帮你逐步构造这个证明项。例如，当你对目标“A → B → A”使用“intro a. intro b. exact a.”策略时，系统会依次构建证明项：λ (a:A) (b:B). a。每一步策略都对应一个或多个证明项的构造规则（如λ抽象、应用等）。证明完成后，系统最终保存的是这个完整的、经过类型检查的证明项，而不是策略序列。

5. 证明项的核心价值在于可靠性：定理证明器只需验证这个最终证明项的类型是否与命题一致，而无需信任策略实现的正确性。这个过程叫做“证明确认”（proof checking），它只依赖于相对简单的类型检查算法，极大降低了系统可信计算基的复杂度。依赖类型则保证了证明的丰富表达能力，使得从基本的逻辑命题到复杂的数学定理都能被统一表示为“类型”，其证明被表示为“项”。

6. 最后，依赖类型和证明项的紧密结合，还使得“程序即证明，证明即程序”成为可能。例如，一个类型为“Π (n:ℕ), Σ (m:ℕ), m = n + 1”的项，既是一个证明（对所有n，存在m使得m等于n+1），也是一个可计算的函数（输入n，返回配对(n+1)以及一个等式证明）。这种对应是交互式定理证明器中程序验证和形式化数学的基石。