Correctness of strict van Emde Boas successor

The recursive algorithm returns the least represented key strictly greater than its query. Queries may lie outside the represented universe; failure means that every represented key is at most the query. These are mathematical correctness statements, without a machine cost claim.

Main definitions

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

Main results

• Tree.successor_spec: the successful and unsuccessful result specifications.
• Tree.successor_eq_some_iff: success is equivalent to being the least greater stored key.
• Tree.successor_eq_none_iff: failure is equivalent to having no greater stored key.
• Tree.successor_isSome_of_lt_max: a query strictly below the cached maximum always has a strict successor in [0, universeSize d).

References

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

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor_spec {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) : match t.successor x with | some y => t.Contains y ∧ x < y ∧ ∀ (z : ℕ), t.Contains z → x < z → y ≤ z | none => ∀ (z : ℕ), t.Contains z → z ≤ x

A returned key is the least represented key strictly above the query; failure certifies that every represented key is at most the query. No bound on the query is required.

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

A successful result is exactly the least represented key strictly greater than the query.

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

Failure is exactly the absence of a represented key strictly above the query.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor_isSome_of_lt_max {d m M query : ℕ} {tree : Tree d} (ht : tree.Valid) (hb : tree.bounds = some (m, M)) (hq : query < M) : ∃ ans < universeSize d, tree.successor query = some ans

A valid node with a query strictly below its cached maximum always has a strict successor in [0, universeSize d).