本章额外介绍了一些证明策略和手段， 它们能用来证明更多关于函数式程序的有趣性质。 我们会看到：

• 如何在“向前证明”和“向后证明”两种风格中使用辅助引理；
• 如何对数据构造子进行论证，特别是，如何利用它们单射且不交的事实；
• 如何增强归纳假设，以及何时需要增强；
• 还有通过分类讨论进行论证的更多细节。

apply 策略

我们经常会遇到待证目标与上下文中的前提或已证引理'刚好相同'的情况。

我们可以像之前那样用“rewrite → eq₂. reflexivity.”来完成。 不过如果我们使用 apply 策略，只需一步就能完成此证明：

apply 策略也可以配合'条件（Conditional）'假设和引理来使用： 如果被应用的语句是一个蕴含式，那么该蕴含式的前提就会被添加到待证子目标列表中。

通常，当我们使用 apply H 时，语句 H 会以一个引入了某些 '通用变量（Universal Variables）' 的 ∀ 开始。在 Coq 针对 H 的结论匹配当前目标时，它会尝试为这些变量查找适当的值。例如， 当我们在以下证明中执行 apply eq₂ 时，eq₂ 中的通用变量 q 会以 n 实例化，而 r 会以 m 实例化。

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

请只用 intros 和 apply 完成以下证明。

要使用 apply 策略，被应用的事实（的结论）必须精确地匹配证明目标： 例如, 当等式的左右两边互换后，apply 就无法起效了。

在这里，我们无法直接使用 apply，不过我们可以用 symmetry 策略 它会交换证明目标中等式的左右两边。

（此处的 simpl 是可选的，因为 apply 会在需要时先进行化简。）

练习：3 星, standard (apply_exercise1)

（'提示'：你可以配合之前定义的引理来使用 apply，不仅限于当前上下文中的前提。 记住 Search 是你的朋友。）

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

简述 apply 与 rewrite 策略之区别。哪些情况下二者均可有效利用？

apply with 策略

以下愚蠢的例子在一行中使用了两次改写来将 [a;b] 变成 [e;f]。

由于这种模式十分常见，因此我们希望一劳永逸地把它作为一条引理记录下来， 即等式具有传递性。

现在，按理说我们应该可以用 trans_eq 来证明前面的例子了。 然而，为此我们还需要稍微改进一下 apply 策略。

如果此时我们只是告诉 Coq apply trans_eq，那么它会 （根据该引理的结论对证明目标的匹配）说 X 应当实例化为 [nat]、n 实例化为 [a,b]、以及 o 实例化为 [e,f]。然而，匹配过程并没有为 m 确定实例：我们必须在 apply 的调用后面加上 "with (m:=[c,d])" 来显式地提供一个实例。

（实际上，我们通常不必在 with 从句中包含名字 m，Coq 一般足够聪明来确定我们实例化的变量。我们也可以写成： apply trans_eq with [c;d]。）

练习：3 星, standard, optional (apply_with_exercise)

The injection and discriminate Tactics

回想自然数的定义：
     Inductive nat : Type :=
       | O
       | S (n : nat).

我们可从该定义中观察到，所有的数都是两种形式之一：要么是构造子 O， 要么就是将构造子 S 应用到另一个数上。不过这里还有无法直接看到的： 自然数的定义中还蕴含了两个事实：

• 构造子 S 是'单射（Injective）'或'一一对应'的。 即，如果 S n = S m，那么 n = m 必定成立。
• 构造子 O 和 S 是'不相交（Disjoint）'的。 即，对于任何 n，O 都不等于 S n。

类似的原理同样适用于所有归纳定义的类型：所有构造子都是单射的， 而不同构造子构造出的值绝不可能相等。对于列表来说，cons 构造子是单射的， 而 nil 不同于任何非空列表。对于布尔值来说，true 和 false 是不同的。 因为 true 和 false 二者都不接受任何参数，它们既不在这边也不在那边。 其它归纳类型亦是如此。 例如，我们可以使用定义在 Basics.v 中的 pred 函数来证明 S 的单射性。 .

这个技巧可以通过编写等价的 pred 来推广到任意的构造子上 —— 即编写一个“撤销”一次构造子调用的函数。为此，Coq 提供了更加简便的 injection 策略，它能让我们利用任意构造子的单射性。 下面是使用 injection 对上面定理的另一种证法：

通过在此处编写 injection H as Hmn，我们让 Coq 利用构造子的单射性来产生所有它能从 H 所推出的等式（本例中为等式 n = m）。 每一个这样的等式都作为假设（本例中为 Hmn）被添加到上下文中。

以下例子展示了一个 injection 如何直接得出多个等式。

另一方面，如果你只使用 injection H 而不带 as 从句， 那么所有的等式都会在目标的开头被转变为假设。

练习：3 星, standard (injection_ex₃)

So much for injectivity of constructors. What about disjointness? The principle of disjointness says that two terms beginning with different constructors (like O and S, or true and false) can never be equal. This means that, any time we find ourselves in a context where we've assumed that two such terms are equal, we are justified in concluding anything we want, since the assumption is nonsensical. The discriminate tactic embodies this principle: It is used on a hypothesis involving an equality between different constructors (e.g., S n = O), and it solves the current goal immediately. Here is an example:

我们可以通过对 n 进行分类讨论来继续。第一种分类是平凡的。

However, the second one doesn't look so simple: assuming 0 =? (S n') = true, we must show S n' = 0! The way forward is to observe that the assumption itself is nonsensical:

如果我们对这个假设使用 discriminate ， Coq 便会确认我们当前正在证明的目标不可行，并同时移除它，不再考虑。

本例是逻辑学原理'爆炸原理'的一个实例，它断言矛盾的前提会推出任何东西， 甚至是假命题！

爆炸原理可能令你费解，那么请记住上述证明'并不'肯定其后件， 而是说明：'如果'荒谬的前件成立，'那么'就会得出荒谬的结论， 如此一来我们将生活在一个不一致的宇宙中，这里每个陈述都是正确的。 下一章将进一步讨论爆炸原理。

练习：1 星, standard (discriminate_ex₃)

构造子的单射性能让我们论证 ∀ (n m : nat), S n = S m → n = m。 此蕴含式的逆形式是一个构造子和函数的更一般的实例， 在后面我们会发现它用起来很方便：

There is also a tactic named `f_equal` that can prove such theorems. Given a goal of the form f a₁ ... an = g b₁ ... bn, the tactic f_equal will produce subgoals of the form f = g, a₁ = b₁, ..., an = bn. At the same time, any of these subgoals that are simple enough (e.g., immediately provable by reflexivity) will be automatically discharged by f_equal.

对假设使用策略

默认情况下，大部分策略会作用于目标公式并保持上下文不变。然而， 大部分策略还有对应的变体来对上下文中的语句执行类似的操作。 例如，策略 simpl in H 会对上下文中的假设 H 执行化简。

类似地，apply L in H 会针对上下文中的假设 H 匹配某些 （形如 X → Y 中的）条件语句 L。然而，与一般的 apply 不同 （它将匹配 Y 的目标改写为子目标 X），apply L in H 会针对 X 匹配 H，如果成功，就将其替换为 Y。 换言之，apply L in H 给了我们一种“正向推理”的方式：根据 X → Y 和一个匹配 X 的假设，它会产生一个匹配 Y 的假设。作为对比，apply L 是一种“反向推理”：它表示如果我们知道 X → Y 并且试图证明 Y， 那么证明 X 就足够了。 下面是前面证明的一种变体，它始终使用正向推理而非反向推理。

正向推理从'给定'的东西开始（即前提、已证明的定理）， 根据它们迭代地刻画结论直到抵达目标。反向推理从'目标'开始， 迭代地推理蕴含目标的东西，直到抵达前提或已证明的定理。 你在数学或计算机科学课上见过的非形式化证明可能倾向于正向推理。 通常，Coq 习惯上倾向于使用反向推理，但在某些情况下，正向推理更易于思考。

变换归纳假设

在 Coq 中进行归纳证明时，有时控制归纳假设的确切形式是十分重要的。 特别是，在调用 induction 策略前，我们有时需要用 intros 将假设从目标移到上下文中时要十分小心。例如，假设我们要证明 double 函数是单射的 -- 即，它将不同的参数映射到不同的结果：
       Theorem double_injective: ∀ n m,
         double n = double m → n = m.

此证明的开始方式有点微妙：如果我们以
       intros n. induction n.

开始，那么一切都好。然而假如以
       intros n m. induction n.

开始，就会卡在归纳情况中...

此时，归纳假设 IHn' '不会'给出 n' = m' -- 会有个额外的 S 阻碍 -- 因此该目标无法证明。

哪里出了问题？ 问题在于，我们在调用归纳假设的地方已经将 m 引入了上下文中 -- 直观上，我们已经告诉了 Coq“我们来考虑具体的 n 和 m...”， 而现在必须为那些'具体的' n 和 m 证明 double n = double m， 然后才有 n = m。 下一个策略 induction n 告诉 Coq：我们要对 n 归纳来证明该目标。 也就是说，我们要证明对于'所有的' n，命题

• P n = "if double n = double m, then n = m"

成立，需通过证明

• P O
  （即，若“double O = double m 则 O = m”）和
• P n → P (S n)
  （即，若“double n = double m 则 n = m”蕴含“若 double (S n) = double m 则 S n = m”）来得出。

如果我们仔细观察第二个语句，就会发现它说了奇怪的事情：即，对于一个'具体的' m，如果我们知道

• “若 double n = double m 则 n = m”

那么我们就能证明

• “若 double (S n) = double m 则 S n = m”。

要理解为什么它很奇怪，我们来考虑一个具体的（任意但确定的）m -- 比如说 5。该语句就会这样说：如果我们知道

• Q = “若 double n = 10 则 n = 5”

那么我们就能证明

• R = “若 double (S n) = 10 则 S n = 5”。

但是知道 Q 对于证明 R 来说并没有任何帮助！（如果我们试着根据 Q 证明 R，就会以“假设 double (S n) = 10..”这样的句子开始， 不过之后我们就会卡住：知道 double (S n) 为 10 并不能告诉我们 double n 是否为 10。（实际上，它强烈地表示 double n '不是' 10！） 因此 Q 是没有用的。） 当 m 已经在上下文中时，试图对 n 进行归纳来进行此证明是行不通的， 因为我们之后要尝试证明涉及'每一个' n 的命题，而不只是'单个' m。 对 double_injective 的成功证明将 m 留在了目标语句中 induction 作用于 n 的地方：

注意，此时的证明目标和归纳假设是不同的：证明目标要求我们证明更一般的事情 （即，为'每一个' m 证明该语句），而归纳假设 IH 相应地更加灵活， 允许我们在应用归纳假设时选择任何想要的 m。

现在我们选择了一个具体的 m 并引入了假设 double n = double m。 由于我们对 n 做了情况分析，因此还要对 m 做情况分析来保持两边“同步”。

0 的情况很显然：

到这里，由于我们在 destruct m 的第二个分支中，因此上下文中涉及到的 m' 就是我们开始讨论的 m 的前趋。由于我们也在归纳的 S 分支中，这就很完美了： 如果我们在归纳假设中用当前的 m'（此实例由下一步的 apply 自动产生） 实例化一般的 m，那么 IHn' 就刚好能给出我们需要的来结束此证明。

What you should take away from all this is that we need to be careful, when using induction, that we are not trying to prove something too specific: When proving a property involving two variables n and m by induction on n, it is sometimes crucial to leave m generic. 以下练习遵循同样的模式。

练习：2 星, standard (eqb_true)

练习：2 星, advanced (eqb_true_informal)

给出一个详细的 eqb_true 的非形式化证明，量词要尽可能明确。

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

In addition to being careful about how you use intros, practice using "in" variants in this proof. (Hint: use plus_n_Sm.)

在 induction 之前做一些 intros 来获得更一般归纳假设并不总是奏效。 有时需要对量化的变量做一下'重排'。例如，假设我们想要通过对 m 而非 n 进行归纳来证明 double_injective。

问题在于，要对 m 进行归纳，我们首先必须对 n 归纳。 （而如果我们不引入任何东西就执行 induction m，Coq 就会自动为我们引入 n！） 我们可以对它做什么？一种可能就是改写该引理的陈述使得 m 在 n 之前量化。 这样是可行的，不过它不够好：我们不想调整该引理的陈述来适应具体的证明策略！ 我们更想以最清晰自然的方式陈述它。 我们可以先引入所有量化的变量，然后'重新一般化（re-generalize）' 其中的一个或几个，选择性地从上下文中挑出几个变量并将它们放回证明目标的开始处。 用 generalize dependent 策略就能做到。

我们来看一下此定理的非形式化证明。注意我们保持 n 的量化状态并通过归纳证明的命题，对应于我们形式化证明中依赖的一般化。 '定理'：对于任何自然数 n 和 m，若 double n = double m，则 n = m。 '证明'：令 m 为一个 nat。我们通过对 m 进行归纳来证明，对于任何 n， 若 double n = double m，则 n = m。

• 首先，设 m = 0，而 n 是一个数使得 double n = double m。 我们必须证明 n = 0。
  由于 m = 0，根据 double 的定义，我们有 double n = 0。此时对于 n 需要考虑两种情况。若 n = 0，则得证，因为 m = 0 = n，正如所需。 否则，若对于某个 n' 有 n = S n'，我们就会导出矛盾：根据 double 的定义，我们可得出 double n = S (S (double n'))，但它与 double n = 0 相矛盾。
• 其次，设 m = S m'，而 n 同样是一个数使得 double n = double m。 我们必须证明 n = S m'，根据归纳假设，对于任何数 s，若 double s = double m'，则 s = m'。
  根据 m = S m' 的事实以及 double 的定义我们有 double n = S (S (double m'))。 此时对于 n 需要考虑两种情况。
  若 n = 0，则根据 double n = 0 的定义会得出矛盾。
  故存在 n' 使得 n = S n'。再次根据 double 之定义，可得 S (S (double n')) = S (S (double m'))。再由构造子单射可知 double n' = double m'。以n' 代入归纳假设，推得 n' = m'，故显然 S n' = S m'， 其中 S n' = n，S m' = m，所以原命题得证。 ☐

在结束本节之前，我们先稍微跑个题，使用 eqb_true 来证明一个标识符的类似性质以备后用：

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

通过对 l 进行归纳来证明它。

展开定义

It sometimes happens that we need to manually unfold a name that has been introduced by a Definition so that we can manipulate the expression it denotes. For example, if we define...

...并试图证明一个关于 square 的简单事实...

...那么就会卡住：simpl 无法化简任何东西，而由于我们尚未证明任何关于 square 的事实，也就没有任何可以用来 apply 或 rewrite 的东西。 为此，我们可以手动用 unfold 展开 square 的定义：

现在我们有很多工作要做：等式两边都是涉及乘法的表达式， 而我们有很多可用的关于乘法的事实。特别是，我们知道它满足交换性和结合性， 该引理据此不难证明。

现在，是时候讨论下展开和化简了。 我们已经观察到，像 simpl、reflexivity 和 apply 这样的策略， 通常总会在需要时自动展开函数的定义。例如，若我们将 foo m 定义为常量 5...

那么在以下证明中 simpl（或 reflexivity，如果我们忽略 simpl） 就会将 foo m 展开为 (fun x ⇒ 5) m 并进一步将其化简为 5。

然而，这种自动展开有些保守。例如，若我们用模式匹配定义稍微复杂点的函数...

...那么类似的证明就会被卡住：

simpl 没有进展的原因在于，它注意到在试着展开 bar m 之后会留下被匹配的 m，它是一个变量，因此 match 无法被进一步化简。它还没有聪明到发现 match 的两个分支是完全相同的。因此它会放弃展开 bar m 并留在那。 类似地，在试着展开 bar (m+1) 时会留下一个 match，被匹配者是一个函数应用 （即它本身，即便在展开 + 的定义后也无法被化简），因此 simpl 会留下它。 此时有两种方法可以继续。一种是用 destruct m 将证明分为两种情况， 每一种都关注于更具体的 m（O vs S _）。在这两种情况下， bar 中的 match 可以继续了，证明则很容易完成。

这种方法是可行的，不过它依赖于我们能发现隐藏在 bar 中的 match 阻碍了证明的进展。 一种更直白的方式就是明确地告诉 Coq 去展开 bar。

现在很明显，我们在 = 两边的 match 上都卡住了，不用多想就能用 destruct 来结束证明。

对复合表达式使用 destruct

我们已经见过许多通过 destruct 进行情况分析来处理一些变量的值了。 有时我们需要根据某些'表达式'的结果的情况来进行推理。我们也可以用 destruct 来做这件事。 下面是一些例子：

在前面的证明中展开 sillyfun 后，我们发现卡在 if (n =? 3) then ... else ... 上了。但由于 n 要么等于 3 要么不等于，因此我们可以用 destruct (eqb n 3) 来对这两种情况进行推理。 通常，destruct 策略可用于对任何计算结果进行情况分析。如果 e 是某个表达式，其类型为归纳定义的类型 T，那么对于 T 的每个构造子 c，destruct e 都会生成一个子目标，其中（即目标和上下文中）所有的 e 都会被替换成 c。

练习：3 星, standard, optional (combine_split)

以下是 Poly 一章中出现过的 split 函数的实现：

请证明 split 和 combine 在以下概念下互为反函数：

destruct 策略的 eqn: 部分是可选的：目前，我们大部分时间都会包含它， 只是为了文档的目的。 然而在用 destruct 结构复合表达式时，eqn: 记录的信息是十分关键的： 如果我们丢弃它，那么 destruct 会擦除我们完成证明时所需的信息。 例如，假设函数 sillyfun1 定义如下：

Now suppose that we want to convince Coq that sillyfun1 n yields true only when n is odd. If we start the proof like this (with no eqn: on the destruct)...

... then we are stuck at this point because the context does not contain enough information to prove the goal! The problem is that the substitution performed by destruct is quite brutal -- in this case, it thows away every occurrence of n =? 3, but we need to keep some memory of this expression and how it was destructed, because we need to be able to reason that, since n =? 3 = true in this branch of the case analysis, it must be that n = 3, from which it follows that n is odd. What we want here is to substitute away all existing occurences of n =? 3, but at the same time add an equation to the context that records which case we are in. This is precisely what the eqn: qualifier does.

练习：2 星, standard (destruct_eqn_practice)

复习

现在我们已经见过 Coq 中最基础的策略了。未来的章节中我们还会介绍更多， 之后我们会看到一些更加强大的'自动化'策略，它能让 Coq 帮我们处理底层的细节。 不过基本上我们已经有了完成工作所需的东西。 下面是我们已经见过的：

• intros：将前提/变量从证明目标移到上下文中
• reflexivity：（当目标形如 e = e 时）结束证明
• apply：用前提、引理或构造子证明目标
• apply... in H：将前提、引理或构造子应用到上下文中的假设上（正向推理）
• apply... with...：为无法被模式匹配确定的变量显式指定值
• simpl：化简目标中的计算
• simpl in H：化简前提中的计算
• rewrite：使用相等关系假设（或引理）来改写目标
• rewrite ... in H：使用相等关系假设（或引理）来改写前提
• symmetry：将形如 t=u 的目标改为 u=t
• symmetry in H：将形如 t=u 的前提改为 u=t
• unfold：用目标中的右式替换定义的常量
• unfold... in H：用前提中的右式替换定义的常量
• destruct... as...：对归纳定义类型的值进行情况分析
• destruct... eqn:...：为添加到上下文中的等式指定名字， 记录情况分析的结果
• induction... as...: 对归纳定义类型的值进行归纳
• injection: reason by injectivity on equalities between values of inductively defined types
• discriminate: reason by disjointness of constructors on equalities between values of inductively defined types
• assert (H: e)（或 assert (e) as H）：引入“局部引理”e 并称之为 H
• generalize dependent x：将变量 x（以及任何依赖它的东西） 从上下文中移回目标公式内的前提中

附加练习

练习：3 星, standard (eqb_sym)

练习：3 星, advanced, optional (eqb_sym_informal)

根据前面你对该引理的形式化证明，给出与它对应的非形式化证明： 定理：对于任何自然数 n m，n =? m = m =? n. 证明：

练习：3 星, standard, optional (eqb_trans)

练习：3 星, advanced (split_combine)

在前面的练习中，我们证明了对于所有序对的列表，combine 是 split 的反函数。你如何形式化陈述 split 是 combine 的反函数？何时此性质成立？ 请完成下面 split_combine_statement 的定义，其性质指出 split 是 combine 的反函数。之后，证明该性质成立。（除必要的 intros 之外，不要进行更多的 intros，以此来保证你的归纳假设的一般性。 提示：你需要 l₁ 和 l₂ 的什么性质来保证 split (combine l₁ l₂) = (l₁,l₂) 成立？）

练习：3 星, advanced (filter_exercise)

本练习有点难度。为你的归纳假设的形式花点心思。

练习：4 星, advanced, recommended (forall_exists_challenge)

定义两个递归的 Fixpoints，forallb 和 existsb。 第一个检查列表中的每一个元素是否均满足给定的断言：
      forallb oddb [1;3;5;7;9] = true

      forallb negb [false;false] = true

      forallb evenb [0;2;4;5] = false

      forallb (eqb 5) [] = true

第二个检查列表中是否存在一个元素满足给定的断言：
      existsb (eqb 5) [0;2;3;6] = false

      existsb (andb true) [true;true;false] = true

      existsb oddb [1;0;0;0;0;3] = true

      existsb evenb [] = false

接着，用 forallb 和 negb 定义一个 existsb 的非递归版本，名为 existsb'。 最后，证明定理 existsb_existsb' 指出 existsb' 和 existsb 的行为相同。