Revamp of Data.List.Relation.Binary.Subset (#1355)

Author: MatthewDaggitt

CHANGELOG.md

@@ -21,6 +21,10 @@ Bug-fixes
 * The binary relation `_≉_` exposed by records in `Relation.Binary.Bundles` now has
   the correct infix precedence.
 
+* Fixed the fixity of the reasoning combinators in
+  `Data.List.Relation.Binary.Subset.(Propositional/Setoid).Properties`so that they
+  compose properly.
+
 * Added version to library name
 
 Non-backwards compatible changes
@@ -33,24 +37,28 @@ Non-backwards compatible changes
 * The module `Algebra.Construct.Zero` and `Algebra.Module.Construct.Zero`
   are now level-polymorphic, each taking two implicit level parameters.
 
-* Previously the definition of `_⊖_` in `Data.Integer.Base` was defined
-  inductively as:
+* Previously `_⊖_` in `Data.Integer.Base` was defined inductively as:
   ```agda
   _⊖_ : ℕ → ℕ → ℤ
   m       ⊖ ℕ.zero  = + m
   ℕ.zero  ⊖ ℕ.suc n = -[1+ n ]
   ℕ.suc m ⊖ ℕ.suc n = m ⊖ n
   ```
-  which meant that the unary arguments had to be evaluated. To make it
-  much faster it's definition has been changed to use operations on `ℕ`
-  that are backed by builtin operations:
+  which meant that it had to recursively evaluate its unary arguments.
+  The definition has been changed as follows to use operations on `ℕ` that are backed
+  by builtin operations, greatly improving its performance:
   ```agda
   _⊖_ : ℕ → ℕ → ℤ
   m ⊖ n with m ℕ.<ᵇ n
   ... | true  = - + (n ℕ.∸ m)
   ... | false = + (m ℕ.∸ n)
   ```
 
+* The proofs `↭⇒∼bag` and `∼bag⇒↭` have been moved from
+  `Data.List.Relation.Binary.Permutation.Setoid.Properties`
+  to `Data.List.Relation.Binary.BagAndSetEquality` as their current location
+  were causing cyclic import dependencies.
+
 Deprecated modules
 ------------------
 
@@ -97,6 +105,24 @@ Deprecated names
   Plus′ ↦ TransClosure
   ```
 
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  mono            ↦ Any-resp-⊆
+  map-mono        ↦ map⁺
+  concat-mono     ↦ concat⁺
+  >>=-mono        ↦ >>=⁺
+  _⊛-mono_        ↦ ⊛⁺
+  _⊗-mono_        ↦ ⊗⁺
+  any-mono        ↦ any⁺
+  map-with-∈-mono ↦ map-with-∈⁺
+  filter⁺         ↦ filter-⊆
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+    ```agda
+  filter⁺         ↦ filter-⊆
+  ```
+
 New modules
 -----------
 
@@ -236,6 +262,60 @@ Other minor additions
   m-n≡m⊖n         : + m + (- + n) ≡ m ⊖ n
   ```
 
+* Added new relations in `Data.List.Relation.Binary.Subset.(Propositional/Setoid)`:
+  ```agda
+  xs ⊇ ys = ys ⊆ xs
+  xs ⊉ ys = ¬ xs ⊇ ys
+  ```
+
+* Added new proofs in `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  ⊆-respʳ-≋      : _⊆_ Respectsʳ _≋_
+  ⊆-respˡ-≋      : _⊆_ Respectsˡ _≋_
+
+  ↭⇒⊆            : _↭_ ⇒ _⊆_
+  ⊆-respʳ-↭      : _⊆_ Respectsʳ _↭_
+  ⊆-respˡ-↭      : _⊆_ Respectsˡ _↭_
+  ⊆-↭-isPreorder : IsPreorder _↭_ _⊆_
+  ⊆-↭-preorder   : Preorder _ _ _
+
+  Any-resp-⊆     : P Respects _≈_ → (Any P) Respects _⊆_
+  All-resp-⊇     : P Respects _≈_ → (All P) Respects _⊇_
+
+  xs⊆xs++ys      : xs ⊆ xs ++ ys
+  xs⊆ys++xs      : xs ⊆ ys ++ xs
+  ++⁺ʳ           : xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
+  ++⁺ˡ           : xs ⊆ ys → xs ++ zs ⊆ ys ++ zs
+  ++⁺            : ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs
+  ```
+
+* Added new proofs in `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  ↭⇒⊆            : _↭_ ⇒ _⊆_
+  ⊆-respʳ-↭      : _⊆_ Respectsʳ _↭_
+  ⊆-respˡ-↭      : _⊆_ Respectsˡ _↭_
+  ⊆-↭-isPreorder : IsPreorder _↭_ _⊆_
+  ⊆-↭-preorder   : Preorder _ _ _
+
+  Any-resp-⊆     : (Any P) Respects _⊆_
+  All-resp-⊇     : (All P) Respects _⊇_
+
+  xs⊆xs++ys      : xs ⊆ xs ++ ys
+  xs⊆ys++xs      : xs ⊆ ys ++ xs
+  ++⁺ʳ           : xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
+  ++⁺ˡ           : xs ⊆ ys → xs ++ zs ⊆ ys ++ zs
+  ```
+
+* Added new proof in `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  ++↭ʳ++ : xs ++ ys ↭ xs ʳ++ ys
+  ```
+
+* Added new proof in `Data.List.Relation.Binary.Permutation.Setoi.Properties`:
+  ```agda
+  ++↭ʳ++ : xs ++ ys ↭ xs ʳ++ ys
+  ```
+
 * Added new definition in `Data.Nat.Base`:
   ```agda
   _≤ᵇ_ : (m n : ℕ) → Bool

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

@@ -17,10 +17,12 @@ open import Data.List.Base
 open import Data.List.Categorical using (monad; module MonadProperties)
 import Data.List.Properties as LP
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties
+open import Data.List.Relation.Unary.Any.Properties hiding (++-comm)
 open import Data.List.Membership.Propositional using (_∈_)
 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 as Prod hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
@@ -558,3 +560,48 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
     open Inverse
     open P.≡-Reasoning
   ... | ()
+
+
+
+------------------------------------------------------------------------
+-- Relationships to other relations
+
+module _ {a} {A : Set a} where
+
+  ↭⇒∼bag : _↭_ ⇒ _∼[ bag ]_
+  ↭⇒∼bag xs↭ys {v} = inverse (to xs↭ys) (from xs↭ys) (from∘to xs↭ys) (to∘from 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)         = 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 (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
+
+  ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_
+  ∼bag⇒↭ {[]} eq with empty-unique {A = A} (Inv.sym eq)
+  ... | refl = refl
+  ∼bag⇒↭ {x ∷ xs} eq with ∈-∃++ (to ⟨$⟩ (here P.refl))
+    where open Inv.Inverse (eq {x})
+  ... | zs₁ , zs₂ , p rewrite p = begin
+    x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (Inv._∘_ (comm zs₁ (x ∷ zs₂)) eq)) ⟩
+    x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
+    x ∷ (zs₁ ++ zs₂) ↭˘⟨ shift x zs₁ zs₂ ⟩
+    zs₁ ++ x ∷ zs₂   ∎
+    where
+    open CommutativeMonoid (commutativeMonoid bag A)
+    open PermutationReasoning