------------------------------------------------------------------------
-- 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)
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
open import Data.List.Membership.Setoid.Properties
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 (_⇒_)
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 PreorderReasoning

open Setoid using (Carrier)

private
  variable
    a p q  : Level

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

module _ (S : Setoid a ) where

  open Subset S
  open Equality S
  open Membership S

  ⊆-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 Setoid S renaming (Carrier to A)
  open Subset S
  open Membership S

  private
    module Base = PreorderReasoning (⊆-preorder S)

  open Base public
    hiding (step-∼; step-≈; step-≈˘)

  infixr 2 step-⊆ step-≋ step-≋˘
  infix 1 step-∈

  step-∈ :  x {xs ys}  xs IsRelatedTo ys  x  xs  x  ys
  step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs

  step-⊆  = Base.step-∼
  step-≋  = Base.step-≈
  step-≋˘ = Base.step-≈˘

  syntax step-∈  x  xs⊆ys x∈xs  = x  ∈⟨  x∈xs   xs⊆ys
  syntax step-⊆  xs ys⊆zs xs⊆ys = xs ⊆⟨  xs⊆ys  ys⊆zs
  syntax step-≋  xs ys⊆zs xs≋ys = xs ≋⟨  xs≋ys  ys⊆zs
  syntax step-≋˘ xs ys⊆zs xs≋ys = xs ≋˘⟨ xs≋ys  ys⊆zs

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

  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

  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)

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

module _ (S : Setoid a ) where

  open Setoid S renaming (Carrier to A)
  open Subset S

  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."
#-}