समानता पर उत्तराधिकारी की प्रतिस्थापन संपत्ति प्रदान करना

Question

मैं chapter 7 of "theorem proving in lean" से अपरिवर्तनीय प्रकारों को समझने की कोशिश कर रहा हूं।

inductive natural : Type 
| zero : natural 
| succ : natural -> natural 

lemma succ_over_equality (a b : natural) (H : a = b) : 
    (natural.succ a) = (natural.succ b) := sorry 

कुछ अटकलबाजी और काफी संपूर्ण खोज रहा संभावनाओं के एक जोड़े के साथ संकलक को संतुष्ट करने में सक्षम था के बाद:

मैं अपने आप को प्राकृतिक संख्याओं का है कि उत्तराधिकारी साबित करने का एक कार्य सेट समानता पर एक प्रतिस्थापन संपत्ति है:

lemma succ_over_equality (a b : natural) (H : a = b) : 
    (natural.succ a) = (natural.succ b) := 
    eq.rec_on H (eq.refl (natural.succ a)) 
    --eq.rec_on H rfl 
    --eq.subst H rfl 
    --eq.subst H (eq.refl (natural.succ a)) 
    --congr_arg (λ (n : natural), (natural.succ n)) H 

मुझे समझ में नहीं आता कि मैंने वास्तव में क्या सबूत दिए हैं।

1. eq (अनिवार्य) प्रकार की पूर्ण परिभाषा क्या है? वीएससीओडी में मैं eq के प्रकार हस्ताक्षर eq Π {α : Type} α → α → Prop के रूप में देख सकता हूं, लेकिन मैं natural से व्यक्तिगत (अपरिवर्तनीय) रचनाकार (zero और succ के अनुरूप नहीं देख सकता)। स्रोत कोड doesn't look quite right में सबसे अच्छा मुझे मिल सकता है।
2. eq.subst का सबूत (natural.succ a) = (natural.succ b) का प्रमाण प्रदान करने के लिए खुश क्यों है?
3. higher order unification क्या है और यह इस विशेष उदाहरण पर कैसे लागू होता है?
4. त्रुटि जब मैं #check (eq.rec_on H (eq.refl (natural.succ a))) टाइप मैं मिलता है, जो है [Lean] invalid 'eq.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort l} {a_1 : α}, a = a_1 → C a → C a_1

Answer 1

1. eq inductive eq {α : Sort u} (a : α) : α → Prop | refl : eq a विचार होने की https://github.com/leanprover/lean/blob/master/library/init/core.lean#L120 में परिभाषित किया गया है का अर्थ क्या है कि किसी भी अवधि में ही समान हो जाता है, और दो शर्तों के बराबर होने का एकमात्र तरीका उनके लिए एक ही शब्द होना है। यह आईटीटी जादू का थोड़ा सा महसूस कर सकता है। सौंदर्य इस परिभाषा के लिए स्वचालित रूप से जेनरेट किए गए रिकर्सर से आता है: eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1}, C a → Π {a_1 : α}, a = a_1 → C a_1 यह समानता के लिए प्रतिस्थापन सिद्धांत है। "अगर सी में ए, और ए = ए_1 है, तो सी ए_1 का रखता है।" (वहाँ एक ऐसी ही व्याख्या है कि अगर सी प्रकार-मान के बजाय प्रोप-मान है।)

2. eq.substsucc a = succ a प्रमाण के साथ a = b का एक सबूत ले जा रहा है। ध्यान दें कि eq.subst मूल रूप से ऊपर eq.rec का एक सुधार है। मान लीजिए कि संपत्ति C, एक चर x पर parametrized, succ a = succ x है। Ca के लिए रिफ्लेक्सिविटी द्वारा रखता है, और a = b के बाद, हमारे पास Cb है।

3. जब आप eq.subst H rfl लिखते हैं, तो लीन को यह पता लगाने की आवश्यकता होती है कि संपत्ति (या "उद्देश्य") C क्या माना जाता है। यह उच्च आदेश एकीकरण का एक उदाहरण है: अज्ञात चर को लैम्ब्डा अभिव्यक्ति के साथ एकजुट करने की आवश्यकता है। https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf में सेक्शन 6.10 में इसकी चर्चा है, और कुछ सामान्य जानकारी https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification पर है।

4. आप succ a = succ a में a = b स्थानापन्न करने झुक पूछ रहे हैं, यह कह रही है आप को साबित करने की कोशिश कर रहे हैं के बिना। आप succ b = succ b, या succ b = succ a, या यहां तक ​​कि succ a = succ a (कहीं भी प्रतिस्थापित करके) साबित करने का प्रयास कर सकते हैं।लीन C के उद्देश्य को तब तक अनुमानित नहीं कर सकता जब तक कि यह जानकारी न हो।

सामान्य में, प्रतिस्थापन कर "मैन्युअल" (eq.rec, subst, आदि के साथ) मुश्किल है के बाद से उच्च आदेश एकीकरण नकचढ़ा और महंगा है। आप अक्सर मिल जाएगा कि यह rw (पुनर्लेखन) की तरह रणनीति का उपयोग करने के लिए बेहतर है: lemma succ_over_equality (a b : natural) (H : a = b) : (natural.succ a) = (natural.succ b) := by rw H

आप चतुर होना चाहते हैं, तो आप के झुक समीकरण संकलक का उपयोग कर सकते हैं, और तथ्य यह है कि "केवल" a=b का सबूत rfl है: lemma succ_over_equality : Π (a b : natural), a = b → (natural.succ a) = (natural.succ b) | ._ _ rfl := rfl