日々の流転

λ. 「Coqで“無限オブ無限”」のyoshihiroさんによる証明

先日のCoqで“無限オブ無限”で書いたCoqのコードが題意を満たすことを、にわとり小屋でのプログラミング日記のyoshihiro503さんが証明してくれました。ありがとうございます。
⇒ Coqで”無限オブ無限”(証明部分)

これは圧巻。面倒そうだとは思っていたものの、なんと500行もの証明に。 ……自分でやらなくて正解だったかも(苦笑

Coqを知らない人はこれを見て何が何だか分からないと思うけど、CoqIDEに読み込ませてステップ実行*1させていくと、ゴールがどう変形されていくかが分かって、何をやってるかが分るはず。といっても、僕もまだ全部はとても理解できていないけど。