Coqで証明付きのマージソートを書く - fetburner.core

この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。 少し季節外れの記事になりますが、前期はプロ演A^1の季節でしたね。 僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、 とりわけ彼らが苦戦していたのはマージソートを書く課題のようでした。 面白そうなので僕もCoqで実装してみましょう。 もちろん、証明付きで。 実装 とりあえず比較関数等の準備 Require Import Arith Div2 List Orders Sorted Permutation Program. Require Omega. Section MergeSort. Local Coercion is_true : bool >-> Sortclass. Local Hint Constructors Permutation St

[sh19910711]

"Coqを用いる事による利点は正しさが保証される事に留まりません。 今までバグを恐れて行えなかった積極的な最適化を行う勇気も我々に与えてくれる"

[ruicc]

証明つけつつパフォーマンス向上させようと