Recursive van Emde Boas sets

The universe at depth d is [0, 2 ^ (2 ^ d)). Each internal node stores its minimum outside its clusters, caches its maximum, and records nonempty clusters in a recursive summary. This is the recursive variant presented in Demaine's lecture notes, not the stratified-tree implementation of van Emde Boas, Kaas and Zijlstra. The lecture notes credit Michael Bender for a 2001 personal communication.

The functions here are Lean algorithms. Immutable function updates, pattern matching and recursive calls have no certified machine cost. The separate word-RAM realization must charge instructions, initialization and memory before any machine running-time claim is made.

Main definitions

• Tree: a fully allocated recursive shape, with a two-key base universe.
• Tree.empty, Tree.insert, Tree.member, Tree.successor: set operations.
• Tree.Contains: mathematical interpretation of the stored keys.
• Tree.Valid: the recursive extrema, cluster and summary invariant.

References

• P. van Emde Boas, R. Kaas and E. Zijlstra, Design and implementation of an efficient priority queue
• E. Demaine, Divide and conquer: van Emde Boas trees, Lecture 4

inductive Cslib.Algorithms.Lean.VanEmdeBoas.Tree : ℕ → Type

The extrema use one shared presence bit. A present pair stores minimum and maximum.

• leaf (bounds : Option (ℕ × ℕ)) : Tree 0

  A node for the universe {0, 1}.

• node {d : ℕ} (bounds : Option (ℕ × ℕ)) (summary : Tree d) (cluster : Fin (universeSize d) → Tree d) : Tree (d + 1)

  A node with a recursive summary and a direct-indexed array of clusters.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.bounds {d : ℕ} : Tree d → Option (ℕ × ℕ)

Cached extrema; none denotes an empty node.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.minimum {d : ℕ} (t : Tree d) : Option ℕ

Cached minimum, without a search through clusters.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.maximum {d : ℕ} (t : Tree d) : Option ℕ

Cached maximum, without a search through clusters.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.withBounds {d : ℕ} : Tree d → Option (ℕ × ℕ) → Tree d

Change only the local extrema. A caller must justify the children and summary invariant.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.empty (d : ℕ) : Tree d

The fully allocated empty tree. Allocation cost is not measured in this Lean definition.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.member {d : ℕ} : Tree d → ℕ → Bool

Set membership. On valid trees, arguments outside the universe are rejected.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.insert {d : ℕ} : Tree d → ℕ → Tree d

Insert a bounded key. Repeated insertion of the local minimum does no recursive work. For an empty cluster, its first element is installed directly and only the summary recurses.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor {d : ℕ} : Tree d → ℕ → Option ℕ

The least stored key strictly greater than the query, or none if it does not exist. The cached maximum chooses between one cluster recursion and one summary recursion.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Contains {d : ℕ} : Tree d → ℕ → Prop

Mathematical interpretation. The minimum is absent from the cluster interpretation.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Extrema {d : ℕ} (t : Tree d) : Prop

The local extrema correctly describe a bounded set of keys.

def Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid {d : ℕ} : Tree d → Prop

Recursive invariant: bounded extrema, valid children and summary, exact summary occupancy, and strict exclusion of the local minimum from every cluster.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.bounds_empty (d : ℕ) : (empty d).bounds = none

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.minimum_empty (d : ℕ) : (empty d).minimum = none

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.maximum_empty (d : ℕ) : (empty d).maximum = none

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.contains_empty (d x : ℕ) : ¬(empty d).Contains x

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.valid_empty (d : ℕ) : (empty d).Valid

The representation invariant has a concrete instance at every depth.

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.member_empty (d x : ℕ) : (empty d).member x = false

@[simp]

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.successor_empty (d x : ℕ) : (empty d).successor x = none

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid.extrema {d : ℕ} {t : Tree d} (h : t.Valid) : t.Extrema

Every valid tree has correctly bounded extrema.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid.contains_lt {d : ℕ} {t : Tree d} (h : t.Valid) {x : ℕ} (hx : t.Contains x) : x < universeSize d

Stored keys lie in the advertised bounded universe.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.not_contains_of_bounds_none {d : ℕ} {t : Tree d} (hb : t.bounds = none) (x : ℕ) : ¬t.Contains x

An empty local header has no represented elements.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid.contains_minimum {d : ℕ} {t : Tree d} (h : t.Valid) {m M : ℕ} (hb : t.bounds = some (m, M)) : t.Contains m

An occupied valid node has a represented cached minimum.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.Valid.contains_maximum {d : ℕ} {t : Tree d} (h : t.Valid) {m M : ℕ} (hb : t.bounds = some (m, M)) : t.Contains M

An occupied valid node has a represented cached maximum.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.cluster_coordinates {u i y : ℕ} (hu : 0 < u) (hy : y < u) : (i * u + y) / u = i ∧ (i * u + y) % u = y

Division and remainder recover a cluster's coordinates for bounded low parts.

theorem Cslib.Algorithms.Lean.VanEmdeBoas.Tree.member_iff_contains {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) : t.member x = true ↔ t.Contains x

Boolean lookup agrees with the mathematical interpretation of every valid tree.