ssreflect

Question

में कैनोलिक संरचनाएं मैं ssreflect में कैननिकल संरचनाओं से निपटने की कोशिश कर रहा हूं। कोड के 2 टुकड़े हैं जिन्हें मैंने here से लिया था।

मैं बूल और विकल्प प्रकार के लिए टुकड़े लाऊंगा।

Section BoolFinType. 

    Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed. 
    Definition bool_finMixin := Eval hnf in FinMixin bool_enumP. 
    Canonical bool_finType := Eval hnf in FinType bool bool_finMixin. 
    Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed. 

End BoolFinType. 

Section OptionFinType. 

    Variable T : finType. 
    Notation some := (@Some _) (only parsing). 

    Local Notation enumF T := (Finite.enum T). 

    Definition option_enum := None :: map some (enumF T). 

    Lemma option_enumP : Finite.axiom option_enum. 
    Proof. by case => [x|]; rewrite /= count_map (count_pred0, enumP). Qed. 

    Definition option_finMixin := Eval hnf in FinMixin option_enumP. 
    Canonical option_finType := Eval hnf in FinType (option T) option_finMixin. 

    Lemma card_option : #|{: option T}| = #|T|.+1. 
    Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed. 

End OptionFinType. 

अब, मैं finType से एक समारोह च प्रोप करने के लिए है लगता है

Variable T: finType. 
Variable f: finType -> Prop. 

Goal f T. (* Ok *) 
Goal f bool. (* Not ok *) 
Goal f (option T). (* Not ok *) 

पिछले दो मामलों मैं निम्नलिखित त्रुटि मिलती है:।

The term "bool/option T" has type "Set/Type" while it is expected to have type "finType".

मैं गलत क्या कर रहा हूँ ?

Answer 1

कैननिकल संरचनाओं के लिए उदाहरण खोज इन मामलों में थोड़ा सा अंतर्ज्ञानी है। मान लीजिए आप निम्नलिखित बातें है:

• एक संरचना प्रकार S, और एक प्रकार T;
• proj : S -> TS;
• एक तत्व x : T; और
• एक तत्व st : S जिसे कैननिकल के रूप में घोषित किया गया है, जैसे proj st को x के रूप में परिभाषित किया गया है।

अपने उदाहरण में, हम होगा:

• S = finType
• T = Type
• proj = Finite.sort
• x = bool
• st = bool_finType।

विहित संरचना खोज निम्नलिखित मामले में केवल शुरू हो रहा है: जब प्रकार-चेकिंग एल्गोरिथ्म एक मूल्य के वैध समीकरण proj _ = x में छेद को भरने के लिए खोजने की कोशिश कर रहा है। फिर, यह छेद भरने के लिए st : S का उपयोग करेगा। आपके उदाहरण में, आपको एल्गोरिदम को यह समझने की उम्मीद है कि bool को finType के रूप में उपयोग किया जा सकता है, इसे bool_finType में परिवर्तित करके, जो ऊपर वर्णित नहीं है।

कोक अनुमान लगाने के लिए जो आप चाहते हैं, आपको उस फ़ॉर्म की एकीकरण समस्या का उपयोग करने की आवश्यकता है। उदाहरण के लिए,

Variable P : finType -> Prop. 
Check ((fun (T : finType) (x : T) => P T) _ true). 

यहां क्या हो रहा है? याद रखें कि Finite.sort को finType से Type पर एक दबाव के रूप में घोषित किया गया है, इसलिए x : T वास्तव में x : Finite.sort T का अर्थ है। जब आप fun अभिव्यक्ति को true : bool पर अभिव्यक्त करते हैं, तो कोक को Finite.sort _ = bool के लिए समाधान ढूंढना होगा। इसके बाद bool_finType पाता है, क्योंकि इसे कैननिकल घोषित किया गया था। इसलिए bool का तत्व खोज को ट्रिगर करता है, लेकिन bool स्वयं नहीं है।

रूप ejgallego ने कहा, इस पैटर्न इतना आम है कि ssreflect विशेष [finType of ...] वाक्य रचना प्रदान करता है। लेकिन यह अभी भी उपयोगी हो सकता है कि हुड के नीचे क्या हो रहा है।