数据和功能 Data and Functions I

枚举类型 Enumerated Types

Inductive day

以下声明告诉 Coq，我们正在定义一组数据值 - a type。

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

新 type 称为 day ，其成员为 monday、tuesday 等。 定义了 day 后，我们可以编写在 day 上操作的 function 。

Definition next_weekday

Definition next_weekday (d:day) : day :=
  match d with
  | monday ⇒ tuesday
  | tuesday ⇒ wednesday
  | wednesday ⇒ thursday
  | thursday ⇒ friday
  | friday ⇒ monday
  | saturday ⇒ monday
  | sunday ⇒ monday
  end.

需要注意的一点是，明确声明此函数的参数和返回类型。与大多数功能性编程语言一样，Coq 经常可以在未明确给出这些类型时自行找出这些类型（即它可以进行类型推理）但通常我们会将其包括在内，以便于阅读。
定义了一个 function 后，我们接下来应该检查它是否适用于某些示例。
实际上，在 Coq 中，有三种不同的方法可以做这些例子。

计算 Compute

首先，我们可以使用命令 Compute 来评估涉及 next_weekday 的复合表达。

Compute (next_weekday friday).
(* ==> monday : day *)

Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

示例 Example

其次，我们可以以 Coq Example 的形式记录我们期望的结果：

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.

此声明有两件事：它做出断言（ Saturday 之后的第二个工作日是 Tuesday），并且它给断言起一个名字，以后可以用来参考它。在做出断言后，我们还可以要求 Coq 这样验证它：

Proof. simpl. reflexivity. Qed.

提取 Extract

第三，我们可以要求 Coq 从我们的定义中提取另一种更传统的编程语言（OCaml、计划或哈斯克尔）中的程序，并配备高性能编译器。

家庭作业提交指南

不要改变划分练习的"标记"：练习头、练习名称、末尾的"空方括号"标记等。请留下这个标记。
不要删除练习。如果您跳过练习（例如，因为它被标记为"可选"，或者因为无法解决它），请确定在您的.v文件中留下部分证据。这种情况下，请确保它以 Admitted 结束（而不是，例如 Abort）。
在解决方案中使用其他定义（帮助功能、有用的 Lemmas 等）是可以的。你可以把这些放在练习头和你被要求证明的定理之间。
如果你介绍一个帮手 Lemma ，你最终无法证明，因此用 Admitted 结束它，然后确保也用 Admitted 结束你使用它的主要定理，而不是Qed。

布尔值 Booleans

Inductive bool

以类似的方式，我们可以定义布尔值的标准类型 bool ，成员 true 和 false 。

Inductive bool : Type :=
  | true
  | false.

Definition negb

对 Booleans 的 Function 可以以与上述相同的方式定义：

Definition negb (b:bool) : bool :=
  match b with
  | true ⇒ false
  | false ⇒ true
  end.

Definition andb

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ⇒ b2
  | false ⇒ false
  end.

Definition orb

Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ⇒ true
  | false ⇒ b2
  end.

（虽然我们在这里滚动我们自己的布尔值，以建立一切从零开始，Coq当然提供一个默认的布尔值的实施，以及许多有用的 Functions 和 Lemmas 。只要有可能，我们将命名我们自己的定义和定理，以便它们与标准库中的定义和定理完全一致。 最后两个说明了 Coq 的多参数函数定义语法。相应的多参数应用语法由以下"单位测试"说明，该测试构成了 orb 函数的完整规范 （真值表）：

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.

符号 Notation

我们还可以介绍一些熟悉的固定语法，我们刚刚定义的布尔值操作。 Notation 命令为现有定义定义了新的符号符号。

Notation "x && y" := (andb x y).

Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

Notation 说明：在.v文件，我们使用方括号在注释中划定 Coq 代码的片段;此公约也由coqdoc文档工具使用，使其在视觉上与周围的文本保持独立。在 HTML 版本的文件中，这些文本以不同的字体显示。
这些示例也是引入 Coq 编程语言的又一个小功能的机会：有条件表达式。

有条件表达式 Conditional Expressions

Definition negb' (b:bool) : bool :=
  if b then false
  else true.

Definition andb' (b1:bool) (b2:bool) : bool :=
  if b1 then b2
  else false.

Definition orb' (b1:bool) (b2:bool) : bool :=
  if b1 then true
  else b2.

Coq 的条件与任何其他语言中的条件完全一样，具有一个小概括。由于bool类型不是内置的，Coq 实际上支持有条件的表达方式，而不是任何具有电感定义的类型，其定义中正好有两个子句。如果保护者对 Inductive 定义第一条款的"构造者"进行评估（在这种情况下恰好被称为 true ），则该护卫被视为 true ，如果对第二个条款进行评估则被视为 false 。

练习 Exercise

1: 1 star, standard (nandb)

命令 Admitted 可用作不完整证据的占位符。我们在练习中使用它来指示我们要留给你的部分 - 即， 你的工作是用真实的 Proofs 来取代 Admitted 。 删除" Admitted "，并完成以下功能的定义：然后确保以下 Examples 断言可以由 Coq 验证。（即，按照上面的 orb 测试模型填写每个证明，并确保 Coq 接受它。如果其中一项或两项输入都是 false 的，则该函数应返回 true 。

Definition nandb (b1:bool) (b2:bool) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_nandb1: (nandb true false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb2: (nandb false false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb3: (nandb false true) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb4: (nandb true true) = false.
(* FILL IN HERE *) Admitted.

Coq代码

Definition nandb (b1:bool) (b2:bool) : bool 
:= 
if andb b1 b2 then false
else true.

Coq运行截图

2: 1 star, standard (andb3)

对下面的 andb3 功能也做同样的操作。当所有输入都是 true 的时候返回 true，否则这个功能应该会返回 false 。

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_andb31: (andb3 true true true) = true.
(* FILL IN HERE *) Admitted.
Example test_andb32: (andb3 false true true) = false.
(* FILL IN HERE *) Admitted.
Example test_andb33: (andb3 true false true) = false.
(* FILL IN HERE *) Admitted.
Example test_andb34: (andb3 true true false) = false.
(* FILL IN HERE *) Admitted.

Coq代码

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
:=
if andb(andb b1 b2) b3 then true
else false.

Coq运行截图