B-tree
InductiveRaw B-trees#✓fully proved
A raw B-tree with keys in a type \(\alpha\) is either a leaf, holding a list of keys, or an internal node, holding a list of separator keys and a list of child raw B-trees. The type imposes no invariant: that an internal node with \(k\) keys has \(k + 1\) children, the bounds on key counts, the balance of the tree and the ordering of the keys are imposed separately by the structural and ordering invariants of B-trees.
public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αUsed by 69
DefinitionAccumulating flattening of a B-tree#✓fully proved
Given a raw B-tree \(T\) and a list \(s\), this returns the inorder traversal of \(T\) followed by \(s\). For a leaf it is the leaf's key list followed by \(s\). For an internal node with separator keys \(k_1, \dots, k_m\) and children \(c_0, \dots, c_n\) it is the sequence \(c_0, k_1, c_1, k_2, \dots\), in which children and keys alternate starting with a child until one of the two lists runs out, then the remaining keys or children in order, and finally \(s\); each key contributes itself, and each child contributes its own accumulating flattening with everything after it as the suffix. In particular every key of the tree occurs in the result.
The result is built from right to left, so each key is copied only once.
public def flattenAux : BTree α → List α → List α
| .leaf keys, suffix => keys ++ suffix
| .node keys children, suffix => flattenListAux keys children suffix
where
flattenListAux : List α → List (BTree α) → List α → List α
| [], [], suffix => suffix
| [], child :: children, suffix =>
flattenAux child (flattenListAux [] children suffix)
| key :: keys, [], suffix => key :: flattenListAux keys [] suffix
| key :: keys, child :: children, suffix =>
flattenAux child (key :: flattenListAux keys children suffix)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 15
DefinitionInorder flattening of a B-tree#✓fully proved
The flattening of a raw B-tree is the list of its keys defined recursively: for a leaf it is the leaf's key list, and for an internal node with keys \(k_1, k_2, \dots\) and children \(c_1, c_2, \dots\) it is the flattening of \(c_1\), then \(k_1\), then the flattening of \(c_2\), then \(k_2\), and so on, alternating while both lists last; whatever remains of the longer list is then appended in order, each surplus child contributing its flattening and each surplus key contributing itself. In particular every key of the tree occurs in the flattening.
The flattening is computed in linear time by an accumulator-passing auxiliary function.
public def flatten (tree : BTree α) : List α :=
flattenAux tree []public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flattenAux : BTree α → List α → List α
| .leaf keys, suffix => keys ++ suffix
| .node keys children, suffix => flattenListAux keys children suffix
where
flattenListAux : List α → List (BTree α) → List α → List α
| [], [], suffix => suffix
| [], child :: children, suffix =>
flattenAux child (flattenListAux [] children suffix)
| key :: keys, [], suffix => key :: flattenListAux keys [] suffix
| key :: keys, child :: children, suffix =>
flattenAux child (key :: flattenListAux keys children suffix)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:78
Uses 2 · Used by 33
TheoremThe accumulating B-tree flattening is correct#✓fully proved
For every raw B-tree \(T\) and every list \(s\), the accumulating flattening of \(T\) with suffix \(s\) equals the inorder flattening of \(T\) followed by \(s\).
public theorem flattenAux_eq (t : BTree α) (suffix : List α) :
flattenAux t suffix = flatten t ++ suffixpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flattenAux : BTree α → List α → List α
| .leaf keys, suffix => keys ++ suffix
| .node keys children, suffix => flattenListAux keys children suffix
where
flattenListAux : List α → List (BTree α) → List α → List α
| [], [], suffix => suffix
| [], child :: children, suffix =>
flattenAux child (flattenListAux [] children suffix)
| key :: keys, [], suffix => key :: flattenListAux keys [] suffix
| key :: keys, child :: children, suffix =>
flattenAux child (key :: flattenListAux keys children suffix)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:78
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 3 · Used by 8
TheoremFlattening a keyless node, one child at a time#✓fully proved
For a raw B-tree \(c\) and a list \(C\) of raw B-trees, the flattening of the node with no keys and child list \(c\) followed by \(C\) is the flattening of \(c\) followed by the flattening of the node with no keys and child list \(C\).
This covers nodes with more children than a well-formed node would have.
public theorem flatten_node_nil_cons {child : BTree α}
{children : List (BTree α)} :
flatten (.node [] (child :: children) : BTree α) =
flatten child ++ flatten (.node [] children)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 4 · Used by 6
TheoremFlattening a childless node, one key at a time#✓fully proved
For a key \(k\) and a list of keys \(K\), the flattening of the node with key list \(k\) followed by \(K\) and no children is \(k\) followed by the flattening of the node with key list \(K\) and no children.
This covers nodes with more keys than a well-formed node would have.
public theorem flatten_node_cons_nil {key : α} {keys : List α} :
flatten (.node (key :: keys) [] : BTree α) =
key :: flatten (.node keys [])public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 3 · Used by 3
TheoremFlattening of the empty node#✓fully proved
The flattening of the internal node with no keys and no children is the empty list.
public theorem flatten_node_nil_nil :
flatten (.node [] [] : BTree α) = []public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 3 · Used by 6
TheoremSplitting a node's flattening at a separator#✓fully proved
Let \(K_1\) and \(K_2\) be lists of keys, \(m\) a key, and \(C_1\) and \(C_2\) lists of raw B-trees such that \(C_1\) has exactly one more element than \(K_1\). Then the flattening of the node whose key list is \(K_1\) followed by \(m\) followed by \(K_2\) and whose child list is \(C_1\) followed by \(C_2\) equals the flattening of the node with keys \(K_1\) and children \(C_1\), followed by \(m\), followed by the flattening of the node with keys \(K_2\) and children \(C_2\).
public theorem flatten_node_append_cons {median : α} :
∀ {keys₁ : List α} {children₁ : List (BTree α)} {keys₂ : List α}
{children₂ : List (BTree α)},
children₁.length = keys₁.length + 1 →
flatten (node (keys₁ ++ median :: keys₂) (children₁ ++ children₂) :
BTree α) =
flatten (node keys₁ children₁ : BTree α) ++
median :: flatten (node keys₂ children₂ : BTree α)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 6 · Used by 5
DefinitionMembership in a B-tree#✓fully proved
A key \(x\) belongs to a tree \(T\) when \(x\) occurs in the inorder flattening of \(T\).
Structurally, a key belongs to an internal node exactly when it is one of the node's separator keys or belongs to one of its children.
public def Mem (x : α) (tree : BTree α) : Prop :=
x ∈ flatten treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 2 · Used by 11
DefinitionOrdered B-tree#✓fully proved
A B-tree over a type with a relation \(<\) is ordered when its inorder flattening is strictly increasing, that is, each key of the flattening is less than every key that comes after it. This single condition packages sortedness of the keys at each node and the separator bounds between a node's keys and the keys stored in its subtrees.
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 2 · Used by 21
TheoremThe separator keys of an ordered node are sorted#✓fully proved
If an internal node with separator list \(K\) is ordered, then \(K\) is strictly increasing: every key of \(K\) is smaller than every key that comes after it in \(K\).
public theorem Ordered.node_keys_pairwise [LT α] {keys : List α}
{children : List (BTree α)} (h : Ordered (node keys children : BTree α)) :
keys.Pairwise (· < ·)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
TheoremSeparator bounds in an ordered B-tree node#✓fully proved
Let \(K_1\) and \(K_2\) be lists of keys, \(k\) a key, and \(C_1\) and \(C_2\) lists of B-trees such that \(C_1\) has exactly one more tree than \(K_1\) has keys. If the internal node whose key list is \(K_1\) followed by \(k\) followed by \(K_2\), and whose child list is \(C_1\) followed by \(C_2\), is ordered, then every key in the flattening of the node with keys \(K_1\) and children \(C_1\) is less than \(k\), and \(k\) is less than every key in the flattening of the node with keys \(K_2\) and children \(C_2\).
Here the last tree of \(C_1\) is the subtree immediately left of \(k\) and the first tree of \(C_2\) the one immediately right of it; in particular, every key in a child of an ordered node lies strictly between the separators adjacent to it.
public theorem Ordered.separator_bounds [LT α] {keys₁ keys₂ : List α}
{children₁ children₂ : List (BTree α)} {key : α}
(hlen : children₁.length = keys₁.length + 1)
(h : Ordered (node (keys₁ ++ key :: keys₂) (children₁ ++ children₂) : BTree α)) :
(∀ x ∈ flatten (node keys₁ children₁ : BTree α), x < key) ∧
(∀ x ∈ flatten (node keys₂ children₂ : BTree α), key < x)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 4
TheoremAn ordered B-tree has no duplicate keys#✓fully proved
For a linearly ordered key type, the flattening of an ordered raw B-tree has no duplicate entries.
public theorem Ordered.flatten_nodup [LinearOrder α] {tree : BTree α} (h : Ordered tree) :
(flatten tree).Noduppublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 3 · Used by 4
InductiveStructural invariant of a B-tree#✓fully proved
For a minimum degree \(t\) and a minimum key count \(m\) for the top node, the invariant is defined inductively over the height: a leaf with \(k\) keys satisfies it at height \(0\) when \(m \le k \le 2t - 1\), and for every natural number \(h\), an internal node with \(k\) keys satisfies it at height \(h + 1\) when \(m \le k \le 2t - 1\), the node has exactly \(k + 1\) children, and every child satisfies the invariant with minimum key count \(t - 1\) at height \(h\). Here \(2t - 1\) and \(t - 1\) are truncated at \(0\).
Consequently all leaves of a valid tree sit at the same depth, every node has at most \(2t - 1\) keys, and every node other than the top one has at least \(t - 1\) keys. Non-root trees are used with \(m = t - 1\); the root of a B-tree satisfies the root invariant instead.
public inductive Valid (t : Nat) : Nat → Nat → BTree α → Prop where
| leaf {mink : Nat} {keys : List α} (hlo : mink ≤ keys.length)
(hhi : keys.length ≤ 2 * t - 1) : Valid t mink 0 (.leaf keys)
| node {mink height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : mink ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
Valid t mink (height + 1) (.node keys children)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 7
InductiveRoot invariant of a B-tree#✓fully proved
For a minimum degree \(t\) and a height \(h\), a tree satisfies the root invariant when either \(h = 0\) and the tree is a leaf with at most \(2t - 1\) keys (possibly none, for the empty tree), or \(h = h' + 1\) and the tree is an internal node with between \(1\) and \(2t - 1\) keys and exactly one more child than keys, every child satisfying the structural invariant for minimum degree \(t\), minimum top-node key count \(t - 1\) and height \(h'\). Here \(2t - 1\) and \(t - 1\) are truncated at \(0\).
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public inductive Valid (t : Nat) : Nat → Nat → BTree α → Prop where
| leaf {mink : Nat} {keys : List α} (hlo : mink ≤ keys.length)
(hhi : keys.length ≤ 2 * t - 1) : Valid t mink 0 (.leaf keys)
| node {mink height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : mink ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
Valid t mink (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:517
Uses 2 · Used by 15
TheoremRoot-valid B-trees are valid#✓fully proved
If a tree satisfies the root invariant for minimum degree \(t\) at height \(h\), then for some natural number \(m\) it satisfies the structural invariant for minimum degree \(t\), minimum top-node key count \(m\) and height \(h\).
public theorem ValidRoot.valid {t height : Nat} {tree : BTree α}
(h : ValidRoot t height tree) : ∃ mink, Valid t mink height treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
public inductive Valid (t : Nat) : Nat → Nat → BTree α → Prop where
| leaf {mink : Nat} {keys : List α} (hlo : mink ≤ keys.length)
(hhi : keys.length ≤ 2 * t - 1) : Valid t mink 0 (.leaf keys)
| node {mink height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : mink ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
Valid t mink (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:517
Uses 3 · Used by 4
DefinitionB-tree search#✓fully proved
For a linearly ordered key type, the search for a key \(x\) in a raw B-tree proceeds as follows. At a leaf, report whether \(x\) is in the leaf's key list. At an internal node with separators \(k_1, \dots, k_m\) and children \(c_0, c_1, \dots\), scan the separators in order. On reaching \(k_i\), report failure if the node has no child \(c_{i-1}\); otherwise search \(c_{i-1}\) if \(x < k_i\), report success if \(x = k_i\), and move on to the next separator if \(k_i < x\). If every separator is less than \(x\), search the child \(c_m\), or report failure if the node has no such child.
public def contains [LinearOrder α] (x : α) : BTree α → Bool
| .leaf keys => decide (x ∈ keys)
| .node keys children => containsList x keys children
where
containsList (x : α) : List α → List (BTree α) → Bool
| [], child :: _ => contains x child
| [], [] => false
| key :: keys, child :: children =>
if x < key then contains x child
else if key < x then containsList x keys children
else true
| _ :: _, [] => falsepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionResult of inserting into a B-tree subtree#✓fully proved
An insertion result over a key type \(\alpha\) is either a single tree over \(\alpha\), or a triple \((\ell, m, r)\) of two trees \(\ell\) and \(r\) over \(\alpha\) and a key \(m\) of \(\alpha\). In insertion, the first form is a subtree that did not split, and the second form is an overflowing node split into two trees of the same height, with the median key \(m\) promoted between them; the type itself does not record heights.
public def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 8
DefinitionFlattening of a B-tree insertion result#✓fully proved
The flattening of an insertion result that is a single tree is the flattening of that tree; for a result that splits into a left tree \(\ell\), a promoted median key \(m\) and a right tree \(r\), it is the flattening of \(\ell\), followed by \(m\), followed by the flattening of \(r\).
public def grownFlatten : InsResult α → List α
| .inl tree => flatten tree
| .inr (left, median, right) => flatten left ++ median :: flatten rightpublic def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:660
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 3 · Used by 2
DefinitionInsertion into a B-tree leaf#✓fully proved
Over a linearly ordered key type, let \(t\) be a natural number, \(x\) a key, \(K\) the key list of a leaf, and \(K'\) the result of ordered insertion of \(x\) into \(K\). If \(K'\) has at most \(2t - 1\) keys, the insertion result is the single leaf with keys \(K'\). Otherwise the leaf is split: the result consists of the leaf holding the first \(t - 1\) keys of \(K'\), the next key of \(K'\) promoted as the median, and the leaf holding the remaining keys. Here subtraction of natural numbers is truncated at \(0\).
public def insLeaf [LinearOrder α] (t : Nat) (x : α) (keys : List α) : InsResult α :=
if (orderedInsert x keys).length ≤ 2 * t - 1 then .inl (.leaf (orderedInsert x keys))
else match (orderedInsert x keys).drop (t - 1) with
| [] => .inl (.leaf (orderedInsert x keys))
| median :: rest => .inr (.leaf ((orderedInsert x keys).take (t - 1)), median, .leaf rest)public def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:660
public def orderedInsert [LinearOrder α] (x : α) : List α → List α
| [] => [x]
| a :: as =>
if x < a then x :: a :: as
else if a < x then a :: orderedInsert x as
else a :: asCSLibExt/Algorithms/Lean/DataStructures/OrderedInsert.lean:44
Uses 3 · Used by 3
DefinitionSplitting a B-tree node#✓fully proved
Let \(t\) be a minimum degree, \(s = t - 1\) (so \(s = 0\) when \(t = 0\)), \(k_1, \dots, k_m\) a list of keys and \(c_1, \dots, c_n\) a list of B-trees. If \(m > s\), splitting returns the pair of internal nodes formed by the keys \(k_1, \dots, k_s\) with the first \(t\) children (all of them if \(n < t\)) and by the keys \(k_{s+2}, \dots, k_m\) with the children after the first \(t\), together with the key \(k_{s+1}\) promoted between them. If \(m \le s\), it returns the single internal node with keys \(k_1, \dots, k_m\) and children \(c_1, \dots, c_n\) unchanged.
On an overfull node with \(2t\) keys and \(t \ge 1\), the promoted key \(k_t\) is the median key.
public def splitNode (t : Nat) (keys : List α) (children : List (BTree α)) : InsResult α :=
match keys.drop (t - 1) with
| [] => .inl (.node keys children)
| median :: rightKeys =>
.inr (.node (keys.take (t - 1)) (children.take t), median,
.node rightKeys (children.drop t))public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:660
Uses 2 · Used by 3
DefinitionRebuilding an internal node after insertion#✓fully proved
For minimum degree \(t\), a separator list \(K\) and a child list \(C\), the result is the internal node with separators \(K\) and children \(C\), kept as a single tree when \(K\) has at most \(2t - 1\) keys, and otherwise split by node splitting into two nodes and a promoted median key.
public def mkNode (t : Nat) (keys : List α) (children : List (BTree α)) : InsResult α :=
if keys.length ≤ 2 * t - 1 then .inl (.node keys children) else splitNode t keys childrenpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:660
public def splitNode (t : Nat) (keys : List α) (children : List (BTree α)) : InsResult α :=
match keys.drop (t - 1) with
| [] => .inl (.node keys children)
| median :: rightKeys =>
.inr (.node (keys.take (t - 1)) (children.take t), median,
.node rightKeys (children.drop t))CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:679
Uses 3 · Used by 3
DefinitionSplit-returning insertion into a B-tree subtree#✓fully proved
For minimum degree \(t\) and a key \(x\), insertion of \(x\) into a tree returns an insertion result and is defined by recursion. At a leaf with key list \(K\), it is leaf insertion of \(x\) into \(K\). At an internal node, the separator list and the child list are scanned together from the left. If \(x\) is smaller than the current separator, or no separator is left but a child is, \(x\) is inserted into the current child. If \(x\) is larger than the current separator, the scan moves on to the next separator and child. If \(x\) equals the current separator, or no child is left, the remaining lists are kept unchanged. When the child that received \(x\) returns a single tree, that tree replaces the child; when it returns two trees \(\ell\), \(r\) with a median \(m\), the child is replaced by \(\ell\) and \(r\) with \(m\) inserted as a separator between them. The rebuilt separator and child lists are then turned into a node by the internal-node rebuilding step: kept as one node if there are at most \(2t - 1\) separators, and split otherwise.
Cslib.Algorithms.Lean.BTree.ins · 23 lines
public def ins [LinearOrder α] (t : Nat) (x : α) : BTree α → InsResult α
| .leaf keys => insLeaf t x keys
| .node keys children =>
let (keys', children') := insList t x keys children
mkNode t keys' children'
where
insList (t : Nat) (x : α) : List α → List (BTree α) → List α × List (BTree α)
| [], child :: children =>
match ins t x child with
| .inl child' => ([], child' :: children)
| .inr (left, median, right) => ([median], left :: right :: children)
| [], [] => ([], [])
| key :: keys, child :: children =>
if x < key then
match ins t x child with
| .inl child' => (key :: keys, child' :: children)
| .inr (left, median, right) =>
(median :: key :: keys, left :: right :: children)
else if key < x then
let (keys', children') := insList t x keys children
(key :: keys', child :: children')
else (key :: keys, child :: children)
| key :: keys, [] => (key :: keys, [])public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def InsResult (α : Type u) := BTree α ⊕ (BTree α × α × BTree α)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:660
public def insLeaf [LinearOrder α] (t : Nat) (x : α) (keys : List α) : InsResult α :=
if (orderedInsert x keys).length ≤ 2 * t - 1 then .inl (.leaf (orderedInsert x keys))
else match (orderedInsert x keys).drop (t - 1) with
| [] => .inl (.leaf (orderedInsert x keys))
| median :: rest => .inr (.leaf ((orderedInsert x keys).take (t - 1)), median, .leaf rest)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:670
public def mkNode (t : Nat) (keys : List α) (children : List (BTree α)) : InsResult α :=
if keys.length ≤ 2 * t - 1 then .inl (.node keys children) else splitNode t keys childrenCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:688
Uses 4 · Used by 3
DefinitionB-tree insertion#✓fully proved
For minimum degree \(t\), the tree obtained by inserting a key \(x\) into a tree \(T\) is computed from the split-returning insertion of \(x\) into \(T\): if that returns a single tree, this tree is the result; if it returns two trees \(\ell\) and \(r\) with a promoted median key \(m\), the result is a new root node with the single separator \(m\) and the two children \(\ell\) and \(r\).
When \(T\) is a B-tree of minimum degree \(t\), inserting a key already present in \(T\) returns a tree with the same flattening.
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def ins [LinearOrder α] (t : Nat) (x : α) : BTree α → InsResult α
| .leaf keys => insLeaf t x keys
| .node keys children =>
let (keys', children') := insList t x keys children
mkNode t keys' children'
where
insList (t : Nat) (x : α) : List α → List (BTree α) → List α × List (BTree α)
| [], child :: children =>
match ins t x child with
| .inl child' => ([], child' :: children)
| .inr (left, median, right) => ([median], left :: right :: children)
| [], [] => ([], [])
⋯CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:696
Uses 3 · Used by 6
DefinitionThe empty B-tree#✓fully proved
The empty B-tree is the leaf with no keys.
public def empty : BTree α :=
.leaf []public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 2
DefinitionB-trees of a given minimum degree#✓fully proved
A tree \(T\) is a B-tree of minimum degree \(t\) when \(t \ge 2\) (the CLRS Chapter 18 minimum-degree requirement), \(T\) is ordered, and \(T\) is root-valid at some height. This is the invariant preserved by insertion and by building a tree from a list.
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
Uses 3 · Used by 23
TheoremThe minimum degree of a B-tree is at least two#✓fully proved
If a tree is a B-tree of minimum degree \(t\), then \(t \ge 2\).
public theorem IsBTree.two_le [LT α] {t : Nat} {tree : BTree α}
(h : IsBTree t tree) : 2 ≤ tpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
Uses 4
TheoremB-trees are ordered#✓fully proved
If a tree is a B-tree of minimum degree \(t\), then it is ordered: each key of its inorder flattening is less than every key that comes after it.
public theorem IsBTree.ordered [LT α] {t : Nat} {tree : BTree α}
(h : IsBTree t tree) : Ordered treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
Uses 4 · Used by 5
TheoremB-trees satisfy the root invariant#✓fully proved
If \(T\) is a B-tree of minimum degree \(t\), then there is a height \(h\) such that \(T\) satisfies the root structural invariant of minimum degree \(t\) at height \(h\).
public theorem IsBTree.exists_validRoot [LT α] {t : Nat} {tree : BTree α}
(h : IsBTree t tree) : ∃ height, ValidRoot t height treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
Uses 4 · Used by 2
TheoremThe empty tree is a B-tree#✓fully proved
For every key type equipped with a binary relation \(<\) and every natural number \(t \ge 2\), the empty B-tree is a B-tree of minimum degree \(t\).
public theorem IsBTree.empty [LT α] {t : Nat} (ht : 2 ≤ t) :
IsBTree t (empty : BTree α)public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def empty : BTree α :=
.leaf []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1123
public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 7 · Used by 1
TheoremB-tree insertion as sorted list insertion#✓fully proved
Let \(\alpha\) be linearly ordered, let \(t \ge 2\), and let \(T\) be a B-tree of minimum degree \(t\) with keys in \(\alpha\). For every key \(x \in \alpha\), the inorder flattening of the tree obtained by inserting \(x\) into \(T\) with minimum degree \(t\) equals the sorted insertion of \(x\) into the inorder flattening of \(T\).
public theorem flatten_insert [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) :
flatten (insert t x tree) = orderedInsert x (flatten tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1117
public def orderedInsert [LinearOrder α] (x : α) : List α → List α
| [] => [x]
| a :: as =>
if x < a then x :: a :: as
else if a < x then a :: orderedInsert x as
else a :: asCSLibExt/Algorithms/Lean/DataStructures/OrderedInsert.lean:44
Uses 21 · Used by 4
TheoremMembership after B-tree insertion#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For all keys \(x\) and \(y\), \(y\) belongs to the tree obtained by inserting \(x\) into \(T\) if and only if \(y = x\) or \(y\) belongs to \(T\).
public theorem mem_insert [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x y : α}
{tree : BTree α} (h : IsBTree t tree) :
y ∈ insert t x tree ↔ y = x ∨ y ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1117
Uses 8 · Used by 1
TheoremInsertion preserves the B-tree invariant#✓fully proved
Let \(t \ge 2\) and let the keys come from a linearly ordered type. If \(T\) is a B-tree of minimum degree \(t\), then for every key \(x\) the tree obtained by inserting \(x\) into \(T\) is again a B-tree of minimum degree \(t\): it is ordered and root-valid at some height.
public theorem IsBTree.insert [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) : IsBTree t (BTree.insert t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1117
Uses 22 · Used by 1
TheoremCorrectness of B-tree search#✓fully proved
Let \(\alpha\) be linearly ordered and let \(T\) be a B-tree of minimum degree \(t\) with keys in \(\alpha\). For every key \(x \in \alpha\), the search procedure returns true on \(x\) and \(T\) if and only if \(x\) is a member of \(T\), that is, \(x\) occurs in the inorder flattening of \(T\).
public theorem contains_eq_true_iff [LinearOrder α] {t : Nat} {x : α} {tree : BTree α}
(h : IsBTree t tree) : contains x tree = true ↔ x ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def contains [LinearOrder α] (x : α) : BTree α → Bool
| .leaf keys => decide (x ∈ keys)
| .node keys children => containsList x keys children
where
containsList (x : α) : List α → List (BTree α) → Bool
| [], child :: _ => contains x child
| [], [] => false
| key :: keys, child :: children =>
if x < key then contains x child
else if key < x then containsList x keys children
else true
| _ :: _, [] => falseCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:549
Uses 13 · Used by 2
TheoremSize of a B-tree after insertion#✓fully proved
Let \(\alpha\) be linearly ordered, let \(t \ge 2\), let \(T\) be a B-tree of minimum degree \(t\) with keys in \(\alpha\), and let \(x \in \alpha\). Let \(T'\) be the tree obtained by inserting \(x\) into \(T\) with minimum degree \(t\). If \(x\) occurs in the inorder flattening of \(T\), then the flattening of \(T'\) has the same length as that of \(T\); otherwise it is one longer.
public theorem flatten_length_insert [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) :
(flatten (insert t x tree)).length =
if x ∈ flatten tree then (flatten tree).length else (flatten tree).length + 1public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1117
Uses 9
DefinitionB-tree built from a list#✓fully proved
For a linearly ordered key type and a natural number \(t\), the tree built from the empty list is the empty tree, and the tree built from a list with head \(x\) and tail \(L\) is the result of inserting \(x\), with minimum degree \(t\), into the tree built from \(L\). Thus the elements are inserted from right to left.
public def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def empty : BTree α :=
.leaf []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1123
public def insert [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
match ins t x tree with
| .inl tree' => tree'
| .inr (left, median, right) => .node [median] [left, right]CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1117
Uses 3 · Used by 5
TheoremBuilding from a list yields a B-tree#✓fully proved
For a linearly ordered key type, every natural number \(t \ge 2\) and every list \(L\) of keys, the tree obtained by inserting the elements of \(L\) from right to left into the empty tree, each insertion with minimum degree \(t\), is a B-tree of minimum degree \(t\).
public theorem IsBTree.fromList [LinearOrder α] {t : Nat} (ht : 2 ≤ t) (xs : List α) :
IsBTree t (fromList t xs)public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1272
Uses 4 · Used by 3
TheoremMembership in a B-tree built from a list#✓fully proved
Let \(t \ge 2\) and let \(xs\) be a list over a linearly ordered key type. A key \(x\) belongs to the tree of minimum degree \(t\) built from \(xs\) (by inserting the elements of \(xs\) into the empty tree, from right to left) if and only if \(x\) is an element of \(xs\).
public theorem mem_fromList [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{xs : List α} : x ∈ fromList t xs ↔ x ∈ xspublic def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1272
TheoremBuilding a B-tree from a strictly increasing list#✓fully proved
Let \(t \ge 2\). For every strictly increasing list \(L\) of keys, the tree built from \(L\) by inserting its keys from right to left into the empty tree with minimum degree \(t\) has flattening exactly \(L\).
public theorem flatten_fromList_of_pairwise [LinearOrder α] {t : Nat} (ht : 2 ≤ t) :
∀ {keys : List α}, keys.Pairwise (· < ·) → flatten (fromList t keys) = keyspublic def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1272
Uses 7 · Used by 1
DefinitionB-tree deletion by rebuilding#✓fully proved
For a minimum degree \(t\), a key \(x\) and a tree \(T\), the rebuilding deletion of \(x\) from \(T\) is the tree obtained by inserting the keys of the list \(L\), from right to left, into the empty tree with B-tree insertion of minimum degree \(t\), where \(L\) is the inorder flattening of \(T\) with the first occurrence of \(x\) removed (\(L\) is the flattening itself when \(x\) does not occur in it).
This is a reference implementation, not the single-pass borrow-and-merge deletion of CLRS Section 18.3, which is formalized separately.
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1272
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 3 · Used by 11
TheoremRebuilding deletion unfolds to erase and rebuild#✓fully proved
For every minimum degree \(t\), key \(x\) and tree \(T\), the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) equals the tree built from the list obtained by removing the first occurrence of \(x\) from the flattening of \(T\), by inserting its keys from right to left into the empty tree with minimum degree \(t\).
public theorem deleteRebuild_eq_fromList_erase [LinearOrder α] {t : Nat} {x : α}
{tree : BTree α} : deleteRebuild t x tree = fromList t ((flatten tree).erase x)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
public def fromList [LinearOrder α] (t : Nat) : List α → BTree α
| [] => empty
| x :: xs => insert t x (fromList t xs)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1272
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
Uses 4
TheoremFlattening after rebuilding deletion#✓fully proved
Let \(t \ge 2\), let \(T\) be an ordered tree and let \(x\) be a key. The flattening of the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) is the flattening of \(T\) with the first occurrence of \(x\) removed (unchanged if \(x\) does not occur).
No occupancy hypothesis on \(T\) is needed.
public theorem flatten_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : Ordered tree) :
flatten (deleteRebuild t x tree) = (flatten tree).erase xpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5 · Used by 4
TheoremRebuilding deletion yields a B-tree#✓fully proved
Let \(t \ge 2\). For every key \(x\) and every tree \(T\), whether or not \(T\) is itself a B-tree, the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) is a B-tree of minimum degree \(t\).
public theorem IsBTree.deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} : IsBTree t (deleteRebuild t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5 · Used by 3
TheoremRebuild deletion yields an ordered tree#✓fully proved
Let \(t \ge 2\) and let keys come from a linearly ordered type. For every key \(x\) and every tree \(T\), not necessarily ordered, the tree obtained from \(T\) by rebuild deletion of \(x\) (removing the first occurrence of \(x\), if any, from the inorder flattening of \(T\) and rebuilding a B-tree of minimum degree \(t\) from the remaining keys) is ordered: its inorder flattening is strictly increasing.
public theorem ordered_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} : Ordered (deleteRebuild t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5 · Used by 1
TheoremRebuilding deletion yields a root-valid tree#✓fully proved
Let \(t \ge 2\). For every key \(x\) and every tree \(T\), there is a height \(h\) such that the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) is root-valid of minimum degree \(t\) and height \(h\): all leaves sit at depth \(h\), every node holds at most \(2t - 1\) keys, every non-root node holds at least \(t - 1\) keys, an internal root holds at least one key, and an internal node with \(k\) keys has \(k + 1\) children.
No relation between \(h\) and the height of \(T\) is claimed.
public theorem deleteRebuild_validRoot [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} : ∃ height, ValidRoot t height (deleteRebuild t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5
TheoremMembership after rebuild deletion from a B-tree#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) with keys in a linearly ordered type. For all keys \(x\) and \(y\), the key \(y\) lies in the tree obtained from \(T\) by rebuild deletion of \(x\) (erasing \(x\) from the inorder flattening of \(T\) and rebuilding a B-tree of minimum degree \(t\) from the remaining keys) if and only if \(y \ne x\) and \(y\) lies in \(T\).
public theorem mem_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x y : α}
{tree : BTree α} (h : IsBTree t tree) :
y ∈ deleteRebuild t x tree ↔ y ≠ x ∧ y ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 8 · Used by 2
TheoremThe deleted key is absent after rebuild deletion#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) with keys in a linearly ordered type. For every key \(x\), the tree obtained from \(T\) by rebuild deletion of \(x\) (erasing \(x\) from the inorder flattening of \(T\) and rebuilding a B-tree of minimum degree \(t\) from the remaining keys) does not contain \(x\).
public theorem not_mem_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) : x ∉ deleteRebuild t x treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5
TheoremSearch after rebuilding deletion#✓fully proved
Let \(t \ge 2\), let \(T\) be a B-tree of minimum degree \(t\), and let \(x\) and \(y\) be keys. The B-tree search for \(y\) in the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) returns true if and only if \(y \ne x\) and \(y\) is stored in \(T\).
public theorem contains_deleteRebuild_iff [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x y : α}
{tree : BTree α} (h : IsBTree t tree) :
contains y (deleteRebuild t x tree) = true ↔ y ≠ x ∧ y ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def contains [LinearOrder α] (x : α) : BTree α → Bool
| .leaf keys => decide (x ∈ keys)
| .node keys children => containsList x keys children
where
containsList (x : α) : List α → List (BTree α) → Bool
| [], child :: _ => contains x child
| [], [] => false
| key :: keys, child :: children =>
if x < key then contains x child
else if key < x then containsList x keys children
else true
| _ :: _, [] => falseCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:549
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
TheoremRebuilding deletion of an absent key#✓fully proved
Let \(t \ge 2\), let \(T\) be an ordered tree and let \(x\) be a key that does not occur in the flattening of \(T\). Then the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) has the same flattening as \(T\).
The tree itself may be rebuilt to a different shape with the same flattening.
public theorem flatten_deleteRebuild_of_not_mem [LinearOrder α] {t : Nat} (ht : 2 ≤ t)
{x : α} {tree : BTree α} (h : Ordered tree) (hx : x ∉ flatten tree) :
flatten (deleteRebuild t x tree) = flatten treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5
TheoremKey count after rebuilding deletion#✓fully proved
Let \(t \ge 2\), let \(T\) be an ordered tree with flattening of length \(n\), and let \(x\) be a key. The flattening of the rebuilding deletion of \(x\) from \(T\) with minimum degree \(t\) has length \(n - 1\) if \(x\) occurs in the flattening of \(T\), and length \(n\) otherwise.
public theorem flatten_length_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : Ordered tree) :
(flatten (deleteRebuild t x tree)).length =
if x ∈ flatten tree then (flatten tree).length - 1 else (flatten tree).lengthpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
Uses 5
TheoremRebuilding deletion of the same key twice#✓fully proved
Let \(t \ge 2\), let \(T\) be an ordered tree (its flattening is strictly increasing) and let \(x\) be a key. Deleting \(x\) twice by rebuilding with minimum degree \(t\) gives a tree with the same flattening as deleting \(x\) once.
public theorem flatten_deleteRebuild_deleteRebuild [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : Ordered tree) :
flatten (deleteRebuild t x (deleteRebuild t x tree)) = flatten (deleteRebuild t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def deleteRebuild [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) : BTree α :=
fromList t ((flatten tree).erase x)CSLibExt/Algorithms/Lean/DataStructures/BTree/Delete.lean:112
DefinitionNumber of keys at the root of a B-tree#✓fully proved
For a raw B-tree \(T\), this is the length of the key list stored at the root of \(T\): the number of keys of \(T\) if \(T\) is a leaf, and the number of separator keys of \(T\) if \(T\) is an internal node. Keys in the children are not counted.
public def keyCount : BTree α → Nat
| .leaf keys => keys.length
| .node keys _ => keys.lengthpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionSplitting off the last element of a list#✓fully proved
For a nonempty list \(l\), the result is the pair consisting of \(l\) with its last element removed and the last element of \(l\); for the empty list there is no result.
DefinitionRightmost key of a B-tree#✓fully proved
For a tree \(T\), the rightmost key of \(T\) is an optional key defined by descending the rightmost spine: for a leaf it is the last of its keys (none if the leaf has no keys); for an internal node with at least one child it is the rightmost key of its last child; for an internal node with no children it is the last of its separator keys (none if there are none).
If \(T\) satisfies the structural B-tree invariant for a minimum degree \(t \ge 2\) and has at least one key at its root, the rightmost key exists and is the last key of the inorder flattening of \(T\), so on an ordered tree it is the greatest key. Each step splits a child list of length at most \(2t\), so on a valid tree of height \(h\) the descent costs \(O(t h)\), without computing the flattening.
def maxKey : BTree α → Option α
| .leaf keys => keys.getLast?
| .node keys children =>
match h : splitLast children with
| some (_, last) => maxKey last
| none => keys.getLast?
termination_by tree => sizeOf tree
decreasing_by
have hmem : last ∈ children := by
rw [splitLast_spec h]
simp
have hlt := List.sizeOf_lt_of_mem hmem
rw [BTree.node.sizeOf_spec]
omegapublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
def splitLast : List α → Option (List α × α)
| [] => none
| a :: l => some ((a :: l).dropLast, (a :: l).getLast (by simp))CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:73
Uses 2 · Used by 3
DefinitionLeftmost key of a B-tree#✓fully proved
For a tree \(T\), the leftmost key of \(T\) is an optional key defined by descending the leftmost spine: for a leaf it is the first of its keys (none if the leaf has no keys); for an internal node with at least one child it is the leftmost key of its first child; for an internal node with no children it is the first of its separator keys (none if there are none).
If \(T\) satisfies the structural B-tree invariant for a minimum degree \(t \ge 2\) and has at least one key at its root, the leftmost key exists and is the first key of the inorder flattening of \(T\), so on an ordered tree it is the least key.
def minKey : BTree α → Option α
| .leaf keys => keys.head?
| .node keys children =>
match children with
| child :: _ => minKey child
| [] => keys.head?public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionMerging two B-tree nodes around a separator#✓fully proved
Given a key \(s\) and trees \(L\) and \(R\), the merge of \(L\) and \(R\) around \(s\) is defined as follows. If \(L\) and \(R\) are leaves with key lists \(k_1\) and \(k_2\), it is the leaf with keys \(k_1\), then \(s\), then \(k_2\). If \(L\) and \(R\) are internal nodes with key lists \(k_1, k_2\) and child lists \(c_1, c_2\), it is the internal node with keys \(k_1\), then \(s\), then \(k_2\), and children \(c_1\) followed by \(c_2\). In every other case it is \(L\).
In deletion from a B-tree of minimum degree \(t\), it is applied to two trees of the same height that each hold \(t - 1\) keys at the root, so the merged node holds \(2t - 1\) keys.
def merge (sep : α) : BTree α → BTree α → BTree α
| .leaf ks1, .leaf ks2 => .leaf (ks1 ++ sep :: ks2)
| .node ks1 cs1, .node ks2 cs2 => .node (ks1 ++ sep :: ks2) (cs1 ++ cs2)
| tree, _ => treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionBorrowing a key from the right sibling#✓fully proved
Given a tree \(c\) (the child), a separator key \(k\) and a tree \(s\) (the right sibling) such that \(c\) and \(s\) are both leaves or both internal nodes, \(s\) has at least one key, and, when they are internal nodes, \(s\) has at least one child: \(k\) becomes the last key of \(c\), the first key of \(s\) is removed from \(s\) and becomes the new separator, and, for internal nodes, the first child of \(s\) is removed from \(s\) and becomes the last child of \(c\). The result is the triple of the new child, the new separator and the new sibling. In every other case the result is the unchanged triple \((c, k, s)\).
def borrowRight : BTree α → α → BTree α → BTree α × α × BTree α
| .leaf ks, sep, .leaf (s0 :: ss) => (.leaf (ks ++ [sep]), s0, .leaf ss)
| .node ks cs, sep, .node (s0 :: ss) (sc0 :: scs) =>
(.node (ks ++ [sep]) (cs ++ [sc0]), s0, .node ss scs)
| child, sep, sib => (child, sep, sib)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionBorrowing a key from the left sibling#✓fully proved
Given a tree \(s\) (the left sibling), a separator key \(k\) and a tree \(c\) (the child) such that \(s\) and \(c\) are both leaves or both internal nodes, \(s\) has at least one key, and, when they are internal nodes, \(s\) has at least one child: the last key of \(s\) is removed from \(s\) and becomes the new separator, \(k\) becomes the first key of \(c\), and, for internal nodes, the last child of \(s\) is removed from \(s\) and becomes the first child of \(c\). The result is the triple of the new sibling, the new separator and the new child. In every other case the result is the unchanged triple \((s, k, c)\).
def borrowLeft : BTree α → α → BTree α → BTree α × α × BTree α
| .leaf ks, sep, .leaf kc =>
match splitLast ks with
| some (init, last) => (.leaf init, last, .leaf (sep :: kc))
| none => (.leaf ks, sep, .leaf kc)
| .node ks cs, sep, .node kc cc =>
match splitLast ks, splitLast cs with
| some (iks, last), some (ics, clast) =>
(.node iks ics, last, .node (sep :: kc) (clast :: cc))
| _, _ => (.node ks cs, sep, .node kc cc)
| sib, sep, child => (sib, sep, child)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
def splitLast : List α → Option (List α × α)
| [] => none
| a :: l => some ((a :: l).dropLast, (a :: l).getLast (by simp))CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:73
Uses 2 · Used by 3
DefinitionDeletion within a B-tree node#✓fully proved
Let \(D\) be an operation that deletes a key from a tree, let \(t\) be a natural number, let \(x\) be a key of a linearly ordered key type, and write \(|c|\) for the number of keys stored at the root of a tree \(c\). Deleting \(x\) within a node with separator list \(K\) and child list \(C\), using \(D\) on children, produces a new separator list and a new child list. Write \(k\) for the first separator, \(c\) for the first child, and \(K'\) and \(C'\) for the remaining separators and children.
If \(K\) is empty and \(C\) is nonempty, \(D\) deletes \(x\) from the first child and nothing else changes; if both are empty, so is the result.
If \(x < k\) and either \(|c| \ge t\) or \(C'\) is empty, \(D\) deletes \(x\) from \(c\). Otherwise let \(s\) be the first tree of \(C'\). If \(|s| \ge t\), borrowing for \(c\) from its right sibling \(s\) with separator \(k\) gives \((c', k', s')\), which replace \(c\), \(k\) and \(s\), and \(D\) deletes \(x\) from \(c'\). If \(|s| < t\), the trees \(c\) and \(s\) are merged with \(k\) into one tree, which replaces \(c\) and \(s\), \(k\) is dropped from the separators, and \(D\) deletes \(x\) from the merged tree.
If \(k < x\), \(K'\) is empty and \(C'\) consists of a single tree \(l\): if \(|l| \ge t\), \(D\) deletes \(x\) from \(l\); otherwise, if \(|c| \ge t\), borrowing for \(l\) from its left sibling \(c\) with separator \(k\) gives \((c', k', l')\), which replace \(c\), \(k\) and \(l\), and \(D\) deletes \(x\) from \(l'\); otherwise the result has no separators and a single child, obtained by applying \(D\) to delete \(x\) from the merge of \(c\) and \(l\) with \(k\). If \(k < x\) and \(K'\) is nonempty, \(k\) and \(c\) are kept and the deletion continues recursively within \(K'\) and \(C'\).
If \(x = k\) and \(C'\) is nonempty with first tree \(r\): if \(|c| \ge t\), the key \(p\) found by descending the rightmost spine of \(c\) (following last children down to a leaf or to an internal node without children, and taking the last key there) replaces \(k\) and \(D\) deletes \(p\) from \(c\); otherwise, if \(|r| \ge t\), the key \(q\) found by descending the leftmost spine of \(r\) (following first children in the same way and taking the first key there) replaces \(k\) and \(D\) deletes \(q\) from \(r\); otherwise \(c\) and \(r\) are merged with \(k\) into one tree, which replaces \(c\) and \(r\), \(k\) is dropped from the separators, and \(D\) deletes \(x\) from the merged tree.
In every remaining case (a shape of the separator and child lists not covered above, or a spine descent that ends at a node with no keys) the lists are returned unchanged.
Cslib.Algorithms.Lean.BTree.delList · 41 lines
def delList [LinearOrder α] (delChild : α → BTree α → BTree α) (t : Nat)
(x : α) : List α → List (BTree α) → List α × List (BTree α)
| [], child :: children => ([], delChild x child :: children)
| [], [] => ([], [])
| key :: keys, child :: children =>
if x < key then
if t ≤ keyCount child then (key :: keys, delChild x child :: children)
else
match children with
| sib :: rest =>
if t ≤ keyCount sib then
let (child', sep', sib') := borrowRight child key sib
(sep' :: keys, delChild x child' :: sib' :: rest)
else (keys, delChild x (merge key child sib) :: rest)
| [] => (key :: keys, delChild x child :: children)
else if key < x then
match keys, children with
| [], [last] =>
if t ≤ keyCount last then ([key], [child, delChild x last])
else if t ≤ keyCount child then
let (child', sep', last') := borrowLeft child key last
([sep'], [child', delChild x last'])
else ([], [delChild x (merge key child last)])
| _ :: _, _ =>
let (keys', children') := delList delChild t x keys children
(key :: keys', child :: children')
| _, _ => (key :: keys, child :: children)
else
match children with
| rchild :: rest =>
if t ≤ keyCount child then
match maxKey child with
| some p => (p :: keys, delChild p child :: rchild :: rest)
| none => (key :: keys, child :: children)
else if t ≤ keyCount rchild then
match minKey rchild with
| some s => (s :: keys, child :: delChild s rchild :: rest)
| none => (key :: keys, child :: children)
else (keys, delChild x (merge key child rchild) :: rest)
| [] => (key :: keys, child :: children)
| keys, children => (keys, children)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def keyCount : BTree α → Nat
| .leaf keys => keys.length
| .node keys _ => keys.lengthCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:67
def borrowRight : BTree α → α → BTree α → BTree α × α × BTree α
| .leaf ks, sep, .leaf (s0 :: ss) => (.leaf (ks ++ [sep]), s0, .leaf ss)
| .node ks cs, sep, .node (s0 :: ss) (sc0 :: scs) =>
(.node (ks ++ [sep]) (cs ++ [sc0]), s0, .node ss scs)
| child, sep, sib => (child, sep, sib)CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:161
def merge (sep : α) : BTree α → BTree α → BTree α
| .leaf ks1, .leaf ks2 => .leaf (ks1 ++ sep :: ks2)
| .node ks1 cs1, .node ks2 cs2 => .node (ks1 ++ sep :: ks2) (cs1 ++ cs2)
| tree, _ => treeCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:152
def borrowLeft : BTree α → α → BTree α → BTree α × α × BTree α
| .leaf ks, sep, .leaf kc =>
match splitLast ks with
| some (init, last) => (.leaf init, last, .leaf (sep :: kc))
| none => (.leaf ks, sep, .leaf kc)
| .node ks cs, sep, .node kc cc =>
match splitLast ks, splitLast cs with
| some (iks, last), some (ics, clast) =>
(.node iks ics, last, .node (sep :: kc) (clast :: cc))
| _, _ => (.node ks cs, sep, .node kc cc)
| sib, sep, child => (sib, sep, child)CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:171
def maxKey : BTree α → Option α
| .leaf keys => keys.getLast?
| .node keys children =>
match h : splitLast children with
| some (_, last) => maxKey last
| none => keys.getLast?
termination_by tree => sizeOf tree
decreasing_by
have hmem : last ∈ children := by
rw [splitLast_spec h]
simp
have hlt := List.sizeOf_lt_of_mem hmem
⋯CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:103
def minKey : BTree α → Option α
| .leaf keys => keys.head?
| .node keys children =>
match children with
| child :: _ => minKey child
| [] => keys.head?CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:132
DefinitionHeight-indexed B-tree deletion#✓fully proved
Given a height \(h\), a minimum degree \(t\), a key \(x\) of a linearly ordered key type and a tree \(T\), the result is defined as follows. If \(T\) is a leaf, the result is the leaf whose key list is that of \(T\) with the first occurrence of \(x\) erased, whatever \(h\) is. If \(T\) is an internal node and \(h = 0\), the result is \(T\). If \(T\) is an internal node and \(h = n + 1\), the result is the internal node whose separator and child lists are obtained by deletion of \(x\) within the node of \(T\) (with minimum degree \(t\)), where deletion from a child is height-indexed deletion with minimum degree \(t\) at height \(n\).
The correctness specification only covers heights that match the shape of the tree.
def delH [LinearOrder α] : Nat → Nat → α → BTree α → BTree α
| 0, _, x, .leaf keys => .leaf (keys.erase x)
| 0, _, _, .node keys children => .node keys children
| _ + 1, _, x, .leaf keys => .leaf (keys.erase x)
| h + 1, t, x, .node keys children =>
match delList (delH h t) t x keys children with
| (keys', children') => .node keys' children'public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
def delList [LinearOrder α] (delChild : α → BTree α → BTree α) (t : Nat)
(x : α) : List α → List (BTree α) → List α × List (BTree α)
| [], child :: children => ([], delChild x child :: children)
| [], [] => ([], [])
| key :: keys, child :: children =>
if x < key then
if t ≤ keyCount child then (key :: keys, delChild x child :: children)
else
match children with
| sib :: rest =>
if t ≤ keyCount sib then
let (child', sep', sib') := borrowRight child key sib
⋯CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:192
Uses 2 · Used by 3
DefinitionHeight of a B-tree along first children#✓fully proved
The height of a B-tree is computed by following first children: a leaf has height \(0\), an internal node with no children has height \(0\), and an internal node whose first child is \(c\) has height one more than the height of \(c\).
If a tree satisfies the B-tree structural invariant (or the root invariant) at height \(h\), then this height equals \(h\).
public def treeHeight : BTree α → Nat
| .leaf _ => 0
| .node _ children =>
match children with
| [] => 0
| child :: _ => treeHeight child + 1public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
Uses 1 · Used by 3
DefinitionTop-down B-tree deletion#✓fully proved
Deleting a key \(x\) of a linearly ordered key type from a tree \(T\) with minimum degree \(t\) applies height-indexed deletion of \(x\) with minimum degree \(t\) to \(T\) at the height of \(T\), where the height of a leaf, or of an internal node without children, is \(0\), and the height of any other internal node is one more than the height of its first child. If the outcome is an internal node with no keys and exactly one child, the result is that child; otherwise the result is the outcome itself.
This follows the top-down deletion of CLRS Section 18.3.
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
def delH [LinearOrder α] : Nat → Nat → α → BTree α → BTree α
| 0, _, x, .leaf keys => .leaf (keys.erase x)
| 0, _, _, .node keys children => .node keys children
| _ + 1, _, x, .leaf keys => .leaf (keys.erase x)
| h + 1, t, x, .node keys children =>
match delList (delH h t) t x keys children with
| (keys', children') => .node keys' children'CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:241
public def treeHeight : BTree α → Nat
| .leaf _ => 0
| .node _ children =>
match children with
| [] => 0
| child :: _ => treeHeight child + 1CSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:252
Uses 3 · Used by 10
TheoremDeletion from a B-tree erases the key from its flattening#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), the inorder flattening of the tree obtained from \(T\) by top-down deletion of \(x\) with minimum degree \(t\) is the flattening of \(T\) with the first occurrence of \(x\) removed (unchanged if \(x\) does not occur).
public theorem flatten_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) :
flatten (delete t x tree) = (flatten tree).erase xpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 25 · Used by 4
TheoremTop-down deletion lowers the height by at most one#✓fully proved
Let \(t \ge 2\) and let \(T\) be an ordered tree over a linearly ordered key type (its inorder flattening is strictly increasing) that satisfies the root invariant of B-trees of minimum degree \(t\) at height \(h\). For every key \(x\), the tree obtained by deleting \(x\) from \(T\) with minimum degree \(t\) satisfies the root invariant of minimum degree \(t\) at height \(h\) or at height \(h - 1\), where \(h - 1\) is truncated subtraction, so equal to \(0\) when \(h = 0\).
public theorem delete_validRoot [LinearOrder α] {t height : Nat} (ht : 2 ≤ t)
{x : α} {tree : BTree α} (hOrd : Ordered tree)
(hv : ValidRoot t height tree) :
ValidRoot t height (delete t x tree) ∨
ValidRoot t (height - 1) (delete t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 24 · Used by 1
TheoremTop-down deletion preserves the B-tree invariant#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), the tree obtained by deleting \(x\) from \(T\) with minimum degree \(t\) is again a B-tree of minimum degree \(t\).
public theorem IsBTree.delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) : IsBTree t (delete t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 8 · Used by 4
TheoremDeletion from a B-tree yields an ordered tree#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), the tree obtained from \(T\) by deleting \(x\) (with minimum degree \(t\)) is ordered: its inorder flattening is strictly increasing.
public theorem ordered_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) : Ordered (delete t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def Ordered [LT α] (tree : BTree α) : Prop :=
(flatten tree).Pairwise (· < ·)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:382
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 6
TheoremTop-down deletion yields a root-valid tree#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), the tree obtained by deleting \(x\) from \(T\) with minimum degree \(t\) satisfies the root invariant of B-trees of minimum degree \(t\) at some height.
public theorem delete_validRoot_exists [LinearOrder α] {t : Nat} (ht : 2 ≤ t)
{x : α} {tree : BTree α} (h : IsBTree t tree) :
∃ height, ValidRoot t height (delete t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public inductive ValidRoot (t : Nat) : Nat → BTree α → Prop where
| leaf {keys : List α} (hhi : keys.length ≤ 2 * t - 1) : ValidRoot t 0 (.leaf keys)
| node {height : Nat} {keys : List α} {children : List (BTree α)}
(hlo : 1 ≤ keys.length) (hhi : keys.length ≤ 2 * t - 1)
(hlen : children.length = keys.length + 1)
(hchildren : ∀ child ∈ children, Valid t (t - 1) height child) :
ValidRoot t (height + 1) (.node keys children)CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:530
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 6
TheoremMembership after deletion from a B-tree#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For all keys \(x\) and \(y\), \(y\) belongs to the tree obtained from \(T\) by deleting \(x\) (with minimum degree \(t\)) if and only if \(y \ne x\) and \(y\) belongs to \(T\).
public theorem mem_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x y : α}
{tree : BTree α} (h : IsBTree t tree) :
y ∈ delete t x tree ↔ y ≠ x ∧ y ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 8 · Used by 2
TheoremThe deleted key is absent after deletion from a B-tree#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), \(x\) does not belong to the tree obtained from \(T\) by deleting \(x\) (with minimum degree \(t\)).
public theorem not_mem_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t) {x : α}
{tree : BTree α} (h : IsBTree t tree) : x ∉ delete t x treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 5
TheoremSearch after top-down deletion#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For all keys \(x\) and \(y\), searching for \(y\) in the tree obtained by deleting \(x\) from \(T\) with minimum degree \(t\) succeeds if and only if \(y \ne x\) and \(y\) is a key of \(T\).
public theorem contains_delete_iff [LinearOrder α] {t : Nat} (ht : 2 ≤ t)
{x y : α} {tree : BTree α} (h : IsBTree t tree) :
contains y (delete t x tree) = true ↔ y ≠ x ∧ y ∈ treepublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def contains [LinearOrder α] (x : α) : BTree α → Bool
| .leaf keys => decide (x ∈ keys)
| .node keys children => containsList x keys children
where
containsList (x : α) : List α → List (BTree α) → Bool
| [], child :: _ => contains x child
| [], [] => false
| key :: keys, child :: children =>
if x < key then contains x child
else if key < x then containsList x keys children
else true
| _ :: _, [] => falseCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:549
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
TheoremDeletion shortens the flattening by one exactly when the key is present#✓fully proved
Let \(t \ge 2\), let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type, and let \(x\) be a key. If \(x\) occurs in the inorder flattening of \(T\), the flattening of the tree obtained from \(T\) by deleting \(x\) (with minimum degree \(t\)) has length one less than the flattening of \(T\); otherwise the two flattenings have the same length.
public theorem flatten_length_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t)
{x : α} {tree : BTree α} (h : IsBTree t tree) :
(flatten (delete t x tree)).length =
if x ∈ flatten tree then (flatten tree).length - 1
else (flatten tree).lengthpublic inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 5
TheoremRepeated top-down deletion#✓fully proved
Let \(t \ge 2\) and let \(T\) be a B-tree of minimum degree \(t\) over a linearly ordered key type. For every key \(x\), deleting \(x\) from \(T\) twice with minimum degree \(t\) gives a tree with the same inorder flattening as deleting \(x\) from \(T\) once.
public theorem flatten_delete_delete [LinearOrder α] {t : Nat} (ht : 2 ≤ t)
{x : α} {tree : BTree α} (h : IsBTree t tree) :
flatten (delete t x (delete t x tree)) =
flatten (delete t x tree)public inductive BTree (α : Type u) where
| leaf (keys : List α) : BTree α
| node (keys : List α) (children : List (BTree α)) : BTree αCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:61
public def IsBTree [LT α] (t : Nat) (tree : BTree α) : Prop :=
2 ≤ t ∧ Ordered tree ∧ ∃ height, ValidRoot t height treeCSLibExt/Algorithms/Lean/DataStructures/BTree.lean:1129
public def flatten (tree : BTree α) : List α :=
flattenAux tree []CSLibExt/Algorithms/Lean/DataStructures/BTree.lean:97
public def delete [LinearOrder α] (t : Nat) (x : α) (tree : BTree α) :
BTree α :=
match delH (treeHeight tree) t x tree with
| .node [] [child] => child
| other => otherCSLibExt/Algorithms/Lean/DataStructures/BTree/DeleteBalanced.lean:263
Uses 8
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.