归纳定义的命题

在 Logic 一章中，我们学习了多种方式来书写命题，包括合取、析取和存在量词。 在本章中，我们引入另一种新的方式：'归纳定义（Inductive Definitions）'。 '注意'：为简单起见，本章中的大部分内容都用一个归纳定义的“偶数性”作为展示的例子。 你可能会为此感到不解，因为我们已经有一种将偶数性定义为命题的完美方法了（若 n 等于某个整数的二倍，那么它是是偶数）。尚若如此，那么请放心， 在本章末尾和以后的章节中，我们会看到更多引人入胜的归纳定义的命题示例。 在前面的章节中，我们已经见过两种表述 n 为偶数的方式了： (1) evenb n = true，以及 (2) ∃ k, n = double k。 然而还有一种方式是通过如下规则来建立 n 的偶数性质：

• 规则 ev_0: 0 是偶数。
• 规则 ev_SS: 如果 n 是偶数, 那么 S (S n) 也是偶数。

为了理解这个新的偶数性质定义如何工作，我们可想象如何证明 4 是偶数。 根据规则 ev_SS，需要证明 2 是偶数。这时，只要证明 0 是偶数， 我们可继续通过规则 ev_SS 确保它成立。而使用规则 ev_0 可直接证明 0 是偶数。 接下来的课程中，我们会看到很多类似方式定义的命题。 在非形式化的讨论中，使用简单的记法有助于阅读和书写。 '推断规则（Inference Rules）'就是其中的一种。 （我们为此性质取名为 ev，因为 even 已经用过了。）

	(ev_0)
ev 0

ev n	(ev_SS)
ev (S (S n))

若将上面的规则重新排版成推断规则，我们可以这样阅读它，如果线上方的 '前提（Premises）'成立，那么线下方的'结论（Conclusion）'成立。 比如，规则 ev_SS 读做如果 n 满足 even，那么 S (S n) 也满足。 如果一条规则在线上方没有前提，则结论直接成立。 我们可以通过组合推断规则来展示证明。下面展示如何转译 4 是偶数的证明：
                             -------- (ev_0)
                              ev 0
                             -------- (ev_SS)
                              ev 2
                             -------- (ev_SS)
                              ev 4

（为什么我们把这样的证明称之为“树”而非其他，比如“栈”？ 因为一般来说推断规则可以有多个前提。我们很快就会看到一些例子。

偶数性的归纳定义

基于上述，可将偶数性质的定义翻译为在 Coq 中使用 Inductive 声明的定义， 声明中每一个构造子对应一个推断规则：

这个定义与之前 Inductive 定义的用法有一个有趣的区别：一方面， 我们定义的并不是一个 Type（如 nat），而是一个将 nat 映射到 Prop 的函数——即关于数的性质。然而真正要关注的是，由于 ev 中的 nat 参数出现在冒号'右侧'，这允许在不同的构造子类型中使用不同的值：例如 ev_0 类型中的 0 以及 ev_SS 类型中的 S (S n)。与此相应， 每个构造子的类型必须在冒号后显式指定，并且对于某个自然数 n 来说，每个构造子的类型都必须有 ev n 的形式。 相反，回忆 list 的定义：
    Inductive list (X:Type) : Type :=
      | nil
      | cons (x : X) (l : list X).

它以'全局的方式'在冒号'左侧'引入了参数 X， 强迫 nil 和 cons 的结果为同一个类型（list X）。 如果在定义 ev 时将 nat 置于冒号左侧，就会得到如下错误：

在 Inductive 定义中，类型构造子冒号左侧的参数叫做形参（Parameter）， 而右侧的叫做索引（Index）或注解（Annotation）。 例如，在 Inductive list (X : Type) := ... 中，X 是一个形参；而在 Inductive ev : nat → Prop := ... 中，未命名的 nat 参数是一个索引。 在 Coq 中，我们可以认为 ev 定义了一个性质 ev : nat → Prop，其包括 “证据构造子” ev_0 : ev 0 和 ev_SS : ∀ n, ev n → ev (S (S n))。 这些 “证据构造子” 等同于已经证明过的定理。 具体来说，我们可以使用 Coq 中的 apply 策略和规则名称来证明某个数的 ev 性质……

……或使用函数应用的语法：

我们同样可以对前提中使用到 ev 的定理进行证明。

更一般地，我们可以证明以任意数乘 2 是偶数：

练习：1 星, standard (ev_double)

在证明中使用证据

除了'构造'证据（evidence）来表示某个数是偶数，我们还可以'解构'这样的证据， 这等于对它的构造进行论证。 对 ev 而言，使用 Inductive 声明来引入 ev 会告诉 Coq， ev_0 和 ev_SS 构造子不仅是构造偶数证明证据的有效方式， 还是构造一个数满足 ev 的证据的'唯一'方式。 换句话说，如果某人展示了对于 ev n 的证据 E，那么我们知道 E 必是二者其一：

• E 是 ev_0（且 n 为 O），或
• E 是 ev_SS n' E'（且 n 为 S (S n')，E' 为 ev n' 的证据）.

这样的形式暗示着，我们可以像分析归纳定义的数据结构一样分析形如 ev n 的假设；特别地，对于这类证据使用'归纳（induction）'和'分类讨论（case analysis）'来进行论证也是可行的。让我们通过一些例子来学习实践中如何使用他们。

对证据进行反演

Suppose we are proving some fact involving a number n, and we are given ev n as a hypothesis. We already know how to perform case analysis on n using destruct or induction, generating separate subgoals for the case where n = O and the case where n = S n' for some n'. But for some proofs we may instead want to analyze the evidence that ev n directly. As a tool, we can prove our characterization of evidence for ev n, using destruct.

用 destruct 解构证据即可证明下述定理：

However, this variation cannot easily be handled with just destruct.

直观来说，我们知道支撑前提的证据不会由 ev_0 组成，因为 0 和 S 是 nat 类型不同的构造子；由此 ev_SS 是唯一需要应对的情况（译注：ev_0 无条件成立）。 不幸的是，destruct 并没有如此智能，它仍然为我们生成两个子目标。 更坏的是，于此同时最终目标没有改变，也无法为完成证明提供任何有用的信息。

究竟发生了什么？应用 destruct 把性质的参数替换为对应于构造子的值。 这对于证明 ev_minus2' 是有帮助的，因为在最终目标中直接使用到了参数 n。 然而，这对于 evSS_ev 并没有帮助，因为被替换掉的 S (S n) 并没有在其他地方被使用。 If we remember that term S (S n), the proof goes through. (We'll discuss remember in more detail below.)

Alternatively, the proof is straightforward using our inversion lemma.

Note how both proofs produce two subgoals, which correspond to the two ways of proving ev. The first subgoal is a contradiction that is discharged with discriminate. The second subgoal makes use of injection and rewrite. Coq provides a handy tactic called inversion that factors out that common pattern. The inversion tactic can detect (1) that the first case (n = 0) does not apply and (2) that the n' that appears in the ev_SS case must be the same as n. It has an "as" variant similar to destruct, allowing us to assign names rather than have Coq choose them.

The inversion tactic can apply the principle of explosion to "obviously contradictory" hypotheses involving inductively defined properties, something that takes a bit more work using our inversion lemma. For example:

练习：1 星, standard (inversion_practice)

利用 inversion 策略证明以下结论。（如想进一步练习，请使用反演定理证明之。）

练习：1 星, standard (ev5_nonsense)

请使用 inversion 策略证明以下结果。

The inversion tactic does quite a bit of work. For example, when applied to an equality assumption, it does the work of both discriminate and injection. In addition, it carries out the intros and rewrites that are typically necessary in the case of injection. It can also be applied, more generally, to analyze evidence for inductively defined propositions. As examples, we'll use it to reprove some theorems from chapter Tactics. (Here we are being a bit lazy by omitting the as clause from inversion, thereby asking Coq to choose names for the variables and hypotheses that it introduces.)

inversion 的工作原理大致如下：假设 H 指代上下文中的假设 P， 且 P 由 Inductive 归纳定义，则对于 P 每一种可能的构造，inversion H 各为其生成子目标。子目标中自相矛盾者被忽略，证明其余子命题即可得证原命题。 在证明子目标时，上下文中的 H 会替换为 P 的构造条件， 即其构造子所需参数以及必要的等式关系。例如：倘若 ev n 由 evSS 构造， 上下文中会引入参数 n'、ev n'，以及等式 S (S n') = n。 上面的 ev_double 练习展示了偶数性质的一种新记法，其被之前的两种记法所蕴含。 （因为，由 Logic 一章中的 even_bool_prop，我们已经知道 他们是互相等价的。） 为了展示这三种方式的一致性，我们需要下面的引理：

我们可以尝试使用分类讨论或对 n 进行归纳。但由于 ev 在前提中出现，所以和前面章节的一些例子一样，这种策略行不通， 因为如前面提到的，归纳法则会讨论 n-1，而它并不是偶数！ 如此我们似乎可以先试着对 ev 的证据进行反演。 确实，第一个分类可以被平凡地证明。

然而第二个分类要困难一些。我们需要证明 ∃ k, S (S n') = double k， 但唯一可用的假设是 E'，也即 ev n' 成立。但这对证明并没有帮助， 我们似乎被卡住了，而对 E 进行分类讨论是徒劳的。 如果仔细观察第二个（子）目标，我们可以发现一些有意思的事情： 对 E 进行分类讨论，我们可以把要证明的原始目标归约到另一个上， 其涉及到另一个 ev 的证据： E'。 形式化地说，我们可以通过展示如下证据来完成证明：
        ∃ k', n' = double k',

这同原始的命题是等价的，只是 n' 被替换为 n。确实，通过这个中间结果完成证明 并不困难。

对证据进行归纳

上面的情形看起来似曾相识，但这并非巧合。在 Induction 一章中，我们曾试着用分类讨论来证明其实需要归纳才能证明的命题。 这一次，解决方法仍然是……使用归纳！ 对证据和对数据使用 induction 具有同样的行为：它导致 Coq 对每个可用于构造证据的构造子生成一个子目标，同时对递归出现的问题性质提供了归纳假设。 To prove a property of n holds for all numbers for which ev n holds, we can use induction on ev n. This requires us to prove two things, corresponding to the two ways in which ev n could have been constructed. If it was constructed by ev_0, then n=0, and the property must hold of 0. If it was constructed by ev_SS, then the evidence of ev n is of the form ev_SS n' E', where n = S (S n') and E' is evidence for ev n'. In this case, the inductive hypothesis says that the property we are trying to prove holds for n'. 让我们再次尝试证明这个引理：

这里我们看到 Coq 对 E' 产生了 IH，而 E' 是唯一递归出现的 ev 命题。 由于 E' 中涉及到 n'，这个归纳假设是关于 n' 的， 而非关于 n 或其他数字的。 关于偶数性质的第二个和第三个定义的等价关系如下：

我们会在后面的章节中看到，对证据进行归纳在很多领域里是一种常用的技术， 特别是在形式化程序语言的语义时，由于其中很多有趣的性质都是归纳定义的。 下面的练习提供了一些简单的例子，来帮助你熟悉这项技术。

练习：2 星, standard (ev_sum)

练习：4 星, advanced, optional (ev'_ev)

一般来说，有很多种方式来归纳地定义一个性质。比如说，下面是关于 ev 的另一种（蹩脚的）定义：

请证明这个定义在逻辑上等同于前述定义。为了精简证明，请使用 Logic 一章中将定理应用到参数的技术，注意同样的技术也可用于归纳定义的命题的构造子。

练习：3 星, advanced, recommended (ev_ev__ev)

这里有两个可以试着在其上进行归纳的证据，一个不行就换另一个。

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

本练习只需要使用前述引理，而无需使用归纳或分类讨论， 虽然一些改写可能会比较乏味。

归纳关系

我们可以认为被一个数所参数化的命题（比如 ev）是一个'性质'，也即， 它定义了 nat　的一个子集，其中的数可以被证明满足此命题。 以同样的方式，我们可认为有两个参数的命题是一个'关系'，也即，它定义了一个 可满足此命题的序对集合。

和命题一样，关系也可以归纳地定义。一个很有用的例子是整数的“小于等于”关系。 下面的定义应当是比较直观的。它提供了两种方法来描述一个数小于等于另一个数的证据： 要么可观察到两个数相等，或提供证据显示第一个数小于等于第二个数的前继。　

类似于证明 ev 这样的性质，使用 le_n 和 le_S 构造子来证明关于 ≤ 的事实遵循了同样的模式。我们可以对构造子使用 apply 策略来证明 ≤ 目标 （比如证明 3<=3 或 3<=6），也可以使用 inversion 策略来从上下文中 ≤ 的假设里抽取信息（比如证明 (2<=1) → 2+2=5）。 这里提供一些完备性检查。（请注意，尽管这同我们在开始课程时编写的 函数“单元测试”类似，但我们在这里必须明确地写下他们的证明——simpl 和 reflexivity 并不会有效果，因为这些证明不仅仅是对表达式进行简化。）

现在“严格小于”关系 n < m 可以使用 le 来定义。

这里展示了一些定义于自然数上的关系：

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

请定一个二元归纳关系 total_relation 对每一个自然数的序对成立。

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

请定一个二元归纳关系 empty_relation 对自然数永远为假。

From the definition of le, we can sketch the behaviors of destruct, inversion, and induction on a hypothesis H providing evidence of the form le e₁ e₂. Doing destruct H will generate two cases. In the first case, e₁ = e₂, and it will replace instances of e₂ with e₁ in the goal and context. In the second case, e₂ = S n' for some n' for which le e₁ n' holds, and it will replace instances of e₂ with S n'. Doing inversion H will remove impossible cases and add generated equalities to the context for further use. Doing induction H will, in the second case, add the induction hypothesis that the goal holds when e₂ is replaced with n'.

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

这里展示一些 ≤ 和 < 关系的事实，我们在接下来的课程中将会用到他们。 证明他们将会是非常有益的练习。

Hint: the next one may be easiest to prove by induction on n.

提示：在下面的问题中，对 m 进行归纳会使证明容易一些。

提示：以下定理可以不使用 induction 而证明。

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

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

通过同样的方式，我们可以定义三元关系、四元关系等。例如，考虑以下定义在自然数上的三元关系：

• 下列哪个命题是可以被证明的？
  • R 1 1 2
  • R 2 2 6
• 如果在 R 的定义中我们丢弃 c₅ 构造子，可被证明的集合会发生变化吗？ 简要（一句话）解释你的答案。
• 如果在 R 的定义中我们丢弃 c₄ 构造子，可被证明的集合会发生变化吗？ 简要（一句话）解释你的答案。

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

关系 R 其实编码了一个熟悉的函数。请找出这个函数，定义它并在 Coq 中证明他们等价。

练习：2 星, advanced (subsequence)

如果一个列表的所有元素以相同的顺序出现在另一个列表之中（但允许其中出现其他额外的元素）， 我们把第一个列表称作第二个列表的'子序列'。 例如：
      [1;2;3]

是以下所有列表的子序列
      [1;2;3]
      [1;1;1;2;2;3]
      [1;2;7;3]
      [5;6;1;9;9;2;7;3;8]

但'不是'以下列表的子序列
      [1;2]
      [1;3]
      [5;6;2;1;7;3;8].

• 在 list nat 上定一个归纳命题 subseq，其表达了子序列的涵义。 （提示：你需要三个分类。）
• 证明子序列的自反关系 subseq_refl，也即任何列表是它自身的子序列。
• 证明关系 subseq_app 对任意列表 l₁，l₂ 和 l₃，如果 l₁ 是 l₂ 的子序列，那么 l₁ 也是 l₂ ++ l₃ 的子序列。
• （可选的，困难）证明子序列的传递关系 subseq_trans——也即，如果 l₁ 是 l₂ 的子序列，且 l₂ 是 l₃ 的子序列，那么 l₁ 是 l₃ 的子序列。 （提示：仔细选择进行归纳的项！）

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

假设我们在 Coq 中有如下定义：
    Inductive R : nat → list nat → Prop :=
      | c₁ : R 0 []
      | c₂ n l (H: R n l) : R (S n) (n :: l)
      | c₃ n l (H: R (S n) l) : R n l.

下列命题哪个是可被证明的？

• R 2 [1;0]
• R 1 [1;2;1;0]
• R 6 [3;2;1;0]

案例学习：正则表达式

性质 ev 提供了一个简单的例子来展示归纳定义和其基础的推理技巧， 但这还不是什么激动人心的东西——毕竟，even 等价于我们之前见过的两个非归纳的定义， 而看起来归纳定义并没有提供什么好处。为了更好地展示归纳定义的表达能力， 我们继续使用它来建模计算机科学中的一个经典概念——正则表达式。 正则表达式是用来描述字符串集合的一种简单语言，定义如下：

请注意这个定义是'多态的'：reg_exp T 中的正则表达式描述了字符串， 而其中的字符取自 T——也即，T 的元素构成的列表。 （同一般的实践略有不同，我们不要求类型 T 是有限的。由此可形成一些不同的正则表达式 理论，但对于我们在本章的目的而言并无不同。） 我们通过以下规则来构建正则表达式和字符串，这些规则定义了正则表达式何时匹配一个字符串：

• 表达式 EmptySet 不匹配任何字符串。
• 表达式 EmptyStr 匹配空字符串 [].
• 表达式 Char x 匹配单个字符构成的字符串 [x].
• 如果 re₁ 匹配 s₁, 且 re₂ 匹配 s₂, 那么 App re₁ re₂ 匹配 s₁ ++ s₂.
• 如果 re₁ 和 re₂ 中至少一个匹配 s, 那么 Union re₁ re₂ 匹配 s.
• 最后，如果我们写下某个字符串 s 作为一个字符串序列的连接 s = s_1 ++ ... ++ s_k，且表达式 re 匹配其中每一个字符串 s_i，那么 Star re 匹配 s。
  特别来说，此字符串序列可能为空，因此无论 re 是什么 Star re 总是匹配空字符串 []。

容易把非形式化的定义翻译为使用 Inductive 的定义。我们用记法 s =~ re 表示，通过把该记法用 Reserved “预留”在 Inductive 定义之前，我们就能在定义中使用它！

出于可读性的考虑，在此我们也展示使用推断规则表示的定义。

	(MEmpty)
[] =~ EmptyStr

	(MChar)
[x] =~ Char x

s1 =~ re1    s2 =~ re2	(MApp)
s1 ++ s2 =~ App re1 re2

s1 =~ re1	(MUnionL)
s1 =~ Union re1 re2

s2 =~ re2	(MUnionR)
s2 =~ Union re1 re2

	(MStar0)
[] =~ Star re

s1 =~ re    s2 =~ Star re	(MStarApp)
s1 ++ s2 =~ Star re

请注意这些规则不'完全'等同于之前给出的非形式化定义。 首先，我们并不需要一个规则来直接表述无字符串匹配 EmptySet； 我们做的仅仅是不囊括任何可能导致有字符串被 EmptySet 所匹配的规则。 （的确，归纳定义的语法并不'允许'我们表达类似的“否定规则”（negative rule））。 其次，非形式化定义中的 Union 和 Star 各自对应了两个构造子： MUnionL / MUnionR，和 MStar0 / MStarApp。这在逻辑上等价于 原始的定义，但在 Coq 中这样更加方便，因为递归出现的 exp_match 是作为构造子的直接参数给定的，这在对证据进行归纳时更简单。 （练习 exp_match_ex₁ 和 exp_match_ex₂ 会要求你证明归纳定义中的构造子 和从非形式化规则的表述中提炼的规则确实是等价的。） 接下来我们对一些例子使用这些规则：

（请注意，后一个例子对字符串 [1] 和 [2] 直接应用了 MApp。 由于目标的形式是 [1; 2] 而非 [1] ++ [2]，Coq 并不知道如何分解这个字符串。） 使用 inversion，我们还可以证明某些字符串'不'匹配一个正则表达式：

我们可以定义一些辅助函数来简化正则表达式的书写。函数 reg_exp_of_list 接受一个列表做参数，并构造一个正则表达式来精确地匹配这个列表：

我们还可以证明一些关于 exp_match 的性质。比如，下面的引理显示 任意一个匹配 re 的字符串 s 也匹配 Star re。

（请注意对 app_nil_r 的使用改变了目标，以此可匹配 MStarApp 所需要的形式。）

练习：3 星, standard (exp_match_ex₁)

下面的引理显示从形式化的归纳定义中可以得到本章开始的非形式化匹配规则。

接下来的引理使用了 Poly 一章中出现的 fold 函数： 如果 ss : list (list T) 表示一个字符串序列 s₁, ..., sn，那么 fold app ss [] 是将所有字符串连接的结果。

练习：4 星, standard, optional (reg_exp_of_list_spec)

请证明 reg_exp_of_list 满足以下规范：

由于 exp_match 以递归方式定义，我们可能会发现 关于正则表达式的证明常常需要对证据进行归纳。 比如，假设我们想要证明以下显然的结果：如果正则表达式 re 匹配某个字符串 s， 那么 s 中的所有元素必在 re 中某处以字符字面量的形式出现。 为了表达这个定理，我们首先定义函数 re_chars 来列举一个正则表达式中出现的 所有字符：

接下来我们这样陈述此定理：

Something interesting happens in the MApp case. We obtain two induction hypotheses: One that applies when x occurs in s₁ (which matches re₁), and a second one that applies when x occurs in s₂ (which matches re₂).

我们再次得到了两个归纳假设，它们表明了为什么我们需要对 exp_match 的证据而非 re 进行归纳：对后者的归纳仅仅提供匹配 re 的字符串的归纳假设，却无法允许我们对 In x s₂ 分类进行推理。

练习：4 星, standard (re_not_empty)

请编写一个递归函数 re_not_empty 用来测试某个正则表达式是否会匹配一些字符串。 并证明你的函数是正确的。

remember 策略

induction 策略让人困惑的一个特点是它会接受任意一个项并尝试归纳， 即使这个项不够一般（general）。其副作用是会丢失掉一些信息（类似没有 eqn: 从句的 destruct），并且使你无法完成证明。比如：

仅仅对 H₁ 反演并不会对处理含有递归的分类有太多帮助。（尝试一下！） 因此我们需要对证据进行归纳！下面是一个朴素的尝试：

现在，尽管我们得到了七个分类（正由我们从 exp_match 的定义中期待的那样）， 但 H₁ 还是丢失了一个非常重要的信息：s₁ 事实上匹配了某种形式的 Star re。 这意味着对于'全部'的七个构造子分类我们都需要给出证明，尽管除了其中两个（MStar0 和 MStarApp）之外，剩下的五个构造子分类是和前提矛盾的。 我们仍然可以在一些构造子上继续证明，比如 MEmpty……

……但有一些分类我们却卡住了。比如，对于 MChar 我们需要证明
    s₂ =~ Char x' → x' :: s₂ =~ Char x',

这显然是不可能完成的。

问题是，只有当 Prop 的假设是完全一般的时候，对其使用 induction 的才会起作用， 也即，我们需要其所有的参数都是变量，而非更复杂的表达式，比如 Star re。 （由此，对证据使用 induction 的行为更像是没有 eqn: 的 destruct 而非 inversion。） 解决此问题的一种直接的方式是“手动推广”这个有问题的表达式， 即为此引理添加一个显式的等式：

我们现在可以直接对证据进行归纳，因为第一个假设的参数已经足够一般， 这意味着我们可以通过反演当前上下文中的 re' = Star re 来消解掉多数分类。 这在 Coq 中是一种常用的技巧，因此 Coq 提供了策略来自动生成这种等式， 并且我们也不必改写定理的陈述。

在 Coq 中调用 remember e as x 策略会（1）替换所有表达式 e 为变量 x， （2）在当前上下文中添加一个等式 x = e。我们可以这样使用 remember 来证明上面的结果：

我们现在有 Heqre' : re' = Star re.

Heqre' 与多数分类相互矛盾，因此我们可以直接结束这些分类。

值得注意的分类是 Star。请注意 MStarApp 分类的归纳假设 IH₂ 包含到一个额外的前提 Star re'' = Star re，这是由 remember 所添加的等式所产生的。

练习：4 星, standard, optional (exp_match_ex₂)

下面的引理 MStar''（以及它的逆，之前的练习题中的 MStar'）显示 exp_match 中 Star 的定义等价于前面给出的非形式化定义。

练习：5 星, advanced (weak_pumping)

正则表达式中一个非常有趣的定理叫做'泵引理（Pumping Lemma）'， 非形式化地来讲，它陈述了任意某个足够长的字符串 s 若匹配一个正则表达式 re， 则可以被抽取（pumped）——将 s 的某个中间部分重复任意次产生的新字符串 仍然匹配 re。 （为了简单起见，我们考虑一个比自动机理论课上陈述的定理稍微弱一点的定理。） 我们首先定义什么是“足够长”。由于 Coq 中使用的是构造性逻辑，我们事实上需要计算 对于任何一个正则表达式 re 其最小的“可被抽取（pumpability）”长度。

在证明后面的泵引理时，你会发现关于抽取常量的引理十分有用。

接下来，定义辅助函数 napp 来重复（连接到它自己）一个字符串特定次数。

这个辅助引理在你证明泵引理时也非常有用。

（弱化的）泵引理是说，如果 s =~ re 且 s 的长度最小是 re 的抽取常数（pumping constant）， 那么 s 可分割成三个子字符串 s₁ ++ s₂ ++ s₃，其中 s₂ 可被重复任意次， 其结果同 s₁ 和 s₃ 合并后仍然匹配 re。由于 s₂ 必须为非空字符串， 这是一种（构造性的）方式来以我们想要的长度生成匹配 re 的字符串。

You are to fill in the proof. Several of the lemmas about le that were in an optional exercise earlier in this chapter may be useful.

练习：5 星, advanced, optional (pumping)

Now here is the usual version of the pumping lemma. In addition to requiring that s₂ ≠ [], it also requires that length s₁ + length s₂ ≤ pumping_constant re.

You may want to copy your proof of weak_pumping below.

案例学习：改进互映

在 Logic 一章中，我们经常需要关联起对布尔值的计算和 Prop 中的陈述，然而进行这样的关联往往会导致冗长的证明。请考虑以下定理的证明：

在 destruct 后的第一个分支中，我们解构 n =? m 后生成的等式显式地使用了 eqb_eq 引理，以此将假设 n =? m 转换为假设 n = m；接着使用 rewrite 策略和这个假设来完成此分支的证明。 为了简化这样的证明，我们可定义一个归纳命题，用于对 n =? m 产生更好的分类讨论原理。 它不会生成类似 (n =? m) = true这样的等式，因为一般来说对证明并不直接有用， 其生成的分类讨论原理正是我们所需要的假设: n = m。

性质 reflect 接受两个参数：一个命题 P 和一个布尔值 b。 直观地讲，它陈述了性质 P 在布尔值 b 中所'映现'（也即，等价）： 换句话说，P 成立当且仅当 b = true。为了理解这一点，请注意定义， 我们能够产生 reflect P true 的证据的唯一方式是证明 P 为真并使用 ReflectT 构造子。如果我们反转这个陈述，意味着从 reflect P true 的证明中抽取出 P 的证据也是可能的。与此类似，证明 reflect P false 的唯一方式是合并 ¬ P 的证据和 ReflectF 构造子。 形式化这种直觉并证明 P ↔ b = true 和 reflect P b 这两个表述确实等价是十分容易的。首先是从左到右的蕴含：

Now you prove the right-to-left implication:

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

使用 reflect 而非“当且仅当”连词的好处是，通过解构一个形如 reflect P b 的假设或引理，我们可以对 b 进行分类讨论，同时为两个分支（第一个子目标中的 P 和第二个中的 ¬ P）生成适当的假设。

filter_not_empty_In 的一种更流畅证明如下所示。请注意对 destruct 和 rewrite 的使用是如何合并成一个 destruct 的使用。 （为了更清晰地看到这点，使用 Coq 查看 filter_not_empty_In 的两个证明，并观察在 destruct 的第一个分类开始时证明状态的区别。）

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

使用上面的 eqbP 证明以下定理：

这个小例子展示了互映证明可以怎样为我们提供一些便利。在大型的开发中， 使用 reflect 往往更容易写出清晰和简短的证明脚本。我们将会在后面的章节 和'编程语言基础'一卷中看到更多的例子。 对 reflect 性质的使用已被 'SSReflect' 推广开来，这是一个 Coq 程序库，用于形式化一些数学上的重要结果，包括四色定理和法伊特－汤普森定理。 SSReflect 的名字代表着 'small-scale reflection'，也即，普遍性地使用 互映来简化与布尔值计算有关的证明。

额外练习

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

写出性质的归纳定义是本课程中你需要的重要技能。请尝试去独立解决以下的练习。 列表连续地重复某元素称为 "百叶窗式" (stutter)。 （此概念不同于不包含重复元素：1;4;1 虽然包含重复元素 1， 但因其未连续出现，故不是百叶窗式列表）。 nostutter mylist 表示 mylist 不是百叶窗式列表。 请写出 nostutter 的归纳定义。

请确保以下测试成功，但如果你觉得我们建议的证明（在注释中）并不有效，也可随意更改他们。 若你的定义与我们的不同，也可能仍然是正确的，但在这种情况下可能需要不同的证明。 （你会注意到建议的证明中使用了一些我们尚未讨论过的策略，这可以让证明适用于不同的 nostutter 定义方式。你可以取消注释并直接使用他们，也可以用基础的策略证明这些例子。）

练习：4 星, advanced (filter_challenge)

让我们证明在 Poly 一章中 filter 的定义匹配某个抽象的规范。 可以这样非形式化地描述这个规范： 列表 l 是一个 l₁ 和 l₂ 的“顺序合并”（in-order merge），如果它以 l₁ 和 l₂ 中元素的顺序包含 l₁ 和 l₂ 中的所有元素，尽管可能是交替的。比如：
    [1;4;6;2;3]

是
    [1;6;2]

和
    [4;3].

的顺序合并。 现在，假设我们有集合 X，函数 test: X→bool 和一个类型为 list X 的列表 l。接着接设如果 l 是 l₁ 和 l₂ 的顺序合并，且 l₁ 中的每个元素满足 test， 而 l₂ 中没有元素满足 test，那么 filter test l = l₁。 请将这段规范翻译为 Coq 中的定理并证明它。（你首先需要定义合并两个列表的含义是什么。 请使用归纳关系而非 Fixpoint 来完成。）

练习：5 星, advanced, optional (filter_challenge_2)

另一种刻画 filter 行为的方式是：在 l 的所有其元素满足 test 的子序列中， filter test l 是最长的那个。请形式化这个命题并证明它。

练习：4 星, standard, optional (palindromes)

回文是倒序排列与正序排列相同的序列。

• 在 listX 上定义一个归纳命题 pal 来表达回文的含义。 （提示：你需要三个分类。定义应当基于列表的结构；仅仅使用一个构造子，例如
          c : ∀ l, l = rev l → pal l
  看起来十分显而易见，但并不会很好的工作。)
• 证明（pal_app_rev）
         ∀ l, pal (l ++ rev l).
• 证明（pal_rev that）
         ∀ l, pal l → l = rev l.

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

由于缺乏证据，反方向的证明要困难许多。使用之前练习中定义的 pal 来证明
     ∀ l, l = rev l → pal l.

练习：4 星, advanced, optional (NoDup)

请回忆一下 Logic 章节中性质 In 的定义，其断言值 x 在列表 l 中至少出现一次：

你的第一个任务是使用 In 来定义命题 disjoint X l₁ l₂：仅当列表 l₁ 和 l₂（元素的类型为 X）不含有相同的元素时其可被证明。

接下来，使用 In　定义归纳命题 NoDup X l，其可被证明仅当列表 l （元素类型为 X）的每个元素都不相同。比如，NoDup nat [1;2;3;4] 和 NoDup bool [] 是可被证明的，然而 NoDup nat [1;2;1] 和 NoDup bool [true;true] 是不行的。

最后，使用 disjoint，NoDup 和 ++（列表连接）陈述并证明一个或多个有趣的定理。

练习：4 星, advanced, optional (pigeonhole_principle)

_鸽笼原理（Pigeonhole Principle）'是一个关于计数的基本事实： 将超过 n 个物体放进 n 个鸽笼，则必有鸽笼包含至少两个物体。 与此前诸多情形相似，这一数学事实看似乏味，但其证明手段并不平凡， 如下所述： 首先容易证明一个有用的引理。

现在请定一个性质 repeats，使 repeats X l 断言 l 包含至少一个（类型为 X 的）重复的元素。

现在，我们这样来形式化鸽笼原理。假设列表 l₂ 表示鸽笼标签的列表，列表 l₁ 表示标签被指定给一个列表里的元素。如果元素的个数多于标签的个数，那么至少有两个 元素被指定了同一个标签——也即，列表 l₁ 含有重复元素。 如果使用 excluded_middule 假设并展示 In 是可判定的（decidable）， 即 ∀ x l, (In x l) ∨ ¬ (In x l)，那么这个证明会容易很多。 然而，若'不'假设 In 的可判定性也同样可以证明它；在这样的情况下便不必使用 excluded_middle 假设。

扩展练习：经验证的正则表达式匹配器

我们现在已经定义了正则表达式的匹配关系和多态列表。我们可以使用这些定义来手动地证明 给定的正则表达式是否匹配某个字符串，但这并不是一个可以自动地判断是否匹配的程序。 有理由期待，用于构造匹配关系证据的归纳规则可以被翻译为一个递归函数， 其在正则表达式上的递归对应于这种关系。然而，定义这样的函数并没有那么直接， 由于给定的正则表达式会被 Coq 识别为递归变量，作为结果，Coq 并不会接受这个函数， 即使它总是停机。 重度优化的匹配器会将正则表达式翻译为一个状态机，并决定状态机是否接受 某个字符串。然而，正则表达式匹配也可以通过一个算法来实现，其仅仅操作字符串和 正则表达式，无需定义和维护额外的数据类型，例如状态机。我们将会实现这样的算法， 并验证其值与匹配关系是互映的。 我们将要实现的正则表达式匹配器会匹配由 ASCII 字符构成的列表：

Coq 标准库中包含了一个不同的 ASCII 字符串的归纳定义。然而，为了应用 之前定义的匹配关系，我们在此使用刚刚给出的 ASCII 字符列表作为定义。 我们也可以定义工作在多态列表上的正则表达式匹配器，而非特定于 ASCII 字符列表。 我们将要实现的匹配算法需要知道如何对列表中的元素判断相等，因此需要给定一个 相等关系测试函数。一般化我们给出的定义、定理和证明有一点枯燥，但是可行的。 正则表达式匹配器的正确性证明会由匹配函数的性质和 match 关系的性质组成， match 关系并不依赖匹配函数。我们将会首先证明后一类性质。他们中的多数 将会是很直接的证明，已经被直接给出；少部分关键的引理会留给你来证明。

每个可被证明的 Prop 等价于 True。

其逆可被证明的 Prop 等价于 False。