[Agda] red black trees with delete
Adam Gundry
adam.gundry at strath.ac.uk
Wed Jan 11 12:55:35 CET 2012
On 11/01/12 02:36, jleivent at comcast.net wrote:
> Attached is an Agda implementation of Red Black trees (the
> old-fashioned non-leaning variety) with insert, find, and delete
> functions. The dependent types show that the trees have the usual
> red-black level and color invariants, are sorted, and contain the
> right multiset of elements following each function. I also tried to
> keep the types a transparent as possible.
Very nice. There are several implementations of red-black trees floating
around, notably [1], but not so many handle deletion and few of them
verify the multiset properties as you do.
I've attached my own effort in case you are interested. It uses a trick
Conor McBride taught me for setting up ordered data structures so that
the proof obligations are easy (easy enough for instance arguments to
squash them automatically, most of the time). I use a (Huet) zipper to
manage insertion and deletion conveniently. For most of the
implementation it is enough to follow one's nose, when the types are
this precise, as you observe...
> [...] I just allowed the combination of the Agda
> type checker and the exacting dependent type signatures to do their
> thing (with some simple reasoning about what the delete function must
> contain - such as a delete minimum function) - making me feel more
> like a facilitator than a programmer.
> Also, I'm not sure of the approach I took for erasability (via
> parameterized module) - but it was the only thing I could think of,
> following a failed attempt to use Agda's irrelevance feature. I
> wanted to demonstrate erasability of the proof terms because had I
> not, one could argue that the implementation could be extracting
> information from the proof terms to cheat somewhere. Also, those
> proof terms would be pretty heavy-weight at runtime!
This seems like a good approach to me; using a parameterized module
makes explicit the properties of the monoid you need. It would be nice
if you could get by with fewer lemmas, but that may just be the cost of
proving that your functions modify the multiset of elements correctly.
It is annoying that we all have to do so much work to prove what ought
to be an obvious property - that elements from the data structure are
used linearly, so regardless of how they are rearranged to balance the
tree, the multiset is not modified. Surely there is a better way!
Adam Gundry
[1] http://web.student.chalmers.se/groups/datx02-dtp/
-------------- next part --------------
module RedBlackImplicit where
open import Data.Nat using (zero ; suc) renaming (ℕ to Nat)
open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥)
open import Data.List using (List ; [] ; _∷_ ; _++_ ; [_])
open import Data.Bool using (Bool ; true ; false)
--------------------------------------------------------------------------------
-- Basic ordering machinery
--------------------------------------------------------------------------------
-- Any key set with a (decidable) total order will do, but this one is
-- nice because Agda can infer the proofs whenever we have concrete
-- values. Moreover, the new "instance arguments" feature of Agda
-- 2.3.0 gets us even more automation.
trivial : ⊤
trivial = _
Key = Nat
_<_ : Key -> Key -> Set
zero < zero = ⊥
zero < suc _ = ⊤
suc _ < zero = ⊥
suc m < suc n = m < n
<-trans : forall i {j k}{{p : i < j}}{{q : j < k}} -> i < k
<-trans zero {zero} {zero} {{q = ()}}
<-trans zero {suc _} {zero} {{q = ()}}
<-trans zero {j} {suc k} = _
<-trans (suc n) {zero} {zero} {{q = ()}}
<-trans (suc n) {suc j} {zero} {{q = ()}}
<-trans (suc n) {zero} {suc k} {{p = ()}}
<-trans (suc n) {suc j} {suc k} = <-trans n
data Trich : Key -> Key -> Set where
same : forall {i} -> Trich i i
less : forall {i j}{{p : i < j}} -> Trich i j
more : forall {i j}{{p : j < i}} -> Trich i j
trichotomy : (i j : Key) -> Trich i j
trichotomy zero zero = same
trichotomy zero (suc j) = less
trichotomy (suc i) zero = more
trichotomy (suc i) (suc j) with trichotomy i j
trichotomy (suc i) (suc .i) | same = same
trichotomy (suc i) (suc j) | less = less
trichotomy (suc i) (suc j) | more = more
--------------------------------------------------------------------------------
-- Red-black tree data structure
--------------------------------------------------------------------------------
data Colour : Set where
red blk : Colour
data Tree (lo hi : Key) : Colour -> Nat -> Set where
e : {{p : lo < hi}} -> Tree lo hi blk 0
tr : forall {n}(x : Key)(l : Tree lo x blk n)(r : Tree x hi blk n) ->
Tree lo hi red n
tb : forall {n cl cr}(x : Key)(l : Tree lo x cl n)(r : Tree x hi cr n) ->
Tree lo hi blk (suc n)
wkTree : forall {lo hi ha c n}{{p : hi < ha}} -> Tree lo hi c n -> Tree lo ha c n
wkTree {lo} e = e {{p = <-trans lo}}
wkTree (tr x l r) = tr x l (wkTree r)
wkTree (tb x l r) = tb x l (wkTree r)
r2b : forall {lo hi n} -> Tree lo hi red n -> Tree lo hi blk (suc n)
r2b (tr l x r) = tb l x r
--------------------------------------------------------------------------------
-- Aside: flattening an RBT produces a sorted list
--------------------------------------------------------------------------------
flatten : forall {lo hi c n} -> Tree lo hi c n -> List Key
flatten e = []
flatten (tr x l r) = flatten l ++ [ x ] ++ flatten r
flatten (tb x l r) = flatten l ++ [ x ] ++ flatten r
Sorted : Key -> Key -> List Key -> Set
Sorted l u [] = l < u
Sorted l u (x ∷ xs) = l < x × Sorted x u xs
appendSorted : forall {lo x hi}(l r : List Key) ->
Sorted lo x l -> Sorted x hi r ->
Sorted lo hi (l ++ [ x ] ++ r)
appendSorted {lo} [] [] lSorted rSorted = lSorted , rSorted
appendSorted {lo} [] (x ∷ xs) lSorted (p , q) = lSorted , p , q
appendSorted (x ∷ xs) r (p , q) rSorted = p , appendSorted xs r q rSorted
flattenSorted : forall {lo hi c n}(t : Tree lo hi c n) ->
Sorted lo hi (flatten t)
flattenSorted (e {{p}}) = p
flattenSorted (tr x l r) = appendSorted (flatten l) (flatten r)
(flattenSorted l) (flattenSorted r)
flattenSorted (tb x l r) = appendSorted (flatten l) (flatten r)
(flattenSorted l) (flattenSorted r)
--------------------------------------------------------------------------------
-- Zipper data structure
--------------------------------------------------------------------------------
-- This is parameterised by the bounds, colour and black height
-- delivered at the root; it is indexed by the values demanded at the
-- hole.
data TreeZip (rlo rhi : Key)(rc : Colour)(rn : Nat) :
Key -> Key -> Colour -> Nat -> Set where
root : TreeZip rlo rhi rc rn rlo rhi rc rn
zrl : forall {n lo hi}(x : Key)
(z : TreeZip rlo rhi rc rn lo hi red n)(r : Tree x hi blk n) ->
TreeZip rlo rhi rc rn lo x blk n
zrr : forall {n lo hi}(x : Key)
(l : Tree lo x blk n)(z : TreeZip rlo rhi rc rn lo hi red n) ->
TreeZip rlo rhi rc rn x hi blk n
zbl : forall {n c hc lo hi}(x : Key)
(z : TreeZip rlo rhi rc rn lo hi blk (suc n))(r : Tree x hi c n) ->
TreeZip rlo rhi rc rn lo x hc n
zbr : forall {n c hc lo hi}(x : Key)
(l : Tree lo x c n)(z : TreeZip rlo rhi rc rn lo hi blk (suc n)) ->
TreeZip rlo rhi rc rn x hi hc n
plug : forall {rlo rhi rc rn lo hi c n} -> Tree lo hi c n ->
TreeZip rlo rhi rc rn lo hi c n -> Tree rlo rhi rc rn
plug t root = t
plug t (zrl x z r) = plug (tr x t r) z
plug t (zrr x l z) = plug (tr x l t) z
plug t (zbl x z r) = plug (tb x t r) z
plug t (zbr x l z) = plug (tb x l t) z
plugBR : forall {lo hi n rlo rhi rn} -> Tree lo hi blk n ->
TreeZip rlo rhi blk rn lo hi red n -> Tree rlo rhi blk rn
plugBR t (zbl x z r) = plug t (zbl x z r)
plugBR t (zbr x l z) = plug t (zbr x l z)
-- Aside: zippers can be composed
composeZip : forall {rlo rhi rc rn lo hi c n hlo hhi hc hn} ->
TreeZip rlo rhi rc rn lo hi c n ->
TreeZip lo hi c n hlo hhi hc hn ->
TreeZip rlo rhi rc rn hlo hhi hc hn
composeZip z1 root = z1
composeZip z1 (zrl x z2 r) = zrl x (composeZip z1 z2) r
composeZip z1 (zrr x l z2) = zrr x l (composeZip z1 z2)
composeZip z1 (zbl x z2 r) = zbl x (composeZip z1 z2) r
composeZip z1 (zbr x l z2) = zbr x l (composeZip z1 z2)
--------------------------------------------------------------------------------
-- Search
--------------------------------------------------------------------------------
-- Binary search is parameterised by two functions:
-- * what to do if a leaf is reached (so the key does not exist in
-- the tree); and
-- * what to do if the key is found.
-- In each case, a zipper is supplied with the leaf or node at the
-- focus. This allows the same method to be used for membership testing,
-- insertion and deletion.
search : forall {A : Set}{rlo rhi rn}(x : Key){{p : rlo < x}}{{q : x < rhi}} ->
(forall {lo hi}{{p : lo < x}}{{q : x < hi}} ->
TreeZip rlo rhi blk rn lo hi blk 0 -> A) ->
(forall {lo hi c n}{{p : lo < x}}{{q : x < hi}} -> Tree lo hi c n ->
TreeZip rlo rhi blk rn lo hi c n -> A) ->
Tree rlo rhi blk rn -> A
search {A} {rlo} {rhi} {rn} x fe fn = help root
where
help : forall {lo hi c n}{{p : lo < x}}{{q : x < hi}} ->
TreeZip rlo rhi blk rn lo hi c n -> Tree lo hi c n -> A
help z e = fe z
help z (tr y l r) with trichotomy x y
help z (tr .x l r) | same = fn (tr x l r) z
help z (tr y l r) | less = help (zrl y z r) l
help z (tr y l r) | more = help (zrr y l z) r
help z (tb y l r) with trichotomy x y
help z (tb .x l r) | same = fn (tb x l r) z
help z (tb y l r) | less = help (zbl y z r) l
help z (tb y l r) | more = help (zbr y l z) r
member : forall {lo hi n}(x : Key){{p : lo < x}}{{q : x < hi}} ->
Tree lo hi blk n -> Bool
member x = search x (\ _ -> false) (\ _ _ -> true)
--------------------------------------------------------------------------------
-- Insertion
--------------------------------------------------------------------------------
-- Once we have inserted a key, we are either on the level (inserting
-- a tree into a hole of the correct black height, though not
-- necessarily the same colour) or in a panic (because we have a red
-- child of a red parent). We propagate the change upwards.
data InsProb (lo hi : Key) : Colour -> Nat -> Set where
level : forall {n c}(ci : Colour)(t : Tree lo hi ci n) -> InsProb lo hi c n
panicRB : forall {n}(x : Key)
(l : Tree lo x red n)(r : Tree x hi blk n) -> InsProb lo hi red n
panicBR : forall {n}(x : Key)
(l : Tree lo x blk n)(r : Tree x hi red n) -> InsProb lo hi red n
solveIns : forall {rlo rhi rn lo hi c n} -> InsProb lo hi c n ->
TreeZip rlo rhi blk rn lo hi c n -> ∃ \ rc -> Tree rlo rhi rc rn
solveIns (level c t) root = c , t
solveIns (level c t) (zbl x z r) = solveIns (level blk (tb x t r)) z
solveIns (level c t) (zbr x l z) = solveIns (level blk (tb x l t)) z
solveIns (level red t) (zrl x z r) = solveIns (panicRB x t r) z
solveIns (level red t) (zrr x l z) = solveIns (panicBR x l t) z
solveIns (level blk t) (zrl x z r) = solveIns (level red (tr x t r)) z
solveIns (level blk t) (zrr x l z) = solveIns (level red (tr x l t)) z
solveIns (panicRB x (tr lx ll lr) r) (zbl y z r') = solveIns (level red (tr x (tb lx ll lr) (tb y r r'))) z
solveIns (panicRB x (tr lx ll lr) r) (zbr y l z) = solveIns (level red (tr lx (tb y l ll) (tb x lr r))) z
solveIns (panicBR x l (tr rx rl rr)) (zbl y z r) = solveIns (level red (tr rx (tb x l rl) (tb y rr r))) z
solveIns (panicBR x l (tr rx rl rr)) (zbr y l' z) = solveIns (level red (tr x (tb y l' l) (tb rx rl rr))) z
-- To insert a key, we search for it, then invoke the above method if
-- we ended up at a leaf, or simply return the original tree if
-- the node already exists.
ins : forall {rlo rhi rn}(x : Key){{p : rlo < x}}{{q : x < rhi}} -> Tree rlo rhi blk rn ->
∃ \ rc -> Tree rlo rhi rc rn
ins x t = search x
(\ z -> solveIns (level red (tr x e e)) z)
(\ _ _ -> blk , t) t
ins2 : forall {lo hi n}(x : Key){{p : lo < x}}{{q : x < hi}} -> Tree lo hi blk n ->
∃ \ n' -> Tree lo hi blk n'
ins2 x t with ins x t
... | blk , t' = _ , t'
... | red , t' = _ , r2b t'
insert : forall {lo hi n}(x : Key){{p : lo < x}}{{q : x < hi}}
(t : Tree lo hi blk n) ->
Tree lo hi blk (proj₁ (ins2 x t))
insert x t = proj₂ (ins2 x t)
--------------------------------------------------------------------------------
-- Deletion
--------------------------------------------------------------------------------
-- This section probably makes the most sense if read from bottom to
-- top. A redundant mutual block might make this easier to explain in
-- the right order.
-- If we are deleting a black leaf (either directly or because it is
-- the minimum in the right subtree of a deleted internal node), the
-- black height must be reduced by one. Generally, the problem is to
-- fit a tree of black height n into a hole that expects a tree of
-- height (suc n). This involves a lot of easy cases; interactive
-- construction and the type checker make this a lot easier to write
-- than to read!
solveDel : forall {rlo rhi rn lo hi n} -> Tree lo hi blk n ->
TreeZip rlo rhi blk rn lo hi blk (suc n) ->
∃ \ n' -> Tree rlo rhi blk n'
solveDel t root = _ , t
solveDel t (zrl x z (tb {cl = red} y (tr lx ll lr) r)) = _ , plug (tr lx (tb x t ll) (tb y lr r)) z
solveDel t (zrl x z (tb {cr = red} y l (tr rx rl rr))) = _ , plug (tr y (tb x t l) (tb rx rl rr)) z
solveDel t (zrl x z (tb {cl = blk} {cr = blk} y l r)) = _ , plugBR (tb y (tr x t l) r) z
solveDel t (zrr x (tb {cl = red} y (tr lx ll lr) r) z) = _ , plug (tr y (tb lx ll lr) (tb x r t)) z
solveDel t (zrr x (tb {cr = red} y l (tr rx rl rr)) z) = _ , plug (tr rx (tb y l rl) (tb x rr t)) z
solveDel t (zrr x (tb {cl = blk} {cr = blk} y l r) z) = _ , plugBR (tb x (tr y l r) t) z
solveDel t (zbl x z (tr y (tb {cl = blk} lx ll lr) r)) = _ , plug (tb y (tb lx (tr x t ll) lr) r) z
solveDel t (zbl x z (tr y (tb {cl = red} lx (tr llx lll llr) lr) r)) = _ , plug (tb llx (tb x t lll) (tr y (tb lx llr lr) r)) z
solveDel t (zbl x z (tb {cl = blk} y l r)) = solveDel (tb y (tr x t l) r) z
solveDel t (zbl x z (tb {cl = red} {cr = blk} y (tr lx ll lr) r)) = solveDel (tb lx (tr x t ll) (tr y lr r)) z
solveDel t (zbl x z (tb {cl = red} {cr = red} y (tr lx ll lr) (tr rx rl rr))) = _ , plug (tb lx (tb x t ll) (tb y lr (tr rx rl rr))) z
solveDel t (zbr x (tr y l (tb {cr = blk} rx rl rr)) z) = _ , plug (tb y l (tb rx rl (tr x rr t))) z
solveDel t (zbr x (tr y l (tb {cr = red} rx rl (tr rrx rrl rrr))) z) = _ , plug (tb rrx (tr y l (tb rx rl rrl)) (tb x rrr t)) z
solveDel t (zbr x (tb {cr = blk} y l r) z) = solveDel (tb y l (tr x r t)) z
solveDel t (zbr x (tb {cl = blk} {cr = red} y l (tr rx rl rr)) z) = solveDel (tb rx (tr y l rl) (tr x rr t)) z
solveDel t (zbr x (tb {cl = red} {cr = red} y (tr lx ll lr) (tr rx rl rr)) z) = _ , plug (tb y (tb lx ll lr) (tb rx rl (tr x rr t))) z
-- Here we are inside the right subtree of the node whose key is being
-- deleted, looking for the minimum key (which we will use to replace
-- the deleted one). The zipper context abstracts over the (as yet
-- unknown) minimum key. If we find the minimum on a red node, we can
-- simply remove it and reconstruct the tree. However, if the minimum
-- is on a black node or leaf, then we have to invoke the above method
-- to decrease the black height.
findMin : forall {n rlo rhi rn lo hi c} -> Tree lo hi c (suc n) ->
((k : Key){{p : lo < k}} -> TreeZip rlo rhi blk rn k hi c (suc n)) ->
∃ \ n' -> Tree rlo rhi blk n'
findMin {zero} (tr x (tb {cr = blk} y e lr) r) f = solveDel lr (zrl x (f y) r)
findMin {zero} (tr x (tb {cr = red} y e lr) r) f = _ , plug (r2b lr) (zrl x (f y) r)
findMin {zero} (tr x (tb y (tr k e e) lr) r) f = _ , plug e (zbl y (zrl x (f k) r) lr)
findMin {zero} (tb x (tr y e e) r) f = _ , plug e (zbl x (f y) r)
findMin {zero} (tb {cr = red} x e r) f = _ , plug (r2b r) (f x)
findMin {zero} (tb {cr = blk} x e r) f = solveDel r (f x)
findMin {suc m} (tr x (tb y ll lr) r) f = findMin ll (\ k -> zbl y (zrl x (f k) r) lr)
findMin {suc m} (tb x l r) f = findMin l (\ k -> zbl x (f k) r)
-- To delete the node at the focus, we replace the deleted key with
-- the minimum of its right subtree using findMin, provided the
-- subtree has black height 1 or more. If not, we handle the base
-- cases individually.
delFocus : forall {c n lo hi rlo rhi rn} -> Tree lo hi c n ->
TreeZip rlo rhi blk rn lo hi c n ->
∃ \ n' -> Tree rlo rhi blk n'
delFocus {red} {zero} {lo} (tr x e e) z = _ , plugBR (e {{p = <-trans lo }}) z
delFocus {blk} {zero} e z = _ , plug e z
delFocus {blk} {suc zero} {lo} (tb x e e) z = solveDel (e {{p = <-trans lo}}) z
delFocus {blk} {suc zero} (tb x (tr y e e) e) z = _ , plug (tb y e (e {{p = <-trans y}})) z
delFocus {blk} {suc zero} {lo} (tb x e (tr y e e)) z = _ , plug (tb y (e {{p = <-trans lo}}) e) z
delFocus {blk} {suc zero} (tb x (tr k e e) (tr y e e)) z = _ , plug (tb k e (tr y (e {{p = <-trans k}}) e)) z
delFocus {red} {suc m} (tr x l r) z = findMin r (\ k -> zrr k (wkTree l) z)
delFocus {blk} {suc (suc m)} (tb x l r) z = findMin r (\ k -> zbr k (wkTree l) z)
-- To kick off deletion, we search for the node to delete and, if we
-- find it, invoke the above method to delete the focus.
del : forall {rlo rhi rn}(x : Key){{p : rlo < x}}{{q : x < rhi}} ->
Tree rlo rhi blk rn ->
∃ \ n' -> Tree rlo rhi blk n'
del x t = search x (\ _ -> _ , t) (\ t z -> delFocus t z) t
delete : forall {lo hi n}(x : Key){{p : lo < x}}{{q : x < hi}}
(t : Tree lo hi blk n) -> Tree lo hi blk (proj₁ (del x t))
delete x t = proj₂ (del x t)
--------------------------------------------------------------------------------
-- Test data
--------------------------------------------------------------------------------
t1 = insert {0} {10} 1 e
t2 = insert 9 (insert 7 (insert 1 (insert 4 (insert 5 (insert 6
(insert 2 (insert 3 (insert 2 t1))))))))
t3 = delete 2 (delete 2 (delete 5 t2))
t4 = delete 1 t1
More information about the Agda
mailing list