Correctness of van Emde Boas insertion

The recursive minimum-excluded insertion algorithm follows [Dem15], pp. 4–5. The results here concern the functional Lean implementation and its represented set, with no machine running-time claim.

Main definitions

The algorithm and recursive invariant are Tree.insert and Tree.Valid, imported from Basic.

Main results

• Tree.valid_insert: insertion of a bounded key preserves the recursive invariant.
• Tree.contains_insert: insertion represents exactly the union with the inserted key.

References

• E. Demaine, Divide and conquer: van Emde Boas trees, Lecture 4

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.contains_leaf_some (m M y : ℕ) : (leaf (some (m, M))).Contains y ↔ y = m ∨ y = M

A leaf with bounds some (m, M) contains y iff y = m or y = M.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.contains_node_some {d : ℕ} (m M : ℕ) (s : Tree d) (c : Fin (universeSize d) → Tree d) (y : ℕ) : (node (some (m, M)) s c).Contains y ↔ y = m ∨ ∃ (i : Fin (universeSize d)) (a : ℕ), (c i).Contains a ∧ y = ↑i * universeSize d + a

An internal node with bounds some (m, M) contains y iff y = m or y is in some cluster.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid.bounds_isSome_iff {d : ℕ} {t : Tree d} (ht : t.Valid) : t.bounds.isSome = true ↔ ∃ (y : ℕ), t.Contains y

A valid node is occupied exactly when it represents at least one key.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.valid_insert {d : ℕ} {t : Tree d} (ht : t.Valid) {x : ℕ} (hx : x < universeSize d) : (t.insert x).Valid

Bounded insertion preserves the recursive representation invariant.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.contains_insert {d : ℕ} {t : Tree d} (ht : t.Valid) {x : ℕ} (hx : x < universeSize d) (y : ℕ) : (t.insert x).Contains y ↔ y = x ∨ t.Contains y

The represented set after bounded insertion is exactly the old set plus the inserted key.