diff options
Diffstat (limited to 'Data/Permutation/Sort.agda')
| -rw-r--r-- | Data/Permutation/Sort.agda | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda new file mode 100644 index 0000000..8d097f2 --- /dev/null +++ b/Data/Permutation/Sort.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Bundles using (DecTotalOrder) + +module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where + +open DecTotalOrder dto using (module Eq; totalOrder) renaming (Carrier to A) + +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 = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys + where + 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 ∎ |