------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of membership for AVL sets
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.Tree.AVL.Sets.Membership.Properties
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Data.Bool.Base using (true; false)
open import Data.Product.Base as Prod using (_,_; proj₁; proj₂)
open import Data.Sum.Base as Sum using (_⊎_)
open import Data.Unit.Base using (tt)
open import Function.Base using (_∘_; _∘′_; const)

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Nullary using (¬_; yes; no; Reflects)
open import Relation.Nullary.Reflects using (fromEquivalence)

open StrictTotalOrder strictTotalOrder renaming (Carrier to A)
open import Data.Tree.AVL.Sets strictTotalOrder
open import Data.Tree.AVL.Sets.Membership strictTotalOrder
open import Data.Tree.AVL.Map.Membership.Propositional strictTotalOrder using (_∈ₖᵥ_)
import Data.Tree.AVL.Map.Membership.Propositional.Properties strictTotalOrder as Map
open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ

private
  variable
    x y : A
    s : ⟨Set⟩

∈toMap : x ∈ s → (x , tt) ∈ₖᵥ s
∈toMap = Mapₚ.map (_, refl)

∈fromMap : (x , tt) ∈ₖᵥ s → x ∈ s
∈fromMap = Mapₚ.map proj₁

------------------------------------------------------------------------
-- empty

∈-empty : x ∉ empty
∈-empty = Map.∈ₖᵥ-empty ∘ ∈toMap

------------------------------------------------------------------------
-- singleton

∈-singleton⁺ : x ∈ singleton x
∈-singleton⁺ = ∈fromMap Map.∈ₖᵥ-singleton⁺

∈-singleton⁻ : x ∈ singleton y → x ≈ y
∈-singleton⁻ p = proj₁ (Map.∈ₖᵥ-singleton⁻ (∈toMap p))

------------------------------------------------------------------------
-- insert

∈-insert⁺ : x ∈ s → x ∈ insert y s
∈-insert⁺ {x = x} {s = s} {y = y} x∈s with x ≟ y
... | yes x≈y = ∈fromMap (Map.∈ₖᵥ-Respectsˡ (Eq.sym x≈y , refl) Map.∈ₖᵥ-insert⁺⁺)
... | no x≉y = ∈fromMap (Map.∈ₖᵥ-insert⁺ x≉y (∈toMap x∈s))

∈-insert⁺⁺ : x ∈ insert x s
∈-insert⁺⁺ = ∈fromMap Map.∈ₖᵥ-insert⁺⁺

∈-insert⁻ : x ∈ insert y s → x ≈ y ⊎ x ∈ s
∈-insert⁻ = Sum.map proj₁ (∈fromMap ∘ proj₂) ∘ Map.∈ₖᵥ-insert⁻ ∘ ∈toMap

------------------------------------------------------------------------
-- member

∈-member : x ∈ s → member x s ≡ true
∈-member = Map.∈ₖᵥ-member ∘′ ∈toMap

∉-member : x ∉ s → member x s ≡ false
∉-member x∉s = Map.∉ₖᵥ-member (const (x∉s ∘ ∈fromMap))

member-∈ : member x s ≡ true → x ∈ s
member-∈ = ∈fromMap ∘′ proj₂ ∘′ Map.member-∈ₖᵥ

member-∉ : member x s ≡ false → x ∉ s
member-∉ p = Map.member-∉ₖᵥ p tt ∘ ∈toMap

member-Reflects-∈ : Reflects (x ∈ s) (member x s)
member-Reflects-∈ {x = x} {s = s} with member x s in eq
... | true = Reflects.ofʸ (member-∈ eq)
... | false = Reflects.ofⁿ (member-∉ eq)