নির্দেশনা
আপনার কাজ হলো একটি নিজস্ব অ্যারে-উল্টানোর ফাংশন আর বিল্ট-ইন List.reverse-এর মধ্যে সমতা প্রমাণ করা।
এই অনুশীলনীর ধরন অনুযায়ী, প্রচলিত রানটাইম টেস্টের উপর নির্ভর না করে check নামের একটি উপপাদ্য দিয়ে প্রমাণটি যাচাই করা হয়।
এই উপপাদ্যটি টাইপচেক করতে পারলে আপনি টেস্টটি পাস হয়েছে বলে ধরতে পারেন।
আপনি যদি স্থানীয়ভাবে বা Lean-এর অনলাইন প্লেগ্রাউন্ড-এ কাজ করেন, তাহলে Lean InfoView-এর মাধ্যমে কোনো উপপাদ্য সফল হয়েছে কি ব্যর্থ হয়েছে, আর ব্যর্থ হলে কেন, তার তাৎক্ষণিক ফিডব্যাক পাবেন।
এটি এক অমূল্য টুল, যা আপনার প্রমাণে ব্যবহৃত সব স্থানীয় মান এবং আপনার বর্তমান লক্ষ্য দেখাতে সক্ষম।
sorry ট্যাকটিক যেকোনো প্রমাণকে সঠিক বলে দেখায়।
এই কারণে, আসলে কোনো প্রমাণ লেখার আগেই check উপপাদ্যটি স্বয়ংক্রিয়ভাবে টাইপচেক হয়ে যেতে পারে বলে মনে হতে পারে।
আপনার প্রমাণ থেকে sorry সরিয়ে ফেললেই Lean InfoView সঠিক ফিডব্যাক দেখাবে।
Lean-এ থিওরেম প্রমাণ করা
থিওরেম প্রুভিং Lean-এর একটি অবিচ্ছেদ্য অংশ।
এটি প্রোগ্রামারদের তাদের প্রোগ্রাম সম্পর্কে বৈশিষ্ট্য প্রমাণ করার, তাদের আচরণ নিয়ে যুক্তি করার, এবং টাইপ লেভেলে সীমাবদ্ধতা ও স্পেসিফিকেশন এনকোড করার ক্ষমতা দেয়।
এই অধ্যায়টি Lean-এ থিওরেম প্রুভিংয়ের একটি ভালো পরিচিতি দেয়।
আরও গভীরে যেতে চাইলে, Lean-এর ওয়েবসাইটে অফিসিয়াল রিসোর্স হিসেবে এই বইটি তালিকাভুক্ত আছে।
Lean অনেক ট্যাকটিক দেয়, যা প্রমাণ বা তার অংশবিশেষ নিজে থেকেই সম্পন্ন করতে পারে।
আপনি চাইলে একটি ভাষা রেফারেন্স দেখে নিতে পারেন।
দুটি ডেফিনিশনের মধ্যে সাম্য প্রমাণ করে এমন একটি থিওরেমে আমরা কম্পাইলার অ্যাট্রিবিউট csimp ব্যবহার করতে পারি।
এই অ্যাট্রিবিউট কম্পাইলারকে প্রথম ডেফিনিশনের জায়গায় দ্বিতীয়টি ব্যবহার করতে নির্দেশ দেয়:
@[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`.
এমন পরিস্থিতিতে এটি বিশেষভাবে কাজে লাগে, যেখানে একটি ইমপ্লিমেন্টেশন বেশি কার্যকর কিন্তু কম স্পষ্ট।
আমরা একটি সরল স্পেসিফিকেশন লিখতে পারি এবং কম্পাইল করা কোডকে তার বদলে আরও কার্যকর ইমপ্লিমেন্টেশনটি ব্যবহার করাতে পারি।
List ও Array-এর অনেক ফাংশন এই প্যাটার্নটি ব্যবহার করে।
