数据和函数

1、枚举类型

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

　　上面的例子定义了一个 day 的类型，包括 monday, tuesday, etc. 第二行以及下面可以读作"monday is a day, tuesday is a dat, etc".

　　有了上面 day 的定义，可以可以编写一个关于 day 操作的函数：

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

　　"(d:day) : day"：显示的声明了此函数的参数和返回类型。

　　定义了一个函数后，我们应该检查它是否适用于某些示例。在Coq中实际上有三种不同的方法可以做到这一点。首先，我们可以使用命令 Compute 来评估涉及next_weekday的复合表达式。

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

　　其次，我们可以以Coq示例的形式记录我们期望结果的内容：

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

　　这个声明做了两件事：它产生一个断言（星期六之后的第二个工作日是星期二），它给断言一个可以用来稍后引用的名称。做出断言后，我们也可以让Coq验证它，如下所示：

Proof. simpl. reflexivity. Qed.

　　第三，我们可以要求Coq 从我们的定义（definition）中提取（extract）一个带有高性能编译器的其他更传统的编程语言（OCaml，Scheme或Haskell）的程序.

2、布尔类型

Inductive bool : Type :=
  | true : bool
  | false : bool.

　　布尔函数可以用与上面相同的方式定义：

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

　　最后两个说明了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 "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

　　关于符号的注释：在.v文件中，我们使用方括号来分隔注释中的Coq代码片段; 此约定也由coqdoc文档工具使用，使它们在视觉上与周围文本分开。在文件的HTML版本中，这些文本以不同的字体显示。

　　"Admitted" 命令可用作不完整证据的占位符。我们将在练习中使用它来表明我们要为您留下的部分 - 即，您的工作是用真实的证据替换 Admitted。

3、函数类型

　　Coq中的每个表达式都有一个类型，描述它计算的是什么类型的东西。“ check ”命令要求Coq的打印的表达式的类型。

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

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

Check negb.
(* ===> negb : bool -> bool *)

　　可以读取书写bool → bool和发音为“ bool arrow bool ” 的negb类型，“给定bool类型的输入，此函数生成bool类型的输出。” 类似地，andb的类型，写成bool → bool → bool，可以读取，“给定两个输入，两个类型bool，此函数产生bool类型的输出。”