------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the extensional sublist relation over setoid equality.
------------------------------------------------------------------------

{-# 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 Function.Base using (_∘_; _∘₂_; _$_)
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 Setoid using (Carrier)

private
  variable
    a b p q r ℓ : Level

------------------------------------------------------------------------
-- Relational properties with _≋_ (pointwise equality)
------------------------------------------------------------------------

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
    }

------------------------------------------------------------------------
-- Relational properties with _↭_ (permutations)
------------------------------------------------------------------------

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
    }

------------------------------------------------------------------------
-- Reasoning over subsets
------------------------------------------------------------------------

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

------------------------------------------------------------------------
-- Relationship with other binary relations
------------------------------------------------------------------------

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)

------------------------------------------------------------------------
-- Relationship with predicates
------------------------------------------------------------------------

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 ∘ ⊇)

------------------------------------------------------------------------
-- Properties of list functions
------------------------------------------------------------------------
-- ∷

module _ (S : Setoid a ℓ) where

  open Setoid S
  open Subset S
  open Membership S
  open Membershipₚ

  xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
  xs⊆x∷xs xs x = there

  ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
  ∷⁺ʳ x xs⊆ys (here  p) = here p
  ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)

  ∈-∷⁺ʳ : ∀ {xs ys x} → 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

------------------------------------------------------------------------
-- ++

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)

------------------------------------------------------------------------
-- map

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))

------------------------------------------------------------------------
-- reverse

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

-- NB. the unit and counit of this adjunction are given by:
-- reverse-η : ∀ {xs} → xs ⊆ reverse xs
-- reverse-η = Membershipₚ.reverse⁺ S
-- reverse-ε : ∀ {xs} → reverse xs ⊆ xs
-- 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

------------------------------------------------------------------------
-- filter

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])

  -- Should be known as `filter⁺` (no prime) but `filter-⊆` used
  -- to be called this so for backwards compatability reasons, the
  -- correct name will have to wait until the deprecated name is
  -- removed.
  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)

------------------------------------------------------------------------
-- applyUpTo

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)


------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------

-- Version 1.5

filter⁺ = filter-⊆
{-# WARNING_ON_USAGE filter⁺
"Warning: filter⁺ was deprecated in v1.5.
Please use filter-⊆ instead."
#-}