我正在阅读有关 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_recbool_rect 的表达式是什么意思。似乎 P true(对于 Setbool_rec,对于 0x25181224141 是 Type)被视为值(value)命题 3。我在这里缺少什么?

最佳答案

你对 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 成立,则
  • 对于每个 bool 值 b
  • P b 持有。

  • 但这不仅仅是一个逻辑公式,它是一种类型。具体来说,它是一个(依赖)函数类型。作为一个函数类型,它说(如果你允许我为未命名的参数和结果创造名称的自由):
  • 给定一个值 P : bool -> Prop
  • 一个值 Pt : P true ,
  • Pf : P false
  • 一个值 b : bool ,
  • 我们可以构造一个值 Pb : P b

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

    这里最重要的事情是,使 Coq 在成为编程语言的同时作为定理证明者(反之亦然)的原因是 Curry-Howard correspondence:类型是命题,值是这些命题的证明。例如,简单函数类型 -> 对应于蕴涵,从属函数类型 forall 对应于全称量化。 (这个符号很有启发性:-))所以在 Coq 中,为了证明 φ → ψ,我们必须构造一个类型为 φ -> ψ 的值:一个函数,它采用类型为 φ 的值(或者换句话说,是命题的证明φ) 并用它构造一个类型为 ψ 的值(命题 ψ 的证明)。

    在 Coq 中,我们可以这样考虑所有类型,无论这些类型位于 SetType 还是 Prop 中。 (因此,当您说“似乎 P true(它是 bool rec 的 Set 和 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' 时,它看起来不太“证明”,而是非常“程序化”。当然,多亏了库里-霍华德的通信,这些都是一样的。但请注意,对于其他两个函数,完全相同的实现就足够了:
    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_recbool_rect 的另一种方式:它们封装了谈论 0x251812431 的每个值所需的知识。但无论哪种方式,我们都在打包这些信息:如果我知道 bool 的某些信息,以及 true 的某些信息,那么我知道所有 false 的信息。
    bool 函数的定义抽象了我们在 bool 值上编写函数的通常方式:一个参数对应于真分支,一个对应于假分支。或者,换句话说:这些函数只是 bool_{ind,rec,rect} 语句。在非依赖类型语言中,它们可以具有更简单的类型 if :
    Definition bool_simple_rec (S : Set) (St : P) (Sf : P) (b : bool) : S :=
      match b with
        | true  => St
        | false => Sf
      end.
    

    但是,因为类型可以依赖于值,所以我们必须将 forall S : Set, S -> S -> bool -> S 贯穿所有类型。但是,如果事实证明我们不想要那样,我们可以使用更通用的函数并告诉:
    Definition bool_simple_rec' (S : Set) : S -> S -> bool -> S :=
      bool_rec (fun _ => S).
    

    没有人说过我们的 b 必须使用 P : bool -> Set !

    所有这些函数对于递归类型都更有趣。例如,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
    

    连同相应的 boolnat_rec 。 (读者练习:直接实现这些功能。)

    乍一看,这只是数学归纳法的原理。然而,这也是我们在 nat_rect s 上编写递归函数的方式;它们是一样的。通常,nat 上的递归函数如下所示:
    fix f n => match n with
                 | O    => ...
                 | S n' => ... f n' ...
               end
    
    nat(基本情况)之后的匹配臂只是类型 O 的值。以下P O(递归情况下),本场比赛的 ARM 是什么传入S n'类型的功能:forall n' : nat, P n' -> P (S n')可相同,而n'值是递归调用P n'的结果。

    考虑 f n'_rec 函数之间的等价性的另一种方式——我认为在无限类型上比在 _ind 上更清晰——它与数学上的 123141312312314123141313141312312314年 12313123131315结构)bool ursion(发生在 indProp 中)。

    让我们开始实践并使用这些功能。我们将定义一个将 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.
    

    (注意:这些函数在语法上是相同的。这是比简单地做同样的事情更强的条件。)

    这里, SetType ;它为我们提供了不依赖于参数的返回类型。我们的 bool_recP : bool -> Set ,当我们得到 fun _ => nat 时要计算的东西;类似地,我们的 Pt : P true1

    如果我们想使用依赖项,我们必须编写一个有用的数据类型。怎么样
    Inductive has_if (A : Type) : bool -> Type :=
      | has   : A -> has_if A true
      | lacks : has_if A false.
    

    根据这个定义, truePf : P false 同构, 0has_if A true 同构。然后我们可以有一个函数,当且仅当它传递 A 时,它会保留它的第一个参数。
    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.
    

    这里,函数的返回类型取决于参数 has_if A false ,所以我们的 unit 实际上做了一些事情。

    这是一个更有趣的例子,使用自然数和长度索引列表。如果您还没有看过长度索引列表(也称为向量),那么它们就是它们在 jar 头上所说的那样; trueb P : bool -> Type s 的列表。
    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} _ _.
    

    (vec A n 机制处理隐式参数。)现在,我们想要生成某个特定元素的 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.
    

    或者,我们可以使用 A :
    Definition vreplicate_rect {A : Type} (n : nat) (a : A) : vec A n :=
      nat_rect (vec A) vnil (fun n' v => vcons a v) n.
    

    请注意,由于 Arguments 捕获递归模式,因此 n 本身不是固定点。需要注意的一件事是 nat_rect 的第三个参数:
    fun n' v => vcons a v
    
    nat_rect 在概念上是递归调用 vreplicate_rect 的结果; nat_rect 抽象出递归模式,所以我们不需要直接调用它。 v 确实与 0x25181231343141 中的 vreplicate_rect n' a 相同,但现在看来我们不需要明确提及它。为什么会传入?如果我们写出我们的类型,那就很清楚了:
    fun (n' : nat) (v : vec A n') => vcons a v : vec A (S n')
    

    我们需要 nat_rect,所以我们知道 n' 的类型,以及结果的类型。

    让我们看看这些函数的作用:
    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.
    

    上面,我和 friend 们提出了重新实现n'的练习。答案如下:
    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.
    

    这有希望说明 vreplicate_fix 如何抽象递归模式,以及为什么它足够通用。

    关于types - coq Set 或 Type 如何成为命题,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/17254011/

    10-16 06:44
    查看更多