Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごと…

Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。 アルゴリズムの定義 仕様の検証その 1 仕…

Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。 アルゴリズムの定義 仕様の検証その 1 (この記事) 仕様の検証その 2 今回の目標 さて、前回の最後にも触れた通り、前回定義…

以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。 アルゴリズムの定義 (この記事) 仕様の検証その 1 仕様の検証その 2 ちなみに、…

前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明して…