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) → (x ≤ y ⊎ y ≤ x) 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 + 1 ≡ 1 + 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