二分木に要素を追加しても全てのノードのキーが、左の木の全てのノードのキーよりも大きく、右の木の全てのノードのキーよりも小さくなることを証明した。
補題を思い付くのが難しい。たぶん3時間くらいかかった。
https://gitlab.com/tojoqk/practice-acl2/-/blob/b9222e3aad3d4c8d9eb78a04f49621e56e13a718/binary-tree.lisp
#ACL2
ACL2 エキスパートになれば、補題とヒントをすぐに思い付けるようになるのだろうか…。もしも、訓練によって補題とヒントがすぐに思い付けるようになったらめっちゃ効率的に証明によってプログラムの信頼性を保証していけるわけなので頑張っていきたい。
後からみると10分くらいで思い付きそうなことしかしていないのが悲しい…
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!
ACL2 エキスパートになれば、補題とヒントをすぐに思い付けるようになるのだろうか…。もしも、訓練によって補題とヒントがすぐに思い付けるようになったらめっちゃ効率的に証明によってプログラムの信頼性を保証していけるわけなので頑張っていきたい。