Proofs: Left-leaning red-black tree

Insertion and deletion keep the left-leaning red-black rules full

This proof shows: correctness.

The rules are (L1) search order, (L2) no red right child, (L3) no red node with a red left child, (L4) the same number of black nodes on every path from the root to nil, and (L5) a black root. For a node $h$, write $bh(h)$ for the number of black nodes on a path from $h$ down to nil, counting $h$ itself, with $bh(\text{nil}) = 0$; it is well defined when (L4) holds in the subtree of $h$. Call a subtree valid when (L1) to (L4) hold in it; its root may be red. In a valid subtree, a red node has two black children: the left one by (L3), the right one by (L2).

Lemma A (the steps). A rotation of a red link, where the child moves up, takes the color of the old top, and the old top becomes red, keeps (L1), keeps (L4) in the subtree, and keeps $bh$ of the top. A color flip at a node whose two children both have the color opposite to its own keeps (L1), (L4) and $bh$ of the top.

Proof. A rotation keeps the in-order sequence of the keys. For ROTATE-LEFT$(h)$ with $x = h.right$ red, let $c$ be the color of $h$ and $\alpha$, $\beta$, $\gamma$ the subtrees $h.left$, $x.left$, $x.right$. Before, a path from the top to $\alpha$, $\beta$ or $\gamma$ meets the node $h$ of color $c$ and, for $\beta$ and $\gamma$, the red $x$. After, it meets the node $x$ of color $c$ and, for $\alpha$ and $\beta$, the red $h$. Red nodes add nothing, so each path has the same count. ROTATE-RIGHT is the mirror image. A flip at a black node with two red children makes the node red and the children black: a path from the top meets one black node before (the top) and one after (a child). The other flip is the reverse. Neither step changes keys. $\square$

Insertion

Lemma 1 (PUT). Let $h$ be valid or nil, and $k \notin K(h)$. Then $x = \text{PUT}(h, k)$ has the keys $K(h) \cup \{k\}$ and $bh(x) = bh(h)$, (L1), (L2) and (L4) hold in its subtree, and (L3) holds at every node except possibly at $x$ itself. If $h$ is black or nil, (L3) holds at $x$ too, so $x$ is valid. If $h$ is red, then $x$ is red.

Proof. By induction on the size. If $h$ is nil, line L1 returns a red node with two nil children, which is valid, with $bh = 0$. Else let $c$ be the child of $h$ on the side of $k$ and $x_c$ the result of the recursive call at line L2 or L3. Every node below $x_c$ satisfies the rules, and by Lemma A the steps of FIX-UP keep (L1), (L4) and $bh$. We follow FIX-UP in each case.

$h$ black, $k < h.key$. Then $h.right$ is black, by (L2). If $c$ is black or nil, $x_c$ is valid by induction, so if $x_c$ is red its left child is black. No test of FIX-UP is true, and $h$ is valid. If $c$ is red, $x_c$ is red and only (L3) at $x_c$ may fail. If $x_c.left$ is red, line L7 rotates right at $h$: the black top $x_c$ has the red left child $x_c.left$ and the red right child $h$, whose new left child, the old $x_c.right$, is black. Line L8 flips: the top is red with two black children, whose own children are black or valid. In both cases the result is valid.

$h$ black, $k > h.key$. Then $c$ is black or nil and $x_c$ is valid. If $x_c$ is black, nothing changes. If $x_c$ is red and $h.left$ is black, line L6 rotates left: the top $x_c$ is black, its left child $h$ is red with two black children (the old $h.left$, and the old $x_c.left$, black since $x_c$ was red), and its right child is the black old $x_c.right$. Lines L7 and L8 do nothing. If $x_c$ is red and $h.left$ is red, line L8 flips, and $h$ is red with two black children.

$h$ red. Its children are black. If $k < h.key$, $x_c$ is valid, so line L7 does not apply (if $x_c$ is red, its left child is black), and $h$ stays red, with a possibly red left child. If $k > h.key$ and $x_c$ is red, line L6 rotates left: the top $x_c$ takes the red color of $h$, and $h$ becomes its red left child, with two black children. Lines L7 and L8 do nothing. The top is red, and only (L3) at the top may fail. $\square$

INSERT. The root is black or nil, so by Lemma 1 PUT returns a valid tree with the new key. Line L10 paints the root black; this adds one to every path, so (L4) holds, and (L5) holds. An insertion of a key that is already there stops at line L4 with nothing changed (the implementation searches first).

Deletion

A call REMOVE$(h, k)$ has the precondition that $k \in K(h)$, that (L1), (L3), (L4) hold in the subtree of $h$ and (L2) holds at every node except possibly at $h$, and that one of these holds:

1. (P1) $h$ is red, with two black children;
2. (P2) $h$ is black, $h.left$ is red and $h.right$ is black;
3. (P3) $h$ is black, $h.left$ is black, $h.right$ is red, and $k \ge h.key$.

In the 2-3 view, (P1) and (P2) say that $h$ is not a 2-node, so a key can leave it. The postcondition is that the result $x$ is valid, with keys $K(h) \setminus \{k\}$ and $bh(x) = bh(h)$, and that $x$ is black if $h$ was black when the call began. DELETE-MIN$(h)$ has the same precondition with (P1) or (P2), with $k$ the least key, and the same postcondition.

Lemma 2 (FIX-UP in deletion). If both children of $h$ are valid with the same $bh$, and if $h$ is red only when both children are black, then FIX-UP$(h)$ returns a valid subtree with the same keys and $bh$. If $h$ is black and $h.right$ is black, the result is $h$ itself, black.

Proof. If $h$ is red, its children are black and no test is true. If $h$ is black: with two black children nothing changes; with a red left child and a black right child, line L7 does not apply, since the left child is valid and red, so its left child is black; with a black left child and a red right child, line L6 rotates left and gives a black top with a red left child $h$ whose two children are black, as in Lemma 1; with two red children, line L8 flips and gives a red top with two black children. $\square$

Lemma 3 (MOVE-RED-LEFT). Let $h$ be red with valid black children $l$ and $r$, and let $l.left$ be black. After MOVE-RED-LEFT$(h)$, the subtree has the same keys and $bh$, (L1) and (L4) hold, and either (a) the top is $h$, black, with two red children, each with two black children, or (b) the top is red, its right child is black and valid, and its left child is the old $h$, black, with the red left child $l$ (whose children are black) and a black right child.

Proof. Line L16 flips at $h$, a red node with two black children: $h$ is black, and $l$ and $r$ are red. The children of $l$ are black ($l.left$ by assumption, $l.right$ by (L2)), and $r.right$ is black by (L2). If $r.left$ is black, the result is (a). Else let $s = r.left$, red, with two black children. Line L17 rotates right at $r$: $s$ takes the red color of $r$ and $r$ becomes its red right child, whose left child is the old $s.right$, black. Then it rotates left at $h$: $s$ moves up with the black color of $h$, $h$ becomes its red left child, and the right child of $h$ is the old $s.left$, black. Then it flips at $s$, a black node with two red children: $s$ is red, and $h$ and $r$ are black. Now $h$ has the red left child $l$ and a black right child, and $r$ has two black children. Every step is one of Lemma A. $\square$

Lemma 4 (MOVE-RED-RIGHT). Let $h$ be red with valid black children $l$ and $r$, and let $r.left$ be black. After MOVE-RED-RIGHT$(h)$, the subtree has the same keys and $bh$, (L1) and (L4) hold, and either (a) the top is $h$, black, with two red children, each with two black children, or (b) the top $t$ is red with two black children; $t.left$ is valid, and $t.right$ is the old $h$, black, with a black left child and the red right child $r$, whose children are black; and $t.key < h.key$.

Proof. Line L18 flips at $h$: $h$ is black, and $l$ and $r$ are red. The children of $r$ are black ($r.left$ by assumption, $r.right$ by (L2)), and $l.right$ is black by (L2). If $l.left$ is black, the result is (a). Else $l.left$ is red, with black children. Line L19 rotates right at $h$: $l$ moves up with the black color of $h$, $h$ becomes its red right child, and the left child of $h$ is the old $l.right$, black. Then it flips at $l$, a black node with two red children: $l$ is red, $l.left$ is black, and $h$ is black. The node $h$ keeps the red right child $r$. Since $l$ was the left child of $h$, $l.key < h.key$. $\square$

Lemma 5 (REMOVE and DELETE-MIN). Under the precondition, REMOVE$(h, k)$ and DELETE-MIN$(h)$ meet the postcondition.

Proof. By induction on the size. In every case below, the recursive call meets the precondition, so by induction it returns a valid subtree with the same $bh$ as the child it replaces; then Lemma 2 applies to the last line, and we check its two conditions and the color of the result.

Case $k < h.key$ (lines L20 to L22). Since (P3) needs $k \ge h.key$, this case has (P1) or (P2). The key is in $h.left$, which is not nil.

• (P2): $h.left$ is red with black children, so line L21 does nothing and the call on $h.left$ has (P1). Line L22 replaces $h.left$; the right child of $h$ is black and unchanged. By Lemma 2, the result is $h$, black.
• (P1) and $h.left.left$ red: line L21 does nothing. The call on the black $h.left$ has (P2) and returns a black node. At FIX-UP, $h$ is red with two black children, so Lemma 2 applies.
• (P1) and $h.left.left$ black: $h.right$ is not nil, since $bh(h.right) = bh(h.left) \ge 1$. Line L21 calls MOVE-RED-LEFT. In Lemma 3 (a), the call on the red left child has (P1), and at FIX-UP the top is black. In Lemma 3 (b), $k$ is less than the key of the old $h$, which is the left child of the new top, so the recursion goes there, with (P2), and returns a black node; at FIX-UP the top is red with two black children.

Case $k \ge h.key$ (lines L23 to L27).

• (P2): line L23 rotates right at $h$. The new top $t$ is the old $h.left$, black, with the black left child $h.left.left$ (by (L3)) and the red right child $h$, whose children are black. Now $k > t.key$, line L24 does not apply ($t.right \ne$ nil), line L25 does nothing ($t.right$ is red), and line L27 calls REMOVE on the red $h$, which has (P1). At FIX-UP, $t$ is black with a black left child, so Lemma 2 gives a black result.
• (P3): line L23 does nothing, line L24 does not apply ($h.right \ne$ nil), and line L25 does nothing ($h.right$ is red). The red right child has two black children, by (L3) and (L2) below $h$. If $k = h.key$, line L26 calls DELETE-MIN on it, and else line L27 calls REMOVE on it; both calls have (P1). At FIX-UP, $h$ is black with a black left child, and the result is black.
• (P1): line L23 does nothing. If $k = h.key$ and $h.right$ is nil, then $bh(h.left) = 0$ and $h.left$ is black, so $h.left$ is nil: $h$ is a red leaf, and line L24 returns nil, with $bh = 0 = bh(h)$. Else $h.right$ is not nil, and neither is $h.left$, by (L4). If $h.right.left$ is red, line L25 does nothing, and the call at line L26 or L27 on the black $h.right$ has (P2) and returns a black node; at FIX-UP, $h$ is red with two black children. If $h.right.left$ is black, line L25 calls MOVE-RED-RIGHT. In Lemma 4 (a), the call on the red right child has (P1), and the top is black at FIX-UP. In Lemma 4 (b), the new top $t$ has $t.key < h.key \le k$, so line L26 does not apply, and line L27 calls REMOVE on the old $h$, which is black, with a black left child and a red right child, and $k \ge h.key$: (P3). It returns a black node, so at the FIX-UP of $t$, $t$ is red with two black children.

When line L26 runs, $h.key$ becomes the least key $m$ of $h.right$. Every key of $h.left$ is less than $k < m$, and every other key of $h.right$ is greater than $m$, so after DELETE-MIN removes $m$ from $h.right$, (L1) holds and the key $k$ is gone.

DELETE-MIN. If $h.left$ is nil, then (P2) is impossible, so $h$ is red, and as above $h$ is a red leaf and the result is nil. Else it runs the case $k < h.key$ above, with DELETE-MIN in place of REMOVE.

In every case the keys are $K(h) \setminus \{k\}$, and $bh$ is kept, by Lemma A, by induction and by Lemma 2. A result that comes from a call with $h$ black is black, as shown in each case. $\square$

DELETE. Line L11 makes sure that $k$ is in the tree. Before line L12 the tree is valid with a black root. If both children of the root are black, line L12 paints the root red, which subtracts one from every path and so keeps (L4); now (P1) holds. Else the root has a red child, which is the left one by (L2), and (P2) holds. By Lemma 5, REMOVE returns a valid tree without $k$. Line L14 paints the root black, which keeps (L4) and gives (L5).

Conclusion

Theorem. Starting from the empty tree, after any sequence of insertions and deletions the tree satisfies (L1) to (L5) and holds exactly the keys inserted and not deleted since. A search returns true exactly for these keys.

Proof. The empty tree satisfies the rules. INSERT and DELETE keep them and change the key set as stated, by Lemma 1 and Lemma 5. A search is correct by (L1). $\blacksquare$