6
के उप-संपीड़न पर पुनर्लेखन का उपयोग कैसे करें, क्या यह किसी भी तरह से वर्तमान लक्ष्य के उप-संपीड़न के लिए लेम्मा या परिकल्पना लागू करना संभव है? उदाहरण के लिए, मैं इस तथ्य को लागू करना चाहता हूं कि इस उदाहरण में 3 और 4 को स्वैप करने के लिए प्लस कम्यूटेटिव है।वर्तमान लक्ष्य
Require Import Coq.Arith.Plus.
Inductive foobar : nat -> Prop :=
| foob : forall n:nat, foobar n.
Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)
देता है:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".
मैं कैसे इस लक्ष्य में जहां बिल्कुल Coq बता plus_comm लागू करने के लिए कर सकते हैं?
यह काम करता है जब मैं निम्नलिखित करता हूं, जो मैं वास्तव में पहले स्थान पर साबित करना चाहता था। लक्ष्य foobar (3 + 4) = foobar (4 + 3)। सबूत। plus_comm पुनः लिखें। रिफ्लेक्सिविटी। प्रश्नोत्तरी। मुझे लगता है कि पुनः लिखना मूल्यों पर काम नहीं करता है, केवल प्रकारों पर। –
'पुनर्लेखन' दोनों पर काम करता है (वास्तव में प्रकार Coq ;-) में हैं। यहां मुख्य मुद्दा यह है कि 'foob (3 + 4)' प्रकार 'foobar (3 + 4) 'और' foob (4 + 3) 'प्रकार' foobar (4 + 3)' है। Coq जांच सकता है कि दोनों बराबर हैं (इसलिए समानता अच्छी तरह से टाइप की गई है), लेकिन 'पुनः लिखना' एक मध्यवर्ती रूप का उपयोग करता है जहां यह मामला नहीं है, इसलिए क्रिप्टिक त्रुटि संदेश जिसे आप 'पुनः लिखना' (plus_comm 3 4) 'के साथ प्राप्त करते हैं। – Virgile
आम तौर पर, आप शब्द के अंदर कहीं भी स्थानीय कार्यों के लिए 'pattern' (http://coq.inria.fr/refman/Reference-Manual011.html#pattern) का उपयोग करने में सक्षम होना चाहिए। हालांकि, यह वही कारण @ Virgile के लिए विफल रहता है। यदि यह संभव है, तो आप अस्थायी रूप से 'अधिक पूर्ण' समानता प्रकार पर भी जा सकते हैं (उदा। 'जेएमईक्यू'), वहां सामान करें और फिर वापस जाएं। (मुझे इसे 'जटिल संख्या' के रूप में सोचना पसंद है-समानता का एनालॉग।) – nobody