【形式化】Coq 中的函数式编程基础（长文）

在这里插入图片描述

引言

函数式编程风格建立在简单且日常的数学直觉之上：如果一个程序或方法没有副作用，那么（忽略效率问题）我们只需要了解它如何将输入映射到输出——也就是说，我们可以把它看作是计算一个数学函数的具体方法。这就是“函数式编程”中“函数式”的其中一层含义。程序与简单数学对象之间的直接联系，既支持形式化的正确性证明，也有助于对程序行为进行合理的非正式推理。

函数式编程“函数式”的另一层含义是，它强调将函数作为一等公民——即可以作为参数传递给其他函数、作为结果返回、包含在数据结构中的值。认识到函数可以被当作数据来处理，催生了许多有用且强大的编程惯用法。

函数式语言的其他常见特性包括代数数据类型和模式匹配，它们使得构建和操作复杂的数据结构变得容易，还有支持抽象和代码复用的多态类型系统。Coq 具备所有这些特性。

本章的前半部分将介绍 Coq 原生函数式编程语言 Gallina 中最重要的元素。后半部分将介绍一些用于证明 Gallina 程序性质的基本策略。

数据和函数

枚举类型

Coq 值得注意的一点是，它的内置特性集非常小。例如，Coq 没有提供常见的原子数据类型（布尔值、整数、字符串等），而是提供了一种强大的机制，可以从头开始定义新的数据类型，上述这些常见类型都可以作为其具体实例。

当然，Coq 发行版附带了一个广泛的标准库，其中提供了布尔值、数字以及许多常见数据结构（如列表和哈希表）的定义。但这些库定义并没有什么神奇或原始的地方。为了说明这一点，在本课程中，我们将明确重新定义（几乎）所有我们需要的定义，而不是从标准库中获取它们。

一周的天数
为了了解这种定义机制是如何工作的，让我们从一个非常简单的例子开始。以下声明告诉 Coq，我们正在定义一组数据值——一种类型。

coq">Inductive day : Type :=| monday| tuesday| wednesday| thursday| friday| saturday| sunday.

这个新类型叫做 day，它的成员有 monday、tuesday 等等。

定义了 day 之后，我们可以编写对这些日期进行操作的函数。

coq">Definition next_working_day (d:day) : day :=match d with| monday ⇒ tuesday| tuesday ⇒ wednesday| wednesday ⇒ thursday| thursday ⇒ friday| friday ⇒ monday| saturday ⇒ monday| sunday ⇒ mondayend.

注意，这个函数的参数和返回类型在这里都有明确声明。和大多数函数式编程语言一样，当没有明确给出类型时，Coq 通常可以自己推断出这些类型——即它可以进行类型推断——但我们通常会包含这些类型，以便于阅读。

定义了一个函数后，我们可以检查它在一些例子上的工作情况。在 Coq 中，实际上有三种不同的方式来进行示例测试。
首先，我们可以使用 Compute 命令来计算一个涉及 next_working_day 的复合表达式。

coq">Compute (next_working_day friday).
(* ==> monday : day *)
Compute (next_working_day (next_working_day saturday)).
(* ==> tuesday : day *)

（我们在注释中显示 Coq 的响应；如果你手头有电脑，这将是一个绝佳的时机，在你喜欢的 IDE 下启动 Coq 解释器（有关安装说明，请参阅前言）并亲自尝试一下。从本书的 Coq 源代码中加载 Basics.v 文件，找到上述示例，将其提交给 Coq，并观察结果。）

其次，我们可以以 Coq 示例的形式记录我们期望的结果：

coq">Example test_next_working_day:(next_working_day (next_working_day saturday)) = tuesday.

这个声明做了两件事：它提出了一个断言（即周六之后的第二个工作日是周二），并且给这个断言起了一个名字，以便以后可以引用它。提出断言后，我们也可以让 Coq 像这样验证它：

coq">Proof. simpl. reflexivity. Qed.

目前细节并不重要，但本质上这个小脚本可以理解为 “我们刚刚提出的断言可以通过观察等式两边计算结果相同来证明”。

第三，我们可以让 Coq 从我们的 Definition 中提取出用更传统的编程语言（OCaml、Scheme 或 Haskell）编写的程序，这些语言有高性能的编译器。这个功能非常有用，因为它为我们提供了一条从用 Gallina 编写的已证明正确的算法到高效机器代码的途径。
（当然，我们要相信 OCaml/Haskell/Scheme 编译器以及 Coq 的提取功能本身的正确性，但这仍然比当今大多数软件开发方式有了很大的进步！）
实际上，这也是开发 Coq 的主要用途之一。我们将在后面的章节中回到这个话题。

下一行的 Require Export 语句告诉 Coq 使用标准库中的 String 模块。我们将在后面的章节中用字符串做各种事情，但我们在这里需要 Require 它，以便评分脚本可以在内部使用它。

coq">From Coq Require Export String.

布尔值
按照上面一周天数的模式，我们可以定义标准的布尔类型 bool，其成员为 true 和 false。

coq">Inductive bool : Type :=| true| false.

布尔值上的函数可以用与上面相同的方式定义：

coq">Definition negb (b:bool) : bool :=match b with| true ⇒ false| false ⇒ trueend.Definition andb (b1:bool) (b2:bool) : bool :=match b1 with| true ⇒ b2| false ⇒ falseend.Definition orb (b1:bool) (b2:bool) : bool :=match b1 with| true ⇒ true| false ⇒ b2end.

（虽然我们在这里从头开始构建布尔值，但 Coq 当然提供了布尔值的默认实现，以及大量有用的函数和引理。只要可能，我们会给我们自己的定义和定理起与标准库中相同的名字。）

后两个定义展示了 Coq 中多参数函数定义的语法。相应的多参数应用语法通过以下 “单元测试” 进行说明，这些测试构成了 orb 函数的完整真值表：

coq">Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.

我们还可以为刚刚定义的布尔运算引入一些常见的中缀语法。Notation 命令为现有的定义定义了一种新的符号表示法。

coq">Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

关于符号表示的说明：在 .v 文件中，我们使用方括号来分隔注释中的 Coq 代码片段；这个约定也被 coqdoc 文档工具使用，它使这些代码片段在视觉上与周围的文本区分开来。在文件的 HTML 版本中，这些文本片段会以不同的字体显示。

这些例子也是介绍 Coq 编程语言的另一个小特性的机会：条件表达式…

coq">Definition negb' (b:bool) : bool :=if b then falseelse true.Definition andb' (b1:bool) (b2:bool) : bool :=if b1 then b2else false.Definition orb' (b1:bool) (b2:bool) : bool :=if b1 then trueelse b2.

Coq 的条件表达式与其他任何语言中的条件表达式完全一样，只是有一个小的扩展：
由于 bool 类型不是内置的，Coq 实际上支持对任何归纳定义的类型进行条件表达式操作，只要该类型的定义中恰好有两个子句。如果条件表达式的值计算为 Inductive 定义的第一个子句的 “构造函数”（在这种情况下恰好称为 true），则认为条件为真；如果计算为第二个子句，则认为条件为假。

例如，我们可以定义以下数据类型 bw，它有两个构造函数分别代表黑色（b）和白色（w），并定义一个函数 invert，使用条件表达式来反转该类型的值。

coq">Inductive bw : Type :=| bw_black| bw_white.Definition invert (x: bw) : bw :=if x then bw_whiteelse bw_black.Compute (invert bw_black).
(* ==> bw_white : bw *)
Compute (invert bw_white).
(* ==> bw_black : bw *)

练习：1 星，标准难度（nandb）
Admitted 命令可以用作未完成证明的占位符。我们在练习中使用它来表示留给你的部分——即你的任务是用真正的证明替换 Admitted。

删除 “Admitted.” 并完成以下函数的定义；然后确保下面的 Example 断言都可以由 Coq 验证。（即，按照上面 orb 测试的模式填写每个证明，并确保 Coq 接受它。）该函数应该在其一个或两个输入为 false 时返回 true。

提示：如果在你的证明中 simpl 无法简化目标，可能是因为你在定义 nandb 时没有使用 match 表达式。尝试用不同的方式定义 nandb，或者直接跳过 simpl 并使用 reflexivity。我们将在本章后面解释这种现象。

coq">Definition nandb (b1:bool) (b2:bool) : bool(* 用 ":= _你的定义_ ." 替换这一行 *) Admitted.Example test_nandb1: (nandb true false) = true.
(* 在此处填写证明 *) Admitted.Example test_nandb2: (nandb false false) = true.
(* 在此处填写证明 *) Admitted.Example test_nandb3: (nandb false true) = true.
(* 在此处填写证明 *) Admitted.Example test_nandb4: (nandb true true) = false.
(* 在此处填写证明 *) Admitted.

练习：1 星，标准难度（andb3）
对下面的 andb3 函数执行相同的操作。该函数应该在其所有输入都为 true 时返回 true，否则返回 false。

coq">Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool(* 用 ":= _你的定义_ ." 替换这一行 *) Admitted.Example test_andb31: (andb3 true true true) = true.
(* 在此处填写证明 *) Admitted.Example test_andb32: (andb3 false true true) = false.
(* 在此处填写证明 *) Admitted.Example test_andb33: (andb3 true false true) = false.
(* 在此处填写证明 *) Admitted.Example test_andb34: (andb3 true true false) = false.
(* 在此处填写证明 *) Admitted.

类型

Coq 中的每个表达式都有一个类型，描述它计算的是什么样的东西。Check 命令要求 Coq 打印一个表达式的类型。

coq">Check true.
(* ===> true : bool *)

如果 Check 后面的东西跟着一个冒号和一个类型声明，Coq 将验证表达式的类型是否与给定的类型匹配，如果不匹配则会报错并停止。

coq">Check true: bool.Check (negb true): bool.

像 negb 这样的函数本身也是数据值，就像 true 和 false 一样。它们的类型称为函数类型，用箭头表示。

coq">Check negb: bool → bool.

negb 的类型写作 bool → bool，读作 “布尔箭头布尔”，可以理解为 “给定一个布尔类型的输入，这个函数产生一个布尔类型的输出”。类似地，andb 的类型写作 bool → bool → bool，可以理解为 “给定两个布尔类型的输入，这个函数产生一个布尔类型的输出”。

从旧类型创建新类型

到目前为止，我们定义的类型都是 “枚举类型” 的例子：它们的定义明确列举了一组有限的元素，称为构造函数。这里有一个更有趣的类型定义，其中一个构造函数带有一个参数：

coq">Inductive rgb : Type :=| red| green| blue.Inductive color : Type :=| black| white| primary (p : rgb).

让我们更详细地看一下。

一个 Inductive 定义做了两件事：

它定义了一组新的构造函数。例如，red、primary、true、false、monday 等都是构造函数。
它将它们组合成一个新的命名类型，如 bool、rgb 或 color。

构造函数表达式是通过将构造函数应用于零个或多个其他构造函数或构造函数表达式而形成的，要遵循构造函数参数声明的数量和类型。例如，这些是有效的构造函数表达式…

coq">red
true
primary red

…但这些不是：

coq">red primary
true red
primary (primary red)

特别是，rgb 和 color 的定义说明了哪些构造函数表达式属于 rgb 和 color 集合：

red、green 和 blue 属于 rgb 集合；
black 和 white 属于 color 集合；
如果 p 是属于 rgb 集合的构造函数表达式，那么 primary p（“构造函数 primary 应用于参数 p”）是属于 color 集合的构造函数表达式；
以这些方式形成的构造函数表达式是属于 rgb 和 color 集合的唯一表达式。

我们可以像对 day 和 bool 那样，使用模式匹配来定义对颜色的函数。

coq">Definition monochrome (c : color) : bool :=match c with| black ⇒ true| white ⇒ true| primary p ⇒ falseend.

由于 primary 构造函数带有一个参数，匹配 primary 的模式应该包含一个变量，就像我们刚刚做的那样（注意我们可以自由选择它的名称），或者是一个合适类型的常量（如下所示）。

coq">Definition isred (c : color) : bool :=match c with| black ⇒ false| white ⇒ false| primary red ⇒ true| primary _ ⇒ falseend.

这里的模式 “primary _” 是 “构造函数 primary 应用于除 red 之外的任何 rgb 构造函数” 的简写。
（通配符模式 _ 与 monochrome 定义中的哑元模式变量 p 具有相同的效果。）

模块
Coq 提供了一个模块系统来帮助组织大型开发项目。我们不需要它的大部分功能，但这里有一个很有用：如果我们将一组声明放在 Module X 和 End X 标记之间，那么在 End 之后的文件其余部分中，这些定义将以 X.foo 这样的名称引用，而不是仅仅 foo。我们将使用这个功能来限制定义的作用域，这样我们就可以自由地重用名称。

coq">Module Playground.Definition foo : rgb := blue.
End Playground.Definition foo : bool := true.Check Playground.foo : rgb.
Check foo : bool.

元组

coq">Module TuplePlayground.

一个带有多个参数的单一构造函数可以用来创建一个元组类型。例如，考虑表示一个半字节（4 位）中的四个比特。我们首先定义一个类似于 bool 的数据类型 bit（使用构造函数 B0 和 B1 表示两个可能的比特值），然后定义数据类型 nybble，它本质上是四个比特的元组。

coq">Inductive bit : Type :=| B1| B0.Inductive nybble : Type :=| bits (b0 b1 b2 b3 : bit).Check (bits B1 B0 B1 B0): nybble.

bits 构造函数充当其内容的包装器。可以通过模式匹配来展开它，如下述 all_zero 函数所示，该函数测试一个半字节的所有比特是否都是 B0。
我们使用下划线 (_) 作为通配符模式，以避免发明不会被使用的变量名。

coq">Definition all_zero (nb : nybble) : bool :=match nb with| (bits B0 B0 B0 B0) ⇒ true| (bits _ _ _ _) ⇒ falseend.Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : bool *)
End TuplePlayground.

数字
我们将这部分放在一个模块中，这样我们自己对自然数的定义就不会与标准库中的定义冲突。在本书的其余部分，我们将使用标准库中的定义。

coq">Module NatPlayground.

到目前为止，我们定义的所有类型——包括像 day、bool 和 bit 这样的 “枚举类型”，以及由它们构建的像 nybble 这样的元组类型——都是有限的。另一方面，自然数是一个无限集合，所以我们需要使用一种稍微更丰富的类型声明形式来表示它们。

有许多表示数字的方式可供选择。你几乎肯定最熟悉十进制表示法（以 10 为基数），使用 0 到 9 的数字，例如，组成数字 123。你很可能也遇到过十六进制表示法（以 16 为基数），在这种表示法中，相同的数字表示为 7B，或者八进制（以 8 为基数），表示为 173，或者二进制（以 2 为基数），表示为 1111011。使用枚举类型来表示数字，我们可以使用这些表示法中的任何一种来表示自然数。实际上，在某些情况下，这些选择中的每一种都很有用。

二进制表示法在计算机硬件中很有价值，因为数字可以只用两种不同的电压电平来表示，从而产生简单的电路。类似地，我们在这里希望选择一种使证明更简单的表示法。

实际上，有一种比二进制更简单的数字表示法，即一元（以 1 为基数），在这种表示法中只使用一个数字（就像我们的祖先可能在洞穴墙壁上划痕来计算天数一样）。为了用 Coq 数据类型表示一元数，我们使用两个构造函数。大写字母 O 构造函数表示零。S 构造函数可以应用于自然数 n 的表示，得到 n + 1 的表示，其中 S 代表 “后继”（或 “划痕”）。以下是完整的数据类型定义：

coq">Inductive nat : Type :=| O| S (n : nat).

根据这个定义，0 用 O 表示，1 用 S O 表示，2 用 S (S O) 表示，依此类推。

非正式地，定义的子句可以这样理解：

O 是一个自然数（记住这是字母 “O”，而不是数字 “0”）。
S 可以放在一个自然数前面得到另一个自然数——即，如果 n 是一个自然数，那么 S n 也是。

同样，让我们更仔细地看一下。nat 的定义说明了 nat 集合中的表达式是如何构建的：

构造函数表达式 O 属于 nat 集合；
如果 n 是属于 nat 集合的构造函数表达式，那么 S n 也是属于 nat 集合的构造函数表达式；
以这两种方式形成的构造函数表达式是属于 nat 集合的唯一表达式。

这些条件是我们给 Coq 的 Inductive 声明的确切含义。它们意味着构造函数表达式 O、构造函数表达式 S O、构造函数表达式 S (S O)、构造函数表达式 S (S (S O)) 等等都属于 nat 集合，而其他构造函数表达式，如 true、andb true false、S (S false) 和 O (O (O S)) 则不属于。

这里的一个关键点是，到目前为止我们所做的只是定义了一种数字的表示法：一种写下它们的方式。O 和 S 的名称是任意的，在这一点上它们没有特殊的含义——它们只是我们可以用来写下数字的两个不同的标记，再加上一条规则，即任何 nat 都将写成一些 S 标记后面跟着一个 O 的字符串。如果我们愿意，我们可以用以下方式写出本质上相同的定义：

coq">Inductive otherNat : Type :=| stop| tick (foo : otherNat).

这些标记的解释来自于我们如何使用它们进行计算。

我们可以通过编写对自然数表示进行模式匹配的函数来实现这一点，就像我们上面对布尔值和日期所做的那样——例如，下面是前驱函数：

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

第二个分支可以理解为：“如果 n 的形式是 S n'，其中 n' 是某个数，那么返回 n'”。

以下的 End 命令关闭当前模块，因此 nat 将重新引用标准库中的类型。

coq">End NatPlayground.

因为自然数是一种非常常见的数据类型，Coq 确实为解析和打印它们提供了一点内置的便利：普通的十进制数字可以作为构造函数 S 和 O 定义的 “一元” 表示法的替代。Coq 默认以十进制形式打印数字：

coq">Check (S (S (S (S O)))).
(* ===> 4 : nat *)Definition minustwo (n : nat) : nat :=match n with| O ⇒ O| S O ⇒ O| S (S n') ⇒ n'end.Compute (minustwo 4).
(* ===> 2 : nat *)

构造函数 S 的类型是 nat → nat，就像 pred 和 minustwo 等函数一样：

coq">Check S : nat → nat.
Check pred : nat → nat.
Check minustwo : nat → nat.

这些都是可以应用于一个数字以得到另一个数字的东西。然而，S 和其他两个有一个根本的区别：像 pred 和 minustwo 这样的函数是通过给出计算规则来定义的——例如，pred 的定义说 pred 2 可以简化为 1——而 S 的定义没有这样的行为。虽然它在可以应用于一个参数的意义上类似于一个函数，但它实际上什么也不做！它只是一种写下数字的方式。

想想标准的十进制数字：数字 1 不是一个计算；它是一块数据。当我们写 111 表示数字一百一十一时，我们使用了 1 三次来写下一个数字的具体表示。

让我们继续定义更多关于数字的函数。

对于大多数涉及数字的有趣计算，简单的模式匹配是不够的：我们还需要递归。例如，要检查一个数字 n 是否为偶数，我们可能需要递归地检查 n - 2 是否为偶数。这类函数使用关键字 Fixpoint 而不是 Definition 来引入。

coq">Fixpoint even (n:nat) : bool :=match n with| O ⇒ true| S O ⇒ false| S (S n') ⇒ even n'end.

我们可以通过类似的 Fixpoint 声明来定义 odd 函数，但这里有一个更简单的方法：

coq">Definition odd (n:nat) : bool :=negb (even n).Example test_odd1: odd 1 = true.
Proof. simpl. reflexivity. Qed.Example test_odd2: odd 4 = false.
Proof. simpl. reflexivity. Qed.

（如果你逐步执行这些证明，你可能会注意到 simpl 实际上对目标没有影响——所有的工作都由 reflexivity 完成。我们很快会讨论原因。）

自然地，我们也可以通过递归定义多参数函数。

coq">Module NatPlayground2.Fixpoint plus (n : nat) (m : nat) : nat :=match n with| O ⇒ m| S n' ⇒ S (plus n' m)end.

2 加 3 等于 5（呼！）：

coq">Compute (plus 3 2).
(* ===> 5 : nat *)

Coq 在这里执行的简化步骤可以可视化如下：

(*      plus 3 2即 plus (S (S (S O))) (S (S O))==> S (plus (S (S O)) (S (S O)))根据 match 的第二个子句==> S (S (plus (S O) (S (S O))))根据 match 的第二个子句==> S (S (S (plus O (S (S O)))))根据 match 的第二个子句==> S (S (S (S (S O))))根据 match 的第一个子句即 5  *)

作为一种符号上的便利，如果两个或多个参数具有相同的类型，它们可以一起写。在以下定义中，(n m : nat) 与我们写成 (n : nat) (m : nat) 的意思相同。

coq">Fixpoint mult (n m : nat) : nat :=match n with| O ⇒ O| S n' ⇒ plus m (mult n' m)end.Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.

我们可以通过在两个表达式之间用逗号分隔来同时匹配它们：

coq">Fixpoint minus (n m:nat) : nat :=match n, m with| O , _ ⇒ O| S _ , O ⇒ n| S n', S m' ⇒ minus n' m'end.End NatPlayground2.Fixpoint exp (base power : nat) : nat :=match power with| O ⇒ S O| S p ⇒ mult base (exp base p)end.

练习：1 星，标准难度（factorial）
回忆标准的数学阶乘函数：

       factorial(0)  =  1factorial(n)  =  n * factorial(n - 1)     (如果 n > 0)

将其转换为 Coq 代码。

确保在我们提供的函数头和你的定义之间加上 :=。如果你看到像 “The reference factorial was not found in the current environment” 这样的错误，这意味着你忘记了 :=。

coq">Fixpoint factorial (n:nat) : nat(* 用 ":= _你的定义_ ." 替换这一行 *) Admitted.Example test_factorial1: (factorial 3) = 6.
(* 在此处填写证明 *) Admitted.Example test_factorial2: (factorial 5) = (mult 10 12).
(* 在此处填写证明 *) Admitted.

同样，我们可以通过为加法、减法和乘法引入符号表示法，使数值表达式更易于读写。

coq">Notation "x + y" := (plus x y)(at level 50, left associativity): nat_scope.
Notation "x - y" := (minus x y)(at level 50, left associativity): nat_scope.
Notation "x * y" := (mult x y)(at level 40, left associativity): nat_scope.Check ((0 + 1) + 1) : nat.

（level、associativity 和 nat_scope 注释控制 Coq 解析器如何处理这些符号表示法。目前细节并不重要，但感兴趣的读者可以参考本章末尾的 “更多关于符号表示法” 部分。）

请注意，这些声明不会改变我们已经做出的定义：它们只是告诉 Coq 解析器接受 x + y 来代替 plus x y，反之亦然，告诉它的漂亮打印机将 plus x y 显示为 x + y。

当我们说 Coq 几乎没有内置任何东西时，我们是认真的：甚至测试相等性也是一个用户定义的操作！以下是一个函数 eqb，它测试自然数是否相等，返回一个布尔值。注意这里使用了嵌套的 match（我们也可以像在 minus 中那样使用同时匹配）。

coq">Fixpoint eqb (n m : nat) : bool :=match n with| O ⇒ match m with| O ⇒ true| S m' ⇒ falseend| S n' ⇒ match m with| O ⇒ false| S m' ⇒ eqb n' m'endend.

类似地，leb 函数测试其第一个参数是否小于或等于第二个参数，返回一个布尔值。

coq">Fixpoint leb (n m : nat) : bool :=match n with| O ⇒ true| S n' ⇒match m with| O ⇒ false| S m' ⇒ leb n' m'endend.Example test_leb1: leb 2 2 = true.
Proof. simpl. reflexivity. Qed.Example test_leb2: leb 2 4 = true.
Proof. simpl. reflexivity. Qed.Example test_leb3: leb 4 2 = false.
Proof. simpl. reflexivity. Qed.

我们会经常使用这些函数（特别是 eqb），所以让我们给它们定义中缀符号表示法。

coq">Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.

现在我们有两个看起来都像相等的符号：= 和 =?。我们稍后会更多地讨论它们的区别和相似之处。目前，主要需要注意的是 x = y 是一个逻辑断言——一个 “命题”——我们可以尝试证明它，而 x =? y 是一个布尔表达式，我们可以计算它的值（true 或 false）。

练习：1 星，标准难度（ltb）
ltb 函数测试自然数的小于关系，返回一个布尔值。不要为这个函数编写新的 Fixpoint 定义，而是根据之前定义的函数来定义

coq">(* ltb 函数的实现，根据之前定义的函数来实现 *)
Definition ltb (n m : nat) : bool :=andb (leb n m) (negb (n =? m)).Example test_ltb1: ltb 2 2 = false.
Proof. simpl. reflexivity. Qed.Example test_ltb2: ltb 2 4 = true.
Proof. simpl. reflexivity. Qed.Example test_ltb3: ltb 4 2 = false.
Proof. simpl. reflexivity. Qed.Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.Example test_ltb3': (4 <? 2) = false.
Proof. simpl. reflexivity. Qed.

归纳证明

现在我们已经定义了自然数和一些对它们进行操作的函数，让我们开始证明关于这些定义的一些事实。

我们之前看到，我们可以使用 simpl 和 reflexivity 来证明一些关于数字和布尔值的简单事实。例如，证明 (0 + 1) + 1 等于 2 只需要几步计算：

coq">Theorem plus_0_r : forall n : nat, n + 0 = n.
Proof.intros n.induction n as [| n' IHn'].- (* n = 0 *)reflexivity.- (* n = S n' *)simpl. rewrite -> IHn'. reflexivity.
Qed.

这里，Theorem 关键字引入了一个新的定理声明，forall n : nat 表示我们要证明的是对于所有自然数 n 都成立的性质。intros 策略将 n 引入到证明上下文中，induction 策略对 n 进行归纳证明。

归纳证明通常分为两个情况：基础情况（n = 0）和归纳情况（n = S n'）。在基础情况中，我们直接使用 reflexivity 来证明等式成立。在归纳情况中，我们使用 simpl 来简化表达式，然后使用 rewrite 策略应用归纳假设 IHn'，最后再次使用 reflexivity 完成证明。

加法结合律

加法结合律指出，对于任意的自然数 n、m 和 p，有 (n + m) + p = n + (m + p)。我们可以使用归纳证明来证明这个性质：

coq">Theorem plus_assoc : forall n m p : nat,(n + m) + p = n + (m + p).
Proof.intros n m p.induction n as [| n' IHn'].- (* n = 0 *)reflexivity.- (* n = S n' *)simpl. rewrite -> IHn'. reflexivity.
Qed.

同样，我们使用 intros 引入变量，induction 进行归纳证明。在基础情况中，等式直接成立；在归纳情况中，我们简化表达式，应用归纳假设，然后使用 reflexivity 完成证明。

加法交换律

加法交换律指出，对于任意的自然数 n 和 m，有 n + m = m + n。证明这个性质需要一些额外的步骤：

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

这里，我们在基础情况中使用了之前证明的 plus_0_r 定理，在归纳情况中使用了另一个辅助定理 plus_n_Sm（我们还没有证明）。

辅助定理 `plus_n_Sm`

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

这个辅助定理在证明加法交换律时非常有用。

证明中的策略组合

在证明过程中，我们经常需要组合多个策略来完成一个步骤。例如，rewrite -> IHn'; reflexivity. 可以写成一个复合策略：

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

这里，; 用于组合多个策略，使得证明更加简洁。

证明中的 `destruct` 策略

除了 induction 策略，我们还可以使用 destruct 策略来进行情况分析。例如，我们可以使用 destruct 来证明 eqb 函数的一些性质：

coq">Theorem eqb_refl : forall n : nat,(n =? n) = true.
Proof.intros n.induction n as [| n' IHn'].- (* n = 0 *)reflexivity.- (* n = S n' *)simpl. rewrite -> IHn'. reflexivity.
Qed.Theorem eqb_true_iff : forall n m : nat,(n =? m) = true <-> n = m.
Proof.intros n m. split.- (* -> *)induction n as [| n' IHn'].+ (* n = 0 *)destruct m as [| m'].* (* m = 0 *)reflexivity.* (* m = S m' *)simpl. intros H. inversion H.+ (* n = S n' *)destruct m as [| m'].* (* m = 0 *)simpl. intros H. inversion H.* (* m = S m' *)simpl. intros H. apply IHn' in H. rewrite H. reflexivity.- (* <- *)intros H. rewrite H. apply eqb_refl.
Qed.

这里，destruct 策略用于对 m 进行情况分析，inversion 策略用于处理矛盾情况。

证明中的 `split` 策略

split 策略用于证明双向蕴含关系（iff）。在 eqb_true_iff 定理的证明中，我们使用 split 将证明分为两个方向：从左到右和从右到左。

证明中的 `apply` 策略

apply 策略用于应用已经证明的定理或假设。在 eqb_true_iff 定理的证明中，我们使用 apply IHn' in H 来应用归纳假设 IHn' 到假设 H 上。

证明中的 `rewrite` 策略

rewrite 策略用于替换等式中的一边为另一边。在 eqb_true_iff 定理的证明中，我们使用 rewrite H 来将等式 H 中的一边替换为另一边。

证明中的 `simpl` 策略

simpl 策略用于简化表达式。在很多证明中，我们使用 simpl 来简化目标表达式，使得 reflexivity 或其他策略能够更容易地应用。

证明中的 `reflexivity` 策略

reflexivity 策略用于证明等式两边相等。当等式两边经过简化后完全相同时，reflexivity 可以直接完成证明。

证明中的 `intros` 策略

intros 策略用于将全称量词（forall）后面的变量引入到证明上下文中。在很多证明中，我们首先使用 intros 来引入变量，然后再进行后续的证明步骤。

证明中的 `inversion` 策略

inversion 策略用于处理构造函数的情况。当我们有一个等式，其中一边是构造函数应用，另一边是其他表达式时，inversion 可以帮助我们推导出一些有用的信息。

证明中的 `unfold` 策略

unfold 策略用于展开定义。当我们需要查看某个定义的具体内容时，可以使用 unfold 来展开它。

证明中的 `fold` 策略

fold 策略用于折叠定义。当我们已经展开了某个定义，并且想要将其恢复到原来的形式时，可以使用 fold 来折叠它。

证明中的 `assert` 策略

assert 策略用于引入一个中间结论。当我们在证明过程中需要一个额外的事实时，可以使用 assert 来声明并证明这个事实，然后再使用它来完成后续的证明。

证明中的 `clear` 策略

clear 策略用于从证明上下文中移除一个变量或假设。当某个变量或假设在后续的证明中不再需要时，可以使用 clear 来移除它，以简化证明上下文。

证明中的 `rename` 策略

rename 策略用于重命名证明上下文中的变量。当变量名不够清晰或容易引起混淆时，可以使用 rename 来重命名它们。

证明中的 `revert` 策略

revert 策略用于将一个变量从证明上下文中移除，并重新添加到全称量词中。当我们需要对某个变量进行重新归纳或情况分析时，可以使用 revert 来实现。

证明中的 `generalize` 策略

generalize 策略用于将一个表达式推广为一个变量。当我们需要对某个表达式进行统一处理时，可以使用 generalize 来将其替换为一个变量。

证明中的 `pattern` 策略

pattern 策略用于指定一个表达式作为模式进行重写。当我们需要对某个特定的表达式进行重写时，可以使用 pattern 来指定这个表达式。

证明中的 `set` 策略

set 策略用于为一个表达式定义一个新的变量。当我们需要多次使用某个复杂的表达式时，可以使用 set 来为它定义一个新的变量，以简化证明。

证明中的 `pose` 策略

pose 策略与 set 策略类似，用于为一个表达式定义一个新的变量。不同之处在于，pose 可以同时定义多个变量。

证明中的 `exists` 策略

exists 策略用于证明存在量词（exists）的命题。当我们需要证明存在某个元素满足某个性质时，可以使用 exists 来指定这个元素。

证明中的 `destruct` 策略（续）

destruct 策略还可以用于对布尔值、元组等类型进行情况分析。例如：

coq">Theorem andb_true_iff : forall b c, andb b c = true <-> b = true /\ c = true.
Proof.intros b c. split.- (* -> *)destruct b.+ (* b = true *)destruct c.* (* c = true *)intros H. split; reflexivity.* (* c = false *)simpl. intros H. inversion H.+ (* b = false *)simpl. intros H. inversion H.- (* <- *)intros [Hb Hc]. rewrite Hb. rewrite Hc. reflexivity.
Qed.

这里，我们使用 destruct 对布尔值 b 和 c 进行情况分析，然后使用 inversion 处理矛盾情况。

证明中的 `match` 策略

match 策略用于在证明中进行模式匹配。当我们需要根据某个表达式的不同情况进行不同的处理时，可以使用 match 策略。例如：

coq">Theorem match_example : forall b : bool,(match b with| true => true| false => falseend) = b.
Proof.intros b.destruct b.- (* b = true *)reflexivity.- (* b = false *)reflexivity.
Qed.

这里，我们使用 destruct 对布尔值 b 进行情况分析，然后使用 reflexivity 完成证明。

证明中的 `case` 策略

case 策略与 destruct 策略类似，用于进行情况分析。不同之处在于，case 可以接受一个模式作为参数，而 destruct 只能接受一个变量。例如：

coq">Theorem case_example : forall b : bool,(if b then true else false) = b.
Proof.intros b.case b.- (* b = true *)reflexivity.- (* b = false *)reflexivity.
Qed.

这里，我们使用 case 对布尔值 b 进行情况分析，然后使用 reflexivity 完成证明。

证明中的 `try` 策略

try 策略用于尝试执行一个策略，如果该策略失败，则忽略失败并继续执行后续的策略。例如：

coq">Theorem try_example : forall b : bool,(try (rewrite <- plus_0_r); reflexivity).
Proof.intros b.try (rewrite <- plus_0_r).reflexivity.
Qed.

这里，我们使用 try 尝试执行 rewrite <- plus_0_r 策略，如果该策略失败，则忽略失败并继续执行 reflexivity 策略。

证明中的 `repeat` 策略

repeat 策略用于重复执行一个策略，直到该策略失败为止。例如：

coq">Theorem repeat_example : forall n : nat,(repeat (simpl; rewrite <- plus_0_r); reflexivity).
Proof.intros n.repeat (simpl; rewrite <- plus_0_r).reflexivity.
Qed.

这里，我们使用 repeat 重复执行 simpl; rewrite <- plus_0_r 策略，直到该策略失败为止，然后使用 reflexivity 完成证明。

证明中的 `idtac` 策略

idtac 策略用于在证明中输出一条消息。例如：

coq">Theorem idtac_example : forall n : nat,(idtac "Starting proof..."; simpl; idtac "Proof finished."; reflexivity).
Proof.intros n.idtac "Starting proof...".simpl.idtac "Proof finished.".reflexivity.
Qed.

这里，我们使用 idtac 在证明开始和结束时输出消息。

证明中的 `Fail` 策略

Fail 策略用于尝试执行一个策略，如果该策略成功，则证明失败。例如：

coq">Theorem Fail_example : forall n : nat,(Fail (rewrite <- plus_0_r); reflexivity).
Proof.intros n.Fail (rewrite <- plus_0_r).reflexivity.
Qed.

这里，我们使用 Fail 尝试执行 rewrite <- plus_0_r 策略，如果该策略成功，则证明失败，否则继续执行 reflexivity 策略。

证明中的 `Time` 策略

Time 策略用于测量执行一个策略所花费的时间。例如：

coq">Theorem Time_example```coq
: forall n : nat,(Time (simpl; rewrite <- plus_0_r); reflexivity).
Proof.intros n.Time (simpl; rewrite <- plus_0_r).reflexivity.
Qed.

在这个例子里，Time 策略会记录 simpl; rewrite <- plus_0_r 这一系列操作所耗费的时间，方便我们对证明过程的效率进行评估。

证明自动化

在 Coq 里，除了手动使用各种策略来完成证明，还可以使用一些自动化机制来简化证明过程。例如 auto 策略，它能自动应用一些简单的证明步骤，尝试去完成证明。

coq">Theorem auto_example : forall n m : nat,n + 0 = n /\ m + 0 = m.
Proof.intros n m.auto.
Qed.

在这个证明中，auto 策略会自动引入假设、应用已经证明的定理（如 plus_0_r），并处理逻辑连接词（如 /\），最终完成证明。

`tauto` 策略

tauto 策略专门用于处理命题逻辑中的重言式证明。它能自动识别并证明那些仅依赖于逻辑连接词（如 and、or、not、implies 等）的逻辑关系。

coq">Theorem tauto_example : forall P Q R : Prop,(P -> Q) -> (Q -> R) -> P -> R.
Proof.intros P Q R.tauto.
Qed.

这里 tauto 策略会自动分析命题逻辑结构，找到从前提到结论的推导路径，完成证明。

`firstorder` 策略

firstorder 策略功能更强大，它不仅能处理命题逻辑，还能处理一阶逻辑的证明，包括全称量词（forall）和存在量词（exists）。

coq">Theorem firstorder_example : forall (X : Type) (P Q : X -> Prop),(forall x, P x -> Q x) -> (exists x, P x) -> exists x, Q x.
Proof.intros X P Q.firstorder.
Qed.

firstorder 策略会对全称量词和存在量词进行合理的实例化和推理，从而完成证明。

自定义证明策略

除了使用 Coq 自带的策略，我们还可以自定义策略。例如，定义一个组合策略，将多个常用的策略组合在一起。

coq">Ltac my_strategy :=simpl; rewrite <- plus_0_r; reflexivity.Theorem custom_strategy_example : forall n : nat,n + 0 = n.
Proof.intros n.my_strategy.
Qed.

这里我们定义了一个名为 my_strategy 的自定义策略，它将 simpl、rewrite <- plus_0_r 和 reflexivity 组合在一起。在证明 custom_strategy_example 时，直接使用这个自定义策略就能完成证明。

证明中的策略提示（Hint）

策略提示是一种让 Coq 自动记住某些定理并在合适的时候应用它们的机制。例如，我们可以将 plus_0_r 定理设置为提示，这样在证明过程中，Coq 可能会自动应用它。

coq">Hint Resolve plus_0_r.Theorem hint_example : forall n : nat,(n + 0) + 0 = n.
Proof.intros n.auto.
Qed.

通过 Hint Resolve plus_0_r，我们将 plus_0_r 定理添加到了 Coq 的提示数据库中。在 hint_example 的证明中，auto 策略就有可能自动应用这个定理来完成证明。

证明中的重写提示（Rewrite Hint）

重写提示专门用于重写规则。我们可以将一些等式定理设置为重写提示，让 Coq 在证明过程中自动进行重写。

coq">Hint Rewrite plus_0_r.Theorem rewrite_hint_example : forall n : nat,(n + 0) + 0 = n.
Proof.intros n.autorewrite with core.reflexivity.
Qed.

这里 Hint Rewrite plus_0_r 将 plus_0_r 定理设置为重写提示，autorewrite with core 会自动应用这些重写提示对表达式进行重写，然后再使用 reflexivity 完成证明。

关于归纳证明的更多高级技巧

多重归纳

有时候我们需要对多个变量同时进行归纳证明。例如，对于一个涉及两个自然数的函数性质，我们可能需要同时对这两个自然数进行归纳。

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

虽然这里只是对 n 进行了归纳，但在实际情况中，如果问题更复杂，可能需要同时对 n 和 m 进行归纳。

归纳中的泛化

在进行归纳证明时，有时候需要先对一些变量进行泛化处理，以便能更好地应用归纳假设。

coq">Theorem generalize_induction_example : forall n m : nat,(n + m) + 0 = n + (m + 0).
Proof.intros n m.generalize dependent m.induction n as [| n' IHn'].- (* n = 0 *)intros m. reflexivity.- (* n = S n' *)intros m. simpl. rewrite -> IHn'. reflexivity.
Qed.

generalize dependent m 这一步将 m 进行了泛化，使得在归纳过程中可以更灵活地应用归纳假设。

练习：不同难度的证明练习

练习：2 星，标准难度（`plus_comm'`）

coq">Theorem plus_comm' : forall n m : nat,n + m = m + n.
Proof.(* 在此处填写证明 *) Admitted.

练习：3 星，标准难度（`mult_comm`）

coq">Theorem mult_comm : forall n m : nat,n * m = m * n.
Proof.(* 在此处填写证明 *) Admitted.

练习：3 星，标准难度（`distribute_plus_mult`）

coq">Theorem distribute_plus_mult : forall n m p : nat,(n + m) * p = (n * p) + (m * p).
Proof.(* 在此处填写证明 *) Admitted.

练习：4 星，高级难度（`fibonacci_proof`）

首先，定义斐波那契数列：

coq">Fixpoint fib (n:nat) : nat :=match n with| O ⇒ O| S O ⇒ S O| S (S n') ⇒ fib n' + fib (S n')end.

然后证明关于斐波那契数列的一个性质：

coq">Theorem fibonacci_proof : forall n : nat,fib (S (S (S n))) = fib (S n) + fib (S (S n)).
Proof.(* 在此处填写证明 *) Admitted.

证明的调试与优化

在进行证明时，可能会遇到各种问题，比如策略应用失败、证明陷入死循环等。这时就需要对证明进行调试。

逐步调试

可以通过逐步执行策略，观察每一步的证明状态，找出问题所在。例如，在使用 rewrite 策略时，如果出现错误，可以逐步检查重写的等式是否正确。

优化证明

有时候证明过程可能过于冗长，我们可以通过使用更合适的策略、组合策略或者利用自动化机制来优化证明。例如，将一些常用的证明步骤封装成自定义策略，或者使用 auto、tauto 等自动化策略来简化证明。

总结

在 Coq 中进行证明是一个系统且富有挑战性的过程。我们可以使用各种策略，如 intros、simpl、rewrite、reflexivity、induction 等，来构建证明。同时，还可以利用自动化机制，如 auto、tauto、firstorder 等，提高证明效率。自定义策略和策略提示可以让我们根据具体问题定制证明流程。在遇到复杂问题时，多重归纳、归纳中的泛化等高级技巧可以帮助我们完成证明。并且，通过调试和优化证明，我们能让证明过程更加简洁和高效。

后续可以继续探索更多复杂的数据类型和证明技巧，进一步提升在 Coq 中进行形式化证明的能力。例如，探索更复杂的递归数据类型（如列表、树等），以及关于这些数据类型的操作和性质的证明。