{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Subset.Setoid.Properties where
open import Data.Bool.Base using (Bool; true; false)
open import Data.List.Base hiding (_∷ʳ_; find)
import Data.List.Properties as List
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Relation.Unary.All as All using (All)
import Data.List.Membership.Setoid as Membership
import Data.List.Membership.Setoid.Properties as Membershipₚ
open import Data.Nat.Base using (ℕ; s≤s; _≤_)
import Data.List.Relation.Binary.Subset.Setoid as Subset
import Data.List.Relation.Binary.Sublist.Setoid as Sublist
import Data.List.Relation.Binary.Equality.Setoid as Equality
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ
open import Data.Product.Base using (_,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
open import Level using (Level)
open import Relation.Nullary using (¬_; does; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary using (Pred; Decidable) renaming (_⊆_ to _⋐_)
open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)
open import Relation.Binary.Definitions
using (Reflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects_)
open import Relation.Binary.Bundles using (Setoid; Preorder)
open import Relation.Binary.Structures using (IsPreorder)
import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
open import Relation.Binary.Reasoning.Syntax
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open Setoid using (Carrier)
private
variable
a b p q r ℓ : Level
module _ (S : Setoid a ℓ) where
open Setoid S using (refl)
open Subset S
∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
∷⊈[] p = Membershipₚ.∉[] S $ p (here refl)
⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
⊆[]⇒≡[] {x = []} _ = ≡.refl
⊆[]⇒≡[] {x = _ ∷ _} p with () ← ∷⊈[] p
module _ (S : Setoid a ℓ) where
open Subset S
open Equality S
open Membership S
open Membershipₚ
⊆-reflexive : _≋_ ⇒ _⊆_
⊆-reflexive xs≋ys = ∈-resp-≋ S xs≋ys
⊆-refl : Reflexive _⊆_
⊆-refl x∈xs = x∈xs
⊆-trans : Transitive _⊆_
⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs)
⊆-respʳ-≋ : _⊆_ Respectsʳ _≋_
⊆-respʳ-≋ xs≋ys = ∈-resp-≋ S xs≋ys ∘_
⊆-respˡ-≋ : _⊆_ Respectsˡ _≋_
⊆-respˡ-≋ xs≋ys = _∘ ∈-resp-≋ S (≋-sym xs≋ys)
⊆-isPreorder : IsPreorder _≋_ _⊆_
⊆-isPreorder = record
{ isEquivalence = ≋-isEquivalence
; reflexive = ⊆-reflexive
; trans = ⊆-trans
}
⊆-preorder : Preorder _ _ _
⊆-preorder = record
{ isPreorder = ⊆-isPreorder
}
module _ (S : Setoid a ℓ) where
open Subset S
open Permutation S
open Membership S
⊆-reflexive-↭ : _↭_ ⇒ _⊆_
⊆-reflexive-↭ xs↭ys = Permutationₚ.∈-resp-↭ S xs↭ys
⊆-respʳ-↭ : _⊆_ Respectsʳ _↭_
⊆-respʳ-↭ xs↭ys = Permutationₚ.∈-resp-↭ S xs↭ys ∘_
⊆-respˡ-↭ : _⊆_ Respectsˡ _↭_
⊆-respˡ-↭ xs↭ys = _∘ Permutationₚ.∈-resp-↭ S (↭-sym xs↭ys)
⊆-↭-isPreorder : IsPreorder _↭_ _⊆_
⊆-↭-isPreorder = record
{ isEquivalence = ↭-isEquivalence
; reflexive = ⊆-reflexive-↭
; trans = ⊆-trans S
}
⊆-↭-preorder : Preorder _ _ _
⊆-↭-preorder = record
{ isPreorder = ⊆-↭-isPreorder
}
module ⊆-Reasoning (S : Setoid a ℓ) where
open Membership S using (_∈_)
private module Base = ≲-Reasoning (⊆-preorder S)
open Base public
hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼)
renaming (≲-go to ⊆-go; ≈-go to ≋-go)
open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → Base.begin x) public
open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public
module _ (S : Setoid a ℓ) where
open Setoid S
open Subset S
open Sublist S renaming (_⊆_ to _⊑_)
Sublist⇒Subset : ∀ {xs ys} → xs ⊑ ys → xs ⊆ ys
Sublist⇒Subset (x≈y ∷ xs⊑ys) (here v≈x) = here (trans v≈x x≈y)
Sublist⇒Subset (x≈y ∷ xs⊑ys) (there v∈xs) = there (Sublist⇒Subset xs⊑ys v∈xs)
Sublist⇒Subset (y ∷ʳ xs⊑ys) v∈xs = there (Sublist⇒Subset xs⊑ys v∈xs)
module _ (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open Subset S
open Membership S
Any-resp-⊆ : ∀ {P : Pred A p} → P Respects _≈_ → (Any P) Respects _⊆_
Any-resp-⊆ resp ⊆ pxs with find pxs
... | (x , x∈xs , px) = lose resp (⊆ x∈xs) px
All-resp-⊇ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _⊇_
All-resp-⊇ resp ⊇ pxs = All.tabulateₛ S (All.lookupₛ S resp pxs ∘ ⊇)
module _ (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open Subset S
open Membership S
open Membershipₚ
xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
xs⊆x∷xs xs x = there
private variable
x y : A
xs ys : List A
∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
∷⁺ʳ x xs⊆ys (here p) = here p
∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
∈-∷⁺ʳ : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
∈-∷⁺ʳ x∈ys _ (here v≈x) = ∈-resp-≈ S (sym v≈x) x∈ys
∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
⊆∷⇒∈∨⊆ {xs = []} []⊆y∷ys = inj₂ λ ()
⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there
... | inj₁ y∈xs = inj₁ $ there y∈xs
... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl)
... | here x≈y = inj₁ $ here (sym x≈y)
... | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys)
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys
... | inj₁ y∈xs = contradiction y∈xs y∉xs
... | inj₂ xs⊆ys = xs⊆ys
module _ (S : Setoid a ℓ) where
open Subset S
open Membership S
open Membershipₚ
xs⊆xs++ys : ∀ xs ys → xs ⊆ xs ++ ys
xs⊆xs++ys xs ys = ∈-++⁺ˡ S
xs⊆ys++xs : ∀ xs ys → xs ⊆ ys ++ xs
xs⊆ys++xs xs ys = ∈-++⁺ʳ S _
++⁺ʳ : ∀ {xs ys} zs → xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
++⁺ʳ [] xs⊆ys = xs⊆ys
++⁺ʳ (x ∷ zs) xs⊆ys (here p) = here p
++⁺ʳ (x ∷ zs) xs⊆ys (there p) = there (++⁺ʳ zs xs⊆ys p)
++⁺ˡ : ∀ {xs ys} zs → xs ⊆ ys → xs ++ zs ⊆ ys ++ zs
++⁺ˡ {[]} {ys} zs xs⊆ys = xs⊆ys++xs zs ys
++⁺ˡ {x ∷ xs} {ys} zs xs⊆ys (here p) = xs⊆xs++ys ys zs (xs⊆ys (here p))
++⁺ˡ {x ∷ xs} {ys} zs xs⊆ys (there p) = ++⁺ˡ zs (xs⊆ys ∘ there) p
++⁺ : ∀ {ws xs ys zs} → ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs
++⁺ ws⊆xs ys⊆zs = ⊆-trans S (++⁺ˡ _ ws⊆xs) (++⁺ʳ _ ys⊆zs)
module _ (S : Setoid a ℓ) (R : Setoid b r) where
private
module S = Setoid S
module R = Setoid R
module S⊆ = Subset S
module R⊆ = Subset R
open Membershipₚ
map⁺ : ∀ {as bs} {f : S.Carrier → R.Carrier} →
f Preserves S._≈_ ⟶ R._≈_ →
as S⊆.⊆ bs → map f as R⊆.⊆ map f bs
map⁺ {f = f} f-pres as⊆bs v∈f[as] =
let x , x∈as , v≈f[x] = ∈-map⁻ S R v∈f[as] in
∈-resp-≈ R (R.sym v≈f[x]) (∈-map⁺ S R f-pres (as⊆bs x∈as))
module _ (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open Subset S
reverse-selfAdjoint : ∀ {as bs} → as ⊆ reverse bs → reverse as ⊆ bs
reverse-selfAdjoint rs = reverse⁻ ∘ rs ∘ reverse⁻
where reverse⁻ = Membershipₚ.reverse⁻ S
reverse⁺ : ∀ {as bs} → as ⊆ bs → reverse as ⊆ reverse bs
reverse⁺ {as} {bs} rs = reverse-selfAdjoint $ begin
as ⊆⟨ rs ⟩
bs ≡⟨ List.reverse-involutive bs ⟨
reverse (reverse bs) ∎
where open ⊆-Reasoning S
reverse⁻ : ∀ {as bs} → reverse as ⊆ reverse bs → as ⊆ bs
reverse⁻ {as} {bs} rs = begin
as ≡⟨ List.reverse-involutive as ⟨
reverse (reverse as) ⊆⟨ reverse-selfAdjoint rs ⟩
bs ∎
where open ⊆-Reasoning S
module _ (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open Subset S
open Membershipₚ
filter-⊆ : ∀ {P : Pred A p} (P? : Decidable P) →
∀ xs → filter P? xs ⊆ xs
filter-⊆ P? (x ∷ xs) y∈f[x∷xs] with does (P? x)
... | false = there (filter-⊆ P? xs y∈f[x∷xs])
... | true with y∈f[x∷xs]
... | here y≈x = here y≈x
... | there y∈f[xs] = there (filter-⊆ P? xs y∈f[xs])
filter⁺′ : ∀ {P : Pred A p} (P? : Decidable P) → P Respects _≈_ →
∀ {Q : Pred A q} (Q? : Decidable Q) → Q Respects _≈_ →
P ⋐ Q → ∀ {xs ys} → xs ⊆ ys → filter P? xs ⊆ filter Q? ys
filter⁺′ P? P-resp Q? Q-resp P⋐Q xs⊆ys v∈fxs with ∈-filter⁻ S P? P-resp v∈fxs
... | v∈xs , Pv = ∈-filter⁺ S Q? Q-resp (xs⊆ys v∈xs) (P⋐Q Pv)
module _ (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open Subset S
applyUpTo⁺ : ∀ (f : ℕ → A) {m n} → m ≤ n → applyUpTo f m ⊆ applyUpTo f n
applyUpTo⁺ _ (s≤s m≤n) (here f≡f[0]) = here f≡f[0]
applyUpTo⁺ _ (s≤s m≤n) (there v∈xs) = there (applyUpTo⁺ _ m≤n v∈xs)
filter⁺ = filter-⊆
{-# WARNING_ON_USAGE filter⁺
"Warning: filter⁺ was deprecated in v1.5.
Please use filter-⊆ instead."
#-}