------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------

module Data.List.Any.Membership.Propositional where

open import Data.Empty
open import Data.Fin
open import Function.Inverse using (_↔_)
open import Function.Related as Related hiding (_∼[_]_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Any using (Any; map)
import Data.List.Any.Membership as Membership
open import Data.List.Relation.Pointwise as ListEq using ([]; _∷_)
open import Data.Product as Prod using (∃; _×_; _,_; uncurry′; proj₂)
open import Relation.Nullary
open import Relation.Binary hiding (Decidable)
import Relation.Binary.InducedPreorders as Ind
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_)

private module M {a} {A : Set a} = Membership (PropEq.setoid A)
open M public hiding (lose)

lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
       x ∈ xs → P x → Any P xs
lose {P = P} = M.lose (PropEq.subst P)

-- _⊆_ is a preorder.

⊆-preorder : ∀ {a} → Set a → Preorder _ _ _
⊆-preorder A = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_
                                      (PropEq.subst (_∈_ _))

-- Set and bag equality and related preorders.

open Related public
  using (Kind; Symmetric-kind)
   renaming ( implication         to subset
            ; reverse-implication to superset
            ; equivalence         to set
            ; injection           to subbag
            ; reverse-injection   to superbag
            ; bijection           to bag
            )

[_]-Order : Kind → ∀ {a} → Set a → Preorder _ _ _
[ k ]-Order A = Related.InducedPreorder₂ k (_∈_ {A = A})

[_]-Equality : Symmetric-kind → ∀ {a} → Set a → Setoid _ _
[ k ]-Equality A = Related.InducedEquivalence₂ k (_∈_ {A = A})

infix  _∼[_]_

_∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
_∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys

-- Bag equality implies the other relations.

bag-=⇒ : ∀ {k a} {A : Set a} {xs ys : List A} →
         xs ∼[ bag ] ys → xs ∼[ k ] ys
bag-=⇒ xs≈ys = ↔⇒ xs≈ys

-- "Equational" reasoning for _⊆_.

module ⊆-Reasoning where
  import Relation.Binary.PreorderReasoning as PreR
  private
    open module PR {a} {A : Set a} = PreR (⊆-preorder A) public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)

  infixr  _∼⟨_⟩_
  infix   _∈⟨_⟩_

  _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} →
           x ∈ xs → xs IsRelatedTo ys → x ∈ ys
  x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

  _∼⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} →
           xs ∼[ ⌊ k ⌋→ ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs
  xs ∼⟨ xs≈ys ⟩ ys≈zs = xs ⊆⟨ ⇒→ xs≈ys ⟩ ys≈zs