数据和功能 Data and Functions II

类型 Types

检查 Check

Coq 中的每个表达式都有一个类型，描述它计算的事物类型。Check 命令要求 Coq 打印表示式的类型。

Check true.
(* ===> true : bool *)

如果 Check 后的表达式后面跟着一个冒号和一个类型，Coq 将验证该表示式的类型是否与给定类型匹配，如果没有，则以错误停止。

Check true
  : bool.
Check (negb true)
  : bool.

函数类型 Function Types

像negb本身的 function 也是数据值，就像 true 与 false 一样。它们的类型称为函数类型，并且它们用箭头书写。

Check negb
  : bool → bool.

ngb 的类型，写成 bool → bool 和发音为"bool 箭头 bool"，可以读成"鉴于 bool 类型的输入，此函数产生 bool 类型输出。类似地，可以读成"给予两个 bool 类型的输入，此函数产生 bool 类型的输出"的andb，写成 bool → bool → bool。

从旧类型到新类型 New Types from Old

构造器 Constructors

到目前为止，我们定义的类型是"枚举类型"的例子：它们的定义明确列举了一组有限的元素，称为构造器。下面是一个更有趣的类型定义，其中一个构造器进行参数：

Inductive rgb : Type :=
  | red
  | green
  | blue.
Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

让我们更详细地看看这个问题。 Inductive 定义有两件事：

  • 它定义了一组新的构造器。例如，red, primary, true, false, monday 等是构造者。
  • 它把它们分为一个新的命名类型，如 bool ，rgb ，或 color。

构造器表达式是通过将构造器应用于零或更多其他构造器或构造器表达，遵守构建器参数的申报数和类型而形成的。例如，

  • red
  • true
  • primary red
  • etc.

但不是

  • red primary
  • true red
  • primary (primary red)
  • etc.

特别是，rgb 和 color 的定义表示哪个构造器表示属于组 rgb 和 color ：

  • red, green, 和 blue属于 rgb 组 ;
  • black 和 white属于 color 组;
  • 如果p是属于 rgb 组的构造器表示式，则 primary p（发音为"适用于参数p的构造器原句"）是属于 color 组的构造器表示式
  • 以这些方式形成的构造器表示仅属于 rgb 组和 color组。

Definition monochrome

我们可以定义 colors 上的函数使用模式 match ，就像我们做 day 和 bool。

Definition monochrome (c : color) : bool :=
  match c with
  | black ⇒ true
  | white ⇒ true
  | primary p ⇒ false
  end.

Definition isred

由于 Primary 构造器需要参数，因此匹配 Primary 的模式应包括变量（如上所示 - 请注意，我们可以自由选择其名称）或适当类型的常数（如下所示）。

Definition isred (c : color) : bool :=
  match c with
  | black ⇒ false
  | white ⇒ false
  | primary red ⇒ true
  | primary _ ⇒ false
  end.

此处的模式"primary_"是"除红色外适用于任何 rgb 构造器的 Primary 构造器"的速记。（通配符模式_在单色定义中具有与 monochrome 模式变量 p 相同的效果。

模块 Modules

Coq 提供 modules 系统，以帮助组织大型开发。我们不需要它的大部分功能，但有一个是有用的：如果我们在Module X 和 End X 标记之间包含一组声明，那么，在 End 之后的其余文件中，这些定义被像X.foo这样的名称所引用，而不仅仅是foo。我们将使用此功能来限制定义的范围，以便我们可以自由地重复使用名称。

Module Playground.
  Definition b : rgb := blue.
End Playground.

Definition b : bool := true.

Check Playground.b : rgb.
Check b : bool.

多元组 Tuples

Module TuplePlayground.

具有多个参数的单个构造器可用于创建 Tuple 类型。例如，考虑在 nybble（半字段）中表示四个位。我们首先定义一个类似于bool的数据类型位（使用构造器B0和B1来定义两个可能的位值），然后定义数据类型nybble，它本质上是四个位的元组。

Inductive bit 类似于bool的数据类型位（使用构造器B0和B1来定义两个可能的位值）

Inductive bit : Type :=
  | B0
  | B1.

Inductive nybble 四个位的元组

Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Check (bits B1 B0 B1 B0)
  : nybble.

Definition all_zero 测试一个 ngb ，看看它的所有位是否是B0

bits 构造器充当其内容的包装。拆开可以通过模式匹配完成，如在 all_zero 函数，测试一个 nybble ，看看它的所有位是否是B0。我们使用下划线 （_） 作为通配符模式，以避免发明不会使用的可变名称。

Definition all_zero (nb : nybble) : bool :=
  match nb with
  | (bits B0 B0 B0 B0) ⇒ true
  | (bits _ _ _ _) ⇒ false
  end.

Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : bool *)

End TuplePlayground.

数字 Numbers

我们将此部分放入 module 中，以便我们自己对自然数字的定义不会干扰标准库中的定义。在这本书的其余部分，我们将使用标准图书馆的。

Module NatPlayground.

到目前为止，我们定义的所有类型——无论是"枚举类型"，如 day 、 bool ，还是从它们构建的 bit 和 tuple类型，都是有限的。另一方面，自然数字是一个无限的集合，因此我们需要使用稍微丰富的类型声明形式来表示它们。 有许多数字表示要选择。我们最熟悉的十进制符号（基数 10），例如，使用数字 0 到 9 来表示数字 123。您可能遇到六角符号（基数 16），其中相同的数字表示为 7B，或八度（基数 8），即 173，或二进制（基数 2），其中1111011。使用列举的类型来表示数字，我们可以使用其中任何一个作为我们的表示自然数字。事实上，在某些情况下，这些选择中的每一个都是有用的。 二进制表示在计算机硬件中很有价值，因为数字只能用两个不同的电压水平表示，从而产生简单的电路。类似地，我们希望在这里选择一个使证据更简单的表示。 事实上，数字的表示甚至比二进制数字更简单，即一元数字（基数1），其中只使用一个位数（就像人们通过抓墙来计算监狱中的天数一样）。要用 Coq 数据类型表示一次性数字，我们使用两个构造器。
大写字母O构造器表示为零。

Inductive nat

当S构造器应用于自然编号 n 的表示时，结果为 n+1 的表示，S代表"继承者"（或"刮伤"，如果一个人在监狱中）。下面是完整的数据类型定义。

Inductive nat : Type :=
  | O
  | S (n : nat).

根据这个定义，0代表O，1由S O，2由S（S O），等等。
非正式地，定义的条款可以读取：

  • O是一个自然数字（记住这是字母"O"，而不是数字"0"）。
  • S可以放在自然数前面产生另一个 - 如果n是自然数，那么 S n 也是。

再说一遍，让我们更详细地看看这个问题。 nat 的定义说明了如何构建 nat 集中的表达式：

  • 构造器表示 O 属于nat 集;
  • 如果n是属于 nat 集的构造器表示式，则 S n 也是属于 nat 集的构造器表示式：
  • 以这两种方式形成的构造器表达是属于 nat 集的唯一表示形式。

这些条件是 Inductive 声明的精确力量。它们意味着构造器表达式 O 、构造器表达式 S O 、构造器表达式S （S O）等都属于 nat 集，而其他构造器表示函数（如true, andb true false, S (S false), 和 O (O (O S))）不属于。
这里的一个关键点是，我们到目前为止所做的只是定义数字的表示：一种写下来的方法。名称O和S是任意的，在这一点上，他们没有特殊的含义 - 他们只是两个不同的标记，我们可以用来写下数字（连同一个规则，说任何nat将被写成一些字符串的S标记，然后是O）。如果我们喜欢，我们可以这样写基本相同的定义：

Inductive nat' : Type :=
  | stop
  | tick (foo : nat').

这些标记的解释来自我们如何使用它们进行计算。

Definition pred

我们可以通过编写与自然数字表示相匹配的函数来做到这一点，就像我们在上面用 booleans 和 days 所做的那样 -- 例如，下面是前身函数：

Definition pred (n : nat) : nat :=
  match n with
  | O ⇒ O
  | S n' ⇒ n'
  end.

第二个分支可以读取："如果 n 有 n' 具有有 S n' 的形式，则返回 n'。
以下 End 命令关闭当前模块，因此 nat 将从标准库中引用回该类型。

End NatPlayground.

由于自然数字是一种无处不在的数据形式，Coq为解析和打印它们提供了一点点内置的魔力：普通十进制数可用于替代构建者S和O定义的"单一"符号。默认情况下，Coq 打印十进制数表示数字：

Check (S (S (S (S O)))).
(* ===> 4 : nat *)

Definition minustwo

Definition minustwo (n : nat) : nat :=
  match n with
  | O ⇒ O
  | S O ⇒ O
  | S (S n') ⇒ n'
  end.

Compute (minustwo 4).
(* ===> 2 : nat *)

构造器 S 具有 nat → nat 类型， 就像 pred 和 minustwo 函数一样：

Check S : nat → nat.
Check pred : nat → nat.
Check minustwo : nat → nat.

这些都是可以应用于数字以产生数字的东西。然而，S与其他两者之间有根本的区别：像 pred minustwo 等函数是通过给出计算规则来定义的，例如，pred 的定义说，pred 2 的定义可以简化为1，而 S 的定义没有附加这种行为。虽然它就像一个函数，从意义上说，它可以应用于一个论点，它什么都不做！这只是写下数字的一种方式。
（想想标准十进制数：数字1不是计算，而是数据。当我们写111，意思是数字111，我们用1，3次，写下一个数字的具体表示。
现在，让我们继续定义一些更多的函数，而不是数字。

Fixpoint even

对于涉及数字的最有趣的计算，简单的模式匹配是不够的：我们还需要重复。例如，要检查数字n是否偶数，我们可能需要反复检查n-2是否偶数。这种功能是用关键字" Fixpoint "而不是" Definition "来引入的。

Fixpoint even (n:nat) : bool :=
  match n with
  | O ⇒ true
  | S O ⇒ false
  | S (S n') ⇒ even n'
  end.

Definition odd

我们可以用类似的 Fixpoint 声明来定义 odd ， 但这里有一个更简单的方法：

Definition odd (n:nat) : bool :=
  negb (even n).

Example test_odd1: odd 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_odd2: odd 4 = false.
Proof. simpl. reflexivity. Qed.

（你可能会注意到，如果你通过这些证明，simpl 实际上没有影响的目标 - 所有的工作是由 reflexivity 完成的。我们将讨论为什么这是很快。）

Fixpoint plus

当然，我们也可以通过递归来定义多参数函数。

Module NatPlayground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O ⇒ m
  | S n' ⇒ S (plus n' m)
  end.

现在增加3到2给我们5，正如我们所期待的。

Compute (plus 3 2).
(* ===> 5 : nat *)

Coq 执行的简化步骤可可视化为：

(*      plus 3 2
   i.e. plus (S (S (S O))) (S (S O))
    ==> S (plus (S (S O)) (S (S O)))
          by the second clause of the match
    ==> S (S (plus (S O) (S (S O))))
          by the second clause of the match
    ==> S (S (S (plus O (S (S O)))))
          by the second clause of the match
    ==> S (S (S (S (S O))))
          by the first clause of the match
   i.e. 5  *)

Fixpoint mult n m

作为一种记号上的便利，如果两个或两个以上的论点具有相同的类型，它们可以一起书写。在以下定义中，（n m：nat）的意思和我们写的（n：nat）（m：nat）一样。

Fixpoint mult (n m : nat) : nat :=
  match n with
  | O ⇒ O
  | S n' ⇒ plus m (mult n' m)
  end.

Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.

Fixpoint minus

您可以同时匹配两个表达式，在它们之间放置一个逗号：

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O , _ ⇒ O
  | S _ , O ⇒ n
  | S n', S m' ⇒ minus n' m'
  end.
End NatPlayground2.

Fixpoint exp

Fixpoint exp (base power : nat) : nat :=
  match power with
  | O ⇒ S O
  | S p ⇒ mult base (exp base p)
  end.

练习 Exercise

3: 1 star, standard (factorial)

回想一下标准的数学因子函数：
factorial(0) = 1
factorial(n) = n * factorial(n-1) (if n>0)
将其转换为 Coq。

Fixpoint factorial (n:nat) : nat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_factorial1: (factorial 3) = 6.
(* FILL IN HERE *) Admitted.
Example test_factorial2: (factorial 5) = (mult 10 12).
(* FILL IN HERE *) Admitted.

同样，我们可以通过引入加法、乘法和减法的 Notation 来使数字表达更容易读写。

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.
Check ((0 + 1) + 1) : nat.

（ level 、associativity 和nat_scope注释控制 Coq 解析器如何处理这些注释。详细信息对于当前目的并不重要，但感兴趣的读者可以参考本章末尾的"更多记号"部分。 请注意，这些声明不会改变我们已经做出的定义：它们只是指示 Coq 解析器接受 x + y 代替 plus x y ，相反，到 Coq 漂亮的打印机显示 x + y 作为 plus x y 。 当我们说 Coq 几乎没有内置任何东西时，我们真的是认真的：即使是平等测试也是用户定义的操作！这里有一个函数 eqb ，它测试相等的自然数字，产生一个 boolean 。请注意嵌套 matches 的使用（我们也可以同时使用 match ，就像我们在 minus 中所做的那样。）

Coq代码

Fixpoint factorial (n:nat) : nat
:=
match n with
  | O => S O
  | S n' => mult n (factorial n')
end.

Coq运行截图
图片说明

4: 1 star, standard (ltb)

ltb功函数测试les -than 的自然数字， 产生boolean 。与其为此设置新的 Fixpoint ，不如根据先前定义的函数来定义它。（只需一个以前定义的 function 即可完成，但如果您愿意，可以使用两个。）

Definition ltb (n m : nat) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
Example test_ltb1: (ltb 2 2) = false.
(* FILL IN HERE *) Admitted.
Example test_ltb2: (ltb 2 4) = true.
(* FILL IN HERE *) Admitted.
Example test_ltb3: (ltb 4 2) = false.
(* FILL IN HERE *) Admitted.

eqb 测试相等的自然数字

Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O ⇒ match m with
         | O ⇒ true
         | S m' ⇒ false
         end
  | S n' ⇒ match m with
            | O ⇒ false
            | S m' ⇒ eqb n' m'
            end
  end.

leb 测试第一个参数是否小于或等于其第二个参数

同样，leb功能测试其第一个参数是否小于或等于其第二个参数，从而产生布尔值。

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O ⇒ true
  | S n' ⇒
      match m with
      | O ⇒ false
      | S m' ⇒ leb n' m'
      end
  end.

Example test_leb1: leb 2 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: leb 2 4 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: leb 4 2 = false.
Proof. simpl. reflexivity. Qed.

我们将使用这些（特别是 eqb ）很多，所以让我们给他们中缀表示法（Infix Notation）。

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.

我们现在有两个符号 : = 和 =?，看起来像平等。 我们以后对它们之间的差异和相似性有更多的话要说。目前，需要注意的主要事情是，x = y 是一个合乎逻辑的说法- 一个"命题" - 我们可以尝试证明，而x =? y 是一个表达其值（无论是 true 还是 false），我们可以 Compute 。

两个函数 negb ltb

Coq代码

Definition ltb (n m : nat) : bool
:=
  negb (leb m n).

Coq运行截图
图片说明