[ fix #1354 ] Refactoring Permutation.Propositional

CHANGELOG.md

@@ -27,6 +27,13 @@ Non-backwards compatible changes
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
   parametrized by _raw_ bundles, and as such take a proof of reflexivity.
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`, the explicit use of `Pointwise`
+  has been removed in favour of an additional relation on lists. This enables us to keep
+  using `Pointwise _≈_` in the setoid case but use the more convenient `_≡_` instead in
+  the propositional one.
+  Correspondingly, `Data.List.Relation.Binary.Permutation.Propositional` has been refactored
+  as an instance of the generic data structure.
+
 Other major improvements
 ------------------------
 
@@ -79,7 +86,7 @@ New modules
   ```agda
   Algebra.Module.Construct.Idealization
   ```
-  
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
@@ -155,7 +162,7 @@ Additions to existing modules
   quasigroup      : Quasigroup _ _
   isLoop          : IsLoop _∙_ _\\_ _//_ ε
   loop            : Loop _ _
-  
+
   \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
   \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
   \\-leftDivides   : LeftDivides _∙_ _\\_
@@ -174,7 +181,7 @@ Additions to existing modules
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
- 
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -203,7 +210,7 @@ Additions to existing modules
   _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
- 
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -305,7 +312,7 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
-  
+
 * Added new proofs to `Data.Nat.Primality`:
   ```agda
   rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n

doc/README/Data/List/Relation/Binary/Permutation.agda

@@ -9,8 +9,6 @@ module README.Data.List.Relation.Binary.Permutation where
 open import Algebra.Structures using (IsCommutativeMonoid)
 open import Data.List.Base
 open import Data.Nat using (ℕ; _+_)
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; sym; cong; setoid)
 
 ------------------------------------------------------------------------
 -- Permutations

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -23,7 +23,9 @@ 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
+  using (_↭_; ↭-refl; ↭-sym; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+  using (↭-sym-involutive; ∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ++-comm; ↭-shift)
 open import Data.Product.Base as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
@@ -54,6 +56,7 @@ private
     x y : A
     ws xs ys zs : List A
 
+
 ------------------------------------------------------------------------
 -- Definitions
 
@@ -142,8 +145,8 @@ module _ {k} {f g : A → B} {xs ys} where
     helper y = mk↔ₛ′
       (λ x≡fy → ≡.trans x≡fy (        f≗g y))
       (λ x≡gy → ≡.trans x≡gy (≡.sym $ f≗g y))
-      (λ { ≡.refl → ≡.trans-symˡ (f≗g y) })
-      λ { ≡.refl → ≡.trans-symʳ (f≗g y) }
+      (λ { refl → ≡.trans-symˡ (f≗g y) })
+      λ { refl → ≡.trans-symʳ (f≗g y) }
 
 ------------------------------------------------------------------------
 -- _++_
@@ -281,7 +284,6 @@ empty-unique {xs = _ ∷ _} ∷∼[] with () ← ⇒→ ∷∼[] (here refl)
                                                 MP.right-distributive xs₁ xs₂ (pure ∘ f)) ⟩
   (fs >>= λ f → (xs₁ >>= pure ∘ f) ++
                 (xs₂ >>= pure ∘ f))       ≈⟨ >>=-left-distributive fs ⟩
-
   (fs >>= λ f → xs₁ >>= pure ∘ f) ++
   (fs >>= λ f → xs₂ >>= pure ∘ f)         ≡⟨ ≡.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨
 
@@ -295,7 +297,8 @@ private
 
   ¬-drop-cons : ∀ {x : A} →
     ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
-  ¬-drop-cons {x = x} drop-cons with Equivalence.to x∼[] (here refl)
+  ¬-drop-cons {x = x} drop-cons
+    with Equivalence.to x∼[] (here refl)
     where
     x,x≈x :  (x ∷ x ∷ []) ∼[ set ] [ x ]
     x,x≈x = ++-idempotent [ x ]
@@ -584,12 +587,12 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
   to∘from p with res ← from∘to (↭-sym p) rewrite ↭-sym-involutive p = res
 
 ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A}
-∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = refl
+∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = ↭-refl
 ∼bag⇒↭ {A = A} {x ∷ xs} eq
   with zs₁ , zs₂ , p ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) 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₂ ⟨
+    x ∷ (zs₁ ++ zs₂) ↭⟨ ↭-shift zs₁ ⟨
     zs₁ ++ x ∷ zs₂   ∎
     where
     open CommutativeMonoid (commutativeMonoid bag A)

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

@@ -9,10 +9,6 @@
 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 Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
@@ -21,41 +17,45 @@ open import Relation.Binary.Definitions using (Reflexive; Symmetric)
 
 private
   variable
-    a r s : Level
+    a pr r ps s : Level
     A : Set 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
+-- PR is morally the pointwise lifting of R to lists but it need not be intensionally
+data Permutation {A : Set a} (PR : Rel (List A) pr) (R : Rel A r) : Rel (List A) (a ⊔ pr ⊔ r) where
+  refl  : ∀ {xs ys} → PR xs ys → Permutation PR R xs ys
+  prep  : ∀ {xs ys x y} (eq : R x y) → Permutation PR R xs ys → Permutation PR R (x ∷ xs) (y ∷ ys)
+  swap  : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation PR R xs ys → Permutation PR R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys)
+  trans : ∀ {xs ys zs} → Permutation PR R xs ys → Permutation PR R ys zs → Permutation PR R xs zs
 
 ------------------------------------------------------------------------
 -- The Permutation relation is an equivalence
 
-module _ {R : Rel A r}  where
+module _ {PR : Rel (List A) pr} {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)
+  sym : Symmetric PR → Symmetric R → Symmetric (Permutation PR R)
+  sym PR-sym R-sym (refl xs∼ys)           = refl (PR-sym xs∼ys)
+  sym PR-sym R-sym (prep x∼x′ xs↭ys)      = prep (R-sym x∼x′) (sym PR-sym R-sym xs↭ys)
+  sym PR-sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym PR-sym R-sym xs↭ys)
+  sym PR-sym R-sym (trans xs↭ys ys↭zs)    = trans (sym PR-sym R-sym ys↭zs) (sym PR-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
+  isEquivalence : Reflexive PR →
+                  Symmetric PR → Symmetric R →
+                  IsEquivalence (Permutation PR R)
+  isEquivalence PR-refl PR-sym R-sym = record
+    { refl  = refl PR-refl
+    ; sym   = sym PR-sym R-sym
     ; trans = trans
     }
 
-  setoid : Reflexive R → Symmetric R → Setoid _ _
-  setoid R-refl R-sym = record
-    { isEquivalence = isEquivalence R-refl R-sym
+  setoid : Reflexive PR → Symmetric PR → Symmetric R → Setoid _ _
+  setoid PR-refl PR-sym R-sym = record
+    { isEquivalence = isEquivalence PR-refl PR-sym 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)
+map : ∀ {PR : Rel (List A) pr} {PS : Rel (List A) ps} →
+        {R : Rel A r} {S : Rel A s} →
+        (PR ⇒ PS) → (R ⇒ S) → (Permutation PR R ⇒ Permutation PS S)
+map PR⇒PS R⇒S (refl xs∼ys)         = refl (PR⇒PS xs∼ys)
+map PR⇒PS R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map PR⇒PS R⇒S xs∼ys)
+map PR⇒PS R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map PR⇒PS R⇒S xs∼ys)
+map PR⇒PS R⇒S (trans xs∼ys ys∼zs)  = trans (map PR⇒PS R⇒S xs∼ys) (map PR⇒PS R⇒S ys∼zs)

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

@@ -14,41 +14,38 @@ 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
+import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
 
-------------------------------------------------------------------------
--- 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.
+------------------------------------------------------------------------
+-- Definition
 
 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
+_↭_ : Rel (List A) a
+_↭_ = Homogeneous.Permutation _≡_ _≡_
+
+pattern refl = Homogeneous.refl ≡.refl
+pattern prep {xs} {ys} x tl = Homogeneous.prep {xs = xs} {ys = ys} {x = x} ≡.refl tl
+pattern swap {xs} {ys} x y tl = Homogeneous.swap {xs = xs} {ys = ys} {x = x} {y = y} ≡.refl ≡.refl tl
+
+open Homogeneous public
+  using (trans)
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
+↭-reflexive ≡.refl = 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)
+↭-sym = Homogeneous.sym ≡.sym ≡.sym
 
 -- A smart version of trans that avoids unnecessary `refl`s (see #1113).
 ↭-trans : Transitive _↭_
@@ -74,7 +71,7 @@ data _↭_ : Rel (List A) a where
 
 module PermutationReasoning where
 
-  private module Base = EqReasoning ↭-setoid
+  private module Base = ≈-Reasoning ↭-setoid
 
   open Base public
     hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
@@ -89,12 +86,12 @@ 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 x 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 x y 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