ऐरे को उलटिए

निर्देश

आपको एक कस्टम ऐरे उलटने वाले फंक्शन और बिल्ट-इन List.reverse के बीच समानता सिद्ध करनी है।

इस अभ्यास की प्रकृति ऐसी है कि यहाँ पारंपरिक रनटाइम टेस्टों पर भरोसा नहीं किया जाता। इसके बजाय प्रमाण की जाँच एक प्रमेय check से होती है। अगर यह प्रमेय टाइपचेक हो जाए, तो आप टेस्ट को पास मान सकते हैं।

अगर आप स्थानीय रूप से या Lean के ऑनलाइन प्लेग्राउंड में काम करते हैं, तो Lean InfoView के ज़रिए आपको तुरंत फीडबैक मिलता है कि कोई प्रमेय सफल हुआ या असफल, और असफल होने पर क्यों। यह बहुत काम का टूल है, जो आपके प्रमाण में इस्तेमाल हो रही सारी स्थानीय वैल्यू और आपका वर्तमान लक्ष्य दिखा सकता है।

Lean में प्रमेय सिद्ध करना

प्रमेय सिद्ध करना Lean का अभिन्न हिस्सा है। यह प्रोग्रामरों को यह शक्ति देता है कि वे अपने प्रोग्रामों के गुण सिद्ध कर सकें, उनके व्यवहार पर तर्क कर सकें, और टाइप के स्तर पर बाध्यताएँ तथा स्पेसिफिकेशन लिख सकें।

यह अध्याय Lean में प्रमेय सिद्ध करने का अच्छा परिचय देता है। और गहराई में जाने के लिए, Lean की वेबसाइट पर यह किताब एक आधिकारिक संसाधन के रूप में दी गई है।

Lean में कई टैक्टिक उपलब्ध हैं जो सिद्ध करने की प्रक्रिया को, या उसके कुछ हिस्सों को, स्वचालित कर सकती हैं। आप भाषा संदर्भ पर भी एक नज़र डाल सकते हैं।

@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
    ... -- proof here

-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.