Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Correctness and runtime of mergesort, insertion sort and selection sort.
module Sorting where
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.PropositionalEquality as PE
open PE using (_≡_)
open import Function
open import Induction.Nat
open import Induction.WellFounded using (Acc;acc)
open SemiringSolver
-- This follows from extensionality:
postulate acc-irrelevance : {n : ℕ} {a b : Acc _<′_ n} a ≡ b
module FromExtensionality (extensionality : PE.Extensionality ℓ₀ ℓ₀) where
acc-irrelevance' : {n : ℕ} {a b : Acc _<′_ n} a ≡ b
acc-irrelevance' {a = acc a} {b = acc b}
= PE.cong acc (extensionality (\y extensionality (\l acc-irrelevance')))
-----------------------------------------------------------------------------------------
-- Counting monad
-----------------------------------------------------------------------------------------
-- A monad that keeps a natural number counter
module CountingMonad where
private
module Dummy where
infix 1 _in-time_
data _in-time_ {a} (A : Set a) (n : ℕ) : Set a where
box : A A in-time n
open Dummy public using (_in-time_)
open Dummy
unbox : {a} {A : Set a} {n} A in-time n A
unbox (box x) = x
infixl 1 _>>=_
_>>=_ : {a b} {A : Set a} {B : Set b} {n m : ℕ} A in-time n (A B in-time m) B in-time (n + m)
box x >>= f = box (unbox (f x))
_=<<_ : {a b} {A : Set a} {B : Set b} {n m : ℕ} (A B in-time m) A in-time n B in-time (n + m)
_=<<_ = flip _>>=_
infixr 2 _<$>_
_<$>_ : {a b} {A : Set a} {B : Set b} {n : ℕ} (A B) A in-time n B in-time n
f <$> box x = box (f x)
_<$$>_ : {a b} {A : Set a} {B : Set b} {n : ℕ} A in-time n (A B) B in-time n
_<$$>_ = flip _<$>_
return : {a} {A : Set a} {n : ℕ} A A in-time n
return = box
bound-≡ : {a} {A : Set a} {m n} (m ≡ n) A in-time m A in-time n
bound-≡ = PE.subst (_in-time_ _)
bound-+ : {a} {A : Set a} {m n k} (m + k ≡ n) A in-time m A in-time n
bound-+ eq x = bound-≡ eq (x >>= return)
bound-≤ : {a} {A : Set a} {m n} (m ≤ n) A in-time m A in-time n
bound-≤ m≤n = bound-+ (lem m≤n)
where
lem : {m n} (m ≤ n) m + (n ∸ m) ≡ n
lem z≤n = PE.refl
lem (s≤s m≤n') = PE.cong suc (lem m≤n')
bound-≤′ : {a} {A : Set a} {m n} (m ≤′ n) A in-time m A in-time n
bound-≤′ ≤′-refl x = x
bound-≤′ (≤′-step l) x = return {n = 1} x >>= bound-≤′ l
open CountingMonad
-----------------------------------------------------------------------------------------
-- Permutations
-----------------------------------------------------------------------------------------
1+m+n=m+1+n : (m n : ℕ) suc (m + n) ≡ m + suc n
1+m+n=m+1+n zero n = PE.refl
1+m+n=m+1+n (suc m) n = PE.cong suc (1+m+n=m+1+n m n)
module Permutations {a} (A : Set a) where
-- x ◂ xs ≡ ys means that ys is equal to xs with x inserted somewhere
data _◂_≡_ (x : A) : List A → List A → Set a where
here : {xs} x ◂ xs ≡ (x ∷ xs)
there : {y} {xs} {xys} (p : x ◂ xs ≡ xys) x ◂ (y ∷ xs) ≡ (y ∷ xys)
-- Proof that a list is a permutation of another one
data IsPermutation : List A → List A → Set a where
[] : IsPermutation [] []
_∷_ : {x xs ys xys}
(p : x ◂ ys ≡ xys)
(ps : IsPermutation xs ys)
IsPermutation (x ∷ xs) xys
-- Identity permutation
id-permutation : (xs : List A) IsPermutation xs xs
id-permutation [] = []
id-permutation (x ∷ xs) = here ∷ id-permutation xs
-- cons on the other side
insert-permutation : {x xs ys xys}
x ◂ ys ≡ xys IsPermutation ys xs IsPermutation xys (x ∷ xs)
insert-permutation here p = here ∷ p
insert-permutation (there y) (p ∷ ps) = there p ∷ insert-permutation y ps
-- inverse permutations
inverse-permutation : {xs ys} -> IsPermutation xs ys IsPermutation ys xs
inverse-permutation [] = []
inverse-permutation (p ∷ ps) = insert-permutation p (inverse-permutation ps)
swap-inserts : {x y xs xxs yxxs}
(x ◂ xs ≡ xxs) (y ◂ xxs ≡ yxxs) ∃ \yxs (y ◂ xs ≡ yxs) × (x ◂ yxs ≡ yxxs)
swap-inserts p here = _ , here , there p
swap-inserts here (there q) = _ , q , here
swap-inserts (there p) (there q) with swap-inserts p q
... | _ , p' , q' = _ , there p' , there q'
extract-permutation : {x ys zs zs'}
x ◂ ys ≡ zs IsPermutation zs zs'
∃ \ys' (x ◂ ys' ≡ zs') × IsPermutation ys ys'
extract-permutation here (q ∷ qs) = _ , q , qs
extract-permutation (there p) (q ∷ qs) with extract-permutation p qs
... | ys' , r , rs with swap-inserts r q
... | ys'' , s , t = ys'' , t , s ∷ rs
-- composing permutations
compose-permutation : {xs ys zs : List A}
IsPermutation xs ys IsPermutation ys zs IsPermutation xs zs
compose-permutation [] [] = []
compose-permutation (p ∷ ps) qqs with extract-permutation p qqs
... | _ , q , qs = q ∷ compose-permutation ps qs
insert-++₁ : {x xs ys xxs} x ◂ xs ≡ xxs x ◂ (xs ++ ys) ≡ (xxs ++ ys)
insert-++₁ here = here
insert-++₁ (there p) = there (insert-++₁ p)
insert-++₂ : {y xs ys yys} y ◂ ys ≡ yys y ◂ (xs ++ ys) ≡ (xs ++ yys)
insert-++₂ {xs = []} p = p
insert-++₂ {xs = _ ∷ xs} p = there (insert-++₂ {xs = xs} p)
-- Length of permutations
length-insert : {x xs xxs} x ◂ xs ≡ xxs length xxs ≡ suc (length xs)
length-insert here = PE.refl
length-insert (there p) = PE.cong suc (length-insert p)
length-permutation : {xs ys} IsPermutation xs ys length xs ≡ length ys
length-permutation [] = PE.refl
length-permutation (p ∷ ps) = PE.cong suc (length-permutation ps) ⟨ PE.trans ⟩ PE.sym (length-insert p)
same-perm' : {x xs xxs ys} x ◂ xs ≡ xxs x ◂ ys ≡ xxs IsPermutation xs ys
same-perm' here here = id-permutation _
same-perm' here (there q) = insert-permutation q (id-permutation _)
same-perm' (there p) here = p ∷ id-permutation _
same-perm' (there p) (there q) = here ∷ same-perm' p q
same-perm : {x xs xxs y ys yys}
x ≡ y IsPermutation xxs yys x ◂ xs ≡ xxs y ◂ ys ≡ yys IsPermutation xs ys
same-perm PE.refl ps q r with extract-permutation q ps
... | l' , q' , ps' = compose-permutation ps' (same-perm' q' r)
-----------------------------------------------------------------------------------------
-- Sorted lists
-----------------------------------------------------------------------------------------
module SortedList
{a r}
{A : Set a}
{_≤_ : Rel A r}
(isPartialOrder : IsPartialOrder _≡_ _≤_) where
open IsPartialOrder isPartialOrder
-- Less than all values in a list
data _≤*_ (x : A) : List A → Set (lmax a r) where
[] : x ≤* []
_∷_ : {y ys} (x ≤ y) x ≤* ys x ≤* (y ∷ ys)
-- Proof that a list is sorted
data IsSorted : List A → Set (lmax a r) where
[] : IsSorted []
_∷_ : {x xs} x ≤* xs IsSorted xs IsSorted (x ∷ xs)
trans* : {x u us} x ≤ u u ≤* us x ≤* us
trans* p [] = []
trans* p (y ∷ ys) = trans p y ∷ trans* p ys
-- relation to permutations
open Permutations A
less-insert : {x y xs ys} y ◂ ys ≡ xs x ≤* xs x ≤ y
less-insert here (l ∷ _) = l
less-insert (there p) (_ ∷ ls) = less-insert p ls
less-remove : {x y xs ys} y ◂ ys ≡ xs x ≤* xs x ≤* ys
less-remove here (l ∷ ls) = ls
less-remove (there p) (l ∷ ls) = l ∷ less-remove p ls
less-perm : {x xs ys} IsPermutation xs ys x ≤* ys x ≤* xs
less-perm [] [] = []
less-perm (p ∷ ps) ss = less-insert p ss ∷ less-perm ps (less-remove p ss)
-- alternative: insertion instead of selection
insert-less : {x y xs ys} y ◂ ys ≡ xs x ≤ y x ≤* ys x ≤* xs
insert-less here l ks = l ∷ ks
insert-less (there p) l (k ∷ ks) = k ∷ insert-less p l ks
less-perm' : {x xs ys} IsPermutation xs ys x ≤* xs x ≤* ys
less-perm' [] [] = []
less-perm' (p ∷ ps) (s ∷ ss) = insert-less p s (less-perm' ps ss)
less-++ : {x xs ys} x ≤* xs x ≤* ys x ≤* (xs ++ ys)
less-++ [] ys = ys
less-++ (x ∷ xs) ys = x ∷ less-++ xs ys
-- Sorted permutations of xs
data Sorted : List A → Set (lmax a r) where
[] : Sorted []
cons : x {xs xxs} (p : x ◂ xs ≡ xxs) (least : x ≤* xs) (rest : Sorted xs) Sorted xxs
-- Alternative:
record Sorted' (xs : List A) : Set (lmax a r) where
constructor sorted'
field
list : List A
isSorted : IsSorted list
isPerm : IsPermutation list xs
Sorted-to-Sorted' : {xs} Sorted xs Sorted' xs
Sorted-to-Sorted' [] = sorted' [] [] []
Sorted-to-Sorted' (cons x p l xs)
= sorted' (x ∷ list) (IsSorted._∷_ (less-perm isPerm l) isSorted) (p ∷ isPerm)
where open Sorted' (Sorted-to-Sorted' xs)
Sorted'-to-Sorted : {xs} Sorted' xs Sorted xs
Sorted'-to-Sorted (sorted' [] [] []) = []
Sorted'-to-Sorted (sorted' (x ∷ xs) (l ∷ ls) (p ∷ ps))
= cons x p (less-perm' ps l) (Sorted'-to-Sorted (sorted' xs ls ps))
-- Sorted lists are unique
Sorted-to-List : {xs} Sorted xs List A
Sorted-to-List [] = []
Sorted-to-List (cons x _ _ xs) = x ∷ Sorted-to-List xs
Sorted-unique' : {xs xs'} (IsPermutation xs xs') (ys : Sorted xs) (zs : Sorted xs')
Sorted-to-List ys ≡ Sorted-to-List zs
Sorted-unique' [] [] [] = PE.refl
Sorted-unique' [] (cons _ () _ _) _
Sorted-unique' [] _ (cons _ () _ _)
Sorted-unique' (() ∷ _) _ []
Sorted-unique' ps (cons y yp yl ys) (cons z zp zl zs) = PE.cong₂ _∷_ y=z (Sorted-unique' ps' ys zs)
where
y=z : y ≡ z
y=z = antisym (less-insert zp (less-perm' ps (insert-less yp refl yl)))
(less-insert yp (less-perm ps (insert-less zp refl zl)))
ps' = same-perm y=z ps yp zp
Sorted-unique : {xs} (ys zs : Sorted xs) Sorted-to-List ys ≡ Sorted-to-List zs
Sorted-unique = Sorted-unique' (id-permutation _)
-----------------------------------------------------------------------------------------
-- Logarithms
-----------------------------------------------------------------------------------------
module Nat where
open DecTotalOrder Data.Nat.decTotalOrder hiding (_≤_)
_^_ :
x ^ zero = 1
x ^ suc n = x * (x ^ n)
abstract
log-acc : n Acc _<′_ n
log-acc 0 _ = 0
log-acc (suc n) (acc more) = suc (log-acc ⌊ suc n /2⌋ (more _ (s≤′s (⌈n/2⌉≤′n n))))
-- 1 plus the floor of the base-2 logarithm,
-- taking log 0 = -1
log :
log n = log-acc n (<-well-founded n)
1+⌊log₂_⌋ :
1+⌊log₂_⌋ = log
⌊log₂_⌋ :
⌊log₂ n ⌋ = pred (log n)
⌈log₂_⌉ :
⌈log₂ n ⌉ = log (pred n)
-- Properties of /2
⌊/2⌋-monotonic : {m n : ℕ} m ≤ n ⌊ m /2⌋ ≤ ⌊ n /2
⌊/2⌋-monotonic z≤n = z≤n
⌊/2⌋-monotonic {1} {suc _} (s≤s m≤n) = z≤n
⌊/2⌋-monotonic {suc (suc m)} {suc zero} (s≤s ())
⌊/2⌋-monotonic {suc (suc m)} {suc (suc n)} (s≤s (s≤s m≤n)) = s≤s (⌊/2⌋-monotonic m≤n)
n/2*2 : (n : ℕ) ⌈ n /2⌉ + ⌊ n /2⌋ ≡ n
n/2*2 0 = PE.refl
n/2*2 1 = PE.refl
n/2*2 (suc (suc n)) = lem ⌈ n /2⌉ ⌊ n /2⌋ ⟨ PE.trans ⟩ PE.cong (suc ∘ suc) (n/2*2 n)
where
lem : a b (1 + a) + (1 + b) ≡ 2 + (a + b)
lem a b = PE.sym $ 1+m+n=m+1+n (suc a) b
-- solve 2 (\a b → (con 1 :+ a) :+ (con 1 :+ b) := con 2 :+ (a :+ b)) PE.refl
-- Properties of logarithms
log-suc : n log (suc n) ≡ suc (log ⌊ suc n /2⌋)
log-suc n = PE.cong (suc ∘ log-acc ⌊ suc n /2⌋) acc-irrelevance
log-suc' : {n} n > 0 log n ≡ suc (log ⌊ n /2⌋)
log-suc' {zero} ()
log-suc' {suc n} _ = log-suc n
log-monotonic' : {m n am an} m ≤ n log-acc m am ≤ log-acc n an
log-monotonic' {zero} {_} _ = z≤n
log-monotonic' {suc m} {zero} ()
log-monotonic' {suc m} {suc n} {am = acc am} {an = acc an} m≤n
= s≤s (log-monotonic' {am = am _ (s≤′s (⌈n/2⌉≤′n m))}
{an = an _ (s≤′s (⌈n/2⌉≤′n n))}
(⌊/2⌋-monotonic m≤n))
log-monotonic : {m n : ℕ} m ≤ n log m ≤ log n
log-monotonic = log-monotonic'
≤-+ : {a b c d} a ≤ b c ≤ d a + c ≤ b + d
≤-+ {b = b} z≤n c≤d = ≤-steps b c≤d
≤-+ (s≤s a≤b) c≤d = s≤s (≤-+ a≤b c≤d)
≤-* : {a b c d} a ≤ b c ≤ d a * c ≤ b * d
≤-* z≤n c≤d = z≤n
≤-* (s≤s a≤b) c≤d = ≤-+ c≤d (≤-* a≤b c≤d)
log-split : n-2 let n = 2 + n-2 in
⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ + ⌊ n /2⌋)) ≤ n * ⌈log₂ n ⌉
log-split n-2 = let n = 2 + n-2 in
begin
⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ + ⌊ n /2⌋))
≤⟨ ≤-+ (refl {⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉})
(≤-+ (≤-* (refl {⌊ n /2⌋})
(log-monotonic (⌊/2⌋-monotonic (n≤m+n 1 n-2))))
(refl {⌈ n /2⌉ + ⌊ n /2⌋})
) ⟩
⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌈ n /2⌉ + ⌊ n /2⌋))
≡⟨ solve 3 (\c f l c :* l :+ (f :* l :+ (c :+ f)) := (c :+ f) :* (con 1 :+ l))
PE.refl ⌈ n /2⌉ ⌊ n /2⌋ ⌈log₂ ⌈ n /2⌉ ⌉ ⟩
(⌈ n /2⌉ + ⌊ n /2⌋) * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
≡⟨ PE.cong (\nn nn * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)) (n/2*2 n) ⟩
n * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
≡⟨ PE.sym $ PE.cong (_*_ n) (log-suc n-2) ⟩
n * ⌈log₂ n ⌉
where
open ≤-Reasoning
open Nat
-----------------------------------------------------------------------------------------
-- Sorting algorithms
-----------------------------------------------------------------------------------------
module SortingAlgorithm
{A : Set}
{_≤_ : Rel A ℓ₀}
(isPartialOrder : IsPartialOrder _≡_ _≤_)
-- testing ordering can be done in 1 operation
(_≤?_ : (x y : A) → (xyyx) in-time 1) where
open Permutations A
open SortedList isPartialOrder
---------------------------------------------------------------------------
-- Insertion sort
---------------------------------------------------------------------------
-- Insertion sort, O(n^2)
insert : {xs} (x : A) Sorted xs Sorted (x ∷ xs) in-time (length xs)
insert x []
= return $ cons x here [] []
insert x (cons u p0 u≤*us us)
= bound-≡ (PE.sym (length-insert p0))
$ (x ≤? u) >>= λ
{ (inj₁ p) return $ cons x here (insert-less p0 p (trans* p u≤*us)) $ cons u p0 u≤*us us
; (inj₂ p) cons u (there p0) (p ∷ u≤*us) <$> insert x us
}
insertion-sort : (xs : List A) Sorted xs in-time length xs ^ 2
insertion-sort [] = return []
insertion-sort (x ∷ xs)
= bound-≡ (lem (length xs)) $
insertion-sort xs >>= insert x >>= return
where
lem : n (n ^ 2 + n) + (n + 1) ≡ (1 + n) ^ 2
lem = solve 1 (\n (n :^ 2 :+ n) :+ (n :+ con 1)
:= (con 1 :+ n) :^ 2) PE.refl
---------------------------------------------------------------------------
-- Selection sort
---------------------------------------------------------------------------
import Data.Vec as Vec
open Vec using (Vec;toList;fromList;_∷_;[])
-- select least element from a non-empty list x∷xs
select1 : {n} (xs : Vec A (suc n))
(∃₂ \y ys (y ◂ toList ys ≡ toList xs) × (y ≤* toList ys)) in-time n
select1 (x ∷ []) = return $ x , [] , here , []
select1 {suc n} (x ∷ xs)
= bound-≡ (lem n) $
select1 xs >>= \{ (z , zs , perm , least)
x ≤? z >>= \
{ (inj₁ p) return $ x , xs , here , insert-less perm p (trans* p least)
; (inj₂ p) return $ z , (x ∷ zs) , there perm , (p ∷ least)
}}
where
lem : n n + 11 + n
lem = solve 1 (\n n :+ con 1 := con 1 :+ n) PE.refl
selection-sort1 : {n} (xs : Vec A n) (Sorted (toList xs)) in-time (n ^ 2)
selection-sort1 [] = return []
selection-sort1 {suc n} xs
= bound-+ (lem n) $
select1 xs >>= \
{ (y , ys , perm , least)
cons y perm least <$> selection-sort1 ys }
where
lem : n n + (n ^ 2) + (n + 1) ≡ (1 + n) ^ 2
lem = solve 1 (\n n :+ (n :^ 2) :+ (n :+ con 1)
:= (con 1 :+ n) :^ 2) PE.refl
toList∘fromList : (xs : List A) toList (fromList xs) ≡ xs
toList∘fromList [] = PE.refl
toList∘fromList (x ∷ xs) = PE.cong (_∷_ x) (toList∘fromList xs)
selection-sort2 : (xs : List A) (Sorted xs) in-time (length xs ^ 2)
selection-sort2 xs = PE.subst Sorted (toList∘fromList xs)
<$> selection-sort1 (fromList xs)
---------------------------------------------------------------------------
-- Merge sort
---------------------------------------------------------------------------
xs++[]=xs : (xs : List A) xs ++ [] ≡ xs
xs++[]=xs [] = PE.refl
xs++[]=xs (x ∷ xs) = PE.cong (_∷_ x) (xs++[]=xs xs)
length∘toList : {n} (xs : Vec A n) length (toList xs) ≡ n
length∘toList [] = PE.refl
length∘toList (x ∷ xs) = PE.cong suc (length∘toList xs)
merge : {xs ys} Sorted xs Sorted ys (Sorted (xs ++ ys)) in-time (length xs + length ys)
merge [] sys = return sys
merge sxs [] = return $ PE.subst Sorted (PE.sym (xs++[]=xs _)) sxs
merge {xs = []} (cons _ () _ _) _
merge {ys = []} _ (cons _ () _ _)
merge {xs = x ∷ xs} {ys = yys} (cons u {xs = xus} up ul us) (cons v {xs = yvs} vp vl vs)
= go (cons u up ul us) (cons v vp vl vs) =<< (u ≤? v)
where
go : Sorted (x ∷ xs) Sorted yys
(u ≤ v) ⊎ (v ≤ u)
(Sorted (x ∷ xs ++ yys)) in-time (length xs + length yys)
go _ vss (inj₁ u≤v)
= bound-≡ (PE.cong (\l pred l + length (yys)) (PE.sym $ length-insert up))
$ merge us vss <$$>
cons u (insert-++₁ up) (less-++ ul (insert-less vp u≤v (trans* u≤v vl)))
go uus _ (inj₂ v≤u)
= bound-≡ (1+m+n=m+1+n (length xs) _ ⟨ PE.trans ⟩
PE.cong (\l length xs + l) (PE.sym $ length-insert vp))
$ merge uus vs <$$>
cons v (insert-++₂ {xs = x ∷ xs} vp) (less-++ (insert-less up v≤u (trans* v≤u ul)) vl)
splitAtVec : m {n m+n} (xs : Vec A m+n) m + n ≡ m+n
∃₂ \(ys : Vec A m) (zs : Vec A n) toList ys ++ toList zs ≡ toList xs
splitAtVec zero xs PE.refl = [] , xs , PE.refl
splitAtVec (suc m) [] ()
splitAtVec (suc m) (x ∷ xs) PE.refl with splitAtVec m xs PE.refl
... | us , vs , uvx = x ∷ us , vs , PE.cong (_∷_ x) uvx
splitHalf' : {n} (xs : Vec A n) ∃₂ \(ys : Vec A ⌈ n /2⌉) (zs : Vec A ⌊ n /2⌋) toList ys ++ toList zs ≡ toList xs
splitHalf' {n} xs = splitAtVec ⌈ n /2⌉ xs (n/2*2 n)
MergeSort : Set
MergeSort = \n (xs : Vec A n) (Sorted (toList xs)) in-time (n * ⌈log₂ n ⌉)
merge-sort' : n <-Rec MergeSort n MergeSort n
merge-sort' 0 rec [] = return $ []
merge-sort' 1 rec (x ∷ []) = return $ cons x here [] []
merge-sort' (suc (suc n)) rec xs with splitHalf' xs
... | xs₁ , xs₂ , ok
= bound-≤ (log-split n)
$ bound-≡ (PE.cong₂ (\x y 2 + n /2⌉ * ⌈log₂ ⌈ 2 + n /2⌉ ⌉ + (⌊ 2 + n /2⌋ * ⌈log₂ ⌊ 2 + n /2⌋ ⌉ + (x + y)))
(length∘toList xs₁)
(length∘toList xs₂))
$ rec _ (s≤′s $ s≤′s $ ⌈n/2⌉≤′n n) xs₁ >>= \sorted₁
rec _ (s≤′s $ s≤′s $ ⌊n/2⌋≤′n n) xs₂ >>= \sorted₂
PE.subst Sorted ok <$> merge sorted₁ sorted₂
merge-sort : xs (Sorted xs) in-time (length xs * ⌈log₂ length xs ⌉)
merge-sort xs = PE.subst Sorted (toList∘fromList xs)
<$> <-rec MergeSort merge-sort' (length xs) (fromList xs)
-----------------------------------------------------------------------------------------
-- Aside: standard library total orders are decidable
-----------------------------------------------------------------------------------------
total-decidable : {a r} {A : Set a}
(_≤_ : Rel A r)
IsTotalOrder _≡_ _≤_
IsDecTotalOrder _≡_ _≤_
total-decidable {A = A} _≤_ isTotalOrder = record
{ isTotalOrder = isTotalOrder
; _≟_ = _≟_
; _≤?_ = _≤?_
}
where
open IsTotalOrder isTotalOrder
open PE renaming ([_] to reveal)
inj₁≠inj₂ : {b c} {B : Set b} {C : Set c} {x : B} {y : C} inj₁ x ≢ inj₂ y
inj₁≠inj₂ ()
_≟_ : (x y : A) Dec (x ≡ y)
_≟_ x y with total x y | total y x | inspect (total x) y | inspect (total y) x
... | inj₁ x≤y | inj₁ y≤x | _ | _ = yes (antisym x≤y y≤x)
... | inj₂ y≤x | inj₂ x≤y | _ | _ = yes (antisym x≤y y≤x)
... | inj₁ _ | inj₂ _ | reveal a | reveal b
= no \x=y inj₁≠inj₂ (PE.trans (subst₂ (\x' y' _ ≡ total x' y') x=y (sym x=y) (sym a)) b)
... | inj₂ _ | inj₁ _ | reveal a | reveal b
= no \x=y inj₁≠inj₂ (PE.trans (subst₂ (\x' y' _ ≡ total x' y') (sym x=y) x=y (sym b)) a)
_≤?_ : (x y : A) Dec (x ≤ y)
_≤?_ x y with total x y | x ≟ y
... | inj₁ x≤y | _ = yes x≤y
... | inj₂ y≤x | yes x=y = yes (reflexive x=y)
... | inj₂ y≤x | no x≠y = no \x≤y x≠y (antisym x≤y y≤x)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.