Splay tree

DefinitionRoot key of a splay tree#✓fully proved

The optional root key of a binary tree is undefined (none) for the empty tree, and is the key \(k\) for a tree whose root node holds \(k\).

public def root? {α : Type u} : BinaryTree α → Option α
  | .nil => none
  | .node key _ _ => some key

Used by 4

Used bySplay-tree access · Correctness of the splay-tree membership test · Splay-tree insertion puts the inserted key at the root · Root key after splaying a present key

DefinitionSplay operation#✓fully proved

Let \(\alpha\) be a linearly ordered type and write \((k; L, R)\) for the binary tree with root key \(k\), left subtree \(L\) and right subtree \(R\). For \(x \in \alpha\), the splay \(S_x(t)\) of a binary tree \(t\) with keys in \(\alpha\) is defined by recursion on \(t\). The empty tree splays to itself, and \(t = (k; L, R)\) is left unchanged if \(x = k\), if \(x < k\) and \(L\) is empty, or if \(x > k\) and \(R\) is empty. If \(x < k\) and \(L = (a; A, B)\), then: if \(x = a\), the result is the zig \((a; A, (k; B, R))\); if \(x < a\) and \(S_x(A) = (d; A_1, A_2)\), the result is the zig-zig \((d; A_1, (a; A_2, (k; B, R)))\); if \(x > a\) and \(S_x(B) = (d; B_1, B_2)\), the result is the zig-zag \((d; (a; A, B_1), (k; B_2, R))\); and if the splayed subtree \(S_x(A)\), respectively \(S_x(B)\), is empty, the result is the zig \((a; A, (k; B, R))\). The case \(x > k\) with \(R = (b; C, D)\) is the mirror image: if \(x = b\), the result is the zig \((b; (k; L, C), D)\); if \(x > b\) and \(S_x(D) = (d; D_1, D_2)\), it is the zig-zig \((d; (b; (k; L, C), D_1), D_2)\); if \(x < b\) and \(S_x(C) = (d; C_1, C_2)\), it is the zig-zag \((d; (k; L, C_1), (b; C_2, D))\); and if the splayed subtree is empty, it is the zig \((b; (k; L, C), D)\).

The search path for \(x\) runs from the root to the node with key \(x\), or to the last node visited if \(x\) is absent. Each recursive step consumes two edges of this path, starting at the root, so when the path has an odd number of edges the single rotation is performed on its last edge, the one farthest from the root.

Cslib.Algorithms.Lean.SplayTree.splay · 37 lines

public def splay {α : Type u} [LinearOrder α] (x : α) :
    BinaryTree α → BinaryTree α
  | .nil => .nil
  | .node k l r =>
      if x = k then .node k l r
      else if x < k then
        match l with
        | .nil => .node k l r
        | .node lk ll lr =>
            if x = lk then
              .node lk ll (.node k lr r)
            else if x < lk then
              match splay x ll with
              | .nil => .node lk ll (.node k lr r)
              | .node d lll llr =>
                  .node d lll (.node lk llr (.node k lr r))
            else
              match splay x lr with
              | .nil => .node lk ll (.node k lr r)
              | .node d lrl lrr =>
                  .node d (.node lk ll lrl) (.node k lrr r)
      else
        match r with
        | .nil => .node k l r
        | .node rk rl rr =>
            if x = rk then
              .node rk (.node k l rl) rr
            else if rk < x then
              match splay x rr with
              | .nil => .node rk (.node k l rl) rr
              | .node d rrl rrr =>
                  .node d (.node rk (.node k l rl) rrl) rrr
            else
              match splay x rl with
              | .nil => .node rk (.node k l rl) rr
              | .node d rll rlr =>
                  .node d (.node k l rll) (.node rk rlr rr)

Used by 14

Used bySplay-tree access · The tree returned by a splay-tree access · Correctness of the splay-tree membership test · Splaying preserves the inorder traversal · Splay-tree insertion · Keys after splay-tree insertion · Splaying preserves membership · Splaying preserves the number of nodes · Splay-tree insertion preserves the search-tree property · Splaying preserves the search-tree property · Splay-tree insertion puts the inserted key at the root · Splaying a present key brings it to the root · Root key after splaying a present key · Splaying the empty tree

TheoremSplaying the empty tree#✓fully proved

For every key \(x\) of a linearly ordered type, splaying \(x\) in the empty binary tree gives the empty tree.

@[simp] public theorem splay_nil {α : Type u} [LinearOrder α] (x : α) :
    splay x (.nil : BinaryTree α) = .nil

Uses 1

Statement usesSplay operation

TheoremSplaying preserves the inorder traversal#✓fully proved

For every key \(x\) and every binary tree \(t\) over a linearly ordered type, the inorder traversal of the tree obtained by splaying \(x\) in \(t\) equals the inorder traversal of \(t\). No search-tree ordering of \(t\) is assumed.

public theorem inorder_splay {α : Type u} [LinearOrder α] {x : α}
    (t : BinaryTree α) : inorder (splay x t) = inorder t

Uses 3 · Used by 3

Statement usesInorder traversal of a binary tree · Splay operation

Proof usesInorder traversal of a binary tree with an accumulator

Used bySplaying preserves membership · Splaying preserves the number of nodes · Splaying preserves the search-tree property

TheoremSplaying preserves membership#✓fully proved

For keys \(x\) and \(y\) and a binary tree \(t\) over a linearly ordered type, \(y\) is a key of the tree obtained by splaying \(x\) in \(t\) if and only if \(y\) is a key of \(t\).

public theorem mem_splay {α : Type u} [LinearOrder α] {x y : α}
    {t : BinaryTree α} : y ∈ splay x t ↔ y ∈ t

Uses 5 · Used by 2

Statement usesMembership in a binary tree · Splay operation

Proof usesInorder traversal of a binary tree · Membership in the inorder traversal of a binary tree · Splaying preserves the inorder traversal

Used byCorrectness of the splay-tree membership test · Keys after splay-tree insertion

TheoremSplaying preserves the number of nodes#✓fully proved

For every binary tree \(t\) with keys in a linearly ordered type and every key \(x\), the tree obtained by splaying \(x\) in \(t\) has the same number of nodes as \(t\).

public theorem numNodes_splay {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} : (splay x t).numNodes = t.numNodes

Uses 4

Statement usesSplay operation

Proof usesInorder traversal of a binary tree · The length of the inorder traversal of a binary tree is its number of nodes · Splaying preserves the inorder traversal

TheoremSplaying preserves the search-tree property#✓fully proved

Let \(t\) be a binary tree with keys in a linearly ordered type and let \(x\) be a key. If \(t\) is a binary search tree (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key of the node), then the tree obtained by splaying \(x\) in \(t\) is again a binary search tree.

public theorem ordered_splay {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (h : Ordered t) : Ordered (splay x t)

Uses 10 · Used by 1

Statement usesOrdered binary trees · Splay operation

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · 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 inorder traversal of an ordered binary tree is strictly increasing · Splaying preserves the inorder traversal

Used bySplay-tree insertion preserves the search-tree property

TheoremSplaying a present key brings it to the root#✓fully proved

Let \(t\) be a binary search tree with keys in a linearly ordered type (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key of the node), and let \(x\) be a key that occurs in \(t\). Then there are binary trees \(l\) and \(r\) such that splaying \(x\) in \(t\) gives the tree whose root holds \(x\), with left subtree \(l\) and right subtree \(r\).

public theorem root_splay_of_mem {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (hOrd : Ordered t) (hx : x ∈ t) :
    ∃ l r, splay x t = .node x l r

Uses 5 · Used by 1

Statement usesMembership in a binary tree · Ordered binary trees · Splay operation

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members

Used byRoot key after splaying a present key

TheoremRoot key after splaying a present key#✓fully proved

Let \(t\) be a binary search tree with keys in a linearly ordered type (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key of the node), and let \(x\) be a key that occurs in \(t\). Then the tree obtained by splaying \(x\) in \(t\) is nonempty and its root key is \(x\).

public theorem root?_splay_of_mem {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (hOrd : Ordered t) (hx : x ∈ t) :
    root? (splay x t) = some x

Uses 5 · Used by 1

Statement usesMembership in a binary tree · Ordered binary trees · Root key of a splay tree · Splay operation

Proof usesSplaying a present key brings it to the root

Used byCorrectness of the splay-tree membership test

DefinitionSearch-path split at a key#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(x \in \alpha\), and write \((k; L, R)\) for the binary tree with root key \(k\), left subtree \(L\) and right subtree \(R\). The split of a binary tree with keys in \(\alpha\) at \(x\) is the pair of trees defined by recursion: the empty tree splits into two empty trees; if \(x < k\) and \(L\) splits into \((L_1, L_2)\), then \((k; L, R)\) splits into \((L_1, (k; L_2, R))\); if \(k < x\) and \(R\) splits into \((R_1, R_2)\), then \((k; L, R)\) splits into \(((k; L, R_1), R_2)\); and if \(x = k\), then \((k; L, R)\) splits into \((L, R)\).

When the tree is a binary search tree (at every node, the keys of the left subtree are strictly smaller and those of the right subtree strictly larger than the node's key), the first part holds the keys below \(x\) and the second part the keys above \(x\); the key \(x\), if present, is dropped.

public def split {α : Type u} [LinearOrder α] (x : α) :
    BinaryTree α → BinaryTree α × BinaryTree α
  | .nil => (.nil, .nil)
  | .node k l r =>
      if x < k then
        match split x l with
        | (ll, lr) => (ll, .node k lr r)
      else if k < x then
        match split x r with
        | (rl, rr) => (.node k l rl, rr)
      else (l, r)

Used by 8

Used bySplitting an ordered tree separates the keys around the split key · Splay-tree insertion · Keys after splay-tree insertion · Splay-tree split parts contain only original keys · Keys other than the split key survive a split · Splay-tree insertion preserves the search-tree property · Both parts of a split search tree are search trees · Splay-tree insertion puts the inserted key at the root

TheoremSplay-tree split parts contain only original keys#✓fully proved

For keys \(x\) and \(y\) and a binary tree \(t\) over a linearly ordered type, if \(y\) is a key of the left part or of the right part of the split of \(t\) at \(x\), then \(y\) is a key of \(t\).

public theorem mem_of_mem_split {α : Type u} [LinearOrder α]
    {x y : α} {t : BinaryTree α} :
    y ∈ (split x t).1 ∨ y ∈ (split x t).2 → y ∈ t

Uses 2 · Used by 2

Statement usesMembership in a binary tree · Search-path split at a key

Used byKeys after splay-tree insertion · Both parts of a split search tree are search trees

TheoremKeys other than the split key survive a split#✓fully proved

Let \(t\) be a binary tree with keys in a linearly ordered type, and let \(x\) and \(y\) be keys with \(y \ne x\). If \(y\) occurs as a key of \(t\), then \(y\) occurs as a key of the left part or of the right part of the split of \(t\) at \(x\). The tree \(t\) need not be a binary search tree.

public theorem mem_split_of_mem {α : Type u} [LinearOrder α]
    {x y : α} {t : BinaryTree α} (h : y ∈ t) (hyx : y ≠ x) :
    y ∈ (split x t).1 ∨ y ∈ (split x t).2

Uses 2 · Used by 1

Statement usesMembership in a binary tree · Search-path split at a key

Used byKeys after splay-tree insertion

TheoremSplitting an ordered tree separates the keys around the split key#✓fully proved

Let \(t\) be an ordered binary tree over a linearly ordered type and let \(x\) be a key. When \(t\) is split at \(x\), every key of the left part is strictly less than \(x\) and every key of the right part is strictly greater than \(x\).

public theorem all_split {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (hOrd : Ordered t) :
    All (· < x) (split x t).1 ∧ All (x < ·) (split x t).2

Uses 5 · Used by 1

Statement usesA predicate holding at every key of a binary tree · Ordered binary trees · Search-path split at a key

Proof usesMembership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members

Used bySplay-tree insertion preserves the search-tree property

TheoremBoth parts of a split search tree are search trees#✓fully proved

Let \(t\) be a binary tree with keys in a linearly ordered type and let \(x\) be a key. If \(t\) is a binary search tree (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key of the node), then the left part and the right part of the split of \(t\) at \(x\) are both binary search trees.

public theorem ordered_split {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (hOrd : Ordered t) :
    Ordered (split x t).1 ∧ Ordered (split x t).2

Uses 6 · Used by 1

Statement usesOrdered binary trees · Search-path split at a key

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Splay-tree split parts contain only original keys

Used bySplay-tree insertion preserves the search-tree property

DefinitionSplay-tree insertion#✓fully proved

For a key \(x\) and a binary tree \(t\) over a linearly ordered type, inserting \(x\) into \(t\) splays \(x\) in \(t\), splits the resulting tree at \(x\) into a left part and a right part, and returns the tree whose root key is \(x\), whose left subtree is the left part and whose right subtree is the right part.

In an ordered tree that already contains \(x\), the key is splayed to the root and dropped by the split, so no duplicate is created.

public def insert {α : Type u} [LinearOrder α] (x : α)
    (t : BinaryTree α) : BinaryTree α :=
  let p := split x (splay x t)
  .node x p.1 p.2

Uses 2 · Used by 3

Statement usesSplay operation · Search-path split at a key

Used byKeys after splay-tree insertion · Splay-tree insertion preserves the search-tree property · Splay-tree insertion puts the inserted key at the root

DefinitionSplay-tree access#✓fully proved

For a key \(x\) and a binary tree \(t\) over a linearly ordered type, the access of \(x\) in \(t\) is the pair \((b, t')\), where \(t'\) is the tree obtained by splaying \(x\) in \(t\) and \(b\) is true exactly when \(t'\) is nonempty and its root key is \(x\).

public def access {α : Type u} [LinearOrder α] (x : α)
    (t : BinaryTree α) : Bool × BinaryTree α :=
  let t' := splay x t
  (decide (root? t' = some x), t')

Uses 2 · Used by 2

Statement usesRoot key of a splay tree · Splay operation

Used byThe tree returned by a splay-tree access · Splay-tree membership test

DefinitionSplay-tree membership test#✓fully proved

For a key \(x\) and a binary tree \(t\) over a linearly ordered type, the membership test of \(x\) in \(t\) is the Boolean component of the access of \(x\) in \(t\): it is true exactly when the tree obtained by splaying \(x\) in \(t\) is nonempty and its root key is \(x\).

public def contains {α : Type u} [LinearOrder α] (x : α)
    (t : BinaryTree α) : Bool :=
  (access x t).1

Uses 1 · Used by 1

Statement usesSplay-tree access

Used byCorrectness of the splay-tree membership test

TheoremThe tree returned by a splay-tree access#✓fully proved

For a key \(x\) and a binary tree \(t\) over a linearly ordered type, the tree component of the access of \(x\) in \(t\) is the tree obtained by splaying \(x\) in \(t\).

public theorem access_snd {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} : (access x t).2 = splay x t

Uses 2

Statement usesSplay-tree access · Splay operation

TheoremKeys after splay-tree insertion#✓fully proved

For keys \(x\) and \(y\) and a binary tree \(t\) over a linearly ordered type, \(y\) is a key of the tree obtained by splay-tree insertion of \(x\) into \(t\) if and only if \(y = x\) or \(y\) is a key of \(t\).

public theorem mem_insert {α : Type u} [LinearOrder α] {x y : α}
    {t : BinaryTree α} : y ∈ insert x t ↔ y = x ∨ y ∈ t

Uses 7

Statement usesMembership in a binary tree · Splay-tree insertion

Proof usesSplay-tree split parts contain only original keys · Splaying preserves membership · Keys other than the split key survive a split · Splay operation · Search-path split at a key

TheoremSplay-tree insertion preserves the search-tree property#✓fully proved

Let \(t\) be a binary tree with keys in a linearly ordered type and let \(x\) be a key. If \(t\) is a binary search tree (at every node, every key of the left subtree is strictly smaller and every key of the right subtree strictly larger than the key of the node), then the splay-tree insertion of \(x\) into \(t\) is again a binary search tree.

public theorem ordered_insert {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} (h : Ordered t) : Ordered (insert x t)

Uses 8

Statement usesOrdered binary trees · Splay-tree insertion

Proof usesA predicate holding at every key of a binary tree · Splitting an ordered tree separates the keys around the split key · Splaying preserves the search-tree property · Both parts of a split search tree are search trees · Splay operation · Search-path split at a key

TheoremSplay-tree insertion puts the inserted key at the root#✓fully proved

For every binary tree \(t\) with keys in a linearly ordered type and every key \(x\), the splay-tree insertion of \(x\) into \(t\) is a nonempty tree whose root key is \(x\).

public theorem root?_insert {α : Type u} [LinearOrder α] {x : α}
    {t : BinaryTree α} : root? (insert x t) = some x

Uses 4

Statement usesSplay-tree insertion · Root key of a splay tree

Proof usesSplay operation · Search-path split at a key

TheoremCorrectness of the splay-tree membership test#✓fully proved

For an ordered binary tree \(t\) over a linearly ordered type and a key \(x\), the splay-tree membership test of \(x\) in \(t\) returns true if and only if \(x\) is a key of \(t\).

public theorem contains_eq_true_iff {α : Type u} [LinearOrder α]
    {x : α} {t : BinaryTree α} (hOrd : Ordered t) :
    contains x t = true ↔ x ∈ t

Uses 7

Statement usesMembership in a binary tree · Ordered binary trees · Splay-tree membership test

Proof usesSplaying preserves membership · Root key of a splay tree · Root key after splaying a present key · Splay operation

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.