在 Coq 中验证数学命题

Reference. Software Foundations Volume 1: Logical Foundations (Chap. 1, 2), Benjamin C Pierce et al.

惯例的 Q&A

• 对 OI 有什么用？
  • （貌似）没用。只想看 OI 相关内容的人可以即刻退出。
• 到底会讲啥？
  • 通过一系列简单的例子让读者对“有程序辅助的数学证明”有初步的了解。
• 需要什么前置知识？
  • 皮亚诺公理，数学归纳法。.
• 你个初学者还搁这班门弄斧。
  • 请给我提供具体的修改建议。

引入

“非形式化的证明是算法；形式化的证明是程序。”

什么是证明？用白话说，证明是这样一种东西，它能够让读者无可否认的认识到一个命题是成立的。

非形式化证明就是给人看的证明，人们通过阅读证明里的自然语言（比如中文说明）和数学符号来认识到命题的正确性；而形式化证明是给定理证明器看的证明。它是一段程序，里面的语句代表了一些已经证明的逻辑定理，定理证明器通过执行这段程序将命题归约为平凡的结论。

我们平时写的证明都是非形式化的，这也就是说我们需要依靠人类读者（你的老师、你的同学、同行评审，etc）来验证你的证明是否正确。但是，我们也可以通过书写形式化证明，让机器帮忙验证定理的正确性。这带来了若干好处：

• 形式化证明是代码，这也就是说我们可以实现代码复用等，节省了许多重复操作
• 机器帮助你证明，减少了你脑子的负担
• 只要证出来了，结论（几乎）不可能是错的，因为机器（不考虑极端情况）不会出错

接下来就来认识一下形式化证明吧。

认识 Coq

前置准备：到这里 下载并安装 Coq。

Coq 是一个交互式定理证明器，四色定理（任何地图都可以只用四种颜色上色）就是用它证明的。我们将借助它证明几个简单的定理。

CoqIde 是 Coq 自带的交互环境，我觉得它不太好用但是因为是自带的所以这里就用它了，我们将全程在这里编写证明。首先在开始菜单中（或者对于 macOS 用户，在 Launchpad 中；对于 linux 用户，自己鼓捣去）找到 CoqIde 并打开。

（CoqIde 的界面。）

下文中的每一段代码，你都应该复制到 CoqIde 内左侧的输入框里。

提供的练习题应该直接写到 CoqIde 里。它们不是选做的。如果不做，可能会导致下面的源码无法正常编译。实在不想做可以在本文末尾找到参考答案。

类型

Coq 的一大特色是，它并没有所谓“内置的，原始的”类型（比如 C++ 里的 int、bool、char 等）。所有的类型都是通过一种统一的方式定义的。

来看一下在 Coq 中如何定义布尔值：

Inductive bool: Type :=
  | true
  | false.

这里，我们定义了一个 bool 类型，有两种构造方式，分别是 true 和 false，也就是说有两种可能的值。

其中：

• Inductive <类型名>: Type 代表了我们正在定义一个类型；
• := 是 Coq 用的赋值符号；
• 接下来每一行，由 | 打头，后面是这个类型可能的构造方式（也就是说，可能的值）；
• 每个 Coq 语句由 . 结尾。

复制前面那段代码到 CoqIde 中，点击上端第三个按钮（向下的箭头），右下角的 Log 中会出现一些信息，同时这段代码被染绿，这就说明这个类型被定义了。之后每复制一段代码到 CoqIde 中，都可以单击这个按钮执行，点一次执行一句（也就是执行到下一个句号 .）。

（定义类型后的 CoqIde。）

练习题. Ex 1. 定义一个类型 weekday，让它代表一周内的七天。

Inductive weekday: Type :=
  (* 把这段注释替换为你的答案 *).

函数

Coq 作为一门编程语言，当然支持定义函数。但是，正如其他函数式编程语言一样，Coq 只能定义纯函数；更进一步的是，与 Haskell 等语言相比，Coq 只能定义能够终止的函数（无限递归不被允许）。

对于看不懂上面一段在说什么的人，详细说明一下：

• 纯函数是这样一类函数，它能够和数学上的函数等价。这也就是说，纯函数对于相同的输入总是得到相同的结果，并且没有副作用（不更改全局变量，不输出东西到屏幕上，等等）。
• Coq 只能定义能够终止的函数，所以 Coq 中停机是必然的，所以 Coq 不是图灵完全的。

那么，我们来定义一下对于 bool 的操作：取反、与、或、异或。

首先来看一下取反的函数：

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

其中：

• Definition <函数名> (<参数名>:<参数类型>) : <返回类型> 是函数的声明；
• := 依旧是赋值符号；
• match <值> with <模式> end. 是模式匹配。拿前面那段代码具体理解一下：
  • match b with：我们要匹配的值是传入的参数 b。
  • | true => false：如果 b 是通过 true 构造的，那么返回 false；
  • | false => true：如果是通过 false 构造的，那么返回 true；
  • end.：结束。

（定义函数后的 CoqIde。）

同时，也可定义接受多个参数的函数。这里定义一下逻辑与（A \land B）：

Definition andb (b:bool) (c:bool) : bool :=
  match b with
  | true => c
  | false => false
  end.

练习题. Ex 2. 定义对于类型 bool 的逻辑或（命名为 orb）和异或（命名为 xorb）的函数。

Definition orb (b c: bool): bool :=
  (* 把这段注释替换为你的答案 *).
Definition xorb (b c: bool): bool :=
  (* 把这段注释替换为你的答案 *).

平凡的证明

先来解决一些平凡的命题。

例. {\rm true} \land {\rm true} = {\rm true}.

这个命题很平凡。我们来看一下，在 Coq 中如何表达它：Theorem t_and_t_eq_t: (andb true true = true).

其中：

• Theorem <命题名>: <命题>. 声明了一个命题。（注意，Theorem 可以替换成 Example、Lemma、Remark、Fact、Property、Proposition、Definition，效果完全一样，看你乐意用哪个。）
• 命题名怎么取随你喜欢，但最好是有意义的名字。
• 在 Coq（以及许多函数式编程语言）中，我们通过空格而不是括号调用函数。andb true true 可以理解为 andb(true, true) 一样的东西，而括号只是为了调整优先级。

再来看一下，我们如何证明它。

Theorem t_and_t_eq_t: (andb true true = true).
Proof.
  simpl.
  reflexivity.
Qed.

其中：

• 第一行是命题，刚才讲过了。
• Proof. 代表证明的开始。
  • simpl. 将式子两端计算并化成最简。此时，两端都被计算为了 true。
  • reflexivity. 声明，因为等号两端相同，所以命题成立。
  • 另外 reflexivity. 其实也会化简。这里加上 simpl. 只是为了使步骤更清晰。
• Qed. 代表证明的结束。

在 CoqIde 里一步一步执行这段证明，观察右上角的证明区域如何变化。

（开始证明。）

（化简。）

（结束证明。）

练习题. Ex 3. 给出下面几个关于 andb 性质的平凡命题的证明。

Theorem t_and_f_eq_f: (andb true false = false).
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)
Theorem f_and_t_eq_f: (andb false true = false).
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)
Theorem f_and_f_eq_f: (andb false false = false).
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)

自然数与递归

注意，这一段中的类型声明都不用复制到 CoqIde 中（但是函数和证明仍然需要），因为 Coq 预置了相同的类型。

你可能会好奇，如何在 Coq 的类型系统里定义自然数。这里，我们需要知道两点理论基础：

• Coq 类型的构造方式可以接受参数。
• 自然数是由后继关系刻画的（注意，这里我们把一个自然数 n 的后继记为 n^+）。

来看一下自然数的定义：

Inductive nat: Type :=
  | O
  | S n.

它有两个构造方式。

• O 代表 0；
• S n 是接受一个参数的构造方式，它代表那个参数的后继。

这也就是说，O 是 0，S O 是 1，S (S O) 是 2，S (S (S O)) 是 3 ......

同时，我们定义的类型都是不限制大小的。所以，除非我们耗尽内存，否则不会有溢出的情况。

自然数上的许多函数也需要递归定义。Coq 的递归函数使用关键字 Fixpoint 而非 Definition。

来看加法的定义。

Fixpoint plus (a: nat) (b: nat): nat :=
  match a with
  | O => b
  | S a' => S (plus a' b)
  end.

其中有两种模式：

• O 匹配 0；
• S a' 是带参数的匹配，匹配到任何不是 0 的自然数，可以认为这里 a' 把 a 最外层的 S 剥掉了（也就是说减了 1）。

跟数学中自然数加法的定义对比一下，会发现是完全对应的，这里不再赘述。

再看减法（如果结果小于 0 那么仍然得到 0）：

Fixpoint minus (a b: nat): nat :=
  match a with
  | O => O
  | S a' =>
    match b with
    | O => a
    | S b' => minus a' b'
    end
  end.

这里可以看到，match 是能够嵌套的，并且只有最外层需要句号 .。

练习题. Ex 4. 完成以下乘法函数与判等函数。记住 match ... with ... end 能够嵌套。

Fixpoint mult (a b: nat): nat :=
  (* 把这段注释替换为你的答案 *).
Fixpoint eq (a b: nat): bool :=
  (* 把这段注释替换为你的答案 *).

使用重写来证明（rewrite）

来看一下这个命题。

命题. 对于任何自然数 n,m，如果 n=m，那么 n+n=m+m。

在 Coq 里，可以这样描述：Theorem plus_id: forall (n m: nat), n = m -> plus n n = plus m m.

其中：

• forall (<名称>: <类型>), 表达了“对于所有”的意思。也可以有多个参数，就如同书写数学表达式一样。
• -> 代表可以从左边推出右边。

先考虑如何在数学中证明这个命题。

命题. 对于任何自然数 n,m，如果 n=m，那么 n+n=m+m。

证明.

• 因为 n = m，所以将式中 n 全部替换为 m。
• 等式两边都为 m + m，所以命题成立。

而在 Coq 中，可以通过 intros <空格分隔的名称列表>. 来将 n, m 这类“变量”与 n = m 这种“前提”导入到证明当中。在这里，我们可以在证明中写 intros x y H.。Coq 会先引入 forall 中的变量 n, m 并且重命名为 x, y；再引入命题主体里的前提 n = m 并将它命名为 H。用其他名字也没关系，完全是习惯问题。

我们使用 simpl. 时，Coq 会默认化简当前的命题；但是，我们也可以指定化简某个等式。比如我们上面引入了 H，就可以通过 simpl in H. 化简等式 H。

而之前提到的“将一个东西替换为相等的另一个东西”，也就是重写，则可以通过 rewrite -> 等式. 进行。我们现在可以 rewrite -> H.，它会把命题中（n + m = m + m 中）所有这个等式（n = m）左边的值（n）替换为右边的值（m）。这样就可以完成我们的证明。

需要注意的是，还有另外一种重写方式 rewrite <- 等式.，这样会把等式右边的值全替换为左边的值，恰好颠倒过来。

Theorem plus_id:
  forall (n m: nat),
  n = m -> plus n n = plus m m.
Proof.
  intros x y.
  intros H.
  rewrite -> H.
  reflexivity.
Qed.

（intros 前与 intros 后，注意分割线上方出现的东西。）

（重写之后，等式两边相同了。）

练习题. Ex 5. 证明命题：对于所有自然数 n,m，如果 m = n^+，那么 m \times (1 + n) = m \times m。

Theorem mult_S_1:
  forall (m n: nat),
  m = S n
  -> mult m (plus 1 n) = mult m m.
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)

分类讨论（destruct）

在上一节，我们使用了 simpl.、 reflexivity.、intros <...>.、rewrite -> <...>. 这几个策略（tactics）进行了证明。然而，在遇到稍许复杂的命题时，单凭化简和重写可能没法起到很好的作用。

来看一个不是那么平凡的命题。

命题. 对于自然数 n，n + 1 \neq 0.

我们或许会想直接通过化简解决，然而在 Coq 中这行不通：

Theorem plus_1_neq_0_firsttry:
  forall n: nat,
  eq (plus n 1) 0 = false.
Proof. reflexivity. Qed. (* 行不通！ *)

这是因为 Coq 对于 n 具体是什么一无所知。但我们可以分类讨论：

• 如果 n 是 0 那么命题显然成立；
• 如果 n 是某个后继 m^+ 那么可以通过化简 eq 的定义得出成立。

要实现这样的分类讨论，我们可以使用 destruct <名字> eqn: <名字>.。前一个名字是我们要分类讨论的对象，后一个是我们给等式起的名字（也就是说叫什么都行），这个等式在不同情况中代表讨论对象的不同状态，比如在这里，它在两种情况中分别是 n = 0 和 n = S n0。

Theorem plus_1_neq_0:
  forall n: nat,
  eq (plus n 1) 0 = false.
Proof.
  intros n.
  destruct n eqn: E.
  - reflexivity.
  - reflexivity.
Qed.

逐步执行上面的代码，可以看到 destruct n. 将命题拆分成了两个分命题（subgoals）。这些命题中 Coq 有了更多的信息，证明起来也就更容易。在分命题中证明时，我们使用类似 Markdown 列表的语法来分别两个分命题。之后还会有分命题中的分命题，每层都需要使用不同的列表记号（可用的有 -、+、*）。

（destruct 将命题分解。）

(第一个分命题。）

(完成第一个分命题时，Coq 提醒还存在未验证的分命题，同时展示第二个分命题。）

练习题. Ex 6. 证明对于布尔值 b, c，如果 b \land c = {\rm true} 那么 c = {\rm true}。（注意，分类讨论时，你可能会遇到一些荒谬的情况，它们拥有错误的前提。但是不用担心，这些情况下你仍然可以推出结论。记住，从错误的前提什么都可以推出。）

Theorem andb_true_elim2:
  forall (b c: bool),
  andb b c = true
  -> c = true.
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)

归纳证明（induction）

有时候，分类讨论也不管用：

Theorem plus_n_O_firsttry:
  forall n: nat,
  n = plus n 0.
Proof.
  intros n.
  destruct n eqn: E.
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)
    simpl. (* 这里我们卡住了 *)
Abort.

所以，我们需要借助数学归纳法。

数学归纳法. 对于一个命题 P(n) 如果 P(0) 且 P(m) \Rightarrow P(m^+)，那么 P(n) 对于全体自然数成立。

在 Coq 中，可以通过 induction <目标>. 应用数学归纳法，它将命题拆分为两个分命题，要求分别在目标为 0 与 n^+ （此时命题对 n 成立）时证明命题。

Theorem plus_n_O:
  forall n: nat,
  n = plus n 0.
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl.
    rewrite <- IHn.
    reflexivity.
Qed.

特别注意那个 IHn，它是 Coq 为归纳的前提条件（即当目标为 n^+ 时 n = n + 0）自动起的名字。

（执行 induction 后分解为两个分命题）

（基准条件）

（归纳条件）

练习题. Ex 7. 证明一条引理：对于自然数 n, m，(n+m)^+ = n + m^+。

Theorem plus_n_Sm:
  forall n m: nat,
  S (plus n m) = plus n (S m).
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)

加法交换律. 对于自然数 n, m，n + m = m + n.

我们来借助 Coq 证明它。首先写下命题：

Theorem plus_comm:
  forall n m: nat,
  plus n m = plus m n.

尝试归纳：

Proof.
  intros n m.
  induction n.
  - simpl.

看到 CoqIde 给出的第一个分命题：

m = m + 0，正是之前我们证明过的命题 plus_n_O。在 Coq 中，我们可以使用已经证明的命题（也就是定理）进行重写。于是

    rewrite <- plus_n_O.
    reflexivity.

第一个分命题证明完毕。看第二个：

  - simpl.

尝试重写：

    rewrite -> IHn.

S (m + n) = m + S n 正是练习题中证明的引理 plus_n_Sm。重写，证毕。

    rewrite -> plus_n_Sm.
    reflexivity.
Qed.

完整的证明：

Theorem plus_comm:
  forall n m: nat,
  plus n m = plus m n.
Proof.
  intros n m.
  induction n.
  - simpl.
    rewrite <- plus_n_O.
    reflexivity.
  - simpl.
    rewrite -> IHn.
    rewrite -> plus_n_Sm.
    reflexivity.
Qed.

练习题. Ex 8. 证明加法结合律：对于自然数 n, m, p，n+m+p = n+(m+p)。

Theorem plus_assoc:
  forall n m p: nat,
  plus (plus n m) p = plus n (plus m p).
  (* Proof. ... Qed. 用你的证明替换掉这段注释吧。 *)

练习题答案

Ex. 1

Inductive weekday: Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Ex. 2

Definition orb (b c: bool): bool :=
  match b with
  | true => true
  | false => c
  end.
Definition xorb (b c: bool): bool :=
  match b with
  | true => negb c
  | false => c
  end.

Ex. 3

Theorem t_and_f_eq_f: (andb true false = false).
  Proof. reflexivity. Qed.
Theorem f_and_t_eq_f: (andb false true = false).
  Proof. reflexivity. Qed.
Theorem f_and_f_eq_f: (andb false false = false).
  Proof. reflexivity. Qed.

Ex. 4

Fixpoint mult (a b: nat): nat :=
  match a with
  | O => O
  | S a' => plus b (mult a' b)
  end.
Fixpoint eq (a b: nat): bool :=
  match a with
  | O =>
    match b with
    | O => true
    | S b' => false
    end
  | S a' =>
    match b with
    | O => false
    | S b' => eq a' b'
    end
  end.

Ex. 5

Theorem mult_S_1:
  forall (m n: nat),
  m = S n
  -> mult m (plus 1 n) = mult m m.
Proof.
  intros m n H.
  simpl.
  rewrite <- H.
  reflexivity.
Qed.

Ex. 6

Theorem andb_true_elim2:
  forall (b c: bool),
  andb b c = true
  -> c = true.
Proof.
  intros b c H.
  destruct b eqn: Eb.
  - simpl in H.
    rewrite <- H.
    reflexivity.
  - simpl in H.
    destruct c.
    + reflexivity.
    + rewrite -> H.
      reflexivity.
Qed.

Ex. 7

Theorem plus_n_Sm:
  forall n m: nat,
  S (plus n m) = plus n (S m).
Proof.
  intros n m.
  induction n.
  - reflexivity.
  - simpl.
    rewrite -> IHn.
    reflexivity.
Qed.

Ex. 8

Theorem plus_assoc:
  forall n m p: nat,
  plus (plus n m) p = plus n (plus m p).
Proof.
  intros n m p.
  induction n.
  - reflexivity.
  - simpl.
    rewrite -> IHn.
    reflexivity.
Qed.