リストの要素の内、条件に合致するものだけを抜き出す関数 filter の仕様を Coq で証明してみました。元ネタは『ソフトウェアの基礎』の練習問題。完全なコードは https://gist.github.com/4401408 に置いてあります。 とりあえず定義の確認 List モジュール…

この記事は LL/ML Advent Calendar の 23 日目です。「タイトルに "LL" もしくは "ML" を含むこと」という謎ルールに従い、「群の正規部分群の全体がモジュラー束 (Modular Lattices) をなすこと」を Coq により証明してみました。なお、完全なコードは http…