मैं झुक लगता है स्वचालित रूप से recursors even.rec और odd.recType, नहीं Prop के साथ काम करने को बनाने का प्रयास कर रहा है। लेकिन यह काम नहीं करता है क्योंकि लीन तार्किक दुनिया (Prop) और कम्प्यूटेशनल दुनिया (Type) को अलग करता है। दूसरे शब्दों में, हम केवल लॉजिकल टर्म बनाने के लिए लॉजिकल टर्म (सबूत) को नष्ट कर सकते हैं। ध्यान दें, अगर आपका उदाहरण even और odd प्रकार ℕ → Type बनाते हैं तो आपका उदाहरण काम करेगा।
कोक सबूत सहायक, जो एक संबंधित प्रणाली है, इस स्थिति को दो (बल्कि कमजोर और अव्यवहारिक) प्रेरण सिद्धांतों को बनाकर स्वचालित रूप से संभालता है, लेकिन यह सामान्य रिकर्सर्स को निश्चित रूप से उत्पन्न नहीं करता है।
इस Lean wiki article में वर्णित एक कार्यवाही है। इसमें बहुत सारे बॉयलरप्लेट लिखना शामिल है। मुझे एक उदाहरण दें कि इस मामले के लिए यह कैसे किया जा सकता है।
सबसे पहले, हम पारस्परिक अपरिवर्तनीय प्रकारों को एक अपरिवर्तनीय परिवार में संकलित करते हैं।
inductive even_odd: bool → ℕ → Prop
| ze: even_odd tt 0
| ne: ∀ n, even_odd ff n → even_odd tt (n + 1)
| zo: even_odd ff 1
| no: ∀ n, even_odd tt n → even_odd ff (n + 1)
इसके बाद, हम परिभाषित कुछ संक्षिप्त रूपों परस्पर आगमनात्मक प्रकार अनुकरण करने के लिए:: हम एक बूलियन सूचकांक का प्रतिनिधित्व एकरूपता जोड़ने
-- types
def even := even_odd tt
def odd := even_odd ff
-- constructors
def even.z : even 0 := even_odd.ze
def even.n (n : ℕ) (o : odd n): even (n + 1) := even_odd.ne n o
def odd.z : odd 1 := even_odd.zo
def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no n e
अब, चलो हमारे अपने प्रेरण सिद्धांतों शुरू करते हैं:
-- induction principles
def even.induction_on {n : ℕ} (ev : even n) (Ce : ℕ → Prop) (Co : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) : Ce n :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
tt n ev
def odd.induction_on {n : ℕ} (od : odd n) (Co : ℕ → Prop) (Ce : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
ff n od
Ce : ℕ → Propeven.induction_on के पैरामीटर को लागू करने के लिए बेहतर होगा, लेकिन किसी कारण से लीन इसका अनुमान नहीं लगा सकता (अंत में लेम्मा देखें, wher ई हमें Ce स्पष्ट रूप से पास करना होगा, अन्यथा दुबला infers Ce हमारे लक्ष्य से संबंधित नहीं है)। स्थिति odd.induction_on के साथ सममित है।
पारस्परिक रूप से पुनरावर्ती कार्यों को परिभाषित करने के लिए वाक्यविन्यास क्या है?
के रूप में इस lean-user thread में बताया गया है, पारस्परिक रूप से पुनरावर्ती कार्यों के लिए समर्थन बहुत ही सीमित है:
वहाँ मनमाने ढंग से परस्पर पुनरावर्ती कार्यों के लिए कोई समर्थन नहीं है, लेकिन एक बहुत ही सरल मामले के लिए समर्थन नहीं है। हम पारस्परिक रूप से पुनरावर्ती प्रकारों को परिभाषित करने के बाद, हम पारस्परिक रूप से पुनरावर्ती कार्यों को परिभाषित कर सकते हैं जो इन प्रकार की संरचना को "दर्पण" करते हैं।
आप उस धागे में एक उदाहरण पा सकते हैं।लेकिन, फिर, हम एक ही ऐड-ए-स्विचिंग-पैरामीटर दृष्टिकोण का उपयोग करके परस्पर रिकर्सिव फ़ंक्शंस अनुकरण कर सकते हैं। चलो पारस्परिक रूप से पुनरावर्ती बूलियन विधेय evenb और oddb अनुकरण:
def even_oddb : bool → ℕ → bool
| tt 0 := tt
| tt (n + 1) := even_oddb ff n
| ff 0 := ff
| ff (n + 1) := even_oddb tt n
def evenb := even_oddb tt
def oddb := even_oddb ff
यहाँ कैसे की सब से ऊपर इस्तेमाल किया जा सकता का एक उदाहरण है। आइए एक सरल लेम्मा साबित करें:
lemma even_implies_evenb (n : ℕ) : even n -> evenb n = tt :=
assume ev : even n,
even.induction_on ev (λ n, evenb n = tt) (λ n, oddb n = tt)
rfl
(λ (n : ℕ) (IH : oddb n = tt), IH)
rfl
(λ (n : ℕ) (IH : evenb n = tt), IH)