リストの反転

説明

ここでの課題は、自作のリスト反転関数と組み込みの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`.