有很多不同的辅助定理证明工具，各自的用法和机制都不尽相同。

这里主要简单地谈论 Coq，它基于类型论，而不是集合论。

为什么 Coq 代码看起来很晦涩

  • 它是从结论往前写，这和平时写数学证明的习惯不一致。解决方案是正向写，写引理。
  • 有隐含的上下文，可以省略参数名，不写出中间结果。所以可以单步执行，或者显式地写出来参数名和中间结果。
  • 指令基于类型论，而不是常见的逻辑运算。所以可以把针对逻辑运算符的指令当作固定的写法。
  • 提供指令模式和函数模式，两套写法很分割。实际上都可以使用，比如选择简单的写法。

基于传统和应用场合的原因，目前 Coq 代码仍保留传统晦涩的书写风格。一些新的面向数学的比如 Lean 则鼓励正向写出每一步结果，尽管会比较啰嗦。

最基本的是 -> 运算，有两条最基本的运算规则。

  1. A, A->B => B 。这是消去规则。
  2. P|-Q => |-P->Q。这是引入规则。

在 Coq 中对应用到 apply 和 intro 两条指令，分别对应这两条规则。这里指令有引号，防止歧义以免和规则名称混淆。

从程序语言的角度一切看并不复杂，apply 对应函数调用，intro 对应 lambda 语句。实现了一个函数即证明了这个函数（的类型）能够成立，写出程序即完成了证明。

关于证明

以自然数加法的交换律和结合律为例，代码参考自标准库（不完全相同）。

Require Import Arith.

Theorem add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. rewrite <- plus_n_O. reflexivity.
  - (* n = S n' *)
    simpl. rewrite IHn'. rewrite <- plus_n_Sm. reflexivity.
Qed.

这里的思路是按照加法定义利用数学归纳法来证明。

关于上面出现的其他代码，属于固定的模板框架，按照字面意思理解就可以了。这里参数名显式写出了。常见的定理在标准库中实现好了，可以直接使用，以及按运算名词进行检索。

可以自定义类型/谓词，表示某种数或某种性质，这样就可以使用构造函数和解构函数。构造函数需要自行定义，解构函数则直接对应地产生。比如说自然数可以定义为零或者一个自然数的后继，这是两个不同的构造函数，那么对应后一种情况就可以得到它的前驱。

其他用到的指令都是针对自定义类型，常用的逻辑连接词都是这样在系统中定义，然后可以通过调用构造函数来构造。同样的是逻辑运算符以及谓词，也和 -> 是一样也有引入和消去规则，在 Coq 中只是用到的命令不同。

基本指令

执行证明时屏幕上显示 Hypothesis |- Goal ，并处于可输入状态（或者单步执行状态）。

此时可以键入以下指令，使用引入和消除规则：

符号 出现在待证目标 出现在已知假设 H
-> intro apply H
$\forall$ intro apply H
~ intro apply H
结论   exact H, assumption, trivial, auto,
false   absurd, contradiction
$\land$ split, constructor elim H, case H, destruct H
$\lor$ left, right, constructor elim H, case H, destruct H
$\exists$ exists, constructor elim H, case H, destruct H
= reflexivity, rewrite H, rewrite <- H
<> discriminate  
P(X) constructor, apply C elim H, case H, destruct H
P(X) 递归定义 constructor, apply C elim H, intuition H
定义/定理 simp, unfold  
     

说明

  • 对于一个嵌套的表达式，以上表格只看表达式的最外层的符号。
  • 由于是向后证明（想要证明什么就要证明什么），导致看上去针对目标的指令的作用是反的，即从输出到输入。
  • 指令默认是改变目标，但是也可以作用于前提，使用 in 参数比如 apply H1 in H2。
  • 处于版本迭代和实现差异的原因，可能同一功能有多个指令。看代码的时候可能都能看到，自己写的话固定一种就行。也还有很多类似于语法糖的指令，可以很容易从字面意思和上下文上来理解。
  • 可以通过 apply 使用已知的公理和定理。apply一个构造函数，等价于 constructor 指令，在上述表格中也有很多其他方便使用的别名。
  • 正向证明可以使用 assert (H: e)、 pose 显示写出中间结果。也可以在传入参数的时候，以函数调用的形式执行 apply。
  • 对于等式还有利用等式的性质 symmetry, transitivity, ring。
    • 以及谓词的相等性 （出现 P x = P y） f_equal, injection, inversion, （目标是 <>） discriminate。
  • 经典逻辑需要手动开启排中律（$P\lor\lnot P$），从而使用相应的反证法、以及分类讨论。

程序证明

要证明针对所有输入性质成立，那么就使用数学归纳法，利用谓词的递归定义。

对于命令式语言，利用最弱前置条件（Weakest precondition），不再详述。

数学证明

目前 AI 的发展更希望正向显式的书写风格，一步一步写出中间结果，这和人类手稿的习惯类似。中间过程可以用搜索算法补充。

lean4 有数学相关的标准库，工具也以数学问题为导向。

Lean and its Mathematical Library

附录

一些补充的内容：

  • 用途集中在程序正确性、硬件正确性、以及数学证明。
  • 类型系统提供了系统的内置规则，写证明时不需要了解和在意，而是需要去注意问题中出现的范式。
  • 基于类型论的辅助证明工具最初是 Robin Milner 开发的 LCF System。
  • 在特定领域常称为 Automated theorem proving 或 Computer-assisted proof，这里以及检索时会用到也可能更适合作为标题，不过现在 AI 领域这些称呼不是很重要。
  • 详细的用法请参考具体项目以及文档，本文仅仅为了记录一些值得注意的方面。

参考资料

补充：其实思路可以更简单一点，从命题逻辑到谓词逻辑，如何用带类型的 lambda 去表达。千万不要把简单的事情搞复杂了。