Refactor Data.List.Relation.Binary.Permutation.*

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
 ------------------
 

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:
 

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,62 +537,60 @@ 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
 
 ↭⇒∼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

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

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."
+#-}

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<steps : (xs↭ys : Permutation R xs ys) → 0 < steps xs↭ys
+  0<steps (refl _)             = ℕ.n<1+n 0
+  0<steps (prep eq xs↭ys)      = ℕ.m<n⇒m<1+n (0<steps xs↭ys)
+  0<steps (swap eq₁ eq₂ xs↭ys) = ℕ.m<n⇒m<1+n (0<steps xs↭ys)
+  0<steps (trans xs↭ys ys↭zs) =
+    ℕ.<-≤-trans (0<steps xs↭ys) (ℕ.m≤m+n (steps xs↭ys) (steps ys↭zs))
+
+  module _ (R-trans : Transitive R) where
+
+    private
+      ≋-trans : Transitive (Pointwise R)
+      ≋-trans = Pointwise.transitive R-trans
+
+    ↭-respʳ-≋ : (Permutation R) Respectsʳ (Pointwise R)
+    ↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
+    ↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (R-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+    ↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (R-trans eq₁ w≈z) (R-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+    ↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)
+
+    steps-respʳ : (xs≋ys : Pointwise R xs ys) (zs↭xs : Permutation R zs xs) →
+                  steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
+    steps-respʳ _               (refl _)            = ≡.refl
+    steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
+    steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
+    steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)
+
+    module _ (R-sym : Symmetric R) where
+
+      private
+        ≋-sym : Symmetric (Pointwise R)
+        ≋-sym = Pointwise.symmetric R-sym
+
+      ↭-respˡ-≋ : (Permutation R) Respectsˡ (Pointwise R)
+      ↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
+      ↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (R-trans (R-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
+      ↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (R-trans (R-sym x≈y) eq₁) (R-trans (R-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
+      ↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs
+
+      steps-respˡ : (ys≋xs : Pointwise R ys xs) (ys↭zs : Permutation R ys zs) →
+                    steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
+      steps-respˡ _               (refl _)            = ≡.refl
+      steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
+      steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
+      steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+¬x∷xs↭[] = ¬x∷xs↭[]ʳ
+{-# WARNING_ON_USAGE ¬x∷xs↭[]
+"Warning: ¬x∷xs↭[] was deprecated in v2.1.
+Please use ¬x∷xs↭[]ʳ instead."
+#-}
+
+↭-singleton⁻¹ : Transitive R →
+                ∀ {xs x} → Permutation R xs [ x ] → ∃ λ y → xs ≡ [ y ] × R y x
+↭-singleton⁻¹ = ↭-singleton-invʳ
+{-# WARNING_ON_USAGE ↭-singleton⁻¹
+"Warning: ↭-singleton⁻¹ was deprecated in v2.1.
+Please use ↭-singleton-invʳ instead."
+#-}
+

src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/Core.agda

@@ -0,0 +1,242 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core properties of the `Homogeneous` definition of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
+
+module Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core
+  {a r} {A : Set a} {R : Rel A r} where
+
+open import Data.List.Base as List using (List; []; _∷_; [_]; _++_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+open import Data.List.Relation.Binary.Permutation.Homogeneous public
+  using (Permutation; refl; prep; swap; trans)
+
+private
+  variable
+    xs ys zs : List A
+    x y z v w : A
+
+  _++[_]++_ = λ xs (z : A) ys → xs ++ [ z ] ++ ys
+
+_≋_ _↭_ : Rel (List A) _
+_≋_ = Pointwise R
+_↭_ = Permutation R
+
+
+------------------------------------------------------------------------
+-- Properties of _↭_ depending on suitable assumptions on R
+
+-- Constructor alias
+
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = refl
+
+------------------------------------------------------------------------
+-- Reflexivity and its consequences
+
+module Reflexivity (R-refl : Reflexive R) where
+
+  ≋-refl : Reflexive _≋_
+  ≋-refl = Pointwise.refl R-refl
+
+  ↭-refl : Reflexive _↭_
+  ↭-refl = ↭-pointwise ≋-refl
+
+  ↭-prep : ∀ {x} {xs ys} → xs ↭ ys → (x ∷ xs) ↭ (x ∷ ys)
+  ↭-prep xs↭ys = prep R-refl xs↭ys
+
+  ↭-swap : ∀ x y {xs ys} → xs ↭ ys → (x ∷ y ∷ xs) ↭ (y ∷ x ∷ ys)
+  ↭-swap _ _ xs↭ys = swap R-refl R-refl xs↭ys
+
+  ↭-shift : ∀ {v w} → R v w → ∀ xs {ys zs} → ys ↭ zs →
+            (xs ++ v ∷ ys) ↭ (w ∷ xs ++ zs)
+  ↭-shift {v} {w} v≈w []       rel = prep v≈w rel
+  ↭-shift {v} {w} v≈w (x ∷ xs) rel
+    = trans (↭-prep (↭-shift v≈w xs rel)) (↭-swap x w ↭-refl)
+
+  shift : ∀ {v w} → R v w → ∀ xs {ys} → (xs ++[ v ]++ ys) ↭ (w ∷ xs ++ ys)
+  shift v≈w xs = ↭-shift v≈w xs ↭-refl
+
+  shift≈ : ∀ x xs {ys} → (xs ++[ x ]++ ys) ↭ (x ∷ xs ++ ys)
+  shift≈ x xs = shift R-refl xs
+
+------------------------------------------------------------------------
+-- Symmetry and its consequences
+
+module Symmetry (R-sym : Symmetric R) where
+
+  ≋-sym : Symmetric _≋_
+  ≋-sym = Pointwise.symmetric R-sym
+
+  ↭-sym : Symmetric _↭_
+  ↭-sym (refl xs∼ys)           = refl (≋-sym xs∼ys)
+  ↭-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (↭-sym xs↭ys)
+  ↭-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (↭-sym xs↭ys)
+  ↭-sym (trans xs↭ys ys↭zs)    = trans (↭-sym ys↭zs) (↭-sym xs↭ys)
+
+------------------------------------------------------------------------
+-- Transitivity and its consequences
+
+-- A smart version of trans that pushes `refl`s to the leaves (see #1113).
+
+module LRTransitivity
+       (↭-transˡ-≋ : LeftTrans _≋_ _↭_)
+       (↭-transʳ-≋ : RightTrans _↭_ _≋_)
+
+  where
+
+  ↭-trans : Transitive _↭_
+  ↭-trans (refl xs≋ys) ys↭zs = ↭-transˡ-≋ xs≋ys ys↭zs
+  ↭-trans xs↭ys (refl ys≋zs) = ↭-transʳ-≋ xs↭ys ys≋zs
+  ↭-trans xs↭ys ys↭zs        = trans xs↭ys ys↭zs
+
+------------------------------------------------------------------------
+-- Two important inversion properties of ↭, which *no longer*
+-- require `steps` or  well-founded induction... but which
+-- follow from ↭-transˡ-≋, ↭-transʳ-≋ and properties of R
+------------------------------------------------------------------------
+
+-- first inversion: split on a 'middle' element
+
+  module Split (R-refl : Reflexive R) (R-trans : Transitive R) where
+
+    private
+      ≋-trans : Transitive (Pointwise R)
+      ≋-trans = Pointwise.transitive R-trans
+
+      open Reflexivity R-refl using (≋-refl; ↭-refl; ↭-prep; ↭-swap)
+
+      helper : ∀ as bs {xs ys} (p : xs ↭ ys) →
+               ys ≋ (as ++[ v ]++ bs) →
+               ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+                          × (ps ++ qs) ↭ (as ++ bs)
+      helper as           bs (trans xs↭ys ys↭zs) zs≋as++[v]++ys
+        with ps , qs , eq , ↭ ← helper as bs ys↭zs zs≋as++[v]++ys
+        with ps′ , qs′ , eq′ , ↭′ ← helper ps qs xs↭ys eq
+        = ps′ , qs′ , eq′ , ↭-trans ↭′ ↭
+      helper []           _  (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+        = [] , _ , R-trans x≈v v≈y ∷ ≋-refl , refl (≋-trans xs≋vs vs≋ys)
+      helper (a ∷ as)     bs (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+        = _ ∷ as , bs , R-trans x≈v v≈y ∷ ≋-trans xs≋vs vs≋ys , ↭-refl
+      helper []           bs (prep {xs = xs} x≈v xs↭vs) (v≈y ∷ vs≋ys)
+        = [] , xs , R-trans x≈v v≈y ∷ ≋-refl , ↭-transʳ-≋ xs↭vs vs≋ys
+      helper (a ∷ as)     bs (prep x≈v as↭vs) (v≈y ∷ vs≋ys)
+        with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+        = a ∷ ps , qs , R-trans x≈v v≈y ∷ eq , prep R-refl ↭
+      helper []           [] (swap _ _ _) (_ ∷ ())
+      helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
+        = b ∷ [] , _ , R-trans x≈v v≈y ∷ R-trans y≈w w≈z ∷ ≋-refl
+                     , ↭-prep (↭-transʳ-≋ xs↭vs vs≋ys)
+      helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
+        = []     , a ∷ _ , R-trans x≈v v≈y ∷ R-trans y≈w w≈z ∷ ≋-refl
+                         , ↭-prep (↭-transʳ-≋ xs↭vs vs≋ys)
+      helper (a ∷ b ∷ as) bs (swap x≈v y≈w as↭vs) (w≈a ∷ v≈b ∷ vs≋ys)
+        with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+        = b ∷ a ∷ ps , qs , R-trans x≈v v≈b ∷ R-trans y≈w w≈a ∷ eq
+                          , ↭-swap _ _ ↭
+
+    ↭-split : ∀ v as bs {xs} → xs ↭ (as ++[ v ]++ bs) →
+              ∃₂ λ ps qs → xs ≋ (ps ++[ v ]++ qs)
+                         × (ps ++ qs) ↭ (as ++ bs)
+    ↭-split v as bs p = helper as bs p ≋-refl
+
+
+-- second inversion: using ↭-split, drop the middle element
+
+  module DropMiddle (R-≈ : IsEquivalence R) where
+
+    private
+      module ≈ = IsEquivalence R-≈
+      open Reflexivity ≈.refl using (shift)
+      open Symmetry ≈.sym using (↭-sym)
+      open Split ≈.refl ≈.trans
+
+    dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
+                          (ws ++[ x ]++ ys) ≋ (xs ++[ x ]++ zs) →
+                          (ws ++ ys) ↭ (xs ++ zs)
+    dropMiddleElement-≋ []       []       (_   ∷ eq)
+      = ↭-pointwise eq
+    dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq)
+      = ↭-transˡ-≋ eq (shift w≈v xs)
+    dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq)
+      = ↭-transʳ-≋ (↭-sym (shift (≈.sym w≈x) ws)) eq
+    dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq)
+      = prep w≈x (dropMiddleElement-≋ ws xs eq)
+
+    dropMiddleElement : ∀ {x} ws xs {ys zs} →
+                        (ws ++[ x ]++ ys) ↭ (xs ++[ x ]++ zs) →
+                        (ws ++ ys) ↭ (xs ++ zs)
+    dropMiddleElement {x} ws xs {ys} {zs} p
+      with ps , qs , eq , ↭ ← ↭-split x xs zs p
+      = ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
+
+    syntax dropMiddleElement-≋ ws xs ws++x∷ys≋xs++x∷zs
+      = ws ++≋[ ws++x∷ys≋xs++x∷zs ]++ xs
+
+    syntax dropMiddleElement ws xs ws++x∷ys↭xs++x∷zs
+      = ws ++↭[ ws++x∷ys↭xs++x∷zs ]++ xs
+
+
+------------------------------------------------------------------------
+-- Now: Left and Right Transitivity hold outright!
+
+module Transitivity (R-trans : Transitive R) where
+
+  private
+    ≋-trans : Transitive _≋_
+    ≋-trans = Pointwise.transitive R-trans
+
+  ↭-transˡ-≋ : LeftTrans _≋_ _↭_
+  ↭-transˡ-≋ xs≋ys               (refl ys≋zs)
+    = refl (≋-trans xs≋ys ys≋zs)
+  ↭-transˡ-≋ (x≈y ∷ xs≋ys)       (prep y≈z ys↭zs)
+    = prep (R-trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs)
+  ↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs)
+    = swap (R-trans x≈y eq₁) (R-trans w≈z eq₂) (↭-transˡ-≋ xs≋ys ys↭zs)
+  ↭-transˡ-≋ xs≋ys               (trans ys↭ws ws↭zs)
+    = trans (↭-transˡ-≋ xs≋ys ys↭ws) ws↭zs
+
+  ↭-transʳ-≋ : RightTrans _↭_ _≋_
+  ↭-transʳ-≋ (refl xs≋ys)         ys≋zs
+    = refl (≋-trans xs≋ys ys≋zs)
+  ↭-transʳ-≋ (prep x≈y xs↭ys)     (y≈z ∷ ys≋zs)
+    = prep (R-trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs)
+  ↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs)
+    = swap (R-trans eq₁ y≈z) (R-trans eq₂ x≈w) (↭-transʳ-≋ xs↭ys ys≋zs)
+  ↭-transʳ-≋ (trans xs↭ws ws↭ys)  ys≋zs
+    = trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs)
+
+-- Transitivity proper
+
+  ↭-trans : Transitive _↭_
+  ↭-trans = LRTransitivity.↭-trans ↭-transˡ-≋ ↭-transʳ-≋
+
+
+------------------------------------------------------------------------
+-- Permutation is an equivalence (Setoid version)
+
+module _ (R-equiv : IsEquivalence R) where
+
+  private module ≈ = IsEquivalence R-equiv
+
+  isEquivalence : IsEquivalence _↭_
+  isEquivalence = record
+    { refl  = Reflexivity.↭-refl ≈.refl
+    ; sym   = Symmetry.↭-sym ≈.sym
+    ; trans = Transitivity.↭-trans ≈.trans
+    }
+
+  setoid : Setoid _ _
+  setoid = record { isEquivalence = isEquivalence }

src/Data/List/Relation/Binary/Permutation/Homogeneous/Properties/HigherDimensional.agda

@@ -0,0 +1,107 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Higher-dimensional properties of the `Homogeneous` definition of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Permutation.Homogeneous.Properties.HigherDimensional where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.Any as Any
+  using (Any; here; there)
+import Data.List.Relation.Unary.Any.Properties as Any
+open import Function.Base using (_∘_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+  using (Symmetric; Transitive; _Respects_)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+  using (_≡_ ; cong; cong₂)
+
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties as Properties
+
+private
+  variable
+    a r : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+
+------------------------------------------------------------------------
+-- Two higher-dimensional properties useful in the `Propositional` case,
+-- specifically in the equivalence proof between `Bag` equality and `_↭_`
+------------------------------------------------------------------------
+
+module _ {_≈_ : Rel A r} (≈-sym : Symmetric _≈_) where
+
+  open Core {R = _≈_} using (_≋_; _↭_; refl; prep; swap; trans; module Symmetry)
+  open Symmetry ≈-sym using (≋-sym; ↭-sym)
+
+-- involutive symmetry lifts
+
+  module _ (≈-sym-involutive : ∀ {x y} (p : x ≈ y) → ≈-sym (≈-sym p) ≡ p)
+    where
+
+    ↭-sym-involutive : (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
+    ↭-sym-involutive (refl xs≋ys) = cong refl (≋-sym-involutive xs≋ys)
+      where
+      ≋-sym-involutive : (p : xs ≋ ys) → ≋-sym (≋-sym p) ≡ p
+      ≋-sym-involutive [] = ≡.refl
+      ≋-sym-involutive (x≈y ∷ xs≋ys) rewrite ≈-sym-involutive x≈y
+        = cong (_ ∷_) (≋-sym-involutive xs≋ys)
+    ↭-sym-involutive (prep eq p) = cong₂ prep (≈-sym-involutive eq) (↭-sym-involutive p)
+    ↭-sym-involutive (swap eq₁ eq₂ p) rewrite ≈-sym-involutive eq₁ | ≈-sym-involutive eq₂
+      = cong (swap _ _) (↭-sym-involutive p)
+    ↭-sym-involutive (trans p q) = cong₂ trans (↭-sym-involutive p) (↭-sym-involutive q)
+
+    module _ (≈-trans : Transitive _≈_) where
+
+      private
+        ∈-resp-Pointwise : (Any (x ≈_)) Respects  _≋_
+        ∈-resp-Pointwise = Properties.∈-resp-Pointwise ≈-trans
+
+        ∈-resp-↭ : (Any (x ≈_)) Respects _↭_
+        ∈-resp-↭ = Properties.∈-resp-↭ ≈-trans
+
+-- invertible symmetry lifts to equality on proofs of membership
+
+      module _ (≈-trans-trans-sym : ∀ {x y z} (p : x ≈ y) (q : y ≈ z) →
+                                    ≈-trans (≈-trans p q) (≈-sym q) ≡ p) where
+
+        ∈-resp-Pointwise-sym : (p : xs ≋ ys) {ix : Any (x ≈_) xs} →
+                               ∈-resp-Pointwise (≋-sym p) (∈-resp-Pointwise p ix) ≡ ix
+        ∈-resp-Pointwise-sym (x≈y ∷ xs≋ys) {here ix}
+          = cong here (≈-trans-trans-sym ix x≈y)
+        ∈-resp-Pointwise-sym (x≈y ∷ xs≋ys) {there ixs}
+          = cong there (∈-resp-Pointwise-sym xs≋ys)
+
+        ∈-resp-↭-sym′   : (p : ys ↭ xs) {iy : Any (x ≈_) ys} {ix : Any (x ≈_) xs} →
+                           ix ≡ ∈-resp-↭ p iy → ∈-resp-↭ (↭-sym p) ix ≡ iy
+        ∈-resp-↭-sym′ (refl xs≋ys) ≡.refl = ∈-resp-Pointwise-sym xs≋ys
+        ∈-resp-↭-sym′ (prep eq₁ p) {here iy} {here ix} eq
+          with ≡.refl ← eq = cong here (≈-trans-trans-sym iy eq₁)
+        ∈-resp-↭-sym′ (prep eq₁ p) {there iys} {there ixs} eq
+          with ≡.refl ← eq = cong there (∈-resp-↭-sym′ p ≡.refl)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {here ix} {here iy} ()
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {here ix} {there iys} eq
+          with ≡.refl ← eq = cong here (≈-trans-trans-sym ix eq₁)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (here ix)} {there (here iy)} ()
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (here ix)} {here iy} eq
+          with ≡.refl ← eq = cong (there ∘ here) (≈-trans-trans-sym ix eq₂)
+        ∈-resp-↭-sym′ (swap eq₁ eq₂ p) {there (there ixs)} {there (there iys)} eq
+          with ≡.refl ← eq = cong (there ∘ there) (∈-resp-↭-sym′ p ≡.refl)
+        ∈-resp-↭-sym′ (trans p₁ p₂) eq = ∈-resp-↭-sym′ p₁ (∈-resp-↭-sym′ p₂ eq)
+
+        ∈-resp-↭-sym : (p : xs ↭ ys) {ix : Any (x ≈_) xs} →
+                       ∈-resp-↭ (↭-sym p) (∈-resp-↭ p ix) ≡ ix
+        ∈-resp-↭-sym p = ∈-resp-↭-sym′ p ≡.refl
+
+        ∈-resp-↭-sym⁻¹ : (p : xs ↭ ys) {iy : Any (x ≈_) ys} →
+                         ∈-resp-↭ p (∈-resp-↭ (↭-sym p) iy) ≡ iy
+        ∈-resp-↭-sym⁻¹ p with eq′ ← ∈-resp-↭-sym′ (↭-sym p)
+                         rewrite ↭-sym-involutive p = eq′ ≡.refl

src/Data/List/Relation/Binary/Permutation/Propositional.agda

@@ -10,91 +10,65 @@ module Data.List.Relation.Binary.Permutation.Propositional
   {a} {A : Set a} where
 
 open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
 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; Transitive)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.Definitions
+  using (Reflexive; Transitive; LeftTrans; RightTrans)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid)
+
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
 
 ------------------------------------------------------------------------
--- An inductive definition of permutation
+-- Definition of permutation
 
--- Note that one would expect that this would be defined in terms of
--- `Permutation.Setoid`. This is not currently the case as it involves
--- adding in a bunch of trivial `_≡_` proofs to the constructors which
--- a) adds noise and b) prevents easy access to the variables `x`, `y`.
--- This may be changed in future when a better solution is found.
+private
+  module ↭ = Permutation (setoid A)
 
-infix 3 _↭_
+-- Note that this is now defined in terms of `Permutation.Setoid` (#2317)
 
-data _↭_ : Rel (List A) a where
-  refl  : ∀ {xs}        → xs ↭ xs
-  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs
+open ↭ public
+  hiding ( ↭-reflexive; ↭-pointwise; ↭-trans; ↭-isEquivalence
+         ; module PermutationReasoning; ↭-setoid
+         )
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
-
-↭-refl : Reflexive _↭_
-↭-refl = refl
+↭-reflexive refl = ↭-refl
 
-↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
-↭-sym refl                = refl
-↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
-↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
-↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
 
 -- A smart version of trans that avoids unnecessary `refl`s (see #1113).
+↭-transˡ-≋ : LeftTrans _≋_ _↭_
+↭-transˡ-≋ xs≋ys ys↭zs with refl ← ≋⇒≡ xs≋ys = ys↭zs
+
+↭-transʳ-≋ : RightTrans _↭_ _≋_
+↭-transʳ-≋ xs↭ys ys≋zs with refl ← ≋⇒≡ ys≋zs = xs↭ys
+
 ↭-trans : Transitive _↭_
-↭-trans refl ρ₂ = ρ₂
-↭-trans ρ₁ refl = ρ₁
-↭-trans ρ₁ ρ₂   = trans ρ₁ ρ₂
+↭-trans = Core.LRTransitivity.↭-trans ↭-transˡ-≋ ↭-transʳ-≋
 
 ↭-isEquivalence : IsEquivalence _↭_
 ↭-isEquivalence = record
-  { refl  = refl
+  { refl  = ↭-refl
   ; sym   = ↭-sym
   ; trans = ↭-trans
   }
 
-↭-setoid : Setoid _ _
-↭-setoid = record
-  { isEquivalence = ↭-isEquivalence
-  }
-
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs and allow "zooming in"
--- to localised reasoning.
-
-module PermutationReasoning where
+-- to localised reasoning. For details of the axiomatisation, and
+-- in particular the refactored dependencies,
+-- see `Data.List.Relation.Binary.Permutation.Setoid.↭-Reasoning`. 
 
-  private module Base = EqReasoning ↭-setoid
+module PermutationReasoning = ↭-Reasoning ↭-isEquivalence ↭-pointwise
 
-  open Base public
-    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
-    renaming (≈-go to ↭-go)
-
-  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-
-  -- Some extra combinators that allow us to skip certain elements
-
-  infixr 2 step-swap step-prep
-
-  -- Skip reasoning on the first element
-  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
-              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel))
-
-  -- Skip reasoning about the first two elements
-  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
-              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))
+------------------------------------------------------------------------
+-- Bundle export
 
-  syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
-  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
+open PermutationReasoning public using (↭-setoid)

src/Data/List/Relation/Binary/Permutation/Setoid.agda

@@ -5,97 +5,103 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated function `steps`
 
 open import Function.Base using (_∘′_)
 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; Transitive)
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
 open import Relation.Binary.Reasoning.Syntax
 
 module Data.List.Relation.Binary.Permutation.Setoid
   {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.List.Base using (List; _∷_)
 import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
-import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl)
+import Data.List.Relation.Binary.Permutation.Homogeneous.Properties.Core as Core
 open import Data.List.Relation.Binary.Equality.Setoid S
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Nat.Base using (ℕ)
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-private
-  module Eq = Setoid S
-open Eq using (_≈_) renaming (Carrier to A)
+open Setoid S
+  using (_≈_)
+  renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
 
 ------------------------------------------------------------------------
 -- Definition
 
-open Homogeneous public
-  using (refl; prep; swap; trans)
-
 infix 3 _↭_
 
 _↭_ : Rel (List A) (a ⊔ ℓ)
-_↭_ = Homogeneous.Permutation _≈_
+_↭_ = Core._↭_ {R = _≈_}
 
 ------------------------------------------------------------------------
--- Constructor aliases
+-- Smart constructor aliases
+
+-- These provide aliases for the `Homogeneous` smart constructors, in
+-- particular for `swap` and `prep` when the elements being swapped or
+-- prepended are *propositionally* equal
 
--- These provide aliases for `swap` and `prep` when the elements being
--- swapped or prepended are propositionally equal
+↭-pointwise : _≋_ ⇒ _↭_
+↭-pointwise = Core.↭-pointwise
 
 ↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-↭-prep x xs↭ys = prep Eq.refl xs↭ys
+↭-prep _ = Core.Reflexivity.↭-prep ≈-refl
 
 ↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-↭-swap x y xs↭ys = swap Eq.refl Eq.refl xs↭ys
+↭-swap = Core.Reflexivity.↭-swap ≈-refl
+
+↭-trans′ : LeftTrans _≋_ _↭_ → RightTrans _↭_ _≋_ → Transitive _↭_
+↭-trans′ = Core.LRTransitivity.↭-trans
 
 ------------------------------------------------------------------------
--- Functions over permutations
+-- Functions over permutations (retained for legacy)
 
 steps : ∀ {xs ys} → 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
+steps = Homogeneous.steps
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl (Pointwise.refl Eq.refl)
+↭-reflexive refl = Core.Reflexivity.↭-refl ≈-refl
 
 ↭-refl : Reflexive _↭_
 ↭-refl = ↭-reflexive refl
 
 ↭-sym : Symmetric _↭_
-↭-sym = Homogeneous.sym Eq.sym
+↭-sym = Core.Symmetry.↭-sym ≈-sym
 
 ↭-trans : Transitive _↭_
-↭-trans = trans
+↭-trans = Core.Transitivity.↭-trans ≈-trans
 
 ↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym
-
-↭-setoid : Setoid _ _
-↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym
+↭-isEquivalence = record { refl = ↭-refl ; sym = ↭-sym ; trans = ↭-trans }
 
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs
 
-module PermutationReasoning where
+module ↭-Reasoning (↭-isEquivalence : IsEquivalence _↭_)
+                   (↭-pointwise : _≋_ ⇒ _↭_)
+                   where
+
+  ↭-setoid : Setoid _ _
+  ↭-setoid = record { isEquivalence = ↭-isEquivalence }
 
-  private module Base = ≈-Reasoning ↭-setoid
+  private
+    open IsEquivalence ↭-isEquivalence using () renaming (sym to ↭-sym′)
+    module Base = ≈-Reasoning ↭-setoid
 
   open Base public
     hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
     renaming (≈-go to ↭-go)
 
-  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public
+  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym′ public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-pointwise) ≋-sym public
 
   -- Some extra combinators that allow us to skip certain elements
 
@@ -104,12 +110,20 @@ module PermutationReasoning where
   -- Skip reasoning on the first element
   step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel))
+  step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel
 
   -- Skip reasoning about the first two elements
   step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel))
+  step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel
 
   syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
   syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
+
+module PermutationReasoning = ↭-Reasoning ↭-isEquivalence ↭-pointwise
+
+------------------------------------------------------------------------
+-- Bundle export
+
+open PermutationReasoning public using (↭-setoid)
+

src/Data/List/Relation/Ternary/Interleaving/Propositional.agda

@@ -37,6 +37,6 @@ toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
 toPermutation []         = Perm.refl
 toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
 toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
-  a ∷ as       ↭⟨ Perm.prep a (toPermutation sp) ⟩
-  a ∷ l ++ rs  ↭⟨ Perm.↭-sym (shift a l rs) ⟩
+  a ∷ as       <⟨ toPermutation sp ⟩
+  a ∷ l ++ rs  ↭⟨ shift a l rs ⟨
   l ++ a ∷ rs  ∎