我正在阅读关于Coq的教程。它构造了一个 bool 输入如下：
Coq < Inductive bool : Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined
然后它显示了这些东西正在使用“检查”。
Coq < Check bool_ind.
bool_ind
: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
Coq < Check bool_rec.
bool_rec
: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
Coq < Check bool_rect.
bool_rect
: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
我明白 bool_ind。它说如果事情适用 true 它坚持 false那么它适用于所有人 b 在 bool （因为那是唯一的两个）。
但我不明白表达的含义 bool_rec 要么 bool_rect 意思。似乎好像 P true （这是一个 Set 对于 bool_rec 和a Type 对于 bool_rect）被视为命题价值。我在这里想念的是什么？
你的直觉 bool_ind 是现场，但思考为什么 bool_ind 意味着你所说的可能有助于澄清其他两个。我们知道
bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b
如果我们将其视为一个逻辑公式，我们会得到您所做的相同读数：
- 对于每个谓词
P 上 bool是指合同，
- 如果
P true 持有，和
- 如果
P false 等等
- 对于每个布尔值
b，
但这不仅仅是一个逻辑公式，而是一种类型。具体来说，它是（依赖）函数类型。作为一种函数类型，它说（如果你允许我为未命名的参数和结果发明名称的自由）：
- 给定一个价值
P : bool -> Prop，
- 一个值
Pt : P true，
- 一个值
Pf : P false，和
- 一个值
b : bool，
（当然，这是一个curry函数，所以还有其他方法可以将类型分解为散文，但这对我们的目的来说是最清楚的。）
这里最重要的一点是，Coq作为一个定理证明者在编程语言时起作用（反之亦然）是 库里 - 霍华德的通信：类型是命题，值是这些命题的证明。例如，简单的函数类型 -> 对应于暗示和依赖函数类型 forall 对应于普遍量化。 （符号很有启发性:-)）所以在Coq中，要证明φ→ψ，我们必须构造一个类型的值 φ -> ψ：一个取值类型的函数 φ （或换句话说，命题的证明φ）并用它来构造一个类型的值 ψ （命题ψ的证明）。
在Coq中，我们可以用这种方式思考所有类型，无论这些类型是否存在 Set， Type， 要么 Prop。 （所以当你说“似乎P true（这是bool rec的设置和bool_rect的类型）被视为命题值时，”你是对的！）例如，让我们考虑一下我们是怎么做的实行 bool_ind 我们自己。我们首先列出函数的所有参数及其返回类型：
Definition bool_ind' (P : bool -> Prop)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
到现在为止还挺好。在这一点上，我们想要返回一些类型的东西 P b，但我们不知道是什么 b 是。所以，在这些情况下，我们总是模式匹配：
match b with
现在有两个案例。第一， b 可能 true。在这种情况下，我们必须要返回类型的东西 P true，幸运的是我们有这样的价值： Pt。
| true => Pt
该 false 案例类似：
| false => Pf
end.
请注意，当我们实施时 bool_ind'，它看起来不是“证明”，而是非常“程序化”。当然，由于Curry-Howard的对应，这些都是一样的。但请注意，完全相同的实现将足以满足其他两个功能：
Definition bool_rec' (P : bool -> Set)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
Definition bool_rect' (P : bool -> Type)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
看看这个计算定义揭示了另一种方式 bool_ind， bool_rec，和 bool_rect：它们封装了你需要知道的内容 每一个价值 的 bool。但不管怎样，我们正在打包那些信息：如果我知道的话 true等等 false，然后我知道这一切 bool秒。
的定义 bool_{ind,rec,rect} 函数抽象通常我们在布尔值上编写函数：有一个参数对应于真正的分支，一个参数对应于假分支。换句话说：这些功能只是 if 声明。在非依赖类型的语言中，它们可以具有更简单的类型 forall S : Set, S -> S -> bool -> S：
Definition bool_simple_rec (S : Set) (St : P) (Sf : P) (b : bool) : S :=
match b with
| true => St
| false => Sf
end.
但是，因为类型可以依赖于值，所以我们必须对其进行处理 b 通过各种类型。如果事实证明我们不希望这样，我们可以使用我们更通用的功能并告诉：
Definition bool_simple_rec' (S : Set) : S -> S -> bool -> S :=
bool_rec (fun _ => S).
没有人说过我们的 P : bool -> Set 必须 使用 该 bool！
所有这些功能都非常有趣 递归 类型。例如，Coq具有以下类型的自然数：
Inductive nat : Set := O : nat | S : nat -> nat.
我们有
nat_ind : forall P : nat -> Prop,
P O ->
(forall n' : nat, P n' -> P (S n')) ->
forall n : nat,
P n
随着相应的 nat_rec 和 nat_rect。 （为读者练习：直接实现这些功能。）
乍一看，这只是数学归纳的原理。但是，它也是我们编写递归函数的方式 natS;他们是一回事。一般来说，递归函数结束 nat 如下所示：
fix f n => match n with
| O => ...
| S n' => ... f n' ...
end
比赛的手臂紧随其后 O （基本情况）只是类型的值 P O。比赛的手臂紧随其后 S n' （递归情况）是传递给类型函数的东西 forall n' : nat, P n' -> P (S n')： n's是相同的，和的价值 P n' 是递归调用的结果 f n'。
另一种思考等价的方法 _rec 和 _ind 函数，然后 - 我认为在无限类型上比在上面更清楚 bool - 它与数学之间的等价性相同 ind（在...发生） Prop）和（结构） recursion（发生在 Set 和 Type）。
让我们充满热情并使用这些功能。我们将定义一个简单的函数，将布尔值转换为自然数，我们将直接和使用 bool_rec。编写此函数的最简单方法是使用模式匹配：
Definition bool_to_nat_match (b : bool) : nat :=
match b with
| true => 1
| false => 0
end.
另一种定义是
Definition bool_to_nat_rec : bool -> nat :=
bool_rec (fun _ => nat) 1 0.
这两个功能是一样的：
Goal bool_to_nat_match = bool_to_nat_rec.
Proof. reflexivity. Qed.
（注意：这些功能是 句法上相等。这比仅仅做同样的事情更有条件。）
在这里， P : bool -> Set 是 fun _ => nat;它给我们返回类型，它不依赖于参数。我们的 Pt : P true 是 1，当我们被给予时计算的东西 true;同样，我们的 Pf : P false 是 0。
如果我们想要使用依赖项，我们必须编写一个有用的数据类型。怎么样
Inductive has_if (A : Type) : bool -> Type :=
| has : A -> has_if A true
| lacks : has_if A false.
有了这个定义， has_if A true 与...同构 A，和 has_if A false 与...同构 unit。然后我们可以有一个函数，当且仅当它被传递时才保留它的第一个参数 true。
Definition keep_if_match' (A : Type) (a : A) (b : bool) : has_if A b :=
match b with
| true => has A a
| false => lacks A
end.
另一种定义是
Definition keep_if_rect (A : Type) (a : A) : forall b : bool, has_if A b :=
bool_rect (has_if A) (has A a) (lacks A).
他们又是一样的：
Goal keep_if_match = keep_if_rect.
Proof. reflexivity. Qed.
这里，函数的返回类型 是 取决于论点 b所以我们的 P : bool -> Type 实际做了些什么。
这是一个更有趣的例子，使用自然数和长度索引列表。如果你还没有看到长度索引列表，也称为矢量，它们就像他们在锡上说的那样; vec A n 是一个列表 n A秒。
Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A O
| vcons : forall n, A -> vec A n -> vec A (S n).
Arguments vnil {A}.
Arguments vcons {A n} _ _.
（该 Arguments 机器处理隐式参数。）现在，我们想要生成一个列表 n 某些特定元素的副本，因此我们可以使用fixpoint编写它：
Fixpoint vreplicate_fix {A : Type} (n : nat) (a : A) : vec A n :=
match n with
| O => vnil
| S n' => vcons a (vreplicate_fix n' a)
end.
或者，我们可以使用 nat_rect：
Definition vreplicate_rect {A : Type} (n : nat) (a : A) : vec A n :=
nat_rect (vec A) vnil (fun n' v => vcons a v) n.
请注意，因为 nat_rect 捕获递归模式， vreplicate_rect 不是一个固定点本身。有一点需要注意的是第三个参数 nat_rect：
fun n' v => vcons a v
该 v 概念上是递归调用的结果 vreplicate_rect n' a; nat_rect 抽象出递归模式，因此我们不需要直接调用它。该 n' 确实是一样的 n' 如在 vreplicate_fix，但现在看来我们不需要明确提及它。它为什么传入？如果我们写出我们的类型，那就很明显了：
fun (n' : nat) (v : vec A n') => vcons a v : vec A (S n')
我们需要 n' 所以我们知道什么类型 v 有，结果是什么类型的结果。
让我们看看这些功能在起作用：
Eval simpl in vreplicate_fix 0 tt.
Eval simpl in vreplicate_rect 0 tt.
(* both => = vnil : vec unit 0 *)
Eval simpl in vreplicate_fix 3 true.
Eval simpl in vreplicate_rect 3 true.
(* both => = vcons true (vcons true (vcons true vnil)) : vec bool 3 *)
事实上，他们是一样的：
(* Note: these two functions do the same thing, but are not syntactically
equal; the former is a fixpoint, the latter is a function which returns a
fixpoint. This sort of equality is all you generally need in practice. *)
Goal forall (A : Type) (a : A) (n : nat),
vreplicate_fix n a = vreplicate_rect n a.
Proof. induction n; [|simpl; rewrite IHn]; reflexivity. Qed.
上面，我提出了重新实施的练习 nat_rect 和朋友。这是答案：
Fixpoint nat_rect' (P : nat -> Type)
(base_case : P 0)
(recurse : forall n', P n' -> P (S n'))
(n : nat)
: P n :=
match n with
| O => base_case
| S n' => recurse n' (nat_rect' P base_case recurse n')
end.
这有希望说清楚 怎么样 nat_rect 抽象递归模式，以及为什么它足够通用。
你的直觉 bool_ind 是现场，但思考为什么 bool_ind 意味着你所说的可能有助于澄清其他两个。我们知道
bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b
如果我们将其视为一个逻辑公式，我们会得到您所做的相同读数：
- 对于每个谓词
P 上 bool是指合同，
- 如果
P true 持有，和
- 如果
P false 等等
- 对于每个布尔值
b，
但这不仅仅是一个逻辑公式，而是一种类型。具体来说，它是（依赖）函数类型。作为一种函数类型，它说（如果你允许我为未命名的参数和结果发明名称的自由）：
- 给定一个价值
P : bool -> Prop，
- 一个值
Pt : P true，
- 一个值
Pf : P false，和
- 一个值
b : bool，
（当然，这是一个curry函数，所以还有其他方法可以将类型分解为散文，但这对我们的目的来说是最清楚的。）
这里最重要的一点是，Coq作为一个定理证明者在编程语言时起作用（反之亦然）是 库里 - 霍华德的通信：类型是命题，值是这些命题的证明。例如，简单的函数类型 -> 对应于暗示和依赖函数类型 forall 对应于普遍量化。 （符号很有启发性:-)）所以在Coq中，要证明φ→ψ，我们必须构造一个类型的值 φ -> ψ：一个取值类型的函数 φ （或换句话说，命题的证明φ）并用它来构造一个类型的值 ψ （命题ψ的证明）。
在Coq中，我们可以用这种方式思考所有类型，无论这些类型是否存在 Set， Type， 要么 Prop。 （所以当你说“似乎P true（这是bool rec的设置和bool_rect的类型）被视为命题值时，”你是对的！）例如，让我们考虑一下我们是怎么做的实行 bool_ind 我们自己。我们首先列出函数的所有参数及其返回类型：
Definition bool_ind' (P : bool -> Prop)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
到现在为止还挺好。在这一点上，我们想要返回一些类型的东西 P b，但我们不知道是什么 b 是。所以，在这些情况下，我们总是模式匹配：
match b with
现在有两个案例。第一， b 可能 true。在这种情况下，我们必须要返回类型的东西 P true，幸运的是我们有这样的价值： Pt。
| true => Pt
该 false 案例类似：
| false => Pf
end.
请注意，当我们实施时 bool_ind'，它看起来不是“证明”，而是非常“程序化”。当然，由于Curry-Howard的对应，这些都是一样的。但请注意，完全相同的实现将足以满足其他两个功能：
Definition bool_rec' (P : bool -> Set)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
Definition bool_rect' (P : bool -> Type)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
看看这个计算定义揭示了另一种方式 bool_ind， bool_rec，和 bool_rect：它们封装了你需要知道的内容 每一个价值 的 bool。但不管怎样，我们正在打包那些信息：如果我知道的话 true等等 false，然后我知道这一切 bool秒。
的定义 bool_{ind,rec,rect} 函数抽象通常我们在布尔值上编写函数：有一个参数对应于真正的分支，一个参数对应于假分支。换句话说：这些功能只是 if 声明。在非依赖类型的语言中，它们可以具有更简单的类型 forall S : Set, S -> S -> bool -> S：
Definition bool_simple_rec (S : Set) (St : P) (Sf : P) (b : bool) : S :=
match b with
| true => St
| false => Sf
end.
但是，因为类型可以依赖于值，所以我们必须对其进行处理 b 通过各种类型。如果事实证明我们不希望这样，我们可以使用我们更通用的功能并告诉：
Definition bool_simple_rec' (S : Set) : S -> S -> bool -> S :=
bool_rec (fun _ => S).
没有人说过我们的 P : bool -> Set 必须 使用 该 bool！
所有这些功能都非常有趣 递归 类型。例如，Coq具有以下类型的自然数：
Inductive nat : Set := O : nat | S : nat -> nat.
我们有
nat_ind : forall P : nat -> Prop,
P O ->
(forall n' : nat, P n' -> P (S n')) ->
forall n : nat,
P n
随着相应的 nat_rec 和 nat_rect。 （为读者练习：直接实现这些功能。）
乍一看，这只是数学归纳的原理。但是，它也是我们编写递归函数的方式 natS;他们是一回事。一般来说，递归函数结束 nat 如下所示：
fix f n => match n with
| O => ...
| S n' => ... f n' ...
end
比赛的手臂紧随其后 O （基本情况）只是类型的值 P O。比赛的手臂紧随其后 S n' （递归情况）是传递给类型函数的东西 forall n' : nat, P n' -> P (S n')： n's是相同的，和的价值 P n' 是递归调用的结果 f n'。
另一种思考等价的方法 _rec 和 _ind 函数，然后 - 我认为在无限类型上比在上面更清楚 bool - 它与数学之间的等价性相同 ind（在...发生） Prop）和（结构） recursion（发生在 Set 和 Type）。
让我们充满热情并使用这些功能。我们将定义一个简单的函数，将布尔值转换为自然数，我们将直接和使用 bool_rec。编写此函数的最简单方法是使用模式匹配：
Definition bool_to_nat_match (b : bool) : nat :=
match b with
| true => 1
| false => 0
end.
另一种定义是
Definition bool_to_nat_rec : bool -> nat :=
bool_rec (fun _ => nat) 1 0.
这两个功能是一样的：
Goal bool_to_nat_match = bool_to_nat_rec.
Proof. reflexivity. Qed.
（注意：这些功能是 句法上相等。这比仅仅做同样的事情更有条件。）
在这里， P : bool -> Set 是 fun _ => nat;它给我们返回类型，它不依赖于参数。我们的 Pt : P true 是 1，当我们被给予时计算的东西 true;同样，我们的 Pf : P false 是 0。
如果我们想要使用依赖项，我们必须编写一个有用的数据类型。怎么样
Inductive has_if (A : Type) : bool -> Type :=
| has : A -> has_if A true
| lacks : has_if A false.
有了这个定义， has_if A true 与...同构 A，和 has_if A false 与...同构 unit。然后我们可以有一个函数，当且仅当它被传递时才保留它的第一个参数 true。
Definition keep_if_match' (A : Type) (a : A) (b : bool) : has_if A b :=
match b with
| true => has A a
| false => lacks A
end.
另一种定义是
Definition keep_if_rect (A : Type) (a : A) : forall b : bool, has_if A b :=
bool_rect (has_if A) (has A a) (lacks A).
他们又是一样的：
Goal keep_if_match = keep_if_rect.
Proof. reflexivity. Qed.
这里，函数的返回类型 是 取决于论点 b所以我们的 P : bool -> Type 实际做了些什么。
这是一个更有趣的例子，使用自然数和长度索引列表。如果你还没有看到长度索引列表，也称为矢量，它们就像他们在锡上说的那样; vec A n 是一个列表 n A秒。
Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A O
| vcons : forall n, A -> vec A n -> vec A (S n).
Arguments vnil {A}.
Arguments vcons {A n} _ _.
（该 Arguments 机器处理隐式参数。）现在，我们想要生成一个列表 n 某些特定元素的副本，因此我们可以使用fixpoint编写它：
Fixpoint vreplicate_fix {A : Type} (n : nat) (a : A) : vec A n :=
match n with
| O => vnil
| S n' => vcons a (vreplicate_fix n' a)
end.
或者，我们可以使用 nat_rect：
Definition vreplicate_rect {A : Type} (n : nat) (a : A) : vec A n :=
nat_rect (vec A) vnil (fun n' v => vcons a v) n.
请注意，因为 nat_rect 捕获递归模式， vreplicate_rect 不是一个固定点本身。有一点需要注意的是第三个参数 nat_rect：
fun n' v => vcons a v
该 v 概念上是递归调用的结果 vreplicate_rect n' a; nat_rect 抽象出递归模式，因此我们不需要直接调用它。该 n' 确实是一样的 n' 如在 vreplicate_fix，但现在看来我们不需要明确提及它。它为什么传入？如果我们写出我们的类型，那就很明显了：
fun (n' : nat) (v : vec A n') => vcons a v : vec A (S n')
我们需要 n' 所以我们知道什么类型 v 有，结果是什么类型的结果。
让我们看看这些功能在起作用：
Eval simpl in vreplicate_fix 0 tt.
Eval simpl in vreplicate_rect 0 tt.
(* both => = vnil : vec unit 0 *)
Eval simpl in vreplicate_fix 3 true.
Eval simpl in vreplicate_rect 3 true.
(* both => = vcons true (vcons true (vcons true vnil)) : vec bool 3 *)
事实上，他们是一样的：
(* Note: these two functions do the same thing, but are not syntactically
equal; the former is a fixpoint, the latter is a function which returns a
fixpoint. This sort of equality is all you generally need in practice. *)
Goal forall (A : Type) (a : A) (n : nat),
vreplicate_fix n a = vreplicate_rect n a.
Proof. induction n; [|simpl; rewrite IHn]; reflexivity. Qed.
上面，我提出了重新实施的练习 nat_rect 和朋友。这是答案：
Fixpoint nat_rect' (P : nat -> Type)
(base_case : P 0)
(recurse : forall n', P n' -> P (S n'))
(n : nat)
: P n :=
match n with
| O => base_case
| S n' => recurse n' (nat_rect' P base_case recurse n')
end.
这有希望说清楚 怎么样 nat_rect 抽象递归模式，以及为什么它足够通用。