From 2184a8f47f72a415e3387a9aaca042dd63c80fd9 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 18 Jul 2025 17:34:52 -0500 Subject: Sorted lists with the same elements are equal --- Data/Permutation/Sort.agda | 176 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 176 insertions(+) create mode 100644 Data/Permutation/Sort.agda (limited to 'Data/Permutation/Sort.agda') diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda new file mode 100644 index 0000000..977443a --- /dev/null +++ b/Data/Permutation/Sort.agda @@ -0,0 +1,176 @@ +{-# 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 + ; _≤_ ; _≤?_ + ; ≤-respˡ-≈ ; ≤-respʳ-≈ + ; antisym + ) + renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive) + +open import Data.Fin.Base using (Fin) +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) +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.Propositional using (_↭_; ↭-trans; ↭-sym) +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (↭-length) +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 Fin +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 + +apply : {xs ys : List A} {x : A} → xs ↭ ys → x ∈ xs → x ∈ ys +apply refl x-in-xs = x-in-xs +apply (prep x xs↭ys) (here px) = here px +apply (prep x xs↭ys) (there x-in-xs) = there (apply xs↭ys x-in-xs) +apply (swap x y xs↭ys) (here px) = there (here px) +apply (swap x y xs↭ys) (there (here px)) = here px +apply (swap x y xs↭ys) (there (there x-in-xs)) = there (there (apply xs↭ys x-in-xs)) +apply (trans xs↭ys ys↭zs) x-in-xs = apply ys↭zs (apply xs↭ys x-in-xs) + +↭-remove + : {xs ys : List A} + {x : A} + → (xs↭ys : xs ↭ ys) + → (x∈xs : x ∈ xs) + → let x∈ys = apply xs↭ys x∈xs in + remove xs x∈xs ↭ remove ys x∈ys +↭-remove refl x∈xs = refl +↭-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 (apply xs↭ys x∈xs)) + +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 = apply 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 + +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) -- cgit v1.2.3 From 21aa7526f51030be9ffd86be2eabd5d07f64b6f4 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 15 Oct 2025 13:31:13 -0500 Subject: Strengthen permutation sort theorem --- Data/Circuit/Convert.agda | 42 +++++++++++++++++--------------- Data/Hypergraph/Base.agda | 1 + Data/Hypergraph/Edge.agda | 14 +++++++---- Data/Permutation/Sort.agda | 60 ++++++++++++++++++++++++++++++---------------- 4 files changed, 73 insertions(+), 44 deletions(-) (limited to 'Data/Permutation/Sort.agda') diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda index 497b0cd..ce6de69 100644 --- a/Data/Circuit/Convert.agda +++ b/Data/Circuit/Convert.agda @@ -5,16 +5,24 @@ module Data.Circuit.Convert where open import Data.Nat.Base using (ℕ) open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate) open import Data.Fin.Base using (Fin) -open import Function.Bundles using (Equivalence) open import Data.Hypergraph.Edge GateLabel using (Edge) -open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph) +open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph) open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph) open import Data.Permutation using (fromList-↭; toList-↭) open import Data.List using (length) open import Data.Vec.Functional using (toVec; fromVec; toList; fromList) -open import Function.Base using (_∘_; id; _$_) - +open import Function.Bundles using (Equivalence; _↔_) +open import Function.Base using (_∘_; id) +open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation) +open import Data.Product.Base using (proj₁; proj₂; _×_) +open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +import Function.Reasoning as →-Reasoning +import Data.List.Relation.Binary.Permutation.Propositional as L +import Data.Vec.Functional.Relation.Binary.Permutation as V import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph + open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) to : {v : ℕ} → Hypergraph v → Hypergraph′ v @@ -37,9 +45,6 @@ from {v} H = record asEdge : Fin h → Edge v asEdge e = record { label = l e ; ports = toVec (j e) } -open import Data.Product.Base using (proj₁; proj₂) -open import Data.Fin.Permutation using (flip) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′) to-cong {v} {H} {H′} ≈H = record { ↔h = flip ρ @@ -49,8 +54,6 @@ to-cong {v} {H} {H′} ≈H = record } where open Edge using (arity; ports; label) - open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_) - open import Function.Bundles using (_↔_) open ≈-Hypergraph ≈H open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ) open import Data.Fin.Base using (cast) @@ -87,11 +90,9 @@ to-cong {v} {H} {H′} ≈H = record ≡.refl module _ {v : ℕ} where - open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge⇒≡) + open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡) open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭) open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋) - open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_) - open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_) open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map) open import Data.Product.Base using (_,_) open import Data.Hypergraph.Label using (HypergraphLabel) @@ -172,21 +173,24 @@ module _ {v : ℕ} where cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩ toVec (H′.j e) ∎ - H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e + H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e H∘ρ≗H′ e = ≈-Edge⇒≡ record { ≡arity = ≗a′ e ; ≡label = ≗l′ e ; ≡ports = ≗p′ e } + open Hypergraph using (edges) + open →-Reasoning ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′) ≡sorted = - ≡.cong (λ x → record { edges = x } ) $ - Pointwise-≡⇒≡ $ - map ≈-Edge⇒≡ $ - sorted-≋ $ - toList-↭ $ - flip ↔h , H∘ρ≗H′ + flip ↔h , H∘ρ≗H′ ∶ asEdge H V.↭ asEdge H′ + |> toList-↭ ∶ toList (asEdge H) L.↭ toList (asEdge H′) + |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′)) + |> sorted-≋ ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′))) + |> map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′))) + |> Pointwise-≡⇒≡ ∶ sort (edges (from H)) ≡ sort (edges (from H′)) + |> ≡.cong mkHypergraph ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′) equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v) equiv v = record diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda index 5cf5388..6988cf0 100644 --- a/Data/Hypergraph/Base.agda +++ b/Data/Hypergraph/Base.agda @@ -12,6 +12,7 @@ open import Data.String using (String; unlines) import Data.List.Sort as Sort record Hypergraph (v : ℕ) : Set where + constructor mkHypergraph field edges : List (Edge v) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index cbf61e6..13b9278 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -80,6 +80,14 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where module i≈j = ≈-Edge i≈j module j≈k = ≈-Edge j≈k +open import Relation.Binary using (IsEquivalence) +≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v}) +≈-Edge-IsEquivalence = record + { refl = ≈-Edge-refl + ; sym = ≈-Edge-sym + ; trans = ≈-Edge-trans + } + open HL using (_[_<_]) _<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ _<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v}) @@ -300,11 +308,7 @@ tri x y | tri> x≮y x≢y y ¬x Date: Wed, 15 Oct 2025 16:18:45 -0500 Subject: Replace proof with new stdlib property --- Data/Permutation/Sort.agda | 199 ++++----------------------------------------- 1 file changed, 16 insertions(+), 183 deletions(-) (limited to 'Data/Permutation/Sort.agda') 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 ∎ -- cgit v1.2.3