Red–black tree

InductiveRed-black node colors#✓fully proved

The colors of red-black tree nodes are the two values red and black.

public inductive Color where
  | red
  | black
  deriving DecidableEq, Repr
Used by 51
Used byRed invariant away from the root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Okasaki's rebalancing · Black-height balanced red-black tree · Deletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Red-black insertion preserves black-height balance · Black height · Black height after double-black deletion · Insertion raises the black height by at most one · Absorbing a double-black root · Extended root color · Root color · Deletion by rebuilding gives a black root · Double-black deletion leaves a black root · Search in a red-black tree · Search in an ordered red-black tree is correct · Unbalanced red-black tree deletion · Double-black deletion · Color erasure · Recoloring the root black does not change the color erasure · Left repair after double-black deletion · Right repair after double-black deletion · Adding a black to the root · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal of a splice · Unchecked red-black insertion · Splicing two red-black trees · Blackening the root · Membership after deletion by rebuilding · Membership after insertion into a red-black tree · Membership in a splice · Leftmost key of a red-black tree · Red-black deletion yields an ordered tree · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Red property of red-black trees · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Red-black insertion preserves the red property · Recoloring the root black · Red-black tree data type · Valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

InductiveRed-black tree data type#✓fully proved

A red-black tree with keys in a type \(\alpha\) is either empty or a node consisting of a color (red or black), a left subtree, a key in \(\alpha\), and a right subtree.

No ordering, color or balance invariant is imposed by the type itself.

public inductive Tree (α : Type u) where
  | empty
  | node (color : Color) (left : Tree α) (key : α) (right : Tree α)
deriving DecidableEq, Repr
Uses 1 · Used by 78
Statement usesRed-black node colors
Used byPredicate holding at every key of a red-black tree · All keys of a red-black tree via its color erasure · All keys versus members of a red-black tree · Red invariant away from the root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Okasaki's rebalancing · Black-height balanced red-black tree · Black-height balance of a possibly double-black tree · Deletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Red-black insertion preserves black-height balance · Trees with a possibly double-black root · Black height of a possibly double-black tree · Black height · Black height after double-black deletion · Insertion raises the black height by at most one · Absorbing a double-black root · Extended root color · Root color · Deletion by rebuilding gives a black root · Double-black deletion leaves a black root · Search in a red-black tree · Search in an ordered red-black tree is correct · Unbalanced red-black tree deletion · Double-black deletion · Red-black tree deletion by rebuilding · Red-black tree deletion by the double-black method · Color erasure · Recoloring the root black does not change the color erasure · Left repair after double-black deletion · Right repair after double-black deletion · Red-black tree from a list · Adding a black to the root · Inorder traversal of a red-black tree · Inorder traversal onto a suffix · Inorder traversal of a possibly double-black tree · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal ignores colors · Inorder traversal of a splice · Ordered red-black trees have duplicate-free inorder traversals · Unchecked red-black insertion · Red-black tree insertion · Splicing two red-black trees · Blackening the root · Membership in a red-black tree · Membership after deletion by rebuilding · Keys after double-black deletion · Red-black membership is membership in the underlying binary tree · Membership in a red-black tree built from a list · Membership in the inorder traversal of a red-black tree · Membership after insertion into a red-black tree · Membership in a splice · Leftmost key of a red-black tree · The deleted key is absent after double-black deletion · The deleted key is absent after deletion by rebuilding · Ordered red-black tree · Red-black deletion yields an ordered tree · Double-black deletion preserves the search-tree order · A red-black tree is ordered exactly when its underlying binary tree is · The inorder traversal of an ordered red-black tree is strictly increasing · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Rebuilding a red-black tree from its keys · Red property of red-black trees · Red invariant for trees with a possibly double-black root · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Red-black insertion preserves the red property · Recoloring the root black · Valid red-black tree · Red-black deletion yields a valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionColor erasure#✓fully proved

The color erasure of a red-black tree is the binary tree obtained by forgetting the node colors: the empty tree goes to the empty binary tree, and a node with key \(k\) and subtrees \(l\) and \(r\) goes to the binary-tree node with key \(k\) whose subtrees are the color erasures of \(l\) and \(r\).

public def erase {α : Type u} : Tree α → BinaryTree α
  | .empty => .nil
  | .node _ left key right => .node key (erase left) (erase right)
Uses 2 · Used by 24
Statement usesRed-black node colors · Red-black tree data type
Used byPredicate holding at every key of a red-black tree · All keys of a red-black tree via its color erasure · All keys versus members of a red-black tree · Black height after double-black deletion · Search in an ordered red-black tree is correct · Recoloring the root black does not change the color erasure · Inorder traversal of a red-black tree · Inorder traversal onto a suffix · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal ignores colors · Inorder traversal of a splice · Membership in a red-black tree · Membership after deletion by rebuilding · Red-black membership is membership in the underlying binary tree · Membership in the inorder traversal of a red-black tree · Membership after insertion into a red-black tree · Ordered red-black tree · Double-black deletion preserves the search-tree order · A red-black tree is ordered exactly when its underlying binary tree is · The inorder traversal of an ordered red-black tree is strictly increasing · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants

DefinitionMembership in a red-black tree#✓fully proved

An element \(x\) is a member of a red-black tree \(t\) when \(x\) is a member of the binary tree obtained from \(t\) by erasing its colors, that is, when \(x\) equals the key of some node of \(t\).

Membership is structural: it does not use the search-tree ordering.

public def Mem {α : Type u} (x : α) (tree : Tree α) : Prop :=
  BinarySearchTree.Mem x (erase tree)
Uses 3 · Used by 18
Statement usesMembership in a binary tree · Red-black tree data type · Color erasure
Used byAll keys versus members of a red-black tree · Black height after double-black deletion · Search in an ordered red-black tree is correct · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Keys after double-black deletion · Red-black membership is membership in the underlying binary tree · Membership in a red-black tree built from a list · Membership in the inorder traversal of a red-black tree · Membership after insertion into a red-black tree · Membership in a splice · The deleted key is absent after double-black deletion · The deleted key is absent after deletion by rebuilding · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants

DefinitionInorder traversal onto a suffix#✓fully proved

For a red-black tree \(t\) and a list \(s\), this is the accumulator form of the binary-search-tree inorder traversal applied to the color erasure of \(t\): for the empty tree it returns \(s\), and for a node with key \(k\) and subtrees \(l\) and \(r\) it returns the result for \(l\) with suffix the list \(k\) followed by \(u\), where \(u\) is the result for \(r\) with suffix \(s\).

Thus the result lists the keys of \(t\) in inorder followed by \(s\), in time linear in the size of \(t\).

public def inorderAux {α : Type u} (tree : Tree α) (suffix : List α) : List α :=
  BinarySearchTree.inorderAux (erase tree) suffix
Uses 3
Statement usesInorder traversal of a binary tree with an accumulator · Red-black tree data type · Color erasure

DefinitionInorder traversal of a red-black tree#✓fully proved

The inorder traversal of a red-black tree \(t\) is the binary-search-tree inorder traversal of the color erasure of \(t\), computed in linear time with an accumulator starting from the empty list. It lists the keys of \(t\) from left to right: the empty tree gives the empty list, and a node with key \(k\) and subtrees \(l\) and \(r\) gives the traversal of \(l\), then \(k\), then the traversal of \(r\).

public def inorder {α : Type u} (tree : Tree α) : List α :=
  BinarySearchTree.inorder (erase tree)
Uses 3 · Used by 21
Statement usesInorder traversal of a binary tree · Red-black tree data type · Color erasure
Used byDeletion by rebuilding is black-height balanced · Black height after double-black deletion · Deletion by rebuilding gives a black root · Inorder traversal of a possibly double-black tree · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal ignores colors · Inorder traversal of a splice · Ordered red-black trees have duplicate-free inorder traversals · Membership after deletion by rebuilding · Keys after double-black deletion · Membership in the inorder traversal of a red-black tree · Membership after insertion into a red-black tree · Red-black deletion yields an ordered tree · Double-black deletion preserves the search-tree order · The inorder traversal of an ordered red-black tree is strictly increasing · Red-black insertion preserves the search-tree order · Rebuilding a red-black tree from its keys · Red-black deletion yields a tree with no red-red edge · Red-black deletion yields a valid red-black tree · Double-black deletion yields a valid tree from the structural invariants

DefinitionPredicate holding at every key of a red-black tree#✓fully proved

For a predicate \(p\) on \(\alpha\) and a red-black tree \(t\) with keys in \(\alpha\), \(p\) holds at every key of \(t\) when \(p\) holds at every key of the binary search tree obtained from \(t\) by erasing colors.

public def All {α : Type u} (p : α → Prop) (tree : Tree α) : Prop :=
  BinarySearchTree.All p (erase tree)
Uses 3 · Used by 10
Statement usesA predicate holding at every key of a binary tree · Red-black tree data type · Color erasure
Used byAll keys of a red-black tree via its color erasure · All keys versus members of a red-black tree · Black height after double-black deletion · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants

DefinitionOrdered red-black tree#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). A red-black tree with keys in \(\alpha\) is ordered when, at every node with key \(k\), every key \(y\) in the left subtree satisfies \(y < k\) and every key \(z\) in the right subtree satisfies \(k < z\).

Equivalently, the binary tree obtained by erasing the colors is an ordered binary search tree.

public def Ordered {α : Type u} [LT α] (tree : Tree α) : Prop :=
  BinarySearchTree.Ordered (erase tree)
Uses 3 · Used by 26
Statement usesOrdered binary trees · Red-black tree data type · Color erasure
Used byDeletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Black height after double-black deletion · Deletion by rebuilding gives a black root · Search in an ordered red-black tree is correct · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Ordered red-black trees have duplicate-free inorder traversals · Membership after deletion by rebuilding · Keys after double-black deletion · The deleted key is absent after double-black deletion · The deleted key is absent after deletion by rebuilding · Red-black deletion yields an ordered tree · Double-black deletion preserves the search-tree order · A red-black tree is ordered exactly when its underlying binary tree is · The inorder traversal of an ordered red-black tree is strictly increasing · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

TheoremRed-black membership is membership in the underlying binary tree#✓fully proved

For every red-black tree \(t\) and every \(x\), \(x\) is a member of \(t\) if and only if \(x\) is a member of the binary tree obtained from \(t\) by erasing its colors.

This holds by definition.

public theorem mem_erase {α : Type u} {x : α} {tree : Tree α} :
    x ∈ tree ↔ x ∈ erase tree
Uses 4
Statement usesMembership in a binary tree · Membership in a red-black tree · Red-black tree data type · Color erasure

TheoremAll keys of a red-black tree via its color erasure#✓fully proved

For every predicate \(p\) on \(\alpha\) and every red-black tree \(t\) with keys in \(\alpha\), \(p\) holds at every key of \(t\) if and only if \(p\) holds at every key of the binary search tree obtained from \(t\) by erasing colors. This holds by definition.

public theorem all_erase {α : Type u} {p : α → Prop} {tree : Tree α} :
    All p tree ↔ BinarySearchTree.All p (erase tree)
Uses 4
Statement usesA predicate holding at every key of a binary tree · Predicate holding at every key of a red-black tree · Red-black tree data type · Color erasure

TheoremA red-black tree is ordered exactly when its underlying binary tree is#✓fully proved

For keys with a relation \(<\), a red-black tree \(t\) is ordered if and only if the binary tree obtained from \(t\) by erasing its colors is an ordered binary search tree.

This holds by definition.

public theorem ordered_erase {α : Type u} [LT α] {tree : Tree α} :
    Ordered tree ↔ BinarySearchTree.Ordered (erase tree)
Uses 4
Statement usesOrdered binary trees · Ordered red-black tree · Red-black tree data type · Color erasure

TheoremInorder traversal ignores colors#✓fully proved

For every red-black tree \(t\), the inorder traversal of \(t\) equals the binary-search-tree inorder traversal of the color erasure of \(t\); this holds by definition.

public theorem inorder_erase {α : Type u} (tree : Tree α) :
    inorder tree = BinarySearchTree.inorder (erase tree)
Uses 4
Statement usesInorder traversal of a binary tree · Red-black tree data type · Color erasure · Inorder traversal of a red-black tree

DefinitionRoot color#✓fully proved

The root color of a red-black tree is the color of its root node; the empty tree has root color black.

public def colorOf {α : Type u} : Tree α → Color
  | .empty => .black
  | .node color _ _ _ => color
Uses 2 · Used by 18
Statement usesRed-black node colors · Red-black tree data type
Used byDeletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Black height after double-black deletion · Extended root color · Deletion by rebuilding gives a black root · Double-black deletion leaves a black root · Inorder traversal after deletion by rebuilding · Red-black deletion yields an ordered tree · Red property of red-black trees · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Red-black insertion preserves the red property · Valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionRed property of red-black trees#✓fully proved

A red-black tree satisfies the red property when no red node has a red child, where empty subtrees count as black.

public def RedOk {α : Type u} : Tree α → Prop
  | .empty => True
  | .node .red left _ right =>
      RedOk left ∧ RedOk right ∧ colorOf left = .black ∧ colorOf right = .black
  | .node .black left _ right => RedOk left ∧ RedOk right
Uses 3 · Used by 17
Statement usesRed-black node colors · Red-black tree data type · Root color
Used byRed invariant away from the root · Deletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Black height after double-black deletion · Deletion by rebuilding gives a black root · Inorder traversal after deletion by rebuilding · Red-black deletion yields an ordered tree · Red invariant for trees with a possibly double-black root · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Red-black insertion preserves the red property · Valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionRed invariant away from the root#✓fully proved

A red-black tree satisfies the relaxed red invariant when it is empty, or when its left and right subtrees both satisfy the red invariant (no red node has a red child). The root itself is unconstrained, so a red root may have a red child.

This is the intermediate invariant of Okasaki's unchecked insertion.

public def AlmostRedOk {α : Type u} : Tree α → Prop
  | .empty => True
  | .node _ left _ right => RedOk left ∧ RedOk right
Uses 3 · Used by 1
Statement usesRed-black node colors · Red property of red-black trees · Red-black tree data type
Used byRed-black insertion preserves the red property

DefinitionBlack height#✓fully proved

The black height of a red-black tree is the number of black nodes on its leftmost root-to-leaf path, counting the empty leaf as one black node: the empty tree has black height \(1\), a red node has the black height of its left subtree, and a black node has the black height of its left subtree plus \(1\).

public def blackHeight {α : Type u} : Tree α → Nat
  | .empty => 1
  | .node .red left _ _ => blackHeight left
  | .node .black left _ _ => blackHeight left + 1
Uses 2 · Used by 7
Statement usesRed-black node colors · Red-black tree data type
Used byBlack-height balanced red-black tree · Black-height balance of a possibly double-black tree · Red-black insertion preserves black-height balance · Black height of a possibly double-black tree · Black height after double-black deletion · Insertion raises the black height by at most one · Double-black deletion yields a valid tree from the structural invariants

DefinitionBlack-height balanced red-black tree#✓fully proved

A red-black tree is balanced when every root-to-leaf path contains the same number of black nodes. Recursively: the empty tree is balanced, and a node is balanced when both of its subtrees are balanced and have the same black height (the number of black nodes on the leftmost root-to-leaf path, counting the leaf).

public def Balanced {α : Type u} : Tree α → Prop
  | .empty => True
  | .node _ left _ right =>
      Balanced left ∧ Balanced right ∧ blackHeight left = blackHeight right
Uses 3 · Used by 16
Statement usesRed-black node colors · Red-black tree data type · Black height
Used byBlack-height balance of a possibly double-black tree · Deletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Red-black insertion preserves black-height balance · Black height after double-black deletion · Deletion by rebuilding gives a black root · Inorder traversal after deletion by rebuilding · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionValid red-black tree#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). A red-black tree with keys in \(\alpha\) is valid when it is ordered, satisfies the red property (no red node has a red child), is balanced (every root-to-leaf path contains the same number of black nodes), and its root is black, where the empty tree counts as black.

public def Valid {α : Type u} [LT α] (tree : Tree α) : Prop :=
  Ordered tree ∧ RedOk tree ∧ Balanced tree ∧ colorOf tree = .black
Uses 6 · Used by 14
Statement usesBlack-height balanced red-black tree · Red-black node colors · Ordered red-black tree · Red property of red-black trees · Red-black tree data type · Root color
Used byDeletion by rebuilding is black-height balanced · Double-black deletion keeps a valid tree balanced · Black height after double-black deletion · Deletion by rebuilding gives a black root · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Double-black deletion from a valid tree keeps the red invariant · Red-black deletion yields a valid red-black tree · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants · The empty red-black tree is valid · Red-black trees built from a list are valid · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionSearch in a red-black tree#✓fully proved

Searching a red-black tree over a linearly ordered type for a key \(x\) returns a Boolean, ignoring colors: the empty tree gives false, and at a node with key \(k\) the search continues in the left subtree if \(x < k\), continues in the right subtree if \(k < x\), and returns true otherwise.

public def contains {α : Type u} [LinearOrder α] (x : α) : Tree α → Bool
  | .empty => false
  | .node _ left key right =>
      if x < key then contains x left
      else if key < x then contains x right
      else true
Uses 2 · Used by 1
Statement usesRed-black node colors · Red-black tree data type
Used bySearch in an ordered red-black tree is correct

DefinitionOkasaki's rebalancing#✓fully proved

Given a color \(c\), red-black trees \(l\) and \(r\), and a key \(k\), rebalancing produces a tree as follows. Suppose \(c\) is black and one of these configurations occurs, taking the first that applies: \(l\) is a red node with a red left child; \(l\) is a red node with a red right child; \(r\) is a red node with a red left child; \(r\) is a red node with a red right child. The black root and the two red nodes then hold three keys and leave four subtrees, which read in inorder as \(t_1, x, t_2, y, t_3, z, t_4\). The result is a red node with key \(y\), left child the black node with subtrees \(t_1, t_2\) and key \(x\), and right child the black node with subtrees \(t_3, t_4\) and key \(z\). In every other case the result is the node with color \(c\), left subtree \(l\), key \(k\) and right subtree \(r\).

def balance {α : Type u} : Color → Tree α → α → Tree α → Tree α
  | .black, .node .red (.node .red a x b) y c, z, d =>
      .node .red (.node .black a x b) y (.node .black c z d)
  | .black, .node .red a x (.node .red b y c), z, d =>
      .node .red (.node .black a x b) y (.node .black c z d)
  | .black, a, x, .node .red (.node .red b y c) z d =>
      .node .red (.node .black a x b) y (.node .black c z d)
  | .black, a, x, .node .red b y (.node .red c z d) =>
      .node .red (.node .black a x b) y (.node .black c z d)
  | color, left, key, right => .node color left key right
Uses 2 · Used by 6
Statement usesRed-black node colors · Red-black tree data type
Used byRed-black insertion preserves black-height balance · Insertion raises the black height by at most one · Unchecked red-black insertion · Membership after insertion into a red-black tree · Red-black insertion preserves the search-tree order · Red-black insertion preserves the red property

DefinitionUnchecked red-black insertion#✓fully proved

For keys from a linearly ordered type, the unchecked insertion of \(x\) into a red-black tree is defined by recursion on the tree. Inserting \(x\) into the empty tree gives a red node with key \(x\) and two empty subtrees. Inserting \(x\) into a node with color \(c\), left subtree \(l\), key \(k\) and right subtree \(r\) gives: if \(x < k\), Okasaki's rebalancing of color \(c\), left subtree the insertion of \(x\) into \(l\), key \(k\) and right subtree \(r\); if \(k < x\), Okasaki's rebalancing of color \(c\), left subtree \(l\), key \(k\) and right subtree the insertion of \(x\) into \(r\); otherwise the node itself, unchanged.

The result may have a red root with a red child, so it need not satisfy the red invariant.

def ins {α : Type u} [LinearOrder α] (x : α) : Tree α → Tree α
  | .empty => .node .red .empty x .empty
  | tree@(.node color left key right) =>
      if x < key then balance color (ins x left) key right
      else if key < x then balance color left key (ins x right)
      else tree
Uses 3 · Used by 7
Statement usesRed-black node colors · Red-black tree data type · Okasaki's rebalancing
Used byRed-black insertion preserves black-height balance · Insertion raises the black height by at most one · Red-black tree insertion · Membership after insertion into a red-black tree · Red-black insertion preserves the search-tree order · Red-black insertion preserves the red property · Red-black insertion yields a valid tree from the invariants

DefinitionBlackening the root#✓fully proved

Recoloring the root of a red-black tree black leaves the empty tree unchanged and turns a node with any color, left subtree \(l\), key \(k\) and right subtree \(r\) into the black node with left subtree \(l\), key \(k\) and right subtree \(r\).

def makeBlack {α : Type u} : Tree α → Tree α
  | .empty => .empty
  | .node _ left key right => .node .black left key right
Uses 2 · Used by 8
Statement usesRed-black node colors · Red-black tree data type
Used byRed-black insertion preserves black-height balance · Insertion raises the black height by at most one · Recoloring the root black does not change the color erasure · Red-black tree insertion · Membership after insertion into a red-black tree · Red-black insertion preserves the search-tree order · Red-black insertion preserves the red property · Red-black insertion yields a valid tree from the invariants

TheoremRecoloring the root black does not change the color erasure#✓fully proved

For every red-black tree \(t\), the color erasure of the tree obtained from \(t\) by recoloring its root black (the empty tree is left unchanged) equals the color erasure of \(t\).

public theorem erase_makeBlack {α : Type u} {tree : Tree α} :
    erase (makeBlack tree) = erase tree
Uses 4
Statement usesRed-black tree data type · Color erasure · Blackening the root
Proof usesRed-black node colors

DefinitionRed-black tree insertion#✓fully proved

For keys from a linearly ordered type, inserting \(x\) into a red-black tree \(t\) gives the unchecked insertion of \(x\) into \(t\) with its root recolored black.

public def insert {α : Type u} [LinearOrder α] (x : α) (tree : Tree α) :
    Tree α :=
  makeBlack (ins x tree)
Uses 3 · Used by 9
Statement usesRed-black tree data type · Unchecked red-black insertion · Blackening the root
Used byRed-black insertion preserves black-height balance · Insertion raises the black height by at most one · Red-black tree from a list · Membership in a red-black tree built from a list · Membership after insertion into a red-black tree · Red-black insertion preserves the search-tree order · Red-black insertion preserves the red property · Red-black insertion preserves validity · Red-black insertion yields a valid tree from the invariants

DefinitionRed-black tree from a list#✓fully proved

The red-black tree built from a list over a linearly ordered type inserts the elements of the list into the empty tree from right to left: the empty list gives the empty tree, and a list with head \(x\) and tail \(xs\) gives the insertion of \(x\) into the tree built from \(xs\).

public def fromList {α : Type u} [LinearOrder α] : List α → Tree α
  | [] => .empty
  | x :: xs => insert x (fromList xs)
Uses 2 · Used by 5
Statement usesRed-black tree data type · Red-black tree insertion
Used byInorder traversal after deletion by rebuilding · Membership after deletion by rebuilding · Membership in a red-black tree built from a list · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremAll keys versus members of a red-black tree#✓fully proved

For every predicate \(p\) on \(\alpha\) and every red-black tree \(t\) with keys in \(\alpha\), \(p\) holds at every key of \(t\) if and only if \(p(x)\) holds for every \(x \in \alpha\) that is a (structural) member of \(t\).

public theorem all_iff_forall_mem {α : Type u} {p : α → Prop} {tree : Tree α} :
    All p tree ↔ ∀ x, x ∈ tree → p x
Uses 5 · Used by 8
Statement usesPredicate holding at every key of a red-black tree · Membership in a red-black tree · Red-black tree data type
Proof usesA predicate holds at all keys of a binary tree iff it holds at all its members · Color erasure
Used byBlack height after double-black deletion · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants

TheoremMembership in the inorder traversal of a red-black tree#✓fully proved

For every red-black tree \(t\) and every \(x\), \(x\) occurs in the inorder traversal of \(t\) if and only if \(x\) is a member of \(t\).

public theorem mem_inorder {α : Type u} {x : α} {tree : Tree α} :
    x ∈ inorder tree ↔ x ∈ tree
Uses 5 · Used by 9
Statement usesMembership in a red-black tree · Red-black tree data type · Inorder traversal of a red-black tree
Proof usesMembership in the inorder traversal of a binary tree · Color erasure
Used byBlack height after double-black deletion · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Keys after double-black deletion · Membership after insertion into a red-black tree · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Double-black deletion yields a valid tree from the structural invariants

TheoremThe inorder traversal of an ordered red-black tree is strictly increasing#✓fully proved

For keys from a linearly ordered type, if a red-black tree \(t\) is ordered, then every entry of the inorder traversal of \(t\) is strictly smaller than every later entry.

public theorem ordered_inorder {α : Type u} [LinearOrder α] {tree : Tree α}
    (h : Ordered tree) : List.Pairwise (· < ·) (inorder tree)
Uses 5 · Used by 4
Statement usesOrdered red-black tree · Red-black tree data type · Inorder traversal of a red-black tree
Proof usesThe inorder traversal of an ordered binary tree is strictly increasing · Color erasure
Used byInorder traversal after deletion by rebuilding · Ordered red-black trees have duplicate-free inorder traversals · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order

TheoremMembership after insertion into a red-black tree#✓fully proved

For keys from a linearly ordered type, a key \(y\) is a member of the red-black tree obtained by inserting \(x\) into \(t\) if and only if \(y = x\) or \(y\) is a member of \(t\).

public theorem mem_insert {α : Type u} [LinearOrder α] {x y : α} {tree : Tree α} :
    y ∈ insert x tree ↔ y = x ∨ y ∈ tree
Uses 12 · Used by 1
Statement usesMembership in a red-black tree · Red-black tree data type · Red-black tree insertion
Proof usesInorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Red-black node colors · Okasaki's rebalancing · Color erasure · Inorder traversal of a red-black tree · Unchecked red-black insertion · Blackening the root · Membership in the inorder traversal of a red-black tree
Used byMembership in a red-black tree built from a list

TheoremRed-black insertion preserves the search-tree order#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\) a key, and \(t\) a red-black tree with keys in \(\alpha\). If \(t\) is ordered (at every node with key \(k\), every key in the left subtree is less than \(k\) and every key in the right subtree is greater than \(k\)), then the tree obtained by inserting \(x\) into \(t\) is ordered.

public theorem ordered_insert {α : Type u} [LinearOrder α] {x : α} {tree : Tree α}
    (h : Ordered tree) : Ordered (insert x tree)
Uses 18 · Used by 1
Statement usesOrdered red-black tree · Red-black tree data type · Red-black tree insertion
Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Red-black node colors · Membership in a red-black tree · All keys versus members of a red-black tree · Okasaki's rebalancing · Color erasure · Inorder traversal of a red-black tree · Unchecked red-black insertion · Blackening the root · Membership in the inorder traversal of a red-black tree · The inorder traversal of an ordered red-black tree is strictly increasing
Used byRed-black insertion yields a valid tree from the invariants

TheoremRed-black insertion preserves the red property#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\) a key, and \(t\) a red-black tree with keys in \(\alpha\). If no red node of \(t\) has a red child, then no red node of the tree obtained by inserting \(x\) into \(t\) has a red child.

public theorem redOk_insert {α : Type u} [LinearOrder α] {x : α} {tree : Tree α}
    (h : RedOk tree) : RedOk (insert x tree)
Uses 9 · Used by 1
Statement usesRed property of red-black trees · Red-black tree data type · Red-black tree insertion
Proof usesRed invariant away from the root · Red-black node colors · Okasaki's rebalancing · Root color · Unchecked red-black insertion · Blackening the root
Used byRed-black insertion yields a valid tree from the invariants

TheoremRed-black insertion preserves black-height balance#✓fully proved

Let \(\alpha\) be a linearly ordered type. If a red-black tree \(t\) with keys in \(\alpha\) is balanced (every root-to-leaf path contains the same number of black nodes), then for every \(x \in \alpha\) the tree obtained by inserting \(x\) into \(t\) is balanced.

public theorem balanced_insert {α : Type u} [LinearOrder α] {x : α} {tree : Tree α}
    (h : Balanced tree) : Balanced (insert x tree)
Uses 8 · Used by 1
Statement usesBlack-height balanced red-black tree · Red-black tree data type · Red-black tree insertion
Proof usesRed-black node colors · Okasaki's rebalancing · Black height · Unchecked red-black insertion · Blackening the root
Used byRed-black insertion yields a valid tree from the invariants

TheoremInsertion raises the black height by at most one#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every red-black tree \(t\) with keys in \(\alpha\) and every \(x \in \alpha\), the black height of the tree obtained by inserting \(x\) into \(t\) equals either the black height of \(t\) or the black height of \(t\) plus one.

Any increase comes from recoloring the root black at the end of insertion.

public theorem blackHeight_insert {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} :
    blackHeight (insert x tree) = blackHeight tree ∨
      blackHeight (insert x tree) = blackHeight tree + 1
Uses 7
Statement usesRed-black tree data type · Black height · Red-black tree insertion
Proof usesRed-black node colors · Okasaki's rebalancing · Unchecked red-black insertion · Blackening the root

TheoremRed-black insertion yields a valid tree from the invariants#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\) a key, and \(t\) a red-black tree with keys in \(\alpha\) that is ordered, satisfies the red property (no red node has a red child), and is balanced (every root-to-leaf path contains the same number of black nodes). Then the tree obtained by inserting \(x\) into \(t\) is valid.

The root of \(t\) need not be black, since insertion recolors the root black.

public theorem valid_insert_of_invariants {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hOrdered : Ordered tree) (hRedOk : RedOk tree)
    (hBalanced : Balanced tree) : Valid (insert x tree)
Uses 13 · Used by 1
Statement usesBlack-height balanced red-black tree · Ordered red-black tree · Red property of red-black trees · Red-black tree data type · Valid red-black tree · Red-black tree insertion
Proof usesRed-black node colors · Red-black insertion preserves black-height balance · Root color · Unchecked red-black insertion · Blackening the root · Red-black insertion preserves the search-tree order · Red-black insertion preserves the red property
Used byRed-black insertion preserves validity

TheoremRed-black insertion preserves validity#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(x \in \alpha\). If \(t\) is a valid red-black tree with keys in \(\alpha\), then the tree obtained by inserting \(x\) into \(t\) is also valid.

public theorem valid_insert {α : Type u} [LinearOrder α] {x : α} {tree : Tree α}
    (h : Valid tree) : Valid (insert x tree)
Uses 9 · Used by 1
Statement usesRed-black tree data type · Valid red-black tree · Red-black tree insertion
Proof usesBlack-height balanced red-black tree · Red-black node colors · Ordered red-black tree · Red property of red-black trees · Root color · Red-black insertion yields a valid tree from the invariants
Used byRed-black trees built from a list are valid

TheoremSearch in an ordered red-black tree is correct#✓fully proved

Let \(t\) be a red-black tree over a linearly ordered type that is ordered (every left key is smaller and every right key larger, recursively). Then for every key \(x\), the search for \(x\) in \(t\) returns true if and only if \(x\) is a key of some node of \(t\).

public theorem contains_eq_true_iff {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (h : Ordered tree) :
    contains x tree = true ↔ x ∈ tree
Uses 8
Statement usesMembership in a red-black tree · Ordered red-black tree · Red-black tree data type · Search in a red-black tree
Proof usesSearch in a binary search tree · Search in a binary search tree is correct · Red-black node colors · Color erasure

TheoremOrdered red-black trees have duplicate-free inorder traversals#✓fully proved

For a red-black tree \(t\) over a linearly ordered type that is ordered (every left key is smaller and every right key larger, recursively), the inorder traversal of \(t\) contains no key twice.

public theorem inorder_nodup {α : Type u} [LinearOrder α] {tree : Tree α}
    (h : Ordered tree) : (inorder tree).Nodup
Uses 4 · Used by 1
Statement usesOrdered red-black tree · Red-black tree data type · Inorder traversal of a red-black tree
Proof usesThe inorder traversal of an ordered red-black tree is strictly increasing
Used byKeys after double-black deletion

TheoremThe empty red-black tree is valid#✓fully proved

For every type \(\alpha\) with a relation \(<\), the empty red-black tree with keys in \(\alpha\) is a valid red-black tree.

public theorem valid_empty {α : Type u} [LT α] : Valid (.empty : Tree α)
Uses 7 · Used by 1
Statement usesRed-black tree data type · Valid red-black tree
Proof usesBlack-height balanced red-black tree · Red-black node colors · Ordered red-black tree · Red property of red-black trees · Root color
Used byRed-black trees built from a list are valid

TheoremRed-black trees built from a list are valid#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every list \(l\) of elements of \(\alpha\), the red-black tree obtained from the empty tree by inserting the elements of \(l\) one at a time, from the last to the first, is valid.

public theorem valid_fromList {α : Type u} [LinearOrder α] {xs : List α} :
    Valid (fromList xs)
Uses 4 · Used by 6
Statement usesValid red-black tree · Red-black tree from a list
Proof usesThe empty red-black tree is valid · Red-black insertion preserves validity
Used byDeletion by rebuilding is black-height balanced · Deletion by rebuilding gives a black root · Inorder traversal after deletion by rebuilding · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Red-black deletion yields a valid red-black tree

TheoremMembership in a red-black tree built from a list#✓fully proved

For keys from a linearly ordered type and every list \(xs\), a key \(x\) is a member of the red-black tree built from \(xs\) by successive insertion if and only if \(x\) occurs in \(xs\).

public theorem mem_fromList {α : Type u} [LinearOrder α] {x : α} {xs : List α} :
    x ∈ fromList xs ↔ x ∈ xs
Uses 5 · Used by 2
Statement usesMembership in a red-black tree · Red-black tree data type · Red-black tree from a list
Proof usesRed-black tree insertion · Membership after insertion into a red-black tree
Used byInorder traversal after deletion by rebuilding · Membership after deletion by rebuilding

DefinitionSplicing two red-black trees#✓fully proved

The splice of a red-black tree \(t\) with a red-black tree \(s\) is defined by recursion on \(t\). The splice of the empty tree with \(s\) is \(s\). The splice of the node with color \(c\), left subtree \(l\), key \(k\) and right subtree \(r\) with \(s\) is the node with color \(c\), left subtree \(l\), key \(k\) and right subtree the splice of \(r\) with \(s\).

So \(s\) becomes the right subtree of the rightmost node of \(t\), and all existing colors are kept.

public def join {α : Type u} : Tree α → Tree α → Tree α
  | .empty, right => right
  | .node color left key right, other =>
      .node color left key (join right other)
Uses 2 · Used by 6
Statement usesRed-black node colors · Red-black tree data type
Used byUnbalanced red-black tree deletion · Inorder traversal after deletion by rebuilding · Inorder traversal of a splice · Membership after deletion by rebuilding · Membership in a splice · Joining separated ordered trees preserves order

DefinitionUnbalanced red-black tree deletion#✓fully proved

For a key \(x\) of a linearly ordered type, unbalanced deletion of \(x\) from a red-black tree is defined by recursion on the tree. The empty tree stays empty. At a node with color \(c\), left subtree \(l\), key \(k\) and right subtree \(r\): if \(x < k\), the result is the node with color \(c\), left subtree the unbalanced deletion of \(x\) from \(l\), key \(k\) and right subtree \(r\); if \(k < x\), it is the node with color \(c\), left subtree \(l\), key \(k\) and right subtree the unbalanced deletion of \(x\) from \(r\); otherwise (so \(x = k\)) it is the splice of \(l\) with \(r\).

Colors are kept, so the result need not satisfy the red invariant or be black-height balanced.

def del {α : Type u} [LinearOrder α] (x : α) : Tree α → Tree α
  | .empty => .empty
  | .node color left key right =>
      if x < key then .node color (del x left) key right
      else if key < x then .node color left key (del x right)
      else join left right
Uses 3 · Used by 8
Statement usesRed-black node colors · Red-black tree data type · Splicing two red-black trees
Used byDeletion by rebuilding is black-height balanced · Deletion by rebuilding gives a black root · Red-black tree deletion by rebuilding · Inorder traversal after deletion by rebuilding · Membership after deletion by rebuilding · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Red-black deletion yields a valid red-black tree

DefinitionRebuilding a red-black tree from its keys#✓fully proved

For a linearly ordered key type, the rebuild of a red-black tree \(t\) is the tree obtained from the empty tree by inserting the keys of the inorder traversal of \(t\) one at a time with Okasaki insertion, starting from the last key.

The result is a valid red-black tree whose keys are exactly the keys of \(t\).

def rebalance {α : Type u} [LinearOrder α] (tree : Tree α) : Tree α :=
  fromList (inorder tree)
Uses 3 · Used by 8
Statement usesRed-black tree data type · Red-black tree from a list · Inorder traversal of a red-black tree
Used byDeletion by rebuilding is black-height balanced · Deletion by rebuilding gives a black root · Red-black tree deletion by rebuilding · Inorder traversal after deletion by rebuilding · Membership after deletion by rebuilding · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Red-black deletion yields a valid red-black tree

DefinitionRed-black tree deletion by rebuilding#✓fully proved

For a key \(x\) of a linearly ordered type and a red-black tree \(t\), deleting \(x\) from \(t\) by rebuilding first forms the unbalanced deletion of \(x\) from \(t\), then rebalances it: starting from the empty tree, it inserts the keys of the inorder traversal of that tree one at a time, from the last key to the first.

public def delete {α : Type u} [LinearOrder α] (x : α) (tree : Tree α) :
    Tree α :=
  rebalance (del x tree)
Uses 3 · Used by 8
Statement usesRed-black tree data type · Unbalanced red-black tree deletion · Rebuilding a red-black tree from its keys
Used byDeletion by rebuilding is black-height balanced · Deletion by rebuilding gives a black root · Inorder traversal after deletion by rebuilding · Membership after deletion by rebuilding · The deleted key is absent after deletion by rebuilding · Red-black deletion yields an ordered tree · Red-black deletion yields a tree with no red-red edge · Red-black deletion yields a valid red-black tree

TheoremMembership in a splice#✓fully proved

For red-black trees \(t\) and \(s\) with keys of any type, a key \(x\) belongs to the splice of \(t\) with \(s\) if and only if \(x\) belongs to \(t\) or \(x\) belongs to \(s\).

public theorem mem_join {α : Type u} {x : α} {left right : Tree α} :
    x ∈ join left right ↔ x ∈ left ∨ x ∈ right
Uses 4 · Used by 3
Statement usesMembership in a red-black tree · Red-black tree data type · Splicing two red-black trees
Proof usesRed-black node colors
Used byInorder traversal after deletion by rebuilding · Membership after deletion by rebuilding · Joining separated ordered trees preserves order

TheoremInorder traversal of a splice#✓fully proved

For red-black trees \(t\) and \(s\) with keys of any type, the inorder traversal of the splice of \(t\) with \(s\) is the inorder traversal of \(t\) followed by the inorder traversal of \(s\).

public theorem inorder_join {α : Type u} {left right : Tree α} :
    inorder (join left right) = inorder left ++ inorder right
Uses 7 · Used by 1
Statement usesRed-black tree data type · Inorder traversal of a red-black tree · Splicing two red-black trees
Proof usesInorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Red-black node colors · Color erasure
Used byInorder traversal after deletion by rebuilding

TheoremJoining separated ordered trees preserves order#✓fully proved

Let \(<\) be a relation on the keys, and let \(L\) and \(R\) be red-black trees that are ordered for \(<\) such that \(a < b\) for every key \(a\) of \(L\) and every key \(b\) of \(R\). Then the join of \(L\) and \(R\), obtained by putting \(R\) in place of the empty right subtree of the rightmost node of \(L\) (or \(R\) itself if \(L\) is empty) and keeping all colors, is ordered.

public theorem ordered_join {α : Type u} [LT α] {left right : Tree α}
    (hLeft : Ordered left) (hRight : Ordered right)
    (hSeparated : ∀ a ∈ left, ∀ b ∈ right, a < b) :
    Ordered (join left right)
Uses 12 · Used by 1
Statement usesMembership in a red-black tree · Ordered red-black tree · Red-black tree data type · Splicing two red-black trees
Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · Predicate holding at every key of a red-black tree · Red-black node colors · All keys versus members of a red-black tree · Color erasure · Membership in a splice
Used byInorder traversal after deletion by rebuilding

TheoremMembership after deletion by rebuilding#✓fully proved

Let \(x\) and \(y\) be keys of a linearly ordered type and let \(t\) be an ordered red-black tree. Then \(y\) belongs to the tree obtained from \(t\) by deleting \(x\) by rebuilding if and only if \(y\) belongs to \(t\) and \(y \ne x\).

public theorem mem_delete {α : Type u} [LinearOrder α] {x y : α}
    {tree : Tree α} (hTree : Ordered tree) :
    y ∈ delete x tree ↔ y ∈ tree ∧ y ≠ x
Uses 19 · Used by 1
Statement usesMembership in a red-black tree · Ordered red-black tree · Red-black tree data type · Red-black tree deletion by rebuilding
Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · Predicate holding at every key of a red-black tree · Red-black node colors · All keys versus members of a red-black tree · Unbalanced red-black tree deletion · Color erasure · Red-black tree from a list · Inorder traversal of a red-black tree · Splicing two red-black trees · Membership in a red-black tree built from a list · Membership in the inorder traversal of a red-black tree · Membership in a splice · Rebuilding a red-black tree from its keys
Used byThe deleted key is absent after deletion by rebuilding

TheoremThe deleted key is absent after deletion by rebuilding#✓fully proved

Let \(x\) be a key of a linearly ordered type and let \(t\) be an ordered red-black tree. Then \(x\) does not belong to the tree obtained from \(t\) by deleting \(x\) by rebuilding.

public theorem not_mem_delete_self {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Ordered tree) : x ∉ delete x tree
Uses 5
Statement usesMembership in a red-black tree · Ordered red-black tree · Red-black tree data type · Red-black tree deletion by rebuilding
Proof usesMembership after deletion by rebuilding

TheoremInorder traversal after deletion by rebuilding#✓fully proved

Let \(x\) be a key of a linearly ordered type and let \(t\) be an ordered red-black tree. Then the inorder traversal of the tree obtained from \(t\) by deleting \(x\) by rebuilding is the inorder traversal of \(t\) with the first occurrence of \(x\) removed (it is unchanged if \(x\) does not occur).

public theorem inorder_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Ordered tree) :
    inorder (delete x tree) = (inorder tree).erase x
Uses 28
Statement usesOrdered red-black tree · Red-black tree data type · Red-black tree deletion by rebuilding · Inorder traversal of a red-black tree
Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Black-height balanced red-black tree · Red-black node colors · Membership in a red-black tree · Red property of red-black trees · All keys versus members of a red-black tree · Root color · Unbalanced red-black tree deletion · Color erasure · Red-black tree from a list · Inorder traversal of a splice · Splicing two red-black trees · Membership in a red-black tree built from a list · Membership in the inorder traversal of a red-black tree · Membership in a splice · The inorder traversal of an ordered red-black tree is strictly increasing · Joining separated ordered trees preserves order · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremRed-black deletion yields a valid red-black tree#✓fully proved

For every linearly ordered key type, every key \(x\) and every red-black tree \(t\), the tree obtained by deleting \(x\) from \(t\) is a valid red-black tree: it is ordered, no red node has a red child, every root-to-leaf path contains the same number of black nodes, and its root is black (the empty tree counts as black). No hypothesis on \(t\) is needed.

The result is valid because deletion rebuilds the tree by repeated insertion, which always produces a valid red-black tree.

public theorem valid_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : Valid (delete x tree)
Uses 7
Statement usesRed-black tree data type · Valid red-black tree · Red-black tree deletion by rebuilding
Proof usesUnbalanced red-black tree deletion · Inorder traversal of a red-black tree · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremRed-black deletion yields an ordered tree#✓fully proved

For every linearly ordered key type, every key \(x\) and every red-black tree \(t\), the tree obtained by deleting \(x\) from \(t\) is ordered: at every node, all keys in the left subtree are strictly smaller than the node's key and all keys in the right subtree are strictly larger. No hypothesis on \(t\) is needed.

public theorem ordered_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : Ordered (delete x tree)
Uses 12
Statement usesOrdered red-black tree · Red-black tree data type · Red-black tree deletion by rebuilding
Proof usesBlack-height balanced red-black tree · Red-black node colors · Red property of red-black trees · Valid red-black tree · Root color · Unbalanced red-black tree deletion · Inorder traversal of a red-black tree · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremRed-black deletion yields a tree with no red-red edge#✓fully proved

For every linearly ordered key type, every key \(x\) and every red-black tree \(t\), the tree obtained by deleting \(x\) from \(t\) satisfies the red invariant: no red node has a red child. No hypothesis on \(t\) is needed.

public theorem redOk_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : RedOk (delete x tree)
Uses 12
Statement usesRed property of red-black trees · Red-black tree data type · Red-black tree deletion by rebuilding
Proof usesBlack-height balanced red-black tree · Red-black node colors · Ordered red-black tree · Valid red-black tree · Root color · Unbalanced red-black tree deletion · Inorder traversal of a red-black tree · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremDeletion by rebuilding is black-height balanced#✓fully proved

For every linearly ordered type of keys, every key \(x\) and every red-black tree \(t\), with no hypothesis on \(t\), the tree obtained from \(t\) by deleting \(x\) by rebuilding is black-height balanced.

public theorem balanced_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : Balanced (delete x tree)
Uses 12
Statement usesBlack-height balanced red-black tree · Red-black tree data type · Red-black tree deletion by rebuilding
Proof usesRed-black node colors · Ordered red-black tree · Red property of red-black trees · Valid red-black tree · Root color · Unbalanced red-black tree deletion · Inorder traversal of a red-black tree · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

TheoremDeletion by rebuilding gives a black root#✓fully proved

For every linearly ordered type of keys, every key \(x\) and every red-black tree \(t\), with no hypothesis on \(t\), the root of the tree obtained from \(t\) by deleting \(x\) by rebuilding is black, where the empty tree counts as having a black root.

public theorem colorOf_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : colorOf (delete x tree) = .black
Uses 12
Statement usesRed-black node colors · Red-black tree data type · Root color · Red-black tree deletion by rebuilding
Proof usesBlack-height balanced red-black tree · Ordered red-black tree · Red property of red-black trees · Valid red-black tree · Unbalanced red-black tree deletion · Inorder traversal of a red-black tree · Rebuilding a red-black tree from its keys · Red-black trees built from a list are valid

InductiveExtended root colors#✓fully proved

An extended color is one of three values: red, black or double black.

Double black marks the root of a tree after a deletion and counts as two black nodes in its black height.

public inductive BColor where
  | red
  | black
  | doubleBlack
  deriving DecidableEq
Used by 3
Used byBlack height after double-black deletion · Extended root color · Double-black deletion yields a valid tree from the structural invariants

InductiveTrees with a possibly double-black root#✓fully proved

A tree with a possibly double-black root over a type \(\alpha\) is one of the following: a genuine red-black tree over \(\alpha\); the double-black empty tree; or a double-black node consisting of a left subtree, a key in \(\alpha\) and a right subtree, where both subtrees are genuine red-black trees. Hence a double black can occur only at the root.

public inductive BBTree (α : Type u) where
  | regular (tree : Tree α)
  | emptyBB
  | nodeBB (left : Tree α) (key : α) (right : Tree α)
Uses 1 · Used by 16
Statement usesRed-black tree data type
Used byRebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Black-height balance of a possibly double-black tree · Black height of a possibly double-black tree · Black height after double-black deletion · Absorbing a double-black root · Extended root color · Double-black deletion leaves a black root · Double-black deletion · Left repair after double-black deletion · Right repair after double-black deletion · Adding a black to the root · Inorder traversal of a possibly double-black tree · Double-black deletion erases the key from the inorder traversal · Red invariant for trees with a possibly double-black root · Double-black deletion yields a valid tree from the structural invariants

DefinitionInorder traversal of a possibly double-black tree#✓fully proved

The inorder traversal of a red-black tree whose root may be double black ignores the double-black mark: a genuine tree gives its inorder traversal, the double-black empty tree gives the empty list, and a double-black node with left child \(l\), key \(k\) and right child \(r\) gives the inorder traversal of \(l\), followed by \(k\), followed by the inorder traversal of \(r\).

public def inorderBB {α : Type u} : BBTree α → List α
  | .regular tree => inorder tree
  | .emptyBB => []
  | .nodeBB left key right => inorder left ++ key :: inorder right
Uses 3 · Used by 3
Statement usesTrees with a possibly double-black root · Red-black tree data type · Inorder traversal of a red-black tree
Used byBlack height after double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionBlack height of a possibly double-black tree#✓fully proved

The black height of a genuine red-black tree is its usual black height. The double-black empty tree has black height \(2\), and a double-black node with left subtree \(L\) has black height \(h(L) + 2\), where \(h(L)\) is the usual black height of \(L\). Thus a double-black root counts as two black nodes, where the usual black height counts the empty tree as one.

For an ordered, balanced red-black tree satisfying the red invariant, deleting any key by the double-black descent, before the root is blackened, yields a tree whose black height in this sense equals the black height of the original tree.

public def bhBB {α : Type u} : BBTree α → Nat
  | .regular tree => blackHeight tree
  | .emptyBB => 2
  | .nodeBB left _ _ => blackHeight left + 2
Uses 3 · Used by 2
Statement usesTrees with a possibly double-black root · Red-black tree data type · Black height
Used byBlack height after double-black deletion · Double-black deletion yields a valid tree from the structural invariants

DefinitionBlack-height balance of a possibly double-black tree#✓fully proved

A tree whose root may be double black is balanced when it is a genuine red-black tree that is balanced, when it is the double-black empty tree, or when it is a double-black node whose left and right subtrees are both balanced and have the same black height.

public def BalancedBB {α : Type u} : BBTree α → Prop
  | .regular tree => Balanced tree
  | .emptyBB => True
  | .nodeBB left _ right =>
      Balanced left ∧ Balanced right ∧ blackHeight left = blackHeight right
Uses 4 · Used by 2
Statement usesBlack-height balanced red-black tree · Trees with a possibly double-black root · Red-black tree data type · Black height
Used byBlack height after double-black deletion · Double-black deletion yields a valid tree from the structural invariants

DefinitionRed invariant for trees with a possibly double-black root#✓fully proved

A tree whose root may be double black satisfies the red invariant in the following cases: a genuine red-black tree satisfies it when it satisfies the usual red invariant (no red node has a red child); the double-black empty tree always satisfies it; and a double-black node with left subtree \(l\) and right subtree \(r\) satisfies it when both \(l\) and \(r\) satisfy the usual red invariant.

public def RedOkBB {α : Type u} : BBTree α → Prop
  | .regular tree => RedOk tree
  | .emptyBB => True
  | .nodeBB left _ right => RedOk left ∧ RedOk right
Uses 3 · Used by 2
Statement usesTrees with a possibly double-black root · Red property of red-black trees · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion yields a valid tree from the structural invariants

DefinitionExtended root color#✓fully proved

The extended color of a tree whose root may be double black is the color of its root, red or black, when it is a genuine red-black tree, where the empty tree counts as black; it is double black for the double-black empty tree and for every double-black node.

public def colorBB {α : Type u} : BBTree α → BColor
  | .regular tree =>
      match colorOf tree with
      | .red => .red
      | .black => .black
  | .emptyBB => .doubleBlack
  | .nodeBB _ _ _ => .doubleBlack
Uses 5 · Used by 2
Statement usesRed-black node colors · Trees with a possibly double-black root · Extended root colors · Red-black tree data type · Root color
Used byBlack height after double-black deletion · Double-black deletion yields a valid tree from the structural invariants

DefinitionAdding a black to the root#✓fully proved

Add one black to the root of a red-black tree, producing a tree whose root may be double black: the empty tree becomes the double-black empty tree, a red root becomes black, and a black root becomes double black.

public def incrBlack {α : Type u} : Tree α → BBTree α
  | .empty => .emptyBB
  | .node .red left key right => .regular (.node .black left key right)
  | .node .black left key right => .nodeBB left key right
Uses 3 · Used by 4
Statement usesRed-black node colors · Trees with a possibly double-black root · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionRecoloring the root black#✓fully proved

For a red-black tree \(t\), this is the tree obtained from \(t\) by coloring its root black: the empty tree stays empty, and a node with left subtree \(l\), key \(k\) and right subtree \(r\), of either color, becomes the black node with left subtree \(l\), key \(k\) and right subtree \(r\).

public def rootBlack {α : Type u} : Tree α → Tree α
  | .empty => .empty
  | .node _ left key right => .node .black left key right
Uses 2 · Used by 4
Statement usesRed-black node colors · Red-black tree data type
Used byBlack height after double-black deletion · Absorbing a double-black root · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionAbsorbing a double-black root#✓fully proved

Blackening sends a tree whose root may be double black to a genuine red-black tree by changing only its root: a genuine tree has its root recolored black (the empty tree stays empty), the double-black empty tree becomes the empty tree, and a double-black node becomes the black node with the same subtrees and key.

public def blacken {α : Type u} : BBTree α → Tree α
  | .regular tree => rootBlack tree
  | .emptyBB => .empty
  | .nodeBB left key right => .node .black left key right
Uses 4 · Used by 5
Statement usesRed-black node colors · Trees with a possibly double-black root · Recoloring the root black · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion leaves a black root · Red-black tree deletion by the double-black method · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionLeftmost key of a red-black tree#✓fully proved

For a red-black tree \(t\) over a type \(\alpha\), the leftmost key of \(t\) is either a key in \(\alpha\) or undefined. It is undefined when \(t\) is empty. When \(t\) is a node, of either color, with left subtree \(l\) and key \(k\), it is the leftmost key of \(l\) if that is defined, and \(k\) otherwise. Hence the leftmost key is defined exactly when \(t\) is nonempty.

Under the search-tree invariant the leftmost key is the minimum key of the tree.

def minKey {α : Type u} : Tree α → Option α
  | .empty => none
  | .node _ left key _ =>
      match minKey left with
      | some s => some s
      | none => some key
Uses 2 · Used by 4
Statement usesRed-black node colors · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionLeft repair after double-black deletion#✓fully proved

Write \(\mathrm{R}\) and \(\mathrm{B}\) for red and black, and \(N(c, T, y, T')\) for the node of color \(c\) with left subtree \(T\), key \(y\) and right subtree \(T'\). Given a color \(c\), a tree \(D\), a key \(k\) and a tree \(S\), the left repair returns a tree whose root may be double black, by the first case that applies. If \(S = N(\mathrm{B}, T_1, y, N(\mathrm{R}, T_2, z, T_3))\) or, failing that, \(S = N(\mathrm{B}, N(\mathrm{R}, T_1, y, T_2), z, T_3)\), it returns \(N(c, N(\mathrm{B}, D, k, T_1), y, N(\mathrm{B}, T_2, z, T_3))\). Otherwise, if \(S = N(\mathrm{B}, T_1, y, T_2)\), it returns \(N(\mathrm{B}, D, k, N(\mathrm{R}, T_1, y, T_2))\) when \(c\) is red, and the double-black node with left child \(D\), key \(k\) and right child \(N(\mathrm{R}, T_1, y, T_2)\) when \(c\) is black. In the next three cases \(c\) is not used. If \(S = N(\mathrm{R}, N(\mathrm{B}, T_1, y, N(\mathrm{R}, T_2, z, T_3)), w, T_4)\) or, failing that, \(S = N(\mathrm{R}, N(\mathrm{B}, N(\mathrm{R}, T_1, y, T_2), z, T_3), w, T_4)\), it returns \(N(\mathrm{B}, N(\mathrm{R}, N(\mathrm{B}, D, k, T_1), y, N(\mathrm{B}, T_2, z, T_3)), w, T_4)\). Otherwise, if \(S = N(\mathrm{R}, N(\mathrm{B}, T_1, y, T_2), w, T_3)\), it returns \(N(\mathrm{B}, N(\mathrm{B}, D, k, N(\mathrm{R}, T_1, y, T_2)), w, T_3)\). In every remaining case it returns \(N(c, D, k, S)\).

The repair is meant for a deficient left subtree \(D\) whose double black has been absorbed, so that \(D\) has one black node fewer than its sibling \(S\) on every root-to-leaf path.

Cslib.Algorithms.Lean.RedBlackTree.DeleteBalanced.fixLeft · 23 lines 
def fixLeft {α : Type u} : Color → Tree α → α → Tree α → BBTree α
  | color, left, key, .node .black rl rk (.node .red rrl rrk rrr) =>
      .regular (.node color (.node .black left key rl) rk
        (.node .black rrl rrk rrr))
  | color, left, key, .node .black (.node .red rll rlk rlr) rk rr =>
      .regular (.node color (.node .black left key rll) rlk
        (.node .black rlr rk rr))
  | .red, left, key, .node .black rl rk rr =>
      .regular (.node .black left key (.node .red rl rk rr))
  | .black, left, key, .node .black rl rk rr =>
      .nodeBB left key (.node .red rl rk rr)
  | _, left, key, .node .red (.node .black rll rlk (.node .red rrl rrk rrr)) rk rr =>
      .regular (.node .black
        (.node .red (.node .black left key rll) rlk (.node .black rrl rrk rrr))
        rk rr)
  | _, left, key, .node .red (.node .black (.node .red a y b) rlk rlr) rk rr =>
      .regular (.node .black
        (.node .red (.node .black left key a) y (.node .black b rlk rlr))
        rk rr)
  | _, left, key, .node .red (.node .black rll rlk rlr) rk rr =>
      .regular (.node .black
        (.node .black left key (.node .red rll rlk rlr)) rk rr)
  | color, left, key, right => .regular (.node color left key right)
Uses 3 · Used by 4
Statement usesRed-black node colors · Trees with a possibly double-black root · Red-black tree data type
Used byRebalancing after deletion from the left subtree · Black height after double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionRight repair after double-black deletion#✓fully proved

Write \(\mathrm{R}\) and \(\mathrm{B}\) for red and black, and \(N(c, T, y, T')\) for the node of color \(c\) with left subtree \(T\), key \(y\) and right subtree \(T'\). Given a color \(c\), a tree \(S\), a key \(k\) and a tree \(D\), the right repair returns a tree whose root may be double black, by the first case that applies. If \(S = N(\mathrm{B}, N(\mathrm{R}, T_1, y, T_2), z, T_3)\) or, failing that, \(S = N(\mathrm{B}, T_1, y, N(\mathrm{R}, T_2, z, T_3))\), it returns \(N(c, N(\mathrm{B}, T_1, y, T_2), z, N(\mathrm{B}, T_3, k, D))\). Otherwise, if \(S = N(\mathrm{B}, T_1, y, T_2)\), it returns \(N(\mathrm{B}, N(\mathrm{R}, T_1, y, T_2), k, D)\) when \(c\) is red, and the double-black node with left child \(N(\mathrm{R}, T_1, y, T_2)\), key \(k\) and right child \(D\) when \(c\) is black. In the next three cases \(c\) is not used. If \(S = N(\mathrm{R}, T_1, y, N(\mathrm{B}, N(\mathrm{R}, T_2, z, T_3), w, T_4))\) or, failing that, \(S = N(\mathrm{R}, T_1, y, N(\mathrm{B}, T_2, z, N(\mathrm{R}, T_3, w, T_4)))\), it returns \(N(\mathrm{B}, T_1, y, N(\mathrm{R}, N(\mathrm{B}, T_2, z, T_3), w, N(\mathrm{B}, T_4, k, D)))\). Otherwise, if \(S = N(\mathrm{R}, T_1, y, N(\mathrm{B}, T_2, z, T_3))\), it returns \(N(\mathrm{B}, T_1, y, N(\mathrm{B}, N(\mathrm{R}, T_2, z, T_3), k, D))\). In every remaining case it returns \(N(c, S, k, D)\).

The repair is the mirror image of the left repair, meant for a deficient right subtree \(D\) whose double black has been absorbed, so that \(D\) has one black node fewer than its sibling \(S\) on every root-to-leaf path.

Cslib.Algorithms.Lean.RedBlackTree.DeleteBalanced.fixRight · 21 lines 
def fixRight {α : Type u} : Color → Tree α → α → Tree α → BBTree α
  | color, .node .black (.node .red lrl lrk lrr) lk lr, key, right =>
      .regular (.node color (.node .black lrl lrk lrr) lk
        (.node .black lr key right))
  | color, .node .black ll lk (.node .red lrl lrk lrr), key, right =>
      .regular (.node color (.node .black ll lk lrl) lrk
        (.node .black lrr key right))
  | .red, .node .black ll lk lr, key, right =>
      .regular (.node .black (.node .red ll lk lr) key right)
  | .black, .node .black ll lk lr, key, right =>
      .nodeBB (.node .red ll lk lr) key right
  | _, .node .red ll lk (.node .black (.node .red a y b) mk mr), key, right =>
      .regular (.node .black ll lk
        (.node .red (.node .black a y b) mk (.node .black mr key right)))
  | _, .node .red ll lk (.node .black ml mk (.node .red a y b)), key, right =>
      .regular (.node .black ll lk
        (.node .red (.node .black ml mk a) y (.node .black b key right)))
  | _, .node .red ll lk (.node .black ml mk mr), key, right =>
      .regular (.node .black ll lk
        (.node .black (.node .red ml mk mr) key right))
  | color, left, key, right => .regular (.node color left key right)
Uses 3 · Used by 4
Statement usesRed-black node colors · Trees with a possibly double-black root · Red-black tree data type
Used byRebalancing after deletion from the right subtree · Black height after double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionRebalancing after deletion from the left subtree#✓fully proved

Let \(c\) be a color, \(L\) a tree whose root may be double black, \(k\) a key and \(R\) a red-black tree. If \(L\) is a genuine red-black tree, the result is the genuine node with color \(c\), left subtree \(L\), key \(k\) and right subtree \(R\). Otherwise the double black of \(L\) is absorbed first: a double-black empty tree becomes the empty tree, and a double-black node becomes the black node with the same children and key. The result is then the left-deficit repair (Fix Left) applied to the color \(c\), the absorbed tree, the key \(k\) and the sibling \(R\); it may again have a double-black root.

def balLeft {α : Type u} (color : Color) (left : BBTree α) (key : α)
    (right : Tree α) : BBTree α :=
  match left with
  | .regular tree => .regular (.node color tree key right)
  | .emptyBB => fixLeft color .empty key right
  | .nodeBB l k r => fixLeft color (.node .black l k r) key right
Uses 4 · Used by 4
Statement usesRed-black node colors · Trees with a possibly double-black root · Left repair after double-black deletion · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionRebalancing after deletion from the right subtree#✓fully proved

Let \(c\) be a color, \(L\) a red-black tree, \(k\) a key and \(R\) a tree whose root may be double black. If \(R\) is a genuine red-black tree, the result is the genuine node with color \(c\), left subtree \(L\), key \(k\) and right subtree \(R\). Otherwise the double black of \(R\) is absorbed first: a double-black empty tree becomes the empty tree, and a double-black node becomes the black node with the same children and key. The result is then the right-deficit repair (Fix Right) applied to the color \(c\), the sibling \(L\), the key \(k\) and the absorbed tree; it may again have a double-black root.

def balRight {α : Type u} (color : Color) (left : Tree α) (key : α)
    (right : BBTree α) : BBTree α :=
  match right with
  | .regular tree => .regular (.node color left key tree)
  | .emptyBB => fixRight color left key .empty
  | .nodeBB l k r => fixRight color left key (.node .black l k r)
Uses 4 · Used by 4
Statement usesRed-black node colors · Trees with a possibly double-black root · Right repair after double-black deletion · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionDouble-black deletion#✓fully proved

For a key \(x\) of a linearly ordered type, deleting \(x\) from a red-black tree returns a tree whose root may be double black, by recursion on the tree. The empty tree gives the empty tree. At a node of color \(c\) with left subtree \(l\), key \(k\) and right subtree \(r\): if \(x < k\), the result is the left reassembly of color \(c\), the deletion of \(x\) from \(l\), key \(k\) and \(r\); if \(k < x\), it is the right reassembly of color \(c\), \(l\), key \(k\) and the deletion of \(x\) from \(r\). A reassembly rebuilds the node when the recursive result is a genuine tree, and otherwise repairs the double-black child against its sibling. If \(x = k\) and \(l\) is empty, the result is \(r\) when \(c\) is red and \(r\) with one black added at its root when \(c\) is black; otherwise, if \(r\) is empty, the same with \(l\) in place of \(r\). If \(x = k\) and both subtrees are nonempty, let \(s\) be the leftmost key of \(r\); the result is the right reassembly of color \(c\), \(l\), key \(s\) and the deletion of \(s\) from \(r\). Thus a node with two children is deleted by promoting its successor, the minimum key of its right subtree.

Cslib.Algorithms.Lean.RedBlackTree.DeleteBalanced.del · 18 lines 
def del {α : Type u} [LinearOrder α] (x : α) : Tree α → BBTree α
  | .empty => .regular .empty
  | .node color left key right =>
      if x < key then balLeft color (del x left) key right
      else if key < x then balRight color left key (del x right)
      else match left, right with
        | .empty, _ =>
            match color with
            | .red => .regular right
            | .black => incrBlack right
        | _, .empty =>
            match color with
            | .red => .regular left
            | .black => incrBlack left
        | _, _ =>
            match minKey right with
            | some s => balRight color left s (del s right)
            | none => .regular left
Uses 7 · Used by 5
Statement usesRed-black node colors · Trees with a possibly double-black root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Adding a black to the root · Leftmost key of a red-black tree · Red-black tree data type
Used byBlack height after double-black deletion · Double-black deletion leaves a black root · Red-black tree deletion by the double-black method · Double-black deletion erases the key from the inorder traversal · Double-black deletion yields a valid tree from the structural invariants

DefinitionRed-black tree deletion by the double-black method#✓fully proved

For a key \(x\) of a linearly ordered type and a red-black tree \(t\), deleting \(x\) from \(t\) runs the double-black deletion of \(x\) from \(t\), which returns a tree whose root may be double black, and then absorbs a remaining double black at the root and recolors the root black.

When \(t\) is ordered, has no red node with a red child and has the same number of black nodes on every root-to-leaf path, the result is a valid red-black tree; when \(t\) is only ordered, the inorder traversal of the result is that of \(t\) with \(x\) erased.

public def deleteBal {α : Type u} [LinearOrder α] (x : α) (tree : Tree α) :
    Tree α :=
  blacken (del x tree)
Uses 3 · Used by 10
Statement usesAbsorbing a double-black root · Double-black deletion · Red-black tree data type
Used byDouble-black deletion keeps a valid tree balanced · Black height after double-black deletion · Double-black deletion leaves a black root · Double-black deletion erases the key from the inorder traversal · Keys after double-black deletion · The deleted key is absent after double-black deletion · Double-black deletion preserves the search-tree order · Double-black deletion from a valid tree keeps the red invariant · Double-black deletion preserves validity · Double-black deletion yields a valid tree from the structural invariants

TheoremDouble-black deletion erases the key from the inorder traversal#✓fully proved

For a key \(x\) of a linearly ordered type and an ordered red-black tree \(t\), the inorder traversal of the tree obtained by deleting \(x\) from \(t\) by the double-black method is the inorder traversal of \(t\) with the first occurrence of \(x\) removed (unchanged if \(x\) does not occur).

public theorem inorder_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Ordered tree) :
    inorder (deleteBal x tree) = (inorder tree).erase x
Uses 25 · Used by 2
Statement usesRed-black tree deletion by the double-black method · Ordered red-black tree · Red-black tree data type · Inorder traversal of a red-black tree
Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Red-black node colors · Trees with a possibly double-black root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Absorbing a double-black root · Double-black deletion · Left repair after double-black deletion · Right repair after double-black deletion · Adding a black to the root · Inorder traversal of a possibly double-black tree · Leftmost key of a red-black tree · Recoloring the root black · Membership in a red-black tree · All keys versus members of a red-black tree · Color erasure · Membership in the inorder traversal of a red-black tree
Used byKeys after double-black deletion · Double-black deletion preserves the search-tree order

TheoremKeys after double-black deletion#✓fully proved

For keys \(x\) and \(y\) of a linearly ordered type and an ordered red-black tree \(t\), \(y\) is a key of the tree obtained by deleting \(x\) from \(t\) by the double-black method if and only if \(y\) is a key of \(t\) and \(y \ne x\).

public theorem mem_deleteBal {α : Type u} [LinearOrder α] {x y : α}
    {tree : Tree α} (hTree : Ordered tree) :
    y ∈ deleteBal x tree ↔ y ∈ tree ∧ y ≠ x
Uses 8 · Used by 1
Statement usesRed-black tree deletion by the double-black method · Membership in a red-black tree · Ordered red-black tree · Red-black tree data type
Proof usesDouble-black deletion erases the key from the inorder traversal · Inorder traversal of a red-black tree · Ordered red-black trees have duplicate-free inorder traversals · Membership in the inorder traversal of a red-black tree
Used byThe deleted key is absent after double-black deletion

TheoremThe deleted key is absent after double-black deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(t\) a red-black tree with keys in \(\alpha\) that is ordered, that is, at every node all keys of the left subtree are strictly smaller and all keys of the right subtree are strictly larger than the node's key. Then for every \(x \in \alpha\), the key \(x\) does not occur in the tree obtained by deleting \(x\) from \(t\) by the double-black method.

public theorem not_mem_deleteBal_self {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Ordered tree) : x ∉ deleteBal x tree
Uses 5
Statement usesRed-black tree deletion by the double-black method · Membership in a red-black tree · Ordered red-black tree · Red-black tree data type
Proof usesKeys after double-black deletion

TheoremDouble-black deletion preserves the search-tree order#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(t\) a red-black tree with keys in \(\alpha\) that is ordered, that is, at every node all keys of the left subtree are strictly smaller and all keys of the right subtree are strictly larger than the node's key. Then for every \(x \in \alpha\), the tree obtained by deleting \(x\) from \(t\) by the double-black method is again ordered.

public theorem ordered_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Ordered tree) : Ordered (deleteBal x tree)
Uses 16 · Used by 1
Statement usesRed-black tree deletion by the double-black method · Ordered red-black tree · Red-black tree data type
Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Red-black node colors · Double-black deletion erases the key from the inorder traversal · Membership in a red-black tree · All keys versus members of a red-black tree · Color erasure · Inorder traversal of a red-black tree · Membership in the inorder traversal of a red-black tree · The inorder traversal of an ordered red-black tree is strictly increasing
Used byDouble-black deletion yields a valid tree from the structural invariants

TheoremDouble-black deletion yields a valid tree from the structural invariants#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(t\) a red-black tree with keys in \(\alpha\) that is ordered, satisfies the red invariant (no red node has a red child), and is black-height balanced (all root-to-leaf paths contain the same number of black nodes). Then for every \(x \in \alpha\), the tree obtained by deleting \(x\) from \(t\) by the double-black method is a valid red-black tree.

The root of \(t\) need not be black, since the deletion recolors the root of its result black.

public theorem valid_deleteBal_of_invariants {α : Type u} [LinearOrder α]
    {x : α} {tree : Tree α} (hOrdered : Ordered tree) (hRedOk : RedOk tree)
    (hBalanced : Balanced tree) : Valid (deleteBal x tree)
Uses 36 · Used by 1
Statement usesBlack-height balanced red-black tree · Red-black tree deletion by the double-black method · Ordered red-black tree · Red property of red-black trees · Red-black tree data type · Valid red-black tree
Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Red-black node colors · Trees with a possibly double-black root · Extended root colors · Black-height balance of a possibly double-black tree · Red invariant for trees with a possibly double-black root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Black height of a possibly double-black tree · Absorbing a double-black root · Extended root color · Double-black deletion · Left repair after double-black deletion · Right repair after double-black deletion · Adding a black to the root · Inorder traversal of a possibly double-black tree · Leftmost key of a red-black tree · Double-black deletion preserves the search-tree order · Recoloring the root black · Membership in a red-black tree · All keys versus members of a red-black tree · Black height · Root color · Color erasure · Inorder traversal of a red-black tree · Membership in the inorder traversal of a red-black tree
Used byDouble-black deletion preserves validity

TheoremDouble-black deletion preserves validity#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(t\) a valid red-black tree with keys in \(\alpha\): it is ordered, satisfies the red invariant, is black-height balanced, and has a black root. Then for every \(x \in \alpha\), the tree obtained by deleting \(x\) from \(t\) by the double-black method is again a valid red-black tree.

The proof uses only that \(t\) is ordered, satisfies the red invariant and is balanced.

public theorem valid_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Valid tree) : Valid (deleteBal x tree)
Uses 9 · Used by 2
Statement usesRed-black tree deletion by the double-black method · Red-black tree data type · Valid red-black tree
Proof usesBlack-height balanced red-black tree · Red-black node colors · Double-black deletion yields a valid tree from the structural invariants · Ordered red-black tree · Red property of red-black trees · Root color
Used byDouble-black deletion keeps a valid tree balanced · Double-black deletion from a valid tree keeps the red invariant

TheoremDouble-black deletion from a valid tree keeps the red invariant#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(t\) a valid red-black tree with keys in \(\alpha\): it is ordered, satisfies the red invariant, is black-height balanced, and has a black root. Then for every \(x \in \alpha\), the tree obtained by deleting \(x\) from \(t\) by the double-black method satisfies the red invariant: no red node has a red child.

public theorem redOk_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Valid tree) : RedOk (deleteBal x tree)
Uses 9
Statement usesRed-black tree deletion by the double-black method · Red property of red-black trees · Red-black tree data type · Valid red-black tree
Proof usesBlack-height balanced red-black tree · Red-black node colors · Double-black deletion preserves validity · Ordered red-black tree · Root color

TheoremDouble-black deletion keeps a valid tree balanced#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), and \(T\) a valid red-black tree over \(\alpha\). Then the tree obtained from \(T\) by double-black deletion of \(x\) is balanced.

public theorem balanced_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Valid tree) : Balanced (deleteBal x tree)
Uses 9
Statement usesBlack-height balanced red-black tree · Red-black tree deletion by the double-black method · Red-black tree data type · Valid red-black tree
Proof usesRed-black node colors · Double-black deletion preserves validity · Ordered red-black tree · Red property of red-black trees · Root color

TheoremDouble-black deletion leaves a black root#✓fully proved

For every key \(x\) of a linearly ordered type and every red-black tree \(t\), valid or not, the root of the tree obtained by deleting \(x\) from \(t\) by the double-black method is black, where the empty tree counts as black.

public theorem colorOf_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} : colorOf (deleteBal x tree) = .black
Uses 7
Statement usesRed-black node colors · Red-black tree deletion by the double-black method · Red-black tree data type · Root color
Proof usesTrees with a possibly double-black root · Absorbing a double-black root · Double-black deletion

TheoremBlack height after double-black deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), \(T\) a valid red-black tree over \(\alpha\), and \(T'\) the tree obtained from \(T\) by double-black deletion of \(x\). Then the black height of \(T'\) either equals the black height of \(T\) or is one less than it.

The black height drops by one when a double black left by the deletion is absorbed at the root.

public theorem blackHeight_deleteBal {α : Type u} [LinearOrder α] {x : α}
    {tree : Tree α} (hTree : Valid tree) :
    blackHeight (deleteBal x tree) = blackHeight tree ∨
      blackHeight (deleteBal x tree) + 1 = blackHeight tree
Uses 35
Statement usesRed-black tree deletion by the double-black method · Red-black tree data type · Valid red-black tree · Black height
Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Predicate holding at every key of a red-black tree · Black-height balanced red-black tree · Red-black node colors · Trees with a possibly double-black root · Extended root colors · Black-height balance of a possibly double-black tree · Red invariant for trees with a possibly double-black root · Rebalancing after deletion from the left subtree · Rebalancing after deletion from the right subtree · Black height of a possibly double-black tree · Absorbing a double-black root · Extended root color · Double-black deletion · Left repair after double-black deletion · Right repair after double-black deletion · Adding a black to the root · Inorder traversal of a possibly double-black tree · Leftmost key of a red-black tree · Recoloring the root black · Membership in a red-black tree · Ordered red-black tree · Red property of red-black trees · All keys versus members of a red-black tree · Root color · Color erasure · Inorder traversal of a red-black tree · Membership in the inorder traversal of a red-black tree
82 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.