[ add ] Module ⊆-Reasoning for Data.List.Relation.Binary.Sublist.*

CHANGELOG.md

@@ -337,15 +337,22 @@ Additions to existing modules
                                             ([] , [])
   ```
 
+* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
+  ```agda
+  module ⊆-Reasoning (≲ : Preorder a e r)
+  ```
+
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
   ```agda
   ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
   ```agda
-  concat⁺    : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
-  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
+  module ⊆-Reasoning
+  concat⁺               : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
+  all⊆concat            : (xss : List (List A)) → All (_⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda

@@ -39,6 +39,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsDecPartialOrder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
+open import Relation.Binary.Reasoning.Syntax
 
 private
   variable
@@ -470,6 +472,19 @@ decPoset ER-poset = record
   { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder
   } where module ER = DecPoset ER-poset
 
+------------------------------------------------------------------------
+-- Reasoning over sublists
+------------------------------------------------------------------------
+
+module ⊆-Reasoning (≲ : Preorder a e r) where
+
+  open ≲-Reasoning (preorder ≲) public
+    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼)
+    renaming (≲-go to ⊆-go; ≈-go to ≋-go)
+
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public
+
 ------------------------------------------------------------------------
 -- Properties of disjoint sublists
 

src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda

@@ -26,6 +26,8 @@ open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; cong; cong₂)
+import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
+open import Relation.Binary.Reasoning.Syntax
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
@@ -102,6 +104,19 @@ module _ (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) 
   ⊆-trans-assoc [] [] [] = refl
 
 
+------------------------------------------------------------------------
+-- Reasoning over sublists
+------------------------------------------------------------------------
+
+module ⊆-Reasoning where
+
+  open ≲-Reasoning ⊆-preorder public
+    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼)
+    renaming (≲-go to ⊆-go; ≈-go to ≋-go)
+
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public
+
 ------------------------------------------------------------------------
 -- Various functions' outputs are sublists
 ------------------------------------------------------------------------