कोक में सेट के लगातार फॉर्मूलेशन?

Question

मैं कोक में काफी नया हूं और अपने शोध के आधार पर एक ढांचा विकसित करने की कोशिश कर रहा हूं। मेरा काम काफी परिभाषा-भारी है और मुझे कोक को सेट का इलाज करने के तरीके के कारण एन्कोडिंग में परेशानी हो रही है।

वहाँ Type और Set हैं, जो वे 'प्रकार' कहते हैं, और मैं एक नया सेट को परिभाषित करने के लिए उपयोग कर सकते हैं:

Variable X: Type. 

और फिर वहाँ एक पुस्तकालय एन्कोडिंग (उप) के रूप में 'Ensembles' सेट है, जो Type से Prop पर फ़ंक्शंस हैं।

Variable Y: Ensemble X. 

Ensemble रों उचित गणितीय सेट की तरह अधिक लग रहा है: दूसरे शब्दों में, वे एक Type पर विधेय हैं। इसके अलावा, वे कई अन्य पुस्तकालयों द्वारा निर्मित किए जाते हैं। मैंने उन पर ध्यान केंद्रित करने की कोशिश की है: एक सार्वभौमिक सेट U: Set परिभाषित करना, और फिर U पर स्वयं को (उप) Ensemble एस तक सीमित करना। लेकिन नहीं। Ensemble अन्य चर के लिए प्रकार के रूप में इस्तेमाल नहीं किया जा सकता है और न ही नई सबसेट परिभाषित करने के लिए:

Variable y: Y.   (* Error *) 
Variable Z: Ensemble Y. (* Error *) 

अब, मैं जानता हूँ कि वहाँ कई तरीके है कि चारों ओर पाने के लिए कर रहे हैं। प्रश्न "Subset parameter" दो प्रदान करता है। दोनों प्रयोगों का उपयोग करें। पहली छड़ें Set एस। दूसरा अनिवार्य रूप से Ensemble एस (हालांकि नाम से नहीं) का उपयोग करता है। लेकिन दोनों को कुछ आसान करने के लिए काफी कुछ मशीनरी की आवश्यकता होती है।

प्रश्न: लगातार (और सुंदर ढंग से) हैंडलिंग सेट का अनुशंसित तरीका क्या है?

उदाहरण: यहाँ मैं क्या करना चाहते हैं उसका एक उदाहरण है: एक सेट डीडी मान लें। एक जोड़ी dm = परिभाषित करें (डी, <) जहां डीडीडी और < की एक निश्चित सबसेट है डी पर एक सख्त आंशिक आदेश है।

मुझे यकीन है कि जबरन या अन्य संरचनाओं के साथ पर्याप्त टिंचरिंग के साथ, मैं इसे पूरा कर सकता हूं; लेकिन विशेष रूप से पठनीय तरीके से नहीं; और ढांचे को आगे बढ़ाने के तरीके के बारे में अच्छी अंतर्ज्ञान के बिना। उदाहरण के लिए, निम्न प्रकार-जांच:

Record OrderedSet {DD: Set} : Type := { 
    D  : (Ensemble DD); 
    order : (relation {d | In _ D d}); 

    is_finite   : (Finite _ D); 
    is_strict_partial : (is_strict_partial_order order) 
}. 

लेकिन मैं इतना यकीन है कि यह मैं क्या चाहते हो नहीं हूँ, और यह निश्चित रूप से बहुत सुंदर नहीं दिखता है। ध्यान दें कि मैं Set और Ensemble के बीच एक मनमाने ढंग से रास्ते में पीछे और आगे जा रहा हूं।

वहां बहुत सारे पुस्तकालय हैं जो Ensemble एस का उपयोग करते हैं, इसलिए उनके इलाज के लिए एक अच्छा तरीका होना चाहिए, लेकिन उन पुस्तकालयों को बहुत अच्छी तरह से दस्तावेज नहीं लग रहा है (या ... बिल्कुल)।

अद्यतन: मामलों को और जटिल करने के लिए, MSets जैसे कई अन्य सेट कार्यान्वयन भी दिखाई देते हैं। यह Ensemble के साथ पूरी तरह से अलग और असंगत प्रतीत होता है। यह कुछ कारणों से Prop के बजाय bool का भी उपयोग करता है। FSets भी है, लेकिन यह एमएसएएस का पुराना संस्करण प्रतीत होता है।

Answer 1

जब मैं कोक का उपयोग करता हूं तो यह (शाब्दिक) वर्षों से रहा है, लेकिन मुझे मदद करने की कोशिश करें।

मैं गणितीय बोल लगता U: Set की तरह कह U तत्वों की एक ब्रह्मांड है और Ensemble U तो कि ब्रह्मांड से तत्वों का एक सेट का मतलब होगा है। तो सामान्य विचारों और परिभाषाओं के लिए आप लगभग निश्चित रूप से Set और Ensemble का उपयोग तत्वों के सबसेट के बारे में तर्क के बारे में एक संभावित तरीका है।

मैं सुझाव दूंगा कि आप मैथ्यूउ सोज़ौ द्वारा महान काम पर नज़र डालें, जिन्होंने type classes to Coq पेश किया, जो हास्केल के प्रकार वर्गों पर आधारित एक बहुत ही उपयोगी विशेषता है। विशेष रूप से मानक पुस्तकालय में आपको PartialOrder की कक्षा-आधारित परिभाषा मिल जाएगी जिसे आपने अपने प्रश्न में उल्लेख किया है।

एक और संदर्भ CoLoR library शब्द पुनर्लेखन को समाप्त करने के लिए आवश्यक विचारों को औपचारिक रूप देने के लिए होगा। ऑर्डर पर क्या है और क्या नहीं, यह generic purpose definitions का काफी बड़ा सेट है।