Вказівки
Доведіть рівність між власною функцією обертання масиву та вбудованою 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 використовують цей прийом.
