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

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

open import Relation.Binary using (StrictTotalOrder)

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

open import Data.Bool.Base using (true; false)
open import Data.Product 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 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ₚ

    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)