Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 00:18:16 JST きゅーけー

   ACL2 でリストの全ての順列を求める関数を書いて、順列の数が元のリストの長さの階乗個になることを証明できた。これは想像以上に大変だった。順列の実装は20行未満なのに補助関数や補助定理で 300 行くらい書いている……。たぶん何か回り道をしている気がするので短縮は可能だと思う。

   source: https://git.tojo.tokyo/acl2-theorems.git/tree/permutations.lisp?id=c7cb466e2caf7bc500f66472d8781a14037eec1eCI: https://ci.tojo.tokyo/jobs/acl2-verify/221

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 13-Aug-2021 12:48:15 JST きゅーけー

     in reply to

     ACL2 のリストの順列の数が階乗になるやつの証明を超リファクタリングした。やはり全てが見えている状態でかくと違う。無駄な定理の証明を省いたことで 300 行あったのが 200 行くらいになったし、全体的に美しくなった。最高だ。

     source: https://git.tojo.tokyo/acl2-theorems.git/tree/permutations.lisp?id=7e2450d7f7ef454e8fa0a5c41ec6c305cc5a8c25CI: https://ci.tojo.tokyo/jobs/acl2-verify/235