コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

Leanでrev_rev_id

rev_rev_idとは、リストを2回逆順にすると元に戻る、というやつだ。
Leanで挑戦してみた。

Leanのインストール

バイナリがあるから、それを持ってくるだけ。
本格的にやりたい方は
https://righ1113.hatenablog.com/entry/2020/06/06/101151
をどうぞ。

開発環境

VSCodeで、インタラクティブにコーディングできる。

型の確認と、値の評価

  • #checkで型の確認ができる。
  • #reduceで値の評価ができる。

structured proofとtactic

まだやっていない。

Equational Reasoning

calcでおこなうみたい。
Reasoningの中でrewrite(rw)できるのは大きいかも。

rev_rev_idの実装

例によってsnocを使う方法でやってみた。
みょんみょんさんの実装を参考にした。

.
.