Agda で挿入ソートする - zyxwvの日記概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコードはあんまり見ない気がするので、誰かの参考になれば幸いです。 関数定義 インサート関数 insert と、リストをソートする関数 insertSort をごく普通に定義します。 "≤?" は Coq で言うところの SumBool 型の値を返す不等号演算子です。たぶん。こちらを使うと、条件分岐した先でその条件が仮定として使えるようになるので、後の証明がしやすくなります。 insert : ℕ → List ℕ → List ℕ insert x [] = [ x ] insert x (x' ∷ xs)
