diff options
| -rw-r--r-- | Data/Permutation/Sort.agda | 199 |
1 files changed, 16 insertions, 183 deletions
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda index 658997d..8d097f2 100644 --- a/Data/Permutation/Sort.agda +++ b/Data/Permutation/Sort.agda @@ -4,193 +4,26 @@ open import Relation.Binary.Bundles using (DecTotalOrder) module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where -open DecTotalOrder dto - using - ( _≈_ ; module Eq - ; totalOrder - ; _≤_ ; _≤?_ - ; ≤-respˡ-≈ ; ≤-respʳ-≈ - ; antisym - ) - renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive) +open DecTotalOrder dto using (module Eq; totalOrder) renaming (Carrier to A) -open import Data.Nat.Base using (ℕ) -open import Data.List.Base using (List; _++_; [_]) -open import Data.List.Membership.Setoid Eq.setoid using (_∈_) -open import Data.List.Relation.Binary.Pointwise using (module Pointwise) -open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans; ≋-length; Any-resp-≋) -open import Data.List.Relation.Unary.Linked using (Linked) -open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted) -open import Data.List.Relation.Binary.Permutation.Homogeneous using (map) -open import Data.List.Relation.Binary.Permutation.Propositional using () renaming (_↭_ to _↭′_) -open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; ↭-trans; ↭-sym; refl; prep; swap; trans; ↭-reflexive-≋) -open import Data.List.Relation.Binary.Permutation.Setoid.Properties Eq.setoid using (∈-resp-↭) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -open import Data.List.Relation.Binary.Permutation.Setoid.Properties (≡.setoid A) using (map⁺) -open import Data.List.Relation.Unary.Any using (Any) -open import Data.List.Sort dto using (sort; sort-↭; sort-↗) -open import Relation.Nullary.Decidable.Core using (yes; no) -open ℕ -open Any -open List -open Linked -open Pointwise - -insert : List A → A → List A -insert [] x = [ x ] -insert (x₀ ∷ xs) x with x ≤? x₀ -... | yes _ = x ∷ x₀ ∷ xs -... | no _ = x₀ ∷ insert xs x - -insert-resp-≋ : {xs ys : List A} (v : A) → xs ≋ ys → insert xs v ≋ insert ys v -insert-resp-≋ _ [] = ≋-refl -insert-resp-≋ {x ∷ xs} {y ∷ ys} v (x≈y ∷ xs≋ys) - with v ≤? x | v ≤? y -... | yes v≤x | yes v≤y = Eq.refl ∷ x≈y ∷ xs≋ys -... | yes v≤x | no v≰y with () ← v≰y (≤-respʳ-≈ x≈y v≤x) -... | no v≰x | yes v≤y with () ← v≰x (≤-respʳ-≈ (Eq.sym x≈y) v≤y) -... | no v≰x | no v≰y = x≈y ∷ insert-resp-≋ v xs≋ys - -remove : {x : A} (xs : List A) → x ∈ xs → List A -remove (_ ∷ xs) (here _) = xs -remove (x ∷ xs) (there elem) = x ∷ remove xs elem - -remove-sorted : {x : A} {xs : List A} → Sorted xs → (x∈xs : x ∈ xs) → Sorted (remove xs x∈xs) -remove-sorted [-] (here x≡x₀) = [] -remove-sorted (x₀≤x₁ ∷ s-xs) (here px) = s-xs -remove-sorted (x₀≤x₁ ∷ [-]) (there (here px)) = [-] -remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (here px)) = ≤-trans x₀≤x₁ x₁≤x₂ ∷ s-xs -remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (there x∈xs)) = x₀≤x₁ ∷ remove-sorted (x₁≤x₂ ∷ s-xs) (there x∈xs) - -head : {xs : List A} {x : A} → .(x ∈ xs) → A -head {x ∷ _} _ = x - -tail : {xs : List A} {x : A} → .(x ∈ xs) → List A -tail {_ ∷ xs} _ = xs - -head-≤ : {xs : List A} - {x : A} - → Sorted xs - → (x∈xs : x ∈ xs) - → head x∈xs ≤ x -head-≤ {x ∷ []} [-] (here px) = ≤-reflexive (Eq.sym px) -head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (here px) = ≤-reflexive (Eq.sym px) -head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (there x∈xs) = ≤-trans x₀≤x₁ (head-≤ s-xs x∈xs) - -remove-head - : {xs : List A} - {x : A} - → Sorted xs - → (x∈xs : x ∈ xs) - → x ≈ head x∈xs - → remove xs x∈xs ≋ tail x∈xs -remove-head _ (here _) _ = ≋-refl -remove-head {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) x≈x₀ = - x₀≈x₁ ∷ remove-head s-xs x∈xs x≈x₁ - where - x₀≈x₁ : x₀ ≈ x₁ - x₀≈x₁ = antisym x₀≤x₁ (≤-respʳ-≈ x≈x₀ (head-≤ s-xs x∈xs)) - x≈x₁ : x ≈ x₁ - x≈x₁ = Eq.trans x≈x₀ x₀≈x₁ - -insert-remove - : {xs : List A} - {x : A} - → (s-xs : Sorted xs) - → (x∈xs : x ∈ xs) - → insert (remove xs x∈xs) x ≋ xs -insert-remove [-] (here px) = px ∷ [] -insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (here px) with x ≤? x₁ -... | yes x≤x₁ = px ∷ ≋-refl -... | no x≰x₁ with () ← x≰x₁ (≤-respˡ-≈ (Eq.sym px) x₀≤x₁) -insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) with x ≤? x₀ -... | yes x≤x₀ = - antisym x≤x₀ (≤-trans x₀≤x₁ x₁≤x) ∷ - antisym x₀≤x₁ (≤-trans x₁≤x x≤x₀) ∷ - remove-head s-xs x∈xs (antisym (≤-trans x≤x₀ x₀≤x₁) (head-≤ s-xs x∈xs)) - where - x₁≤x : x₁ ≤ x - x₁≤x = head-≤ s-xs x∈xs -... | no x≰x₀ = Eq.refl ∷ insert-remove s-xs x∈xs - -open import Data.List.Base using (length) -open import Function.Base using (_∘_; flip; id) -open import Data.List.Relation.Binary.Permutation.Propositional using (↭⇒↭ₛ) - -∈-resp-≋ : {xs ys : List A} {x : A} → xs ≋ ys → x ∈ xs → x ∈ ys -∈-resp-≋ = Any-resp-≋ (flip Eq.trans) - -≋-remove - : {xs ys : List A} - {x : A} - → (xs≋ys : xs ≋ ys) - → (x∈xs : x ∈ xs) - → let x∈ys = ∈-resp-≋ xs≋ys x∈xs in - remove xs x∈xs ≋ remove ys x∈ys -≋-remove (x≈y ∷ xs≋ys) (here px) = xs≋ys -≋-remove (x≈y ∷ xs≋ys) (there x∈xs) = x≈y ∷ ≋-remove xs≋ys x∈xs - -↭-remove - : {xs ys : List A} - {x : A} - → (xs↭ys : xs ↭ ys) - → (x∈xs : x ∈ xs) - → let x∈ys = ∈-resp-↭ xs↭ys x∈xs in - remove xs x∈xs ↭ remove ys x∈ys -↭-remove (refl xs≋ys) x∈xs = ↭-reflexive-≋ (≋-remove xs≋ys x∈xs) -↭-remove (prep x xs↭ys) (here px) = xs↭ys -↭-remove (prep x xs↭ys) (there x∈xs) = prep x (↭-remove xs↭ys x∈xs) -↭-remove (swap x y xs↭ys) (here px) = prep y xs↭ys -↭-remove (swap x y xs↭ys) (there (here px)) = prep x xs↭ys -↭-remove (swap x y xs↭ys) (there (there x∈xs)) = swap x y (↭-remove xs↭ys x∈xs) -↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (∈-resp-↭ xs↭ys x∈xs)) - -↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys -↭-length (refl xs≋ys) = ≋-length xs≋ys -↭-length (prep x lr) = ≡.cong suc (↭-length lr) -↭-length (swap x y lr) = ≡.cong (suc ∘ suc) (↭-length lr) -↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂) - -sorted-unique - : {xs ys : List A} - → xs ↭ ys - → Sorted xs - → Sorted ys - → xs ≋ ys -sorted-unique {[]} {ys} xs↭ys s-xs s-ys with .(↭-length xs↭ys) -sorted-unique {[]} {[]} xs↭ys s-xs s-ys | _ = [] -sorted-unique xs@{x ∷ xs′} {ys} xs↭ys s-xs s-ys = ≋-trans ≋xs (≋-trans xs≋ys″ ≋ys) - where - x∈xs : x ∈ xs - x∈xs = here Eq.refl - x∈ys : x ∈ ys - x∈ys = ∈-resp-↭ xs↭ys x∈xs - s-xs′ : Sorted (remove xs x∈xs) - s-xs′ = remove-sorted s-xs x∈xs - s-ys′ : Sorted (remove ys x∈ys) - s-ys′ = remove-sorted s-ys x∈ys - xs↭ys′ : remove xs x∈xs ↭ remove ys x∈ys - xs↭ys′ = ↭-remove xs↭ys x∈xs - xs≋ys′ : remove xs x∈xs ≋ remove ys x∈ys - xs≋ys′ = sorted-unique {xs′} xs↭ys′ s-xs′ s-ys′ - xs≋ys″ : insert (remove xs x∈xs) x ≋ insert (remove ys x∈ys) x - xs≋ys″ = insert-resp-≋ x xs≋ys′ - ≋xs : xs ≋ insert (remove xs x∈xs) x - ≋xs = ≋-sym (insert-remove s-xs x∈xs) - ≋ys : insert (remove ys x∈ys) x ≋ ys - ≋ys = insert-remove s-ys x∈ys +open import Data.List.Base using (List) +open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_) +open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; module PermutationReasoning) +open import Data.List.Relation.Unary.Sorted.TotalOrder.Properties using (↗↭↗⇒≋) +open import Data.List.Sort dto using (sortingAlgorithm) +open import Data.List.Sort.Base totalOrder using (SortingAlgorithm) +open SortingAlgorithm sortingAlgorithm using (sort; sort-↭ₛ; sort-↗) sorted-≋ : {xs ys : List A} → xs ↭ ys → sort xs ≋ sort ys -sorted-≋ {xs} {ys} xs↭ys = - sorted-unique - (↭-trans - (⇒↭ (sort-↭ xs)) - (↭-trans xs↭ys (↭-sym (⇒↭ (sort-↭ ys))))) - (sort-↗ xs) - (sort-↗ ys) +sorted-≋ {xs} {ys} xs↭ys = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys where - ⇒↭ : {xs ys : List A} → xs ↭′ ys → xs ↭ ys - ⇒↭ = map Eq.reflexive ∘ ↭⇒↭ₛ + open PermutationReasoning + sort-xs↭sort-ys : sort xs ↭ sort ys + sort-xs↭sort-ys = begin + sort xs ↭⟨ sort-↭ₛ xs ⟩ + xs ↭⟨ xs↭ys ⟩ + ys ↭⟨ sort-↭ₛ ys ⟨ + sort ys ∎ |