An implementation of mergesort in Agda.

MergeSort.agda

open import Level                                      using (_⊔_)
open import Function                                   using (_∘_)
open import Data.Vec                                   using (Vec; []; _∷_; foldr)
open import Data.Nat                                   using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties.Simple                 using (+-right-identity; +-suc)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Data.Product                               using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty                                 using (⊥-elim)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Relation.Binary                            using (module DecTotalOrder; DecTotalOrder; Rel)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; cong; sym)


module MergeSort {c ℓ₁ ℓ₂} (decTotalOrder : DecTotalOrder c ℓ₁ ℓ₂) where


  open DecTotalOrder decTotalOrder using (_≤_; _≤?_; total; trans) renaming (Carrier to A)
  open DecTotalOrder Data.Nat.decTotalOrder using () renaming (_≤?_ to _≤?-ℕ_)


  -- A bounded version of the A type that is bounded at the top by ⊤
  -- and at the bottom by ⊥.

  data  : Set c where
    ⊤ : Â
    ⟦_⟧ : A → Â


  -- Computes the minimum of two bounded values.

  infix 5 _⊓_

  _⊓_ : Â → Â → Â
  ⊤ ⊓ y = y
  x ⊓ ⊤ = x
  ⟦ x ⟧ ⊓ ⟦ y ⟧ with x ≤? y
  ⟦ x ⟧ ⊓ ⟦ y ⟧ | yes x≤y = ⟦ x ⟧
  ⟦ x ⟧ ⊓ ⟦ y ⟧ | no  x>y = ⟦ y ⟧


  infix 4 _≲_

  data _≲_ : Rel  (c ⊔ ℓ₂) where
    ≲⊤     : ∀ {x} → x ≲ ⊤
    ≤-lift : ∀ {x y} → x ≤ y → ⟦ x ⟧ ≲ ⟦ y ⟧

  -- Smart constructor for when we only have a proof of y≰x.

  ≰-lift : ∀ {x y} → ¬ (y ≤ x) → ⟦ x ⟧ ≲ ⟦ y ⟧
  ≰-lift {x} {y} y≰x with total x y
  ≰-lift y≰x | inj₁ x≤y = ≤-lift x≤y
  ≰-lift y≰x | inj₂ y≤x = ⊥-elim (y≰x y≤x)

  -- Proof that ⊓ conserves ≲.

  ⊓-conserves-≲ : ∀ {x y z} → x ≲ y → x ≲ z → x ≲ y ⊓ z
  ⊓-conserves-≲ {x} {⊤}     {_} _ q = q
  ⊓-conserves-≲ {x} {⟦ _ ⟧} {⊤} p _ = p
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} p q with y ≤? z
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} p _ | yes y≤z = p
  ⊓-conserves-≲ {x} {⟦ y ⟧} {⟦ z ⟧} _ q | no  y≰z = q


  -- Representation a vector of length n, of which the first k
  -- elements are still unsorted, and which has lower bound l.

  infix 5 _∷_by_

  data OVec : Â → ℕ → Set (c ⊔ ℓ₂) where
    []     : OVec ⊤ 0
    _∷_by_ : ∀ {l k} (x : A) (xs : OVec l k) → ⟦ x ⟧ ≲ l → OVec ⟦ x ⟧ (suc k)


  -- Converts an ordered list to a regular length-indexed list.

  toVec : ∀ {l k} → OVec l k → Vec A k
  toVec [] = []
  toVec (x ∷ xs by _) = x ∷ toVec xs

  ⊓-identity : ∀ {l} → l ⊓ ⊤ ≡ l
  ⊓-identity {  ⊤  } = refl
  ⊓-identity {⟦ x ⟧} = refl

  ≲-transitive : ∀ {x y z} → x ≲ y → y ≲ z → x ≲ z
  ≲-transitive ≲⊤ ≲⊤ = ≲⊤
  ≲-transitive (≤-lift p₁) ≲⊤ = ≲⊤
  ≲-transitive (≤-lift p₁) (≤-lift p₂) = ≤-lift (trans p₁ p₂)


  merge : ∀ {l₁ l₂ k₁ k₂} → OVec l₁ k₁ → OVec l₂ k₂ → OVec (l₁ ⊓ l₂) (k₁ + k₂)
  merge {⊤ } {l₂} {0 } {k₂} [] ys = ys
  merge {l₁} {⊤ } {k₁} {0 } xs [] rewrite ⊓-identity {l₁} | +-right-identity k₁ = xs
  merge {.(⟦ x ⟧)} {.(⟦ y ⟧)} {suc k₁} {suc k₂} (x ∷ xs by p) (y ∷ ys by q) with x ≤? y
  ... | yes x≤y
      = x ∷ (merge xs (y ∷ ys by q)) by ⊓-conserves-≲ p (≤-lift x≤y)
  ... | no  x≰y rewrite +-suc k₁ k₂
      = y ∷ (merge (x ∷ xs by p) ys) by ⊓-conserves-≲ (≰-lift x≰y) q


  -- A direct implementation of the sorting function using split
  -- requires a proof of well-foundedness for the recursion on the two
  -- halves, as Agda cannot automatically infer that the two halves
  -- are smaller than the whole.
  --
  -- However, we can use a trick: we can make the recursion explicit
  -- in a data structure and sort by induction on that. Using this
  -- trick agda is able to infer that both the vector in dealT and the
  -- tree in mergeT become structurally smaller.

  data Tree {ℓ} (A : Set ℓ) : ℕ → Set ℓ where
    null : Tree A 0
    leaf : A → Tree A 1
    fork : ∀ {r l} → Tree A r → Tree A l → Tree A (r + l)

  insertT : ∀ {ℓ} {n} {A : Set ℓ} → A → Tree A n → Tree A (suc n)
  insertT {_} {.0}       x (null)               = leaf x
  insertT {_} {.1}       x (leaf y)             = fork (leaf x) (leaf y)
  insertT {_} {.(r + l)} x (fork {r} {l} tᴿ tᴸ) with r ≤?-ℕ l
  ... | yes r≤l = fork (insertT x tᴿ) tᴸ
  ... | no  r≰l rewrite sym (+-suc r l) = fork tᴿ (insertT x tᴸ)

  dealT : ∀ {k} → Vec A k → Tree A k
  dealT = foldr (Tree A) insertT null

  mergeT : ∀ {k} → Tree A k → ∃ (λ l → OVec l k)
  mergeT (null)     = ⊤ , []
  mergeT (leaf x)   = ⟦ x ⟧ , x ∷ [] by ≲⊤
  mergeT (fork r l) with mergeT r | mergeT l
  ... | m , xs | n , ys = m ⊓ n , merge xs ys


  -- Now we can easily define the mergesort function using the
  -- `mergeT` and `dealT` primitives.

  mergesort : ∀ {k} → Vec A k → ∃ (λ l → OVec l k)
  mergesort = mergeT ∘ dealT

HI
I tried running this with
agda 2.6.2.2
agda-stdlib 1.7.1
with GHC backend 8.10.7 and 9.2.1
but I'm getting this error
Failed to find source of module Data.Nat.Properties.Simple in any
of the following locations:
_ C:\Users\User\Documents\Code\agda\demo-agda\Data\Nat\Properties\Simple.agda
C:\Users\User\Documents\Code\agda\demo-agda\Data\Nat\Properties\Simple.lagda
C:\Users\User\Documents\Code\agda\plfa\agda-stdlib-1.7.1\src\Data\Nat\Properties\Simple.agda
C:\Users\User\Documents\Code\agda\plfa\agda-stdlib-1.7.1\src\Data\Nat\Properties\Simple.lagda
C:\Users\User\Documents\Code\agda\agda.stack-work\install\1ec3edc8\share\x86_64-windows-ghc-9.2.1\Agda-2.6.2.2\lib\prim\Data\Nat\Properties\Simple.agda
C:\Users\User\Documents\Code\agda\agda.stack-work\install\1ec3edc8\share\x86_64-windows-ghc-9.2.1\Agda-2.6.2.2\lib\prim\Data\Nat\Properties\Simple.lagda
when scope checking the declaration
open import Data.Nat.Properties.Simple using (+-right-identity;
+-suc)_

This was written in 2015 for an old version of Agda and the standard library. You can probably patch this up by fixing the imports to the newer versions, but I wouldn’t expect it to work out of the box.