Skip to content

Instantly share code, notes, and snippets.

@twanvl
Last active December 2, 2022 16:44
  • Star 25 You must be signed in to star a gist
  • Fork 2 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save twanvl/5635740 to your computer and use it in GitHub Desktop.
Correctness and runtime of mergesort, insertion sort and selection sort.
module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction
open import Data.Nat.Tactic.RingSolver
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming ([_] to reveal)
open import Function
-----------------------------------------------------------------------------------------
-- 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
unbox : ∀ {a} {A : Set a} {n} → A in-time n → A
unbox (box x) = x
open Dummy public using (_in-time_)
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-≡ = 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-+ (m+[n∸m]≡n 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 = solve-∀
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 = refl
length-insert (there p) = cong suc (length-insert p)
length-permutation : ∀ {xs ys} → IsPermutation xs ys → length xs ≡ length ys
length-permutation [] = refl
length-permutation (p ∷ ps) = cong suc (length-permutation ps) ⟨ trans ⟩ 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 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 renaming (trans to ≤-trans; refl to ≤-refl)
-- 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' [] [] [] = refl
Sorted-unique' [] (cons _ () _ _) _
Sorted-unique' [] _ (cons _ () _ _)
Sorted-unique' (() ∷ _) _ []
Sorted-unique' ps (cons y yp yl ys) (cons z zp zl zs) = 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
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⌉))
≤⟨ +-monoˡ-≤ (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
(*-monoʳ-≤ ⌊ n /2⌋
(⌈log₂⌉-mono-≤ (⌊n/2⌋≤⌈n/2⌉ n))) ⟩
⌊ n /2⌋ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
≡⟨ lem ⌊ n /2⌋ ⌈ n /2⌉ ⌈log₂ ⌈ n /2⌉ ⌉ ⟩
(⌊ n /2⌋ + ⌈ n /2⌉) * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
≡⟨ cong (\nn → nn * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)) (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
n * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
≡⟨ cong (\l → n * (1 + l)) (⌈log₂⌈n/2⌉⌉≡⌈log₂n⌉∸1 n) ⟩
n * ⌈log₂ n ⌉
where
open ≤-Reasoning
lem : ∀ a b c → a * c + (b * c + (a + b)) ≡ (a + b) * (1 + c)
lem = solve-∀
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-≡ (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 : ∀ n → (n * (n * 1) + n) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
lem = solve-∀
---------------------------------------------------------------------------
-- 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-∀
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
-- Note: ring solver reflection doesn't understand exponents
--lem : ∀ n → n + (n ^ 2) + (n + 1) ≡ (1 + n) ^ 2
lem : ∀ n → n + (n * (n * 1)) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
lem = solve-∀
toList∘fromList : ∀ (xs : List A) → toList (fromList xs) ≡ xs
toList∘fromList [] = refl
toList∘fromList (x ∷ xs) = cong (_∷_ x) (toList∘fromList xs)
selection-sort2 : ∀ (xs : List A) → (Sorted xs) in-time (length xs ^ 2)
selection-sort2 xs = subst Sorted (toList∘fromList xs)
<$> selection-sort1 (fromList xs)
---------------------------------------------------------------------------
-- Merge sort
---------------------------------------------------------------------------
xs++[]=xs : ∀ (xs : List A) → xs ++ [] ≡ xs
xs++[]=xs [] = refl
xs++[]=xs (x ∷ xs) = cong (_∷_ x) (xs++[]=xs xs)
length∘toList : ∀ {n} (xs : Vec A n) → length (toList xs) ≡ n
length∘toList [] = refl
length∘toList (x ∷ xs) = 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 $ subst Sorted (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-≡ (cong (\l → pred l + length (yys)) (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) _ ⟨ trans ⟩
cong (\l → length xs + l) (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 refl = [] , xs , refl
splitAtVec (suc m) [] ()
splitAtVec (suc m) (x ∷ xs) refl with splitAtVec m xs refl
... | us , vs , uvx = x ∷ us , vs , 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⌋+⌈n/2⌉≡n 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-≡ (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₂
→ subst Sorted ok <$> merge sorted₁ sorted₂
merge-sort : ∀ xs → (Sorted xs) in-time (length xs * ⌈log₂ length xs ⌉)
merge-sort xs = 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 using (reflexive; total; antisym)
_≟_ : (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 way
where
way : ¬ x ≡ y
way refl with trans (sym a) b
... | ()
... | inj₂ _ | inj₁ _ | reveal a | reveal b = no way
where
way : ¬ x ≡ y
way refl with trans (sym a) b
... | ()
_≤?_ : (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