इडिस

Question

में रीराइट रणनीति के साथ संघर्ष करना मैं टेरी ताओ की वास्तविक विश्लेषण पाठ्यपुस्तक के माध्यम से जा रहा हूं, जो प्राकृतिक संख्याओं से मौलिक गणित का निर्माण करता है। जितना संभव हो उतना सबूत औपचारिक रूप से, मैं खुद को इडिस और आश्रित दोनों प्रकारों से परिचित कराने की उम्मीद करता हूं।

data GE: Nat -> Nat -> Type where 
    Ge : (n: Nat) -> (m: Nat) -> GE n (n + m) 

प्रस्ताव का प्रतिनिधित्व करने के लिए कि एक प्राकृतिक संख्या से अधिक है या किसी अन्य के बराबर है:

मैं निम्नलिखित डेटाप्रकार को परिभाषित किया है।

मैं वर्तमान में इस संबंध का रिफ्लेक्सिविटी साबित करने के लिए है, यानी हस्ताक्षर

geRefl : GE n n 

मेरा पहला प्रयास बस geRefl {n} = Ge n Z कोशिश करने के लिए था के साथ सबूत के निर्माण के लिए संघर्ष कर रही है, लेकिन इस टाइप Ge n (add n Z) है।

geRefl : GE n n                 
geRefl {n} = x                 
    where x : GE n (n + Z)              
      x = rewrite plusZeroRightNeutral n in Ge n Z 

लेकिन इस typecheck नहीं करता है: यह प्राप्त करने के लिए वांछित हस्ताक्षर के साथ एकजुट करने के लिए, हम स्पष्ट रूप से, फिर से लिखने के कुछ प्रकार के प्रदर्शन करने के लिए शायद लेम्मा

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left 

मेरे सबसे अच्छे प्रयास शामिल है निम्नलिखित है ।

क्या आप कृपया इस प्रमेय का सही सबूत दे सकते हैं, और इसके पीछे तर्क बता सकते हैं?

Answer 1

पहली समस्या सतही है: आप गलत जगह पर पुनर्लेखन लागू करने की कोशिश कर रहे हैं। आप x : GE n (n + Z) है, तो आप आप geRefl : GE n n की परिभाषा के रूप में उपयोग करना चाहते हैं तो अपने प्रकार पुनर्लेखन करना होगा, ताकि आप

geRefl : GE n n 
geRefl {n} = rewrite plusZeroRightNeutral n in x 

लिखने के लिए होगा लेकिन है कि अभी भी काम नहीं करेगा। वास्तविक समस्या यह है कि आप केवल GE n n के एक हिस्से को फिर से लिखना चाहते हैं: यदि आप इसे n + 0 = n का उपयोग करके फिर से लिखते हैं, तो आपको GE (n + 0) (n + 0) मिल जाएगा, जिसे आप अभी भी Ge n 0 : GE n (n + 0) का उपयोग करके साबित नहीं कर सकते हैं।

आपको यह करने की ज़रूरत है कि a = b, तो x : GE n ax' : GE n b में बदल दिया जा सकता है।

replace : (x = y) -> P x -> P y 

इस का उपयोग करना, P = GE n की स्थापना, और Ge n 0 : GE n (n + 0) का उपयोग करके, हम लिख सकते geRefl

geRefl {n} = replace {P = GE n} (plusZeroRightNeutral n) (Ge n 0) 

के रूप में (ध्यान दें कि इदरिस पूरी तरह से सक्षम है: यह वास्तव में क्या मानक पुस्तकालय में replace समारोह प्रदान करता है अंतर्निहित पैरामीटर P का अनुमान लगाने के लिए, इसलिए यह इसके बिना काम करता है, लेकिन मुझे लगता है कि इस मामले में यह स्पष्ट हो जाता है कि क्या हो रहा है)