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 `↭-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,21 +537,18 @@ 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₂ ⟩
+  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with begin
+    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)                                         ∎
+    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)                                     ∎
     where
     open Inverse
     open ≡-Reasoning
@@ -562,38 +558,31 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 -- 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)
+↭⇒∼bag {A = A} xs↭ys {v} = mk↔ (from∘to xs↭ys , to∘from xs↭ys)
+  --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} {iy : v ∈ ys} →
+            ix ≡ from p iy → to p ix ≡ iy
+  from∘to = ∈-resp-↭-sym⁻¹
+
+  to∘from : (p : ys ↭ xs) {iy : v ∈ ys} {ix : v ∈ xs} →
+            ix ≡ to p iy → from p ix ≡ iy
+  to∘from = ∈-resp-↭-sym
 
 ∼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