定理证明器是一种特殊的编程语言。我们平常的编程语言在编译的时候会做类型检查，来确保没有类型错误，而定理证明器则是设计出来确保数学证明没有错误的。在使用它们的时候，我们会把数学定理的证明写成程序，然后让软件来做类型检查。

这篇文章会介绍定理证明器的一些基本的工作原理，以及程序员一般不太熟悉的看待类型的视角。使用 Agda 是因为它是定理证明器里比较接近程序员的，也拥有非常优美的语法特性，是学起来很值的语言。

以集合来理解类型

data Apple : Set where
  red-apple : Apple
  green-apple : Apple
  yellow-apple : Apple

上面的代码定义了一个苹果的集合，这个集合包含三个元素，分别是红苹果、绿苹果和黄苹果。

在 Agda 里集合（Set）和类型是同义词，定义一个集合就等同于定义一个类型，实际上我们也可以将类型看作集合。在传统的编程语言如 C 里，int 是一个类型，如果把 int 看作一个集合，也就是整数集合，那么 1、2、3 等都是其中的元素。

理论上在 Agda 中我们可以这样表述一个自然数的集合，或者类型：

data Nat : Set where
  0 : Nat
  1 : Nat
  2 : Nat
  ......

这里我们通过把每一个元素都罗列出来定义这个集合，但是实际上这是做不到的，因为自然数有无穷多个。稍后我们会看到更实用的定义自然数的方式。

在 C 里，如果一个函数接受 int，我们可以把 1、2、3 传给它。同样的，Apple 也是一个类型，如果一个函数需要 Apple，我们可以把三种苹果之一传给它。在传统语言里，类型一般只被理解为一种标记，但是在定理证明器里，类型往往描述的是一种性质，例如“有某某性质的集合”。因此，以集合的视角来看待类型会更接近它们在定理证明器里的形态。

证明即可被构造

考虑这么一个问题，我们如何证明一个苹果存在？最简单的方法就是找到一个苹果的实例。那么这如何在 Agda 里表述呢？

proof-that-apple-exist : Apple
proof-that-apple-exist = ?

以上代码中的 proof-that-apple-exist 是一个未完成的证明，问号的地方有待填入内容，但是这个证明的目标是明确的，它需要找到一个苹果的实例。我们也会发现这个 proof 本身的类型就是 Apple，这和我们的目标是对应的。

proof-that-apple-exist : Apple
proof-that-apple-exist = red-apple

在问号的地方我们可以填入一个 red-apple，于是这个 red-apple 就证明了苹果的存在，就像我们给要求我们证明的人扔了一个红苹果。这段代码是可以通过类型检查的，这也意味着我们形式化地证明了苹果的存在。

这看起来是非常平凡的结论，但是它有很深远的意义，例如我们可以设想这样一段代码：

proof-that-1-plus-1-equals-2 : (1 + 1 == 2)
proof-that-1-plus-1-equals-2 = ?

这段代码里 proof-that-1-plus-1-equals-2 的类型是 (1 + 1 == 2)，如果我们把这个类型视为一个需要证明存在的整体，只要我们提供一个 (1 + 1 == 2) 类型的实例，我们就证明了 1 + 1 = 2。

(1 + 1 == 2) 看起来完全不像一个类型，但是这在有依赖类型的语言里（包括 Agda）是完全合法的。于是，类型和定理证明联系了起来。如果我们可以把一个数学定理写成一个类型，那么只要提供一个这个类型的实例，我们就证明了这个定理。

那么如何提供一个这样的实例呢？我们需要了解 (1 + 1 == 2) 这个类型是怎么定义的，这个类型的核心是==，一种常见的定义如下：

data _==_ {A : Set} : A -> A -> Set where
  refl : (a : A) -> (a == a)

这个定义里的==是一个二元操作符，接受两个参数，返回一个类型。具体的语法不重要，重要的是这个类型拥有一个名为 refl 的元素。不过和苹果的例子不同的是，这个元素不是一个简单的实例，而是一个函数，它的意思是给它任意一个 a，它可以返回一个 (a == a) 的实例。

refl 称作==类型的一个构造器，我们之前的 Apple 类型里的三种苹果也是构造器，只不过那些构造器不需要参数就可以直接构造出实例，而 refl 需要参数。另外，由于 refl 是==类型唯一的构造器，也就意味着我们仅有此一种方式去构造一个==的实例。而在苹果的例子中，我们有三种不同的方式去构造一个苹果。

因此，(1 + 1 == 2) 这个类型是可以被构造的，而构造它势必会用到 refl。实际上，我们可以直接在问号处填入 refl 来通过类型检查，这是因为 1 + 1 在 Agda 的计算过程中会规约为 2，于是待证明的类型变成了 (2 == 2)，而 refl 函数正好可以构造这么一个类型。

proof-that-1-plus-1-equals-2 : (1 + 1 == 2)
proof-that-1-plus-1-equals-2 = refl 2

上面的代码要实际运行还依赖自然数和加法的定义，这里暂时略过，但是证明的原理就是构造一个类型的实例。这种类型和证明之间的联系称为柯里 - 霍华德同构（Curry-Howard correspondence）。这个理论指出，一个逻辑命题和一个类型是等价的，而命题的证明和类型的实例是等价的。上面的例子中，(1 + 1 == 2) 是一个数学命题也是一个类型，而 refl 是这个命题的证明也是这个类型的实例。

实际上更常见的命题以函数的形式出现的，例如：

proof-that-addition-commutes : (a b : Nat) -> (a + b == b + a)
proof-that-addition-commutes a b = ?

这是一个加法交换律的证明，它本身是一个函数。它的类型签名的意思是，输入 a 和 b 两个自然数，可以输出一个 a + b == b + a 的证明，也就是对于任意自然数 a 和 b，加法交换律成立。这个函数接受了两个参数，而问号的地方需要填入的就是它的函数体。这也是柯里 - 霍华德同构的另一种常见表述，命题和函数类型等价，而函数的实现和证明等价。因此，每一个计算机程序实际上都是一个命题，而计算机程序本身就是这个命题的证明。

递归构造器

在文章开头我们提到过一种很蹩脚的定义自然数的方式，由于自然数有无穷多个，我们实际上是没办法把它们全部枚举的。那么我们该如何表述一个无限的集合呢？我们可以用到递归：

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

这个自然数的类型有两个构造器。zero 代表 0，也就是声明了 0 本身是一个自然数。succ 是一个函数，输入一个自然数，输出一个自然数，我们可以用 succ 构造出其他自然数。

zero 是自然数，那么 (succ zero) 根据签名也会是一个自然数，(succ (succ zero)) 也会是一个自然数。succ 是后继者（successor）的意思，我们可以把 (succ zero) 视作 1，因为它是 0 的后继。接着 (succ (succ zero)) 便是 2，因为它是 1 的后继。不断叠加 succ，我们便可以获得无限多的自然数。

这便是皮亚诺公理（Peano's axioms）里定义的自然数的表示法，仅仅凭借这个定义，Agda 并不能知道 1 就是 (succ zero)，因为 1 只是我们日常用来简写的符号，但是任何一个自然数都可以仅通过 succ 和 zero 两个构造器构造出来，因此我们可以确定它们处在 Nat 的集合中。

分类讨论

让我们来证明一些简单的关于自然数的定理，首先我们需要定义加法。

_+_ : (a b : Nat) -> Nat
_+_ a b = ?

我们定义 + 为一个二元操作符，输入 a 和 b 两个自然数，输出一个自然数。问号的地方应该填入加法的函数体，但是应该填入什么呢？我们对 a 和 b 一无所知，但是我们知道它们既然是自然数，那要么是通过 zero 构造的，要么是通过 succ 构造的。我们可以使用 Agda 的交互证明功能，对 a 进行一个分类讨论。

_+_ : (a b : Nat) -> Nat
zero + b = ?
(succ x) + b = ?

Agda 的编译器可以帮我们把 a 按构造器来分类讨论，于是我们的函数有两种情况，第一种情况是 a 为 zero，第二种情况是 a 是某个数的后继，也就是 (succ x)，其中 x 为任意的自然数。这两种情况是可以覆盖所有可能的，因为自然数仅仅有这两种构造器。

_+_ : (a b : Nat) -> Nat
zero + b = b
(succ x) + b = succ (x + b)

对于第一种情况，显然 0 + b 是等于 b 的，这样才符合我们常用的加法。对于第二种情况，x 的后继加 b 实际上等于 (x + b) 的后继。这是一个递归定义，我们可以简单考虑一下 2 + 2 是如何递归的。

a	b	参数的模式匹配	结果	下一步需要计算
2	2	(succ 1) + 2	succ (1 + 2)	1 + 2
1	2	(succ zero) + 2	succ (zero + 2)	zero + 2
0	2	zero + 2	2

可以看到前两次调用都是分支二，最后一次调用到了分支一，所以这个递归是会终止的。把递归结果代入回前两次调用，就会是 (succ (succ 2))，也就是 4，结果是正确的。

因此，一个类型有哪些构造器也决定了我们在使用它们的时候需要考虑的可能，只有把每一个构造器的可能都覆盖到了，我们的函数定义才是完备的。

数学归纳法

我们来尝试证明一个简单的定理：

proof-that-zero-is-identity : (a : Nat) -> (a + zero) == a
proof-that-zero-is-identity a = ?

这个定理代表了对任意自然数 a，a 加上 zero 都是它自身。我们首先对 a 进行分类讨论：

proof-that-zero-is-identity : (a : Nat) -> (a + zero) == a
proof-that-zero-is-identity zero = ?
proof-that-zero-is-identity (succ x) = ?

第一种情况里需要证明的是 (zero + zero) == zero，这个可以通过 refl 直接解决。第二种情况需要证明的是 ((succ x) + zero) == succ x。我们可以猜想到第二种情况的证明一定是需要递归的，当我们调用 (proof-that-zero-is-identity x) 的时候，我们会得到一个 ((x + zero) == x) 的证明，然后只要对两边同时应用 succ，我们就可以得到我们的目标了。实际的证明代码如下：

proof-that-zero-is-identity : (a : Nat) -> (a + zero) == a
proof-that-zero-is-identity zero = refl zero
proof-that-zero-is-identity (succ x) = cong succ (proof-that-zero-is-identity x)

这里的 cong succ 是在两边同时加上 succ 的意思，例如我们有 a == b 的时候，根据函数的定义，也必定会有 (succ a == succ b)。

我们在对 (proof-that-zero-is-identity (succ x)) 的证明中，用到了 (proof-that-zero-is-identity x)，有数学训练的读者应该很容易发现，这实际上是使用了数学归纳法，(proof-that-zero-is-identity x) 就是归纳假设。我们要证明一个定理对自然数成立的时候，只要证明它对 0 成立，同时当 k 成立的时候对 k+1 也成立，那么它就对所有自然数都成立。

在定理证明器里使用数学归纳法是非常常见的，而实际上这也是由递归构造器的定义所决定的。

停机检查

程序员大概都会听过“停机问题是不可判定的”，也就是给定一个程序，我们并不能确定它在有限时间内一定会停下来。在普通的应用里这不是很大的问题，但是如果我们的程序是用来证明一个数学定理的，而我们不能确保它一定会停机，也就不能得到一个确定的证明，这是不可接受的。

Agda 既然要证明定理，就需要确保所有证明都是可以停机的，这也意味着证明里不能包含死循环。为了解决这个问题，Agda 内置了一个停机检查器（termination checker），并且默认开启。我们用一个例子来解释这个停机检查是如何工作的。

proof-that-zero-is-identity : (a : Nat) -> (a + zero) == a
proof-that-zero-is-identity zero = refl zero
proof-that-zero-is-identity (succ x) = proof-that-zero-is-identity (succ x)

初学 Agda 的人可能会写出这样的证明，这个证明的类型是正确的，但是 Agda 会提示这个证明没法通过停机检查，因为证明的第二个分支实际上是一个死循环，它在不断地用相同的参数调用自身。

为了通过停机检查，我们需要确保每次递归调用自身的时候，参数都比上一次变小了。例如在我们正确的证明中，对 (proof-that-zero-is-identity (succ x)) 的情况，我们调用了 (proof-that-zero-is-identity x)，新的参数是比原来的参数更小的，于是 Agda 知道我们的递归是一定会终止的。

总结

通过此文，读者应该能想象到人们是怎么在 Agda 里描述和证明定理的，只要定义证明需要的类型和构造器，Agda 就能保证我们的推理符合规则和不遗漏状况。而 Agda 的核心可以非常小，我们所需要用到的东西都可以通过类型这一基本概念定义出来。

Agda 的交互式证明实际上是非常酷的，但是仅仅通过文章没有办法展示，有兴趣的读者可以看千里冰封的演示视频https://www.bilibili.com/video/BV1xx411L7Jr。

关于类型系统，还有一个演讲也十分有趣https://www.bilibili.com/video/BV1Pt4y1k7tf。