{-# OPTIONS --without-K --safe #-}
open import Relation.Binary hiding (Decidable)
module Data.List.Relation.Binary.Subset.Propositional.Properties
where
open import Category.Monad
open import Data.Bool.Base using (Bool; true; false; T)
open import Data.List.Base
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties hiding (filter⁺)
open import Data.List.Categorical
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
import Data.List.Relation.Binary.Subset.Setoid.Properties as Setoidₚ
open import Data.List.Relation.Binary.Subset.Propositional
import Data.Product as Prod
import Data.Sum.Base as Sum
open import Function.Base using (_∘_; _∘′_; id; _$_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Equivalence using (module Equivalence)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Unary using (Decidable)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.PropositionalEquality
using (_≡_; _≗_; isEquivalence; refl; setoid; module ≡-Reasoning)
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
private
open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
module _ {a} {A : Set a} where
⊆-reflexive : _≡_ ⇒ (_⊆_ {A = A})
⊆-reflexive refl = id
⊆-refl : Reflexive {A = List A} _⊆_
⊆-refl x∈xs = x∈xs
⊆-trans : Transitive {A = List A} (_⊆_ {A = A})
⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs)
module _ {a} (A : Set a) where
⊆-isPreorder : IsPreorder {A = List A} _≡_ _⊆_
⊆-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ⊆-reflexive
; trans = ⊆-trans
}
⊆-preorder : Preorder _ _ _
⊆-preorder = record
{ isPreorder = ⊆-isPreorder
}
module ⊆-Reasoning {a} (A : Set a) where
open Setoidₚ.⊆-Reasoning (setoid A) public
hiding (step-≋; step-≋˘; _≋⟨⟩_)
module _ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} where
mono : xs ⊆ ys → Any P xs → Any P ys
mono xs⊆ys =
_⟨$⟩_ (Inverse.to Any↔) ∘′
Prod.map id (Prod.map xs⊆ys id) ∘
_⟨$⟩_ (Inverse.from Any↔)
module _ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} where
map-mono : xs ⊆ ys → map f xs ⊆ map f ys
map-mono xs⊆ys =
_⟨$⟩_ (Inverse.to (map-∈↔ f)) ∘
Prod.map id (Prod.map xs⊆ys id) ∘
_⟨$⟩_ (Inverse.from (map-∈↔ f))
module _ {a} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where
_++-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
_++-mono_ xs₁⊆ys₁ xs₂⊆ys₂ =
_⟨$⟩_ (Inverse.to ++↔) ∘
Sum.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
_⟨$⟩_ (Inverse.from ++↔)
module _ {a} {A : Set a} {xss yss : List (List A)} where
concat-mono : xss ⊆ yss → concat xss ⊆ concat yss
concat-mono xss⊆yss =
_⟨$⟩_ (Inverse.to $ concat-∈↔ {A = A}) ∘
Prod.map id (Prod.map id xss⊆yss) ∘
_⟨$⟩_ (Inverse.from $ concat-∈↔ {A = A})
module _ {ℓ} {A B : Set ℓ} (f g : A → List B) {xs ys} where
>>=-mono : xs ⊆ ys → (∀ {x} → f x ⊆ g x) → (xs >>= f) ⊆ (ys >>= g)
>>=-mono xs⊆ys f⊆g =
_⟨$⟩_ (Inverse.to $ >>=-∈↔ {A = A}) ∘
Prod.map id (Prod.map xs⊆ys f⊆g) ∘
_⟨$⟩_ (Inverse.from $ >>=-∈↔ {A = A})
module _ {ℓ} {A B : Set ℓ} {fs gs : List (A → B)} {xs ys : List A} where
_⊛-mono_ : fs ⊆ gs → xs ⊆ ys → (fs ⊛ xs) ⊆ (gs ⊛ ys)
_⊛-mono_ fs⊆gs xs⊆ys =
_⟨$⟩_ (Inverse.to $ ⊛-∈↔ gs) ∘
Prod.map id (Prod.map id (Prod.map fs⊆gs (Prod.map xs⊆ys id))) ∘
_⟨$⟩_ (Inverse.from $ ⊛-∈↔ fs)
module _ {ℓ} {A B : Set ℓ} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} where
_⊗-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
xs₁⊆ys₁ ⊗-mono xs₂⊆ys₂ =
_⟨$⟩_ (Inverse.to $ ⊗-∈↔ {A = A}) ∘
Prod.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
_⟨$⟩_ (Inverse.from $ ⊗-∈↔ {A = A})
module _ {a} {A : Set a} (p : A → Bool) {xs ys} where
any-mono : xs ⊆ ys → T (any p xs) → T (any p ys)
any-mono xs⊆ys =
_⟨$⟩_ (Equivalence.to any⇔) ∘
mono xs⊆ys ∘
_⟨$⟩_ (Equivalence.from any⇔)
module _ {a b} {A : Set a} {B : Set b}
{xs : List A} {f : ∀ {x} → x ∈ xs → B}
{ys : List A} {g : ∀ {x} → x ∈ ys → B} where
map-with-∈-mono : (xs⊆ys : xs ⊆ ys) → (∀ {x} → f {x} ≗ g ∘ xs⊆ys) →
map-with-∈ xs f ⊆ map-with-∈ ys g
map-with-∈-mono xs⊆ys f≈g {x} =
_⟨$⟩_ (Inverse.to map-with-∈↔) ∘
Prod.map id (Prod.map xs⊆ys (λ {x∈xs} x≡fx∈xs → begin
x ≡⟨ x≡fx∈xs ⟩
f x∈xs ≡⟨ f≈g x∈xs ⟩
g (xs⊆ys x∈xs) ∎)) ∘
_⟨$⟩_ (Inverse.from map-with-∈↔)
where open ≡-Reasoning
module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where
filter⁺ : ∀ xs → filter P? xs ⊆ xs
filter⁺ = Setoidₚ.filter⁺ (setoid A) P?
boolFilter-⊆ : ∀ {a} {A : Set a} (p : A → Bool) →
(xs : List A) → boolFilter p xs ⊆ xs
boolFilter-⊆ p (x ∷ xs) with p x | boolFilter-⊆ p xs
... | false | hyp = there ∘ hyp
... | true | hyp =
λ { (here eq) → here eq
; (there ∈boolFilter) → there (hyp ∈boolFilter)
}
{-# WARNING_ON_USAGE boolFilter-⊆
"Warning: boolFilter was deprecated in v0.15.
Please use filter instead."
#-}