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

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 `↭-prep ` 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/Permutation/Propositional.agda

@@ -20,29 +20,18 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid)
 
 import Data.List.Relation.Binary.Permutation.Setoid as Permutation
 
-
 ------------------------------------------------------------------------
--- An inductive 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.
-{-
-infix 3 _↭_
-
-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 module ↭ = Permutation (setoid A) public
-  hiding ( ↭-reflexive; ↭-pointwise; ↭-trans
-         ; ↭-isEquivalence; ↭-setoid; module PermutationReasoning
-         )
+-- Definition of permutation
+
+private
+  module ↭ = Permutation (setoid A)
 
+-- Note that this is now defined in terms of `Permutation.Setoid` (#2317)
+
+open ↭ public
+  hiding ( ↭-reflexive; ↭-pointwise; ↭-trans; ↭-isEquivalence
+         ; module PermutationReasoning; ↭-setoid
+         )
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
@@ -74,7 +63,7 @@ open module ↭ = Permutation (setoid A) public
 -- A reasoning API to chain permutation proofs and allow "zooming in"
 -- to localised reasoning. For details of the axiomatisation, and
 -- in particular the refactored dependencies,
--- see `Data.List.Relation.Binary.Permutation.Setoid`
+-- see `Data.List.Relation.Binary.Permutation.Setoid.↭-Reasoning`. 
 
 module PermutationReasoning = ↭-Reasoning ↭-isEquivalence ↭-pointwise
 

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

@@ -42,12 +42,15 @@ private
     ws xs ys zs : List A
     vs : List B
 
-open Propositional {A = A}
-open module P = Permutation (setoid A) public
+  module ↭ = Permutation (setoid A)
+
+
+open Propositional {A = A} public
+open ↭ public
 -- legacy variations in naming
   renaming (dropMiddleElement-≋ to drop-mid-≡; dropMiddleElement to drop-mid)
 -- legacy variation in implicit/explicit parametrisation
-  hiding (shift)
+  hiding (shift; map⁺)
 
 ------------------------------------------------------------------------
 -- Some useful lemmas
@@ -166,7 +169,9 @@ Any-resp-[σ⁻¹∘σ] (swap _ _ σ)  (there (there ix))
 module _  {B : Set b} (f : A → B) where
 
   open Propositional {A = B} using () renaming (_↭_ to _↭′_)
-  private module ↭′ = Permutation (setoid B)
+
+  map⁺ : xs ↭ ys → List.map f xs ↭′ List.map f ys
+  map⁺ = ↭.map⁺ (setoid B) {!≡.cong f!}
 {-
   -- permutations preserve 'being a mapped list'
   ↭-map-inv : List.map f xs ↭′ vs → ∃ λ ys → vs ≡ List.map f ys × xs ↭ ys

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

@@ -131,7 +131,7 @@ steps-respʳ = Properties.steps-respʳ ≈-trans
 ------------------------------------------------------------------------
 -- map
 
-module _ (T : Setoid b ℓ) where
+module _ (T : Setoid b r) where
 
   open Setoid T using () renaming (_≈_ to _≈′_)
   open Permutation T using () renaming (_↭_ to _↭′_)