कोक में वास्तविक संख्याओं के लिए "कम से कम" परिभाषित कैसे किया गया है?

Question

मैं सोच रहा हूं कि असली संख्याओं के लिए "कम से कम" रिश्ते को परिभाषित किया गया है।

मैं समझता हूँ कि प्राकृतिक संख्या (nat) के लिए, < (1+) एक और नंबर के उत्तराधिकारी S जा रहा है एक संख्या के मामले में रिकर्सिवली परिभाषित किया जा सकता। मैंने सुना है कि वास्तविक संख्याओं के बारे में कई चीजें कोक में स्वस्थ हैं और गणना नहीं करते हैं।

लेकिन मैं सोच रहा हूं कि कोक में वास्तविक संख्याओं के लिए सिद्धांतों का न्यूनतम सेट है या नहीं, जिसके आधार पर अन्य गुण/संबंध प्राप्त किए जा सकते हैं। (जैसे Coq.Reals.RIneq कि Rplus_0_r : forall r, r + 0 = r. एक स्वयंसिद्ध है, दूसरों के बीच यह है)

विशेष रूप से, मैं में क्या इस तरह के < या <= के रूप में रिश्तों समानता संबंध के शीर्ष पर परिभाषित किया जा सकता दिलचस्पी है। उदाहरण के लिए, मैं पारंपरिक गणित में कल्पना कर सकते हैं कि, दो नंबर r1 r2 दिया:

r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2. 

लेकिन Coq की रचनात्मक तर्क में इस धारण करता है? और क्या मैं कम से कम असमानताओं के बारे में कुछ तर्क करने के लिए इसका उपयोग कर सकता हूं (हर समय सिद्धांतों को फिर से लिखने के बजाय)?

Answer 1

Coq.Reals.RIneq में यह है कि Rplus_0_r: forall r, r + 0 = r। Rplus_0_r एक स्वयंसिद्ध नहीं है, लेकिन Rplus_0_l है: एक स्वयंसिद्ध, दूसरों के बीच

nitpick है। आप मॉड्यूल Coq.Reals.Raxioms में Coq.Reals.Rdefinitions में उपयोग किए गए पैरामीटर की एक सूची में उनकी एक सूची प्राप्त कर सकते हैं।

जैसा कि आप देख सकते हैं कि "से अधिक (या बराबर)" और "उससे कम या बराबर" सभी "कम से कम" के संदर्भ में परिभाषित किए गए हैं जो आपके द्वारा सुझाए गए प्रस्ताव का उपयोग करके पेश किए गए हैं।

ऐसा लगता है कि Rlt वास्तव में आपके द्वारा सुझाए गए फैशन में परिभाषित किया जा सकता है: दो प्रस्ताव नीचे दिखाए गए अनुसार बराबर हैं।

Require Import Reals. 
Require Import Psatz. 
Open Scope R_scope. 

Goal forall (r1 r2 : R), r1 < r2 <-> exists s, s > 0 /\ r1 + s = r2. 
Proof. 
intros r1 r2; split. 
- intros H; exists (r2 - r1); split; [lra | ring]. 
- intros [s [s_pos eq]]; lra. 
Qed. 

हालांकि आप अभी भी क्या यह "कड़ाई से सकारात्मक" s > 0 बिट के लिए समझ बनाने के लिए होने का क्या मतलब है और यह बिल्कुल स्पष्ट नहीं है कि आप अंत में कम सूक्तियों होगा निर्धारित करना होगा (जैसे धारणा कड़ाई से सकारात्मक होने के अलावा, गुणा, आदि के तहत बंद किया जाना चाहिए)।

Answer 2

वास्तव में, Coq.Real लाइब्रेरी इस अर्थ में थोड़ा कमजोर है कि इसे पूरी तरह से सिद्धांतों के रूप में निर्दिष्ट किया गया है, और अतीत में कुछ (संक्षिप्त) बिंदुओं पर यह असंगत था।

तो ली की परिभाषा इस अर्थ में थोड़ी "विज्ञापन" है कि सिस्टम के दृष्टिकोण से यह केवल स्थिर और कुछ सिद्धांतों के रूप में शून्य कम्प्यूटेशनल अर्थ रखता है। आप एक्सीम "x < x" को अच्छी तरह से जोड़ सकते हैं और कोक इसका पता लगाने के लिए कुछ भी नहीं कर सकता है।

यह Coq के लिए reals के कुछ विकल्प निर्माण की ओर इशारा करते के लायक है: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

केवल

यह:

मेरा पसंदीदा शास्त्रीय निर्माण जॉर्जिस गोंथियर और बी वर्नर द्वारा चार रंग प्रमेय में किया जाता है बहिष्कृत मध्य वसंत (मुख्य रूप से वास्तविक संख्याओं की तुलना करने के लिए) का उपयोग करता है, इसलिए इसकी स्थिरता में विश्वास बहुत अधिक है।

वास्तविकता का सबसे अच्छा ज्ञात एक्सीम-मुक्त विशेषता सी-कॉर्न प्रोजेक्ट है, http://corn.cs.ru.nl/ लेकिन हम जानते हैं कि रचनात्मक विश्लेषण सामान्य से काफी अलग है।