Order statistic tree

StructureOrder-statistic tree node entry#✓fully proved

A node entry of an order-statistic tree over a type \(\alpha\) consists of a key in \(\alpha\) and a natural number, the cached number of nodes in the subtree rooted at that node.

public structure Entry (α : Type u) where
  key : α
  subtreeSize : Nat
deriving DecidableEq, Repr

Used by 27

Used byCorrect size caches · Order-statistic deletion preserves cache correctness · Insertion preserves correct size caches · Order-statistic merge preserves cache correctness · The cache-computing node constructor preserves correct size caches · Cached root size · Correct caches give the tree size · Search in an order-statistic tree · Search in an ordered order-statistic tree is correct · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree · Insertion commutes with forgetting the size caches · Order-statistic tree built from a list · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Insertion into an order-statistic tree · Keys of an order-statistic tree after deletion · Keys of an order-statistic merge · Merging order-statistic trees · Order-statistic tree node with computed cache · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Rank in an order-statistic tree · Cached rank agrees with traversal rank · Select in an order-statistic tree · Cached select agrees with inorder select · Order-statistic tree

AbbreviationOrder-statistic tree#✓fully proved

An order-statistic tree with keys in a type \(\alpha\) is a binary tree, possibly empty, each of whose nodes carries a key in \(\alpha\) together with a natural number, meant as the cached number of nodes in the subtree rooted at that node. That these caches are correct is a separate condition.

public abbrev Tree (α : Type u) := BinaryTree (Entry α)

Uses 1 · Used by 37

Statement usesOrder-statistic tree node entry

Used byCorrect size caches · Order-statistic deletion preserves cache correctness · Insertion preserves correct size caches · Order-statistic merge preserves cache correctness · The cache-computing node constructor preserves correct size caches · Cached root size · Correct caches give the tree size · Search in an order-statistic tree · Search misses a key deleted from an order-statistic tree · Search in an ordered order-statistic tree is correct · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree · Insertion commutes with forgetting the size caches · Order-statistic tree built from a list · Inorder traversal of an order-statistic tree · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Insertion into an order-statistic tree · Keys of an order-statistic tree after deletion · Keys of an order-statistic tree built from a list · Keys of an order-statistic merge · Merging order-statistic trees · Order-statistic tree node with computed cache · Deleted key is absent from an order-statistic tree · Ordered order-statistic tree · Deletion preserves order in an order-statistic tree · Insertion preserves ordering of order-statistic trees · Merging separated ordered order-statistic trees preserves order · Rank in an order-statistic tree · Rank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Select in an order-statistic tree · Selection after deletion in an order-statistic tree · Cached select agrees with inorder select · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

DefinitionCached root size#✓fully proved

The cached root size of an order-statistic tree is the subtree size stored in the entry of its root node, and is \(0\) for the empty tree.

public def cachedSize {α : Type u} : Tree α → Nat
  | .nil => 0
  | .node entry _ _ => entry.subtreeSize

Uses 2 · Used by 7

Statement usesOrder-statistic tree node entry · Order-statistic tree

Used byThe cache-computing node constructor preserves correct size caches · Correct caches give the tree size · Order-statistic tree node with computed cache · Rank in an order-statistic tree · Cached rank agrees with traversal rank · Select in an order-statistic tree · Cached select agrees with inorder select

DefinitionErasing the size caches of an order-statistic tree#✓fully proved

The erasure of an order-statistic tree is the binary tree of the same shape whose node keys are the keys of the original nodes: the empty tree is sent to the empty tree, and a node is sent to the node with the same key whose left and right subtrees are the erasures of the original left and right subtrees, so every cached subtree size is dropped.

public def erase {α : Type u} : Tree α → BinaryTree α
  | .nil => .nil
  | .node entry left right => .node entry.key (erase left) (erase right)

Uses 2 · Used by 21

Statement usesOrder-statistic tree node entry · Order-statistic tree

Used bySearch misses a key deleted from an order-statistic tree · Search in an ordered order-statistic tree is correct · Insertion commutes with forgetting the size caches · Inorder traversal of an order-statistic tree · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Keys of an order-statistic tree after deletion · Keys of an order-statistic tree built from a list · Keys of an order-statistic merge · Deleted key is absent from an order-statistic tree · Ordered order-statistic tree · Deletion preserves order in an order-statistic tree · Insertion preserves ordering of order-statistic trees · Merging separated ordered order-statistic trees preserves order · Rank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Selection after deletion in an order-statistic tree · Cached select agrees with inorder select · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

DefinitionCorrect size caches#✓fully proved

An order-statistic tree has correct size caches when, at every node, the cached subtree size equals the number of nodes of the left subtree plus the number of nodes of the right subtree plus one, that is, the number of nodes of the subtree rooted at that node. The empty tree has correct size caches.

public def CacheCorrect {α : Type u} : Tree α → Prop
  | .nil => True
  | .node entry left right =>
      CacheCorrect left ∧ CacheCorrect right ∧
        entry.subtreeSize = left.numNodes + right.numNodes + 1

Uses 2 · Used by 13

Statement usesOrder-statistic tree node entry · Order-statistic tree

Used byOrder-statistic deletion preserves cache correctness · Order-statistic trees built from a list have correct size caches · Insertion preserves correct size caches · Order-statistic merge preserves cache correctness · The cache-computing node constructor preserves correct size caches · Correct caches give the tree size · Rank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Selection after deletion in an order-statistic tree · Cached select agrees with inorder select · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

DefinitionOrdered order-statistic tree#✓fully proved

An order-statistic tree over a type equipped with a relation \(<\) is ordered when the binary tree obtained by erasing its cached sizes is an ordered binary search tree: at every node, each key of the left subtree is \(<\) the node's key, the node's key is \(<\) each key of the right subtree, and both subtrees are ordered.

public def Ordered {α : Type u} [LT α] (tree : Tree α) : Prop :=
  BinarySearchTree.Ordered (erase tree)

Uses 3 · Used by 14

Statement usesOrdered binary trees · Order-statistic tree · Erasing the size caches of an order-statistic tree

Used bySearch misses a key deleted from an order-statistic tree · Search in an ordered order-statistic tree is correct · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Deleted key is absent from an order-statistic tree · Deletion preserves order in an order-statistic tree · Order-statistic trees built from lists are ordered · Insertion preserves ordering of order-statistic trees · Merging separated ordered order-statistic trees preserves order · Rank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

DefinitionInorder traversal of an order-statistic tree#✓fully proved

The inorder traversal of an order-statistic tree is the inorder traversal of the binary tree obtained by erasing its cached subtree sizes: the traversal of the left subtree, then the root key, then the traversal of the right subtree, and the empty list for the empty tree.

public def inorder {α : Type u} (tree : Tree α) : List α :=
  BinarySearchTree.inorder (erase tree)

Uses 3 · Used by 2

Statement usesInorder traversal of a binary tree · Order-statistic tree · Erasing the size caches of an order-statistic tree

Used byInorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge

DefinitionOrder-statistic tree node with computed cache#✓fully proved

Given a key \(k\) and order-statistic trees \(L\) and \(R\), the node built from them has key \(k\), left subtree \(L\), right subtree \(R\), and cached subtree size equal to the cached root size of \(L\) plus the cached root size of \(R\) plus one, where the empty tree has cached root size zero.

public def node {α : Type u} (key : α) (left right : Tree α) : Tree α :=
  .node { key, subtreeSize := cachedSize left + cachedSize right + 1 } left right

Uses 3 · Used by 11

Statement usesOrder-statistic tree node entry · Order-statistic tree · Cached root size

Used byOrder-statistic deletion preserves cache correctness · Insertion preserves correct size caches · Order-statistic merge preserves cache correctness · The cache-computing node constructor preserves correct size caches · Deletion from an order-statistic tree · Insertion commutes with forgetting the size caches · Inorder traversal after order-statistic deletion · Insertion into an order-statistic tree · Keys of an order-statistic tree after deletion · Merging order-statistic trees · Deletion preserves order in an order-statistic tree

DefinitionSearch in an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(q \in \alpha\). Searching for \(q\) in the empty tree returns false. At a node with key \(k\), the search continues in the left subtree if \(q < k\), continues in the right subtree if \(k < q\), and returns true otherwise.

public def contains {α : Type u} [LinearOrder α] (query : α) : Tree α → Bool
  | .nil => false
  | .node entry left right =>
      if query < entry.key then contains query left
      else if entry.key < query then contains query right
      else true

Uses 2 · Used by 2

Statement usesOrder-statistic tree node entry · Order-statistic tree

Used bySearch misses a key deleted from an order-statistic tree · Search in an ordered order-statistic tree is correct

DefinitionInsertion into an order-statistic tree#✓fully proved

Inserting a key \(k\) of a linearly ordered type into the empty tree gives a single node with key \(k\) and cached size \(1\). For a nonempty tree with root key \(r\): if \(k < r\), the key is inserted into the left subtree; if \(r < k\), it is inserted into the right subtree; in both cases the root is rebuilt with key \(r\) and cached size equal to the cached root sizes of its two subtrees plus one (an empty subtree counts as zero). Otherwise \(k = r\) and the tree is returned unchanged.

public def insert {α : Type u} [LinearOrder α] (key : α) : Tree α → Tree α
  | .nil => node key .nil .nil
  | tree@(.node entry left right) =>
      if key < entry.key then node entry.key (insert key left) right
      else if entry.key < key then node entry.key left (insert key right)
      else tree

Uses 3 · Used by 5

Statement usesOrder-statistic tree node entry · Order-statistic tree · Order-statistic tree node with computed cache

Used byInsertion preserves correct size caches · Insertion commutes with forgetting the size caches · Order-statistic tree built from a list · Keys of an order-statistic tree built from a list · Insertion preserves ordering of order-statistic trees

DefinitionOrder-statistic tree built from a list#✓fully proved

For a linearly ordered key type, the order-statistic tree built from a list of keys is obtained by inserting the keys into the empty tree from right to left: the empty list gives the empty tree, and a list with head \(k\) and tail \(l\) gives the insertion of \(k\) into the tree built from \(l\).

public def fromList {α : Type u} [LinearOrder α] : List α → Tree α
  | [] => .nil
  | key :: keys => insert key (fromList keys)

Uses 3 · Used by 3

Statement usesOrder-statistic tree node entry · Order-statistic tree · Insertion into an order-statistic tree

Used byOrder-statistic trees built from a list have correct size caches · Keys of an order-statistic tree built from a list · Order-statistic trees built from lists are ordered

DefinitionRank in an order-statistic tree#✓fully proved

For a key \(q\) of a linearly ordered type, the rank of \(q\) in an order-statistic tree is computed by descending from the root. It is \(0\) for the empty tree. At a node with key \(k\), left subtree \(L\) and right subtree \(R\), it is the rank of \(q\) in \(L\) if \(q < k\); it is \(s(L) + 1\) plus the rank of \(q\) in \(R\) if \(k < q\); and it is \(s(L)\) if \(q = k\). Here \(s(L)\) is the subtree size cached at the root of \(L\), and \(0\) if \(L\) is empty.

When the cached sizes are correct and the tree is ordered, this is the number of keys in the tree strictly smaller than \(q\).

public def rank {α : Type u} [LinearOrder α] (query : α) : Tree α → Nat
  | .nil => 0
  | .node entry left right =>
      if query < entry.key then rank query left
      else if entry.key < query then cachedSize left + 1 + rank query right
      else cachedSize left

Uses 3 · Used by 5

Statement usesOrder-statistic tree node entry · Order-statistic tree · Cached root size

Used byRank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

DefinitionSelect in an order-statistic tree#✓fully proved

For an order-statistic tree \(T\) and a natural number \(i\), select at index \(i\) in \(T\) is computed by descending from the root. It returns nothing for the empty tree. At a node with key \(k\), left subtree \(L\) and right subtree \(R\), it is select at index \(i\) in \(L\) if \(i < s(L)\); it returns \(k\) if \(i = s(L)\); and it is select at index \(i - s(L) - 1\) in \(R\) if \(i > s(L)\). Here \(s(L)\) is the subtree size cached at the root of \(L\), and \(0\) if \(L\) is empty.

When the cached sizes are correct, this returns the key at zero-based position \(i\) of the inorder traversal, and nothing if \(T\) has at most \(i\) nodes.

public def select {α : Type u} : Tree α → Nat → Option α
  | .nil, _ => none
  | .node entry left right, index =>
      if index < cachedSize left then select left index
      else if index = cachedSize left then some entry.key
      else select right (index - cachedSize left - 1)

Uses 3 · Used by 5

Statement usesOrder-statistic tree node entry · Order-statistic tree · Cached root size

Used byRank inverts select in an order-statistic tree · Selection after deletion in an order-statistic tree · Cached select agrees with inorder select · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion

TheoremCorrect caches give the tree size#✓fully proved

If an order-statistic tree \(T\) has correct cached subtree sizes at every node, then the cached root size of \(T\) (zero for the empty tree) equals the number of nodes of \(T\).

public theorem cachedSize_eq_numNodes {α : Type u} {tree : Tree α}
    (hTree : CacheCorrect tree) : cachedSize tree = tree.numNodes

Uses 4 · Used by 3

Statement usesCorrect size caches · Order-statistic tree node entry · Order-statistic tree · Cached root size

Used byThe cache-computing node constructor preserves correct size caches · Cached rank agrees with traversal rank · Cached select agrees with inorder select

TheoremThe cache-computing node constructor preserves correct size caches#✓fully proved

Let \(k\) be a key and let \(L\) and \(R\) be order-statistic trees whose cached subtree sizes are correct at every node. Then the node with key \(k\), left subtree \(L\) and right subtree \(R\), whose root cache is the cached root size of \(L\) plus the cached root size of \(R\) plus one, also has correct cached subtree sizes at every node.

public theorem cacheCorrect_node {α : Type u} {key : α} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    CacheCorrect (node key left right)

Uses 6 · Used by 3

Statement usesCorrect size caches · Order-statistic tree · Order-statistic tree node with computed cache

Proof usesOrder-statistic tree node entry · Cached root size · Correct caches give the tree size

Used byOrder-statistic deletion preserves cache correctness · Insertion preserves correct size caches · Order-statistic merge preserves cache correctness

TheoremInsertion commutes with forgetting the size caches#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) and \(T\) an order-statistic tree over \(\alpha\). Forgetting the cached sizes of the tree obtained by inserting \(k\) into \(T\) gives the same binary tree as inserting \(k\), by ordinary binary-search-tree insertion, into \(T\) with its cached sizes forgotten.

public theorem erase_insert {α : Type u} [LinearOrder α] (key : α) (tree : Tree α) :
    erase (insert key tree) = BinarySearchTree.insert key (erase tree)

Uses 6 · Used by 2

Statement usesInsertion into a binary search tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Insertion into an order-statistic tree

Proof usesOrder-statistic tree node entry · Order-statistic tree node with computed cache

Used byKeys of an order-statistic tree built from a list · Insertion preserves ordering of order-statistic trees

TheoremInsertion preserves correct size caches#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(k \in \alpha\), and let \(T\) be an order-statistic tree over \(\alpha\) whose cached subtree sizes are correct at every node. Then the tree obtained by inserting \(k\) into \(T\) also has correct cached subtree sizes at every node.

public theorem cacheCorrect_insert {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hTree : CacheCorrect tree) : CacheCorrect (insert key tree)

Uses 6 · Used by 1

Statement usesCorrect size caches · Order-statistic tree · Insertion into an order-statistic tree

Proof usesOrder-statistic tree node entry · The cache-computing node constructor preserves correct size caches · Order-statistic tree node with computed cache

Used byOrder-statistic trees built from a list have correct size caches

TheoremInsertion preserves ordering of order-statistic trees#✓fully proved

Let \(T\) be an order-statistic tree over a linearly ordered key type that is ordered, meaning that after its cached sizes are erased, at every node each key of the left subtree is strictly smaller than the node's key and each key of the right subtree is strictly larger. Then for every key \(k\), the tree obtained by inserting \(k\) into \(T\) is again ordered.

public theorem ordered_insert {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hTree : Ordered tree) : Ordered (insert key tree)

Uses 8 · Used by 1

Statement usesOrdered order-statistic tree · Order-statistic tree · Insertion into an order-statistic tree

Proof usesOrdered binary trees · Insertion into a binary search tree · Binary search tree insertion preserves order · Erasing the size caches of an order-statistic tree · Insertion commutes with forgetting the size caches

Used byOrder-statistic trees built from lists are ordered

TheoremOrder-statistic trees built from a list have correct size caches#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every list \(\ell\) of elements of \(\alpha\), the order-statistic tree obtained by inserting the elements of \(\ell\) into the empty tree, from right to left, has correct cached subtree sizes at every node.

public theorem cacheCorrect_fromList {α : Type u} [LinearOrder α] {keys : List α} :
    CacheCorrect (fromList keys)

Uses 3

Statement usesCorrect size caches · Order-statistic tree built from a list

Proof usesInsertion preserves correct size caches

TheoremOrder-statistic trees built from lists are ordered#✓fully proved

For every list \(l\) of keys from a linearly ordered type, the order-statistic tree built from \(l\) by successive insertion is ordered: after its cached sizes are erased, at every node each key of the left subtree is strictly smaller than the node's key and each key of the right subtree is strictly larger.

public theorem ordered_fromList {α : Type u} [LinearOrder α] {keys : List α} :
    Ordered (fromList keys)

Uses 3

Statement usesOrdered order-statistic tree · Order-statistic tree built from a list

Proof usesInsertion preserves ordering of order-statistic trees

TheoremKeys of an order-statistic tree built from a list#✓fully proved

For a linearly ordered key type, a key \(k\) and a list \(l\) of keys, \(k\) is a key of some node of the order-statistic tree built from \(l\) by successive insertion if and only if \(k\) occurs in \(l\).

public theorem mem_fromList {α : Type u} [LinearOrder α] {key : α} {keys : List α} :
    key ∈ fromList keys ↔ key ∈ keys

Uses 9

Statement usesMembership in a binary tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Order-statistic tree built from a list

Proof usesBinary search tree built from a list · Insertion into a binary search tree · Members of the binary search tree built from a list · Insertion commutes with forgetting the size caches · Insertion into an order-statistic tree

TheoremSearch in an ordered order-statistic tree is correct#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(T\) an order-statistic tree over \(\alpha\) that is ordered: after forgetting the cached sizes, at every node all keys in the left subtree are smaller than the node's key and all keys in the right subtree are larger. Then for every \(q \in \alpha\), comparison search for \(q\) in \(T\) returns true if and only if \(q\) is the key of some node of \(T\).

public theorem contains_eq_true_iff {α : Type u} [LinearOrder α] {query : α}
    {tree : Tree α} (hTree : Ordered tree) : contains query tree = true ↔ query ∈ tree

Uses 8 · Used by 1

Statement usesMembership in a binary tree · Ordered order-statistic tree · Order-statistic tree · Search in an order-statistic tree · Erasing the size caches of an order-statistic tree

Proof usesSearch in a binary search tree · Search in a binary search tree is correct · Order-statistic tree node entry

Used bySearch misses a key deleted from an order-statistic tree

TheoremCached rank agrees with traversal rank#✓fully proved

Let \(T\) be an order-statistic tree over a linearly ordered key type whose cached subtree sizes are correct at every node and which is ordered. Then for every query \(q\), the rank of \(q\) computed by descending \(T\) with cached left-subtree sizes equals the number of entries strictly smaller than \(q\) in the inorder traversal of the binary tree obtained by erasing the caches of \(T\).

public theorem rank_eq_bstRank {α : Type u} [LinearOrder α] {query : α}
    {tree : Tree α} (hCache : CacheCorrect tree) (hTree : Ordered tree) :
    rank query tree = BinarySearchTree.rank query (erase tree)

Uses 17 · Used by 3

Statement usesRank of a key in a binary tree · Correct size caches · Ordered order-statistic tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Rank in an order-statistic tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · The length of the inorder traversal of a binary tree is its number of nodes · Order-statistic tree node entry · Cached root size · Correct caches give the tree size

Used byRank after deletion in an order-statistic tree · Rank inverts select in an order-statistic tree · Select inverts rank in an order-statistic tree

TheoremCached select agrees with inorder select#✓fully proved

For every order-statistic tree \(T\) whose cached subtree sizes are correct and every natural number \(i\), select at index \(i\) in \(T\) (descending with the cached sizes) returns the same result as taking the element at zero-based position \(i\) of the inorder traversal of the binary tree obtained from \(T\) by erasing the cached sizes; in particular both return nothing when that position does not exist.

public theorem select_eq_bstSelect {α : Type u} {tree : Tree α}
    (hCache : CacheCorrect tree) (index : Nat) :
    select tree index = BinarySearchTree.select (erase tree) index

Uses 11 · Used by 3

Statement usesInorder selection in a binary tree · Correct size caches · Order-statistic tree · Erasing the size caches of an order-statistic tree · Select in an order-statistic tree

Proof usesInorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · The length of the inorder traversal of a binary tree is its number of nodes · Order-statistic tree node entry · Cached root size · Correct caches give the tree size

Used byRank inverts select in an order-statistic tree · Selection after deletion in an order-statistic tree · Select inverts rank in an order-statistic tree

TheoremSelect inverts rank in an order-statistic tree#✓fully proved

Let \(T\) be an order-statistic tree over a linearly ordered type whose cached subtree sizes are correct and which satisfies the binary-search-tree ordering. For every key \(k\) in \(T\), select in \(T\) at the index equal to the rank of \(k\) in \(T\) returns \(k\).

public theorem select_rank {α : Type u} [LinearOrder α] {key : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hTree : Ordered tree) (hKey : key ∈ tree) :
    select tree (rank key tree) = some key

Uses 12 · Used by 1

Statement usesMembership in a binary tree · Correct size caches · Ordered order-statistic tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Rank in an order-statistic tree · Select in an order-statistic tree

Proof usesRank of a key in a binary tree · Inorder selection in a binary tree · Selecting the rank of a key returns the key · Cached rank agrees with traversal rank · Cached select agrees with inorder select

Used bySelecting the rank of a surviving key after deletion

TheoremRank inverts select in an order-statistic tree#✓fully proved

Let \(T\) be an order-statistic tree over a linearly ordered type whose cached subtree sizes are correct and which satisfies the binary-search-tree ordering. If select at zero-based index \(i\) in \(T\) returns a key \(k\), then the rank of \(k\) in \(T\) equals \(i\).

public theorem rank_select {α : Type u} [LinearOrder α] {tree : Tree α}
    (hCache : CacheCorrect tree) (hTree : Ordered tree) {index : Nat} {key : α}
    (hSelect : select tree index = some key) : rank key tree = index

Uses 11

Statement usesCorrect size caches · Ordered order-statistic tree · Order-statistic tree · Rank in an order-statistic tree · Select in an order-statistic tree

Proof usesRank of a key in a binary tree · The rank of a selected key is its index · Inorder selection in a binary tree · Erasing the size caches of an order-statistic tree · Cached rank agrees with traversal rank · Cached select agrees with inorder select

DefinitionMerging order-statistic trees#✓fully proved

The merge of order-statistic trees \(A\) and \(B\) is defined by recursion on \(A\). If \(A\) is empty, it is \(B\). If \(A\) has root key \(x\), left subtree \(L\) and right subtree \(R\), it is the node with key \(x\), left subtree \(L\) and right subtree the merge of \(R\) and \(B\), whose cached size is the sum of the cached root sizes of its children plus one, an empty child counting as zero. Thus \(B\) is attached below the rightmost path of \(A\), and every node on that path gets a recomputed cache.

The merge is intended for trees in which every key of \(A\) is smaller than every key of \(B\), but it is defined for all pairs of trees.

public def merge {α : Type u} : Tree α → Tree α → Tree α
  | .nil, right => right
  | .node entry left right, other => node entry.key left (merge right other)

Uses 3 · Used by 9

Statement usesOrder-statistic tree node entry · Order-statistic tree · Order-statistic tree node with computed cache

Used byOrder-statistic deletion preserves cache correctness · Order-statistic merge preserves cache correctness · Deletion from an order-statistic tree · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Keys of an order-statistic tree after deletion · Keys of an order-statistic merge · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order

DefinitionDeletion from an order-statistic tree#✓fully proved

Deleting a key \(k\) from an order-statistic tree over a linearly ordered type follows the comparison path from the root. The empty tree stays empty. At a node with key \(x\), left subtree \(L\) and right subtree \(R\): if \(k < x\), the result is the node with key \(x\), left subtree the deletion of \(k\) from \(L\) and right subtree \(R\); if \(x < k\), it is the node with key \(x\), left subtree \(L\) and right subtree the deletion of \(k\) from \(R\); otherwise (\(k = x\)) it is the merge of \(L\) and \(R\). Each rebuilt node gets as cached size the sum of the cached root sizes of its children plus one, an empty child counting as zero.

If \(k\) does not occur in the tree, the result has the same keys.

public def delete {α : Type u} [LinearOrder α] (key : α) : Tree α → Tree α
  | .nil => .nil
  | .node entry left right =>
      if key < entry.key then node entry.key (delete key left) right
      else if entry.key < key then node entry.key left (delete key right)
      else merge left right

Uses 4 · Used by 9

Statement usesOrder-statistic tree node entry · Order-statistic tree · Merging order-statistic trees · Order-statistic tree node with computed cache

Used byOrder-statistic deletion preserves cache correctness · Search misses a key deleted from an order-statistic tree · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Deleted key is absent from an order-statistic tree · Deletion preserves order in an order-statistic tree · Rank after deletion in an order-statistic tree · Selection after deletion in an order-statistic tree · Selecting the rank of a surviving key after deletion

TheoremOrder-statistic merge preserves cache correctness#✓fully proved

Let \(A\) and \(B\) be order-statistic trees whose cached subtree size at every node equals the number of nodes in that node's subtree. Then the merge of \(A\) and \(B\) has the same property. No ordering between the keys of \(A\) and \(B\) is assumed.

public theorem cacheCorrect_merge {α : Type u} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    CacheCorrect (merge left right)

Uses 6 · Used by 1

Statement usesCorrect size caches · Order-statistic tree · Merging order-statistic trees

Proof usesOrder-statistic tree node entry · The cache-computing node constructor preserves correct size caches · Order-statistic tree node with computed cache

Used byOrder-statistic deletion preserves cache correctness

TheoremOrder-statistic deletion preserves cache correctness#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) a key and \(T\) an order-statistic tree over \(\alpha\). If the cached subtree size at every node of \(T\) equals the number of nodes in that node's subtree, then the same holds for the tree obtained by deleting \(k\) from \(T\).

public theorem cacheCorrect_delete {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hTree : CacheCorrect tree) : CacheCorrect (delete key tree)

Uses 8 · Used by 3

Statement usesCorrect size caches · Order-statistic tree · Deletion from an order-statistic tree

Proof usesOrder-statistic tree node entry · Order-statistic merge preserves cache correctness · The cache-computing node constructor preserves correct size caches · Merging order-statistic trees · Order-statistic tree node with computed cache

Used byRank after deletion in an order-statistic tree · Selection after deletion in an order-statistic tree · Selecting the rank of a surviving key after deletion

TheoremMerging separated ordered order-statistic trees preserves order#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(L\) and \(R\) be ordered order-statistic trees over \(\alpha\) such that \(x < y\) for every key \(x\) of \(L\) and every key \(y\) of \(R\). Then the merge of \(L\) and \(R\) is ordered.

public theorem ordered_merge {α : Type u} [LinearOrder α] {left right : Tree α}
    (hLeft : Ordered left) (hRight : Ordered right)
    (hSeparated : ∀ x ∈ left, ∀ y ∈ right, x < y) : Ordered (merge left right)

Uses 12

Statement usesMembership in a binary tree · Ordered order-statistic tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Merging order-statistic trees

Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · Order-statistic tree node entry

TheoremDeletion preserves order in an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(T\) be an order-statistic tree over \(\alpha\) that is ordered, that is, after its cached sizes are removed, every key in a left subtree is strictly smaller than the key of its node and every key in a right subtree is strictly larger. Then for every key \(k\), the tree obtained from \(T\) by deleting \(k\) is again ordered.

public theorem ordered_delete {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hTree : Ordered tree) : Ordered (delete key tree)

Uses 14 · Used by 3

Statement usesOrdered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · Order-statistic tree node entry · Erasing the size caches of an order-statistic tree · Merging order-statistic trees · Order-statistic tree node with computed cache

Used bySearch misses a key deleted from an order-statistic tree · Rank after deletion in an order-statistic tree · Selecting the rank of a surviving key after deletion

TheoremInorder traversal of an order-statistic merge#✓fully proved

For order-statistic trees \(A\) and \(B\), the inorder traversal of the merge of \(A\) and \(B\) is the inorder traversal of \(A\) followed by the inorder traversal of \(B\). No ordering between the keys of \(A\) and \(B\) is assumed.

public theorem inorder_merge {α : Type u} {left right : Tree α} :
    inorder (merge left right) = inorder left ++ inorder right

Uses 7

Statement usesOrder-statistic tree · Inorder traversal of an order-statistic tree · Merging order-statistic trees

Proof usesInorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Order-statistic tree node entry · Erasing the size caches of an order-statistic tree

TheoremKeys of an order-statistic merge#✓fully proved

For order-statistic trees \(A\) and \(B\) over a type \(\alpha\) and any \(x \in \alpha\), \(x\) is a key of the merge of \(A\) and \(B\) if and only if \(x\) is a key of \(A\) or a key of \(B\). No ordering between the keys of \(A\) and \(B\) is assumed.

public theorem mem_merge {α : Type u} {x : α} {left right : Tree α} :
    x ∈ merge left right ↔ x ∈ left ∨ x ∈ right

Uses 8

Statement usesMembership in a binary tree · Order-statistic tree · Erasing the size caches of an order-statistic tree · Merging order-statistic trees

Proof usesInorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · Order-statistic tree node entry

TheoremInorder traversal after order-statistic deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) and \(T\) an ordered order-statistic tree over \(\alpha\) (at every node, all keys of the left subtree are smaller and all keys of the right subtree are larger than the node's key). The inorder traversal of the tree obtained by deleting \(k\) from \(T\) is the inorder traversal of \(T\) with every occurrence of \(k\) removed.

public theorem inorder_delete {α : Type u} [LinearOrder α] {key : α} {tree : Tree α}
    (hTree : Ordered tree) :
    inorder (delete key tree) = (inorder tree).filter (· ≠ key)

Uses 15

Statement usesOrdered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree · Inorder traversal of an order-statistic tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · Order-statistic tree node entry · Erasing the size caches of an order-statistic tree · Merging order-statistic trees · Order-statistic tree node with computed cache

TheoremKeys of an order-statistic tree after deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) and \(T\) an ordered order-statistic tree over \(\alpha\) (at every node, all keys of the left subtree are smaller and all keys of the right subtree are larger than the node's key). For every \(y \in \alpha\), \(y\) is a key of the tree obtained by deleting \(k\) from \(T\) if and only if \(y\) is a key of \(T\) and \(y \ne k\).

public theorem mem_delete_iff {α : Type u} [LinearOrder α] {key y : α} {tree : Tree α}
    (hTree : Ordered tree) : y ∈ delete key tree ↔ y ∈ tree ∧ y ≠ key

Uses 14 · Used by 1

Statement usesMembership in a binary tree · Ordered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree

Proof usesA predicate holding at every key of a binary tree · Ordered binary trees · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree · Order-statistic tree node entry · Merging order-statistic trees · Order-statistic tree node with computed cache

Used byDeleted key is absent from an order-statistic tree

TheoremDeleted key is absent from an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) and \(T\) an ordered order-statistic tree over \(\alpha\) (at every node, all keys of the left subtree are smaller and all keys of the right subtree are larger than the node's key). Then \(k\) is not a key of the tree obtained by deleting \(k\) from \(T\).

public theorem not_mem_delete {α : Type u} [LinearOrder α] {key : α} {tree : Tree α}
    (hTree : Ordered tree) : key ∉ delete key tree

Uses 6 · Used by 1

Statement usesMembership in a binary tree · Ordered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree

Proof usesKeys of an order-statistic tree after deletion

Used bySearch misses a key deleted from an order-statistic tree

TheoremSearch misses a key deleted from an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \alpha\) and \(T\) an ordered order-statistic tree over \(\alpha\) (at every node, all keys of the left subtree are smaller and all keys of the right subtree are larger than the node's key). Comparison search for \(k\) in the tree obtained by deleting \(k\) from \(T\) returns false.

public theorem contains_delete_self {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hTree : Ordered tree) :
    contains key (delete key tree) = false

Uses 9

Statement usesOrdered order-statistic tree · Order-statistic tree · Search in an order-statistic tree · Deletion from an order-statistic tree

Proof usesMembership in a binary tree · Search in an ordered order-statistic tree is correct · Erasing the size caches of an order-statistic tree · Deleted key is absent from an order-statistic tree · Deletion preserves order in an order-statistic tree

TheoremRank after deletion in an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(T\) be an order-statistic tree over \(\alpha\) that is ordered and whose cached subtree sizes are correct. Let \(k\) and \(q\) be keys and let \(T'\) be the tree obtained from \(T\) by deleting \(k\). Then the rank of \(q\) in \(T'\), computed by navigation with cached sizes, equals the number of entries strictly smaller than \(q\) in the inorder traversal of \(T'\) with its cached sizes removed.

public theorem rank_delete_eq_bstRank {α : Type u} [LinearOrder α] {key query : α}
    {tree : Tree α} (hCache : CacheCorrect tree) (hTree : Ordered tree) :
    rank query (delete key tree) =
      BinarySearchTree.rank query (erase (delete key tree))

Uses 10

Statement usesRank of a key in a binary tree · Correct size caches · Ordered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree · Rank in an order-statistic tree

Proof usesOrder-statistic deletion preserves cache correctness · Deletion preserves order in an order-statistic tree · Cached rank agrees with traversal rank

TheoremSelection after deletion in an order-statistic tree#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(T\) be an order-statistic tree over \(\alpha\) whose cached subtree sizes are correct. Let \(k\) be a key and let \(T'\) be the tree obtained from \(T\) by deleting \(k\). Then for every natural number \(i\), selecting position \(i\) in \(T'\) by navigation with cached sizes returns the entry at zero-based position \(i\) of the inorder traversal of \(T'\) with its cached sizes removed, and returns nothing when that traversal has at most \(i\) entries.

public theorem select_delete_eq_bstSelect {α : Type u} [LinearOrder α] {key : α}
    {tree : Tree α} (hCache : CacheCorrect tree) (index : Nat) :
    select (delete key tree) index =
      BinarySearchTree.select (erase (delete key tree)) index

Uses 8

Statement usesInorder selection in a binary tree · Correct size caches · Order-statistic tree · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree · Select in an order-statistic tree

Proof usesOrder-statistic deletion preserves cache correctness · Cached select agrees with inorder select

TheoremSelecting the rank of a surviving key after deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(T\) be an order-statistic tree over \(\alpha\) that is ordered and whose cached subtree sizes are correct, let \(k\) be a key, and let \(T'\) be the tree obtained from \(T\) by deleting \(k\). If \(y\) is a key of \(T'\), then selecting, with cached sizes, the position in \(T'\) given by the cached rank of \(y\) in \(T'\) returns \(y\).

public theorem select_rank_delete {α : Type u} [LinearOrder α] {key y : α}
    {tree : Tree α} (hCache : CacheCorrect tree) (hTree : Ordered tree)
    (hy : y ∈ delete key tree) :
    select (delete key tree) (rank y (delete key tree)) = some y

Uses 11

Statement usesMembership in a binary tree · Correct size caches · Ordered order-statistic tree · Order-statistic tree · Deletion from an order-statistic tree · Erasing the size caches of an order-statistic tree · Rank in an order-statistic tree · Select in an order-statistic tree

Proof usesOrder-statistic deletion preserves cache correctness · Deletion preserves order in an order-statistic tree · Select inverts rank in an order-statistic tree

41 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.