coq Set或Type如何是命题?< / h1 >

Question

我正在看一篇关于Coq的教程。它按照如下方式构造一个bool类型:

Coq < Inductive bool :  Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

然后用"Check"来显示这些东西是什么

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都成立，那么它对bool中的所有b都成立(因为这是唯一的两个)。

但是我不明白bool_rec或bool_rect的表达式是什么意思。似乎P true(这是bool_rec的Set和bool_rect的Type)被视为命题值。我遗漏了什么?

Answer 1

你对bool_ind的直觉是正确的，但是想想为什么bool_ind意味着你所说的可能有助于澄清其他两个。我们知道

bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b

如果我们把它当作一个逻辑公式来读，我们会得到和你一样的结果:

• 对于bool上的每个谓词P，
  • 如果P true保持，并且
  • 如果P false保持，则
  • 对于每个布尔值b，
    • P b保持

但这不仅仅是一个逻辑公式，它还是一个类型。具体来说，它是一个(依赖的)函数类型。作为函数类型，它表示(如果您允许我为未命名的参数和结果创造名称):

• 给定值P : bool -> Prop，
  • A值Pt : P true，
  • A值Pf : P false，和
  • A值b : bool，
    • 我们可以构造一个值Pb : P b

(当然，这是一个柯里化函数，因此还有其他方法可以将类型分解为散文，但这对于我们的目的来说是最清楚的。)

这里最重要的是，使Coq作为一个定理证明者而同时又是一种编程语言(反之亦然)的是Curry-Howard对应:类型是命题，值是这些命题的证明。例如，简单函数类型->对应于蕴涵，依赖函数类型forall对应于全称量化。(表示法很有暗示性:-))所以在Coq中，为了证明φ→ψ，我们必须构造一个类型为φ -> ψ的值:一个函数，它取一个类型为φ的值(或者换句话说，命题φ的证明)，并用它构造一个类型为ψ的值(命题ψ的证明)。

在Coq中，我们可以这样考虑所有类型，无论这些类型是在Set、Type还是Prop中。(因此，当您说"似乎P为真(它是bool recc的Set和bool_rect的Type)被视为命题值"时，您是对的!)例如，让我们考虑如何自己实现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'时，它看起来不是很"证明"，而是很"程序化"。当然，多亏了库里和霍华德的通信，这些都是一样的。但请注意，相同的实现将足以满足其他两个函数:

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。(给读者的练习:直接实现这些功能)

乍一看，这只是数学归纳法的原理。然而，这也是我们在nat上写递归函数的方式;它们是一样的。一般来说，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'的值是相同的，P n'的值是递归调用f n'的结果。

另一种思考_rec和_ind函数之间等价性的方式——我认为这在无限类型上比在bool上更清晰——是与数学上的ind运算(发生在Prop中)和(结构上的)rec运算(发生在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是nAs的列表。

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'确实与vreplicate_fix中的n'相同，但现在我们似乎不需要显式地提及它。为什么会传入呢?如果我们写出类型，这就很清楚了:

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如何抽象递归模式，以及为什么它足够通用。