Weight-balanced tree

TheoremNumber of keys of the empty tree#✓fully proved

The empty binary tree has \(0\) nodes.

@[simp] public theorem numNodes_empty :
    (BinaryTree.nil : BinaryTree α).numNodes = 0

TheoremNumber of keys of a node#✓fully proved

Write \(|t|\) for the number of nodes of a binary tree \(t\). For binary trees \(l\) and \(r\) and a key \(k\), the node with key \(k\), left subtree \(l\) and right subtree \(r\) has \(|l| + |r| + 1\) nodes.

@[simp] public theorem numNodes_node {left right : BinaryTree α} {key : α} :
    (BinaryTree.node key left right).numNodes =
      left.numNodes + right.numNodes + 1

DefinitionWeight of a binary tree#✓fully proved

The Nievergelt–Reingold weight \(w(t)\) of a binary tree \(t\) is its number of keys plus one. Equivalently, it counts the external leaves: the empty tree has weight \(1\), and the weight of a node is the sum of the weights of its two children.

public def weight (t : BinaryTree α) : Nat :=
  t.numNodes + 1
Used by 2
Used byWeight form of the balance condition at a node · Exponential weight lower bound for weight-balanced trees

DefinitionWeight-balanced trees#✓fully proved

Write \(|t|\) for the number of keys of a binary tree \(t\) and \(w(t) = |t| + 1\) for its weight. A binary tree is weight-balanced, or satisfies the invariant \(\mathrm{BB}[1/4]\), when it is empty, or when it is a node with left subtree \(L\) and right subtree \(R\) such that \(L\) and \(R\) are weight-balanced, \(4\,w(L) \le 3(w(L) + w(R))\) and \(4\,w(R) \le 3(w(L) + w(R))\). Since the weight of a node is \(w(L) + w(R)\), this says that each child has weight at most three quarters of the weight of the node.

public def Balanced : BinaryTree α → Prop
  | .nil => True
  | .node _ left right =>
      Balanced left ∧ Balanced right ∧
        4 * (left.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2) ∧
          4 * (right.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2)
Used by 7
Used byWeight-balanced rebalancing restores balance · Weight-balanced trees built by insertion are balanced · Weight-balanced insertion preserves balance · Building a weight-balanced node · Weight form of the balance condition at a node · Height of a weight-balanced tree is logarithmic · Exponential weight lower bound for weight-balanced trees

DefinitionWeight-balanced rebalancing#✓fully proved

For binary trees \(L\), \(R\) and a key \(k\), write \(|t|\) for the number of keys of a tree \(t\), \(w(t) = |t| + 1\) for its weight, \(w = w(L) + w(R)\), and \(\langle X, x, Y \rangle\) for the node with key \(x\), left subtree \(X\) and right subtree \(Y\). The rebalanced node \(\mathrm{balance}(L, k, R)\) is defined as follows. If \(3w < 4\,w(L)\), then \(L = \langle A, a, B \rangle\) is a node; if \(|B| \le 2|A|\), the result is the single rotation \(\langle A, a, \langle B, k, R \rangle \rangle\), and otherwise \(B = \langle B_1, b, B_2 \rangle\) is a node and the result is the double rotation \(\langle \langle A, a, B_1 \rangle, b, \langle B_2, k, R \rangle \rangle\). Otherwise, if \(3w < 4\,w(R)\), then \(R = \langle C, c, D \rangle\) is a node; if \(|C| \le 2|D|\), the result is \(\langle \langle L, k, C \rangle, c, D \rangle\), and otherwise \(C = \langle C_1, d, C_2 \rangle\) is a node and the result is \(\langle \langle L, k, C_1 \rangle, d, \langle C_2, c, D \rangle \rangle\). In all remaining cases the result is \(\langle L, k, R \rangle\).

Cslib.Algorithms.Lean.WeightBalancedTree.balance · 26 lines 
public def balance (left : BinaryTree α) (key : α) (right : BinaryTree α) : BinaryTree α :=
  if 3 * (left.numNodes + right.numNodes + 2) < 4 * (left.numNodes + 1) then
    match left with
    | .node leftKey leftLeft leftRight =>
        if leftRight.numNodes ≤ 2 * leftLeft.numNodes then
          .node leftKey leftLeft (.node key leftRight right)
        else
          match leftRight with
          | .node leftRightKey leftRightLeft leftRightRight =>
              .node leftRightKey (.node leftKey leftLeft leftRightLeft)
                (.node key leftRightRight right)
          | .nil => .node key left right
    | .nil => .node key left right
  else if 3 * (left.numNodes + right.numNodes + 2) < 4 * (right.numNodes + 1) then
    match right with
    | .node rightKey rightLeft rightRight =>
        if rightLeft.numNodes ≤ 2 * rightRight.numNodes then
          .node rightKey (.node key left rightLeft) rightRight
        else
          match rightLeft with
          | .node rightLeftKey rightLeftLeft rightLeftRight =>
              .node rightLeftKey (.node key left rightLeftLeft)
                (.node rightKey rightLeftRight rightRight)
          | .nil => .node key left right
    | .nil => .node key left right
  else .node key left right
Used by 10
Used byWeight-balanced rebalancing restores balance · Weight-balanced insertion preserves balance · Weight-balanced insertion · Weight-balanced insertion does not decrease the number of keys · Membership after weight-balanced rebalancing · Membership after weight-balanced insertion · Weight-balanced rebalancing preserves the number of keys · Weight-balanced insertion adds at most one key · Weight-balanced rebalancing preserves ordering · Weight-balanced insertion preserves the search-tree order

DefinitionWeight-balanced insertion#✓fully proved

For a key \(x\) of a linearly ordered type, the insertion \(\mathrm{insert}(x, t)\) of \(x\) into a binary tree \(t\) is defined by recursion on \(t\). Into the empty tree it gives the single node with key \(x\). Into the node \(N\) with key \(k\), left subtree \(L\) and right subtree \(R\) it gives \(\mathrm{balance}(\mathrm{insert}(x, L), k, R)\) if \(x < k\), \(\mathrm{balance}(L, k, \mathrm{insert}(x, R))\) if \(k < x\), and \(N\) itself if \(x = k\), where \(\mathrm{balance}\) is weight-balanced rebalancing.

public def insert [LinearOrder α] (x : α) : BinaryTree α → BinaryTree α
  | .nil => .node x .nil .nil
  | tree@(.node key left right) =>
      if x < key then balance (insert x left) key right
      else if key < x then balance left key (insert x right)
      else tree
Uses 1 · Used by 7
Statement usesWeight-balanced rebalancing
Used byWeight-balanced insertion preserves balance · Weight-balanced tree from a list · Weight-balanced insertion does not decrease the number of keys · Membership in a weight-balanced tree built from a list · Membership after weight-balanced insertion · Weight-balanced insertion adds at most one key · Weight-balanced insertion preserves the search-tree order

DefinitionWeight-balanced tree from a list#✓fully proved

The tree built from a list \(x_1, \dots, x_n\) of elements of a linearly ordered type is obtained from the empty tree by inserting \(x_n, x_{n-1}, \dots, x_1\) in this order with weight-balanced insertion; the empty list gives the empty tree.

public def fromList [LinearOrder α] : List α → BinaryTree α
  | [] => .nil
  | x :: xs => insert x (fromList xs)
Uses 1 · Used by 3
Statement usesWeight-balanced insertion
Used byWeight-balanced trees built by insertion are balanced · Membership in a weight-balanced tree built from a list · Weight-balanced trees built from a list are ordered

TheoremBuilding a weight-balanced node#✓fully proved

Let \(L\) and \(R\) be weight-balanced trees and \(k\) a key, and write \(|t|\) for the number of keys of a tree \(t\). If \(4(|L| + 1) \le 3(|L| + |R| + 2)\) and \(4(|R| + 1) \le 3(|L| + |R| + 2)\), then the node with key \(k\), left subtree \(L\) and right subtree \(R\) is weight-balanced.

public theorem balanced_node {key : α} {left right : BinaryTree α}
    (hLeft : Balanced left) (hRight : Balanced right)
    (hWeightLeft :
      4 * (left.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2))
    (hWeightRight :
      4 * (right.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2)) :
    Balanced (.node key left right)
Uses 1 · Used by 2
Statement usesWeight-balanced trees
Used byWeight-balanced rebalancing restores balance · Weight-balanced insertion preserves balance

TheoremWeight form of the balance condition at a node#✓fully proved

Write \(|t|\) for the number of keys of a tree \(t\) and \(w(t) = |t| + 1\) for its weight. Let \(N\) be the node with key \(k\), left subtree \(L\) and right subtree \(R\). Then \(N\) is weight-balanced if and only if \(L\) and \(R\) are weight-balanced, \(4\,w(L) \le 3\,w(N)\) and \(4\,w(R) \le 3\,w(N)\). This is the classical \(\mathrm{BB}[1/4]\) invariant: each child has weight at most three quarters of the weight of the node.

public theorem balanced_node_iff_weight {key : α} {left right : BinaryTree α} :
    Balanced (.node key left right) ↔
      Balanced left ∧ Balanced right ∧
        4 * weight left ≤ 3 * weight (.node key left right) ∧
          4 * weight right ≤ 3 * weight (.node key left right)
Uses 2
Statement usesWeight-balanced trees · Weight of a binary tree

TheoremWeight-balanced rebalancing preserves the number of keys#✓fully proved

Write \(|t|\) for the number of nodes of a binary tree \(t\). For binary trees \(l\) and \(r\) and a key \(k\), the weight-balanced rebalancing of \(l\), \(k\), \(r\) has exactly \(|l| + |r| + 1\) nodes.

public theorem numNodes_balance {key : α} {left right : BinaryTree α} :
    (balance left key right).numNodes = left.numNodes + right.numNodes + 1
Uses 1 · Used by 2
Statement usesWeight-balanced rebalancing
Used byWeight-balanced insertion does not decrease the number of keys · Weight-balanced insertion adds at most one key

TheoremWeight-balanced rebalancing restores balance#✓fully proved

Let \(L\) and \(R\) be weight-balanced trees and \(k\) a key, and write \(|t|\) for the number of keys of a tree \(t\). If \(4(|L| + 1) \le 3(|L| + |R| + 2) + 1\) and \(4(|R| + 1) \le 3(|L| + |R| + 2) + 1\), then the rebalanced node \(\mathrm{balance}(L, k, R)\) is weight-balanced.

These hypotheses are the two inequalities of the weight-balance invariant for the node with children \(L\) and \(R\), each with its right-hand side increased by \(1\); this is the precondition that one insertion step maintains.

public theorem balanced_balance {key : α} {left right : BinaryTree α}
    (hBalLeft : Balanced left) (hBalRight : Balanced right)
    (hDiffLeft : 4 * (left.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2) + 1)
    (hDiffRight : 4 * (right.numNodes + 1) ≤ 3 * (left.numNodes + right.numNodes + 2) + 1) :
    Balanced (balance left key right)
Uses 3 · Used by 1
Statement usesWeight-balanced trees · Weight-balanced rebalancing
Proof usesBuilding a weight-balanced node
Used byWeight-balanced insertion preserves balance

TheoremMembership after weight-balanced rebalancing#✓fully proved

For binary trees \(l\) and \(r\) and a key \(k\), an element \(x\) occurs in the weight-balanced rebalancing of \(l\), \(k\), \(r\) exactly when \(x\) occurs in \(l\), \(x = k\), or \(x\) occurs in \(r\). Membership is structural: \(x\) is the key of some node.

public theorem mem_balance {x key : α} {left right : BinaryTree α} :
    x ∈ balance left key right ↔ x ∈ left ∨ x = key ∨ x ∈ right
Uses 2 · Used by 1
Statement usesMembership in a binary tree · Weight-balanced rebalancing
Used byMembership after weight-balanced insertion

TheoremWeight-balanced rebalancing preserves ordering#✓fully proved

Let the keys carry a linear order, let \(l\) and \(r\) be ordered binary trees (strict binary search trees), and let \(k\) be a key such that every key of \(l\) is less than \(k\) and every key of \(r\) is greater than \(k\). Then the weight-balanced rebalancing of \(l\), \(k\), \(r\) is ordered.

public theorem ordered_balance [LinearOrder α] {key : α} {left right : BinaryTree α}
    (hOrdLeft : BinarySearchTree.Ordered left) (hOrdRight : BinarySearchTree.Ordered right)
    (hAllLeft : BinarySearchTree.All (· < key) left) (hAllRight : BinarySearchTree.All (key < ·) right) :
    BinarySearchTree.Ordered (balance left key right)
Uses 3 · Used by 1
Statement usesA predicate holding at every key of a binary tree · Ordered binary trees · Weight-balanced rebalancing
Used byWeight-balanced insertion preserves the search-tree order

TheoremWeight-balanced insertion adds at most one key#✓fully proved

Let the keys carry a linear order. For every key \(x\) and every binary tree \(t\), the tree obtained from \(t\) by weight-balanced insertion of \(x\) has at most one more node than \(t\).

public theorem numNodes_insert_le [LinearOrder α] {x : α} {tree : BinaryTree α} :
    (insert x tree).numNodes ≤ tree.numNodes + 1
Uses 3 · Used by 1
Statement usesWeight-balanced insertion
Proof usesWeight-balanced rebalancing · Weight-balanced rebalancing preserves the number of keys
Used byWeight-balanced insertion preserves balance

TheoremWeight-balanced insertion does not decrease the number of keys#✓fully proved

Let the keys carry a linear order. For every key \(x\) and every binary tree \(t\), the number of nodes of \(t\) is at most the number of nodes of the tree obtained from \(t\) by weight-balanced insertion of \(x\).

public theorem le_numNodes_insert [LinearOrder α] {x : α} {tree : BinaryTree α} :
    tree.numNodes ≤ (insert x tree).numNodes
Uses 3 · Used by 1
Statement usesWeight-balanced insertion
Proof usesWeight-balanced rebalancing · Weight-balanced rebalancing preserves the number of keys
Used byWeight-balanced insertion preserves balance

TheoremWeight-balanced insertion preserves balance#✓fully proved

For every key \(x\) of a linearly ordered type and every weight-balanced tree \(t\), the tree obtained by inserting \(x\) into \(t\) with weight-balanced insertion is weight-balanced.

public theorem balanced_insert [LinearOrder α] {x : α} {tree : BinaryTree α}
    (hBal : Balanced tree) : Balanced (insert x tree)
Uses 7 · Used by 1
Statement usesWeight-balanced trees · Weight-balanced insertion
Proof usesWeight-balanced rebalancing · Weight-balanced rebalancing restores balance · Building a weight-balanced node · Weight-balanced insertion does not decrease the number of keys · Weight-balanced insertion adds at most one key
Used byWeight-balanced trees built by insertion are balanced

TheoremMembership after weight-balanced insertion#✓fully proved

Let the keys carry a linear order. For all keys \(x\), \(y\) and every binary tree \(t\), \(y\) occurs in the tree obtained from \(t\) by weight-balanced insertion of \(x\) exactly when \(y = x\) or \(y\) occurs in \(t\).

public theorem mem_insert [LinearOrder α] {x y : α} {tree : BinaryTree α} :
    y ∈ insert x tree ↔ y = x ∨ y ∈ tree
Uses 4 · Used by 2
Statement usesMembership in a binary tree · Weight-balanced insertion
Proof usesWeight-balanced rebalancing · Membership after weight-balanced rebalancing
Used byMembership in a weight-balanced tree built from a list · Weight-balanced insertion preserves the search-tree order

TheoremWeight-balanced insertion preserves the search-tree order#✓fully proved

Let the keys be linearly ordered. If a binary tree \(t\) is ordered as a search tree (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key at the node), then the tree obtained from \(t\) by weight-balanced insertion of any key \(x\) is again ordered.

public theorem ordered_insert [LinearOrder α] {x : α} {tree : BinaryTree α}
    (hTree : BinarySearchTree.Ordered tree) : BinarySearchTree.Ordered (insert x tree)
Uses 8 · Used by 1
Statement usesOrdered binary trees · Weight-balanced insertion
Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Weight-balanced rebalancing · Membership after weight-balanced insertion · Weight-balanced rebalancing preserves ordering
Used byWeight-balanced trees built from a list are ordered

TheoremWeight-balanced trees built by insertion are balanced#✓fully proved

For every list \(x_1, \dots, x_n\) of elements of a linearly ordered type, the tree obtained from the empty tree by inserting \(x_n, x_{n-1}, \dots, x_1\) in this order with weight-balanced insertion is weight-balanced.

public theorem balanced_fromList [LinearOrder α] {xs : List α} :
    Balanced (fromList xs)
Uses 3
Statement usesWeight-balanced trees · Weight-balanced tree from a list
Proof usesWeight-balanced insertion preserves balance

TheoremWeight-balanced trees built from a list are ordered#✓fully proved

Let the keys carry a linear order. For every list \(xs\), the weight-balanced tree built from \(xs\) by repeated insertion is ordered, that is, a strict binary search tree.

public theorem ordered_fromList [LinearOrder α] {xs : List α} :
    BinarySearchTree.Ordered (fromList xs)
Uses 3
Statement usesOrdered binary trees · Weight-balanced tree from a list
Proof usesWeight-balanced insertion preserves the search-tree order

TheoremMembership in a weight-balanced tree built from a list#✓fully proved

Let the keys carry a linear order. For every key \(x\) and every list \(xs\), \(x\) occurs in the weight-balanced tree built from \(xs\) by repeated insertion exactly when \(x\) is an element of \(xs\).

public theorem mem_fromList [LinearOrder α] {x : α} {xs : List α} :
    x ∈ fromList xs ↔ x ∈ xs
Uses 4
Statement usesMembership in a binary tree · Weight-balanced tree from a list
Proof usesWeight-balanced insertion · Membership after weight-balanced insertion

TheoremExponential weight lower bound for weight-balanced trees#✓fully proved

Write \(w(t)\) for the weight of a binary tree \(t\) (its number of keys plus one), and measure height so that the empty tree has height \(0\) and a node has height one more than the taller of its children. If \(t\) is weight balanced with parameter \(1/4\) (at every node, each child has weight at most three quarters of the weight of the node) and has height \(k + 1\) for a natural number \(k\), then \(w(t) \ge (4/3)^k\); in integer form, \(4^k \le 3^k \, w(t)\).

The proof uses the weight form of the invariant: the taller child has weight at most three quarters of the weight of the node.

public theorem pow_height_le {tree : BinaryTree α} (hBal : Balanced tree) :
    ∀ k : Nat, BinaryTree.height tree = k + 1 → 4 ^ k ≤ 3 ^ k * weight tree
Uses 2 · Used by 1
Statement usesWeight-balanced trees · Weight of a binary tree
Used byHeight of a weight-balanced tree is logarithmic

TheoremHeight of a weight-balanced tree is logarithmic#✓fully proved

Write \(|t|\) for the number of keys of a binary tree \(t\) and \(h(t)\) for its height, where the empty tree has height \(0\) and a node has height one more than the larger height of its two subtrees. If \(t\) is weight-balanced, then \(h(t) \le \lfloor \log_2 ((|t| + 1)^3) \rfloor + 1\).

The proof passes from the exponential weight lower bound in base \(4/3\) to base \(2\), using \((4/3)^3 > 2\).

public theorem height_le_log2 {tree : BinaryTree α} (hBal : Balanced tree) :
    BinaryTree.height tree ≤ Nat.log2 ((tree.numNodes + 1) ^ 3) + 1
Uses 2
Statement usesWeight-balanced trees
Proof usesExponential weight lower bound for weight-balanced trees
23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.