前文已讨论过 Coq 既可以用 nat、list 等归纳类型及其函数'编程'，又可 以用归纳命题（如 ev）、蕴含式、全称量词等工具'证明'程序的性质。我们一直 以来区别对待此两种用法，在很多情况下确实可以这样。但也有迹象表明在 Coq 中编 程与证明紧密相关。例如，关键字 Inductive 同时用于声明数据类型和命题，以及 → 同时用于描述函数类型和逻辑蕴含式。这可并不是语法上的巧合！事实上，在 Coq 里面程序和证明几乎就是同一件事情。这一章我们会学习背后的原理。 我们已经知道这个基础的思想：在Coq里面，可证明性表现为拥有具体的'证据'。 为基本命题构造证明，实则以树状结构表示其证据。 对于形如 A → B 的蕴含式，其证明为证据'转化装置（transformer）'，可将任何 证明 A 的依据转化为 B 的证据。所以从根本上来讲，证明仅仅就是操纵证据的程 序。 试问：如果是证据是数据，那么命题本身是什么？ 答曰：类型也！ 回顾一下 ev 这个性质的形式化定义。

我们可以换种方式来解读“:”：用“是……的证明”而非“具有……类型”。例如将 ev 定义中第二行的 ev_0 : ev 0 读作“ev_0 是 ev 0 的证明”而非“ev_0 的类型为 ev 0”。 此处 : 既在类型层面表达“具有……类型”，又在命题层面表示“是……的证明”。 这种双关称为'柯里-霍华德同构（Curry-Howard correspondence）'。 它指出了逻辑与计算之间的深层联系：

                 命题           ~  类型
                 证明           ~  数据值

[Wadler 2015] 里有简单的历史和最新的详细介绍可供参考。 该同构启发很多看问题的新方法。首先，对 ev_SS 构造子的理解变得更加自然：

可以将其读作“ev_SS 构造子接受两个参数——数字 n 以及命题 ev n 的证明——并产生 ev (S (S n)) 的证明。” 现在让我们回顾一下之前有关 ev 的一个证明。

就像是处理普通的数据值和函数一样，我们可以使用 Print 指令来查看 这个证明脚本所产生的'证据对象 (proof object)'

实际上，我们也可以不借助脚本'直接'写出表达式作为证明。

表达式 ev_SS 2 (ev_SS 0 ev_0) 可视为向构造子 ev_SS 传入参数 2 和 0 等参数，以及对应的 ev 2 与 ev 0 之依据所构造的证明。或言之，视 ev_SS 为“构造证明”之原语，需要给定一个数字，并进一步提供该数为偶数之依据以构造证明。 其类型表明了它的功能：
      ∀ n, ev n → ev (S (S n)),

类似地，多态类型 ∀ X, list X 表明可以将 nil 视为从某类型到由该类型元素组成的空列表的函数。 我们在 Logic 这一章中已经了解到，我们可以使用函数应用 的语法来实例化引理中的全称量化变量，也可以使用该语法提供引理所要求 的假设。例如：

证明脚本

我们一直在讨论的'证明对象 (Proof Objects)'是Coq如何运作的核心。 当Coq执行一个证明脚本的时候，在内部，Coq逐渐构造出一个证明对象—— 一个类型是想要证明的命题的项。在 Proof 和 Qed 之间的策略告诉 Coq如何构造该项。为了了解这个过程是如何进行的，在下面的策略证明里， 我们在多个地方使用 Show Proof 指令来显示当前证明树的状态。

在任意的给定时刻，Coq已经构造了一个包含一个“洞(hole)”（即 ?Goal ）的项，并且Coq知道该洞需要什么类型的证据来填补。 每一个洞对应一个子目标。当没有子目标时，代表证明已经完成。此时，我 们构造的证明将会被存储在全局环境中，其名字就是在 Theorem 中给定的名字 策略证明非常有用且方便，但是它们并不是必要的：原则上，我们总是能够 手动构造想要的证据，如下所示。此处我们可以通过 Definition （而非 Theorem）来直接给这个证据一个全局名称。

所有这些构造证明的不同方式，对应的存储在全局环境中的证明是完全一样的。

练习：2 星, standard (eight_is_even)

写出对应 ev 8 的策略证明和证明对象。

量词，蕴含式，函数

在Coq的计算世界里（即所有的数据结构和程序存在的地方），有两种值的 类型中拥有箭头：一种是'构造子(Constructor)'，它通过归纳地定义数据类型 引入，另一种是'函数(Function)'。 类似地，在Coq的逻辑世界里（即我们运用证明的地方），有两种方式来给 与蕴含式需要的证据：构造子，通过归纳地定义命题引入，和...函数！ 例如，考虑下列陈述：

对应 ev_plus4 的证明对象是什么？ 我们在寻找一个'类型(Type)'是 ∀ n, ev n → ev (4 + n) 的表达式——也 就是说，一个接受两个参数（一个数字和一个证据）并返回一个证据的 '函数(Function)'! 它的证据对象：

回顾 fun n ⇒ blah 意味着“一个函数，给定 n，产生 blah”， 并且Coq认为 4 + n 和 S (S (S (S n))) 是同义词，所以另一种写出 这个定义的方式是：

当我们将 ev_plus4 证明的命题视为一个函数类型时，我们可以发现一个 有趣的现象：第二个参数的类型，ev n，依赖于第一个参数 n 的'值'。 虽然这样的'依赖类型 (Dependent type)'在传统的编程语言中并不存在， 但是它们对于编程来说有时候非常有用。最近它们在函数式编程社区里的活 跃很好地表明了这一点。 注意到蕴含式（→）和量化（∀）都表示证据上的函数。事实上，他们 是同一个东西：当我们使用∀时没有依赖，就可以简写为当→。即，我 们没有必要给与箭头左边的类型一个名字：
           ∀ (x:nat), nat
        = ∀ (_:nat), nat
        = nat → nat

例如，考虑下列命题：

这个命题的一个证明项会是一个拥有两个参数的函数：一个数字n 和一个表明n是偶数的证据E。但是对于这个证据来说，名字E并没有 在ev_plus2剩余的陈述里面被使用，所以还专门为它取一个名字并没有意 义。因此我们可以使用虚拟标志符_来替换真实的名字：

或者，等同地，我们可以使用更加熟悉的记号：

总的来说，"P → Q"只是 "∀ (_:P), Q"的语法糖。

使用策略编程

如果我们可以通过显式地给出项，而不是执行策略脚本，来构造证明，你可 能会好奇我们是否可以通过'策略'，而不是显式地给出项，来构造'程序'。 自然地，答案是可以！

注意到我们通过使用.终止了Definition，而不是使用:=和一个项来 定义它。这个记号会告诉Coq进入'证明脚本模式(Proof Scripting Mode)'来构造类型是nat → nat的项。并且，我们通过使用Defined而不是 Qed来终止证明；这使得这个定义是'透明的(Transparent)'，所以它可 以在计算中就像正常定义的函数一样被使用。（通过Qed定义的对象在计 算中是不透明的。） 这个特性主要是在定义拥有依赖类型的函数时非常有用。我们不会在本书中 详细讨论后者。但是它确实表明了Coq里面基本思想的一致性和正交性。

逻辑联结词作为归纳类型

归纳定义足够用于表达我们目前为止遇到的大多数的联结词。事实上， 只有全称量化（以及作为特殊情况的蕴含式）是Coq内置的，所有其他的都是被归纳 定义的。在这一节中我们会看到它们的定义。

合取

为了证明P ∧ Q成立，我们必须同时给出P和Q的证据。因此，我们可 以合理地将P ∧ Q的证明对象定义为包含两个证明的元祖：一个是P的 证明，另一个是Q的证明。即我们拥有如下定义。

注意到这个定义与在章节 Poly 中给出的 prod 定义的类型的相似处； 唯一的不同之处在于，prod的参数是Type，而and的类型是Prop。

这个定义能够解释为什么destruct和intros模式能用于一个合取前提。 情况分析允许我们考虑所有P ∧ Q可能被证明的方式——只有一种方式（即 conj构造子）。 类似地，split策略能够用于所有只有一个构造子的归 纳定义命题。特别地，它能够用于and：

这解释了为什么一直以来我们能够使用策略来操作and的归纳定义。我们 也可以使用模式匹配来用它直接构造证明。例如：

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

构造一个证明对象来证明下列命题。

析取

析取的归纳定义有两个构造子，分别用于析取的两边：

这个声明解释了destruct策略在一个析取前提上的行为，产生的子类型和 or_introl以及or_intror构造子的形状相匹配。 又一次地，我们可以不使用策略，直接写出涉及or的定义的证明对象。

练习：2 星, standard, optional (or_commut'')

尝试写下or_commut的显式证明对象。（不要使用Print来偷看我们已经 定义的版本！）

存在量化

为了给出存在量词的证据，我们将一个证据类型x和x满足性质P的证明打包在一起：

打包之后的命题可以通过解包操作受益。这里的核心定义是为了用于构造 ex P命题的类型构造器ex，其中P自身是一个从类型为A的证据类型 值到命题的'函数(Function)'。构造子ex_intro提供了一个给定 证据类型x和P x的证 明，可以构造ex P的证据的方式。 我们更加熟悉的类型∃ x, P x可以转换为一个涉及ex的表达式：

下面是我们如何定义一个涉及ex的显式证明对象：

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

完成下列证明对象的定义：

True和False

True命题的归纳定义很简单：

它拥有一个构造子（因此True的所有证据都是一样的，所以给出一个 True的证明并没有信息量。） False也一样的简单——事实上，它是如此简单，以致于第一眼看上去像是一个 语法错误。

也就是说， False是一个'没有'构造子的归纳类型--即，没有任何方式能 够构造一个它的证明。

相等关系

在Coq里，甚至连相等关系都不是内置的。它拥有如下的归纳定义。（事实上， 在标准库里的定义是这里给出的定义的轻微变体，前者给出了稍微容易使用 一些的归纳法则。）

我们可以这样理解这个定义，给定一个集合X，它定义了由X的一对值 (x和y)所索引的“x与y相等”的一'系列(Family)'的命题。只有 一种方式能够构造该系列中成员的证据：将构造子eq_refl应用到类型X 和值x:X，产生一个x等于x的证据。 其它形如 eq x y 的类型中的 x 和 y 并不相同，因此是非居留的。 我们可以使用eq_refl来构造证据，比如说，2 = 2。那么我们能否使用 它来构造证据1 + 1 = 2呢？答案是肯定的。事实上，它就是同一个证据！ 原因是如果两个项能够通过一些简单的计算规则'可转换(convertible)' ， 那么Coq认为两者“相等”。 这些计算规则，与Compute所使用的规则相似，包括函数应用的计算，定 义的内联，match语句的化简。

至今为止我们所用来证据相等关系的reflexivity策略本质上只是apply eq_refl的简写。 在基于策略的相等关系证明中，转换规则通常隐藏在simpl的使用后面（在 其他策略中或显式或隐式，例如reflexivity）。 而在如下的显式证明对象中，你可以直接看到它们：

练习：2 星, standard (equality__leibniz_equality)

相等关系的归纳定义隐含了'Leibniz相等关系(Leibniz equality)'：当我们 说“x和y相等的时候”，我们意味着所有x满足的性质P，对于y 来说也满足。

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

请说明，事实上，相等关系的归纳定义和Leibniz相等关系是 '等价的(equivalent)'。

再论反演

我们曾经见过inversion被同时用于相等关系前提，和关于被归纳定义的命 题的前提。现在我们明白了实际上它们是同一件事情。那么我们现在可以细 究一下inversion是如何工作的。 一般来说，inversion策略...

• 接受一个前提H，该前提的类型P是通过归纳定义的，以及
• 对于P的定义里的每一个构造子C，
  • 产生一个新的子目标，在该子目标中我们假设H是通过C构造的，
  • 作为额外的假设，在子目标的上下文中增加C的论据（前提），
  • 将C的结论（结果类型）与当前的目标相匹配，计算出为了能够应用C而必须成立的一些相等关系，
  • 将这些相等关系加入上下文中（以及，为了方便，在目标中替换它们），以及
  • 如果这些相等关系无法满足（例如，它们涉及到S n = O），那么立即解决这个子目标。

'例子'：如果我们反演一个使用or构造的前提，它有两个构 造子，所以产生了两个子目标。构造子的结论（结果类型，即P ∨ Q） 并没有对于P和Q的形式有任何要求，所以在子目标的上下文中我们不会 获得额外的相等关系。 '例子'：如果我们反演一个使用and构造的前提，它只有一个构造子， 所以只产生一个子目标。再一次地，构造子的结论（结果类型，即P ∧ Q） 并没有对于P和Q的形式有任何要求，所以在子目标的上下文中我们不会 获得额外的相等关系。不过，这个构造子有两个额外的参数，我们能够在子 目标的上下文中看到它们。 '例子'：如果我们反演一个使用eq构造的前提，它也只有一个构造子， 所以只产生一个子目标。但是，现在eq_refl构造子的形式给我们带来 的额外的信息：它告诉eq的两个参数必须是一样的。于是inversion策 略会将这个事实加入到上下文中。