    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of the membership relation for AVL Maps identifying values
    -- up to propositional equality.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (StrictTotalOrder)

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

    open import Data.Bool.Base using (true; false)
    open import Data.Maybe.Base using (just; nothing; is-just)
    open import Data.Product.Base as Product
      using (_×_; ∃-syntax; _,_; proj₁; proj₂)
    open import Data.Product.Relation.Binary.Pointwise.NonDependent
      renaming (Pointwise to _×ᴿ_)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
    open import Function.Base using (_∘_; _∘′_)
    open import Level using (Level)
    open import Relation.Binary.Definitions
      using (Transitive; Symmetric; _Respectsˡ_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Construct.Intersection using (_∩_)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
    open import Relation.Nullary.Reflects using (Reflects)
    open import Relation.Nullary.Decidable.Core using (yes; no)
    open import Relation.Nullary.Negation.Core using (contradiction; ¬_)

    open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
    open Eq using (refl; sym; trans)
    open import Data.Tree.AVL strictTotalOrder using (tree)
    open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
    import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny
    import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties strictTotalOrder as IAnyₚ
    open import Data.Tree.AVL.Key strictTotalOrder using (⊥⁺<[_]<⊤⁺)
    open import Data.Tree.AVL.Map strictTotalOrder
      using (Map; empty; insert; lookup; member; singleton)
    open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Map
      using (Any)
    open import Data.Tree.AVL.Map.Membership.Propositional strictTotalOrder
    open import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Any
      using (tree)

    private
      variable
        v p q : Level
        V : Set v
        m : Map V
        k k′ : Key
        x x′ y y′ : V
        kx : Key × V

    ≈ₖᵥ-trans : Transitive (_≈ₖᵥ_ {V = V})
    ≈ₖᵥ-trans {i = i} {k = k} = ×-transitive Eq.trans ≡-trans {i = i} {k = k}

    ≈ₖᵥ-sym : Symmetric (_≈ₖᵥ_ {V = V})
    ≈ₖᵥ-sym {x = x} {y = y} = ×-symmetric sym ≡-sym {x} {y}

    ∈ₖᵥ-Respectsˡ : _∈ₖᵥ_ {V = V} Respectsˡ _≈ₖᵥ_
    ∈ₖᵥ-Respectsˡ x~y = Any.map (≈ₖᵥ-trans (≈ₖᵥ-sym x~y))

    ∈ₖᵥ-empty : kx ∉ₖᵥ empty
    ∈ₖᵥ-empty (tree ())

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

    ∈ₖᵥ-singleton⁺ : (k , x) ∈ₖᵥ singleton k x
    ∈ₖᵥ-singleton⁺ = tree (IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl))

    ∈ₖᵥ-singleton⁻ : (k , x) ∈ₖᵥ singleton k′ x′ → k ≈ k′ × x ≡ x′
    ∈ₖᵥ-singleton⁻ (tree p) = IAnyₚ.singleton⁻ _ _ _ p

    private
      ≈-lookup : (p : (k , x) ∈ₖᵥ m) → k ≈ Any.lookupKey p
      ≈-lookup (tree p) = proj₁ (IAnyₚ.lookup-result p)

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

    ∈ₖᵥ-insert⁺ : k ≉ k′ → (k , x) ∈ₖᵥ m → (k , x) ∈ₖᵥ insert k′ x′ m
    ∈ₖᵥ-insert⁺ {k′ = k′} {m = m@(tree t)} k≉k′ (tree p) =
      tree (IAnyₚ.insert⁺ _ _ _ (⊥⁺<[ _ ]<⊤⁺) p k′≉key-p)
      where
      k′≉key-p : k′ ≉ Any.lookupKey (tree p)
      k′≉key-p k′≈key-p = k≉k′ (Eq.trans (≈-lookup (tree p)) (Eq.sym k′≈key-p))

    ∈ₖᵥ-insert⁺⁺ : (k , x) ∈ₖᵥ insert k x m
    ∈ₖᵥ-insert⁺⁺ {k = k} {m = tree t} with IAny.any? ((k ≟_) ∘ key) t
    ... | yes k∈ = tree (IAnyₚ.Any-insert-just _ _ _ _ (λ k′ → _, ≡-refl) k∈)
    ... | no ¬k∈ = tree (IAnyₚ.Any-insert-nothing _ _ _ _ (refl , ≡-refl) ¬k∈)

    private
      ≈ₖᵥ-Resp : k ≈ k′ → kx ≈ₖᵥ (k′ , x) → kx ≈ₖᵥ (k , x)
      ≈ₖᵥ-Resp = (λ{ k′≈l (k≈l , x≡) → (trans k≈l (sym k′≈l) , x≡)})

    ∈ₖᵥ-insert⁻ : (k , x) ∈ₖᵥ insert k′ x′ m → (k ≈ k′ × x ≡ x′) ⊎ (k ≉ k′ × (k , x) ∈ₖᵥ m)
    ∈ₖᵥ-insert⁻ {m = tree t} (tree kx∈insert)
        with IAnyₚ.insert⁻ ≈ₖᵥ-Resp _ _ t (⊥⁺<[ _ ]<⊤⁺) kx∈insert
    ... | inj₁ p = inj₁ p
    ... | inj₂ p = let k′≉p , k≈p , _ = IAnyₚ.lookup-result p
                       k≉k′ = λ k≈k′ → k′≉p (trans (sym k≈k′) k≈p)
                   in inj₂ (k≉k′ , tree (IAny.map proj₂ p))

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

    ∈ₖᵥ-lookup⁺ : (k , x) ∈ₖᵥ m → lookup m k ≡ just x
    ∈ₖᵥ-lookup⁺ {k = k} {m = tree t} (tree kx∈m)
        with IAnyₚ.lookup⁺ t k (⊥⁺<[ _ ]<⊤⁺) kx∈m | IAnyₚ.lookup-result kx∈m
    ... | inj₁ p≉k        | k≈p , x≡p = contradiction (sym k≈p) p≉k
    ... | inj₂ (p≈k , eq) | k≈p , x≡p = ≡-trans eq (cong just (≡-sym x≡p))

    ∈ₖᵥ-lookup⁻ : lookup m k ≡ just x → (k , x) ∈ₖᵥ m
    ∈ₖᵥ-lookup⁻ {m = tree t} {k = k} {x = x} eq
      = tree (IAny.map (Product.map sym ≡-sym) (IAnyₚ.lookup⁻ t k x (⊥⁺<[ _ ]<⊤⁺) eq))

    ∈ₖᵥ-lookup-nothing⁺ : (∀ x → (k , x) ∉ₖᵥ m) → lookup m k ≡ nothing
    ∈ₖᵥ-lookup-nothing⁺ {k = k} {m = m@(tree t)} k∉m with lookup m k in eq
    ... | nothing = ≡-refl
    ... | just x = contradiction (∈ₖᵥ-lookup⁻ eq) (k∉m x)

    ∈ₖᵥ-lookup-nothing⁻ : lookup m k ≡ nothing → (k , x) ∉ₖᵥ m
    ∈ₖᵥ-lookup-nothing⁻ eq kx∈m with ≡-trans (≡-sym eq) (∈ₖᵥ-lookup⁺ kx∈m)
    ... | ()

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

    ∈ₖᵥ-member : (k , x) ∈ₖᵥ m → member k m ≡ true
    ∈ₖᵥ-member = cong is-just ∘ ∈ₖᵥ-lookup⁺

    ∉ₖᵥ-member : (∀ x → (k , x) ∉ₖᵥ m) → member k m ≡ false
    ∉ₖᵥ-member = cong is-just ∘ ∈ₖᵥ-lookup-nothing⁺

    member-∈ₖᵥ : member k m ≡ true → ∃[ x ] (k , x) ∈ₖᵥ m
    member-∈ₖᵥ {k = k} {m = m} ≡true with lookup m k in eq
    ... | just x = x , ∈ₖᵥ-lookup⁻ eq

    member-∉ₖᵥ : member k m ≡ false → ∀ x → (k , x) ∉ₖᵥ m
    member-∉ₖᵥ {k = k} {m = m} ≡false x with lookup m k in eq
    ... | nothing = ∈ₖᵥ-lookup-nothing⁻ eq

    member-Reflects-∈ₖᵥ : Reflects (∃[ x ] (k , x) ∈ₖᵥ m) (member k m)
    member-Reflects-∈ₖᵥ {k = k} {m = m} with lookup m k in eq
    ... | just x = Reflects.ofʸ (x , ∈ₖᵥ-lookup⁻ eq)
    ... | nothing = Reflects.ofⁿ (∈ₖᵥ-lookup-nothing⁻ eq ∘ proj₂)