[ refactor ] Move `Data.List.Relation.Unary.All.Properties.all⊆concat…

…` to `Data.List.Relation.Binary.Sublist.Setoid.Properties` (#2524)

* refactor: prepare for code migration

* refactor: move code as is

* refactor: add new lemmas to `Setoid` and `Propositional`

* refactor: use new lemmas

* refactor: localise appeals to `SetoidMembership`; pull lemma back to `SetoidProperties`

* refactor: pull `all⊆concat` back to `Setoid.Properties`

* refactor: tidy up

* refactor: tidy up

* refactor: tidy up

* refactor: tidy up

* refactor: make proof `rewrite`-free

* oops: uncommitted file save

* tighten `import`s

CHANGELOG.md

@@ -342,9 +342,14 @@ Additions to existing modules
   ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
   ```
 
-* In `Data.List.Relation.Unary.All.Properties`:
+* 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
+  ```
+
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
   all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
   all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
   ```

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

@@ -13,7 +13,9 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ) where
 
 open import Data.List.Base hiding (_∷ʳ_)
+open import Data.List.Properties using (++-identityʳ)
 open import Data.List.Relation.Unary.Any using (Any)
+open import Data.List.Relation.Unary.All using (All; tabulateₛ)
 import Data.Maybe.Relation.Unary.All as Maybe
 open import Data.Nat.Base using (ℕ; _≤_; _≥_)
 import Data.Nat.Properties as ℕ
@@ -22,28 +24,32 @@ open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+  using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (¬?; yes; no)
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
+import Data.List.Relation.Binary.Sublist.Heterogeneous
+  as Hetero
 import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
   as HeteroProperties
 import Data.List.Membership.Setoid as SetoidMembership
 
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
-open SetoidEquality S using (_≋_; ≋-refl)
+open SetoidEquality S using (_≋_; ≋-refl; ≋-reflexive; ≋-setoid)
 open SetoidSublist S hiding (map)
-open SetoidMembership S using (_∈_)
+
 
 private
   variable
     p q r s t : Level
     a b x y : A
     as bs cs ds xs ys : List A
+    xss yss : List (List A)
     P : Pred A p
     Q : Pred A q
     m n : ℕ
@@ -175,6 +181,28 @@ module _ where
   ++⁻ : length as ≡ length bs → as ++ cs ⊆ bs ++ ds → cs ⊆ ds
   ++⁻ = HeteroProperties.++⁻
 
+------------------------------------------------------------------------
+-- concat
+
+module _ where
+
+  concat⁺ : Hetero.Sublist _⊆_ xss yss →
+            concat xss ⊆ concat yss
+  concat⁺ = HeteroProperties.concat⁺
+
+  open SetoidMembership ≋-setoid using (_∈_)
+  open SetoidSublist ≋-setoid
+    using ()
+    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)))
+
+  all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
+  all⊆concat _ = tabulateₛ ≋-setoid xs∈xss⇒xs⊆concat[xss]
+
 ------------------------------------------------------------------------
 -- take
 
@@ -306,6 +334,8 @@ module _ where
 
 module _ where
 
+  open SetoidMembership S using (_∈_)
+
   to∈-injective : ∀ {p q : [ x ] ⊆ xs} → to∈ p ≡ to∈ q → p ≡ q
   to∈-injective = HeteroProperties.toAny-injective
 

src/Data/List/Relation/Unary/All/Properties.agda

@@ -20,9 +20,6 @@ import Data.List.Membership.Setoid as SetoidMembership
 import Data.List.Properties as List
 import Data.List.Relation.Binary.Equality.Setoid as ≋
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-import Data.List.Relation.Binary.Sublist.Propositional as Sublist
-import Data.List.Relation.Binary.Sublist.Propositional.Properties
-  as Sublist
 import Data.List.Relation.Binary.Subset.Propositional as Subset
 open import Data.List.Relation.Unary.All as All using
   ( All; []; _∷_; lookup; updateAt
@@ -49,7 +46,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private
@@ -388,11 +385,6 @@ concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
 concat⁻ {xss = []}       []  = []
 concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)
 
-all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
-all⊆concat [] = []
-all⊆concat (xs ∷ xss) =
-  Sublist.++⁺ʳ (concat xss) Sublist.⊆-refl ∷ All.map (Sublist.++⁺ˡ xs) (all⊆concat xss)
-
 ------------------------------------------------------------------------
 -- snoc