[ fix agda#1354 ] Refactoring Permutation.Propositional

Author: gallais

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,6 +23,7 @@ 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
 open import Data.Product.Base as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
@@ -54,6 +55,7 @@ private
     x y : A
     ws xs ys zs : List A
 
+
 ------------------------------------------------------------------------
 -- Definitions
 
@@ -142,8 +144,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) }
 
 ------------------------------------------------------------------------
 -- _++_
@@ -282,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₂) ⟨
 
@@ -296,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 ]
@@ -357,7 +359,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     (∃ λ z → z ∈ xs)                   ↔⟨ Σ.cong K-refl (∈-index xs) ⟩
     (∃ λ z → ∃ λ i → z ≡ lookup xs i)  ↔⟨ ∃∃↔∃∃ _ ⟩
     (∃ λ i → ∃ λ z → z ≡ lookup xs i)  ↔⟨ Σ.cong K-refl (mk↔ₛ′ _ (λ _ → _ , refl) (λ _ → refl) (λ { (_ , refl) → refl })) ⟩
-    (Fin (length xs) × ⊤)              ↔⟨ ×-identityʳ _ _ ⟩
+   (Fin (length xs) × ⊤)              ↔⟨ ×-identityʳ _ _ ⟩
     Fin (length xs)                    ∎
     where
     open Related.EquationalReasoning
@@ -571,24 +573,16 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
   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
+  from∘to = Any-resp-[σ⁻¹∘σ]
 
   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
 
 ∼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))
+... | 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₁ ⟩

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
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
+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