में "वर्बोज़" ऑटो मैं कोक और पुस्तक जिसे मैं सीख रहा हूं, सीख रहा हूं, (CPDT) सबूत में auto का भारी उपयोग करता है।कोक
चूंकि मैं सीख रहा हूं, मुझे लगता है कि यह देखने के लिए मेरे लिए उपयोगी हो सकता है कि auto हुड के नीचे क्या कर रहा है (बेहतर जादू कम से कम)। क्या सबूत की गणना करने के लिए इसका उपयोग करने वाली रणनीति या तकनीकों का प्रदर्शन करने के लिए इसे मजबूर करने का कोई तरीका है?
यदि नहीं, तो क्या कोई जगह है जो विवरण auto करता है?
हुड के नीचे क्या हो रहा है पर एक नज़र पाने के कई तरीके हैं।
टीएलडीआर: अपनी रणनीति से पहले info रखो, या रणनीति को कॉल करने से पहले और बाद में Show Proof. का उपयोग करें और मतभेदों को स्पॉट करें।
देखने के लिए क्या एक विशेष रणनीति के मंगलाचरण कर रहा है, तो आप info साथ है उपसर्ग कर सकते हैं, तो के रूप में विशेष रूप से सबूत कदम यह उठाया है दिखाने के लिए।
(यदि आप की जरूरत है यह Coq 8.4 से तोडा जा सकता हो सकता है, मुझे लगता है कि वे कुछ रणनीति के info_ संस्करणों प्रदान करते हैं त्रुटि संदेश पढ़ा।)
यह एक शुरुआत के स्तर पर आप क्या चाहते हैं शायद है यह पहले से ही काफी terse हो सकता है।
जो वर्तमान में एक सबूत के भीतर चल रहा है देखने के लिए एक और तरीका है आदेश Show Proof. उपयोग करने के लिए है। यह आपको वर्तमान में निर्मित छेद के साथ निर्मित शब्द दिखाएगा, और आपको दिखाएगा कि आपके प्रत्येक वर्तमान लक्ष्य को कौन सा छेद भरना है।
यह शायद और अधिक उन्नत है, खासकर यदि आप induction या inversion के रूप में रणनीति इस तरह के प्रयोग करते हैं, अवधि काफी शामिल होने जा रहा है बनाया जा रहा है, और प्रेरण योजनाओं या निर्भर पैटर्न मिलान की अंतर्निहित प्रकृति को समझने की आवश्यकता होगी (जो सीपीडीटी आपको जल्द ही सिखाएगा)।
एक बार जब आप Qed. (या Defined.) के साथ एक प्रमाण समाप्त कर दिया है, तो आप भी शब्द है कि Print term. का उपयोग कर जहां term प्रमेय/अवधि का नाम है द्वारा बनाया गया था को देखने के लिए पूछ सकते हैं।
यह अक्सर एक बड़ा और बदसूरत शब्द होगा, और इसमें शामिल प्रशिक्षण के लिए इन्हें पढ़ने में सक्षम होने के लिए कुछ प्रशिक्षण की आवश्यकता है। विशेष रूप से, यदि शब्द शक्तिशाली रणनीति के उपयोग के माध्यम से बनाया गया है (जैसे omega, crush, आदि), तो यह संभवतः अपठनीय होने जा रहा है। आप मूल रूप से केवल उस शब्द के किसी विशेष स्थान पर स्कैन करने के लिए इसका उपयोग करेंगे, यदि आप रुचि रखते हैं। यदि यह 10 से अधिक लाइनों से अधिक है, तो इसे ऐसे कच्चे प्रारूप में पढ़ने को परेशान न करें! :)
पिछले के सभी के साथ, आप पहले से Set Printing All. उपयोग कर सकते हैं, ताकि Coq सब कुछ सामने आया, स्पष्ट संस्करणों प्रिंट करता है। यह अतिरिक्त वर्बोज़ है लेकिन जब आप सोचते हैं कि अंतर्निहित मानकों के मूल्य क्या हैं, तो यह मदद कर सकता है।
ये सभी हैं जो मैं अपने सिर के शीर्ष पर सोच सकता हूं, और भी हो सकता है।
क्या एक रणनीति करता है के रूप में, हमेशा की तरह सबसे अच्छा जवाब दस्तावेज में पाया जाता है:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155
असल में, auto की कोशिश करता सभी दिए गए संकेतों (डेटाबेस आप उपयोग के आधार पर उपयोग करने के लिए), और अपने लक्ष्य को कुछ गहराई तक जोड़कर हल करने के लिए (जिसे आप निर्दिष्ट कर सकते हैं)। डिफ़ॉल्ट रूप से, डेटाबेस core है और गहराई 5 है।
कि बारे में अधिक जानकारी यहां पाया जा सकता:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases
'info_auto' केवल" सफलता के मार्ग "को दर्शाता है। यह देखने के लिए कि वास्तव में 'ऑटो' क्या प्रयास करता है, वह 'डीबग ऑटो' का उपयोग कर सकता है: यह सभी विफलताओं (!) और सफलताओं को दिखाता है। –