AVL tree

InductiveBinary trees with cached heights#✓fully proved

For a type \(\alpha\), a tree with cached heights over \(\alpha\) (the underlying type of AVL trees) is either empty, or a node made of a natural number \(h\) (its cached height), a left subtree, a key in \(\alpha\) and a right subtree.

The type does not require \(h\) to equal the actual height of the node.

public inductive Tree (α : Type u) where
  | empty : Tree α
  | node (height : Nat) (left : Tree α) (key : α) (right : Tree α) : Tree α
deriving DecidableEq, Repr

Used by 73

Used byEvery key of an AVL tree satisfies a predicate · The all-keys predicate in terms of membership (AVL trees) · Keys left after removing the minimum exceed it · The all-keys predicate is unchanged by erasing height caches · AVL rebalancing · Rebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL balance invariant · AVL rebalancing yields a balanced tree · Deleting a key preserves AVL balance · Minimum deletion preserves AVL balance · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL insertion preserves balance · The AVL node constructor preserves balance · Correct cached heights · AVL rebalancing preserves cached heights · Deleting a key keeps cached heights correct · Minimum deletion keeps cached heights correct · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · AVL insertion preserves cached heights · The AVL node constructor preserves cached heights · Membership search in an AVL tree · Correctness of AVL search · AVL tree deletion under its alternative name · Minimum deletion in an AVL tree · AVL tree deletion · Removing the leftmost key of an AVL tree · Building an AVL tree from a list · Cached height of an AVL tree · Upper bound on height after AVL rebalancing · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Upper bound on height after AVL insertion · Inorder traversal of an AVL tree · Inorder traversal of an AVL tree onto a suffix · AVL rebalancing preserves the inorder traversal · Inorder traversal after AVL deletion, alternative name · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · The inorder traversal of an ordered AVL tree has no duplicates · AVL inorder traversal agrees with the erased binary search tree · Insertion into an AVL tree · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height · Membership in an AVL tree · Membership after AVL rebalancing · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership in an AVL tree built from a list · Membership in the inorder traversal of an AVL tree · Membership after insertion into an AVL tree · AVL membership is membership in the underlying binary tree · Leftmost key of a tree · The leftmost key lies in the tree · AVL node with computed height · Deletion removes the deleted key from an ordered AVL tree · Ordered AVL trees · Rebalancing an AVL node preserves the search-tree order · Deleting a key from an ordered AVL tree keeps it ordered · Successor-step minimum removal preserves search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · The inorder traversal of an ordered AVL tree is strictly increasing · AVL insertion preserves the search-tree order · Order of an AVL tree via its underlying binary tree · Erasing the cached heights of an AVL tree

DefinitionCached height of an AVL tree#✓fully proved

The cached height of the empty tree is \(0\), and the cached height of a node is the height value stored at that node, so it is read off the root in constant time.

public def height : Tree α → Nat
  | .empty => 0
  | .node cached _ _ _ => cached

Uses 1 · Used by 30

Statement usesBinary trees with cached heights

Used byAVL rebalancing · Rebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL balance invariant · AVL rebalancing yields a balanced tree · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL insertion preserves balance · The AVL node constructor preserves balance · Correct cached heights · AVL rebalancing preserves cached heights · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · AVL insertion preserves cached heights · The AVL node constructor preserves cached heights · Upper bound on height after AVL rebalancing · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Upper bound on height after AVL insertion · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height · AVL node with computed height · Rebalancing an AVL node preserves the search-tree order · AVL insertion preserves the search-tree order

DefinitionAVL node with computed height#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\), with \(h\) of the empty tree equal to \(0\). Given trees \(L\) and \(R\) and a key \(k\), this is the node with left subtree \(L\), key \(k\) and right subtree \(R\) whose cached height is \(\max(h(L), h(R)) + 1\).

public def mkNode (left : Tree α) (key : α) (right : Tree α) : Tree α :=
  .node (max (height left) (height right) + 1) left key right

Uses 2 · Used by 19

Statement usesBinary trees with cached heights · Cached height of an AVL tree

Used byAVL rebalancing · Rebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL rebalancing yields a balanced tree · The AVL node constructor preserves balance · AVL rebalancing preserves cached heights · The AVL node constructor preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Insertion into an AVL tree · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height · Membership after insertion into an AVL tree · Rebalancing an AVL node preserves the search-tree order

DefinitionCorrect cached heights#✓fully proved

The empty tree has correct cached heights. A node storing the height \(c\), with left subtree \(\ell\) and right subtree \(r\), has correct cached heights when \(\ell\) and \(r\) have correct cached heights and \(c = \max(h(\ell), h(r)) + 1\), where \(h\) denotes the height cached at the root of a tree (and \(0\) for the empty tree).

public def CacheCorrect : Tree α → Prop
  | .empty => True
  | .node cached left _ right =>
      CacheCorrect left ∧ CacheCorrect right ∧
        cached = max (height left) (height right) + 1

Uses 2 · Used by 22

Statement usesBinary trees with cached heights · Cached height of an AVL tree

Used byAVL rebalancing yields a balanced tree · Deleting a key preserves AVL balance · Minimum deletion preserves AVL balance · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL insertion preserves balance · AVL rebalancing preserves cached heights · Deleting a key keeps cached heights correct · Minimum deletion keeps cached heights correct · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · AVL trees built from a list have correct cached heights · AVL insertion preserves cached heights · The AVL node constructor preserves cached heights · Upper bound on height after AVL rebalancing · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Upper bound on height after AVL insertion · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height

DefinitionAVL balance invariant#✓fully proved

The empty tree is balanced. A node with left subtree \(\ell\) and right subtree \(r\) is balanced when \(\ell\) and \(r\) are balanced and \(h(\ell) \le h(r) + 1\) and \(h(r) \le h(\ell) + 1\), where \(h\) denotes the height cached at the root of a tree (and \(0\) for the empty tree). Equivalently, at every node the balance factor \(h(\ell) - h(r)\) lies in \(\{-1, 0, 1\}\).

public def Balanced : Tree α → Prop
  | .empty => True
  | .node _ left _ right =>
      Balanced left ∧ Balanced right ∧ height left ≤ height right + 1 ∧
        height right ≤ height left + 1

Uses 2 · Used by 11

Statement usesBinary trees with cached heights · Cached height of an AVL tree

Used byAVL rebalancing yields a balanced tree · Deleting a key preserves AVL balance · Minimum deletion preserves AVL balance · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL trees built from a list are balanced · AVL insertion preserves balance · The AVL node constructor preserves balance · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height

DefinitionErasing the cached heights of an AVL tree#✓fully proved

Let \(\alpha\) be a type. Erasing the cached heights sends a tree with cached heights over \(\alpha\) to a binary tree over \(\alpha\): the empty tree goes to the empty binary tree, and a node with height \(h\), left subtree \(L\), key \(k\) and right subtree \(R\) goes to the binary-tree node with key \(k\) whose left and right subtrees are the erasures of \(L\) and \(R\).

public def toBinaryTree : Tree α → BinaryTree α
  | .empty => .nil
  | .node _ left key right => .node key (toBinaryTree left) (toBinaryTree right)

Uses 1 · Used by 27

Statement usesBinary trees with cached heights

Used byEvery key of an AVL tree satisfies a predicate · The all-keys predicate in terms of membership (AVL trees) · Keys left after removing the minimum exceed it · The all-keys predicate is unchanged by erasing height caches · Correctness of AVL search · Inorder traversal of an AVL tree · Inorder traversal of an AVL tree onto a suffix · AVL rebalancing preserves the inorder traversal · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · The inorder traversal of an ordered AVL tree has no duplicates · AVL inorder traversal agrees with the erased binary search tree · Membership in an AVL tree · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership in the inorder traversal of an AVL tree · Membership after insertion into an AVL tree · AVL membership is membership in the underlying binary tree · The leftmost key lies in the tree · Deletion removes the deleted key from an ordered AVL tree · Ordered AVL trees · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · The inorder traversal of an ordered AVL tree is strictly increasing · AVL insertion preserves the search-tree order · Order of an AVL tree via its underlying binary tree

DefinitionMembership in an AVL tree#✓fully proved

A key \(x\) belongs to a tree \(T\) when \(x\) belongs to the binary tree obtained from \(T\) by erasing the cached heights. Equivalently, no key belongs to the empty tree, and \(x\) belongs to a node with left subtree \(L\), key \(k\) and right subtree \(R\) exactly when \(x\) belongs to \(L\), \(x = k\), or \(x\) belongs to \(R\).

public def Mem (x : α) (tree : Tree α) : Prop :=
  BinarySearchTree.Mem x (toBinaryTree tree)

Uses 3 · Used by 17

Statement usesBinary trees with cached heights · Erasing the cached heights of an AVL tree · Membership in a binary tree

Used byThe all-keys predicate in terms of membership (AVL trees) · Keys left after removing the minimum exceed it · Correctness of AVL search · Inorder traversal after AVL deletion · Membership after AVL rebalancing · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership in an AVL tree built from a list · Membership in the inorder traversal of an AVL tree · Membership after insertion into an AVL tree · AVL membership is membership in the underlying binary tree · The leftmost key lies in the tree · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order

DefinitionEvery key of an AVL tree satisfies a predicate#✓fully proved

For a predicate \(p\) on keys and a tree \(t\) with cached heights, \(\mathrm{All}(p, t)\) holds when \(p\) holds at the key of every node of \(t\). It is defined as the corresponding predicate on the plain binary tree obtained from \(t\) by erasing its cached heights.

public def All (p : α → Prop) (tree : Tree α) : Prop :=
  BinarySearchTree.All p (toBinaryTree tree)

Uses 3 · Used by 9

Statement usesBinary trees with cached heights · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree

Used byThe all-keys predicate in terms of membership (AVL trees) · Keys left after removing the minimum exceed it · The all-keys predicate is unchanged by erasing height caches · Inorder traversal after AVL deletion · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order

DefinitionOrdered AVL trees#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). A tree with cached heights over \(\alpha\) is ordered when the binary tree obtained by erasing its cached heights is an ordered binary search tree: the empty tree is ordered, and a node with key \(k\) is ordered when its left and right subtrees are ordered, every key of the left subtree is less than \(k\), and every key of the right subtree is greater than \(k\).

public def Ordered [LT α] (tree : Tree α) : Prop :=
  BinarySearchTree.Ordered (toBinaryTree tree)

Uses 3 · Used by 16

Statement usesBinary trees with cached heights · Erasing the cached heights of an AVL tree · Ordered binary trees

Used byKeys left after removing the minimum exceed it · Correctness of AVL search · Inorder traversal after AVL deletion, alternative name · Inorder traversal after AVL deletion · The inorder traversal of an ordered AVL tree has no duplicates · Keys of an ordered AVL tree after deletion · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · Deleting a key from an ordered AVL tree keeps it ordered · Successor-step minimum removal preserves search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL trees built from a list are ordered · The inorder traversal of an ordered AVL tree is strictly increasing · AVL insertion preserves the search-tree order · Order of an AVL tree via its underlying binary tree

DefinitionInorder traversal of an AVL tree onto a suffix#✓fully proved

Given a tree \(t\) and a list \(s\), this is the list of keys of \(t\) in inorder (left subtree, root key, right subtree, recursively) followed by \(s\). It is computed in linear time by the binary search tree traversal of \(t\) with its cached heights erased.

public def inorderAux (tree : Tree α) (suffix : List α) : List α :=
  BinarySearchTree.inorderAux (toBinaryTree tree) suffix

Uses 3

Statement usesBinary trees with cached heights · Erasing the cached heights of an AVL tree · Inorder traversal of a binary tree with an accumulator

DefinitionInorder traversal of an AVL tree#✓fully proved

The inorder traversal of a tree \(t\) lists its keys with the left subtree first, then the root key, then the right subtree, recursively. It is the binary search tree inorder traversal of \(t\) with its cached heights erased, computed in linear time.

public def inorder (tree : Tree α) : List α :=
  BinarySearchTree.inorder (toBinaryTree tree)

Uses 3 · Used by 10

Statement usesBinary trees with cached heights · Erasing the cached heights of an AVL tree · Inorder traversal of a binary tree

Used byAVL rebalancing preserves the inorder traversal · Inorder traversal after AVL deletion, alternative name · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · The inorder traversal of an ordered AVL tree has no duplicates · AVL inorder traversal agrees with the erased binary search tree · Membership after AVL rebalancing · AVL deletion keeps every other key · Membership in the inorder traversal of an AVL tree · The inorder traversal of an ordered AVL tree is strictly increasing

TheoremAVL membership is membership in the underlying binary tree#✓fully proved

A key \(x\) lies in a tree \(T\) if and only if \(x\) lies in the binary tree obtained from \(T\) by erasing the cached heights.

This holds by definition.

public theorem mem_toBinaryTree {x : α} {tree : Tree α} :
    x ∈ tree ↔ x ∈ toBinaryTree tree

Uses 4

Statement usesMembership in an AVL tree · Binary trees with cached heights · Erasing the cached heights of an AVL tree · Membership in a binary tree

TheoremThe all-keys predicate is unchanged by erasing height caches#✓fully proved

For a predicate \(p\) on keys and a tree \(t\) with cached heights, \(\mathrm{All}(p, t)\) holds if and only if \(p\) holds at every key of the plain binary tree obtained from \(t\) by erasing its cached heights. This holds by definition.

public theorem all_toBinaryTree {p : α → Prop} {tree : Tree α} :
    All p tree ↔ BinarySearchTree.All p (toBinaryTree tree)

Uses 4

Statement usesEvery key of an AVL tree satisfies a predicate · Binary trees with cached heights · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree

TheoremOrder of an AVL tree via its underlying binary tree#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). A tree \(t\) with cached heights over \(\alpha\) is ordered if and only if the binary tree obtained from \(t\) by erasing the cached heights is an ordered binary search tree.

public theorem ordered_toBinaryTree [LT α] {tree : Tree α} :
    Ordered tree ↔ BinarySearchTree.Ordered (toBinaryTree tree)

Uses 4

Statement usesOrdered AVL trees · Binary trees with cached heights · Erasing the cached heights of an AVL tree · Ordered binary trees

TheoremAVL inorder traversal agrees with the erased binary search tree#✓fully proved

For every AVL tree \(t\), the inorder traversal of \(t\) equals the binary search tree inorder traversal of the binary tree obtained from \(t\) by erasing its cached heights; this holds by definition.

public theorem inorder_toBinaryTree (tree : Tree α) :
    inorder tree = BinarySearchTree.inorder (toBinaryTree tree)

Uses 4

Statement usesBinary trees with cached heights · Inorder traversal of an AVL tree · Erasing the cached heights of an AVL tree · Inorder traversal of a binary tree

DefinitionMembership search in an AVL tree#✓fully proved

For a linearly ordered type \(\alpha\) and a key \(x\), the search for \(x\) returns false on the empty tree; at a node with key \(k\) it searches the left subtree if \(x < k\), searches the right subtree if \(k < x\), and returns true otherwise. The cached heights are ignored.

public def contains [LinearOrder α] (x : α) : Tree α → Bool
  | .empty => false
  | .node _ left key right =>
      if x < key then contains x left
      else if key < x then contains x right
      else true

Uses 1 · Used by 1

Statement usesBinary trees with cached heights

Used byCorrectness of AVL search

DefinitionAVL rebalancing#✓fully proved

For trees \(l\), \(r\) with cached heights and a key \(x\), write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree) and \(N(A, y, B)\) for the node with left subtree \(A\), key \(y\), right subtree \(B\) and cached height \(\max(h(A), h(B)) + 1\). The node \(\mathrm{balance}(l, x, r)\) is defined by cases. If \(h(l) > h(r) + 1\) and \(l\) has left subtree \(A\), key \(y\) and right subtree \(B\), it is the single right rotation \(N(A, y, N(B, x, r))\) when \(h(B) \le h(A)\), and otherwise, when \(B\) has left subtree \(B_1\), key \(z\) and right subtree \(B_2\), the left-right double rotation \(N(N(A, y, B_1), z, N(B_2, x, r))\). Symmetrically, if \(h(l) \le h(r) + 1\), \(h(r) > h(l) + 1\) and \(r\) has left subtree \(A\), key \(y\) and right subtree \(B\), it is the single left rotation \(N(N(l, x, A), y, B)\) when \(h(A) \le h(B)\), and otherwise, when \(A\) has left subtree \(A_1\), key \(z\) and right subtree \(A_2\), the right-left double rotation \(N(N(l, x, A_1), z, N(A_2, y, B))\). In every other case it is \(N(l, x, r)\).

For balanced children with correct cached heights whose heights differ by at most two, the result is balanced again.

Cslib.Algorithms.Lean.AvlTree.balance · 26 lines

public def balance (left : Tree α) (key : α) (right : Tree α) : Tree α :=
  if height right + 1 < height left then
    match left with
    | .node _ leftLeft leftKey leftRight =>
        if height leftRight ≤ height leftLeft then
          mkNode leftLeft leftKey (mkNode leftRight key right)
        else
          match leftRight with
          | .node _ leftRightLeft leftRightKey leftRightRight =>
              mkNode (mkNode leftLeft leftKey leftRightLeft) leftRightKey
                (mkNode leftRightRight key right)
          | .empty => mkNode left key right
    | .empty => mkNode left key right
  else if height left + 1 < height right then
    match right with
    | .node _ rightLeft rightKey rightRight =>
        if height rightLeft ≤ height rightRight then
          mkNode (mkNode left key rightLeft) rightKey rightRight
        else
          match rightLeft with
          | .node _ rightLeftLeft rightLeftKey rightLeftRight =>
              mkNode (mkNode left key rightLeftLeft) rightLeftKey
                (mkNode rightLeftRight rightKey rightRight)
          | .empty => mkNode left key right
    | .empty => mkNode left key right
  else mkNode left key right

Uses 3 · Used by 37

Statement usesBinary trees with cached heights · Cached height of an AVL tree · AVL node with computed height

Used byKeys left after removing the minimum exceed it · Rebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL rebalancing yields a balanced tree · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL insertion preserves balance · AVL rebalancing preserves cached heights · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · AVL insertion preserves cached heights · AVL tree deletion · Removing the leftmost key of an AVL tree · Upper bound on height after AVL rebalancing · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Upper bound on height after AVL insertion · AVL rebalancing preserves the inorder traversal · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · Insertion into an AVL tree · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height · Membership after AVL rebalancing · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership after insertion into an AVL tree · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order

DefinitionInsertion into an AVL tree#✓fully proved

Let the keys be linearly ordered, and write \(\mathrm{balance}(L, k, R)\) for the AVL rebalancing of the node with left subtree \(L\), key \(k\) and right subtree \(R\). Inserting \(x\) into the empty tree gives the node with key \(x\), two empty children and cached height \(1\). Inserting \(x\) into a node with left subtree \(L\), key \(k\) and right subtree \(R\) gives \(\mathrm{balance}(L', k, R)\), where \(L'\) is the result of inserting \(x\) into \(L\), when \(x < k\); it gives \(\mathrm{balance}(L, k, R')\), where \(R'\) is the result of inserting \(x\) into \(R\), when \(k < x\); and otherwise it returns the node unchanged.

public def insert [LinearOrder α] (x : α) : Tree α → Tree α
  | .empty => mkNode .empty x .empty
  | tree@(.node _ left key right) =>
      if x < key then balance (insert x left) key right
      else if key < x then balance left key (insert x right)
      else tree

Uses 3 · Used by 8

Statement usesBinary trees with cached heights · AVL rebalancing · AVL node with computed height

Used byAVL insertion preserves balance · AVL insertion preserves cached heights · Building an AVL tree from a list · Upper bound on height after AVL insertion · Insertion does not lower the height · Membership in an AVL tree built from a list · Membership after insertion into an AVL tree · AVL insertion preserves the search-tree order

DefinitionBuilding an AVL tree from a list#✓fully proved

For a linearly ordered type \(\alpha\), the tree built from the empty list is the empty tree, and the tree built from a list with head \(x\) and tail \(xs\) is obtained by AVL insertion of \(x\) into the tree built from \(xs\). Thus the list is inserted from right to left, starting from the empty tree.

public def fromList [LinearOrder α] : List α → Tree α
  | [] => .empty
  | x :: xs => insert x (fromList xs)

Uses 2 · Used by 4

Statement usesBinary trees with cached heights · Insertion into an AVL tree

Used byAVL trees built from a list are balanced · AVL trees built from a list have correct cached heights · Membership in an AVL tree built from a list · AVL trees built from a list are ordered

TheoremThe all-keys predicate in terms of membership (AVL trees)#✓fully proved

For a predicate \(p\) on keys and a tree \(t\) with cached heights, \(\mathrm{All}(p, t)\) holds if and only if \(p(x)\) holds for every \(x \in t\), where \(x \in t\) means that \(x\) is the key of some node of \(t\).

public theorem all_iff_forall_mem {p : α → Prop} {tree : Tree α} :
    All p tree ↔ ∀ x, x ∈ tree → p x

Uses 5 · Used by 7

Statement usesEvery key of an AVL tree satisfies a predicate · Membership in an AVL tree · Binary trees with cached heights

Proof usesErasing the cached heights of an AVL tree · A predicate holds at all keys of a binary tree iff it holds at all its members

Used byKeys left after removing the minimum exceed it · Inorder traversal after AVL deletion · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order

TheoremMembership in the inorder traversal of an AVL tree#✓fully proved

A key \(x\) occurs in the inorder traversal of a tree \(T\) if and only if \(x\) lies in \(T\).

public theorem mem_inorder {x : α} {tree : Tree α} :
    x ∈ inorder tree ↔ x ∈ tree

Uses 5 · Used by 3

Statement usesMembership in an AVL tree · Binary trees with cached heights · Inorder traversal of an AVL tree

Proof usesErasing the cached heights of an AVL tree · Membership in the inorder traversal of a binary tree

Used byInorder traversal after AVL deletion · Membership after AVL rebalancing · AVL deletion keeps every other key

TheoremThe inorder traversal of an ordered AVL tree is strictly increasing#✓fully proved

Let \(\alpha\) be a linearly ordered type. If a tree \(t\) with cached heights over \(\alpha\) is ordered, then in the inorder traversal of \(t\) every key is less than every key that comes after it.

public theorem ordered_inorder [LinearOrder α] {tree : Tree α}
    (hTree : Ordered tree) : List.Pairwise (· < ·) (inorder tree)

Uses 5

Statement usesOrdered AVL trees · Binary trees with cached heights · Inorder traversal of an AVL tree

Proof usesErasing the cached heights of an AVL tree · The inorder traversal of an ordered binary tree is strictly increasing

TheoremThe inorder traversal of an ordered AVL tree has no duplicates#✓fully proved

For a linearly ordered type \(\alpha\), if an AVL tree is ordered, then its inorder traversal contains no key twice.

public theorem inorder_nodup [LinearOrder α] {tree : Tree α}
    (hTree : Ordered tree) : (inorder tree).Nodup

Uses 5

Statement usesOrdered AVL trees · Binary trees with cached heights · Inorder traversal of an AVL tree

Proof usesErasing the cached heights of an AVL tree · The inorder traversal of a binary search tree has no duplicates

TheoremThe AVL node constructor preserves cached heights#✓fully proved

If two AVL trees \(\ell\) and \(r\) have correct cached heights, then for every key \(k\) the node built from \(\ell\), \(k\) and \(r\) by the smart constructor, which stores the height \(\max(h(\ell), h(r)) + 1\) where \(h\) denotes the height cached at the root (and \(0\) for the empty tree), also has correct cached heights.

public theorem cacheCorrect_mkNode {key : α} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    CacheCorrect (mkNode left key right)

Uses 4 · Used by 2

Statement usesCorrect cached heights · Binary trees with cached heights · AVL node with computed height

Proof usesCached height of an AVL tree

Used byAVL rebalancing preserves cached heights · AVL insertion preserves cached heights

TheoremThe AVL node constructor preserves balance#✓fully proved

Let \(\ell\) and \(r\) be AVL trees that satisfy the AVL balance invariant, and write \(h(\ell)\) and \(h(r)\) for the heights cached at their roots (with height \(0\) for the empty tree). If \(h(\ell) \le h(r) + 1\) and \(h(r) \le h(\ell) + 1\), then for every key \(k\) the node built from \(\ell\), \(k\) and \(r\) by the smart constructor, which stores the height \(\max(h(\ell), h(r)) + 1\), satisfies the AVL balance invariant.

public theorem balanced_mkNode {key : α} {left right : Tree α}
    (hLeft : Balanced left) (hRight : Balanced right)
    (hLeftRight : height left ≤ height right + 1)
    (hRightLeft : height right ≤ height left + 1) :
    Balanced (mkNode left key right)

Uses 4 · Used by 2

Statement usesAVL balance invariant · Binary trees with cached heights · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL insertion preserves balance

TheoremRebalancing when the heights of the children differ by at most one#✓fully proved

Let \(l\) and \(r\) be trees with cached heights, let \(x\) be a key, and write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree). If \(h(l) \le h(r) + 1\) and \(h(r) \le h(l) + 1\), then \(\mathrm{balance}(l, x, r)\) is the node with left subtree \(l\), key \(x\), right subtree \(r\) and cached height \(\max(h(l), h(r)) + 1\); no rotation is performed.

public theorem balance_eq_mkNode_of_le {key : α} {left right : Tree α}
    (hLeft : height left ≤ height right + 1) (hRight : height right ≤ height left + 1) :
    balance left key right = mkNode left key right

Uses 4 · Used by 9

Statement usesBinary trees with cached heights · AVL rebalancing · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL rebalancing preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height · Rebalancing an AVL node preserves the search-tree order

TheoremSingle right rotation in AVL rebalancing#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree), \(\langle c; A, y, B \rangle\) for the node with cached height \(c\), left subtree \(A\), key \(y\) and right subtree \(B\), and \(N(A, y, B)\) for the node \(\langle \max(h(A), h(B)) + 1; A, y, B \rangle\). Let \(A\), \(B\), \(R\) be trees with cached heights, let \(x\), \(y\) be keys and let \(c\) be a natural number. If \(h(R) + 1 < c\) and \(h(B) \le h(A)\), then \(\mathrm{balance}(\langle c; A, y, B \rangle, x, R) = N(A, y, N(B, x, R))\).

public theorem balance_left_single {key leftKey : α} {cached : Nat}
    {leftLeft leftRight right : Tree α}
    (hTall : height right + 1 < cached) (hSingle : height leftRight ≤ height leftLeft) :
    balance (.node cached leftLeft leftKey leftRight) key right =
      mkNode leftLeft leftKey (mkNode leftRight key right)

Uses 4 · Used by 6

Statement usesBinary trees with cached heights · AVL rebalancing · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL rebalancing preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Rebalancing an AVL node preserves the search-tree order

TheoremLeft-right double rotation in AVL rebalancing#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree), \(\langle c; A, y, B \rangle\) for the node with cached height \(c\), left subtree \(A\), key \(y\) and right subtree \(B\), and \(N(A, y, B)\) for the node \(\langle \max(h(A), h(B)) + 1; A, y, B \rangle\). Let \(A\), \(B\), \(C\), \(R\) be trees with cached heights, let \(x\), \(y\), \(z\) be keys and let \(c\), \(c'\) be natural numbers. If \(h(R) + 1 < c\) and \(h(A) < c'\), then \(\mathrm{balance}(\langle c; A, y, \langle c'; B, z, C \rangle \rangle, x, R) = N(N(A, y, B), z, N(C, x, R))\).

public theorem balance_left_double {key leftKey leftRightKey : α}
    {cached cachedRight : Nat}
    {leftLeft leftRightLeft leftRightRight right : Tree α}
    (hTall : height right + 1 < cached) (hDouble : height leftLeft < cachedRight) :
    balance (.node cached leftLeft leftKey
        (.node cachedRight leftRightLeft leftRightKey leftRightRight)) key right =
      mkNode (mkNode leftLeft leftKey leftRightLeft) leftRightKey
        (mkNode leftRightRight key right)

Uses 4 · Used by 6

Statement usesBinary trees with cached heights · AVL rebalancing · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL rebalancing preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Rebalancing an AVL node preserves the search-tree order

TheoremSingle left rotation in AVL rebalancing#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree), \(\langle c; A, y, B \rangle\) for the node with cached height \(c\), left subtree \(A\), key \(y\) and right subtree \(B\), and \(N(A, y, B)\) for the node \(\langle \max(h(A), h(B)) + 1; A, y, B \rangle\). Let \(L\), \(A\), \(B\) be trees with cached heights, let \(x\), \(y\) be keys and let \(c\) be a natural number. If \(h(L) + 1 < c\) and \(h(A) \le h(B)\), then \(\mathrm{balance}(L, x, \langle c; A, y, B \rangle) = N(N(L, x, A), y, B)\).

public theorem balance_right_single {key rightKey : α} {cached : Nat}
    {left rightLeft rightRight : Tree α}
    (hTall : height left + 1 < cached)
    (hSingle : height rightLeft ≤ height rightRight) :
    balance left key (.node cached rightLeft rightKey rightRight) =
      mkNode (mkNode left key rightLeft) rightKey rightRight

Uses 4 · Used by 6

Statement usesBinary trees with cached heights · AVL rebalancing · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL rebalancing preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Rebalancing an AVL node preserves the search-tree order

TheoremRight-left double rotation in AVL rebalancing#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree), \(\langle c; A, y, B \rangle\) for the node with cached height \(c\), left subtree \(A\), key \(y\) and right subtree \(B\), and \(N(A, y, B)\) for the node \(\langle \max(h(A), h(B)) + 1; A, y, B \rangle\). Let \(L\), \(A\), \(B\), \(C\) be trees with cached heights, let \(x\), \(y\), \(z\) be keys and let \(c\), \(c'\) be natural numbers. If \(h(L) + 1 < c\) and \(h(C) < c'\), then \(\mathrm{balance}(L, x, \langle c; \langle c'; A, z, B \rangle, y, C \rangle) = N(N(L, x, A), z, N(B, y, C))\).

public theorem balance_right_double {key rightKey rightLeftKey : α}
    {cached cachedLeft : Nat}
    {left rightLeftLeft rightLeftRight rightRight : Tree α}
    (hTall : height left + 1 < cached)
    (hDouble : height rightRight < cachedLeft) :
    balance left key (.node cached
        (.node cachedLeft rightLeftLeft rightLeftKey rightLeftRight) rightKey rightRight) =
      mkNode (mkNode left key rightLeftLeft) rightLeftKey
        (mkNode rightLeftRight rightKey rightRight)

Uses 4 · Used by 6

Statement usesBinary trees with cached heights · AVL rebalancing · Cached height of an AVL tree · AVL node with computed height

Used byAVL rebalancing yields a balanced tree · AVL rebalancing preserves cached heights · Upper bound on height after AVL rebalancing · AVL rebalancing preserves the inorder traversal · Rebalancing does not drop below the taller child · Rebalancing an AVL node preserves the search-tree order

TheoremAVL rebalancing preserves cached heights#✓fully proved

If two AVL trees \(\ell\) and \(r\) have correct cached heights, then for every key \(k\) the tree produced by the rebalancing function from \(\ell\), \(k\) and \(r\) also has correct cached heights.

public theorem cacheCorrect_balance {key : α} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    CacheCorrect (balance left key right)

Uses 11 · Used by 3

Statement usesCorrect cached heights · Binary trees with cached heights · AVL rebalancing

Proof usesRebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · The AVL node constructor preserves cached heights · Cached height of an AVL tree · AVL node with computed height

Used byDeletion keeps cached heights correct · Removing the minimum keeps cached heights correct · AVL insertion preserves cached heights

TheoremUpper bound on height after AVL rebalancing#✓fully proved

Let \(l\) and \(r\) be trees whose cached heights are correct at every node, and write \(h\) for the cached height. Then for every key \(k\), the rebalanced node \(b\) built from \(l\), \(k\) and \(r\) satisfies \(h(b) \le \max(h(l), h(r)) + 1\).

public theorem height_balance_le {key : α} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    height (balance left key right) ≤ max (height left) (height right) + 1

Uses 10 · Used by 3

Statement usesCorrect cached heights · Binary trees with cached heights · AVL rebalancing · Cached height of an AVL tree

Proof usesRebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL node with computed height

Used byDeletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Upper bound on height after AVL insertion

TheoremRebalancing does not drop below the taller child#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\), with \(h\) of the empty tree equal to \(0\), and write \(\mathrm{balance}(L, k, R)\) for the AVL rebalancing of the node with left subtree \(L\), key \(k\) and right subtree \(R\). If \(L\) and \(R\) are trees whose cached heights are correct at every node, then for every key \(k\) we have \(\max(h(L), h(R)) \le h(\mathrm{balance}(L, k, R))\).

public theorem le_height_balance {key : α} {left right : Tree α}
    (hLeft : CacheCorrect left) (hRight : CacheCorrect right) :
    max (height left) (height right) ≤ height (balance left key right)

Uses 10 · Used by 3

Statement usesCorrect cached heights · Binary trees with cached heights · AVL rebalancing · Cached height of an AVL tree

Proof usesRebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · AVL node with computed height

Used byDeletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Insertion does not lower the height

TheoremAVL rebalancing yields a balanced tree#✓fully proved

Let \(l\) and \(r\) be trees whose cached heights are correct at every node and which are balanced (at every node the cached heights of the two subtrees differ by at most one), let \(x\) be a key, and write \(h(T)\) for the cached height at the root of a tree \(T\) (zero for the empty tree). If \(h(l) \le h(r) + 2\) and \(h(r) \le h(l) + 2\), then \(\mathrm{balance}(l, x, r)\) is balanced.

One insertion step maintains this precondition.

public theorem balanced_balance {key : α} {left right : Tree α}
    (hCacheLeft : CacheCorrect left) (hCacheRight : CacheCorrect right)
    (hBalLeft : Balanced left) (hBalRight : Balanced right)
    (hDiffLeft : height left ≤ height right + 2)
    (hDiffRight : height right ≤ height left + 2) :
    Balanced (balance left key right)

Uses 12 · Used by 3

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · AVL rebalancing · Cached height of an AVL tree

Proof usesRebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · The AVL node constructor preserves balance · AVL node with computed height

Used byDeletion preserves AVL balance · Removing the minimum preserves AVL balance · AVL insertion preserves balance

TheoremAVL rebalancing preserves the inorder traversal#✓fully proved

For all trees \(l\) and \(r\) and every key \(k\), the inorder traversal of the rebalanced node built from \(l\), \(k\) and \(r\) is the inorder traversal of \(l\), followed by \(k\), followed by the inorder traversal of \(r\).

public theorem inorder_balance {key : α} {left right : Tree α} :
    inorder (balance left key right) = inorder left ++ key :: inorder right

Uses 13 · Used by 3

Statement usesBinary trees with cached heights · AVL rebalancing · Inorder traversal of an AVL tree

Proof usesRebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · Cached height of an AVL tree · AVL node with computed height · Erasing the cached heights of an AVL tree · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator

Used byThe inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · Membership after AVL rebalancing

TheoremMembership after AVL rebalancing#✓fully proved

Write \(\mathrm{balance}(L, k, R)\) for the AVL rebalancing of the node with left subtree \(L\), key \(k\) and right subtree \(R\). For trees \(L\) and \(R\) and keys \(k\) and \(x\), the key \(x\) lies in \(\mathrm{balance}(L, k, R)\) if and only if \(x\) lies in \(L\), \(x = k\), or \(x\) lies in \(R\).

public theorem mem_balance {x key : α} {left right : Tree α} :
    x ∈ balance left key right ↔ x ∈ left ∨ x = key ∨ x ∈ right

Uses 6 · Used by 7

Statement usesMembership in an AVL tree · Binary trees with cached heights · AVL rebalancing

Proof usesInorder traversal of an AVL tree · AVL rebalancing preserves the inorder traversal · Membership in the inorder traversal of an AVL tree

Used byKeys left after removing the minimum exceed it · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership after insertion into an AVL tree · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order

TheoremRebalancing an AVL node preserves the search-tree order#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(k \in \alpha\), and let \(L\) and \(R\) be ordered trees with cached heights over \(\alpha\) such that every key of \(L\) is less than \(k\) and every key of \(R\) is greater than \(k\). Then the tree that rebalancing produces from left subtree \(L\), key \(k\) and right subtree \(R\) is ordered.

public theorem ordered_balance [LinearOrder α] {key : α} {left right : Tree α}
    (hOrdLeft : Ordered left) (hOrdRight : Ordered right)
    (hAllLeft : All (· < key) left) (hAllRight : All (key < ·) right) :
    Ordered (balance left key right)

Uses 16 · Used by 3

Statement usesEvery key of an AVL tree satisfies a predicate · Ordered AVL trees · Binary trees with cached heights · AVL rebalancing

Proof usesMembership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · Rebalancing when the heights of the children differ by at most one · Left-right double rotation in AVL rebalancing · Single right rotation in AVL rebalancing · Right-left double rotation in AVL rebalancing · Single left rotation in AVL rebalancing · Cached height of an AVL tree · AVL node with computed height · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Ordered binary trees

Used byAVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order

TheoremAVL insertion preserves cached heights#✓fully proved

Let \(\alpha\) be a linearly ordered type. If an AVL tree \(t\) over \(\alpha\) has correct cached heights, then for every \(x \in \alpha\) the tree obtained by inserting \(x\) into \(t\) also has correct cached heights.

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

Uses 7 · Used by 4

Statement usesCorrect cached heights · Binary trees with cached heights · Insertion into an AVL tree

Proof usesAVL rebalancing · AVL rebalancing preserves cached heights · The AVL node constructor preserves cached heights · Cached height of an AVL tree

Used byAVL insertion preserves balance · AVL trees built from a list have correct cached heights · Upper bound on height after AVL insertion · Insertion does not lower the height

TheoremUpper bound on height after AVL insertion#✓fully proved

For a linearly ordered type \(\alpha\), if a tree \(t\) has correct cached heights at every node, then for every key \(x\) the cached height of the tree obtained by inserting \(x\) into \(t\) is at most the cached height of \(t\) plus one.

public theorem height_insert_le [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : CacheCorrect tree) : height (insert x tree) ≤ height tree + 1

Uses 7 · Used by 1

Statement usesCorrect cached heights · Binary trees with cached heights · Cached height of an AVL tree · Insertion into an AVL tree

Proof usesAVL rebalancing · AVL insertion preserves cached heights · Upper bound on height after AVL rebalancing

Used byAVL insertion preserves balance

TheoremInsertion does not lower the height#✓fully proved

Write \(h(T)\) for the cached height at the root of a tree \(T\), with \(h\) of the empty tree equal to \(0\). Let the keys be linearly ordered, and let \(T\) be a tree whose cached heights are correct at every node and which satisfies the AVL balance invariant at every node. Then for every key \(x\), if \(T'\) is the tree obtained by inserting \(x\) into \(T\), we have \(h(T) \le h(T')\).

public theorem le_height_insert [LinearOrder α] {x : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    height tree ≤ height (insert x tree)

Uses 10 · Used by 1

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · Cached height of an AVL tree · Insertion into an AVL tree

Proof usesAVL rebalancing · Rebalancing when the heights of the children differ by at most one · AVL insertion preserves cached heights · Rebalancing does not drop below the taller child · AVL node with computed height

Used byAVL insertion preserves balance

TheoremAVL insertion preserves balance#✓fully proved

Let \(\alpha\) be a linearly ordered type, let \(t\) be an AVL tree over \(\alpha\) and let \(x \in \alpha\). If \(t\) has correct cached heights and satisfies the AVL balance invariant, then the tree obtained by inserting \(x\) into \(t\) also satisfies the AVL balance invariant.

public theorem balanced_insert [LinearOrder α] {x : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    Balanced (insert x tree)

Uses 11 · Used by 1

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · Insertion into an AVL tree

Proof usesAVL rebalancing · AVL rebalancing yields a balanced tree · The AVL node constructor preserves balance · AVL insertion preserves cached heights · Cached height of an AVL tree · Upper bound on height after AVL insertion · Insertion does not lower the height

Used byAVL trees built from a list are balanced

TheoremMembership after insertion into an AVL tree#✓fully proved

Let the keys be linearly ordered. A key \(y\) lies in the tree obtained by inserting \(x\) into a tree \(T\) if and only if \(y = x\) or \(y\) lies in \(T\).

public theorem mem_insert [LinearOrder α] {x y : α} {tree : Tree α} :
    y ∈ insert x tree ↔ y = x ∨ y ∈ tree

Uses 8 · Used by 2

Statement usesMembership in an AVL tree · Binary trees with cached heights · Insertion into an AVL tree

Proof usesAVL rebalancing · Membership after AVL rebalancing · AVL node with computed height · Erasing the cached heights of an AVL tree · Membership in a binary tree

Used byMembership in an AVL tree built from a list · AVL insertion preserves the search-tree order

TheoremAVL insertion preserves the search-tree order#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every key \(x \in \alpha\) and every ordered tree \(t\) with cached heights over \(\alpha\), the tree obtained by inserting \(x\) into \(t\) is ordered.

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

Uses 13 · Used by 1

Statement usesOrdered AVL trees · Binary trees with cached heights · Insertion into an AVL tree

Proof usesEvery key of an AVL tree satisfies a predicate · Membership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · AVL rebalancing · Cached height of an AVL tree · Membership after insertion into an AVL tree · Rebalancing an AVL node preserves the search-tree order · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Ordered binary trees

Used byAVL trees built from a list are ordered

TheoremCorrectness of AVL search#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(t\) be an ordered AVL tree over \(\alpha\). Then for every \(x \in \alpha\), searching for \(x\) in \(t\) by following comparisons from the root returns true if and only if \(x\) is a key of \(t\).

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

Uses 7

Statement usesMembership in an AVL tree · Ordered AVL trees · Binary trees with cached heights · Membership search in an AVL tree

Proof usesErasing the cached heights of an AVL tree · Search in a binary search tree · Search in a binary search tree is correct

TheoremAVL trees built from a list have correct cached heights#✓fully proved

For every list \(L\) over a linearly ordered type, the AVL tree built from \(L\) by successive insertion has correct cached heights.

public theorem cacheCorrect_fromList [LinearOrder α] {xs : List α} :
    CacheCorrect (fromList xs)

Uses 3 · Used by 1

Statement usesCorrect cached heights · Building an AVL tree from a list

Proof usesAVL insertion preserves cached heights

Used byAVL trees built from a list are balanced

TheoremAVL trees built from a list are balanced#✓fully proved

For every list \(L\) over a linearly ordered type, the AVL tree built from \(L\) by successive insertion satisfies the AVL balance invariant.

public theorem balanced_fromList [LinearOrder α] {xs : List α} :
    Balanced (fromList xs)

Uses 4

Statement usesAVL balance invariant · Building an AVL tree from a list

Proof usesAVL insertion preserves balance · AVL trees built from a list have correct cached heights

TheoremAVL trees built from a list are ordered#✓fully proved

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

public theorem ordered_fromList [LinearOrder α] {xs : List α} :
    Ordered (fromList xs)

Uses 3

Statement usesOrdered AVL trees · Building an AVL tree from a list

Proof usesAVL insertion preserves the search-tree order

TheoremMembership in an AVL tree built from a list#✓fully proved

Let the keys be linearly ordered. A key lies in the tree obtained by inserting the entries of a list one at a time, from last to first, into the empty tree exactly when it is in the list.

public theorem mem_fromList [LinearOrder α] {x : α} {xs : List α} :
    x ∈ fromList xs ↔ x ∈ xs

Uses 5

Statement usesMembership in an AVL tree · Binary trees with cached heights · Building an AVL tree from a list

Proof usesInsertion into an AVL tree · Membership after insertion into an AVL tree

DefinitionLeftmost key of a tree#✓fully proved

Given a default value \(d\) and a binary tree \(T\) with cached heights, the leftmost key of \(T\) with default \(d\) is \(d\) when \(T\) is empty; when \(T\) has left subtree \(L\) and root key \(k\), it is the leftmost key of \(L\) with default \(k\). Thus for a nonempty tree it is the key of the node reached from the root by following left children as far as possible, and it does not depend on \(d\).

public def minD : α → Tree α → α
  | default, .empty => default
  | _, .node _ left key _ => minD key left

Uses 1 · Used by 13

Statement usesBinary trees with cached heights

Used byKeys left after removing the minimum exceed it · Deletion preserves AVL balance · Deletion keeps cached heights correct · AVL tree deletion · Deletion does not increase the height of an AVL tree · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · Deletion lowers the height of an AVL tree by at most one · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · The leftmost key lies in the tree · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order

DefinitionRemoving the leftmost key of an AVL tree#✓fully proved

For a tree \(t\) with cached heights, the tree obtained by removing the leftmost key of \(t\) is defined by recursion on \(t\). The empty tree stays empty. A node whose left subtree is empty is replaced by its right subtree. A node with nonempty left subtree \(l\), key \(k\) and right subtree \(r\) is replaced by \(\mathrm{balance}(l', k, r)\), where \(l'\) is \(l\) with its leftmost key removed and \(\mathrm{balance}\) is the AVL rebalancing function.

public def eraseMin : Tree α → Tree α
  | .empty => .empty
  | .node _ left key right =>
      match left with
      | .empty => right
      | .node _ _ _ _ => balance (eraseMin left) key right

Uses 2 · Used by 17

Statement usesBinary trees with cached heights · AVL rebalancing

Used byKeys left after removing the minimum exceed it · Deletion preserves AVL balance · Removing the minimum preserves AVL balance · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · Minimum deletion in an AVL tree · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order

DefinitionMinimum deletion in an AVL tree#✓fully proved

Minimum deletion maps a binary tree with cached heights to the tree obtained by removing its leftmost key and rebalancing on the way back up. It is the operation of removing the minimum, under the name used for the successor step of deletion, where a deleted node with two children is replaced by the minimum of its right subtree.

public def deleteMin : Tree α → Tree α :=
  eraseMin

Uses 2 · Used by 13

Statement usesBinary trees with cached heights · Removing the leftmost key of an AVL tree

Used byMinimum deletion preserves AVL balance · Deletion preserves AVL balance · Minimum deletion keeps cached heights correct · Deletion keeps cached heights correct · AVL tree deletion · Deletion does not increase the height of an AVL tree · Inorder traversal after AVL deletion · Deletion lowers the height of an AVL tree by at most one · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Deletion removes the deleted key from an ordered AVL tree · Successor-step minimum removal preserves search-tree order · AVL deletion preserves search-tree order

DefinitionAVL tree deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(x \in \alpha\). Deleting \(x\) from a tree with cached heights is defined by recursion on the tree, where \(\mathrm{balance}\) denotes the AVL rebalancing function. The empty tree stays empty. For a node with left subtree \(l\), key \(k\) and right subtree \(r\): if \(x < k\), the result is \(\mathrm{balance}(l', k, r)\), where \(l'\) is \(l\) with \(x\) deleted; if \(k < x\), the result is \(\mathrm{balance}(l, k, r')\), where \(r'\) is \(r\) with \(x\) deleted; if \(x = k\), the node is replaced by \(r\) when \(l\) is empty, by \(l\) when \(r\) is empty, and otherwise by \(\mathrm{balance}(l, m, r'')\), where \(m\) is the leftmost key of \(r\) and \(r''\) is \(r\) with its leftmost key removed.

public def erase [LinearOrder α] (x : α) : Tree α → Tree α
  | .empty => .empty
  | .node _ left key right =>
      if x < key then balance (erase x left) key right
      else if key < x then balance left key (erase x right)
      else
        match left, right with
        | .empty, _ => right
        | _, .empty => left
        | _, _ => balance left (minD key right) (deleteMin right)

Uses 4 · Used by 10

Statement usesBinary trees with cached heights · AVL rebalancing · Minimum deletion in an AVL tree · Leftmost key of a tree

Used byDeletion preserves AVL balance · Deletion keeps cached heights correct · AVL tree deletion under its alternative name · Deletion does not increase the height of an AVL tree · Inorder traversal after AVL deletion · Deletion lowers the height of an AVL tree by at most one · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order

DefinitionAVL tree deletion under its alternative name#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a tree \(t\) with cached heights, \(\mathrm{delete}(x, t)\) is defined to be \(\mathrm{erase}(x, t)\), the AVL deletion of \(x\) from \(t\).

public def delete [LinearOrder α] (x : α) (tree : Tree α) : Tree α :=
  erase x tree

Uses 2 · Used by 4

Statement usesBinary trees with cached heights · AVL tree deletion

Used byDeleting a key preserves AVL balance · Deleting a key keeps cached heights correct · Inorder traversal after AVL deletion, alternative name · Deleting a key from an ordered AVL tree keeps it ordered

TheoremThe leftmost key lies in the tree#✓fully proved

For every nonempty binary tree \(T\) with cached heights and every default value \(d\), the leftmost key of \(T\) computed with default \(d\) occurs in \(T\).

public theorem minD_mem {default : α} {tree : Tree α} (hTree : tree ≠ .empty) :
    minD default tree ∈ tree

Uses 5 · Used by 4

Statement usesMembership in an AVL tree · Binary trees with cached heights · Leftmost key of a tree

Proof usesErasing the cached heights of an AVL tree · Membership in a binary tree

Used byKeys left after removing the minimum exceed it · Keys of an ordered AVL tree after deletion · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order

TheoremRemoving the minimum keeps cached heights correct#✓fully proved

Let \(t\) be a binary tree with a cached height at each node whose cached heights are correct: each node stores one more than the larger of the cached heights of its two subtrees, the empty tree having height \(0\). Then the cached heights of the tree obtained from \(t\) by removing its leftmost key, rebalancing on the way back up, are again correct.

public theorem cacheCorrect_eraseMin {tree : Tree α} (hTree : CacheCorrect tree) :
    CacheCorrect (eraseMin tree)

Uses 6 · Used by 8

Statement usesCorrect cached heights · Binary trees with cached heights · Removing the leftmost key of an AVL tree

Proof usesAVL rebalancing · AVL rebalancing preserves cached heights · Cached height of an AVL tree

Used byDeletion preserves AVL balance · Removing the minimum preserves AVL balance · Minimum deletion keeps cached heights correct · Deletion keeps cached heights correct · Deletion does not increase the height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one

TheoremRemoving the leftmost key does not increase the height of an AVL tree#✓fully proved

If \(t\) is a tree whose cached heights are correct, then the cached height of the tree obtained from \(t\) by removing its leftmost key is at most the cached height of \(t\).

public theorem height_eraseMin_le {tree : Tree α} (hTree : CacheCorrect tree) :
    height (eraseMin tree) ≤ height tree

Uses 7 · Used by 5

Statement usesCorrect cached heights · Binary trees with cached heights · Removing the leftmost key of an AVL tree · Cached height of an AVL tree

Proof usesAVL rebalancing · Removing the minimum keeps cached heights correct · Upper bound on height after AVL rebalancing

Used byDeletion preserves AVL balance · Removing the minimum preserves AVL balance · Deletion does not increase the height of an AVL tree · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one

TheoremRemoving the leftmost key lowers the height of an AVL tree by at most one#✓fully proved

If \(t\) is a tree whose cached heights are correct and which is balanced, then the cached height of \(t\) is at most one more than the cached height of the tree obtained from \(t\) by removing its leftmost key.

public theorem le_height_eraseMin {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    height tree ≤ height (eraseMin tree) + 1

Uses 11 · Used by 3

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · Removing the leftmost key of an AVL tree · Cached height of an AVL tree

Proof usesAVL rebalancing · Rebalancing when the heights of the children differ by at most one · Removing the minimum keeps cached heights correct · Removing the leftmost key does not increase the height of an AVL tree · Rebalancing does not drop below the taller child · AVL node with computed height

Used byDeletion preserves AVL balance · Removing the minimum preserves AVL balance · Deletion lowers the height of an AVL tree by at most one

TheoremRemoving the minimum preserves AVL balance#✓fully proved

Let \(t\) be a binary tree with a cached height at each node whose cached heights are correct, and which is balanced: at every node the cached heights of the two subtrees differ by at most one. Then the tree obtained from \(t\) by removing its leftmost key, rebalancing on the way back up, is again balanced.

public theorem balanced_eraseMin {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    Balanced (eraseMin tree)

Uses 10 · Used by 2

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · Removing the leftmost key of an AVL tree

Proof usesAVL rebalancing · AVL rebalancing yields a balanced tree · Removing the minimum keeps cached heights correct · Cached height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Removing the leftmost key lowers the height of an AVL tree by at most one

Used byMinimum deletion preserves AVL balance · Deletion preserves AVL balance

TheoremRemoving the leftmost key preserves search-tree order#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type. If \(T\) is ordered as a search tree, then so is the tree obtained from \(T\) by removing its leftmost key and rebalancing on the way back up.

public theorem ordered_eraseMin [LinearOrder α] {tree : Tree α}
    (hTree : Ordered tree) : Ordered (eraseMin tree)

Uses 13 · Used by 2

Statement usesOrdered AVL trees · Binary trees with cached heights · Removing the leftmost key of an AVL tree

Proof usesEvery key of an AVL tree satisfies a predicate · Membership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · AVL rebalancing · Membership after AVL rebalancing · Rebalancing an AVL node preserves the search-tree order · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees

Used bySuccessor-step minimum removal preserves search-tree order · AVL deletion preserves search-tree order

TheoremKeys left after removing the minimum exceed it#✓fully proved

Let \(t\) be a binary tree with keys from a linearly ordered type and a cached height at each node, and suppose \(t\) is ordered: at every node, all keys in the left subtree are strictly smaller and all keys in the right subtree are strictly larger than the key at that node. Let \(m\) be the leftmost key of \(t\), or an arbitrary default value if \(t\) is empty. Then every key of the tree obtained from \(t\) by removing its leftmost key, rebalancing on the way back up, is strictly greater than \(m\).

public theorem all_minD_lt_eraseMin_of_ordered [LinearOrder α] {default : α} {tree : Tree α}
    (hTree : Ordered tree) : All (minD default tree < ·) (eraseMin tree)

Uses 13 · Used by 1

Statement usesEvery key of an AVL tree satisfies a predicate · Ordered AVL trees · Binary trees with cached heights · Removing the leftmost key of an AVL tree · Leftmost key of a tree

Proof usesMembership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · AVL rebalancing · Membership after AVL rebalancing · The leftmost key lies in the tree · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Ordered binary trees

Used byAVL deletion preserves search-tree order

TheoremThe inorder traversal begins with the leftmost key#✓fully proved

Let \(t\) be a nonempty tree with cached heights and \(m\) its leftmost key. Then the inorder traversal of \(t\) is \(m\) followed by the inorder traversal of the tree obtained from \(t\) by removing its leftmost key.

The leftmost key is computed by a function that takes a default value for the empty tree; the identity holds for every choice of default.

public theorem inorder_eq_minD_cons_eraseMin {default : α} {tree : Tree α}
    (hTree : tree ≠ .empty) :
    inorder tree = minD default tree :: inorder (eraseMin tree)

Uses 9 · Used by 2

Statement usesBinary trees with cached heights · Removing the leftmost key of an AVL tree · Inorder traversal of an AVL tree · Leftmost key of a tree

Proof usesAVL rebalancing · AVL rebalancing preserves the inorder traversal · Erasing the cached heights of an AVL tree · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator

Used byInorder traversal after AVL deletion · AVL deletion keeps every other key

TheoremDeletion keeps cached heights correct#✓fully proved

Let \(t\) be a binary tree with keys from a linearly ordered type and a cached height at each node whose cached heights are correct: each node stores one more than the larger of the cached heights of its two subtrees, the empty tree having height \(0\). Then for every key \(x\), the cached heights of the tree obtained from \(t\) by deleting \(x\), rebalancing along the search path, are again correct.

public theorem cacheCorrect_erase [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : CacheCorrect tree) : CacheCorrect (erase x tree)

Uses 10 · Used by 4

Statement usesCorrect cached heights · Binary trees with cached heights · AVL tree deletion

Proof usesAVL rebalancing · AVL rebalancing preserves cached heights · Removing the minimum keeps cached heights correct · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Cached height of an AVL tree · Leftmost key of a tree

Used byDeletion preserves AVL balance · Deleting a key keeps cached heights correct · Deletion does not increase the height of an AVL tree · Deletion lowers the height of an AVL tree by at most one

TheoremDeletion does not increase the height of an AVL tree#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), and \(t\) a tree whose cached heights are correct. Then the cached height of the tree obtained by deleting \(x\) from \(t\) is at most the cached height of \(t\).

public theorem height_erase_le [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : CacheCorrect tree) : height (erase x tree) ≤ height tree

Uses 12 · Used by 2

Statement usesCorrect cached heights · Binary trees with cached heights · AVL tree deletion · Cached height of an AVL tree

Proof usesAVL rebalancing · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Upper bound on height after AVL rebalancing · Removing the leftmost key does not increase the height of an AVL tree · Leftmost key of a tree

Used byDeletion preserves AVL balance · Deletion lowers the height of an AVL tree by at most one

TheoremDeletion lowers the height of an AVL tree by at most one#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), and \(t\) a balanced tree whose cached heights are correct. Then the cached height of \(t\) is at most one more than the cached height of the tree obtained by deleting \(x\) from \(t\).

public theorem le_height_erase [LinearOrder α] {x : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    height tree ≤ height (erase x tree) + 1

Uses 17 · Used by 1

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · AVL tree deletion · Cached height of an AVL tree

Proof usesAVL rebalancing · Rebalancing when the heights of the children differ by at most one · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Deletion does not increase the height of an AVL tree · Rebalancing does not drop below the taller child · Removing the leftmost key lowers the height of an AVL tree by at most one · Leftmost key of a tree · AVL node with computed height

Used byDeletion preserves AVL balance

TheoremDeletion preserves AVL balance#✓fully proved

Let \(t\) be a binary tree with keys from a linearly ordered type and a cached height at each node, whose cached heights are correct, and which is balanced: at every node the cached heights of the two subtrees differ by at most one. Then for every key \(x\), the tree obtained from \(t\) by deleting \(x\), rebalancing along the search path, is again balanced.

public theorem balanced_erase [LinearOrder α] {x : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    Balanced (erase x tree)

Uses 17 · Used by 1

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · AVL tree deletion

Proof usesAVL rebalancing · AVL rebalancing yields a balanced tree · Removing the minimum preserves AVL balance · Deletion keeps cached heights correct · Removing the minimum keeps cached heights correct · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Cached height of an AVL tree · Removing the leftmost key does not increase the height of an AVL tree · Deletion does not increase the height of an AVL tree · Deletion lowers the height of an AVL tree by at most one · Removing the leftmost key lowers the height of an AVL tree by at most one · Leftmost key of a tree

Used byDeleting a key preserves AVL balance

TheoremAVL deletion preserves search-tree order#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type, ordered as a search tree (every key in a left subtree is smaller, and every key in a right subtree is larger, than the key at the node). Then for every key \(x\), the tree obtained by deleting \(x\) from \(T\) with rebalancing is again ordered as a search tree.

public theorem ordered_erase [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : Ordered tree) : Ordered (erase x tree)

Uses 19 · Used by 1

Statement usesOrdered AVL trees · Binary trees with cached heights · AVL tree deletion

Proof usesEvery key of an AVL tree satisfies a predicate · Membership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · Keys left after removing the minimum exceed it · AVL rebalancing · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Membership after AVL rebalancing · Leftmost key of a tree · The leftmost key lies in the tree · Rebalancing an AVL node preserves the search-tree order · Removing the leftmost key preserves search-tree order · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees

Used byDeleting a key from an ordered AVL tree keeps it ordered

TheoremInorder traversal after AVL deletion#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), and \(t\) an ordered tree. Then the inorder traversal of the tree obtained by deleting \(x\) from \(t\) is the inorder traversal of \(t\) with the first occurrence of \(x\) removed; if \(x\) does not occur, the traversal is unchanged.

public theorem inorder_erase [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : Ordered tree) : inorder (erase x tree) = (inorder tree).erase x

Uses 19 · Used by 1

Statement usesOrdered AVL trees · Binary trees with cached heights · AVL tree deletion · Inorder traversal of an AVL tree

Proof usesEvery key of an AVL tree satisfies a predicate · Membership in an AVL tree · The all-keys predicate in terms of membership (AVL trees) · AVL rebalancing · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · AVL rebalancing preserves the inorder traversal · The inorder traversal begins with the leftmost key · Membership in the inorder traversal of an AVL tree · Leftmost key of a tree · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Ordered binary trees · Inorder traversal of a binary tree · Inorder traversal of a binary tree with an accumulator

Used byInorder traversal after AVL deletion, alternative name

TheoremAVL deletion keeps every other key#✓fully proved

Let \(T\) be a binary tree with cached heights whose keys come from a linearly ordered type, and let \(x\) and \(y\) be keys with \(y \ne x\). If \(y\) occurs in \(T\), then \(y\) occurs in the tree obtained by deleting \(x\) from \(T\). No search-tree ordering of \(T\) is assumed.

public theorem mem_erase_of_mem [LinearOrder α] {x y : α} {tree : Tree α}
    (hy : y ∈ tree) (hxy : y ≠ x) : y ∈ erase x tree

Uses 13 · Used by 1

Statement usesMembership in an AVL tree · Binary trees with cached heights · AVL tree deletion

Proof usesAVL rebalancing · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Inorder traversal of an AVL tree · The inorder traversal begins with the leftmost key · Membership after AVL rebalancing · Membership in the inorder traversal of an AVL tree · Leftmost key of a tree · Erasing the cached heights of an AVL tree · Membership in a binary tree

Used byKeys of an ordered AVL tree after deletion

TheoremDeletion removes the deleted key from an ordered AVL tree#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type, ordered as a search tree. Then for every key \(x\), \(x\) does not occur in the tree obtained by deleting \(x\) from \(T\).

public theorem not_mem_erase_self [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : Ordered tree) : x ∉ erase x tree

Uses 16 · Used by 1

Statement usesMembership in an AVL tree · Ordered AVL trees · Binary trees with cached heights · AVL tree deletion

Proof usesEvery key of an AVL tree satisfies a predicate · The all-keys predicate in terms of membership (AVL trees) · AVL rebalancing · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Membership after AVL rebalancing · Leftmost key of a tree · The leftmost key lies in the tree · Erasing the cached heights of an AVL tree · A predicate holding at every key of a binary tree · Membership in a binary tree · Ordered binary trees

Used byKeys of an ordered AVL tree after deletion

TheoremKeys of an ordered AVL tree after deletion#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type, ordered as a search tree (every key in a left subtree is smaller, and every key in a right subtree is larger, than the key at the node). Then for all keys \(x\) and \(y\), \(y\) occurs in the tree obtained by deleting \(x\) from \(T\) if and only if \(y\) occurs in \(T\) and \(y \ne x\).

public theorem mem_erase [LinearOrder α] {x y : α} {tree : Tree α}
    (hTree : Ordered tree) : y ∈ erase x tree ↔ y ∈ tree ∧ y ≠ x

Uses 14

Statement usesMembership in an AVL tree · Ordered AVL trees · Binary trees with cached heights · AVL tree deletion

Proof usesAVL rebalancing · Minimum deletion in an AVL tree · Removing the leftmost key of an AVL tree · Membership after AVL rebalancing · AVL deletion keeps every other key · Leftmost key of a tree · The leftmost key lies in the tree · Deletion removes the deleted key from an ordered AVL tree · Erasing the cached heights of an AVL tree · Membership in a binary tree

TheoremDeleting a key keeps cached heights correct#✓fully proved

Let \(t\) be a binary tree with keys from a linearly ordered type and a cached height at each node whose cached heights are correct: each node stores one more than the larger of the cached heights of its two subtrees, the empty tree having height \(0\). Then for every key \(x\), the cached heights of the tree obtained from \(t\) by deleting \(x\), rebalancing along the search path, are again correct.

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

Uses 4

Statement usesCorrect cached heights · Binary trees with cached heights · AVL tree deletion under its alternative name

Proof usesDeletion keeps cached heights correct

TheoremDeleting a key preserves AVL balance#✓fully proved

Let \(t\) be a binary tree with keys from a linearly ordered type and a cached height at each node, whose cached heights are correct, and which is balanced: at every node the cached heights of the two subtrees differ by at most one. Then for every key \(x\), the tree obtained from \(t\) by deleting \(x\), rebalancing along the search path, is again balanced.

public theorem balanced_delete [LinearOrder α] {x : α} {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    Balanced (delete x tree)

Uses 5

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · AVL tree deletion under its alternative name

Proof usesDeletion preserves AVL balance

TheoremDeleting a key from an ordered AVL tree keeps it ordered#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type. If \(T\) is ordered as a search tree, then for every key \(x\) the tree obtained by deleting \(x\) from \(T\) with rebalancing is again ordered as a search tree.

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

Uses 4

Statement usesOrdered AVL trees · Binary trees with cached heights · AVL tree deletion under its alternative name

Proof usesAVL deletion preserves search-tree order

TheoremInorder traversal after AVL deletion, alternative name#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(x \in \alpha\), and \(t\) an ordered tree. Then the inorder traversal of \(\mathrm{delete}(x, t)\), the AVL deletion of \(x\) from \(t\) under its alternative name, is the inorder traversal of \(t\) with the first occurrence of \(x\) removed; if \(x\) does not occur, the traversal is unchanged.

public theorem inorder_delete [LinearOrder α] {x : α} {tree : Tree α}
    (hTree : Ordered tree) : inorder (delete x tree) = (inorder tree).erase x

Uses 5

Statement usesOrdered AVL trees · Binary trees with cached heights · AVL tree deletion under its alternative name · Inorder traversal of an AVL tree

Proof usesInorder traversal after AVL deletion

TheoremMinimum deletion keeps cached heights correct#✓fully proved

Let \(t\) be a binary tree with a cached height at each node whose cached heights are correct: each node stores one more than the larger of the cached heights of its two subtrees, the empty tree having height \(0\). Then the cached heights of the tree obtained from \(t\) by minimum deletion (removing its leftmost key, rebalancing on the way back up) are again correct.

public theorem cacheCorrect_deleteMin {tree : Tree α} (hTree : CacheCorrect tree) :
    CacheCorrect (deleteMin tree)

Uses 4

Statement usesCorrect cached heights · Binary trees with cached heights · Minimum deletion in an AVL tree

Proof usesRemoving the minimum keeps cached heights correct

TheoremMinimum deletion preserves AVL balance#✓fully proved

Let \(t\) be a binary tree with a cached height at each node whose cached heights are correct, and which is balanced: at every node the cached heights of the two subtrees differ by at most one. Then the tree obtained from \(t\) by minimum deletion (removing its leftmost key, rebalancing on the way back up) is again balanced.

public theorem balanced_deleteMin {tree : Tree α}
    (hCache : CacheCorrect tree) (hBal : Balanced tree) :
    Balanced (deleteMin tree)

Uses 5

Statement usesAVL balance invariant · Correct cached heights · Binary trees with cached heights · Minimum deletion in an AVL tree

Proof usesRemoving the minimum preserves AVL balance

TheoremSuccessor-step minimum removal preserves search-tree order#✓fully proved

Let \(T\) be a binary tree with cached heights over a linearly ordered type. If \(T\) is ordered as a search tree, then so is the tree obtained by the minimum-removal step used for the successor in deletion, which removes the leftmost key of \(T\) and rebalances on the way back up.

public theorem ordered_deleteMin [LinearOrder α] {tree : Tree α}
    (hTree : Ordered tree) : Ordered (deleteMin tree)

Uses 4

Statement usesOrdered AVL trees · Binary trees with cached heights · Minimum deletion in an AVL tree

Proof usesRemoving the leftmost key preserves search-tree order

77 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.