diff --git a/CHANGELOG.md b/CHANGELOG.md index bbc65af5d7..07a7499a30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,6 +30,15 @@ Non-backwards compatible changes Other major improvements ------------------------ +* Module `Data.List.Relation.Binary.Permutation.Homogeneous` has + been comprehensively refactored, introducing + ```agda + Data.List.Relation.Binary.Permutation.Homogeneous.Properties + Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core + ``` + which then re-export to `Data.List.Relation.Binary.Permutation.Setoid.Properties` + and `Data.List.Relation.Binary.Permutation.Propositional.Properties` + Deprecated modules ------------------ diff --git a/doc/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda index e9141d89c7..5a640b4a7b 100644 --- a/doc/README/Data/List/Relation/Binary/Permutation.agda +++ b/doc/README/Data/List/Relation/Binary/Permutation.agda @@ -26,18 +26,18 @@ open import Relation.Binary.PropositionalEquality open import Data.List.Relation.Binary.Permutation.Propositional -- The permutation relation is written as `_↭_` and has four --- constructors. The first `refl` says that a list is always --- a permutation of itself, the second `prep` says that if the +-- *smart* constructors. The first `↭-refl` says that a list is +-- a permutation of itself, the second `↭-prep` says that if the -- heads of the lists are the same they can be skipped, the third --- `swap` says that the first two elements of the lists can be --- swapped and the fourth `trans` says that permutation proofs +-- `↭-swap` says that the first two elements of the lists can be +-- swapped and the fourth `↭-trans` says that permutation proofs -- can be chained transitively. -- For example a proof that two lists are a permutation of one -- another can be written as follows: lem₁ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ [] -lem₁ = trans (prep 1 (swap 2 3 refl)) (swap 1 3 refl) +lem₁ = ↭-trans (↭-prep 1 (↭-swap 2 3 ↭-refl)) (↭-swap 1 3 ↭-refl) -- In practice it is difficult to parse the constructors in the -- proof above and hence understand why it holds. The @@ -48,10 +48,21 @@ open PermutationReasoning lem₂ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ [] lem₂ = begin - 1 ∷ 2 ∷ 3 ∷ [] ↭⟨ prep 1 (swap 2 3 refl) ⟩ - 1 ∷ 3 ∷ 2 ∷ [] ↭⟨ swap 1 3 refl ⟩ + 1 ∷ 2 ∷ 3 ∷ [] ↭⟨ ↭-prep 1 (↭-swap 2 3 ↭-refl) ⟩ + 1 ∷ 3 ∷ 2 ∷ [] ↭⟨ ↭-swap 1 3 ↭-refl ⟩ 3 ∷ 1 ∷ 2 ∷ [] ∎ +-- In practice it is further useful to extend `PermutationReasoning` +-- with specialised combinators `<⟨_⟩` and `<<⟨_⟩` to support the +-- distinguished use of the `↭-prep ` and `↭-swap` steps, allowing +-- the above proof to be recast in the following form: + +lem₂ᵣ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ [] +lem₂ᵣ = begin + 1 ∷ (2 ∷ (3 ∷ [])) <⟨ ↭-swap 2 3 ↭-refl ⟩ + 1 ∷ 3 ∷ (2 ∷ []) <<⟨ ↭-refl ⟩ + 3 ∷ 1 ∷ (2 ∷ []) ∎ + -- As might be expected, properties of the permutation relation may be -- found in: diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 389721d4c5..40964d151e 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -22,7 +22,6 @@ open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Membership.Propositional.Properties open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-preorder) -open import Data.List.Relation.Binary.Permutation.Propositional open import Data.List.Relation.Binary.Permutation.Propositional.Properties open import Data.Product.Base as Prod hiding (map) import Data.Product.Function.Dependent.Propositional as Σ @@ -31,7 +30,7 @@ open import Data.Sum.Properties hiding (map-cong) open import Data.Sum.Function.Propositional using (_⊎-cong_) open import Data.Unit.Polymorphic.Base open import Function.Base -open import Function.Bundles using (_↔_; Inverse; Equivalence; mk↔ₛ′; mk⇔) +open import Function.Bundles using (_↔_; Inverse; Equivalence; mk↔ₛ′; mk↔; mk⇔) open import Function.Related.Propositional as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym) open import Function.Related.TypeIsomorphisms @@ -538,25 +537,32 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = lemma : ∀ {xs ys} (inv : x ∷ xs ∼[ bag ] x ∷ ys) {z} → Well-behaved (Inverse.to (∼→⊎↔⊎ inv {z})) - lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with - zero ≡⟨⟩ - index-of {xs = x ∷ xs} (here p) ≡⟨⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p) ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ ≡.sym $ - to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q)) ≡⟨ ≡.cong index-of $ - strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩ - index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q) ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩ - index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p) ≡⟨ ≡.cong index-of $ ≡.sym $ - strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p)) ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ - to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs) ≡⟨⟩ - index-of {xs = x ∷ xs} (there z∈xs) ≡⟨⟩ - suc (index-of {xs = xs} z∈xs) ∎ + lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ = case contra of λ () where open Inverse open ≡-Reasoning - ... | () + contra : zero ≡ suc (index-of {xs = xs} z∈xs) + contra = begin + zero + ≡⟨⟩ + index-of {xs = x ∷ xs} (here p) + ≡⟨⟩ + index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p) + ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟨ + index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q)) + ≡⟨ ≡.cong index-of $ strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩ + index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q) + ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩ + index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p) + ≡⟨ ≡.cong index-of $ strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟨ + index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p)) + ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩ + index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs) + ≡⟨⟩ + index-of {xs = x ∷ xs} (there z∈xs) + ≡⟨⟩ + suc (index-of {xs = xs} z∈xs) + ∎ ------------------------------------------------------------------------ -- Relationships to other relations @@ -564,36 +570,27 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ↭⇒∼bag : _↭_ {A = A} ⇒ _∼[ bag ]_ ↭⇒∼bag {A = A} xs↭ys {v} = mk↔ₛ′ (to xs↭ys) (from xs↭ys) (to∘from xs↭ys) (from∘to xs↭ys) where - to : ∀ {xs ys} → xs ↭ ys → v ∈ xs → v ∈ ys - to xs↭ys = Any-resp-↭ {A = A} xs↭ys - - from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs - from xs↭ys = Any-resp-↭ (↭-sym xs↭ys) - - from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q - from∘to refl v∈xs = refl - from∘to (prep _ _) (here refl) = refl - from∘to (prep _ p) (there v∈xs) = ≡.cong there (from∘to p v∈xs) - from∘to (swap x y p) (here refl) = refl - from∘to (swap x y p) (there (here refl)) = refl - from∘to (swap x y p) (there (there v∈xs)) = ≡.cong (there ∘ there) (from∘to p v∈xs) - from∘to (trans p₁ p₂) v∈xs - rewrite from∘to p₂ (Any-resp-↭ p₁ v∈xs) - | from∘to p₁ v∈xs = refl - - to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q - to∘from p with from∘to (↭-sym p) - ... | res rewrite ↭-sym-involutive p = res + + to : xs ↭ ys → v ∈ xs → v ∈ ys + to = ∈-resp-↭ + + from : xs ↭ ys → v ∈ ys → v ∈ xs + from = ∈-resp-↭ ∘ ↭-sym + + from∘to : (p : xs ↭ ys) (ix : v ∈ xs) → from p (to p ix) ≡ ix + from∘to p _ = ∈-resp-↭-sym p + + to∘from : (p : xs ↭ ys) (iy : v ∈ ys) → to p (from p iy) ≡ iy + to∘from p _ = ∈-resp-↭-sym⁻¹ p ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A} -∼bag⇒↭ {A = A} {[]} eq with empty-unique (↔-sym eq) -... | refl = refl -∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) -... | zs₁ , zs₂ , p rewrite p = begin - x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ - x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ - x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨ - zs₁ ++ x ∷ zs₂ ∎ +∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = ↭-refl +∼bag⇒↭ {A = A} {x ∷ xs} eq + with zs₁ , zs₂ , refl ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) = begin + x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ + x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ + x ∷ (zs₁ ++ zs₂) ↭⟨ ↭-shift zs₁ ⟨ + zs₁ ++ x ∷ zs₂ ∎ where open CommutativeMonoid (commutativeMonoid bag A) open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Equality/Propositional.agda b/src/Data/List/Relation/Binary/Equality/Propositional.agda index ffae515086..553348a920 100644 --- a/src/Data/List/Relation/Binary/Equality/Propositional.agda +++ b/src/Data/List/Relation/Binary/Equality/Propositional.agda @@ -14,7 +14,7 @@ open import Relation.Binary.Core using (_⇒_) module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where -open import Data.List.Base +import Data.List.Base as List import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) import Relation.Binary.PropositionalEquality.Properties as ≡ @@ -29,7 +29,7 @@ open SetoidEquality (≡.setoid A) public ≋⇒≡ : _≋_ ⇒ _≡_ ≋⇒≡ [] = refl -≋⇒≡ (refl ∷ xs≈ys) = cong (_ ∷_) (≋⇒≡ xs≈ys) +≋⇒≡ (refl ∷ xs≈ys) = cong (_ List.∷_) (≋⇒≡ xs≈ys) ≡⇒≋ : _≡_ ⇒ _≋_ ≡⇒≋ refl = ≋-refl diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda index 12015b3076..ee331d82cb 100644 --- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda +++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda @@ -8,54 +8,59 @@ module Data.List.Relation.Binary.Permutation.Homogeneous where -open import Data.List.Base using (List; _∷_) -open import Data.List.Relation.Binary.Pointwise.Base as Pointwise - using (Pointwise) -open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise - using (symmetric) +open import Data.List.Base as List using (List; []; _∷_) +open import Data.List.Relation.Binary.Pointwise as Pointwise + using (Pointwise; []; _∷_) +open import Data.Nat.Base using (ℕ; suc; _+_; _<_) open import Level using (Level; _⊔_) open import Relation.Binary.Core using (Rel; _⇒_) -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Structures using (IsEquivalence) -open import Relation.Binary.Definitions using (Reflexive; Symmetric) private variable a r s : Level A : Set a + xs ys zs : List A + x y x′ y′ : A -data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where - refl : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys - prep : ∀ {xs ys x y} (eq : R x y) → Permutation R xs ys → Permutation R (x ∷ xs) (y ∷ ys) - swap : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys) - trans : ∀ {xs ys zs} → Permutation R xs ys → Permutation R ys zs → Permutation R xs zs ------------------------------------------------------------------------ --- The Permutation relation is an equivalence - -module _ {R : Rel A r} where - - sym : Symmetric R → Symmetric (Permutation R) - sym R-sym (refl xs∼ys) = refl (Pointwise.symmetric R-sym xs∼ys) - sym R-sym (prep x∼x′ xs↭ys) = prep (R-sym x∼x′) (sym R-sym xs↭ys) - sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys) - sym R-sym (trans xs↭ys ys↭zs) = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys) - - isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R) - isEquivalence R-refl R-sym = record - { refl = refl (Pointwise.refl R-refl) - ; sym = sym R-sym - ; trans = trans - } - - setoid : Reflexive R → Symmetric R → Setoid _ _ - setoid R-refl R-sym = record - { isEquivalence = isEquivalence R-refl R-sym - } - -map : ∀ {R : Rel A r} {S : Rel A s} → - (R ⇒ S) → (Permutation R ⇒ Permutation S) -map R⇒S (refl xs∼ys) = refl (Pointwise.map R⇒S xs∼ys) -map R⇒S (prep e xs∼ys) = prep (R⇒S e) (map R⇒S xs∼ys) -map R⇒S (swap e₁ e₂ xs∼ys) = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys) -map R⇒S (trans xs∼ys ys∼zs) = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs) +-- Definition + +module _ {A : Set a} (R : Rel A r) where + + data Permutation : Rel (List A) (a ⊔ r) where + refl : Pointwise R xs ys → Permutation xs ys + prep : (eq : R x y) → Permutation xs ys → Permutation (x ∷ xs) (y ∷ ys) + swap : (eq₁ : R x x′) (eq₂ : R y y′) → Permutation xs ys → + Permutation (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys) + trans : Permutation xs ys → Permutation ys zs → Permutation xs zs + +------------------------------------------------------------------------ +-- Map + +module _ {R : Rel A r} {S : Rel A s} where + + map : (R ⇒ S) → (Permutation R ⇒ Permutation S) + map R⇒S (refl xs∼ys) = refl (Pointwise.map R⇒S xs∼ys) + map R⇒S (prep e xs∼ys) = prep (R⇒S e) (map R⇒S xs∼ys) + map R⇒S (swap e₁ e₂ xs∼ys) = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys) + map R⇒S (trans xs∼ys ys∼zs) = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +steps : {R : Rel A r} → Permutation R xs ys → ℕ +steps (refl _) = 1 +steps (prep _ xs↭ys) = suc (steps xs↭ys) +steps (swap _ _ xs↭ys) = suc (steps xs↭ys) +steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs + +{-# WARNING_ON_USAGE steps +"Warning: steps was deprecated in v2.1." +#-} diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda new file mode 100644 index 0000000000..43cada1872 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties.agda @@ -0,0 +1,322 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the `Homogeneous` definition of permutation +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} +{-# OPTIONS --warn=noUserWarning #-} -- for deprecated function `steps` + +module Data.List.Relation.Binary.Permutation.Homogeneous.Properties where + +open import Algebra.Bundles using (CommutativeMonoid) +open import Data.List.Base as List using (List; []; _∷_; [_]; _++_; length) +open import Data.List.Relation.Binary.Pointwise as Pointwise + using (Pointwise; []; _∷_) +open import Data.List.Relation.Unary.All as All using (All; []; _∷_) +open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) +open import Data.List.Relation.Unary.Any as Any using (Any; here; there) +import Data.List.Relation.Unary.Any.Properties as Any +open import Data.Nat.Base using (ℕ; suc; _+_; _<_) +import Data.Nat.Properties as ℕ +open import Data.Product.Base using (_,_; _×_; ∃) +open import Function.Base using (_∘_; flip) +open import Level using (Level; _⊔_) +open import Relation.Binary.Core using (Rel; _Preserves_⟶_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Definitions + using ( Reflexive; Symmetric; Transitive + ; _Respects_; _Respects₂_; _Respectsˡ_; _Respectsʳ_) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_ ; cong; cong₂) +open import Relation.Nullary.Decidable using (yes; no; does) +open import Relation.Nullary.Negation using (¬_; contradiction) +open import Relation.Unary using (Pred; Decidable) + +open import Data.List.Relation.Binary.Permutation.Homogeneous +import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Properties + +private + variable + a p r s : Level + A B : Set a + xs ys zs : List A + x y z v w : A + P : Pred A p + R : Rel A r + S : Rel A s + +------------------------------------------------------------------------ +-- Re-export `Core` properties +------------------------------------------------------------------------ + +open Properties public + +------------------------------------------------------------------------ +-- Inversion principles +------------------------------------------------------------------------ + + +↭-[]-invˡ : Permutation R [] xs → xs ≡ [] +↭-[]-invˡ (refl []) = ≡.refl +↭-[]-invˡ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invˡ xs↭ys = ↭-[]-invˡ ys↭zs + +↭-[]-invʳ : Permutation R xs [] → xs ≡ [] +↭-[]-invʳ (refl []) = ≡.refl +↭-[]-invʳ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invʳ ys↭zs = ↭-[]-invʳ xs↭ys + +¬x∷xs↭[]ˡ : ¬ (Permutation R [] (x ∷ xs)) +¬x∷xs↭[]ˡ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invˡ xs↭ys = ¬x∷xs↭[]ˡ ys↭zs + +¬x∷xs↭[]ʳ : ¬ (Permutation R (x ∷ xs) []) +¬x∷xs↭[]ʳ (trans xs↭ys ys↭zs) with ≡.refl ← ↭-[]-invʳ ys↭zs = ¬x∷xs↭[]ʳ xs↭ys + +module _ (R-trans : Transitive R) where + + ↭-singleton-invˡ : Permutation R [ x ] xs → ∃ λ y → xs ≡ [ y ] × R x y + ↭-singleton-invˡ (refl (xRy ∷ [])) = _ , ≡.refl , xRy + ↭-singleton-invˡ (prep xRy p) + with ≡.refl ← ↭-[]-invˡ p = _ , ≡.refl , xRy + ↭-singleton-invˡ (trans r s) + with _ , ≡.refl , xRy ← ↭-singleton-invˡ r + with _ , ≡.refl , yRz ← ↭-singleton-invˡ s + = _ , ≡.refl , R-trans xRy yRz + + ↭-singleton-invʳ : Permutation R xs [ x ] → ∃ λ y → xs ≡ [ y ] × R y x + ↭-singleton-invʳ (refl (yRx ∷ [])) = _ , ≡.refl , yRx + ↭-singleton-invʳ (prep yRx p) + with ≡.refl ← ↭-[]-invʳ p = _ , ≡.refl , yRx + ↭-singleton-invʳ (trans r s) + with _ , ≡.refl , yRx ← ↭-singleton-invʳ s + with _ , ≡.refl , zRy ← ↭-singleton-invʳ r + = _ , ≡.refl , R-trans zRy yRx + + +------------------------------------------------------------------------ +-- Properties of List functions, possibly depending on properties of R +------------------------------------------------------------------------ + +-- length + +↭-length : Permutation R xs ys → length xs ≡ length ys +↭-length (refl xs≋ys) = Pointwise.Pointwise-length xs≋ys +↭-length (prep _ xs↭ys) = cong suc (↭-length xs↭ys) +↭-length (swap _ _ xs↭ys) = cong (suc ∘ suc) (↭-length xs↭ys) +↭-length (trans xs↭ys ys↭zs) = ≡.trans (↭-length xs↭ys) (↭-length ys↭zs) + +-- map + +module _ {f} (pres : f Preserves R ⟶ S) where + + map⁺ : Permutation R xs ys → Permutation S (List.map f xs) (List.map f ys) + + map⁺ (refl xs≋ys) = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys)) + map⁺ (prep x xs↭ys) = prep (pres x) (map⁺ xs↭ys) + map⁺ (swap x y xs↭ys) = swap (pres x) (pres y) (map⁺ xs↭ys) + map⁺ (trans xs↭ys ys↭zs) = trans (map⁺ xs↭ys) (map⁺ ys↭zs) + + +-- _++_ + +module _ (R-refl : Reflexive R) where + + ++⁺ʳ : ∀ zs → Permutation R xs ys → + Permutation R (xs List.++ zs) (ys List.++ zs) + ++⁺ʳ zs (refl xs≋ys) = refl (Pointwise.++⁺ xs≋ys (Pointwise.refl R-refl)) + ++⁺ʳ zs (prep x xs↭ys) = prep x (++⁺ʳ zs xs↭ys) + ++⁺ʳ zs (swap x y xs↭ys) = swap x y (++⁺ʳ zs xs↭ys) + ++⁺ʳ zs (trans xs↭ys ys↭zs) = trans (++⁺ʳ zs xs↭ys) (++⁺ʳ zs ys↭zs) + + +-- filter + +module _ (R-sym : Symmetric R) + (P? : Decidable P) (P≈ : P Respects R) where + + filter⁺ : Permutation R xs ys → + Permutation R (List.filter P? xs) (List.filter P? ys) + filter⁺ (refl xs≋ys) = refl (Pointwise.filter⁺ P? P? P≈ (P≈ ∘ R-sym) xs≋ys) + filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys) + filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y + ... | yes _ | yes _ = prep x≈y (filter⁺ xs↭ys) + ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py + ... | no ¬Px | yes Py = contradiction (P≈ (R-sym x≈y) Py) ¬Px + ... | no _ | no _ = filter⁺ xs↭ys + filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y + filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py + with P? z | P? w + ... | _ | yes Pw = contradiction (P≈ w≈y Pw) ¬Py + ... | yes Pz | _ = contradiction (P≈ (R-sym x≈z) Pz) ¬Px + ... | no _ | no _ = filter⁺ xs↭ys + filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py + with P? z | P? w + ... | _ | no ¬Pw = contradiction (P≈ (R-sym w≈y) Py) ¬Pw + ... | yes Pz | _ = contradiction (P≈ (R-sym x≈z) Pz) ¬Px + ... | no _ | yes _ = prep w≈y (filter⁺ xs↭ys) + filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | no ¬Py + with P? z | P? w + ... | no ¬Pz | _ = contradiction (P≈ x≈z Px) ¬Pz + ... | _ | yes Pw = contradiction (P≈ w≈y Pw) ¬Py + ... | yes _ | no _ = prep x≈z (filter⁺ xs↭ys) + filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py + with P? z | P? w + ... | no ¬Pz | _ = contradiction (P≈ x≈z Px) ¬Pz + ... | _ | no ¬Pw = contradiction (P≈ (R-sym w≈y) Py) ¬Pw + ... | yes _ | yes _ = swap x≈z w≈y (filter⁺ xs↭ys) + + +------------------------------------------------------------------------ +-- foldr over a Commutative Monoid + +module _ (commutativeMonoid : CommutativeMonoid a r) where + + private + foldr = List.foldr + open module CM = CommutativeMonoid commutativeMonoid + + foldr-commMonoid : Permutation _≈_ xs ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys + foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys + foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) + foldr-commMonoid (swap {x} {x′} {y} {y′} {xs} {ys} x≈x′ y≈y′ xs↭ys) = begin + x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ + (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ + (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ + y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎ + where open ≈-Reasoning CM.setoid + foldr-commMonoid (trans xs↭ys ys↭zs) = + CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) + + +------------------------------------------------------------------------ +-- Relationships to other predicates +------------------------------------------------------------------------ + +-- All and Any + +module _ (resp : P Respects R) where + + All-resp-↭ : (All P) Respects (Permutation R) + All-resp-↭ (refl xs≋ys) pxs = Pointwise.All-resp-Pointwise resp xs≋ys pxs + All-resp-↭ (prep x≈y p) (px ∷ pxs) = resp x≈y px ∷ All-resp-↭ p pxs + All-resp-↭ (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ p pxs + All-resp-↭ (trans p₁ p₂) pxs = All-resp-↭ p₂ (All-resp-↭ p₁ pxs) + + Any-resp-↭ : (Any P) Respects (Permutation R) + Any-resp-↭ (refl xs≋ys) pxs = Pointwise.Any-resp-Pointwise resp xs≋ys pxs + Any-resp-↭ (prep x≈y p) (here px) = here (resp x≈y px) + Any-resp-↭ (prep x≈y p) (there pxs) = there (Any-resp-↭ p pxs) + Any-resp-↭ (swap ≈₁ ≈₂ p) (here px) = there (here (resp ≈₁ px)) + Any-resp-↭ (swap ≈₁ ≈₂ p) (there (here px)) = here (resp ≈₂ px) + Any-resp-↭ (swap ≈₁ ≈₂ p) (there (there pxs)) = there (there (Any-resp-↭ p pxs)) + Any-resp-↭ (trans p₁ p₂) pxs = Any-resp-↭ p₂ (Any-resp-↭ p₁ pxs) + +-- Membership + +module _ {_≈_ : Rel A r} (≈-trans : Transitive _≈_) where + + private + ∈-resp : ∀ {x} → (x ≈_) Respects _≈_ + ∈-resp = flip ≈-trans + + ∈-resp-Pointwise : (Any (x ≈_)) Respects (Pointwise _≈_) + ∈-resp-Pointwise = Pointwise.Any-resp-Pointwise ∈-resp + + ∈-resp-↭ : (Any (x ≈_)) Respects (Permutation _≈_) + ∈-resp-↭ = Any-resp-↭ ∈-resp + +-- AllPairs + +module _ (sym : Symmetric S) (resp@(rʳ , rˡ) : S Respects₂ R) where + + AllPairs-resp-↭ : (AllPairs S) Respects (Permutation R) + AllPairs-resp-↭ (refl xs≋ys) pxs = + Pointwise.AllPairs-resp-Pointwise resp xs≋ys pxs + AllPairs-resp-↭ (prep x≈y p) (∼ ∷ pxs) = + All-resp-↭ rʳ p (All.map (rˡ x≈y) ∼) ∷ AllPairs-resp-↭ p pxs + AllPairs-resp-↭ (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) = + (sym (rʳ eq₂ (rˡ eq₁ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷ + All-resp-↭ rʳ p (All.map (rˡ eq₁) ∼₂) ∷ AllPairs-resp-↭ p pxs + AllPairs-resp-↭ (trans p₁ p₂) pxs = + AllPairs-resp-↭ p₂ (AllPairs-resp-↭ p₁ pxs) + + +------------------------------------------------------------------------ +-- Properties of steps, and related properties of Permutation +-- previously required for proofs by well-founded induction +-- rendered obsolete/deprecatable by Core.↭-transˡ-≋ , Core.↭-transʳ-≋ +------------------------------------------------------------------------ + +module Steps {R : Rel A r} where + +-- Basic property + + 0