Coq SetまたはTypeを命題とするには

Question

私は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（これらは唯一の2つなので）に保持されます。

しかし、bool_recまたはbool_rectの表現が何であるか分かりません。あたかもP true（bool_recの場合はSet、bool_rectの場合はType）が命題値として扱われているようです。私はここで何が欠けていますか？

Answer 1

あなたの直感はbool_indですが、理由について考えてみましょう。bool_indは、他の2つを明確にするのに役立つかもしれないという意味です。 P trueが保持している場合、

• 、bool EANS上のすべての述語Pについて
  • ：私たちは、これは論理式として読み取る場合

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

    が、私たちはあなたがたのと同じ値を得ることを知っていますそして

  • P falseが成り立つ場合、
  • すべてのブール値b,
    • P bが含まれる。

しかし、これは単に論理式ではありません、それはタイプです。具体的には、（依存する）関数型です。

• 値P : bool -> Propを考えると、
  • 値Pt : P true、
  ：そして、関数型として、それは（あなたが私に無名の引数と結果の名前を発明の自由を許すだろう場合）と言います
  • 値Pf : P false、そして
  • 値b : bool、
    • 私たちは、値01を構築することができます。

（もちろん、これはカリー化関数であるので、そこ散文にタイプを打破するために、他の方法がありますが、これは我々の目的のために最も明確です。）

ここで重要なのは、プログラミング言語である間にCoqを定理証明者として働かせることです（逆も同様）。Curry-Howard correspondence：型は命題であり、値はそれらの命題の証明です。たとえば、単純な関数タイプ->は含意に対応し、従属関数タイプforallは普遍的な定量化に対応します。 ）Coqでは、φ→ψを証明するために、タイプφ（つまり命題の証明）の値をとる関数φ -> ψの値を構築する必要がありますφ）を計算し、これを使用してタイプψ（命題ψの証明）の値を構築します。

Coqでは、Set、Type、またはPropのいずれであるかにかかわらず、このようにすべてのタイプについて考えることができます。 （だから、「それは真実かどうかのように（bool recのための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 

ここで2つのケースがあります。まず、bをtrueとすることができます。この場合、タイプP trueのものを返す必要があります。幸いなことに、このような値はPtです。

| true => Pt 

false場合も同様です：

| false => Pf 
    end. 

注我々はbool_ind'を実装する場合、それは非常に "proofy、" ではなく、非常に "programmy" を見ていないこと。もちろん、カリー・ハワードのおかげで、これらは同じです。しかし、非常に同じ実装は、他の2つの機能のために十分ですのでご注意：この計算の定義を見てみると

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}関数の定義は、ブール値に関数を書き込む通常の方法よりも抽象的です。真の枝に対応する1つの引数と、偽の枝に1つの引数があります。つまり、これらの関数はちょうどifステートメントです。型は値に依存することができますので、私たちはどこでも種類によってbを通す必要があり、しかし

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). 

誰も私たちのP : bool -> Setが使用boolに持っていた言いませんでした！

タイプのこれらの関数は、いずれももっと面白いです。例えば、コックは自然数の次のような種類があります。

Inductive nat : Set := O : nat | S : nat -> nat. 

をそして、我々は、対応するnat_recとnat_rectとともに

nat_ind : forall P : nat -> Prop, 
      P O -> 
      (forall n' : nat, P n' -> P (S n')) -> 
      forall n : nat, 
       P n 

を持っています。 （読者のための演習：これらの機能を直接実装してください）

一見、これは数学的誘導の原理に過ぎません。しかし、それはまた、nat sに再帰関数を書く方法です。彼らは同じことです。一般的な、再帰関数で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'の結果です。

私はboolよりも無限の種類に明確だと思う当時と_recと_ind機能間の等価、1について考えるもう一つの方法は、それが中で起こる数学ind uction間の等価（と同じだということ-is Prop）および（構造）rec ursion（これは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. 

されており、これら2つの関数は同じです：

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です。ここに答えがあります：

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は再帰パターンを抽象化し、そしてなぜそれが十分に一般的です。