Finite-set abstraction of recursive van Emde Boas trees

The finite set below is a mathematical observation of the recursive representation. The operations do not enumerate this finite set. No execution-time bound is attached to constructing the observation.

Main definitions

• Tree.elements: the bounded keys represented by a tree.

Main results

• Tree.mem_elements_iff: the finite set agrees with the recursive mathematical interpretation.
• Tree.elements_insert: insertion adds exactly one key to the finite set.
• Tree.successor_elements_some_iff, Tree.successor_elements_none_iff: strict successor and its absence are characterized by the finite set.

References

The representation and its source credit are described in Complexity.Algorithms.Lean.VanEmdeBoas.Basic.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.elements {d : ℕ} (t : Tree d) : Finset ℕ

Mathematical finite-set abstraction; this enumeration is not used by the operations.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.mem_elements_iff {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) : x ∈ t.elements ↔ t.Contains x

The finite observation includes exactly the recursively represented keys.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.elements_empty (d : ℕ) : (empty d).elements = ∅

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

The finite-set observation commutes with bounded insertion.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor_elements_some_iff {d : ℕ} {t : Tree d} (ht : t.Valid) (x y : ℕ) : t.successor x = some y ↔ y ∈ t.elements ∧ x < y ∧ ∀ z ∈ t.elements, x < z → y ≤ z

A successful successor is the least finite-set element strictly above the query.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor_elements_none_iff {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) : t.successor x = none ↔ ∀ z ∈ t.elements, z ≤ x

An absent successor means that every finite-set element is at most the query.