एक मैच ब्लॉक की एक शाखा के अंदर, मैं इस धारणा का उपयोग कैसे करूं कि मिलान की अभिव्यक्ति शाखा के डेटा कन्स्ट्रक्टर अभिव्यक्ति के बराबर है?

Question

मैं एक प्रोग्रामिंग शैली विकसित करने की कोशिश कर रहा हूं जो जल्द से जल्द खराब इनपुट को रोकने पर आधारित है। उदाहरण के लिए, प्राकृतिक संख्या पर पूर्ववर्ती समारोह के लिए निम्नलिखित प्रशंसनीय परिभाषा के बजाय:

Definition pred1 n := 
    match n with 
    | O => None 
    | S n => Some n 
    end. 

मैं इस प्रकार के रूप में यह लिखना चाहते हैं:

Theorem nope n (p : n = O) (q : n <> O) : False. 
    contradict q. 
    exact p. 
Qed. 

Definition pred2 n (q : n <> O) := 
    match n with 
    | S n => n 
    | O => 
     let p := _ in 
     match nope n p q with end 
    end. 

लेकिन मैं पता नहीं है क्या साथ _ को बदलने के लिए । मेरा अंतर्ज्ञान मुझे बताता है कि शाखा में कुछ assumption : n = O उपलब्ध होना चाहिए। क्या वास्तव में कोक इस तरह की धारणा पेश करता है? यदि हां, तो इसका नाम क्या है?

Answer 1

Coq स्वचालित रूप से इस तरह के परिकल्पना को लागू नहीं है, लेकिन आप match निर्माण का पूर्ण रूप का उपयोग करके यह स्पष्ट रूप से लागू कर सकते हैं:

Definition pred2 n (q : n <> O) := 
    match n as n' return n = n' -> nat with 
    | S p => fun _ => p 
    | O => fun Heq => match q Heq with end 
    end (eq_refl n). 

स्पष्टीकरण:

• return के साथ एक प्रकार का एनोटेशन का परिचय पूरे match ... end अभिव्यक्ति का प्रकार;
• as एक परिवर्तनीय नाम प्रस्तुत करता है जिसका उपयोग इस प्रकार की एनोटेशन में किया जा सकता है और प्रत्येक शाखा में बाईं ओर से प्रतिस्थापित किया जाएगा। यहां,
  • पहली शाखा में, दाईं ओर की ओर n = S p -> nat टाइप किया गया है; दूसरी शाखा में
  • , दाईं ओर की ओर n = O -> nat टाइप किया गया है। इसलिए, q Heq में False टाइप किया गया है और मिलान किया जा सकता है। reference manual में

अधिक जानकारी, Extended pattern-matching पर अध्याय में।