प्रेरण का उपयोग करते समय जानकारी रखते हुए?

Question

मैं एक (छोटे) प्रोग्रामिंग भाषा (ब्रूनो डी Fraine, एरिक अर्नस्ट, मारियो Südholt द्वारा Featherweight जावा के एक कार्यान्वयन विस्तार) के एक मॉडल को लागू करने के Coq सबूत सहायक का उपयोग कर रहा हूँ। एक चीज जो induction रणनीति का उपयोग करते समय आती रहती है, यह है कि प्रकार के रचनाकारों में लिपटे जानकारी को कैसे संरक्षित किया जाए।

मैं के रूप में

Inductive sub_type : typ -> typ -> Prop := 
| st_refl : forall t, sub_type t t 
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3 
| st_extends : forall C D, 
    extends C D -> 
    sub_type (c_typ C) (c_typ D). 

Hint Constructors sub_type. 

जहां extends वर्ग विस्तार प्रणाली जावा के रूप में देखा है एक उप टाइपिंग कार्यान्वित प्रोप है, और typ उपलब्ध प्रकार के दो अलग अलग प्रकार का प्रतिनिधित्व करता है,

Inductive typ : Set := 
| c_typ : cname -> typ 
| r_typ : rname -> typ. 

एक जहाँ मैं प्रकार की जानकारी चाहते हैं के उदाहरण को संरक्षित किया जा रहा है जब

की तरह एक परिकल्पना पर induction रणनीति का उपयोग करते हुए

जैसे

u : cname 
v : cname 
fsv : flds 
H : sub_type (c_typ u) (c_typ v) 
H0 : fields v fsv 
============================ 
exists fs : flds, fields u (fsv ++ fs) 

induction H. छोड देता है u और v बारे में सभी जानकारी का उपयोग करने में। st_refl मामले

u : cname 
v : cname 
fsv : flds 
t : typ 
H0 : fields v fsv 
============================ 
exists fs : flds, fields u (fsv ++ fs) 

हो जाता है आप जानकारी है कि u और vH में typ कंस्ट्रक्टर्स से जुड़े हुए हैं, और इस तरह t करने के लिए, खो दिया है देख सकते हैं। इससे भी बदतर यह है कि इस कोक के कारण यह देखने में असमर्थ है कि u और v वास्तव में इस मामले में समान होना चाहिए।

H Coq पर inversion रणनीति का उपयोग करते समय देखकर कि u और v ही कर रहे हैं में सफल होता है। यही कारण है कि रणनीति नहीं लागू यहाँ हालांकि, के रूप में मैं प्रेरण परिकल्पना कि inductionst_trans और st_extends मामलों साबित करने के लिए उत्पन्न करता है की जरूरत है।

वहाँ एक रणनीति है कि दोनों प्रेरण परिकल्पना पैदा करते हैं और क्या कंस्ट्रक्टर्स में लपेटा जाता है के बारे में जानकारी को नष्ट किए बिना समानताओं प्राप्त करने के लिए inversion और induction का सबसे अच्छा जोड़ती है? वैकल्पिक रूप से, क्या मुझे आवश्यक जानकारी मैन्युअल रूप से प्राप्त करने का कोई तरीका है? info inversion H और info induction H दोनों बताते हैं कि परिवर्तनों का एक बहुत (विशेष रूप से inversion के साथ) स्वचालित रूप से लागू कर रहे हैं। इन्होंने change रणनीति के साथ let ... in निर्माण के साथ प्रयोग करने का नेतृत्व किया है, लेकिन बिना किसी प्रगति के।

Answer 1

यह एक सामान्य समस्या है जब आपको एक निर्भर प्रकार (sub_type (c_typ u) (c_typ v)) के साथ एक परिकल्पना को शामिल करने की आवश्यकता होती है जिसका पैरामीटर एक विशेष संरचना (c_typ u) है। एक सामान्य चाल है, जो पर्यावरण में समानता को बनाए रखने, एक चर के लिए संरचित पैरामीटर को चुनिंदा रूप से फिर से लिखना है।

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1. 
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2. 
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *). 

Coq 8.2, के बाद से इस आम सेट-ज़ोर-clearbody पैटर्न में निर्मित रणनीति remember term as ident in *goal_occurences* द्वारा किया जाता है।

यहां एक मूर्खतापूर्ण लेम्मा इस रणनीति का उपयोग कर साबित कर दिया है।

Lemma subtype_r_left_equal : 
    forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2. 
Proof. 
    intros. 
    remember (r_typ r1) as t1 in H. 
    induction H. 
    congruence. 
    solve [firstorder]. 
    discriminate. 
Qed. 

---

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

---

अपने Problem.v के साथ, यहाँ तक परावर्तकता मामले का एक सबूत है। पारगमन के लिए, मुझे संदेह है कि आपकी प्रेरण परिकल्पना पर्याप्त मजबूत नहीं है। यह समस्या को सरल बनाने के तरीके का एक उपज हो सकता है, हालांकि पारगमन को अक्सर आश्चर्यजनक रूप से शामिल प्रेरण अनुमान या लेमास की आवश्यकता होती है।

Fact sub_type_fields: forall u v fsv, 
    sub_type (c_typ u) (c_typ v) -> fields v fsv -> 
    exists fs, fields u (fsv ++ fs). 
Proof. 
    intros. 
    remember (c_typ u) as t1 in H. 
    remember (c_typ v) as t2 in H. 
    induction H. 
    (* case st_refl *) 
    assert (v = u). congruence. subst v t. 
    exists nil. rewrite <- app_nil_end. assumption. 
    (* case st_trans *) 
    subst t1 t3. 
    (* case st_extends *) 
Admitted. 

Answer 2

मैं इसी तरह की समस्या में भाग गया और कोक 8.3 की "आश्रित प्रेरण" रणनीति ने व्यवसाय की देखभाल की।

Answer 3

मुझे यकीन था कि सीपीडीटी के पास इस मुद्दे पर कुछ टिप्पणी थी, लेकिन यह पूरी तरह स्पष्ट नहीं है कि यह कहां है।

1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html धारा "अंतर्निहित समानता के साथ विधेय" शो शायद बहुत सरल मामले में जहां Coq "जानकारी खो देता है" यह भी बताता है कि क्यों इस जानकारी है: यहाँ कुछ लिंक कर रहे हैं (एक विनाश पर, बल्कि एक प्रेरण से।) खो दिया: जब आप एक प्रकार एक तर्क जो एक नि: शुल्क चर नहीं है करने के लिए लागू संहार, उन प्रकार के पहले स्वतंत्र चर के साथ शो "से बचना अभिगृहीत के लिए तरीके" बदल दिया जाता है (जिसके कारण Coq जानकारी खो देता है।)

2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html धारा गिल्स द्वारा वर्णित "समानता चाल" सहित ,xixi के से बचने के लिए कुछ चालें। "गैर चर तर्क पर प्रेरण समर्थन परिवारों टाइप करने के लिए के लिए एक आम समानता के आधार पर चाल का उपयोग कर"

मुझे लगता है कि इस घटना को बारीकी से निर्भर पैटर्न मिलान से संबंधित है के लिए खोजें।