[ fix agda#1354 ] Refactoring Permutation.Propositional

Author: gallais

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

@@ -40,7 +40,7 @@ open import Relation.Binary
 import Relation.Binary.Reasoning.Setoid as EqR
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality as P
-  using (_≡_; _≢_; _≗_; refl)
+  using (_≡_; _≢_; _≗_)
 open import Relation.Nullary
 open import Data.List.Membership.Propositional.Properties
 
@@ -115,7 +115,7 @@ module ⊆-Reasoning where
 module _ {a k} {A : Set a} {x y : A} {xs ys} where
 
   ∷-cong : x ≡ y → xs ∼[ k ] ys → x ∷ xs ∼[ k ] y ∷ ys
-  ∷-cong refl xs≈ys {y} =
+  ∷-cong P.refl xs≈ys {y} =
     y ∈ x ∷ xs        ↔⟨ SK-sym $ ∷↔ (y ≡_) ⟩
     (y ≡ x ⊎ y ∈ xs)  ∼⟨ (y ≡ x ∎) ⊎-cong xs≈ys ⟩
     (y ≡ x ⊎ y ∈ ys)  ↔⟨ ∷↔ (y ≡_) ⟩
@@ -244,8 +244,8 @@ commutativeMonoid {a} k A = record
 
 empty-unique : ∀ {k a} {A : Set a} {xs : List A} →
                xs ∼[ ⌊ k ⌋→ ] [] → xs ≡ []
-empty-unique {xs = []}    _    = refl
-empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl)
+empty-unique {xs = []}    _    = P.refl
+empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here P.refl)
 ... | ()
 
 -- _++_ is idempotent (under set equality).
@@ -278,7 +278,7 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl)
   (fs ⊛ (xs₁ ++ xs₂)) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
 ⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
   fs ⊛ (xs₁ ++ xs₂)                         ≡⟨⟩
-  (fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f)  ≡⟨ (MP.cong (refl {x = fs}) λ f →
+  (fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f)  ≡⟨ (MP.cong (P.refl {x = fs}) λ f →
                                                 MP.right-distributive xs₁ xs₂ (return ∘ f)) ⟩
   (fs >>= λ f → (xs₁ >>= return ∘ f) ++
                 (xs₂ >>= return ∘ f))       ≈⟨ >>=-left-distributive fs ⟩
@@ -297,7 +297,7 @@ private
   ¬-drop-cons : ∀ {a} {A : Set a} {x : A} →
     ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
   ¬-drop-cons {x = x} drop-cons
-    with FE.Equivalence.to x∼[] ⟨$⟩ here refl
+    with FE.Equivalence.to x∼[] ⟨$⟩ here P.refl
     where
     x,x≈x :  (x ∷ x ∷ []) ∼[ set ] [ x ]
     x,x≈x = ++-idempotent [ x ]
@@ -336,8 +336,8 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
     (z ≡ x ⊎ z ∈ xs)                   ↔⟨ K-refl ⊎-cong ∈-index xs ⟩
     (z ≡ x ⊎ ∃ λ i → z ≡ lookup xs i)  ↔⟨ SK-sym $ inverse (λ { (zero , p) → inj₁ p; (suc i , p) → inj₂ (i , p) })
                                                           (λ { (inj₁ p) → zero , p; (inj₂ (i , p)) → suc i , p })
-                                                          (λ { (zero , _) → refl; (suc _ , _) → refl })
-                                                          (λ { (inj₁ _) → refl; (inj₂ _) → refl }) ⟩
+                                                          (λ { (zero , _) → P.refl; (suc _ , _) → P.refl })
+                                                          (λ { (inj₁ _) → P.refl; (inj₂ _) → P.refl }) ⟩
     (∃ λ i → z ≡ lookup (x ∷ xs) i)    ∎
     where
     open Related.EquationalReasoning
@@ -359,7 +359,7 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
   Fin-length xs =
     (∃ λ z → z ∈ xs)                   ↔⟨ Σ.cong K-refl (∈-index xs) ⟩
     (∃ λ z → ∃ λ i → z ≡ lookup xs i)  ↔⟨ ∃∃↔∃∃ _ ⟩
-    (∃ λ i → ∃ λ z → z ≡ lookup xs i)  ↔⟨ Σ.cong K-refl (inverse _ (λ _ → _ , refl) (λ { (_ , refl) → refl }) (λ _ → refl)) ⟩
+    (∃ λ i → ∃ λ z → z ≡ lookup xs i)  ↔⟨ Σ.cong K-refl (inverse _ (λ _ → _ , P.refl) (λ { (_ , P.refl) → P.refl }) (const P.refl)) ⟩
     (Fin (length xs) × ⊤)              ↔⟨ ×-identityʳ _ _ ⟩
     Fin (length xs)                    ∎
     where
@@ -410,8 +410,8 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
         (from (Fin-length xs) ⟨$⟩ (to (Fin-length xs) ⟨$⟩ (z , p))))
     lemma z p with to (Fin-length xs) ⟨$⟩ (z , p)
                  | left-inverse-of (Fin-length xs) (z , p)
-    lemma .(lookup xs i) .(from (∈-index xs) ⟨$⟩ (i , refl)) | i | refl =
-      refl
+    lemma .(lookup xs i) .(from (∈-index xs) ⟨$⟩ (i , P.refl)) | i | P.refl =
+      P.refl
 
   -- Bag equivalence isomorphisms preserve index equality. Note that
   -- this means that, even if the underlying equality is proof
@@ -435,7 +435,7 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
   -- The old inspect idiom.
 
   inspect : ∀ {a} {A : Set a} (x : A) → ∃ (x ≡_)
-  inspect x = x , refl
+  inspect x = x , P.refl
 
   -- A function is "well-behaved" if any "left" element which is the
   -- image of a "right" element is in turn not mapped to another
@@ -548,7 +548,7 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
                                                                                to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩
     index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ (from (∼→⊎↔⊎ inv) ⟨$⟩ inj₁ q))  ≡⟨ P.cong index-of $
                                                                                right-inverse-of (∷↔ _) (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 q)                   ≡⟨ index-equality-preserved (SK-sym inv) P.refl ⟩
     index-of {xs = x ∷ xs} (to (SK-sym inv) ⟨$⟩ here p)                   ≡⟨ P.cong index-of $ P.sym $
                                                                                right-inverse-of (∷↔ _) (from inv ⟨$⟩ here p) ⟩
     index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ (from (∼→⊎↔⊎ inv) ⟨$⟩ inj₁ p))  ≡⟨ P.cong (index-of ∘ (to (∷↔ (_ ≡_)) ⟨$⟩_)) $
@@ -578,23 +578,23 @@ module _ {a} {A : Set a} where
     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)         = P.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)) = P.cong (there ∘ there) (from∘to p v∈xs)
+    from∘to refl          v∈xs                   = P.refl
+    from∘to (prep _ _)    (here P.refl)          = P.refl
+    from∘to (prep _ p)    (there v∈xs)           = P.cong there (from∘to p v∈xs)
+    from∘to (swap x y p)  (here P.refl)          = P.refl
+    from∘to (swap x y p)  (there (here P.refl))  = P.refl
+    from∘to (swap x y p)  (there (there v∈xs))   = P.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 p₁ v∈xs                  = P.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
 
   ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_
   ∼bag⇒↭ {[]} eq with empty-unique {A = A} (Inv.sym eq)
-  ... | refl = refl
+  ... | P.refl = refl
   ∼bag⇒↭ {x ∷ xs} eq with ∈-∃++ (to ⟨$⟩ (here P.refl))
     where open Inv.Inverse (eq {x})
   ... | zs₁ , zs₂ , p rewrite p = begin

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

@@ -9,48 +9,50 @@
 module Data.List.Relation.Binary.Permutation.Homogeneous where
 
 open import Data.List.Base using (List; _∷_)
-open import Data.List.Relation.Binary.Pointwise as Pointwise
-  using (Pointwise)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
 
 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

@@ -10,41 +10,38 @@ module Data.List.Relation.Binary.Permutation.Propositional
   {a} {A : Set a} where
 
 open import Data.List.Base using (List; []; _∷_)
+import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-------------------------------------------------------------------------
--- 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 Eq.refl
+pattern prep x tl = Homogeneous.prep {x = x} Eq.refl tl
+pattern swap x y tl = Homogeneous.swap {x = x} {y = y} Eq.refl Eq.refl tl
+
+open Homogeneous public
+  using (trans)
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
+↭-reflexive Eq.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 Eq.sym Eq.sym
 
 -- A smart version of trans that avoids unnecessary `refl`s (see #1113).
 ↭-trans : Transitive _↭_