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