Coqによる証明駆動開発で Merge Sort プログラムをつくってみた - にわとり小屋でのプログラミングOCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。 プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket。 思ったより簡単ではなく、いろいろなテクニックが必要で非常に勉強になった。Coq初心者の人はMergeSortの問題をとりあえずの目標にして証明を頑張ると非常に効率がいいのではないかと思う。 私は、だいたい以下の流れでプログラムした。 Sortedという命題を作り、リストがソート済みであるという状態を定義する mergesort関数があるとして、満たすべき性質(i)を定理として記述する mergesort関数を定義する mergesort関数に必要な補助関数 merge関数を定義し
