Binary trees ala How To Keep Your Neighbors in Order

binary.agda

open import Level
open import Relation.Nullary
open import Relation.Binary

module binary (ord : DecTotalOrder zero zero zero) where

A = DecTotalOrder.Carrier ord
open DecTotalOrder {{...}}

module bound where
  open import Data.Sum
  open import Data.Product

  data Bound : Set where
    ∞+  : Bound
    ∞-  : Bound
    val : A → Bound

  data _≤b_ : Bound → Bound → Set where
    ∞+  : {b : Bound}         → b     ≤b ∞+
    ∞-  : {b : Bound}         → ∞-    ≤b b
    val : {a b : A}   → a ≤ b → val a ≤b val b

  data _≈b_ : Bound → Bound → Set where
    ∞+  : ∞+ ≈b ∞+
    ∞-  : ∞- ≈b ∞-
    val : {a b : A} → a ≈ b → val a ≈b val b
  private
    _≤b?_ : (a b : Bound) → Dec (a ≤b b)
    _  ≤b? ∞+ = yes ∞+
    ∞+ ≤b? ∞- = no λ ()
    ∞+ ≤b? val x = no λ ()
    ∞- ≤b? _ = yes ∞-
    val x ≤b? ∞- = no λ ()
    val x ≤b? val x₁ with x ≤? x₁
    ... | yes p = yes (val p)
    ... | no ¬p = no λ {(val x₂) → ¬p x₂}

    _≟b_ : (a b : Bound) → Dec (a ≈b b)
    ∞+ ≟b ∞+ = yes ∞+
    ∞+ ≟b ∞- = no (λ ())
    ∞+ ≟b val x = no (λ ())
    ∞- ≟b ∞+ = no (λ ())
    ∞- ≟b ∞- = yes ∞-
    ∞- ≟b val x = no (λ ())
    val x ≟b ∞+ = no (λ ())
    val x ≟b ∞- = no (λ ())
    val x ≟b val x₁ with x ≟ x₁
    ... | yes p = yes (val p)
    ... | no ¬p = no λ { (val p) → ¬p p }

    totalb : (a b : Bound) → a ≤b b ⊎ b ≤b a
    totalb ∞+ _ = inj₂ ∞+
    totalb ∞- _ = inj₁ ∞-
    totalb (val x) ∞+ = inj₁ ∞+
    totalb (val x) ∞- = inj₂ ∞-
    totalb (val x) (val x₁) with total x x₁
    ... | inj₁ p = inj₁ (val p)
    ... | inj₂ p = inj₂ (val p)

    reflexiveb : {a b : Bound} → a ≈b b → a ≤b b
    reflexiveb ∞+ = ∞+
    reflexiveb ∞- = ∞-
    reflexiveb (val x) = val (reflexive x)

    transb : {a b c : Bound} → a ≤b b → b ≤b c → a ≤b c
    transb ∞+ ∞+ = ∞+
    transb ∞- _ = ∞-
    transb (val x) ∞+ = ∞+
    transb (val x) (val x₁) = val (trans x x₁)

    antisymb : {a b : Bound} → a ≤b b → b ≤b a → a ≈b b
    antisymb ∞+ ∞+ = ∞+
    antisymb ∞- ∞- = ∞-
    antisymb (val x) (val x₁) = val (antisym x x₁)

    refl≈b : (x : Bound) → x ≈b x
    refl≈b ∞+ = ∞+
    refl≈b ∞- = ∞-
    refl≈b (val x) = val (IsEquivalence.refl isEquivalence)

    sym≈b : {a b : Bound} → a ≈b b → b ≈b a
    sym≈b ∞+ = ∞+
    sym≈b ∞- = ∞-
    sym≈b (val x) = val (IsEquivalence.sym isEquivalence x)

    trans≈b : {a b c : Bound} → a ≈b b → b ≈b c → a ≈b c
    trans≈b ∞+ ∞+ = ∞+
    trans≈b ∞- ∞- = ∞-
    trans≈b (val x) (val x₁) = val (IsEquivalence.trans isEquivalence x x₁)

  instance decTotal : DecTotalOrder _ _ _
  decTotal = record
    { Carrier = Bound
    ; _≈_ = _≈b_
    ; _≤_ = _≤b_
    ; isDecTotalOrder = record
      { _≤?_ = _≤b?_
      ; _≟_  = _≟b_
      ; isTotalOrder = record
        { total = totalb
        ; isPartialOrder =  record
          { antisym = antisymb
          ; isPreorder = record
            { trans = transb
            ; reflexive = reflexiveb
            ; isEquivalence = record
              { refl = λ {x} → refl≈b x
              ; sym = sym≈b
              ; trans = trans≈b
              }
            }
          }
        }
      }
    }

  lub : (l r : Bound) → Bound
  lub l r with total l r
  ... | (inj₁ x) = r
  ... | (inj₂ y) = l

  glb : (l r : Bound) → Bound
  glb l r with total l r
  ... | (inj₁ x) = l
  ... | (inj₂ y) = r

open bound
open import Data.Sum
open import Data.Empty

data BoundedTree : Bound → Bound → Set where
  leaf : {a b : Bound} → a ≤ b → BoundedTree a b
  node : {a b : Bound}(c : A)
       → BoundedTree a (val c)
       → BoundedTree (val c) b
       → BoundedTree a b

bounds : {l u : Bound} → BoundedTree l u → l ≤ u
bounds (leaf x) = x
bounds (node c t t₁) = trans (bounds t) (bounds t₁)

binsert : {l u : Bound}(a : A)
       → l ≤ val a → val a ≤ u
       → BoundedTree l u
       → BoundedTree l u
binsert a l u (leaf x) = node a (leaf l) (leaf u)
binsert a l u (node c t t₁) with total a c
... | inj₁ p = node c (binsert a l (val p) t) t₁
... | inj₂ p = node c t (binsert a (val p) u t₁)

data _∈_ (a : A) : {l u : Bound} → BoundedTree l u → Set where
  here : {l u : Bound}{c : A}{lt : BoundedTree l (val c)}
         {rt : BoundedTree (val c) u}
       → a ≈ c
       → a ∈ node c lt rt
  there₁ : {c : A}{l u : Bound}{lt : BoundedTree l (val c)}
           {rt : BoundedTree (val c) u}
       → a ∈ lt
       → a ∈ node c lt rt
  there₂ : {c : A}{l u : Bound}{lt : BoundedTree l (val c)}
           {rt : BoundedTree (val c) u}
       → a ∈ rt
       → a ∈ node c lt rt

too-high : {l u : Bound}(a : A)
         → {t : BoundedTree l u}
         → a ∈ t
         → val a ≤ u
too-high a {node c l r} (here x) = trans (val (reflexive x)) (bounds r)
too-high a {node c l r} (there₁ mem) = trans (too-high a mem) (bounds r)
too-high a (there₂ mem) = too-high a mem

too-low : {l u : Bound}(a : A)
         → {t : BoundedTree l u}
         → a ∈ t
         → l ≤ val a
too-low a {node c l r} (here x) = trans (bounds l) (val (reflexive c'))
  where c' = IsEquivalence.sym isEquivalence x
too-low a (there₁ mem) = too-low a mem
too-low a {node c l r} (there₂ mem) = trans (bounds l) (too-low a mem)

flip : {a b : A} → ¬ (a ≤ b) → b ≤ a
flip ¬p = [ (λ x → x) , (λ x → ⊥-elim (¬p x))] (total _ _)

blookup : {l u : Bound}(a : A)
        → l ≤ val a → val a ≤ u
        → (t : BoundedTree l u)
        → Dec (a ∈ t)
blookup a l u (leaf x) = no λ ()
blookup a l u (node c t t₁) with a ≤? c | a ≟ c
... | p | yes p₁ = yes (here p₁)
blookup a l u (node c t t₁) | yes p | no ¬p₁ with blookup a l (val p) t
... | yes p₁ = yes (there₁ p₁)
... | no ¬p = no λ { (here x) → ¬p₁ x
                   ; (there₁ p₁) → ¬p p₁
                   ; (there₂ p₁) → contra (too-low a p₁)
                   }
    where contra : val c ≤b val a → ⊥
          contra (val x) = ¬p₁ (antisym p x)
blookup a l u (node c t t₁) | no ¬p | no ¬p₁ with blookup a (val (flip ¬p)) u t₁
... | yes p₂ = yes (there₂ p₂)
... | no ¬p₂ = no λ { (here x) → ¬p₁ x
                    ; (there₁ p) → contra (too-high a p)
                    ; (there₂ p) → ¬p₂ p
                    }
    where contra : val a ≤b val c → ⊥
          contra (val x) = ¬p x

Tree : Set
Tree = BoundedTree ∞- ∞+

empty : Tree
empty = leaf ∞+

insert : A → Tree → Tree
insert a t = binsert a ∞- ∞+ t

lookup : (a : A)(t : Tree) → Dec (a ∈ t)
lookup a t = blookup a ∞- ∞+ t