# 在agda中合并排序

``````open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module MergeSort
{ℓ a} {A : Set a}
{_<_ : Rel A ℓ}
(strictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open IsStrictTotalOrder strictTotalOrder
``````

``````open import Data.List
open import Data.Nat
hiding (compare)
open import Data.Product
open import Function
open import Induction.Nat
open import Induction.WellFounded
``````

``````merge : (xs ys : List A) → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with compare x y
... | tri< _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri≈ _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri> _ _ _ = y ∷ merge (x ∷ xs) ys
``````

`split` 也很容易：

``````split : List A → List A × List A
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l
``````

``````_<ₗ_ : Rel (List A) _
_<ₗ_ = _<′_ on length
``````

``````-- Lemma.
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl     = ≤′-refl
s≤′s (≤′-step p) = ≤′-step (s≤′s p)

split-less : ∀ (x : A) y ys →
let xs    = x ∷ y ∷ ys
l , r = split (x ∷ y ∷ ys)
in l <ₗ xs × r <ₗ xs
split-less _ _ [] = ≤′-refl , ≤′-refl
split-less _ _ (_ ∷ []) = ≤′-refl , ≤′-step ≤′-refl
split-less _ _ (x ∷ y ∷ ys) with split-less x y ys
... | p₁ , p₂ = ≤′-step (s≤′s p₁) , ≤′-step (s≤′s p₂)
``````

``````open Inverse-image {A = List A} {_<_ = _<′_} length
renaming (well-founded to <ₗ-well-founded)

open All (<ₗ-well-founded <-well-founded)
renaming (wfRec to <ₗ-rec)
``````

``````merge-sort : List A → List A
merge-sort = <ₗ-rec _ _ go
where
go : (xs : List A) → (∀ ys → ys <ₗ xs → List A) → List A
go [] rec = []
go (x ∷ []) rec = x ∷ []
go (x ∷ y ∷ ys) rec =
let (l , r)   = split (x ∷ y ∷ ys)
(p₁ , p₂) = split-less x y ys
in merge (rec l p₁) (rec r p₂)
``````

``````{-# OPTIONS --sized-types #-}
``````

``````open import Data.Product
open import Function
open import Size
``````

``````infixr 5 _∷_

data List {a} (A : Set a) : {ι : Size} → Set a where
[]  : ∀ {ι} →                  List A {↑ ι}
_∷_ : ∀ {ι} → A → List A {ι} → List A {↑ ι}
``````

`merge` 保持大致相同，我们只需要稍微改变一下类型就可以说服终止检查器：

``````merge : ∀ {ι} → List A {ι} → List A → List A
``````

``````split : ∀ {ι} → List A {ι} → List A {ι} × List A {ι}
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l
``````

``````merge-sort : ∀ {ι} → List A {ι} → List A
merge-sort [] = []
merge-sort (x ∷ []) = x ∷ []
merge-sort (x ∷ y ∷ ys) =
let l , r = split ys
in  merge (merge-sort (x ∷ l)) (merge-sort (y ∷ r))
``````

0 条评论