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

#2527) * add: `⊆-Reasoning` on the model of `Subset` * fix title comment * add: `Heterogeneous.Properties.⊆-Reasoning` * fixed `CHANGELOG` * fixed `CHANGELOG`: added missing lemma name from #2517 * oops: fixed `import` * reduce code duplication * refactor: pick the correct `preorder` * do not hide the useful reasoning combinators. Also the ≋-syntax needed a 4th argument. * tidied up symmetry proof * `fix-whitespace` --------- Co-authored-by: Jacques Carette <[email protected]>
agda · Jan 3, 2025 · 4a8cd32 · 4a8cd32
1 parent 11d0a33
commit 4a8cd32
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 5 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -418,6 +418,8 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
   ```agda
   Sublist-[]-universal : Universal (Sublist R [])
+
+  module ⊆-Reasoning (≲ : Preorder a e r)
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
@@ -429,8 +431,11 @@ Additions to existing modules
   ```agda
   []⊆-universal : Universal ([] ⊆_)
 
-  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.Binary.Subset.Propositional.Properties`:

diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/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,20 @@ 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 Preorder ≲ using (module Eq)
+
+  open ≲-Reasoning (preorder ≲) public
+    renaming (≲-go to ⊆-go; ≈-go to ≋-go)
+
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go (Pw.symmetric Eq.sym) public
+
 ------------------------------------------------------------------------
 -- Properties of disjoint sublists
 

diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -24,8 +24,11 @@ open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
+import Relation.Binary.Properties.Setoid as SetoidProperties
 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 (¬_)
@@ -42,6 +45,7 @@ import Data.List.Membership.Setoid as SetoidMembership
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
 open SetoidEquality S using (_≋_; ≋-refl; ≋-reflexive; ≋-setoid)
 open SetoidSublist S hiding (map)
+open SetoidProperties S using (≈-preorder)
 
 
 private
@@ -102,6 +106,12 @@ module _ (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z)
   ⊆-trans-assoc [] [] [] = refl
 
 
+------------------------------------------------------------------------
+-- Reasoning over sublists
+------------------------------------------------------------------------
+
+module ⊆-Reasoning = HeteroProperties.⊆-Reasoning ≈-preorder
+
 ------------------------------------------------------------------------
 -- Various functions' outputs are sublists
 ------------------------------------------------------------------------
@@ -196,9 +206,11 @@ module _ where
     renaming (map to map-≋; from∈ to from∈-≋)
 
   xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
-  xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
-    = ⊆-trans (⊆-reflexive (≋-reflexive (sym (++-identityʳ xs))))
-              (concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)))
+  xs∈xss⇒xs⊆concat[xss] {xs = xs} {xss = xss} xs∈xss = begin
+    xs ≈⟨ ≋-reflexive (++-identityʳ xs) ⟨
+    xs ++ [] ⊆⟨ concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)) ⟩
+    concat xss ∎
+    where open ⊆-Reasoning
 
   all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
   all⊆concat _ = tabulateₛ ≋-setoid xs∈xss⇒xs⊆concat[xss]