Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Monday, 01-Feb-2021 09:11:46 JST きゅーけー

   二分木に要素を追加しても全てのノードのキーが、左の木の全てのノードのキーよりも大きく、右の木の全てのノードのキーよりも小さくなることを証明した。

   補題を思い付くのが難しい。たぶん3時間くらいかかった。

   https://gitlab.com/tojoqk/practice-acl2/-/blob/b9222e3aad3d4c8d9eb78a04f49621e56e13a718/binary-tree.lisp

   #ACL2

   • sumiyaki likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Monday, 01-Feb-2021 09:20:09 JST きゅーけー

     in reply to

     ACL2 エキスパートになれば、補題とヒントをすぐに思い付けるようになるのだろうか…。もしも、訓練によって補題とヒントがすぐに思い付けるようになったらめっちゃ効率的に証明によってプログラムの信頼性を保証していけるわけなので頑張っていきたい。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Monday, 01-Feb-2021 09:20:57 JST きゅーけー

     in reply to

     後からみると10分くらいで思い付きそうなことしかしていないのが悲しい…