------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where at least one element satisfies a given property
------------------------------------------------------------------------

module Data.List.Any where

open import Data.Empty
open import Data.Fin
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv using (module Equivalence)
open import Function.Related as Related hiding (_∼[_]_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Product as Prod using (; _×_; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
open import Relation.Binary hiding (Decidable)
import Relation.Binary.InducedPreorders as Ind
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_)

-- Any P xs means that at least one element in xs satisfies P.

data Any {a p} {A : Set a}
         (P : A  Set p) : List A  Set (a  p) where
  here  :  {x xs} (px  : P x)       Any P (x  xs)
  there :  {x xs} (pxs : Any P xs)  Any P (x  xs)

-- Map.

map :  {a p q} {A : Set a} {P : A  Set p}  {Q : A  Set q} 
      P  Q  Any P  Any Q
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

-- If the head does not satisfy the predicate, then the tail will.

tail :  {a p} {A : Set a} {x : A} {xs : List A} {P : A  Set p} 
       ¬ P x  Any P (x  xs)  Any P xs
tail ¬px (here  px)  = ⊥-elim (¬px px)
tail ¬px (there pxs) = pxs

-- Decides Any.

any :  {a p} {A : Set a} {P : A  Set p} 
      Decidable P  Decidable (Any P)
any p []       = no λ()
any p (x  xs) with p x
any p (x  xs) | yes px = yes (here px)
any p (x  xs) | no ¬px = Dec.map′ there (tail ¬px) (any p xs)

-- index x∈xs is the list position (zero-based) which x∈xs points to.

index :  {a p} {A : Set a} {P : A  Set p} {xs} 
        Any P xs  Fin (List.length xs)
index (here  px)  = zero
index (there pxs) = suc (index pxs)

------------------------------------------------------------------------
-- List membership and some related definitions

module Membership {c  : Level} (S : Setoid c ) where

  private
    open module  S = Setoid S using (_≈_) renaming (Carrier to A)
    open module LS = Setoid (ListEq.setoid S)
      using () renaming (_≈_ to _≋_)

  -- If a predicate P respects the underlying equality then Any P
  -- respects the list equality.

  lift-resp :  {p} {P : A  Set p} 
              P Respects _≈_  Any P Respects _≋_
  lift-resp resp []            ()
  lift-resp resp (x≈y  xs≈ys) (here px)   = here (resp x≈y px)
  lift-resp resp (x≈y  xs≈ys) (there pxs) =
    there (lift-resp resp xs≈ys pxs)

  -- List membership.

  infix 4 _∈_ _∉_

  _∈_ : A  List A  Set _
  x  xs = Any (_≈_ x) xs

  _∉_ : A  List A  Set _
  x  xs = ¬ x  xs

  -- Subsets.

  infix 4 _⊆_ _⊈_

  _⊆_ : List A  List A  Set _
  xs  ys =  {x}  x  xs  x  ys

  _⊈_ : List A  List A  Set _
  xs  ys = ¬ xs  ys

  -- Equality is respected by the predicate which is used to define
  -- _∈_.

  ∈-resp-≈ :  {x}  (_≈_ x) Respects _≈_
  ∈-resp-≈ = flip S.trans

  -- List equality is respected by _∈_.

  ∈-resp-list-≈ :  {x}  _∈_ x Respects _≋_
  ∈-resp-list-≈ = lift-resp ∈-resp-≈

  -- _⊆_ is a preorder.

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = Ind.InducedPreorder₂ (ListEq.setoid S) _∈_ ∈-resp-list-≈

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    open PreR ⊆-preorder public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

    infix 1 _∈⟨_⟩_

    _∈⟨_⟩_ :  x {xs ys}  x  xs  xs IsRelatedTo ys  x  ys
    x ∈⟨ x∈xs  xs⊆ys = (begin xs⊆ys) x∈xs

  -- A variant of List.map.

  map-with-∈ :  {b} {B : Set b}
               (xs : List A)  (∀ {x}  x  xs  B)  List B
  map-with-∈ []       f = []
  map-with-∈ (x  xs) f = f (here S.refl)  map-with-∈ xs (f  there)

  -- Finds an element satisfying the predicate.

  find :  {p} {P : A  Set p} {xs} 
         Any P xs   λ x  x  xs × P x
  find (here px)   = (_ , here S.refl , px)
  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)

  lose :  {p} {P : A  Set p} {x xs} 
         P Respects _≈_  x  xs  P x  Any P xs
  lose resp x∈xs px = map (flip resp px) x∈xs

-- The code above instantiated (and slightly changed) for
-- propositional equality, along with some additional definitions.

module Membership-≡ where

  private
    open module M {a} {A : Set a} = Membership (PropEq.setoid A) public
      hiding (lift-resp; lose; ⊆-preorder; module ⊆-Reasoning)

  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 4 _∼[_]_

  _∼[_]_ :  {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 2 _∼⟨_⟩_
    infix  1 _∈⟨_⟩_

    _∈⟨_⟩_ :  {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

------------------------------------------------------------------------
-- Another function

-- If any element satisfies P, then P is satisfied.

satisfied :  {a p} {A : Set a} {P : A  Set p} {xs} 
            Any P xs   P
satisfied = Prod.map id Prod.proj₂  Membership-≡.find