From b4295880a5500c16e5ecc4c2314102915bc175bb Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sun, 29 Dec 2024 14:02:54 +0000 Subject: [PATCH] =?UTF-8?q?[=20refactor=20]=20Move=20`Data.List.Relation.U?= =?UTF-8?q?nary.All.Properties.all=E2=8A=86concat`=20to=20`Data.List.Relat?= =?UTF-8?q?ion.Binary.Sublist.Setoid.Properties`=20(#2524)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 | 7 +++- .../Binary/Sublist/Setoid/Properties.agda | 36 +++++++++++++++++-- .../List/Relation/Unary/All/Properties.agda | 10 +----- 3 files changed, 40 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 81cd774f0a..67863f2bcf 100644 --- a/CHANGELOG.md +++ b/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 ``` diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index b42e33365d..83c42164d9 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/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,7 +24,8 @@ 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 (¬_) @@ -30,20 +33,23 @@ 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 diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index bbd027b840..7411af335f 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/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