証明したこと
挿入ソートによってソートされることと挿入ソートによって要素が変わらないことを証明しました．
ソースコード
ソースコードはリポジトリにあります．
agda-stdlibのバージョンが0.14以前では≤-totalがなくて動かないので注意してください．
挿入ソートの定義
以下によって挿入ソートを定義しました．
insert : ℕ → List ℕ → List ℕ
insert x [] = x ∷ []
insert x (y ∷ ys) with x ≤? y
... | yes _ = x ∷ y ∷ ys
... | no _ = y ∷ insert x ys
isort : List ℕ → List ℕ
isort [] = []
isort (x ∷ xs) = insert x (isort xs)
x ≤? yの型はDec (x ≤ y)でコンストラクタはyes : x ≤ y → Dec (x ≤ y)とno : ¬ (x ≤ y) → Dec (x ≤ y)なのでパターンマッチすると証明つきで真偽がわかるようになってます．
insertの定義では証明を捨ててますが，正当性の証明では必要になります．
正当性の定義
正当性を証明するにあたってソート済みであることと要素が同じであることを定義する必要があります．
定義はCoqからパクってきました．
data Sorted : List ℕ → Set where
snull : Sorted []
scons1 : {x : ℕ} → Sorted (x ∷ [])
scons : {x y : ℕ} {ys : List ℕ} → x ≤ y → Sorted (y ∷ ys) → Sorted (x ∷ y ∷ ys)
data Permutation {A} : List A → List A → Set where
pnull : Permutation [] []
pskip : {x : A} {xs ys : List A} → Permutation xs ys → Permutation (x ∷ xs) (x ∷ ys)
pswap : {x y : A} {xs : List A} → Permutation (x ∷ y ∷ xs) (y ∷ x ∷ xs)
ptrans : {xs ys zs : List A} → Permutation xs ys → Permutation ys zs → Permutation xs zs
Sortedの定義における_≤_は一般の述語A → A → Setに置き換えても問題ないですが，今回はℕの通常の順序しか扱わないので_≤_に限定しました．
証明
証明はSortedとPermutationのinsertに関する補題を示して，そこから目的の命題を証明するという風に行ないました．
補題の証明はいい感じになるまで帰納法を適用すればいけます．
補題の証明ができれば本題は楽に示せます．
step-insert : {x y : ℕ}{ys : List ℕ} → ¬ (x ≤ y) → insert x (y ∷ ys) ≡ y ∷ insert x ys
step-insert {x} {y} {ys} x≰y with x ≤? y
... | yes x≤y = ⊥-elim (x≰y x≤y)
... | no x≰y₁ = refl
lem-isorted : (x : ℕ) → (xs : List ℕ) → Sorted xs → Sorted (insert x xs)
lem-isorted x [] s = scons1
lem-isorted x (y ∷ ys) s with x ≤? y
... | yes x≤y = scons x≤y s
lem-isorted x (y ∷ []) scons1 | no x≰y = scons (lem-≤ x≰y) scons1
lem-isorted x (y ∷ (z ∷ zs)) (scons y≤z s) | no x≰y with x ≤? z
... | yes x≤z = scons (lem-≤ x≰y) (scons x≤z s)
... | no x≰z = scons y≤z (subst Sorted (step-insert x≰z) (lem-isorted x (z ∷ zs) s))
iSorted : (xs : List ℕ) → Sorted (isort xs)
iSorted [] = snull
iSorted (x ∷ xs) = lem-isorted x (isort xs) (iSorted xs)
lem-iperm : (x : ℕ) (xs : List ℕ) → Permutation (x ∷ xs) (insert x xs)
lem-iperm x [] = pskip pnull
lem-iperm x (y ∷ []) with x ≤? y
... | yes x≤y = pskip (pskip pnull)
... | no x≰y = pswap
lem-iperm x (y ∷ z ∷ zs) with x ≤? y
... | yes x≤y = ptrans pswap pswap
... | no x≰y with x ≤? z
... | yes x≤z = pswap
... | no x≰z = ptrans pswap (pskip (subst (Permutation (x ∷ z ∷ zs)) (step-insert x≰z) (lem-iperm x (z ∷ zs))))
perm-isort : (xs : List ℕ) → Permutation xs (isort xs)
perm-isort [] = pnull
perm-isort (x ∷ xs) = ptrans (pskip (perm-isort xs)) (lem-iperm x (isort xs))
感想
Agdaの型システムが結構バカなので計算を進められるのに進めてくれない場面があって，そういった場面はsubstを使って明示的に変形しなければいけないのが面倒．
あとwithでパターンマッチするときに対象の型がimportされていないとエラーになるが，エラーコードがyes _の左辺がパースできないとかでシンタックスエラーなのかと1時間ほど唸ってしまった．
時間とやる気があればマージソートやクイックソートなどの他のアルゴリズムでも同様のことを証明したり，安定ソートであることを示したりなどしたい．