你的直觉bool_ind是正确的，但想想为什么bool_ind意味着你所说的可能有助于澄清另外两个。我们知道
bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b
如果我们将其视为一个逻辑公式，我们会得到与您相同的读数：
P对于booleans
的每个谓词，
- 如果
P true成立，并且
- 如果
P false成立，那么
- 对于每个布尔值
b，
但这不仅仅是一个逻辑公式，它是一种类型。具体来说，它是一个（依赖）函数类型。作为一个函数类型，它说（如果你允许我为未命名的参数和结果发明名称的自由）：
- 给定一个值
P : bool -> Prop，
- 一个值
Pt : P true，
- 一个值
Pf : P false，和
- 一个值
b : bool，
（当然，这是一个柯里化函数，所以还有其他方法可以将类型分解为散文，但这对于我们的目的来说是最清楚的。）
这里最重要的一点是，让 Coq 在作为编程语言（或反之亦然）的同时作为定理证明器工作的是Curry-Howard 对应关系：类型是命题，值是这些命题的证明。例如，简单函数类型->对应于蕴涵，依赖函数类型forall对应于全称量化。（这个符号很有启发性:-)）所以在 Coq 中，为了证明 φ → ψ，我们必须构造一个类型的值φ -> ψ：一个接受类型值的函数φ（或者换句话说，命题 φ 的证明）并用它来构造一个类型的值ψ（命题 ψ 的证明）。
在 Coq 中，我们可以以这种方式考虑所有类型，无论这些类型存在于Set、Type还是Prop. （因此，当您说“似乎 P true（它是 bool rec 的 Set 和 bool_rect 的 Type）被视为命题值时，”您是对的！）例如，让我们考虑一下我们如何实施bool_ind我们自己。我们将首先列出函数的所有参数及其返回类型：
Definition bool_ind' (P : bool -> Prop)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
到现在为止还挺好。此时，我们想返回 type 的东西P b，但我们不知道是什么b。因此，在这些情况下，我们一如既往地进行模式匹配：
match b with
现在有两种情况。首先，b可能是true。在这种情况下，我们必须要返回一些 type P true，幸运的是我们有这样一个值：Pt。
| true => Pt
false情况类似：
| false => Pf
end.
请注意，当我们实现 时bool_ind'，它看起来并不是非常“可靠”，而是非常“程序化”。当然，多亏了库里-霍华德的对应关系，这些都是一样的。但请注意，对于其他两个功能，相同的实现就足够了：
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，那么我知道所有bools。
函数的定义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（基本情况）只是 type 的值P O。匹配的手臂S n'（递归情况）是传递给 type 函数的内容forall n' : nat, P n' -> P (S n')：n's 是相同的，并且 valueP n'是递归调用的结果f n'。
另一种思考_recand_ind函数之间等价的方法，然后——我认为在无限类型上比 on 更清楚bool——它与数学uction （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 trueis 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 As 的列表。
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 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'确实和 in 一样，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抽象的，以及为什么它足够通用。