# ソースコード

ソースコードはリポジトリにあります．
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`の定義では証明を捨ててますが，正当性の証明では必要になります．

# 正当性の定義

```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`に置き換えても問題ないですが，今回は`ℕ`の通常の順序しか扱わないので`_≤_`に限定しました．

# 証明

```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時間ほど唸ってしまった．