2–3 tree

InductiveHeight-indexed 2-3 trees#✓fully proved

For a type \(\alpha\) of keys, the 2-3 trees over \(\alpha\) indexed by height are generated as follows. The leaf is a tree of height \(0\) and stores no key. For a natural number \(h\), a key \(a\) and trees \(l\), \(r\) of height \(h\), the 2-node with separator \(a\) and children \(l\), \(r\) is a tree of height \(h + 1\). For a natural number \(h\), keys \(a\), \(b\) and trees \(l\), \(m\), \(r\) of height \(h\), the 3-node with separators \(a\), \(b\) and children \(l\), \(m\), \(r\) is a tree of height \(h + 1\). Hence all leaves of a tree of height \(h\) lie at depth \(h\).

public inductive Tree (α : Type u) : Nat → Type u where
  | leaf : Tree α 0
  | node2 {h : Nat} (a : α) (l r : Tree α h) : Tree α (h + 1)
  | node3 {h : Nat} (a b : α) (l m r : Tree α h) : Tree α (h + 1)
Used by 34
Used byPredicate on all keys of a 2-3 tree · All-keys predicate agrees with the flattening on 2-3 trees · All-keys predicate agrees with membership on 2-3 trees · Balance invariant for 2-3 trees · Every height-indexed 2-3 tree is balanced · Every rooted 2-3 tree is balanced · Search in a 2-3 tree · Search in a rooted 2-3 tree · Search in an ordered 2-3 tree is correct · Search in a rooted 2-3 tree is correct · Empty 2-3 tree · Inorder traversal of a 2-3 tree · Inorder traversal of a 2-3 tree root · Accumulated inorder traversal of a 2-3 tree · The accumulated traversal appends the suffix · Insertion into a 2-3 tree is ordered insertion into its traversal · The traversal of an ordered 2-3 tree has no duplicates · Height of a 2-3 tree · Computed height equals the height index · Insertion raises the height of a 2-3 tree by at most one · The stored height of a 2-3 tree root is its computed height · Insertion into a height-indexed 2-3 tree · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · Insertion into a 2-3 tree root · Membership in a 2-3 tree · The inorder traversal lists exactly the keys of a 2-3 tree · Ordering invariant for 2-3 trees · Ordering invariant for 2-3 trees of unspecified height · Inorder traversal of an ordered 2-3 tree is strictly increasing · Insertion preserves the ordering of 2-3 trees · Insertion results for 2-3 trees · 2-3 trees of unspecified height · Turning an insertion result into a 2-3 tree

InductiveInsertion results for 2-3 trees#✓fully proved

For a type \(\alpha\) and a natural number \(h\), an insertion result at height \(h\) is either a 2-3 tree over \(\alpha\) of height \(h\), or a split: two 2-3 trees \(l\) and \(r\) over \(\alpha\) of height \(h\) together with a promoted key \(k \in \alpha\).

It records the outcome of inserting a key into a tree of height \(h\).

public inductive Overflow (α : Type u) : Nat → Type u where
  | ok {h : Nat} (t : Tree α h) : Overflow α h
  | split {h : Nat} (l : Tree α h) (k : α) (r : Tree α h) : Overflow α h
Uses 1 · Used by 7
Statement usesHeight-indexed 2-3 trees
Used byInsertion into a 2-3 tree is ordered insertion into its traversal · Insertion raises the height of a 2-3 tree by at most one · Insertion into a height-indexed 2-3 tree · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · Insertion preserves the ordering of 2-3 trees · Turning an insertion result into a 2-3 tree

DefinitionHeight of a 2-3 tree#✓fully proved

The height of a 2-3 tree is computed along its leftmost spine: a leaf has height \(0\), and a 2-node or a 3-node has height one more than the height of its leftmost child.

public def height : {h : Nat} → Tree α h → Nat
  | _, .leaf => 0
  | _, .node2 _ l _ => height l + 1
  | _, .node3 _ _ l _ _ => height l + 1
Uses 1 · Used by 4
Statement usesHeight-indexed 2-3 trees
Used byBalance invariant for 2-3 trees · Every height-indexed 2-3 tree is balanced · Computed height equals the height index · The stored height of a 2-3 tree root is its computed height

TheoremComputed height equals the height index#✓fully proved

For every 2-3 tree \(t\) with height index \(h\), the height of \(t\) computed along its leftmost spine equals \(h\).

public theorem height_eq {h : Nat} (t : Tree α h) : height t = h
Uses 2 · Used by 2
Statement usesHeight-indexed 2-3 trees · Height of a 2-3 tree
Used byEvery height-indexed 2-3 tree is balanced · The stored height of a 2-3 tree root is its computed height

DefinitionBalance invariant for 2-3 trees#✓fully proved

A leaf is balanced, and a node is balanced when all of its subtrees are balanced and have the same computed height, where the computed height of a tree is the length of its leftmost path from the root down to a leaf. Hence all leaves of a balanced tree lie at the same depth.

public def Balanced : {h : Nat} → Tree α h → Prop
  | _, .leaf => True
  | _, .node2 _ l r => Balanced l ∧ Balanced r ∧ height l = height r
  | _, .node3 _ _ l m r =>
      Balanced l ∧ Balanced m ∧ Balanced r ∧ height l = height m ∧ height m = height r
Uses 2 · Used by 2
Statement usesHeight-indexed 2-3 trees · Height of a 2-3 tree
Used byEvery height-indexed 2-3 tree is balanced · Every rooted 2-3 tree is balanced

TheoremEvery height-indexed 2-3 tree is balanced#✓fully proved

For every height \(h\), every 2-3 tree of height \(h\) satisfies the balance invariant: at every node, the subtrees are balanced and have equal computed heights.

public theorem balanced {h : Nat} (t : Tree α h) : Balanced t
Uses 4 · Used by 1
Statement usesBalance invariant for 2-3 trees · Height-indexed 2-3 trees
Proof usesHeight of a 2-3 tree · Computed height equals the height index
Used byEvery rooted 2-3 tree is balanced

DefinitionMembership in a 2-3 tree#✓fully proved

A key \(x\) is a member of a 2-3 tree when it is one of the separator keys stored at its nodes: nothing is a member of a leaf; \(x\) is a member of a 2-node with key \(a\) and children \(l, r\) when it is a member of \(l\), equals \(a\), or is a member of \(r\); and \(x\) is a member of a 3-node with keys \(a, b\) and children \(l, m, r\) when it is a member of \(l\), equals \(a\), is a member of \(m\), equals \(b\), or is a member of \(r\).

Membership is structural and does not use the ordering invariant.

public def Mem (x : α) : {h : Nat} → Tree α h → Prop
  | _, .leaf => False
  | _, .node2 a l r => Mem x l ∨ x = a ∨ Mem x r
  | _, .node3 a b l m r => Mem x l ∨ x = a ∨ Mem x m ∨ x = b ∨ Mem x r
Uses 1 · Used by 3
Statement usesHeight-indexed 2-3 trees
Used byAll-keys predicate agrees with the flattening on 2-3 trees · All-keys predicate agrees with membership on 2-3 trees · The inorder traversal lists exactly the keys of a 2-3 tree

DefinitionPredicate on all keys of a 2-3 tree#✓fully proved

For a predicate \(p\) on keys and a 2-3 tree \(t\), \(\mathrm{All}_p(t)\) states that every separator key stored at a node of \(t\) satisfies \(p\): it is true at a leaf, and at a node it requires \(p\) of each key of the node and \(\mathrm{All}_p\) of each of its subtrees.

public def All (p : α → Prop) : {h : Nat} → Tree α h → Prop
  | _, .leaf => True
  | _, .node2 a l r => All p l ∧ p a ∧ All p r
  | _, .node3 a b l m r => All p l ∧ p a ∧ All p m ∧ p b ∧ All p r
Uses 1 · Used by 9
Statement usesHeight-indexed 2-3 trees
Used byAll-keys predicate agrees with the flattening on 2-3 trees · All-keys predicate agrees with membership on 2-3 trees · Search in an ordered 2-3 tree is correct · Insertion into a 2-3 tree is ordered insertion into its traversal · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · Ordering invariant for 2-3 trees · Inorder traversal of an ordered 2-3 tree is strictly increasing · Insertion preserves the ordering of 2-3 trees

TheoremAll-keys predicate agrees with membership on 2-3 trees#✓fully proved

For every predicate \(p\) on keys and every 2-3 tree \(t\) of height \(h\), the recursive predicate requiring \(p\) at every key stored at a node of \(t\) holds if and only if \(p(x)\) holds for every member \(x\) of \(t\), where \(x\) is a member of \(t\) when it equals one of the keys stored at some node of \(t\).

public theorem all_iff_forall_mem {p : α → Prop} {h : Nat} {t : Tree α h} :
    All p t ↔ ∀ x, x ∈ t → p x
Uses 3 · Used by 1
Statement usesPredicate on all keys of a 2-3 tree · Membership in a 2-3 tree · Height-indexed 2-3 trees
Used byAll-keys predicate agrees with the flattening on 2-3 trees

DefinitionOrdering invariant for 2-3 trees#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). The leaf is ordered. A 2-node with separator \(a\) and children \(l\), \(r\) is ordered when \(l\) and \(r\) are ordered, \(y < a\) for every key \(y\) stored in \(l\), and \(a < y\) for every key \(y\) stored in \(r\). A 3-node with separators \(a\), \(b\) and children \(l\), \(m\), \(r\) is ordered when \(l\), \(m\) and \(r\) are ordered, \(a < b\), \(y < a\) for every key \(y\) stored in \(l\), \(a < y\) and \(y < b\) for every key \(y\) stored in \(m\), and \(b < y\) for every key \(y\) stored in \(r\).

public def Ordered [LT α] : {h : Nat} → Tree α h → Prop
  | _, .leaf => True
  | _, .node2 a l r =>
      Ordered l ∧ Ordered r ∧ All (· < a) l ∧ All (a < ·) r
  | _, .node3 a b l m r =>
      Ordered l ∧ Ordered m ∧ Ordered r ∧ a < b ∧ All (· < a) l ∧
        All (a < ·) m ∧ All (· < b) m ∧ All (b < ·) r
Uses 2 · Used by 8
Statement usesPredicate on all keys of a 2-3 tree · Height-indexed 2-3 trees
Used bySearch in an ordered 2-3 tree is correct · Insertion into a 2-3 tree is ordered insertion into its traversal · The traversal of an ordered 2-3 tree has no duplicates · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · Ordering invariant for 2-3 trees of unspecified height · Inorder traversal of an ordered 2-3 tree is strictly increasing · Insertion preserves the ordering of 2-3 trees

DefinitionAccumulated inorder traversal of a 2-3 tree#✓fully proved

For a 2-3 tree \(t\) and a list \(s\), the accumulated traversal \(F(t, s)\) is defined by recursion on \(t\): for a leaf, \(F(t, s) = s\); for a 2-node with key \(a\) and children \(l, r\), \(F(t, s)\) is \(F(l, s')\) where \(s'\) is \(a\) prepended to \(F(r, s)\); for a 3-node with keys \(a, b\) and children \(l, m, r\), \(F(t, s)\) is \(F(l, s')\) where \(s'\) is \(a\) prepended to \(F(m, s'')\) and \(s''\) is \(b\) prepended to \(F(r, s)\).

The result is the inorder traversal of \(t\) followed by \(s\). It is built without recopying the traversals of left subtrees.

public def flattenAux : {h : Nat} → Tree α h → List α → List α
  | _, .leaf, suffix => suffix
  | _, .node2 a l r, suffix => flattenAux l (a :: flattenAux r suffix)
  | _, .node3 a b l m r, suffix =>
      flattenAux l (a :: flattenAux m (b :: flattenAux r suffix))
Uses 1 · Used by 7
Statement usesHeight-indexed 2-3 trees
Used bySearch in an ordered 2-3 tree is correct · Inorder traversal of a 2-3 tree · The accumulated traversal appends the suffix · Insertion into a 2-3 tree is ordered insertion into its traversal · Correctness of 2-3 tree insertion · The inorder traversal lists exactly the keys of a 2-3 tree · Inorder traversal of an ordered 2-3 tree is strictly increasing

DefinitionInorder traversal of a 2-3 tree#✓fully proved

The flattening of a 2-3 tree \(t\) is the accumulated inorder traversal of \(t\) onto the empty list. Equivalently, the flattening of a leaf is empty; that of a 2-node with key \(a\) and children \(l, r\) is the flattening of \(l\), then \(a\), then the flattening of \(r\); and that of a 3-node with keys \(a, b\) and children \(l, m, r\) is the flattening of \(l\), then \(a\), then the flattening of \(m\), then \(b\), then the flattening of \(r\).

public def flatten {h : Nat} (t : Tree α h) : List α :=
  flattenAux t []
Uses 2 · Used by 11
Statement usesHeight-indexed 2-3 trees · Accumulated inorder traversal of a 2-3 tree
Used byAll-keys predicate agrees with the flattening on 2-3 trees · Search in an ordered 2-3 tree is correct · Inorder traversal of a 2-3 tree root · The accumulated traversal appends the suffix · Insertion into a 2-3 tree is ordered insertion into its traversal · The traversal of an ordered 2-3 tree has no duplicates · Insertion specification for 2-3 trees · Correctness of 2-3 tree insertion · The inorder traversal lists exactly the keys of a 2-3 tree · Inorder traversal of an ordered 2-3 tree is strictly increasing · Insertion preserves the ordering of 2-3 trees

TheoremThe accumulated traversal appends the suffix#✓fully proved

For every 2-3 tree \(t\) (of any height) and every list \(s\), the accumulated inorder traversal of \(t\) onto \(s\) equals the flattening of \(t\) followed by \(s\).

public theorem flattenAux_eq {h : Nat} (t : Tree α h) (suffix : List α) :
    flattenAux t suffix = flatten t ++ suffix
Uses 3
Statement usesHeight-indexed 2-3 trees · Inorder traversal of a 2-3 tree · Accumulated inorder traversal of a 2-3 tree

TheoremThe inorder traversal lists exactly the keys of a 2-3 tree#✓fully proved

For every 2-3 tree \(t\) of height \(h\) and every key \(x\), \(x\) occurs in the inorder traversal of \(t\) if and only if \(x\) is a member of \(t\), that is, one of the separator keys stored at its nodes.

public theorem mem_flatten {x : α} {h : Nat} {t : Tree α h} :
    x ∈ flatten t ↔ x ∈ t
Uses 4 · Used by 1
Statement usesMembership in a 2-3 tree · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree
Proof usesAccumulated inorder traversal of a 2-3 tree
Used byAll-keys predicate agrees with the flattening on 2-3 trees

TheoremAll-keys predicate agrees with the flattening on 2-3 trees#✓fully proved

For every predicate \(p\) on keys and every 2-3 tree \(t\) of height \(h\), every key stored at a node of \(t\) satisfies \(p\) if and only if every element of the inorder flattening of \(t\) satisfies \(p\).

public theorem all_iff_forall_flatten {p : α → Prop} {h : Nat} {t : Tree α h} :
    All p t ↔ ∀ y ∈ flatten t, p y
Uses 6 · Used by 3
Statement usesPredicate on all keys of a 2-3 tree · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree
Proof usesMembership in a 2-3 tree · All-keys predicate agrees with membership on 2-3 trees · The inorder traversal lists exactly the keys of a 2-3 tree
Used bySearch in an ordered 2-3 tree is correct · Correctness of 2-3 tree insertion · Inorder traversal of an ordered 2-3 tree is strictly increasing

TheoremInorder traversal of an ordered 2-3 tree is strictly increasing#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every natural number \(h\) and every ordered 2-3 tree \(t\) over \(\alpha\) of height \(h\), the flattening (inorder traversal) of \(t\) is strictly increasing: whenever a key \(x\) occurs before a key \(y\) in it, \(x < y\).

public theorem ordered_flatten_pairwise [LinearOrder α] {h : Nat} {t : Tree α h}
    (hOrd : Ordered t) : List.Pairwise (· < ·) (flatten t)
Uses 6 · Used by 1
Statement usesOrdering invariant for 2-3 trees · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree
Proof usesPredicate on all keys of a 2-3 tree · All-keys predicate agrees with the flattening on 2-3 trees · Accumulated inorder traversal of a 2-3 tree
Used byThe traversal of an ordered 2-3 tree has no duplicates

TheoremThe traversal of an ordered 2-3 tree has no duplicates#✓fully proved

If the keys are linearly ordered and a 2-3 tree \(t\) (of any height) is ordered, then no key occurs twice in the flattening of \(t\).

public theorem flatten_nodup [LinearOrder α] {h : Nat} {t : Tree α h}
    (hOrd : Ordered t) : (flatten t).Nodup
Uses 4
Statement usesOrdering invariant for 2-3 trees · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree
Proof usesInorder traversal of an ordered 2-3 tree is strictly increasing

DefinitionSearch in a 2-3 tree#✓fully proved

For a linearly ordered key type, searching a 2-3 tree for a key \(x\) returns false at a leaf. At a 2-node with key \(a\), it searches the left subtree if \(x < a\), otherwise the right subtree if \(a < x\), and otherwise returns true. At a 3-node with keys \(a\) and \(b\), it searches the left subtree if \(x < a\); otherwise, if \(a < x\), it searches the middle subtree if \(x < b\), otherwise the right subtree if \(b < x\), and otherwise returns true; if neither \(x < a\) nor \(a < x\), it returns true.

public def contains [LinearOrder α] (x : α) : {h : Nat} → Tree α h → Bool
  | _, .leaf => false
  | _, .node2 a l r =>
      if x < a then contains x l
      else if a < x then contains x r
      else true
  | _, .node3 a b l m r =>
      if x < a then contains x l
      else if a < x then
        if x < b then contains x m
        else if b < x then contains x r
        else true
      else true
Uses 1 · Used by 2
Statement usesHeight-indexed 2-3 trees
Used bySearch in a rooted 2-3 tree · Search in an ordered 2-3 tree is correct

TheoremSearch in an ordered 2-3 tree is correct#✓fully proved

Let the keys be linearly ordered and let \(t\) be a 2-3 tree of height \(h\) that satisfies the ordering invariant. Then searching \(t\) for a key \(x\) returns true if and only if \(x\) occurs in the inorder flattening of \(t\).

public theorem contains_eq_true_iff [LinearOrder α] {x : α} {h : Nat} {t : Tree α h}
    (hOrd : Ordered t) : contains x t = true ↔ x ∈ flatten t
Uses 7 · Used by 1
Statement usesOrdering invariant for 2-3 trees · Height-indexed 2-3 trees · Search in a 2-3 tree · Inorder traversal of a 2-3 tree
Proof usesPredicate on all keys of a 2-3 tree · All-keys predicate agrees with the flattening on 2-3 trees · Accumulated inorder traversal of a 2-3 tree
Used bySearch in a rooted 2-3 tree is correct

DefinitionInsertion into a height-indexed 2-3 tree#✓fully proved

Inserting a key \(x\) into a 2-3 tree of height \(h\) yields either a single tree of height \(h\) or a split into two trees of height \(h\) around a promoted key. Inserting into a leaf gives the split of two leaves around \(x\). At a 2-node with key \(a\), insertion recurses into the left child if \(x < a\) and into the right child if \(a < x\); a returned tree replaces that child, and a returned split around \(k\) is absorbed by turning the node into a 3-node with keys \(k, a\) (left) or \(a, k\) (right). At a 3-node with keys \(a, b\), insertion recurses into the left child if \(x < a\), the middle child if \(a < x < b\), and the right child if \(a < x\) and \(b < x\); a returned tree replaces that child, and a returned split makes the node split into two 2-nodes, promoting \(a\), the child's promoted key, or \(b\) respectively. In the remaining cases \(x\) equals a key of the node and the tree is returned unchanged.

Cslib.Algorithms.Lean.TwoThreeTree.ins · 28 lines 
public def ins [LinearOrder α] (x : α) : {h : Nat} → Tree α h → Overflow α h
  | _, .leaf => .split .leaf x .leaf
  | _, .node2 a l r =>
      if x < a then
        match ins x l with
        | .ok l' => .ok (.node2 a l' r)
        | .split l₁ k l₂ => .ok (.node3 k a l₁ l₂ r)
      else if a < x then
        match ins x r with
        | .ok r' => .ok (.node2 a l r')
        | .split r₁ k r₂ => .ok (.node3 a k l r₁ r₂)
      else .ok (.node2 a l r)
  | _, .node3 a b l m r =>
      if x < a then
        match ins x l with
        | .ok l' => .ok (.node3 a b l' m r)
        | .split l₁ k l₂ => .split (.node2 k l₁ l₂) a (.node2 b m r)
      else if a < x then
        if x < b then
          match ins x m with
          | .ok m' => .ok (.node3 a b l m' r)
          | .split m₁ k m₂ => .split (.node2 a l m₁) k (.node2 b m₂ r)
        else if b < x then
          match ins x r with
          | .ok r' => .ok (.node3 a b l m r')
          | .split r₁ k r₂ => .split (.node2 a l m) b (.node2 k r₁ r₂)
        else .ok (.node3 a b l m r)
      else .ok (.node3 a b l m r)
Uses 2 · Used by 5
Statement usesInsertion results for 2-3 trees · Height-indexed 2-3 trees
Used byInsertion into a 2-3 tree is ordered insertion into its traversal · Insertion raises the height of a 2-3 tree by at most one · Correctness of 2-3 tree insertion · Insertion into a 2-3 tree root · Insertion preserves the ordering of 2-3 trees

DefinitionInsertion specification for 2-3 trees#✓fully proved

Let \(\alpha\) be linearly ordered, let \(x \in \alpha\), and let \(t\) be a 2-3 tree of height \(h\). An insertion result of height \(h\) meets the specification for inserting \(x\) into \(t\) when the following holds. If it is a single tree \(t'\) of height \(h\), then \(t'\) is ordered and its inorder traversal equals the ordered insertion of \(x\) into the inorder traversal of \(t\). If it is a split into trees \(l\) and \(r\) of height \(h\) around a promoted key \(k\), then \(l\) and \(r\) are ordered, every key of \(l\) is less than \(k\), every key of \(r\) is greater than \(k\), and the traversal of \(l\) followed by \(k\) and then the traversal of \(r\) equals the ordered insertion of \(x\) into the inorder traversal of \(t\).

public def InsSpec [LinearOrder α] (x : α) {h : Nat} (t : Tree α h) :
    Overflow α h → Prop
  | .ok t' => Ordered t' ∧ flatten t' = orderedInsert x (flatten t)
  | .split l k r =>
      Ordered l ∧ Ordered r ∧ All (· < k) l ∧ All (k < ·) r ∧
        flatten l ++ k :: flatten r = orderedInsert x (flatten t)
Uses 6 · Used by 3
Statement usesPredicate on all keys of a 2-3 tree · Ordering invariant for 2-3 trees · Insertion results for 2-3 trees · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree · Ordered insertion into a list
Used byInsertion into a 2-3 tree is ordered insertion into its traversal · Correctness of 2-3 tree insertion · Insertion preserves the ordering of 2-3 trees

TheoremCorrectness of 2-3 tree insertion#✓fully proved

Let \(\alpha\) be linearly ordered, let \(x \in \alpha\), and let \(t\) be an ordered 2-3 tree of height \(h\). Then inserting \(x\) into \(t\) meets the insertion specification. If the insertion returns a single tree \(t'\) of height \(h\), then \(t'\) is ordered and its inorder traversal is the ordered insertion of \(x\) into the inorder traversal of \(t\). If it returns a split into trees \(l\) and \(r\) of height \(h\) around a promoted key \(k\), then \(l\) and \(r\) are ordered, every key of \(l\) is less than \(k\), every key of \(r\) is greater than \(k\), and the traversal of \(l\) followed by \(k\) and then the traversal of \(r\) is the ordered insertion of \(x\) into the inorder traversal of \(t\).

Balance is automatic from the height index.

public theorem ins_spec [LinearOrder α] (x : α) :
    ∀ {h : Nat} (t : Tree α h), Ordered t → InsSpec x t (ins x t)
Uses 10 · Used by 2
Statement usesInsertion specification for 2-3 trees · Ordering invariant for 2-3 trees · Height-indexed 2-3 trees · Insertion into a height-indexed 2-3 tree
Proof usesPredicate on all keys of a 2-3 tree · Insertion results for 2-3 trees · All-keys predicate agrees with the flattening on 2-3 trees · Inorder traversal of a 2-3 tree · Accumulated inorder traversal of a 2-3 tree · Ordered insertion into a list
Used byInsertion into a 2-3 tree is ordered insertion into its traversal · Insertion preserves the ordering of 2-3 trees

Structure2-3 trees of unspecified height#✓fully proved

For a type \(\alpha\), a 2-3 tree of unspecified height over \(\alpha\) is a pair \((h, t)\) of a natural number \(h\) and a height-indexed 2-3 tree \(t\) over \(\alpha\) of height \(h\).

It serves as a standalone search tree.

public structure Root (α : Type u) where
  /-- The height of the underlying tree. -/
  height : Nat
  /-- The underlying height-indexed tree. -/
  tree : Tree α height
Uses 1 · Used by 14
Statement usesHeight-indexed 2-3 trees
Used byEvery rooted 2-3 tree is balanced · Search in a rooted 2-3 tree · Search in a rooted 2-3 tree is correct · Empty 2-3 tree · Inorder traversal of a 2-3 tree root · Insertion into a 2-3 tree is ordered insertion into its traversal · Building a 2-3 tree from a list · Insertion raises the height of a 2-3 tree by at most one · The stored height of a 2-3 tree root is its computed height · Insertion into a 2-3 tree root · Keys after insertion into a 2-3 tree · Ordering invariant for 2-3 trees of unspecified height · Insertion preserves the ordering of 2-3 trees · Turning an insertion result into a 2-3 tree

DefinitionTurning an insertion result into a 2-3 tree#✓fully proved

An insertion result at height \(h\) becomes a 2-3 tree of unspecified height as follows: a tree \(t\) of height \(h\) gives \(t\) itself, of height \(h\), and a split into trees \(l\), \(r\) of height \(h\) around a key \(k\) gives the 2-node with separator \(k\), left child \(l\) and right child \(r\), of height \(h + 1\).

public def Overflow.toRoot : {h : Nat} → Overflow α h → Root α
  | _, .ok t => ⟨_, t⟩
  | _, .split l k r => ⟨_, .node2 k l r⟩
Uses 3 · Used by 1
Statement usesInsertion results for 2-3 trees · 2-3 trees of unspecified height · Height-indexed 2-3 trees
Used byInsertion into a 2-3 tree root

DefinitionEmpty 2-3 tree#✓fully proved

The empty 2-3 tree is the root of height \(0\) whose underlying tree is the leaf.

public def Root.empty : Root α :=
  ⟨0, Tree.leaf⟩
Uses 2 · Used by 2
Statement uses2-3 trees of unspecified height · Height-indexed 2-3 trees
Used byBuilding a 2-3 tree from a list · The empty 2-3 tree is ordered

DefinitionInorder traversal of a 2-3 tree root#✓fully proved

The flattening of a 2-3 tree root is the flattening of its underlying tree, that is, the list of its keys in inorder.

public def Root.flatten (t : Root α) : List α :=
  TwoThreeTree.flatten t.tree
Uses 3 · Used by 4
Statement uses2-3 trees of unspecified height · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree
Used bySearch in a rooted 2-3 tree is correct · Insertion into a 2-3 tree is ordered insertion into its traversal · Keys after insertion into a 2-3 tree · Keys of a 2-3 tree built from a list

DefinitionSearch in a rooted 2-3 tree#✓fully proved

For a linearly ordered key type, searching a root (a 2-3 tree packaged with its height) for a key \(x\) returns the Boolean result of the 2-3 tree search for \(x\) in the underlying height-indexed tree.

public def Root.contains [LinearOrder α] (x : α) (t : Root α) : Bool :=
  TwoThreeTree.contains x t.tree
Uses 3 · Used by 1
Statement uses2-3 trees of unspecified height · Height-indexed 2-3 trees · Search in a 2-3 tree
Used bySearch in a rooted 2-3 tree is correct

DefinitionOrdering invariant for 2-3 trees of unspecified height#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). A 2-3 tree of unspecified height over \(\alpha\) is ordered when its underlying height-indexed 2-3 tree satisfies the ordering invariant.

public def Root.Ordered [LT α] (t : Root α) : Prop :=
  TwoThreeTree.Ordered t.tree
Uses 3 · Used by 6
Statement usesOrdering invariant for 2-3 trees · 2-3 trees of unspecified height · Height-indexed 2-3 trees
Used bySearch in a rooted 2-3 tree is correct · Insertion into a 2-3 tree is ordered insertion into its traversal · Keys after insertion into a 2-3 tree · The empty 2-3 tree is ordered · Building a 2-3 tree from a list gives an ordered tree · Insertion preserves the ordering of 2-3 trees

DefinitionInsertion into a 2-3 tree root#✓fully proved

To insert a key \(x\) into a root, that is, a 2-3 tree together with its height \(h\), insert \(x\) into the underlying tree. If this returns a single tree of height \(h\), that tree is the new root, of height \(h\). If it returns a split into trees \(l\) and \(r\) around a key \(k\), the new root is the 2-node with key \(k\) and children \(l\) and \(r\), of height \(h + 1\).

public def Root.insert [LinearOrder α] (x : α) (t : Root α) : Root α :=
  Overflow.toRoot (ins x t.tree)
Uses 4 · Used by 6
Statement usesTurning an insertion result into a 2-3 tree · 2-3 trees of unspecified height · Height-indexed 2-3 trees · Insertion into a height-indexed 2-3 tree
Used byInsertion into a 2-3 tree is ordered insertion into its traversal · Building a 2-3 tree from a list · Insertion raises the height of a 2-3 tree by at most one · Keys after insertion into a 2-3 tree · Keys of a 2-3 tree built from a list · Insertion preserves the ordering of 2-3 trees

TheoremThe empty 2-3 tree is ordered#✓fully proved

For every type \(\alpha\) with a relation \(<\), the empty 2-3 tree of unspecified height over \(\alpha\) (the leaf, of height \(0\)) satisfies the ordering invariant.

public theorem Root.ordered_empty [LT α] : (Root.empty : Root α).Ordered
Uses 2 · Used by 1
Statement usesOrdering invariant for 2-3 trees of unspecified height · Empty 2-3 tree
Used byBuilding a 2-3 tree from a list gives an ordered tree

TheoremThe stored height of a 2-3 tree root is its computed height#✓fully proved

For every root \(t\), that is, a 2-3 tree together with its height index, the height of the underlying tree computed along its leftmost spine equals the stored height of \(t\).

public theorem Root.height_tree (t : Root α) :
    TwoThreeTree.height t.tree = t.height
Uses 4
Statement uses2-3 trees of unspecified height · Height-indexed 2-3 trees · Height of a 2-3 tree
Proof usesComputed height equals the height index

TheoremEvery rooted 2-3 tree is balanced#✓fully proved

For every root, that is, a 2-3 tree packaged with its height, the underlying height-indexed tree satisfies the balance invariant.

public theorem Root.balanced (t : Root α) : Balanced t.tree
Uses 4
Statement usesBalance invariant for 2-3 trees · 2-3 trees of unspecified height · Height-indexed 2-3 trees
Proof usesEvery height-indexed 2-3 tree is balanced

TheoremInsertion preserves the ordering of 2-3 trees#✓fully proved

Let \(\alpha\) be a linearly ordered type. If \(t\) is an ordered 2-3 tree of unspecified height over \(\alpha\) and \(x \in \alpha\), then the tree obtained by inserting \(x\) into \(t\) is ordered.

public theorem Root.ordered_insert [LinearOrder α] {x : α} {t : Root α}
    (hOrd : t.Ordered) : (t.insert x).Ordered
Uses 12 · Used by 1
Statement uses2-3 trees of unspecified height · Ordering invariant for 2-3 trees of unspecified height · Insertion into a 2-3 tree root
Proof usesPredicate on all keys of a 2-3 tree · Insertion specification for 2-3 trees · Ordering invariant for 2-3 trees · Insertion results for 2-3 trees · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree · Insertion into a height-indexed 2-3 tree · Correctness of 2-3 tree insertion · Ordered insertion into a list
Used byBuilding a 2-3 tree from a list gives an ordered tree

TheoremInsertion into a 2-3 tree is ordered insertion into its traversal#✓fully proved

Let the keys be linearly ordered, let \(t\) be an ordered 2-3 tree root and let \(x\) be a key. Then the flattening of the root obtained by inserting \(x\) into \(t\) equals the ordered insertion of \(x\) into the flattening of \(t\).

public theorem Root.flatten_insert [LinearOrder α] {x : α} {t : Root α}
    (hOrd : t.Ordered) : (t.insert x).flatten = orderedInsert x t.flatten
Uses 14 · Used by 1
Statement uses2-3 trees of unspecified height · Ordering invariant for 2-3 trees of unspecified height · Inorder traversal of a 2-3 tree root · Insertion into a 2-3 tree root · Ordered insertion into a list
Proof usesPredicate on all keys of a 2-3 tree · Insertion specification for 2-3 trees · Ordering invariant for 2-3 trees · Insertion results for 2-3 trees · Height-indexed 2-3 trees · Inorder traversal of a 2-3 tree · Accumulated inorder traversal of a 2-3 tree · Insertion into a height-indexed 2-3 tree · Correctness of 2-3 tree insertion
Used byKeys after insertion into a 2-3 tree

TheoremKeys after insertion into a 2-3 tree#✓fully proved

Let \(\alpha\) be linearly ordered and let \(t\) be an ordered 2-3 tree root over \(\alpha\). For all \(x, y \in \alpha\), \(y\) occurs in the inorder traversal of the root obtained by inserting \(x\) into \(t\) if and only if \(y = x\) or \(y\) occurs in the inorder traversal of \(t\).

public theorem Root.mem_flatten_insert [LinearOrder α] {x y : α} {t : Root α}
    (hOrd : t.Ordered) : y ∈ (t.insert x).flatten ↔ y = x ∨ y ∈ t.flatten
Uses 7 · Used by 1
Statement uses2-3 trees of unspecified height · Ordering invariant for 2-3 trees of unspecified height · Inorder traversal of a 2-3 tree root · Insertion into a 2-3 tree root
Proof usesInsertion into a 2-3 tree is ordered insertion into its traversal · Members after ordered insertion · Ordered insertion into a list
Used byKeys of a 2-3 tree built from a list

TheoremSearch in a rooted 2-3 tree is correct#✓fully proved

Let the keys be linearly ordered and let \(t\) be a root (a 2-3 tree packaged with its height) whose underlying tree satisfies the ordering invariant. Then searching \(t\) for a key \(x\) returns true if and only if \(x\) occurs in the inorder flattening of \(t\).

public theorem Root.contains_eq_true_iff [LinearOrder α] {x : α} {t : Root α}
    (hOrd : t.Ordered) : t.contains x = true ↔ x ∈ t.flatten
Uses 6
Statement uses2-3 trees of unspecified height · Ordering invariant for 2-3 trees of unspecified height · Search in a rooted 2-3 tree · Inorder traversal of a 2-3 tree root
Proof usesHeight-indexed 2-3 trees · Search in an ordered 2-3 tree is correct

TheoremInsertion raises the height of a 2-3 tree by at most one#✓fully proved

For linearly ordered keys, every key \(x\) and every 2-3 tree root \(t\), the stored height of the root obtained by inserting \(x\) into \(t\) is at most the stored height of \(t\) plus one.

public theorem Root.height_insert_le [LinearOrder α] (x : α) (t : Root α) :
    (t.insert x).height ≤ t.height + 1
Uses 5
Statement uses2-3 trees of unspecified height · Insertion into a 2-3 tree root
Proof usesInsertion results for 2-3 trees · Height-indexed 2-3 trees · Insertion into a height-indexed 2-3 tree

DefinitionBuilding a 2-3 tree from a list#✓fully proved

For linearly ordered keys, the 2-3 tree root built from a list is defined by recursion: the empty list gives the empty 2-3 tree, and a list with head \(x\) and tail \(xs\) gives the result of inserting \(x\) into the root built from \(xs\). Thus the elements are inserted into the empty tree from the last to the first.

public def Root.fromList [LinearOrder α] : List α → Root α
  | [] => .empty
  | x :: xs => Root.insert x (Root.fromList xs)
Uses 3 · Used by 2
Statement uses2-3 trees of unspecified height · Empty 2-3 tree · Insertion into a 2-3 tree root
Used byKeys of a 2-3 tree built from a list · Building a 2-3 tree from a list gives an ordered tree

TheoremBuilding a 2-3 tree from a list gives an ordered tree#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every list \(L\) of elements of \(\alpha\), the 2-3 tree of unspecified height built from \(L\), by inserting the elements of \(L\) from right to left into the empty tree, is ordered.

public theorem Root.ordered_fromList [LinearOrder α] (xs : List α) :
    (Root.fromList xs).Ordered
Uses 4 · Used by 1
Statement usesOrdering invariant for 2-3 trees of unspecified height · Building a 2-3 tree from a list
Proof usesThe empty 2-3 tree is ordered · Insertion preserves the ordering of 2-3 trees
Used byKeys of a 2-3 tree built from a list

TheoremKeys of a 2-3 tree built from a list#✓fully proved

Let \(\alpha\) be linearly ordered. For every list \(L\) over \(\alpha\) and every \(x \in \alpha\), \(x\) occurs in the inorder traversal of the 2-3 tree built from \(L\) (by inserting its elements from right to left into the empty tree) if and only if \(x\) occurs in \(L\).

public theorem Root.mem_fromList [LinearOrder α] {x : α} {xs : List α} :
    x ∈ (Root.fromList xs).flatten ↔ x ∈ xs
Uses 5
Statement usesInorder traversal of a 2-3 tree root · Building a 2-3 tree from a list
Proof usesInsertion into a 2-3 tree root · Keys after insertion into a 2-3 tree · Building a 2-3 tree from a list gives an ordered tree
40 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.