دستورالعمل‌ها
وظیفه‌ی شما این است که برابری میان یک تابع سفارشی برای معکوس‌کردن فهرست و 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 از این الگو استفاده می‌کنند.
