我们已经见过很多对事实的断言（即'命题'） 以及如何用证据展示其正确性（即'证明'）的例子了。特别是， 我们证明了大量的'相等性命题'（e₁ = e₂）、蕴含式（P → Q）和量化命题 （∀ x, P x）。在本章中，我们将会看到如何用 Coq 解决类似形式的逻辑推理。 在深入细节之前，我们先来探讨一下 Coq 中数学表达式的地位。 回忆一下，Coq 是一门拥有'类型'的语言，也就是说，一切有意义的 表达式都具有一个相应的类型。逻辑表达也不例外，我们试图在 Coq 中证明的一切语句都有名为 Prop 的类型，即'命题类型'。我们 可以用 Check 指令来查看：

注意：'所有'语法形式良好的命题，无论是否为真，其类型均为 Prop。 简单来说，'是'一个命题与该命题'可以证明'是两回事。

除了拥有类型之外，命题还是'一等的（First-Class）'实体， 即在 Coq 的世界中，我们可以像操作其它实体那样操作命题。 到目前为止，我们已经知道命题可以出现在 Theorem（还有 Lemma 以及 Example）的声明中了。

不过命题还可以用在其它地方。例如，我们可以用 Definition 为命题取名，就像为其它表达式取名一样。

之后我们可以在任何需要此命题的地方使用它们名字——例如，作为一个 Theorem 声明中的断言：

我们也可以写出'参数化'的命题 -- 也就是一个接受某些类型的参数， 然后返回一个命题的函数。 例如，以下函数接受某个数字，返回一个命题断言该数字等于 3：

在 Coq 中，返回命题的函数可以说是定义了其参数的'性质'。 例如，以下（多态的）性质定义了常见的 '单射函数' 的概念。

相等关系运算符 = 也是一个返回 Prop 的函数。 表达式 n = m 只是 eq n m 的语法糖（它使用 Notation 机制定义在 Coq 标准库中）。由于 eq 可被用于任何类型的元素，因此它也是多态的：

（注意我们写的是 @eq 而非 eq：eq 的类型参数 A 是隐式声明的，因此我们需要关掉隐式参数的类型推断以便看到 eq 的完整类型。）

逻辑联结词

合取

命题 A 与 B 的'合取'（即'逻辑与'）写作 A ∧ B，表示一个 A 与 B 均为真的断言。

证明合取的命题通常使用 split 策略。它会分别为语句的两部分生成两个子目标：

对于任意命题 A 和 B，如果我们假设 A 为真且 B 为真， 那么就能得出 A ∧ B 也为真的结论。

由于按照前提对某个目标应用定理会产生与该定理的前提一样多的子目标。 因此我们可以应用 and_intro 来达到和 split 一样的效果。

练习：2 星, standard (and_exercise)

以上就是证明合取语句的方法。要反过来使用，即'使用'合取前提来帮助证明时， 我们会采用 destruct 策略。 如果当前证明上下文中存在形如 A ∧ B 的前提 H，那么 destruct H as [HA HB] 将会从上下文中移除 H 并增加 HA 和 HB 两个新的前提，前者断言 A 为真，而后者断言 B 为真。

和往常一样，我们也可以在引入 H 的同时对其进行解构， 而不必先引入然后再解构：

为什么我们要麻烦地将 n = 0 和 m = 0 这两个前提放一条合取语句中呢？ 完全可以用两条独立的前提来陈述此定理啊：

就此定理而言，两种方式都可以。不过理解如何证明合取前提非常重要， 因为合取语句通常会在证明的中间步骤中出现，特别是在做大型开发的时候。 下面是个简单的例子：

另一种经常遇到合取语句的场景是，我们已经知道了 A ∧ B， 但在某些上下文中只需要 A 或者 B。此时我们可以用 destruct 进行解构（或许是作为 intros 的一部分）并用下划线模式 _ 来丢弃不需要的合取分式。

练习：1 星, standard, optional (proj2)

最后，我们有时需要重新排列合取语句的顺序，或者对多部分的合取语句进行分组。 此时使用下面的交换律和结合律会很方便。

练习：2 星, standard (and_assoc)

（在以下结合律的证明中，注意'嵌套'的 intros 模式是如何将 H : P ∧ (Q ∧ R) 拆分为 HP : P、HQ : Q 和 HR : R 的。 请从那里开始完成证明。）

顺便一提，中缀记法 ∧ 只是 and A B 的语法糖而已； and 是 Coq 中将两个命题合并成一个命题的运算符。

析取

另一个重要的联结词是'析取'，即两个命题的'逻辑或'：若 A 或 B 二者之一为真，则 A ∨ B 为真。（这种中缀记法表示 or A B，其中 or : Prop → Prop → Prop。） 为了在证明中使用析取前提，我们需要分类讨论（它与 nat 之类的数据类型一样，都可以显式地通过 destruct 或隐式地通过 intros 模式来拆分：

相应地，要证明某个析取命题成立，只需证明其任意一边的命题成立就够了。 我们可以用 left 和 right 策略来选取命题。顾名思义，left 会选取待析取证命题的左边，而 right 则会选取它的右边。 下面是一种平凡的用法...

...而这个更有趣的例子则同时需要 left 和 right：

假命题与否定

目前为止，我们主要都在证明某些东西是'真'的：加法满足结合律， 列表的连接满足结合律，等等。当然，我们也关心'否定'的结果， 即证明某些给定的命题'不是'真的。在 Coq 中，这样的否定语句使用逻辑否定运算符 ¬ 来表达。 为了理解否定背后的原理，我们需要回想一下Tactics一章中的'爆炸原理'。 爆炸原理断言，当我们假设了矛盾存在时，就能推出任何命题。 遵循这一直觉，我们可以可以将 ¬ P（即非 P）定义为 ∀ Q, P → Q。 不过 Coq 选择了稍有些不同（但等价）的做法，它将 ¬ P 定义为 P → False，而 False 是在标准库中特别定义的矛盾性命题。

由于 False 是个矛盾性命题，因此爆炸原理对它也适用。如果我们让 False 进入到了证明的上下文中，可以对它使用 destruct 来完成任何待证目标。

拉丁文 'ex falso quodlibet' 的字面意思是“从谬误出发， 你能够证明任何你想要的”，这也是爆炸原理的另一个广为人知的名字。

练习：2 星, standard, optional (not_implies_our_not)

证明 Coq 对否定的定义蕴含前面提到的直觉上的定义：

不等性是十分常见的否定句的例子，，它有一个特别的记法 x ≠ y：
      Notation "x <> y" := (~(x = y)).

我们可以用 not 来陈述 0 和 1 是不同的 nat 元素：

性质 0 ≠ 1 就是 ~(0 = 1)，即 not (0 = 1)， 它会展开为 (0 = 1) → False。（这里显式地用 unfold not 展示了这一点，不过一般可以忽略。

要证明不等性，我们可以反过来假设其相等...

... 然后从中推出矛盾。在这里，等式 O = S O 与构造子 O 和 S 的不交性相矛盾，因此用 discriminate 就能解决它。

为了习惯用 Coq 处理否定命题，我们需要一些练习。 即便你十分清楚为什么某个否定命题成立，但能让 Coq 一下就理解则需要点小技巧。 以下常见事实的证明留给你热身。

练习：2 星, advanced (double_neg_inf)

请写出 double_neg 的非形式化证明： '定理'：对于任何命题 P 而言，P 蕴含 ~~P。

练习：2 星, standard, recommended (contrapositive)

练习：1 星, standard (not_both_true_and_false)

练习：1 星, advanced (informal_not_PNP)

请写出 ∀ P : Prop, ~(P ∧ ¬P) 的非形式化证明。

由于不等性包含一个否定，因此在能够熟练地使用它前还需要一些练习。 这里有个有用的技巧：如果你需要证明某个目标不可能时（例如当前的目标陈述为 false = true），请使用 ex_falso_quodlibet 将该目标转换为 False。 如果在当前上下文中存在形如 ¬P 的假设（特别是形如 x≠y 的假设）， 那么此技巧会让这些假设用起来更容易些。

由于用 ex_falso_quodlibet 推理十分常用，因此 Coq 提供了内建的策略 exfalso。

真值

除 False 外，Coq 的标准库中还定义了 True，一个明显真的命题。 为了证明它，我们使用了预定义的常量 I : True：

与经常使用的 False 不同，True 很少使用，因为它作为证明目标来说过于平凡， 而作为前提又不携带任何有用的信息。 然而在使用条件从句定义复杂的 Prop，或者作为高阶 Prop 的参数时， 它还是挺有用的。之后我们会看到一些例子。

逻辑等价

联结词“当且仅当”用起来十分方便，它是两个蕴含式的合取， 断言了两个命题拥有同样的真值。

练习：3 星, standard (or_distributes_over_and)

广集与逻辑等价

Coq 的某些策略会特殊对待 iff 语句，以此来避免操作某些底层的证明状态。 特别来说，rewrite 和 reflexivity 不仅可以用于相等关系，还可用于 iff 语句。为了开启此行为，我们需要导入 Coq 库来支持它：

“广集（Setoid）”指配备了等价关系的集合，即满足自反性、对称性和传递性的关系。 当一个集合中的两个元素在这种关系上等价时，可以用 rewrite 将其中一个元素替换为另一个。我们已经在 Coq 中见过相等性关系 = 了： 当 x = y 时，我们可以用 rewrite 将 x 替换为 y，反之亦可。 同样，逻辑等价关系 ↔ 也满足自反性、对称性和传递性， 因此我们可以用它将替换命题中的一部分替换为另一部分：若 P ↔ Q，那么我们可以用 rewrite 将 P 替换为 Q，反之亦可。 下面是一个简单的例子，它展示了这些策略如何使用 iff。 首先，我们来证明一些基本的 iff 等价关系命题...

现在我们可以用这些事实配合 rewrite 与 reflexivity 对涉及等价关系的陈述给出流畅的证明了。以下是之前 mult_0 包含三个变量的版本：

apply 策略也可以用在 ↔ 上。当给定一个等价关系命题作为 apply 的参数时，它会试图猜出正确的方向。

存在量化

'存在量化'也是十分重要的逻辑联结词。我们说存在某个类型为 T 的 x，使得某些性质 P 对于 x 成立，写作 ∃ x : T, P。 和 ∀ 一样，如果 Coq 能从上下文中推断出 x 的类型，那么类型标注 : T 就可以省略。 为了证明形如 ∃ x, P 的语句，我们必须证明 P 对于某些特定的 x 成立，这些特定的 x 被称作存在性的'例证'。证明分为两步： 首先，我们调用 ∃ t 策略向 Coq 指出已经知道了使 P 成立的例证 t，然后证明将所有出现的 x 替换成 t 的命题 P。

反之，如果我们的的上下文中有形如 ∃ x, P 的存在前提， 可以将其解构得到一个例证 x 和一个陈述 P 对于 x 成立的前提。

练习：1 星, standard, recommended (dist_not_exists)

请证明“P 对所有 x 成立”蕴含“不存在 x 使 P 不成立。” （提示：destruct H as [x E] 可以用于存在假设！）

练习：2 星, standard (dist_exists_or)

请证明存在量化对析取满足分配律。

使用命题编程

我们学过的逻辑联结词为我们提供了丰富的用简单命题构造复杂命题的词汇。 为了说明，我们来看一下如何表达“元素 x 出现在列表 l 中”这一断言。 注意此性质有着简单的递归结构：

• 若 l 为空列表，则 x 无法在其中出现，因此性质“x 出现在 l 中” 为假。

• 否则，若 l 的形式为 x' :: l'，此时 x 是否出现在 l 中， 取决于它是否等于 x' 或出现在 l' 中。

我们可以将此定义直接翻译成递归函数，它接受一个元素和一个列表， 返回一个命题！：

当 In 应用于具体的列表时，它会被展开为一系列具体的析取式。

（注意我们用空模式'无视'了最后一种情况。） 我们也可证明关于 In 的更一般，更高阶的引理。 注意，首先 In 会被应用到一个变量上，只有当我们对它进行分类讨论时， 它才会被展开：

虽然递归定义命题在某些情况下会很方便，但这种方式也有其劣势。特别是， 这类命题会受到 Coq 对递归函数要求的限制，例如，在 Coq 中递归函数必须是 “明显会终止”的。在下一章中，我们会了解如何'归纳地'定义命题， 这是一种与之不同的技巧，有着其独特的优势和限制。

练习：3 星, standard (In_map_iff)

练习：2 星, standard (In_app_iff)

练习：3 星, standard, recommended (All)

回忆一下，返回命题的函数可以视作对其参数'性质'的定义。例如，若 P 的类型为 nat → Prop，那么 P n 就陈述了性质 P 对 n 成立。 以 In 作为参考，请写出递归函数 All，它陈述某个 P 对列表 l 中的所有元素成立。为了确定你的定义是正确的，请在下方证明 All_In 引理。 （当然，你的定义'不应该'为了通过测试就把 All_In 的左边复述一遍。 ）

练习：3 星, standard (combine_odd_even)

完成以下 combine_odd_even 函数的定义。它接受两个对数字成立的性质 Podd 与 Peven，返回性质 P 使得当 n 为奇数时 P n 等价于 Podd n， 否则等价于 Peven n。

为了测试你的定义，请证明以下事实：

对参数应用定理

Coq 不同于其它证明助理（如 ACL2 和 Isabelle）的一个特性是， 它将'证明'本身也作为一等对象。 关于这一点有很多地方值得着墨，不过了解所有的细节对于使用 Coq 来说不是必须的。 本节点到为止，深入的探讨参见 ProofObjects 和 IndPrinciples。 我们已经知道 Check 命令可以用来显式表达式的类型了， 不过它还可以用来查找某个标识符所指代的定理。

在检查定理 plus_comm 的'陈述'时，Coq 使用了与检查某项的'类型'一样的方式 （如果我们保留以冒号开始的部分，那么它会被打印出来）。这是为什么？ 原因在于标识符 plus_comm 其实指代的是被称作'证明对象'的数据结构， 它表示在命题 ∀ n m : nat, n + m = m + n 的真实性上建立的逻辑推导。 此对象的类型'就是'其所证命题的陈述。 从直觉上来说，这很有道理，因为对定理的陈述说明了该定理可用来做什么， 正如可计算对象的类型告诉了我们可以对它做什么。例如，若我们有一个类型为 nat → nat → nat 的项，就可以给它两个 nat 作为参数并得到一个 nat。 类似地，如果我们有一个类型为 n = m → n + n = m + m 的对象， 就能为它提供一个类型为 n = m 的“参数”并推导出 n + n = m + m。 从操作上来说，这种类比可以更进一步：由于定理可以作为函数， 被应用到对应类型的前提上，因此我们可以直接产生结论而不必在途中使用断言。 例如，假设我们想要证明以下结论：

乍看起来，我们似乎可以用 plus_comm 改写两次使两边匹配来证明它。 然而问题是，第二次 rewrite 会抵消第一次的效果。

我们之前在 Induction 一章中见过类似的问题，绕过它的一种简单方法是使用 assert 导出 plus_comm 的特殊版本，这样我们就能用它按照预期来改写。

一种更优雅的方式是直接把我们想要实例化的参数应用到 plus_comm 上， 就像我们将一个多态函数应用到类型参数上那样。

我们来看看另一个像函数那样使用定理或引理的例子。 以下定理说明：任何包含元素的列表 l 一定非空。

有趣的地方是一个量化的变量（x）没有出现在结论（l ≠ []）中。 我们可以用此引理来证明 x 为 42 的特殊情况。直接用 apply in_not_nil 会失败，因为它无法推出 x 的值。

有一些方法可以绕开它： Use apply ... with ...

Use apply ... in ...

显式地对 x 的值应用引理。

显式地对假设应用引理。

对于几乎所有将定理名作为参数的策略而言，你都可以“将定理作为函数”来使用。 注意，定理应用与函数应用使用了同样的类型推导机制，所以你可以将通配符作为定理的参数， 或者为定理声明默认的隐式前提。这些特性在以下证明中展示。（此证明如何工作的细节 不必关心，这里的目标只是为了展示它的用途。）

在以后的章节中我们将会看到更多这方面的例子。

Coq vs. 集合论

Coq 的逻辑核心，即'归纳构造演算（Calculus of Inductive Constructions）'系统， 在很多重要的方面不同于数学家用来写下精确而严谨的定义和证明的形式化系统。 例如，在主流的纸笔数学家中使用最普遍的'策梅洛-弗兰克尔集合论（ZFC）'中， 一个数学对象可同时属于不同的集合；而在 Coq 的逻辑中，一个项最多只属于一个类型。 这些不同之处需要人们用稍微不同的方式来描述非形式化的数学概念，但总的来说， 它们都是非常自然而易于使用的。例如，在 Coq 中我们一般不说某个自然数 n 属于偶数集合，而是说 even n 成立，其中的 even : nat → Prop 描述了偶数的性质。 然而在某些情况下，将标准的数学论证翻译到 Coq 中会十分繁琐甚至是不可能的， 除非我们引入新的公理来丰富其逻辑核心。作为本章的结尾， 我们将探讨这两个世界之间最显著的区别。

函数的外延性

目前为止我们所看见的相等关系断言基本上都只考虑了归纳类型的元素 （如 nat、bool 等等）。然而由于 Coq 的相等关系运算符是多态的， 因此我们可以在'任何'类型上使用它。特别是，我们可以写出断言'两个函数相等'的命题：

在一般的数学研究中，对于任意两个函数 f 和 g， 只要它们对相同的输入产生相等的结果，那么它们就被认为相等：
    (∀ x, f x = g x) → f = g

这被称作'函数的外延性原理'。 不甚严谨地说，所谓“外延性”是指某个对象可观察到的行为。 因此，函数的外延性就是指函数的标识完全由其行为来决定。 用 Coq 的术语来说，就是函数的身份视其被应用后的结果而定。 然而，函数的外延性并不在 Coq 的基本公理之内，因此某些“合理”的命题是不可证明的：

不过我们可以用 Axiom 指令将函数的外延性添加到 Coq 的核心逻辑系统中。

将某个东西用 Axiom 定义为公理的效果与陈述一个定理并用 Admitted 跳过其证明相同， 不过它会提醒读者这是一个公理，我们无需证明！ 现在我们可以在证明中调用函数的外延性了：

当然，在为 Coq 添加公理时必须十分小心，因为这有可能会导致系统 '不一致'，而当系统不一致的，任何命题都能在其中证明，包括 False 和 2+2=5！ 不幸的是，并没有一种简单的方式能够判断添加某条公理是否安全： 一般来说，确认任何一组公理的一致性都需要训练有素的数学家付出艰辛的努力。 然而，我们已经知道了添加函数外延性后的公理系统'确实是'一致的。 我们可以用 Print Assumptions 指令查看某个证明依赖的所有附加公理。

练习：4 星, standard (tr_rev_correct)

列表反转函数 rev 的定义有一个问题，它会在每一步都执行一次 app 调用，而运行 app 所需时间与列表的大小线性渐近，也就是说 rev 的时间复杂度与列表长度呈渐进平方关系。我们可以用以下定义来改进它：

此版本的 rev 是'尾递归（tail-recursive）'的， 因为对函数自身的递归调用是需要执行的最后一步操作 （即，在递归调用之后我们并不执行 ++ ）。 一个足够好的编译器会为此生成十分高效的代码。 请证明以下两个定义等价。

命题 vs. 布尔值

我们已经知道在 Coq 中有两种编码逻辑事实的方式了，即使用'布尔值' （类型为 bool）和'命题'（类型为 Prop）。 例如，我们可以通过以下两种方式来断言 n 为偶数： evenb n 求值为 true：

或者存在某个 k 使得 n = double k：

当然，如果二者刻画的偶数性描述的不是同一个自然数集合，那么会非常奇怪！ 幸运的是，我们确实可以证明二者相同... 首先我们需要两个辅助引理。

练习：3 星, standard (evenb_double_conv)

Now the main theorem:

此定理说明，布尔计算 evenb n 的真假会从命题 ∃ k, n = double k 的真假中'反映（reflected）'出来。 类似地，以下两种 n 与 m 相等的表述等价：

• (1) n =? m 值为 true；
• (2) n = m。

同样，二者的记法也等价。

然而，即便布尔值和命题式在逻辑上是等价的， 但它们的方便性从某些特定的目上来看并不一样。 在前面的偶数例子中，证明 even_bool_prop 的反向部分（即 evenb_double，从命题到布尔表达式的方向）时，我们对 k 进行了简单的归纳。而反方向的证明（即练习 evenb_double_conv） 则需要一种聪明的一般化方法，因为我们无法直接证明 (evenb n = true) → even n。 对于这些例子来说，命题式的声明比与之对应的布尔表达式要更为有用， 但并非总是如此。例如，我们无法在函数的定义中测试一般的命题是否为真， 因此以下代码片段会被拒绝：

Coq 会抱怨 n = 2 的类型是 Prop，而它想要一个 bool 类型的元素（或其它带有两个元素的归纳类型）。原因与 Coq 核心语言的'可计算性'特质有关，即它能表达的所有函数都是可计算且完全的。 这样设计的的原因之一是为了能从 Coq 开发的代码中提取出可执行程序。 因此，在 Coq 中 Prop '并没有'一种通用的情况分析操作来确定 任意给定的命题是否为真，一旦存在这种操作，我们就能写出不可计算的函数。 尽管一般的不可计算性质无法表述为布尔计算，但值得注意的是，很多 '可计算的'性质更容易通过 Prop 而非 bool 来表达，因为在 Coq 中定义递归函数中会受到很大的限制。例如，下一章会展示如何用 Prop 来定义“某个正则表达式可以匹配给定的字符串”这一性质。如果使用 bool 来定义，就需要写一个真正的正则表达式匹配器了，比起该性质的简单定义 （即非算法的定义）来说，这样会更加复杂，更难以理解，也更难以对它进行推理。 另一方面，通过布尔值来陈述事实会带来一点重要的优势，即通过对 Coq 中的项进行计算可以实现一些自动推理，这种技术被称为'互映证明（Proof by Reflection）'。考虑以下陈述：

对此命题而言，最直接的证明方式就是直接给出 k 的值。

而使用与之对应的布尔语句的证明则更加简单（因为我们不必给出证据，Coq 的计算机制会帮我们搞定它！）

有趣的是，由于这两种定义是等价的，因此我们无需显式地给出 500， 而是使用布尔等价式来证明彼此：

尽管此例的证明脚本的长度并未因此而减少，然而更大的证明通常可通过 这种互映的方式来显著化简。举一个极端的例子，在用 Coq 证明著名的 '四色定理'时，人们使用互映技巧将几百种不同的情况归约成了一个布尔计算。 另一点明显的不同是“布尔事实”的否定可以被直白地陈述并证明， 只需翻转预期的布尔值结果即可。

相反，命题的否定形式可能更难以直接证明。

相等性提供了另一个互补的例子，在命题的世界中它有时更容易处理。 在涉及 n 和 m 的证明中，知道 n =? m = true 通常没什么直接的帮助。然而如果我们将该语句转换为等价的 n = m 形式， 则可利用该等式改写证明目标。

我们不会在这里详细讨论互映技巧，然而对于展示布尔计算与一般命题的互补优势而言， 它是个很好的例子，在后面的章节中，能够在布尔和命题的世界之间来回穿梭通常会非常方便。

练习：2 星, standard (logical_connectives)

以下引理将本章中讨论的命题联结词与对应的布尔操作关联了起来。

练习：1 星, standard (eqb_neq)

以下定理为等价式 eqb_eq 的“否定”版本， 在某些场景中使用它会更方便些（后面的章节中会讲到这方面的例子）。

练习：3 星, standard (eqb_list)

给定一个用于测试类型为 A 的元素相等关系的布尔操作符 eqb， 我们可以定义函数 eqb_list 来测试元素类型为 A 的列表的相等关系。 请完成以下 eqb_list 函数的定义。要确定你的定义是否正确，请证明引理 eqb_list_true_iff。

练习：2 星, standard, recommended (All_forallb)

回忆一下Tactics一章中练习 forall_exists_challenge 的函数 forallb：

请证明以下定理，它将 forallb 与之前的定义中 All 的性质联系了起来。

（未分级的思考题）函数 forallb 是否还存在尚未被此规范刻画到的重要性质？

经典逻辑 vs. 构造逻辑

我们已经知道了，在定义 Coq 函数时是无法判断命题 P 是否成立。 然而'证明'也存在类似的限制！换句话说，以下推理原则即便符合直觉， 不过在 Coq 中它是不可证明的：

为了在操作上理解为何如此, 回忆一下，在证明形如 P ∨ Q 的陈述时，我们使用了 left 与 right 策略，它们能够有效地知道析取的哪边成立。 然而在 excluded_middle 中，P 是被全称量化的'任意'命题，我们对它一无所知。 我们没有足够的信息来选择使用 left 或 right 中的哪一个。就像 Coq 因为缺乏信息而无法在函数内部机械地确定 P 是否成立一样。 然而，如果我们恰好知道 P 与某个布尔项互映，那么就能很轻易地知道它是否成立了： 我们只需检查 b 的值即可。

特别来说，对于自然数 n 和 m 的 n = m 而言，排中律是成立的。

一般的排中律在 Coq 中默认并不可用，因为它是常见的逻辑系统（如 ZFC）中的标准特性。尽管如此，不假设排中律的成立仍有其独特的优点： Coq 中的陈述可以构造出比标准数学中同样陈述更强的断言。特别是， 当存在 ∃ x, P x 的 Coq 证明时，我们可以直接给出一个使 P x 得证的值 x。换言之，任何关于存在性的证明必定是'构造性'的。 像 Coq 一样不假设排中律成立的逻辑系统被称作'构造逻辑'。 像 ZFC 这样更加传统的，排中律对于任何命题都成立的逻辑系统则被称作'经典逻辑'。 以下示例展示了为何假设排中律成立会导致非构造性证明： '命题'：存在无理数 a 和 b 使得 a ^ b（a 的 b 次方）为有理数。 '证明'：易知 sqrt 2 为无理数。若 sqrt 2 ^ sqrt 2 为有理数， 那么可以取 a = b = sqrt 2 证明结束；否则 sqrt 2 ^ sqrt 2 为无理数。 此时，我们可以取 a = sqrt 2 ^ sqrt 2 和 b = sqrt 2，因为 a ^ b = sqrt 2 ^ (sqrt 2 × sqrt 2) = sqrt 2 ^ 2 = 2. ☐ 看到发生什么了吗？我们使用排中律在不知道 sqrt 2 ^ sqrt 2 是否为有理数的情况下就分别考虑了这两种情况！因此，我们通过证明知道了这样的 a 和 b 存在，但却无法确切知道它们的值（至少无法从此论据中获知）。 即便构造逻辑很有用，它也有自身的限制：存在很多容易用经典逻辑证明的命题， 用构造证明只会更加复杂，而对于某些已知的命题而言这样的构造性证明甚至不存在！ 幸运的是，排中律和函数外延性一样都是与 Coq 的逻辑系统兼容的， 我们可以安全地将它作为公理添加到 Coq 中。然而，在本书中我们不必如此： 我们所涉及的结构都可以完全用构造逻辑得到，所需的额外代价则微不足道。 我们需要一定的实践才能理解哪些证明技巧不应在构造推理中使用， 而其中的反证法尤为臭名昭著，因为它会导向非构造性证明。这里有个典型的例子： 假设我们想要证明存在 x 具有某种性质 P，即存在 P x。我们先假设结论为假， 也就是说 ¬ ∃ x, P x。根据此前提，不难推出 ∀ x, ¬ P x。 如果我们能够根据此中间事实得到矛盾，就能得到一个存在性证明而完全不必指出一个 x 的值使得 P x 成立！ 从构造性的角度来看，这里存在着技术上的瑕疵，即我们试图通过对 ¬ ¬ (∃ x, P x) 的证明来证明 ∃ x, P x。从以下练习中我们会看到， 允许自己从任意陈述中去掉双重否定等价于引入排中律。因此，只要我们不引入排中律， 就无法在 Coq 中编码此推理。

练习：3 星, standard (excluded_middle_irrefutable)

证明通用排中律公理与 Coq 的一致性需要复杂的推理，而且并不能在 Coq 自身中进行。然而，以下定理蕴含了假设可判定性公理（即排中律的一个特例） 成立对于任何'具体的'命题 P 而言总是安全的。之所以如此， 是因为我们无法证明这类公理的否定命题。假如我们可以的话，就会同时有 ¬ (P ∨ ¬P) 和 ¬ ¬ (P ∨ ¬P)（因为根据引理 double_neg，P 蕴含 ¬ ¬ P）， 而这会产生矛盾。但因为我们不能，所以将 P ∨ ¬P 作为公理加入是安全的。

练习：3 星, advanced (not_exists_dist)

在经典逻辑中有这样一条定理，它断言以下两条命题是等价的：
    ¬(∃ x, ¬P x)
    ∀ x, P x

之前的 dist_not_exists 证明了此等价式的一个方向。有趣的是， 我们无法用构造逻辑证明另一个方向。你的任务就是证明排中律蕴含此方向的证明。

练习：5 星, standard, optional (classical_axioms)

对于喜欢挑战的读者，以下练习来自于 Bertot 与 Casteran 所著的 Coq'Art 一书中第 123 页。以下四条陈述的每一条，加上 excluded_middle 可以认为刻画了经典逻辑。我们无法在 Coq 中证明其中的任意一条， 不过如果我们希望在经典逻辑下工作的话，可以安全地将其中任意一条作为公理添加到 Coq 中而不会造成不一致性。 请证明所有五个命题都是等价的（这四个再加上 excluded_middle）。 提示：不要去分别考虑每一对命题，而是证明一条将它们连接起来的单向蕴含环链。