概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコードはあんまり見ない気がするので、誰かの参考になれば幸いです。 関数定義 インサート関数 insert と、リストをソートする関数 insertSort をごく普通に定義します。 "≤?" は Coq で言うところの SumBool 型の値を返す不等号演算子です。たぶん。こちらを使うと、条件分岐した先でその条件が仮定として使えるようになるので、後の証明がしやすくなります。 insert : ℕ → List ℕ → List ℕ insert x [] = [ x ] insert x (x' ∷ xs)
![zyxwvの日記](https://cdn-ak-scissors.b.st-hatena.com/image/square/06a15c64ba0ceec233d86d71001ebb29a9dcbf5d/height=288;version=1;width=512/https%3A%2F%2Fcdn.blog.st-hatena.com%2Fimages%2Ftheme%2Fog-image-1500.png)