التعليمات
مهمتك إثبات التساوي بين دالة مخصّصة لعكس مصفوفة و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 هذا النمط.
