形式验证的目标是，将一段程序的功能用另一段程序表达，并且再用另一段程序来表示该程序符合给定的功能要求。

表达程序的方式自然不必说；然而如何表达一项要求，如何将其证明，是我们在这篇文章里主要介绍的。

注意：本文中出现的所有代码块都可以串在一起执行，打开 coqtop 一条一条输入，或者把它们收集到 .v 文件里并且配合 CoqIDE / Proof General / VSCoq 食用。

归纳类型

最简单的数据类型莫过于 bool。它是这样定义的：

Inductive bool :=
| true : bool
| false : bool.

Inductive 告诉 Coq 让它创造一个新类型，名字叫 bool，它只有两个值，true 和 false。

Check true : bool.

Check 告诉 Coq 去检查一项是否类型良好，并给出它的类型（在这里我们显式指定了 true 只能是 bool，如果不是，这条命令就会报错；如果你去掉 : bool，Coq 也会告诉我们 true 是 bool）。

让我们来考虑更加复杂的数据类型，让我们想想看，例如二叉树怎么样？

Inductive binary_tree :=
| node : binary_tree -> binary_tree -> binary_tree
| leaf : binary_tree.

箭头 -> 的意思是左侧到右侧的函数，它右结合。例如，binary_tree -> binary_tree 是从二叉树到二叉树的函数。而 binary_tree -> (binary_tree -> binary_tree) 则是从二叉树到“二叉树到二叉树的函数”的函数。意思是，这个类型的项接受了一个参数以后会变成从二叉树到二叉树的函数，再接受一个参数就会变成二叉树。换言之这个类型代表接受两个二叉树给出一个二叉树的函数。

上述代码的意思是，binary_tree 有两个构造器，node 接受两个 binaty_tree 然后组成一个新的 binary_tree；而 leaf 是特殊的一个 binary_tree（我们认为所有的叶节点完全相同）。

Check node (node leaf (node leaf leaf)) leaf : binary_tree.

Check 这样大些开头的项是命令，它们的调用比函数调用的优先级低。

不过我们过会再讨论它。类似的，我们可以定义一种自然数：

Module mynat.
Inductive nat :=
| O : nat
| S : nat -> nat.

也就是说一个数要么是 0，要么是某个数的后继。

Check S (S O) : nat.

为了演示，我们在一个模组里创建这个定义并展示；另外一个和这个一样的，自带的定义中，Coq 会自动帮我们把这些很长的形式写成阿拉伯数字。

这些类型都是很简单的：它们只是有一些互斥的构造器，构造器可以有多个参数，也可以嵌套这些类型本身。这些构造器，是产生该类型的项的“根本”方式。实际上，我们刚刚创造的这些归纳类型也有它们的类型：

Check nat : Set.
Check nat : Type.

Set 是 Type 的子类型。

我们当然也可以显式地在定义处标上这些。

Inductive nat' : Set := O' : nat' | S' : nat' -> nat'.
End mynat.

接下来让我们看一些更有趣的归纳类型。

类型构造器

例如，我们想要元组。为了简单起见，让我们只考虑二元组：

Inductive prod : Type -> Type -> Type :=
  pair : forall A B, A -> B -> prod A B.

在这里我们就必须要标出 prod 的类型，不然编译器会认为 prod 是一个 Set。从我们使用 prod A B 编译器可以知道 A B 都是 Type 类型的。至于 forall 的用途我们可以一会再讨论。重点在于，我们定义了一个类型构造器，它不再是一个简单的类型，而是对应于 C++ 的模板，Java 的范型的东西：它接受两个类型，并且产生一个新的类型。

Check prod : Type -> Type -> Type.
Check prod nat binary_tree : Type.

而这个类型的项由 pair 产生。例如：

Check pair nat binary_tree 10 leaf : prod nat binary_tree.

注意，我们要重新指定一遍 pair 将会接受 nat 和 binary_tree。为了方便我们可以使用 Arguments 来让 Coq 自动推断应该在此处出现的类型：

Arguments pair {_ _} _ _. (* 自动推断前两个参数 *)
Check pair 233 233 : prod nat nat.

我们用 (* *) 来包裹注释。

类似地我们也可以定义一种列表类型：

Inductive list : Type -> Type :=
| nil : forall A, list A
| cons : forall A, A -> list A -> list A.

如何使用

我们有了表达数据的方式，让我们来看一下怎么表达计算方法。最重要的方式是使用 match ... with ... end，如下所示：

Definition pred (n : nat) :=
  match n with
  | O => O
  | S n' => n'
  end.

它在一个变量上做分类讨论，把变量对各个状况作匹配。Definition 可以定义一个新的常量（在这里是一个函数）。我们还可以定义如下：

Definition pred_pred (n : nat) := pred (pred n).
Definition two := S (S O).
Definition zero := pred_pred two.

pred_pred 中，在 := 左侧出现的 (n : nat) 绑定也可以移到右侧，采用 fun ... => ... 成为 lambda 形式：

Definition pred_pred' := fun n => pred (pred n).

Inductive 也可以用类似于 Definition 的方式把参数写在名字旁边。只要它的每个构造器类型头都有一个公共的 forall ..., 我们就可以把它提到整个类型的头部。

Inductive prod' (A B : Type) :=
  pair' : A -> B -> prod' A B.
  
Inductive list' (A : Type) :=
| nil' : list' A
| cons' : A -> list' A -> list' A.

你也可以注意到 Coq 这样就可以自行推断 prod list 的类型，而不需要我们显式标注了。

说回 match，它的功能就是把项分成多种情况讨论，“拆解”该项。我们还可以写出这样的函数：

Definition fst {A B : Type} (p : prod A B) :=
  match p with
  | pair a b => a
  end.
  
Definition snd {A B : Type} (p : prod A B) :=
  match p with
  | pair a b => b
  end.
  
Definition andb (x y : bool) :=
  match x with
  | false => false
  | true => match y with
            | false => false
			| true => true
			end
  end.
  
Notation "a && b" := (andb a b). (* 告诉 Coq 我们将采用 && 的中缀简便记法 *)

Notation 会让 Coq 把右侧的模式打印成左侧的符号表达。参数列表中用花括号包裹的（就像我们用 Arguments 一样）参数，Coq 会在调用的时候隐式推导它们。

不过问题是，Definition 不能递归。这是个严重的问题，如果不能递归的话很多函数就都写不出来了！如果想要递归的话，用 Fixpoint 代替 Definition。Coq 的特点就是它所有的项都是“全”的，也就是它们都会停机。所以 Coq 必须要保证递归的时候有一个终止条件，以及这个终止条件中引用的项是“下降”的。不过不必太担心，我们构造的良好程序都能通过 Coq 的检查。一部分有些问题的程序也可以用其他方式实现。

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

Notation "a + b" := (plus a b).

你可以注意到上述例子里交换 plus a' b 为 plus b a' 也会实现同样的功能，把两个自然数加在一起，但是 Coq 会提出错误，它觉得这个函数没法终止。

此外，你可以使用 Print 命令来让 Coq 打印一项的定义。

Print plus.

(* ==>
plus = 
fix plus (a b : nat) {struct a} : nat :=
  match a return nat with
  | O => b
  | S a' => S (plus a' b)
  end
     : forall (_ : nat) (_ : nat), nat

Argument scopes are [nat_scope nat_scope]
*)

形式证明

我们已经了解了一些构造数据类型以及在上面写函数的方法，现在我们来了解一下如何表达这些数据类型上的约束并证明它们吧。

本质上，我们会先引入一个叫做 eq 的黑箱子，它代表了两个值相等。

Theorem one_is_one :
  1 = 1.

此处的等号就是 eq；1 = 1 就是 eq 1 1。如果你 Check 1 = 1，Coq 会告诉你它是 Prop，也就是一个命题。在 Theorem 提出以后，Coq 会进入证明模式，并提示当前的子目标。1 = 1 看起来非常显然，但我们还是要对 Coq 给出它成立的证据。接下来我们使用策略 reflexivity：

  reflexivity.

你可以把策略当作一种只能在证明模式中使用的命令（当然实际用途不止于此）。reflexivity 试着让等号两侧一起化简，然后如果它们一样的话就终止当前目标（“因为两边对称，当前目标证明完毕”）。你会发现 Coq 告诉我们没有更多的子目标，证明可以完成了。于是我们使用

Qed.

来结束这个证明。

不过这也太显然了。让我们来试试更有趣的：

Theorem O_plus_n : forall n,
  0 + n = n.

forall 的意思在此处可以直接理解为“对于所有的 n”，它作为命题的变量出现。

在做这个证明的时候首先我们需要引入变量，因为命题讨论的是所有的自然数 n，我们得讨论如果有一个具体的 n 的情况。我们使用

  intros.

这时 n 被移到横线上方成为上下文的一部分，接下来我们证明这个目标。

  simpl.

simpl 把当前的命题化简，这样我们就可以把 0 + n 换成 n。接下来我们只需要说明 n = n 了，像我们刚刚做的那样：

  reflexivity.
Qed.

再例如我们来讨论一个关于 bool 的命题：

Theorem andb_true : forall b,
   b && true = b.
  intros.
  simpl.

Coq 的提示没有改变，因为我们并不知道 b 到底是 true 还是 false。这个时候我们必须要在它上面分类讨论才能解决问题：

  destruct b.

destruct 分解当前上下文里的某个项。它做的事情是为该项的每个构造器生成一个子目标，每个子目标里这一项被替换成它对应的构造器和构造器的参数。构造器的参数会被加入到上下文里。听起来挺复杂的；现在，它只是把 b 分类讨论为 true 和 false，

我们现在有两个子目标了。最好用花括号来组织你的证明，用左花括号来“聚焦”一个目标，然后用右花括号来结束聚焦。

{
  simpl.
  reflexivity.
}
{
  simpl.
  reflexivity.
}

证明对象

不过为什么这些策略能正确地工作？它们的原理到底是什么？实际上，一个证明过程，由 Theorem 开始，到 Qed 结束，合起来定义了一个“证明对象”，它也是合法的 Coq 项。

Print O_plus_n.

(* ==>
O_plus_n = fun n : nat => eq_refl
     : forall n : nat, 0 + n = n

Argument scope is [nat_scope]
*)

Print andb_true.

(* ==>
fun b : bool => if b as b0 return (b0 && true = b0) then eq_refl else eq_refl
     : forall b : bool, b && true = b

Argument scope is [bool_scope]
*)

不过这些都是什么意思？实际上，你可以注意到，冒号后面就是这个命题的内容。命题的内容作为类型，前面这一堆乱七八糟的东西具有这个类型。为了详细解释这种关系，让我们来引入一种比较简单的情形分析。

Inductive even : nat -> Prop :=
| even_O : even 0
| even_SS : forall m, even m -> even (S (S m)).

Arguments even_SS {_} _. (* 自动推断第一个参数 *)

暂时，even_SS 里的箭头可以理解为“推出”的意思（假设我们认为命题里的箭头是特殊的），它代表左边是前提条件，右边是结论的一个“高阶”命题。

上述定义的意思是，even 是 nat 到 Prop 的属性（它是一个依赖类型）。even n，对于任何一个自然数 n，是一个命题，指出 n 是偶数。定义指出，构造器 even_O 是 even 0 类型的（请注意这两者虽然长得像但是前者是后者的类型），而 even_SS 则是一个从 even m 中生成 even (S (S m)) 的构造器。这两个构造器也是命题，但是无条件成立，类似于为了指出什么是偶数的公理。你可以想见，首先我们知道 0 是一个偶数，并且如果我们知道任何一个 m 是偶数，就也可以知道 S (S m) 也是个偶数。这，是我们对偶数的定义方式。也就是说，even 0 是一个命题，even 1 是一个命题（虽然它不是真的），even 2 是一个命题（显然可以用“0 是偶数”在“m 是偶数则 S (S m) 是偶数”中推出），even 3，……

例如，我们可以证明 even 4。

Theorem even_4 : even 4.
  constructor.
  constructor.
  constructor.
Qed.

当我们每次使用 constructor 策略的时候，Coq 试着用构造器之一来匹配当前目标。成功和构造器匹配了以后，它会结束子目标并且生成所有的（在这里是一个）构造器需要的前提条件作为新的子目标。也就是说，even 4 的前提是 even 2，even 2 的前提是 even 0，even 0 没有前提（所以 constructor 直接结束了当前的子目标）。

接下来是更加有趣的环节：让我们 Print even_4 ：

Print even_4.

(* ==>
even_4 = even_SS (even_SS even_O)
     : even 4
*)

看看我们得到了什么！even_4 的类型就是 even 4，和我们在定理开始的时候声明的一样，并且 Coq 告诉我们，它的定义就是 even_SS (even_SS even_O)。实际上，even_SS 也是可以理解为一种函数：它接受一个类型是 even m 的命题，并且给我们 even (S (S m)) 的命题。even_O 的类型是 even 0, 它应用于 even_SS 以后变成了 even 2 的，再应用以后就得到了 even 4 的对象，也就是我们要证明的。我们成功地构造了该类型的对象而完成了这个证明。所以 even_O even_SS even_O 这些对象其实是命题的证据。很明显地，我们也可以构造 even 6 的证据，就是 even_SS even_4。

实际上，命题就是类型，证明就是这些类型的项。我们可以进一步找到 Coq 项和大部分常见逻辑算子的关系。

合取

Inductive and (A B : Prop) : Prop :=
| conj : A -> B -> and A B.

Arguments conj {_ _} _ _.

Notation "A /\ B" := (and A B) : type_scope.

让我们来用它证明 even 4 并且 even 6。

Theorem even_4_and_6 : even 4 /\ even 6.
  split. {
    apply even_4.
  }
  {
    constructor.
    apply even_4.
  }
Qed.

split 是 constructor 的一种特例，不过你应该只用它来拆解 and（实际上之前提到的 reflexivity 也是 constructor 的特例）。apply 是对当前目标应用一个命题。也就是，把当前目标与命题结论匹配，并且生成内容是前提的子目标。constructor 就是自动找到应用的命题：符合当前情况的构造器。例如此处的 constructor 其实就是 apply SS_eval。

Print even_4_and_6.
(* ==>
even_4_and_6 = conj even_4 (even_SS even_4)
     : even 4 /\ even 6
*)

同样的，even 4 /\ even 6 的证据是，通过构造器来结合 even 4 和 even 6 的证据。你可以发现这和我们之前表述的 pair 和 prod 其实几乎是一回事。

不过区别在于，Prop 和 Set 都是 Type 的子类型，然而前两者并不互相兼容。也就是，你不能把是 Set 的类型填入应该是 Prop 的位置，反过来也不行；然而两者都可以填入应该是 Type 的位置。

蕴含

蕴含对应的类型是函数，而对应的项是 lambda。“A 蕴含 B” 的想法就是，你给我 A 的证据我就能生成 B 的证据。例如，

Theorem and_proj1 : forall A B,
  A /\ B -> A.
  intros.

这个时候 Coq 生成了名为 H 的上下文，它的名字意思大概是“假设”。虽然它有确定的类型，Coq 还是需要指示来分析这个类型的各种（虽然只有一种）情况。

  destruct H.
  apply H.
Qed.

destruct 把 H （只）匹配到 conj 上分解成了新的 H 和 H0 并加入当前上下文作为假设。assumption 在当前上下文里寻找和目标一致的假设（A 成立的证据）并且用它来结束目标（“既然我们的假设里就有这条，结论当然只要用这个假设就可以了”）。

Print and_proj1.

(* ==>
and_proj1 = 
fun (A B : Prop) (H : A /\ B) => match H with
                                 | conj H0 _ => H0
                                 end
     : forall A B : Prop, A /\ B -> A

Argument scopes are [type_scope type_scope _]
*)

你可以注意到 destruct 和 match ... with ... end 相对应，intros 和 fun 相对应。实际上，证明过程的前后顺序代表着一种“填洞”的逻辑关系：在证明的一开始，Coq 只知道我们需要一项 forall A B : Prop, A /\ B -> A；

Theorem and_proj1' : forall A B,
  A /\ B -> A.
Show Proof.
(* ==>
?Goal
*)

Show Proof 展示当前生成的证明对象。当前的目标 ?Goal 是一个“存在变量”，或者在别的语言里也叫“洞”。我们证明的过程就是不断地试着填这个洞。

使用了 intros 以后 Coq 生成了

  intros.
Show Proof.
(* ==>
(fun (A B : Prop) (H : A /\ B) => ?Goal)
*)

并推论空缺的位置应该有类型 A；当我们使用 destruct H 的时候，Coq 在 H 上做 match；H 只可能是 conj H0 H1 ，我们得到了

  destruct H.
Show Proof.
(* ==>
(fun (A B : Prop) (H : A /\ B) =>
 match H with
 | conj H0 H1 => ?Goal@{H:=H0; H0:=H1}
 end)
*)

?Goal@{H:=H0; H0:=H1} 在这里表示它将把 ?Goal 中 H 换成 H0，H0 换成 H1，因为我们在 destruct 的时候把 H 覆盖掉了，这里要做个重命名。

空缺的类型仍然是A；最后使用 assumption 时，Coq 认为 H0 （证明中的 H） 符合条件，就把它填上，我们就获得了没有空缺的一整个证据。

  assumption.
Show Proof.
(* ==>
(fun (A B : Prop) (H : A /\ B) => match H with
                                  | conj H0 _ => H0
                                  end)
*)
Qed.

因为 H1 没有用上，Coq 用通配符 _ 取代了它。

在之前和之后的例子里都调用 Show Proof 来体验一下生成证明对象的过程吧。

析取

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> or A B
| or_intror : B -> or A B.

Arguments or_introl {_ _} _.
Arguments or_intror {_ _} _.

Notation "A \/ B" := (or A B) : type_scope.

你可能会想到这里的记号有优先级问题，不过其实 Coq.Logic 里面已经定义了这个符号，我们覆盖它的时候可以继承原来的优先级关系。

考虑这两个构造器。or_introl 接受一个 A 的证据，生成 A \/ B，而 or_intror 则从 B 生成 A \/ B，分别对应析取左侧成立和右侧成立的情况。

Theorem and_or_distr : forall A B C,
  A /\ (B \/ C) ->
  A /\ B \/ A /\ C.
  intros.
  destruct H.

接下来我们要做的事情是在生成的 H0 做 destruct，它是 B \/ C 的证据，所以你可以想见它要么来自某个 B 的证据，要么来自某个 C 的。destruct 会分类讨论它们（也就会生成两个目标）。

  destruct H0. {

第一个目标里，H0 是 B 的证据。我们要证明 A /\ B \/ A /\ C 应该要提供 A /\ B 的证据（因为这种情况下你没有 C 的证据）。

    left.

constructor 在这种情形下并没法推断哪个构造器才是合理的：很明显，or 的两个构造器的结论都是一样的。我们使用 left 来选择从 or_introl 生成（等一下我们会用 right 选择 or_intror 来生成）当前需要的证明目标。从表面来看，它做了个二选一，决定我们通过证明左边部分来证明整体。

证明目标变成了 A /\ B；我们可以用之前的办法，采用 split 和 assumption 来证明。不过我个人更喜欢更简短的方式：我们自己来构造一个 A /\ B 的证明对象并且应用它。

    apply (conj H H0).
  }
  {

这个目标解决了以后我们再用类似的目标做第二种情况，这种情况下我们只有 A 和 C。

    right.
    apply (conj H H0).
  }
Qed.

否定

这可能是构造逻辑中最难以理解，让人混乱的部分。首先，

Inductive False : Prop :=.

这是什么意思？我们定义了一个没有构造器的归纳类型。或者说，这个类型中没有任何合法的项，它是一个空的类型。

Definition not (A : Prop) : Prop := 
  A -> False.
  
Notation "~ A" := (not A) : type_scope.

这又是什么意思？我们指出，命题 A 的否定就是 A -> False。如果我们能从 A 构造 False 就可以证明 A 的否定。反过来，如果我们有 A 的否定，我们就可以从任何 A 得到 False。

Theorem noncontradiction : forall A,
  ~ (A /\ ~ A).
  intros.

要继续证明这个目标成立，我们需要从 not 的定义出发。

  unfold not.
  intros.

unfold 可以把当前的某一个函数展开成它的定义，从而允许我们进一步分析它里面发生了些什么。unfold 以后，你可以看到我们的目标又变成了“从 A /\ (A -> False) 证明 False”，于是我们用 intros 来把前提移到上下文里。

可是我们刚刚对 False 的定义就指出它不能被构造，所以我们的目标是把它替换成别的东西再证明，抑或是在当前上下文里找到矛盾。

  destruct H.

现在我们有了一个可以通过 A 推出 False 的假设，我们应用它就可以把当前目标变成 A。

  apply H0.
  assumption.
Qed.

再来看另外一个例子：

Theorem ex_falso_quodlibet : forall A,
  False -> A.
  intros.
  destruct H.
Qed.

发生了什么？ destruct H 为什么直接结束了这个子目标？

Print ex_falso_quodlibet.

(* ==>
fun (A : Type) (H : False) => match H return A with
                              end
     : forall A : Type, False -> A

Argument scopes are [type_scope _]
*)

这个 match 没有任何分支，不过多了一个描述返回类型的 return A。考虑一下，destruct H 就是分类讨论 H，然而这个分类讨论的东西没有任何一个情形可供讨论。如果我们从每个情况都能推出 A，整个分类讨论就可以代表 H 能推出 A。然而实际上，这里的“每个情况”连一个都没有，其实也算一种“都能推出 A”的情形。就像我们可以描述“在火星上出生的猪都会飞”，当然“火星上出生的猪”暂时一头也没有，你说它们能干什么都是合乎逻辑的。

Theorem double_neg : forall A : Prop,
  A -> ~ ~ A.
  intros.
  unfold not.
  intros.
  apply H0.
  assumption.
Qed.

不过 Coq 里默认只允许直觉逻辑，经典逻辑中有著名的“排中律”，它指出一个命题要么是真的，要么是假的。所以这个系统不适用“反证法”。

（待续……）

本文 .v 文件下载在此处。