List nubsort in Agda

NubSort.agda

open import Relation.Nullary.Decidable
open import Function
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool
open import Data.Product
open import Data.List
open import Data.List.NonEmpty renaming (_∷_ to _⁺∷_ ; length to length⁺ ; [_] to ⁺[_])
open import Relation.Binary.Core
open import Relation.Binary renaming (IsDecStrictPartialOrder to IsDec< ; DecStrictPartialOrder to Dec< ; StrictTotalOrder to STO ; IsStrictTotalOrder to IsSTO)
open import Induction.Nat
open import Induction.WellFounded

module NubSort where

_<?_ : ∀ {d₁ d₂ d₃} {D : STO d₁ d₂ d₃} → Decidable (STO._<_ D)
_<?_ {D = d} = IsSTO._<?_ (STO.isStrictTotalOrder d)

_>?_ : ∀ {d₁ d₂ d₃} {D : STO d₁ d₂ d₃} → Decidable (flip (STO._<_ D))
_>?_ {D = d} = flip (IsSTO._<?_ (STO.isStrictTotalOrder d))

_<<_ : ∀ {a} {A : Set a} → Rel (List A) _
xs << ys = suc (length xs) ≤′ suc (length ys)

<<-trans : ∀ {a} {A : Set a} → Transitive {A = List A} _<<_
<<-trans {i = i} {j} {k} p q with ≤-trans {i = suc (length i)} {j = suc (length j)} {k = suc (length k)}
<<-trans {i = i} {j} {k} p q | t = ≤⇒≤′ (t (≤′⇒≤ p) (≤′⇒≤ q))

∣partition∣ : ∀ {a} {A : Set a} → (p : A → Bool) → (xs : List A) → (proj₁ (partition p xs) << xs) × (proj₂ (partition p xs) << xs)
∣partition∣ _ []                                                    = ≤′-refl     , ≤′-refl
∣partition∣ p (x ∷ xs) with p x | partition p xs | ∣partition∣ p xs
∣partition∣ p (x ∷ xs) | true   | (L , R)        | (∣L∣ , ∣R∣)      = s≤′s    ∣L∣ , ≤′-step ∣R∣
∣partition∣ p (x ∷ xs) | false  | (L , R)        | (∣L∣ , ∣R∣)      = ≤′-step ∣L∣ , s≤′s    ∣R∣

wf : ∀ {a} {A : Set a} → Well-founded {A = List A} (_<′_ on length)
wf = (Inverse-image.well-founded length) <-well-founded

-- Sort the list while removing duplicate elements
-- This is essentially a slightly modified quick sort
-- For an excellent explaination of well-founded recursion using regular quicksort as an example see:
-- http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/
nubsort⁺ : ∀ {d₁ d₂ d₃} {D : STO d₁ d₂ d₃} → List⁺ (STO.Carrier D) → List⁺ (STO.Carrier D)
nubsort⁺ {D = d} (h ⁺∷ t) = ns⁺ (h ⁺∷ t) (wf (h ∷ t))
  where
  ns⁺ : (xs : List⁺ (STO.Carrier d)) → Acc (_<′_ on length) (toList xs) → List⁺ (STO.Carrier d)
  ns⁺ (x ⁺∷ xs) (acc a) with partition <x xs      | ∣partition∣ <x xs
    where
    <x : STO.Carrier d → Bool
    <x y = ⌊ (_<?_ {D = d}) y x ⌋
  ns⁺ (x ⁺∷ xs) (acc a) | (lt             , gteq) | (p , q)           with partition >x gteq | ∣partition∣ >x gteq
    where
    >x : STO.Carrier d → Bool
    >x y = ⌊ (_>?_ {D = d}) y x ⌋
  ns⁺ (x ⁺∷ xs) (acc a) | (lt@(ltₕ ∷ ltₜ) , gteq) | (p , q)           | (gt@(gtₕ ∷ gtₜ) , _) | (r , _)             = sorted-lt ⁺++⁺ ⁺[ x ] ⁺++⁺ sorted-gt
    where
    gt<<xs    = <<-trans {A = STO.Carrier d} {i = gt} {j = gteq} {k = xs} r q
    sorted-lt = ns⁺ (ltₕ ⁺∷ ltₜ) (a lt p)
    sorted-gt = ns⁺ (gtₕ ⁺∷ gtₜ) (a gt gt<<xs)
  ns⁺ (x ⁺∷ xs) (acc a) | ([]             , gteq) | (_ , q)           | (gt@(gtₕ ∷ gtₜ) , _) | (r , _)             =                ⁺[ x ] ⁺++⁺ sorted-gt
    where
    gt<<xs    = <<-trans {A = STO.Carrier d} {i = gt} {j = gteq} {k = xs} r q
    sorted-gt = ns⁺ (gtₕ ⁺∷ gtₜ) (a gt gt<<xs)
  ns⁺ (x ⁺∷ xs) (acc a) | (lt@(ltₕ ∷ ltₜ) ,    _) | (p , _)           | ([]             , _) | (_ , _)             = sorted-lt ⁺++⁺ ⁺[ x ]
    where
    sorted-lt = ns⁺ (ltₕ ⁺∷ ltₜ) (a lt p)
  ns⁺ (x ⁺∷ xs) (acc _) | ([]             ,    _) | (_ , _)           | ([]             , _) | (_ , _)             =                ⁺[ x ]

nubsort : ∀ {d₁ d₂ d₃} {D : STO d₁ d₂ d₃} → List (STO.Carrier D) → List (STO.Carrier D)
nubsort {D = d} xs = ns xs (wf xs)
  where
  ns : (xs : List (STO.Carrier d)) → Acc (_<′_ on length) xs → List (STO.Carrier d)
  ns []       _ = []
  ns (x ∷ xs) _ = toList (nubsort⁺ {D = d} (x ⁺∷ xs))

test₀ : nubsort⁺ {D = strictTotalOrder} (3 ⁺∷ 2 ∷ [ 1 ]) ≡ 1 ⁺∷ 2 ∷ [ 3 ]
test₀ = refl

test₁ : nubsort⁺ {D = strictTotalOrder} (3 ⁺∷ 3 ∷ [ 3 ]) ≡ ⁺[ 3 ]
test₁ = refl

test₂ : nubsort⁺ {D = strictTotalOrder} (3 ⁺∷ 2 ∷ [ 3 ]) ≡ 2 ⁺∷ [ 3 ]
test₂ = refl

test₃ : nubsort⁺ {D = strictTotalOrder} (7 ⁺∷ 5 ∷ 3 ∷ 4 ∷ 2 ∷ 1 ∷ [ 0 ]) ≡ 0 ⁺∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [ 7 ]
test₃ = refl