问题 coq Set或Type如何成为命题


我正在阅读关于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)被视为命题价值。我在这里想念的是什么?


9988
2018-06-22 18:29


起源



答案:


你的直觉 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 b 成立。

但这不仅仅是一个逻辑公式,而是一种类型。具体来说,它是(依赖)函数类型。作为一种函数类型,它说(如果你允许我为未命名的参数和结果发明名称的自由):

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

(当然,这是一个curry函数,所以还有其他方法可以将类型分解为散文,但这对我们的目的来说是最清楚的。)

这里最重要的一点是,Coq作为一个定理证明者在编程语言时起作用(反之亦然)是 库里 - 霍华德的通信:类型是命题,值是这些命题的证明。例如,简单的函数类型 -> 对应于暗示和依赖函数类型 forall 对应于普遍量化。 (符号很有启发性:-))所以在Coq中,要证明φ→ψ,我们必须构造一个类型的值 φ -> ψ:一个取值类型的函数 φ (或换句话说,命题的证明φ)并用它来构造一个类型的值 ψ (命题ψ的证明)。

在Coq中,我们可以用这种方式思考所有类型,无论这些类型是否存在 SetType, 要么 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_indbool_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 抽象递归模式,以及为什么它足够通用。


16
2018-06-23 00:50



谢谢你非常详细的答案。我还在努力理解它。我不知道库里 - 霍华德的信件,我仍然不太明白。我如何直接使用这些函数(例如定义否定)? (教程中的用法封装在“elim”中,所以我找不到明确使用它们的示例) - dspyz
在你的bool_ind定义中,你有:Pt:P是真的,但不是P是支持类型的元素。某些东西(特别是Pt)的类型是什么类型的支持类型? Pt的类型也是Prop吗?如果是这样,P的重点是什么? - dspyz
我不太确定你的第一个问题是什么。你怎么用 哪一个 功能直接?在第二个问题上:Coq中的每个值都有一个类型: 例如, O : nat 要么 I : True。但是因为Coq是依赖类型的,类型只是(特殊)值,所以它们也必须有类型: nat : Set 和 True : Prop (类型的类型有时称为“种类”,尤其是非依赖类型的语言)。那些类型也必须有类型: Set : Type, Prop : Type。所以我们有 Pt : P true : Prop就像我们一样 O : nat : Set。重点 P 是挑选出特定的命题。 - Antal Spector-Zabusky
是的,但我仍然不明白什么是P true的示例实例?什么是Pt? - dspyz
我的第一个问题是要求对bool_ind进行示例函数调用。我想看看所有的论点是什么样的。 - dspyz


答案:


你的直觉 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 b 成立。

但这不仅仅是一个逻辑公式,而是一种类型。具体来说,它是(依赖)函数类型。作为一种函数类型,它说(如果你允许我为未命名的参数和结果发明名称的自由):

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

(当然,这是一个curry函数,所以还有其他方法可以将类型分解为散文,但这对我们的目的来说是最清楚的。)

这里最重要的一点是,Coq作为一个定理证明者在编程语言时起作用(反之亦然)是 库里 - 霍华德的通信:类型是命题,值是这些命题的证明。例如,简单的函数类型 -> 对应于暗示和依赖函数类型 forall 对应于普遍量化。 (符号很有启发性:-))所以在Coq中,要证明φ→ψ,我们必须构造一个类型的值 φ -> ψ:一个取值类型的函数 φ (或换句话说,命题的证明φ)并用它来构造一个类型的值 ψ (命题ψ的证明)。

在Coq中,我们可以用这种方式思考所有类型,无论这些类型是否存在 SetType, 要么 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_indbool_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 抽象递归模式,以及为什么它足够通用。


16
2018-06-23 00:50



谢谢你非常详细的答案。我还在努力理解它。我不知道库里 - 霍华德的信件,我仍然不太明白。我如何直接使用这些函数(例如定义否定)? (教程中的用法封装在“elim”中,所以我找不到明确使用它们的示例) - dspyz
在你的bool_ind定义中,你有:Pt:P是真的,但不是P是支持类型的元素。某些东西(特别是Pt)的类型是什么类型的支持类型? Pt的类型也是Prop吗?如果是这样,P的重点是什么? - dspyz
我不太确定你的第一个问题是什么。你怎么用 哪一个 功能直接?在第二个问题上:Coq中的每个值都有一个类型: 例如, O : nat 要么 I : True。但是因为Coq是依赖类型的,类型只是(特殊)值,所以它们也必须有类型: nat : Set 和 True : Prop (类型的类型有时称为“种类”,尤其是非依赖类型的语言)。那些类型也必须有类型: Set : Type, Prop : Type。所以我们有 Pt : P true : Prop就像我们一样 O : nat : Set。重点 P 是挑选出特定的命题。 - Antal Spector-Zabusky
是的,但我仍然不明白什么是P true的示例实例?什么是Pt? - dspyz
我的第一个问题是要求对bool_ind进行示例函数调用。我想看看所有的论点是什么样的。 - dspyz