AVLMembership.agda

module AVLMembership where

open import Data.Empty
open import Data.Product
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

import Data.AVL

module Membership
  {k v ℓ}
  {Key : Set k} (Value : Key → Set v)
  {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

  open Data.AVL Value isStrictTotalOrder public
  open Extended-key                      public
  open Height-invariants                 public

  open IsStrictTotalOrder isStrictTotalOrder

  private
    _≮_ = λ x y → ¬ (x < y)
    _≯_ = λ x y → ¬ (y < x)

    _≢_ : (x y : Key) → _
    _≢_ = λ x y → ¬ (x ≡ y)

  data _∈_ {lb ub} (K : Key) : ∀ {n} → Indexed.Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
    here : ∀ {hˡ hʳ} V
      {l : Indexed.Tree lb [ K ] hˡ}
      {r : Indexed.Tree [ K ] ub hʳ}
      {b : hˡ ∼ hʳ} →
      K ∈ Indexed.node (K , V) l r b
    left : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Indexed.Tree lb [ K′ ] hˡ}
      {r : Indexed.Tree [ K′ ] ub hʳ}
      {b : hˡ ∼ hʳ} →
      K < K′ →
      K ∈ l →
      K ∈ Indexed.node (K′ , V) l r b
    right : ∀ {hˡ hʳ K′} {V : Value K′}
      {l : Indexed.Tree lb [ K′ ] hˡ}
      {r : Indexed.Tree [ K′ ] ub hʳ}
      {b : hˡ ∼ hʳ} →
      K′ < K →
      K ∈ r →
      K ∈ Indexed.node (K′ , V) l r b

  lem : ∀ {lb ub hˡ hʳ K′ n} {V : Value K′}
      {l : Indexed.Tree lb [ K′ ] hˡ}
      {r : Indexed.Tree [ K′ ] ub hʳ}
      {b : hˡ ∼ hʳ} →
      n ∈ Indexed.node (K′ , V) l r b →
      (n ≯ K′ → n ≢ K′ → n ∈ l) × (n ≮ K′ → n ≢ K′ → n ∈ r)
  lem (here    V) = (λ _ eq → ⊥-elim (eq P.refl)) , (λ _ eq → ⊥-elim (eq P.refl))
  lem (left  x p) = (λ _ _ → p) , (λ ≮ _ → ⊥-elim (≮ x))
  lem (right x p) = (λ ≯ _ → ⊥-elim (≯ x)) , (λ _ _ → p)

  find : ∀ {h lb ub} n (m : Indexed.Tree lb ub h) → Dec (n ∈ m)
  find n (Indexed.leaf _) = no λ ()
  find n (Indexed.node (k , v) l r _) with compare n k
  find n (Indexed.node (k , v) l r _) | tri< a ¬b ¬c with find n l
  ... | yes p = yes (left a p)
  ... | no ¬p = no λ ¬∈l → ¬p (proj₁ (lem ¬∈l) ¬c ¬b)
  find n (Indexed.node (k , v) l r _) | tri≈ ¬a b ¬c rewrite (P.sym b) = yes (here v)
  find n (Indexed.node (k , v) l r _) | tri> ¬a ¬b c with find n r
  ... | yes p = yes (right c p)
  ... | no ¬p = no λ ¬∈r → ¬p (proj₂ (lem ¬∈r) ¬a ¬b)

  get : ∀ {h lb ub n} {m : Indexed.Tree lb ub h} → n ∈ m → Value n
  get (here    V) = V
  get (left  _ p) = get p
  get (right _ p) = get p

open import Data.Nat
open import Data.Nat.Properties

open Membership
  (λ _ → ℕ)
  (StrictTotalOrder.isStrictTotalOrder strictTotalOrder)

un-tree : Tree → ∃ λ h → Indexed.Tree ⊥⁺ ⊤⁺ h
un-tree (tree t) = , t

test : Indexed.Tree _ _ _
test = proj₂ (un-tree
  (insert 5 55 (insert 7 77 (insert 4 44 empty))))

Extract : ∀ {p} {P : Set p} → Dec P → Set _
Extract {P = P} (yes _) = P
Extract {P = P} (no  _) = ¬ P

extract : ∀ {p} {P : Set p} (d : Dec P) → Extract d
extract (yes p) = p
extract (no ¬p) = ¬p

∈-test₁ : ¬ (2 ∈ test)
∈-test₁ = extract (find 2 test)

∈-test₂ : 4 ∈ test
∈-test₂ = extract (find 4 test)