पैटर्न मिलान प्रकार

Question

मैं सॉर्ट में चारों ओर खेल रहा हूं, एक क्रमबद्ध सूची बनाने की कोशिश कर रहा हूं। मैं सिर्फ एक फ़ंक्शन चाहता था जो [1,2,3,2,4] सूची लेता है और Sorted [1,2,3,4] जैसे कुछ वापस लौटाएगा - यानी खराब हिस्सों को बाहर निकालना, लेकिन वास्तव में पूरी सूची को सॉर्ट नहीं करना।

मैंने सोचा कि मैं lesseq प्रकार के एक फ़ंक्शन को परिभाषित करके शुरू करूंगा, और फिर मैं उस सुंदरता पर आसानी से मिलान कर सकता हूं। शायद यह एक बुरा विचार है।

मुद्दा मैं अभी आ रही है की जड़ है कि (टुकड़ा, तल पर पूरे समारोह)

Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match m with 
     | 0 => match n with 
      | 0 => Some (le_n 0) 
      ... 

typechecking नहीं है; यह कहता है कि यह option (m <= n) की अपेक्षा कर रहा है, लेकिन Some (le_n 0) में option (0 <= 0) है। मुझे समझ में नहीं आता है, क्योंकि जाहिर है कि m और n दोनों संदर्भ में शून्य हैं, लेकिन मुझे नहीं पता कि कोक को कैसे बताना है।

पूरे समारोह है:

Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match m with 
    | 0 => match n with 
     | 0 => Some (le_n 0) 
     | S n_ => None 
     end 
    | S m_ => match n with 
     | 0 => None 
     | S _ => match lesseq m_ n with 
       | Some x=> le_S m n x 
       | None => None 
       end 
      end 
    end. 

शायद मैं अपने आप को के आगे हो रही है और सिर्फ पढ़ने रखने के लिए इससे पहले कि मैं इस से निपटने की जरूरत है।

Answer 1

आप शायद (भले ही आप उस पर टिप्पणी ठीक से आप [le_S MNX] प्रकार आप चाहते हैं नहीं है) निम्नलिखित समारोह को परिभाषित करना चाहते:

 Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match n with 
    | 0 => 
     match m with 
     | 0 => Some (le_n 0) 
     | S m0 => None 
     end 
    | S p => 
     match lesseq m p with 
     | Some l => Some (le_S m p l) 
     | None => None 
     end 
    end. 

लेकिन जैसा कि आप देखा है, typechecker है नए संदर्भ को अनुमानित करने के लिए पर्याप्त चालाक नहीं है जब आप परिणाम के प्रकार में दिखाई देने वाले चर को नष्ट करते हैं। आप निम्नलिखित तरीके से मैच पर टिप्पणी करने के लिए है:

 Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match n return (option (m <= n)) with 
    | 0 => 
     match m return (option (m <= 0)) with 
     | 0 => Some (le_n 0) 
     | S m0 => None 
     end 
    | S p => 
     match lesseq m p with 
     | Some l => Some (le_S m p l) 
     | None => None 
     end 
    end. 

देखें संदर्भ मैनुअल यदि आप वास्तव में समझना चाहते हैं कैसे पैटर्न मिलान निर्भर प्रकार के साथ काम करता है। यदि आप इसके लिए पर्याप्त बहादुर महसूस नहीं करते हैं, तो आप अपने प्रमाण ("परिष्कृत" रणनीति के लिए एक महान उपकरण बनाने के लिए रणनीति तंत्र का उपयोग करना चाहते हैं)।

 Definition lesseq m n : option (m <= n). 
    refine (fix lesseq (m : nat) (n : nat) {struct n} := _). 

    destruct n. 
    destruct m. 
    apply Some; apply le_n. 
    apply None. 

    destruct (lesseq m n). 
    apply Some. 
    apply le_S. 
    assumption. 
    apply None. 
    Defined. 

वैसे, मैं, नहीं लगता कि अपने कार्य वास्तव में मददगार होगा (भले ही यह एक अच्छा विचार है) है, क्योंकि आप निम्नलिखित लेम्मा साबित करने के लिए की आवश्यकता होगी: लेम्मा lesseq_complete: forall एमएन, lesseq एमएन <> कोई नहीं -> एम> एन।

यही कारण है कि लोग Coq.Arith.Compare_dec का उपयोग करते हैं। मज़े करो।

Answer 2

क्या आप इस समारोह को व्यायाम के रूप में लिखना चाहते हैं या केवल अपना बड़ा लक्ष्य पूरा करना चाहते हैं? बाद के मामले में आपको मानक लाइब्रेरी पर एक नज़र डालना चाहिए, जो निर्णय कार्य से भरा है जो यहां नौकरी करेगा, Coq.Arith.Compare_dec; उदाहरण के लिए देखें le_gt_dec।

यह भी ध्यान रखें कि आपके द्वारा प्रस्तावित कार्य केवल आपको जानकारी देगा कि । योग प्रकार { ... } + { ... } से मेल खाने वाले पैटर्न के लिए अधिक उपयोगी है, जिससे आपको निपटने के लिए दो संभावित मामले मिलते हैं।