定理证明器背后的数学原理

How it looks like

相比一上来就掰扯复杂的数学理论，我们不如先来看看一个使用定理证明器 Lean ¹ 编写数学定理的证明的实际例子，我们就选择比较容易证明的德摩根定律来证：

open Classical

theorem deMorgan : ¬(p ∧ q) ↔ ¬p ∨ ¬q :=
  Iff.intro
    (λ (left: ¬(p ∧ q)) => (
      Or.elim (em p) 
        (λ (hp: p) => Or.intro_right (¬p) (
          λ (hq: q) => absurd ⟨ hp, hq ⟩ left
        ))
        (λ (hnp: ¬p) => Or.intro_left (¬q) hnp)
    ))
    (λ (left: ¬p ∨ ¬q) => (
      Or.elim left
        (λ (hnp: ¬p) (inner: p ∧ q) => absurd inner.left hnp)
        (λ (hnq: ¬q) (inner: p ∧ q) => absurd inner.right hnq)
    ))

看起来这个证明好像是由一些 λ（就像 Python 中的 lambda，in case 你没学过“正规”的 FP 语言）和一些高阶函数（比如 Or.elim）组成的。

那这些东西凭什么能证明这个命题呢。

这就要牵扯到一个叫 Curry-Howard 同构的东西了。

Curry-Howard 同构

Curry-Howard 同构建立了 “证明”² 和 “程序”³ 的对应关系：

• 一个程序（常体现为一个函数）的内容对应于一个证明

  比如我们上面证明 deMorgan 定律时，无非就是把几个更基本的结论的证明组合起来（比如使用 Iff.intro 来结合 ↔ 从左至右和从右至左的结论的证明，来组成最终的证明），因此编写证明的过程就是在编写一个把 旧有结论的证明 结合成 新结论的证明 的程序。

• 一个类型对应于一个命题

  比如我们上面证明的 deMorgan 定律，其对应的类型也就是之前提到过的“把旧有结论的证明结合成新结论的证明的程序”所对应的函数的类型。

比较简单的想法是，如果我们能从一个命题通过一些程序运算得到另一个命题，那如果前者成立，后者（因为是算出来的）也必定成立，所以这个程序就是两个命题间“实质蕴涵”的一个构造性证明；而为了让这个程序中的 “类型检查” 可以用于保证这个证明是有效的，我们可以用类型的形式“书写”这个命题。

怎么用，也即一些计算机辅助证明的例子

例如我们要在 lean 中证明 (p → (q → r)) → (p ∧ q → r)，或者读作：

For all proposition p, q, and r, "p → (q → r)" implies "(p ∧ q) → r".

根据“程序即证明”的思想接下来我们要写一个类型为 (p → (q → r)) → (p ∧ q → r) 的程序。

-- fill "sorry" here
theorem tt: (p → (q → r)) → (p ∧ q → r) := sorry

我们直接创建一个这个类型的匿名函数：

theorem tt: (p → (q → r)) → (p ∧ q → r) := 
    λ (lhs: p → (q → r)) (hp_and_q: p ∧ q) => sorry

现在要做的就是填入函数体，考虑到 ∧ 的性质，直接将其拆分成 left 和 right，然后作为 lhs 的参数（由于 Curry-Howard 同构，lhs 既是类型为 命题 p → (q → r) 对应的类型 的一个函数，也是这个命题的证明）填入即可。

theorem tt: (p → (q → r)) → (p ∧ q → r) := 
  λ (lhs: p → (q → r)) (hp_and_q: p ∧ q) => 
      lhs hp_and_q.left hp_and_q.right

现在，我们写出了一个类型是 (p → (q → r)) → (p ∧ q → r) 的函数，同时也就构造出了对应命题的证明，由于 lean 的类型检查器没有抱怨，我们就可以认为这个证明是正确的。

实际证明命题的时候，我们可以利用到一些事先已经证明好的定理或者公理（也就是对应的函数），比如：

• Or.elim，其类型为 Or a b → (a → c) → (b → c) → c，也就是说它是一个

  • 接受一个形如 Or a b （常被写作 a ∨ b）的类型（也就是对应的命题）
  • 再接受一个 a → c 类型的函数（或者说 命题 a → c 的证明）
  • 再接受一个 b → c 类型的函数（或者说 命题 b → c 的证明）

  的函数，也即是对应命题的证明。

更多 Lean 证明中可以使用的定理和公理，可以查看 Lean 源码 里的库的部分，比如 Prelude.lean 和包含经典逻辑 的 Classical.lean。