Agda and Binary Search Trees

Question

Just a note, this is for an assignment, so probably best not to post complete solutions, rather, I'm just stuck and need some hints as to what I should be looking at next.

module BST where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)


data Ord (n m : ℕ) : Set where
  smaller : n < m -> Ord n m
  equal   : n ≡ m -> Ord n m
  greater : n > m -> Ord n m

cmp : (n m : ℕ) -> Ord n m
cmp zero zero       = equal refl
cmp zero (suc n)    = smaller (s≤s z≤n)
cmp (suc n) zero    = greater (s≤s z≤n)
cmp (suc n) (suc m) with cmp n m 
... | smaller n<m-pf = smaller (s≤s n<m-pf)
... | equal   n≡m-pf = equal (cong suc n≡m-pf)
... | greater n>m-pf = greater (s≤s n>m-pf)


-- To keep it simple and to exclude duplicates,
-- the BST can only store [1..]
--
data BST (min max : ℕ) : Set where
  branch : (v : ℕ)
         → BST min v → BST v max 
         → BST min max
  leaf   : min < max -> BST min max

These are already imported:

≤-refl : ∀ {a} → a ≤ a 

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c 

We need to implement this function which widens the bounds of the BST:

widen : ∀{min max newMin newMax}
      → BST min max
      → newMin ≤ min
      → max ≤ newMax
      → BST newMin newMax

I have this so far:

widen : ∀{min max newMin newMax}
      → BST min max
      → newMin ≤ min
      → max ≤ newMax
      → BST newMin newMax
widen (leaf min<max-pf) newMin<min-pf max<newMax-pf = BST newMin<min-pf max<newMax-pf
widen (branch v l r) newMin<min-pf max<newMax = branch v 
                                                (widen l newMin<min-pf max<newMax) 
                                                (widen r newMin<min-pf max<newMax)

Now this obviously doesn't work because the new bounds don't have to be strictly less / greater than the min / max. A hint was given: It is not strictly necessary, but you may find it helpful to implement an auxiliary function that widens the range of a strictly smaller than relation of the form min < max. Which is kind of what I've done here, obviously I'd need to change a few things around, but I think the basic idea is there.

This is where I'm at, and I'm just really stuck as to where to go from here, I've done as much research as I can, but there's not a whole lot of reading material out there for using Agda. Do I perhaps need to use ≤-refl or ≤-trans?

Answer 1

The tricky part here is understanding what the widen function actually needs to change. Once you got that, writing the code is fairly easy.

Let's start with the leaf part, we have:

widen (leaf min<max) newMin≤min max≤newMax = {! !}

leaf min<max has type BST min max. After applying widen, we want the tree to have type BST newMin newMax - that means we have to change the proof min < max to newMin < newMax.

Luckily we know that newMin ≤ min and max ≤ newMax. ≤ is transitive (it follows from the fact, that ≤ forms a total order over ℕ) and from that it quite easily follows that newMin ≤ newMax - that is nice and all, but we have to tell that to Agda.

That's where ≤-trans comes into play. Recall that:

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c

That is the definition of transitivity! Exactly what we're looking for. The (rather small) problem is that our proofs use < alongside ≤. If they didn't

trans-4 : ∀ {a b c d} → a ≤ b → b ≤ c → c ≤ d → a ≤ d

would be fairly easy to write (you just have to apply ≤-trans twice). You might want to actually write this function, it will help you with the next part.

We know that a ≤ b (newMin ≤ min) and c ≤ d (max ≤ newMax), but we only know b < c - we cannot just apply ≤-trans twice. Looking at Data.Nat, we find that

_<_ : Rel ℕ Level.zero
m < n = suc m ≤ n

So what we really want to write is this:

trans-4 : ∀ {a b c d} → a ≤ b → suc b ≤ c → c ≤ d → suc a ≤ d

That's a bit harder, so let's break it into two steps. We need to prove that:

trans₁ : ∀ {a b c} → a ≤ b → suc b ≤ c → suc a ≤ c -- a ≤ b → b < c → a < c
trans₂ : ∀ {a b c} → suc a ≤ b → b ≤ c → suc a ≤ c -- a < b → b ≤ c → a < c

We could use ≤-trans if we had suc a ≤ suc b instead of just a ≤ b. But we can get that! If a ≤ b, then surely a + 1 ≤ b + 1. Quick look at standard library again:

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

I leave the rest as an exercise. Once you know that newMin < newMax, reconstructing the proof in leaf becomes trivial.

---

The branch part is actually much easier to write in Agda and of course, the tricky part is figuring out what proofs we need to change.

We have:

widen (branch v l r) newMin≤min max≤newMax = {! !}

Again, branch v l r has type BST min max and we want BST newMin newMax. As you noticed, we need to create a new branch and recursively widen l and r.

If we want to recursively apply widen, we better check what are the types of l and r:

l : BST min v
r : BST v max

Because this answer is already rather long, I'm going to discuss the l subtree, the other case is symmetric.

The problem is of course that if we apply widen to l, we need to also provide two new proofs. min hasn't changed, so we can just pass newMin≤min as the first one. What about the second one? We can no longer give it max≤newMax, because our subtree is BST min v rather than BST min max.

Our final tree must look like BST newMin newMax and we know it must contain v. This gives us only one choice for type of widened left subtree - BST newMin v.

What does that mean? The type of second proof is thus v ≤ v and it's easy from here!

Happy coding!