Coq

Question

में मौजूद अस्तित्व से अंतर्निहित जानकारी पुनर्प्राप्त करना मान लीजिए कि हमारे पास ऐसा कुछ है:

मान लीजिए एक्स एक असली संख्या है। दिखाएं कि यदि कोई वास्तविक संख्या वाई है (वाई + 1)/(वाई - 2) = एक्स, तो एक्स <> 1 "

यदि कोई इसे स्पष्ट तरीके से तैयार करता है: forall x : R, (exists y, ((y + 1) */(y - 2)) = x) -> x <> 1, कोई एक में चलाता है एक मुद्दा बहुत जल्द ही।

हम y ऐसी है कि ((y + 1) */(y - 2)) = x) के अस्तित्व की एक धारणा है। मुझे लगता है गलत यह भी मतलब होना चाहिए कि कि y <> 2? वहाँ Coq में यह जानकारी ठीक करने के लिए एक रास्ता है हूँ?

निश्चित रूप से , यदि y मौजूद है, तो यह 2 नहीं है। कोई इस जानकारी को कोक में कैसे पुनर्प्राप्त करता है - क्या मुझे इसे स्पष्ट रूप से मानने की आवश्यकता है (यानी, कोई डब्ल्यू नहीं है किसी भी तरह अस्तित्व में तत्काल त्वरण से इसे पुनर्प्राप्त करने के लिए?)।

बेशक, destruct H as [y] हमें ((y + 1) */(y - 2)) = x)y : R के लिए देता है, लेकिन अब हम y <> 2 नहीं जानते हैं।

Answer 1

क्या मुझे लगता है कि यह भी मानना ​​चाहिए कि y <> 2?

हां। कोक में, विभाजन कुल, अनियंत्रित कार्य है: आप इसे शून्य विभाजक सहित संख्याओं की किसी भी जोड़ी पर लागू कर सकते हैं। यदि आप y <> 2 मानना ​​चाहते हैं, तो आपको इसे अपने लेम्मा को स्पष्ट धारणा के रूप में जोड़ना होगा।

आपको यह डरावना मिल सकता है: हमें शून्य से कुछ विभाजित करने की अनुमति कैसे दी जा सकती है? जवाब यह है कि इससे कोई फर्क नहीं पड़ता, जब तक आप 0 * (x/0) = x पर बहस करने का प्रयास नहीं करते हैं। This question इस मुद्दे पर अधिक विस्तार से चर्चा करता है।

Answer 2

Coq में वास्तविक संख्या, परिभाषित axiomatically जाता है, यानी वे सिर्फ प्रकार के साथ जुड़े नाम हैं, वहाँ कोई परिभाषाएँ नाम से जुड़ी हैं। वहाँ reals (Rplus, Rmult, आदि) जो निष्पादित नहीं मिलता पर बुनियादी संख्या (R0, R1) और संचालन कर रहे हैं, अर्थात संचालन कार्यों नहीं हैं। एक अर्थ में, केवल डेटा कन्स्ट्रक्टर की तरह ही उन परिचालनों से उन्हें बनाकर वास्तविक संख्याएं बनाते हैं (लेकिन हम वास्तविकताओं पर पैटर्न-मिलान नहीं कर सकते हैं)।

उपर्युक्त अर्थ यह है कि, उदा। 1/0 एक मान्य वास्तविक संख्या है। वास्तविक संख्याओं के लिए यह केवल सिद्धांतों का परिसर है, इस तरह के अभिव्यक्तियों को शामिल करने में कुछ सरलीकरणों को प्रतिबंधित करता है: हम 1/0 * 0 से 1 पर अभिव्यक्तियों को फिर से लिख नहीं सकते हैं (हालांकि, हम इसे 0 पर फिर से लिख सकते हैं)।

From Coq Require Import Reals. 
Open Scope R. 

Goal ~ (forall x y : R, (y + 1)/(y - 2) = x -> y <> 2). 
    unfold "_ - _"; intros contra; specialize (contra ((2+1)/0) 2). 
    rewrite Rplus_opp_r in contra. 
    intuition. 
Qed. 

:

यहाँ हम कैसे दिखा सकते हैं कि हम जैसे

(y + 1)/(y - 2) = x 

एक अभिव्यक्ति से y <> 2 प्राप्त नहीं सकता क्योंकि हम "अजीब" वास्तविक संख्या का उपयोग करने के लिए अनुमति दी जाती है