------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of lists which contain every element of a given type
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.List.Base
open import Data.List.Membership.Setoid.Properties as Membership
open import Data.List.Relation.Unary.Any using (index)
open import Data.List.Relation.Unary.Any.Properties using (lookup-index)
open import Data.List.Relation.Unary.Enumerates.Setoid
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Sum.Relation.Binary.Pointwise
  using (_⊎ₛ_; inj₁; inj₂)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
  using (_×ₛ_)
open import Function.Base using (_∘_)
open import Function.Bundles using (Surjection)
open import Function.Definitions using (Surjective)
open import Function.Consequences using (strictlySurjective⇒surjective)
open import Level
open import Relation.Binary.Bundles using (Setoid; DecSetoid)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Properties.Setoid using (respʳ-flip)

module Data.List.Relation.Unary.Enumerates.Setoid.Properties where


private
  variable
    a b ℓ₁ ℓ₂ : Level

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

module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) where
  open Surjection surj

  map⁺ : ∀ {xs} → IsEnumeration S xs → IsEnumeration T (map to xs)
  map⁺ _∈xs y with strictlySurjective y
  ... | (x , fx≈y) = ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs))

------------------------------------------------------------------------
-- _++_

module _ (S : Setoid a ℓ₁) where

  ++⁺ˡ : ∀ {xs} ys → IsEnumeration S xs → IsEnumeration S (xs ++ ys)
  ++⁺ˡ _ _∈xs v = Membership.∈-++⁺ˡ S (v ∈xs)

  ++⁺ʳ : ∀ xs {ys} → IsEnumeration S ys → IsEnumeration S (xs ++ ys)
  ++⁺ʳ _ _∈ys v = Membership.∈-++⁺ʳ S _ (v ∈ys)

module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where

  ++⁺ : ∀ {xs ys} → IsEnumeration S xs → IsEnumeration T ys →
        IsEnumeration (S ⊎ₛ T) (map inj₁ xs ++ map inj₂ ys)
  ++⁺ _∈xs _ (inj₁ x) = ∈-++⁺ˡ (S ⊎ₛ T)   (∈-map⁺ S (S ⊎ₛ T) inj₁ (x ∈xs))
  ++⁺ _ _∈ys (inj₂ y) = ∈-++⁺ʳ (S ⊎ₛ T) _ (∈-map⁺ T (S ⊎ₛ T) inj₂ (y ∈ys))

------------------------------------------------------------------------
-- cartesianProduct

module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where

  cartesianProduct⁺ : ∀ {xs ys} → IsEnumeration S xs → IsEnumeration T ys →
                      IsEnumeration (S ×ₛ T) (cartesianProduct xs ys)
  cartesianProduct⁺ _∈xs _∈ys (x , y) = ∈-cartesianProduct⁺ S T (x ∈xs) (y ∈ys)

------------------------------------------------------------------------
-- deduplicate

module _ (S? : DecSetoid a ℓ₁) where
  open DecSetoid S? renaming (setoid to S)

  deduplicate⁺ : ∀ {xs} → IsEnumeration S xs →
                 IsEnumeration S (deduplicate _≟_ xs)
  deduplicate⁺ = ∈-deduplicate⁺ S _≟_ (respʳ-flip S) ∘_

------------------------------------------------------------------------
-- lookup

module _ (S : Setoid a ℓ₁) where
  open Setoid S

  lookup-surjective : ∀ {xs} → IsEnumeration S xs →
                      Surjective _≡_ _≈_ (lookup xs)
  lookup-surjective _∈xs = strictlySurjective⇒surjective
    trans (λ { P.refl → refl}) (λ y → index (y ∈xs) , sym (lookup-index (y ∈xs)))