数值序对

在 Inductive 类型定义中，每个构造子（Constructor）可以有任意多个参数 —— 可以没有（如 true 和 O），可以只有一个（如 S），也可以更多 （如 nybble，以及下文所示）：

此声明可以读作：“构造数值序对的唯一一种方法，就是将构造子 pair 应用到两个 nat 类型的参数上。”

下述函数分别用于提取二元组中的第一个和第二个分量。

由于二元组十分常用，不妨以标准的数学记法 (x,y) 取代 pair x y。 通过 Notation 向 Coq 声明该记法：

The new notation can be used both in expressions and in pattern matches.

Note that pattern-matching on a pair (with parentheses: (x, y)) is not to be confused with the "multiple pattern" syntax (with no parentheses: x, y) that we have seen previously. The above examples illustrate pattern matching on a pair with elements x and y, whereas, for example, the definition of minus in Basics performs pattern matching on the values n and m:
       Fixpoint minus (n m : nat) : nat :=
         match n, m with
         | O , _ ⇒ O
         | S _ , O ⇒ n
         | S n', S m' ⇒ minus n' m'
         end.

The distinction is minor, but it is worth knowing that they are not the same. For instance, the following definitions are ill-formed:
        (* Can't match on a pair with multiple patterns: *)
        Definition bad_fst (p : natprod) : nat :=
          match p with
          | x, y ⇒ x
          end.

        (* Can't match on multiple values with pair patterns: *)
        Definition bad_minus (n m : nat) : nat :=
          match n, m with
          | (O , _ ) ⇒ O
          | (S _ , O ) ⇒ n
          | (S n', S m') ⇒ bad_minus n' m'
          end.

现在我们来证明一些有关二元组的简单事实。 如果我们以稍显古怪的方式陈述序对的性质，那么有时只需 reflexivity（及其内建的简化）即可完成证明。

但是，如果我们用一种更为自然的方式来陈述此引理的话，只用 reflexivity 还不够。

我们还需要向 Coq 展示 p 的具体结构，这样 simpl 才能对 fst 和 snd 做模式匹配。通过 destruct 可以达到这个目的。

注意：不同于解构自然数产生两个子目标，destruct 在此只产生 一个子目标。这是因为 natprod 只有一种构造方法。

练习：1 星, standard (snd_fst_is_swap)

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

数值列表

通过推广序对的定义，数值'列表'类型可以这样描述： “一个列表要么是空的，要么就是由一个数和另一个列表组成的序对。”

例如，这是一个三元素列表：

和序对一样，使用熟悉的编程记法来表示列表会更方便些。 以下两个声明能让我们用 :: 作为中缀的 cons 操作符， 用方括号作为构造列表的“外围（outfix）”记法。

我们不必完全理解这些声明，但如果你感兴趣的话，我会大致说明一下 发生了什么。注解 "right associativity" 告诉 Coq 当遇到多个 :: 时如何给表达式加括号，如此一来下面三个声明做的就是同一件事：

"at level 60" 告诉 Coq 当遇到表达式和其它中缀运算符时应该如何加括号。 例如，我们已经为 plus 函数定义了 + 中缀符号，它的优先级是 50：
  Notation "x + y" := (plus x y)
                      (at level 50, left associativity).

+ 会比 :: 结合的更紧密，所以 1 + 2 :: [3] 会被解析成 (1 + 2) :: [3] 而非 1 + (2 :: [3])。 (当你在 .v 文件中看到“1 + (2 :: [3])”这样的记法时可能会很疑惑。 最里面那个括住了 3 的方括号，标明了它是一个列表。而外层的方括号则是用来指示 “coqdoc”这部分要被显示为代码而非普通的文本；在生成的 HTML 文件中，外层的方括号是看不到的。) 上面的第二和第三个 Notation 声明引入了标准的方括号记法来表示列表； 第三个声明的右半部分展示了在 Coq 中声明 n 元记法的语法， 以及将它们翻译成嵌套的二元构造子序列的方法。

Repeat

接下来我们看几个用来构造和操作列表的函数。第一个是 repeat 函数，它接受一个数字 n 和一个 count，返回一个长度为 count，每个元素都是 n 的列表。

Length

length 函数用来计算列表的长度。

Append

app 函数用来把两个列表联接起来。

由于下文中 app 随处可见，不妨将其定义为中缀运算符。

Head 与 Tail

下面介绍列表上的两种运算：hd 函数返回列表的第一个元素（即“表头”）； tl 函数返回列表除去第一个元素以外的部分（即“表尾”）。由于空表没有表头， 我们必须传入一个参数作为返回的默认值。

练习

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

完成以下 nonzeros、oddmembers 和 countoddmembers 的定义， 你可以查看测试函数来理解这些函数应该做什么。

练习：3 星, advanced (alternate)

完成以下 alternate 的定义，它从两个列表中交替地取出元素并合并为一个列表， 就像把拉链“拉”起来一样。更多具体示例见后面的测试。 （注意：alternate 有一种自然而优雅的定义，但是这一定义无法满足 Coq 对于 Fixpoint 必须“显然会终止”的要求。如果你发现你被这种解法束缚住了， 可以试着换一种稍微啰嗦一点的解法，比如同时对两个列表中的元素进行操作。 有种可行的解法需要定义新的序对，但这并不是唯一的方法。）

用列表实现口袋（Bag）

bag（或者叫 multiset 多重集）类似于集合，只是其中每个元素都能出现不止一次。 口袋的一种可行的表示是列表。

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

为袋子完成以下 count、sum、add、和 member 函数的定义。

这些命题都能通过 reflexivity 来证明。

Multiset sum is similar to set union: sum a b contains all the elements of a and of b. (Mathematicians usually define union on multisets a little bit differently -- using max instead of sum -- which is why we don't call this operation union.) For sum, we're giving you a header that does not give explicit names to the arguments. Moreover, it uses the keyword Definition instead of Fixpoint, so even if you had names for the arguments, you wouldn't be able to process them recursively. The point of stating the question this way is to encourage you to think about whether sum can be implemented in another way -- perhaps by using one or more functions that have already been defined.

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

你可以把下面这些和 bag 有关的函数当作额外的练习 倘若某口袋不包含所要移除的数字，那么将 remove_one 作用其上不应改变其内容。 （本练习为选做，但高级班的学生为了完成后面的练习，需要写出 remove_one 的定义。）

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

写一个你认为有趣的关于袋子的定理 bag_theorem，然后证明它； 这个定理需要用到 count 和 add。注意，这是个开放性问题。 也许你写下的定理是正确的，但它可能会涉及到你尚未学过的技巧因而无法证明。 如果你遇到麻烦了，欢迎提问！

有关列表的论证

和数字一样，有些列表处理函数的简单事实仅通过化简就能证明。 例如，对于下面这个例子，reflexivity 所做的简化就已经足够了...

...由于 [] 被替换进了 app 定义中相应的“被检”分支 （即经由匹配“仔细检查”过值的表达式），整个匹配得以被简化。 和数字一样，有时对一个列表做分类讨论（是否是空）是非常有用的。

在这里 nil 的情况能够工作是因为我们定义了 tl nil = nil， 而 destruct 策略中 as 注解引入的两个名字，n 和 l'，分别对应了 cons 构造子的两个参数（正在构造的列表的头和尾）。 然而一般来说，许多关于列表的有趣定理都需要用到归纳法来证明， 接下来我们就会看到证明的方法。 （一点点说教：随着不断地深入，若你只是'阅读'证明的话， 并不会获得什么特别有用的东西。搞清楚每一个细节非常重要，你应该在 Coq 中单步执行这些证明并思考每一步在整个证明中的作用，否则练习题将毫无用处。 啰嗦完毕。）

对列表进行归纳

比起对自然数的归纳，读者可能对归纳证明 natlist 这样的数据类型更加陌生。 不过基本思路同样简单。每个 Inductive 声明定义了一组数据值， 这些值可以用声明过的构造子来构造。例如，布尔值可以用 true 或 false 来构造； 自然数可以用 O 或 S 应用到另一个自然数上来构造；而列表可以用 nil 或者将 cons 应用到一个自然数和另一个列表上来构造。 除此以外，归纳定义的集合中元素的形式 '只能是' 构造子对其它项的应用。 这一事实同时也给出了一种对归纳定义的集合进行论证的方法：一个自然数要么是 O，要么就是 S 应用到某个'更小'的自然数上；一个列表要么是 nil， 要么就是 cons 应用到某个数字和某个'更小'的列表上，诸如此类。 所以，如果我们有某个命题 P 涉及列表 l，而我们想证明 P 对 '一切' 列表都成立，那么可以像这样推理：

• 首先，证明当 l 为 nil 时 P l 成立。
• 然后，证明当 l 为 cons n l' 时 P l 成立，其中 n 是某个自然数，l' 是某个更小的列表，假设 P l' 成立.

由于较大的列表总是能够分解为较小的列表，最终这个较小的列表会变成 nil，这两点合在一起就完成了 P 对一切列表 l 成立的证明。下面是个具体的例子：

注意，和归纳自然数时一样，此处 induction 策略的 as... 从句为在 “l₁ 由构造子 cons 构造而来”这一情况时出现的“更小的列表”和归纳假设取了名字。 再次强调，如果你把 Coq 的证明当做静态的文档，那么可能不会有特别多的收获 —— 如果你通过交互式的 Coq 会话来阅读证明，就能看到当前的目标和上下文， 而这些状态在你阅读写下来的脚本时是不可见的。所以一份用自然语言写成的证明 —— 写给人看的 —— 需要包含更多的提示来帮助读者理解当前的状态， 比如第二种情况下的归纳假设到底是什么。 '定理'：对所有的列表 l₁, l₂, 和 l₃， (l₁ ++ l₂) ++ l₃ = l₁ ++ (l₂ ++ l₃)。 '证明': 通过对 l₁ 使用归纳法。

• 首先, 假设 l₁ = []。我们必须证明：
         ([] ++ l₂) ++ l₃ = [] ++ (l₂ ++ l₃),
  这可以通过展开 ++ 的定义得到。
• 然后, 假设 l₁ = n::l₁'，有：
         (l₁' ++ l₂) ++ l₃ = l₁' ++ (l₂ ++ l₃)
  （归纳假设）。我们必须证明：
         ((n :: l₁') ++ l₂) ++ l₃ = (n :: l₁') ++ (l₂ ++ l₃).
  根据 ++ 的定义, 上式等价于：
         n :: ((l₁' ++ l₂) ++ l₃) = n :: (l₁' ++ (l₂ ++ l₃)),
  该式可通过我们的归纳假设立即证得。 ☐

反转列表

举一个更加深入的例子来说明对列表的归纳证明：假设我们使用 app 来定义一个列表反转函数 rev：

为了比目前所见的证明多一点挑战性， 我们来证明反转一个列表不会改变它的长度。 我们的首次尝试在后继这一分支上卡住了....

不妨单独提出引理，阐述 ++ 与 length 形成的等式关系， 以从我们卡住的地方推进证明。

注意，为了让该引理尽可能 '通用'，我们不仅关心由 rev 得到的列表， 还要对 '所有' 的 natlist 进行全称量化。这很自然，因为这个证明目标 显然不依赖于被反转的列表。除此之外，证明这个更普遍的性质也更容易些。 现在我们可以完成最初的证明了。

作为对比，以下是这两个定理的非形式化证明： '定理'：对于所有的列表 l₁ 和 l₂， length (l₁ ++ l₂) = length l₁ + length l₂. '证明'：对 l₁ 进行归纳。

• 首先，假设 l₁ = []。我们必须证明
          length ([] ++ l₂) = length [] + length l₂,
  根据 length、++ 和 plus 的定义，上式显然可得。
• 其次，假设 l₁ = n::l₁'，并且
          length (l₁' ++ l₂) = length l₁' + length l₂.
  我们必须证明
          length ((n::l₁') ++ l₂) = length (n::l₁') + length l₂.
  根据 length 和 ++ 的定义以及归纳假设，上式显然可得。 ☐

'定理': 对于所有的列表 l，length (rev l) = length l。 '证明': 对 l 进行归纳。

• 首先，假设 l = []。我们必须证明
            length (rev []) = length [],
  根据 length 和 rev 的定义，上式显然可得。
• 其次，假设 l = n::l'，并且
            length (rev l') = length l'.
  我们必须证明
            length (rev (n :: l')) = length (n :: l').
  根据 rev 的定义，上式来自于
            length ((rev l') ++ [n]) = S (length l')
  根据之前的引理，此式等同于
            length (rev l') + length [n] = S (length l').
  根据归纳假设和 length 的定义，上式显然可得。 ☐

这些证明的风格实在是冗长而迂腐。读多了之后，我们会发现减少细枝末节， 详述不太显然的步骤更有助于我们理解证明。毕竟细节更容易在大脑中思考， 必要时我们还可以在草稿纸上补全。下面我们以一种更加紧凑的方式呈现之前的证明： '定理'：对于所有 l，length (rev l) = length l。 '证明'：首先，观察到 length (l ++ [n]) = S (length l) 对一切 l 成立， 这一点可通过对 l 的归纳直接得到。当 l = n'::l' 时，通过再次对 l 使用归纳， 然后同时使用之前观察得到的性质和归纳假设即可证明。 ☐ 一般而言，在不同的情况下合适的风格也会不同：读者对这个问题了解程度， 以及当前的证明与读者熟悉的证明之间的相似度都会影响到这一点。 对于我们现在的目的而言，最好先用更加冗长的方式。

Search 搜索

我们已经见过很多需要使用之前证明过的结论（例如通过 rewrite）来证明的定理了。 但是在引用别的定理时，我们必须事先知道它们的名字。当然，即使是已被证明的定理本身 我们都不能全部记住，更不用提它们的名字了。 Coq 的 Search 指令在这时就非常有用了。执行 Search foo 会让 Coq 显示所有涉及到 foo 的定理。例如，去掉下面的注释后， 你会看到一个我们证明过的所有关于 rev 的定理的列表：

在接下来的学习中，你要记得使用 Search，它能为你节约大量的时间！ 如果你正在使用 ProofGeneral，那么可以用 C-c C-a C-a 来运行 Search。 通过 C-c C-; 可以将它返回的结果粘贴到缓冲区内。

列表练习，第一部分

练习：3 星, standard (list_exercises)

更多有关列表的实践：

下面的练习有简短的解法，如果你开始发现情况已经复杂到你无法理清的程度， 请后退一步并试着寻找更为简单的方法。

一个关于你对 nonzeros 的实现的练习：

练习：2 星, standard (eqblist)

填写 eqblist 的定义，它通过比较列表中的数字来判断是否相等。 证明对于所有列表 l，eqblist l l 返回 true。

列表练习, 第二部分

下面这组简单的定理用于证明你之前关于袋子的定义。

练习：1 星, standard (count_member_nonzero)

下面这条关于 leb 的引理可助你完成下一个证明。

Before doing the next exercise, make sure you've filled in the definition of remove_one above.

练习：3 星, advanced (remove_does_not_increase_count)

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

写下一个用到函数 count 和 sum 的，关于袋子的有趣定理 bag_count_sum， 然后证明它。（你可能会发现该证明的难度取决于你如何定义 count！）

练习：4 星, advanced (rev_injective)

求证 rev 是单射函数，即：
    ∀ (l₁ l₂ : natlist), rev l₁ = rev l₂ → l₁ = l₂.

（这个问题既可以用简单的方式解决也可以用繁琐的方式来解决。）

Options 可选类型

假设我们想要写一个返回某个列表中第 n 个元素的函数。如果我们为它赋予类型 nat → natlist → nat，那么当列表太短时我们仍须返回某个数...

这种方案并不好：如果 nth_bad 返回了 42，那么不经过进一步处理的话， 我们无法得知该值是否真的出现在了输入中。（译注：我们无法判断是什么因素让它返回了 42，因为它可能是列表过短时的返回值，同时也可能是（此时列表足够长）在列表中找到的值） 一种更好的方式是改变 nth_bad 的返回类型，使其包含一个错误值作为可能的结果。 我们将此类型命名为 natoption。

然后我们可以修改前面 nth_bad 的定义，使其在列表太短时返回 None， 在列表足够长且 a 在 n 处时返回 Some a。我们将这个新函数称为 nth_error 来表明它可以产生带错误的结果。

（在 HTML 版本中隐藏了这些老套的证明。若你想看它请点击小方格。） 本例也是个介绍 Coq 编程语言更多细微特性的机会，比如条件表达式...

Coq 的条件语句和其它语言中的一样，不过加上了一点更为一般化的特性。 由于 bool 类型不是内建的，因此 Coq 实际上支持在'任何'带有两个构造子的， 归纳定义的类型上使用条件表达式。当断言（guard）求值为 Inductive 定义中的第一个构造子时，它被认为是真的；当它被求值到第二个构造子时， 则被认为是假的。 以下函数从 natoption 中取出一个 nat，在遇到 None 时它将返回提供的默认值。

练习：2 星, standard (hd_error)

用同样的思路修正之前的 hd 函数，使我们无需为 nil 的情况提供默认元素。

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

此练习能帮助你在新的 hd_error 和旧的 hd 之间建立联系。

偏映射（Partial Maps）

最后演示一下如何在 Coq 中定义基础的数据结构。这是一个简单的 '偏映射' 数据类型，它类似于大多数编程语言中的映射或字典数据结构。 首先，我们定义一个新的归纳数据类型 id 来用作偏映射的“键”。

本质上来说，id 只是一个数。但通过 Id 标签封装自然数来引入新的类型， 能让定义变得更加可读，同时也给了我们更多的灵活性。 我们还需要一个 id 的相等关系测试：

练习：1 星, standard (eqb_id_refl)

现在我们定义偏映射的类型：

此声明可以读作：“有两种方式可以构造一个 partial_map：用构造子 empty 表示一个空的偏映射，或将构造子 record 应用到一个键、一个值和一个既有的 partial_map 来构造一个带“键-值”映射 的 partial_map。” update 函数在部分映射中覆盖给定的键以取缔原值（如该键尚不存在， 则新建其记录）。

最后，find 函数按照给定的键搜索一个 partial_map。若该键无法找到， 它就返回 None；若该键与 val 相关联，则返回 Some val。 若同一个键被映到多个值，find 就会返回它遇到的第一个值。

练习：1 星, standard (update_eq)

练习：1 星, standard (update_neq)

练习：2 星, standard (baz_num_elts)

考虑以下归纳定义：

有'多少'个表达式具备类型 baz？（以注释说明。）