\begin{code} {-# OPTIONS --cubical --safe --postfix-projections #-} open import Relation.Binary open import Prelude hiding (tt) module Data.List.Sort {e} {E : Type e} {r} (totalOrder : TotalOrder E r) where open import Relation.Binary.Construct.LowerBound totalOrder open TotalOrder totalOrder renaming (refl to refl-≤) open TotalOrder lb-ord renaming (trans to ⌊trans⌋) using () open import Data.List open import Data.Unit.UniversePolymorphic as Poly using (tt) open import Data.List.Relation.Binary.Permutation open import Function.Isomorphism open import Data.Fin open import Data.List.Membership \end{code} %<*insert> \begin{code} insert : E → List E → List E insert x [] = x ∷ [] insert x (y ∷ xs) with x ≤? y ... | inl x≤y = x ∷ y ∷ xs ... | inr y≤x = y ∷ insert x xs \end{code} %</insert> %<*insertion-sort> \begin{code} sort : List E → List E sort [] = [] sort (x ∷ xs) = insert x (sort xs) \end{code} %</insertion-sort> \begin{code} private variable lb : ⌊∙⌋ Sorted-cons : E → (⌊∙⌋ → Type r) → ⌊∙⌋ → Type r Sorted-cons x xs lb = (lb ≤⌊ x ⌋) × xs ⌊ x ⌋ SortedFrom : ⌊∙⌋ → List E → Type r SortedFrom = flip (foldr Sorted-cons (const Poly.⊤)) Sorted : List E → Type r Sorted = SortedFrom ⌊⊥⌋ insert-sorts : ∀ x xs → lb ≤⌊ x ⌋ → SortedFrom lb xs → SortedFrom lb (insert x xs) insert-sorts x [] lb≤x Pxs = lb≤x , tt insert-sorts x (y ∷ xs) lb≤x (lb≤y , Sxs) with x ≤? y ... | inl x≤y = lb≤x , x≤y , Sxs ... | inr y≤x = lb≤y , insert-sorts x xs y≤x Sxs \end{code} %<*sort-sorts> \begin{code} sort-sorts : ∀ xs → Sorted (sort xs) \end{code} %</sort-sorts> \begin{code} sort-sorts [] = tt sort-sorts (x ∷ xs) = insert-sorts x (sort xs) tt (sort-sorts xs) insert-perm : ∀ x xs → insert x xs ↭ x ∷ xs insert-perm x [] = reflₚ insert-perm x (y ∷ xs) with x ≤? y ... | inl x≤y = consₚ x reflₚ ... | inr y≤x = consₚ y (insert-perm x xs) ⟨ transₚ ⟩ swapₚ y x xs \end{code} %<*sort-perm> \begin{code} sort-perm : ∀ xs → sort xs ↭ xs \end{code} %</sort-perm> \begin{code} sort-perm [] = reflₚ {xs = []} sort-perm (x ∷ xs) = insert-perm x (sort xs) ⟨ transₚ {xs = insert x (sort xs)} ⟩ consₚ x (sort-perm xs) ord-in : ∀ x xs → SortedFrom lb xs → x ∈ xs → lb ≤⌊ x ⌋ ord-in {lb = lb} x (x₁ ∷ xs) p (f0 , x∈xs) = subst (lb ≤⌊_⌋) x∈xs (p .fst) ord-in {lb} x (y ∷ xs) p (fs n , x∈xs) = ⌊trans⌋ {lb} (p .fst) (ord-in x xs (p .snd) (n , x∈xs)) perm-head : ∀ {lbˣ lbʸ} x xs y ys → SortedFrom lbˣ (x ∷ xs) → SortedFrom lbʸ (y ∷ ys) → (x ∷ xs ↭ y ∷ ys) → x ≡ y perm-head x xs y ys Sxs Sys xs⇔ys with xs⇔ys _ .inv (f0 , refl) ... | f0 , y∈xs = y∈xs ... | fs n , y∈xs with xs⇔ys _ .fun (f0 , refl) ... | f0 , x∈ys = sym x∈ys ... | fs m , x∈ys = antisym (ord-in y xs (Sxs .snd) (n , y∈xs)) (ord-in x ys (Sys .snd) (m , x∈ys)) perm-same : ∀ {lbˣ lbʸ} xs ys → SortedFrom lbˣ xs → SortedFrom lbʸ ys → xs ↭ ys → xs ≡ ys perm-same [] [] Sxs Sys xs⇔ys = refl perm-same [] (y ∷ ys) Sxs Sys xs⇔ys = ⊥-elim (xs⇔ys _ .inv (f0 , refl) .fst) perm-same (x ∷ xs) [] Sxs Sys xs⇔ys = ⊥-elim (xs⇔ys _ .fun (f0 , refl) .fst) perm-same {lbˣ} {lbʸ} (x ∷ xs) (y ∷ ys) Sxs Sys xs⇔ys = let h = perm-head {lbˣ} {lbʸ} x xs y ys Sxs Sys xs⇔ys in cong₂ _∷_ h (perm-same xs ys (Sxs .snd) (Sys .snd) (tailₚ x xs ys (subst (λ y′ → x ∷ xs ↭ y′ ∷ ys) (sym h) xs⇔ys))) \end{code} %<*sorted-perm-eq> \begin{code} sorted-perm-eq : ∀ xs ys → Sorted xs → Sorted ys → xs ↭ ys → xs ≡ ys \end{code} %</sorted-perm-eq> \begin{code} sorted-perm-eq = perm-same \end{code} %<*perm-invar> \begin{code} perm-invar : ∀ xs ys → xs ↭ ys → sort xs ≡ sort ys \end{code} %</perm-invar> \begin{code} perm-invar xs ys xs⇔ys = perm-same (sort xs) (sort ys) (sort-sorts xs) (sort-sorts ys) (λ k → sort-perm xs k ⟨ trans-⇔ ⟩ xs⇔ys k ⟨ trans-⇔ ⟩ sym-⇔ (sort-perm ys k)) \end{code}