एक कॉक सेट या टाइप एक प्रस्ताव

Question

कैसे हो सकता है मैं Coq पर एक ट्यूटोरियल पढ़ रहा हूं।

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

तो यह पता चलता है इन बातों में से प्रत्येक क्या प्रयोग कर रहे हैं "चेक": यह एक bool प्रकार इस प्रकार निर्माण करती है।

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 में सभी के लिए है (क्योंकि वे केवल दो हैं)।

लेकिन मुझे समझ में नहीं आता कि bool_rec या bool_rect का अर्थ क्या है। ऐसा लगता है कि P true (bool_rec के लिए Set और bool_rect के लिए Type) को प्रस्तावित मूल्य के रूप में माना जा रहा है। मुझे यहां क्या समझ नहीं आ रहा है?

Answer 1

bool_ind के लिए आपका अंतर्ज्ञान स्थान पर है, लेकिन bool_ind का अर्थ है कि आपने जो कहा है, वह अन्य दो को स्पष्ट करने में मदद कर सकता है। ,

• • bool eans पर हर विधेय P के लिए, तो P true रखती है: हम जानते हैं कि

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

    अगर हम इस एक तार्किक सूत्र के रूप में पढ़ते हैं, हम एक ही पढ़ तुमने किया था प्राप्त और

  • यदि P false रखता है, तो
  • प्रत्येक बूलियन 012 के लिए,
    • P b रखता है।

लेकिन यह सिर्फ एक तार्किक सूत्र नहीं है, यह एक प्रकार है। विशेष रूप से, यह एक (आश्रित) फ़ंक्शन प्रकार है। और एक समारोह प्रकार के रूप में, यह कहता है (अगर तुम मुझे अनाम तर्कों और परिणाम के लिए नामों की खोज करने की स्वतंत्रता की अनुमति देंगे):

• एक मूल्य P : bool -> Prop को देखते हुए,
  • एक मूल्य Pt : P true,
  • एक मूल्य Pf : P false, और
  • एक मूल्य b : bool,
    • हम एक मूल्य के निर्माण कर सकते हैं Pb : P b।

(बेशक, यह एक curried समारोह है, इसलिए वहाँ नीचे गद्य में प्रकार तोड़ने के लिए अन्य तरीके हैं, लेकिन यह हमारे उद्देश्यों के लिए स्पष्ट है।)

यहां बड़ी बात यह है कि एक प्रोग्रामिंग भाषा (या इसके विपरीत) होने के दौरान कोक एक प्रमेय प्रोवर्टर के रूप में काम करता है, यह प्रकार Curry-Howard correspondence है: प्रकार प्रस्ताव हैं, और मूल्य उन प्रस्तावों के सबूत हैं। उदाहरण के लिए, सरल फ़ंक्शन प्रकार -> निहितार्थ से मेल खाता है, और निर्भर फ़ंक्शन प्रकार forall सार्वभौमिक मात्रा के अनुरूप है। (नोटेशन बहुत ही सूचक है :-)) तो कोक में, यह साबित करने के लिए कि φ → ψ, हमें φ -> ψ प्रकार का मान बनाना होगा: एक ऐसा फ़ंक्शन जो φ (या दूसरे शब्दों में, प्रस्ताव का सबूत) का मान लेता है φ) और ψ (प्रस्ताव a का सबूत) के मूल्य का निर्माण करने के लिए इसका उपयोग करता है।

कोक में, हम इस तरह के सभी प्रकारों के बारे में सोच सकते हैं, चाहे वे प्रकार Set, Type, या Prop में रहते हैं। (तो जब आप कहते हैं "ऐसा लगता है जैसे पी सच (जो बूल रिक के लिए सेट है और बूल_एक्ट के लिए एक प्रकार है) को प्रोपोज़िशनल वैल्यू के रूप में माना जा रहा है," आप सही हैं!) उदाहरण के लिए, चलो देखते हैं कि हम कैसे खुद को bool_ind लागू करें। हम फ़ंक्शन में सभी पैरामीटर को इसके रिटर्न प्रकार के साथ सूचीबद्ध करके शुरू करेंगे:

Definition bool_ind' (P : bool -> Prop) 
        (Pt : P true) 
        (Pf : P false) 
        (b : bool) 
        : P b := 

अभी तक, बहुत अच्छा है। इस बिंदु पर, हम P b के प्रकार को वापस करना चाहते हैं, लेकिन हम नहीं जानते कि b क्या है। इसलिए, हमेशा इन स्थितियों में, हम पैटर्न मिलान:

match b with 

अब दो मामले हैं। सबसे पहले, btrue हो सकता है। इस मामले में, हमें P true के प्रकार को वापस करना होगा, और सौभाग्य से हमारे पास ऐसा मूल्य है: Pt।

| true => Pt 

false मामले समान है:

| false => Pf 
    end. 

नोट जब हम bool_ind' लागू है, यह नहीं दिखता है कि बहुत "proofy," बल्कि बहुत "programmy"। बेशक, करी-हॉवर्ड पत्राचार के लिए धन्यवाद, ये वही हैं। लेकिन ध्यान दें कि बहुत ही कार्यान्वयन अन्य दो कार्यों के लिए पर्याप्त होगा:

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: वे संपुटित तुम किस बारे में बात करने के लिए पता करने की जरूरत के प्रत्येक मूल्य। लेकिन किसी भी तरह से, हम उस जानकारी को पैकेजिंग कर रहे हैं: अगर मुझे true के लिए कुछ पता है, और false के लिए कुछ है, तो मुझे यह सभी 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. 

हालांकि, क्योंकि प्रकार मूल्यों पर निर्भर कर सकते हैं, हम प्रकार के माध्यम से b हर जगह थ्रेड करना होगा: एक गैर dependently टाइप भाषा में, वे सरल प्रकार 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 था!

ये सभी कार्य रिकर्सिव प्रकारों के लिए बहुत अधिक दिलचस्प हैं। उदाहरण के लिए, Coq प्राकृतिक संख्या निम्न प्रकार है:

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 एस पर रिकर्सिव फ़ंक्शन कैसे लिखते हैं; वे एक ही बात हैं। सामान्य, पुनरावर्ती कार्यों में 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 से अनंत प्रकार पर स्पष्ट है के बारे में सोचना -is है कि यह (के बीच गणितीय ind uction तुल्यता जिसमें होता है के रूप में ही है 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. 

है और इन दो कार्यों के समान हैं:

Goal bool_to_nat_match = bool_to_nat_rec. 
Proof. reflexivity. Qed. 

(नोट: सबसे आसान तरीका है इस समारोह में लिखने के लिए एक पैटर्न मैच के साथ है इन फ़ंक्शन सिंटैक्टिक रूप से के बराबर हैं। यह एक ही चीज़ करने की तुलना में एक मजबूत स्थिति है।)

यहां, P : bool -> Setfun _ => nat है; यह हमें रिटर्न प्रकार देता है, जो तर्क पर निर्भर नहीं है। हमारे Pt : P true1 है, जब हमें true दिया जाता है तो गणना करने की बात; इसी तरह, हमारे Pf : P false0 है।

यदि हम निर्भरता का उपयोग करना चाहते हैं, तो हमें एक उपयोगी डेटा प्रकार बनाना होगा। कैसे

Inductive has_if (A : Type) : bool -> Type := 
    | has : A -> has_if A true 
    | lacks : has_if A false. 

इस परिभाषा के साथ

के बारे में, has_if A trueA isomorphic को है, और has_if A falseunit isomorphic को है। तब हमारे पास एक ऐसा कार्य हो सकता है जो अपना पहला तर्क बरकरार रखे और केवल तभी 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 nnA एस की एक सूची है। वैकल्पिक रूप से

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. 

,:

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 साथ हम 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 और दोस्तों reimplementing का प्रयोग करते बनी हुयी थी।यह स्पष्ट सिर्फ कैसे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. 

यह उम्मीद है कि बनाता है: यहाँ जवाब है।