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