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