Van Emde Boas tree

44 fully proved

Van Emde Boas

StructureTwo-level van Emde Boas tree#✓fully proved

For a natural number \(m\), a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) consists of a summary bit vector of length \(m\) and, for each \(i < m\), a cluster bit vector of length \(m\); bit \(j\) of cluster \(i\) records whether the element \(im + j\) is stored. Unlike the fully recursive van Emde Boas tree over universes of size \(2^{2^k}\), the summary and the clusters here are plain bit vectors, not van Emde Boas trees.

public structure VanEmdeBoas (m : Nat) where
  /-- Bit `i` records whether cluster `i` contains a stored element. -/
  summary : Fin m → Bool
  /-- `clusters i j` records whether the element `i * m + j` is stored. -/
  clusters : Fin m → Fin m → Bool

Used by 36

Used bySet of stored elements of a van Emde Boas tree · Contents of the empty van Emde Boas tree · Contents after insertion into a van Emde Boas tree · Empty van Emde Boas tree · Insertion into a van Emde Boas tree · Maximum query of a van Emde Boas tree · When the van Emde Boas maximum query returns nothing · Correctness of the van Emde Boas maximum query · The van Emde Boas maximum query bounds every member · The maximum query of a van Emde Boas tree returns a member · The contents of a van Emde Boas tree are its members · Membership in a van Emde Boas tree · Membership after insertion into a van Emde Boas tree · Insertion into a van Emde Boas tree keeps existing members · Insertion into a van Emde Boas tree leaves other elements unchanged · An inserted element is a member of a van Emde Boas tree · Minimum query of a van Emde Boas tree · Empty minimum query in a van Emde Boas tree · Characterization of the van Emde Boas minimum · The van Emde Boas minimum is a lower bound · The van Emde Boas minimum is stored · Predecessor query in a two-level van Emde Boas tree · Empty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor · Maximality of the van Emde Boas predecessor · The van Emde Boas predecessor is strictly smaller than its argument · The van Emde Boas predecessor is stored · Successor query in a two-level van Emde Boas tree · A van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member · The van Emde Boas successor is strictly larger than its argument · No member lies strictly between an element and its van Emde Boas successor · The van Emde Boas successor is stored · Summary invariant of a van Emde Boas tree · The empty van Emde Boas tree is valid · Insertion preserves validity of van Emde Boas trees

DefinitionEmpty van Emde Boas tree#✓fully proved

For a natural number \(m\), the empty van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) is the tree in which all \(m\) summary bits and all \(m^2\) cluster bits (\(m\) clusters of \(m\) bits each) are unset.

public def empty {m : Nat} : VanEmdeBoas m where
  summary := fun _ => false
  clusters := fun _ _ => false

Uses 1 · Used by 9

Statement usesTwo-level van Emde Boas tree

Used byContents of the empty van Emde Boas tree · Maximum query on the empty van Emde Boas tree · Maximum query on a one-element van Emde Boas tree · The empty van Emde Boas tree has no members · The empty van Emde Boas tree has no minimum · Minimum of a one-element van Emde Boas tree · Predecessor queries in the empty van Emde Boas tree · The empty van Emde Boas tree has no successors · The empty van Emde Boas tree is valid

DefinitionMembership in a van Emde Boas tree#✓fully proved

An element \(x\) of the universe \(\{0, 1, \dots, m^2 - 1\}\) is a member of a two-level van Emde Boas tree \(t\) when bit \(x \bmod m\) of cluster \(\lfloor x / m \rfloor\) of \(t\) is set. The summary bits are not consulted.

public def member {m : Nat} (t : VanEmdeBoas m) (x : Fin (m * m)) : Bool :=
  t.clusters (high x) (low x)

Uses 1 · Used by 31

Statement usesTwo-level van Emde Boas tree

Used bySet of stored elements of a van Emde Boas tree · Contents of the empty van Emde Boas tree · Contents after insertion into a van Emde Boas tree · Maximum query on the empty van Emde Boas tree · When the van Emde Boas maximum query returns nothing · Correctness of the van Emde Boas maximum query · The van Emde Boas maximum query bounds every member · Maximum query on a one-element van Emde Boas tree · The maximum query of a van Emde Boas tree returns a member · The contents of a van Emde Boas tree are its members · The empty van Emde Boas tree has no members · Membership after insertion into a van Emde Boas tree · Insertion into a van Emde Boas tree keeps existing members · Insertion into a van Emde Boas tree leaves other elements unchanged · An inserted element is a member of a van Emde Boas tree · The empty van Emde Boas tree has no minimum · Empty minimum query in a van Emde Boas tree · Characterization of the van Emde Boas minimum · Minimum of a one-element van Emde Boas tree · The van Emde Boas minimum is a lower bound · The van Emde Boas minimum is stored · Predecessor queries in the empty van Emde Boas tree · Empty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor · Maximality of the van Emde Boas predecessor · The van Emde Boas predecessor is stored · The empty van Emde Boas tree has no successors · A van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member · No member lies strictly between an element and its van Emde Boas successor · The van Emde Boas successor is stored

DefinitionInsertion into a van Emde Boas tree#✓fully proved

Let \(m\) be a natural number, let \(t\) be a van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) and let \(x\) be an element of the universe. Inserting \(x\) into \(t\) gives the tree obtained from \(t\) by setting bit \(x \bmod m\) of cluster \(\lfloor x / m \rfloor\) and summary bit \(\lfloor x / m \rfloor\), leaving every other bit unchanged.

public def insert {m : Nat} (x : Fin (m * m)) (t : VanEmdeBoas m) :
    VanEmdeBoas m where
  summary := Function.update t.summary (high x) true
  clusters := Function.update t.clusters (high x)
    (Function.update (t.clusters (high x)) (low x) true)

Uses 1 · Used by 8

Statement usesTwo-level van Emde Boas tree

Used byContents after insertion into a van Emde Boas tree · Maximum query on a one-element van Emde Boas tree · Membership after insertion into a van Emde Boas tree · Insertion into a van Emde Boas tree keeps existing members · Insertion into a van Emde Boas tree leaves other elements unchanged · An inserted element is a member of a van Emde Boas tree · Minimum of a one-element van Emde Boas tree · Insertion preserves validity of van Emde Boas trees

DefinitionSummary invariant of a van Emde Boas tree#✓fully proved

A two-level van Emde Boas tree \(t\) with \(m\) clusters is valid when, for every cluster index \(i < m\), summary bit \(i\) of \(t\) is set exactly when cluster \(i\) of \(t\) is nonempty, that is, when some bit \(j < m\) of cluster \(i\) is set.

public def Valid {m : Nat} (t : VanEmdeBoas m) : Prop :=
  ∀ i : Fin m, t.summary i = true ↔ ∃ j : Fin m, t.clusters i j = true

Uses 1 · Used by 14

Statement usesTwo-level van Emde Boas tree

Used byWhen the van Emde Boas maximum query returns nothing · Correctness of the van Emde Boas maximum query · The van Emde Boas maximum query bounds every member · Empty minimum query in a van Emde Boas tree · Characterization of the van Emde Boas minimum · The van Emde Boas minimum is a lower bound · Empty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor · Maximality of the van Emde Boas predecessor · A van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member · No member lies strictly between an element and its van Emde Boas successor · The empty van Emde Boas tree is valid · Insertion preserves validity of van Emde Boas trees

DefinitionSet of stored elements of a van Emde Boas tree#✓fully proved

Let \(m\) be a natural number. For a van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\), the set of stored elements of \(t\) is the finite set of those elements of the universe that are members of \(t\).

public def contents {m : Nat} (t : VanEmdeBoas m) : Finset (Fin (m * m)) :=
  Finset.univ.filter fun x => t.member x = true

Uses 2 · Used by 3

Statement usesTwo-level van Emde Boas tree · Membership in a van Emde Boas tree

Used byContents of the empty van Emde Boas tree · Contents after insertion into a van Emde Boas tree · The contents of a van Emde Boas tree are its members

TheoremThe empty van Emde Boas tree has no members#✓fully proved

For every \(m\) and every \(x\) in the universe \(\{0, 1, \dots, m^2 - 1\}\), \(x\) is not a member of the empty two-level van Emde Boas tree over that universe.

public theorem member_empty {m : Nat} (x : Fin (m * m)) :
    (empty : VanEmdeBoas m).member x = false

Uses 2 · Used by 7

Statement usesEmpty van Emde Boas tree · Membership in a van Emde Boas tree

Used byContents of the empty van Emde Boas tree · Maximum query on the empty van Emde Boas tree · Maximum query on a one-element van Emde Boas tree · The empty van Emde Boas tree has no minimum · Minimum of a one-element van Emde Boas tree · Predecessor queries in the empty van Emde Boas tree · The empty van Emde Boas tree has no successors

TheoremAn inserted element is a member of a van Emde Boas tree#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and every \(x\) in that universe, \(x\) is a member of the tree obtained by inserting \(x\) into \(t\).

public theorem member_insert_self {m : Nat} (x : Fin (m * m))
    (t : VanEmdeBoas m) : (insert x t).member x = true

Uses 3 · Used by 3

Statement usesTwo-level van Emde Boas tree · Insertion into a van Emde Boas tree · Membership in a van Emde Boas tree

Used byMaximum query on a one-element van Emde Boas tree · Membership after insertion into a van Emde Boas tree · Minimum of a one-element van Emde Boas tree

TheoremInsertion into a van Emde Boas tree leaves other elements unchanged#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and all \(x \ne y\) in that universe, \(y\) is a member of the tree obtained by inserting \(x\) into \(t\) if and only if \(y\) is a member of \(t\).

public theorem member_insert_of_ne {m : Nat} {x y : Fin (m * m)}
    (h : y ≠ x) (t : VanEmdeBoas m) :
    (insert x t).member y = t.member y

Uses 3 · Used by 1

Statement usesTwo-level van Emde Boas tree · Insertion into a van Emde Boas tree · Membership in a van Emde Boas tree

Used byMembership after insertion into a van Emde Boas tree

TheoremMembership after insertion into a van Emde Boas tree#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and all \(x, y\) in that universe, \(y\) is a member of the tree obtained by inserting \(x\) into \(t\) if and only if \(y = x\) or \(y\) is a member of \(t\).

public theorem member_insert {m : Nat} (t : VanEmdeBoas m)
    (x y : Fin (m * m)) :
    (insert x t).member y = true ↔ y = x ∨ t.member y = true

Uses 5 · Used by 4

Statement usesTwo-level van Emde Boas tree · Insertion into a van Emde Boas tree · Membership in a van Emde Boas tree

Proof usesInsertion into a van Emde Boas tree leaves other elements unchanged · An inserted element is a member of a van Emde Boas tree

Used byContents after insertion into a van Emde Boas tree · Maximum query on a one-element van Emde Boas tree · Insertion into a van Emde Boas tree keeps existing members · Minimum of a one-element van Emde Boas tree

TheoremInsertion into a van Emde Boas tree keeps existing members#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and all \(x, y\) in that universe, if \(y\) is a member of \(t\), then \(y\) is a member of the tree obtained by inserting \(x\) into \(t\).

public theorem member_insert_of_member {m : Nat} (t : VanEmdeBoas m)
    (x y : Fin (m * m)) (h : t.member y = true) :
    (insert x t).member y = true

Uses 4

Statement usesTwo-level van Emde Boas tree · Insertion into a van Emde Boas tree · Membership in a van Emde Boas tree

Proof usesMembership after insertion into a van Emde Boas tree

TheoremThe empty van Emde Boas tree is valid#✓fully proved

For every natural number \(m\), the empty two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) satisfies the summary invariant: each summary bit is set exactly when its cluster is nonempty.

public theorem valid_empty {m : Nat} : (empty : VanEmdeBoas m).Valid

Uses 3 · Used by 6

Statement usesSummary invariant of a van Emde Boas tree · Empty van Emde Boas tree

Proof usesTwo-level van Emde Boas tree

Used byMaximum query on the empty van Emde Boas tree · Maximum query on a one-element van Emde Boas tree · The empty van Emde Boas tree has no minimum · Minimum of a one-element van Emde Boas tree · Predecessor queries in the empty van Emde Boas tree · The empty van Emde Boas tree has no successors

TheoremInsertion preserves validity of van Emde Boas trees#✓fully proved

For every natural number \(m\), every element \(x\) of the universe \(\{0, \dots, m^2 - 1\}\) and every two-level van Emde Boas tree \(t\) over that universe that satisfies the summary invariant (each summary bit is set exactly when its cluster is nonempty), the tree obtained from \(t\) by inserting \(x\) also satisfies the summary invariant.

public theorem valid_insert {m : Nat} (x : Fin (m * m))
    (t : VanEmdeBoas m) (hv : t.Valid) : (insert x t).Valid

Uses 3 · Used by 2

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Insertion into a van Emde Boas tree

Used byMaximum query on a one-element van Emde Boas tree · Minimum of a one-element van Emde Boas tree

TheoremThe contents of a van Emde Boas tree are its members#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and every \(x\) in that universe, \(x\) belongs to the finite set of stored elements of \(t\) if and only if \(x\) is a member of \(t\).

@[simp]
public theorem mem_contents {m : Nat} {t : VanEmdeBoas m} {x : Fin (m * m)} :
    x ∈ t.contents ↔ t.member x = true

Uses 3 · Used by 2

Statement usesTwo-level van Emde Boas tree · Set of stored elements of a van Emde Boas tree · Membership in a van Emde Boas tree

Used byContents of the empty van Emde Boas tree · Contents after insertion into a van Emde Boas tree

TheoremContents of the empty van Emde Boas tree#✓fully proved

For every natural number \(m\), the set of stored elements of the empty van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) is empty.

@[simp]
public theorem contents_empty {m : Nat} :
    (empty : VanEmdeBoas m).contents = ∅

Uses 6

Statement usesSet of stored elements of a van Emde Boas tree · Empty van Emde Boas tree

Proof usesTwo-level van Emde Boas tree · The contents of a van Emde Boas tree are its members · Membership in a van Emde Boas tree · The empty van Emde Boas tree has no members

TheoremContents after insertion into a van Emde Boas tree#✓fully proved

Let \(m\) be a natural number, let \(t\) be a van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) and let \(x\) be an element of the universe. The set of stored elements of the tree obtained by inserting \(x\) into \(t\) is the set of stored elements of \(t\) together with \(x\). No validity assumption on \(t\) is needed.

public theorem contents_insert {m : Nat} (x : Fin (m * m))
    (t : VanEmdeBoas m) :
    (insert x t).contents = Insert.insert x t.contents

Uses 6

Statement usesTwo-level van Emde Boas tree · Set of stored elements of a van Emde Boas tree · Insertion into a van Emde Boas tree

Proof usesThe contents of a van Emde Boas tree are its members · Membership in a van Emde Boas tree · Membership after insertion into a van Emde Boas tree

DefinitionMinimum query of a van Emde Boas tree#✓fully proved

Let \(t\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\). If some summary bit of \(t\) is set, let \(h\) be the least cluster index whose summary bit is set; if cluster \(h\) has a set position, let \(\ell\) be the least one. The minimum query on \(t\) then returns the element \(h \cdot m + \ell\). If no summary bit is set, or cluster \(h\) has no set position, it returns no element.

In a valid tree this is the least stored element.

public def min? {m : Nat} (t : VanEmdeBoas m) : Option (Fin (m * m)) :=
  match firstFin? t.summary with
  | none => none
  | some hi =>
    match firstFin? (t.clusters hi) with
    | none => none
    | some lo => some (combine hi lo)

Uses 1 · Used by 6

Statement usesTwo-level van Emde Boas tree

Used byThe empty van Emde Boas tree has no minimum · Empty minimum query in a van Emde Boas tree · Characterization of the van Emde Boas minimum · Minimum of a one-element van Emde Boas tree · The van Emde Boas minimum is a lower bound · The van Emde Boas minimum is stored

TheoremThe van Emde Boas minimum is stored#✓fully proved

Let \(t\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\). If the minimum query on \(t\) returns \(x\), then \(x\) is stored in \(t\).

public theorem min?_mem {m : Nat} {t : VanEmdeBoas m} {x : Fin (m * m)}
    (h : t.min? = some x) : t.member x = true

Uses 3 · Used by 1

Statement usesTwo-level van Emde Boas tree · Membership in a van Emde Boas tree · Minimum query of a van Emde Boas tree

Used byCharacterization of the van Emde Boas minimum

TheoremThe van Emde Boas minimum is a lower bound#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\). If the minimum query on \(t\) returns \(x\), then \(x \le y\) for every \(y\) stored in \(t\).

public theorem min?_least {m : Nat} {t : VanEmdeBoas m} (hv : t.Valid)
    {x y : Fin (m * m)} (h : t.min? = some x) (hy : t.member y = true) :
    x.val ≤ y.val

Uses 4 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Minimum query of a van Emde Boas tree

Used byCharacterization of the van Emde Boas minimum

TheoremEmpty minimum query in a van Emde Boas tree#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\). The minimum query on \(t\) returns no element if and only if no element of the universe is stored in \(t\).

public theorem min?_eq_none_iff {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) :
    t.min? = none ↔ ∀ y : Fin (m * m), t.member y = false

Uses 4 · Used by 2

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Minimum query of a van Emde Boas tree

Used byThe empty van Emde Boas tree has no minimum · Characterization of the van Emde Boas minimum

TheoremCharacterization of the van Emde Boas minimum#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), and let \(x\) be in the universe. The minimum query on \(t\) returns \(x\) if and only if \(x\) is stored in \(t\) and \(x \le y\) for every \(y\) stored in \(t\).

public theorem min?_eq_some_iff_of_valid {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x : Fin (m * m)} :
    t.min? = some x ↔
      t.member x = true ∧
        ∀ y : Fin (m * m), t.member y = true → x.val ≤ y.val

Uses 7 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Minimum query of a van Emde Boas tree

Proof usesEmpty minimum query in a van Emde Boas tree · The van Emde Boas minimum is a lower bound · The van Emde Boas minimum is stored

Used byMinimum of a one-element van Emde Boas tree

TheoremThe empty van Emde Boas tree has no minimum#✓fully proved

For every \(m\), the minimum query of the empty two-level van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) returns no element.

public theorem min?_empty {m : Nat} : (empty : VanEmdeBoas m).min? = none

Uses 6

Statement usesEmpty van Emde Boas tree · Minimum query of a van Emde Boas tree

Proof usesMembership in a van Emde Boas tree · The empty van Emde Boas tree has no members · Empty minimum query in a van Emde Boas tree · The empty van Emde Boas tree is valid

TheoremMinimum of a one-element van Emde Boas tree#✓fully proved

For every \(x\) in the universe \(\{0, \dots, m^2 - 1\}\), the minimum query on the two-level van Emde Boas tree obtained by inserting \(x\) into the empty tree returns \(x\).

public theorem min?_insert_empty {m : Nat} (x : Fin (m * m)) :
    (insert x empty).min? = some x

Uses 10

Statement usesEmpty van Emde Boas tree · Insertion into a van Emde Boas tree · Minimum query of a van Emde Boas tree

Proof usesMembership in a van Emde Boas tree · The empty van Emde Boas tree has no members · Membership after insertion into a van Emde Boas tree · An inserted element is a member of a van Emde Boas tree · Characterization of the van Emde Boas minimum · The empty van Emde Boas tree is valid · Insertion preserves validity of van Emde Boas trees

DefinitionMaximum query of a van Emde Boas tree#✓fully proved

For a two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\), the maximum query first finds the greatest index \(i < m\) whose summary bit is set, and then the greatest index \(j < m\) whose bit is set in cluster \(i\); it returns the element \(i m + j\). It returns no element if no summary bit is set, or if no bit of cluster \(i\) is set. When the summary bits record exactly the nonempty clusters, this is the greatest stored element.

public def max? {m : Nat} (t : VanEmdeBoas m) : Option (Fin (m * m)) :=
  match lastFin? t.summary with
  | none => none
  | some hi =>
    match lastFin? (t.clusters hi) with
    | none => none
    | some lo => some (combine hi lo)

Uses 1 · Used by 6

Statement usesTwo-level van Emde Boas tree

Used byMaximum query on the empty van Emde Boas tree · When the van Emde Boas maximum query returns nothing · Correctness of the van Emde Boas maximum query · The van Emde Boas maximum query bounds every member · Maximum query on a one-element van Emde Boas tree · The maximum query of a van Emde Boas tree returns a member

TheoremThe maximum query of a van Emde Boas tree returns a member#✓fully proved

For every two-level van Emde Boas tree \(t\) over the universe \(\{0, 1, \dots, m^2 - 1\}\) and every \(x\) in that universe, if the maximum query of \(t\) returns \(x\), then \(x\) is a member of \(t\). No validity hypothesis on \(t\) is needed.

public theorem max?_mem {m : Nat} {t : VanEmdeBoas m} {x : Fin (m * m)}
    (h : t.max? = some x) : t.member x = true

Uses 3 · Used by 1

Statement usesTwo-level van Emde Boas tree · Maximum query of a van Emde Boas tree · Membership in a van Emde Boas tree

Used byCorrectness of the van Emde Boas maximum query

TheoremThe van Emde Boas maximum query bounds every member#✓fully proved

Let \(m\) be a natural number and let \(t\) be a valid van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\). If the maximum query on \(t\) returns \(x\), then \(y \le x\) for every member \(y\) of \(t\).

public theorem max?_greatest {m : Nat} {t : VanEmdeBoas m} (hv : t.Valid)
    {x y : Fin (m * m)} (h : t.max? = some x) (hy : t.member y = true) :
    y.val ≤ x.val

Uses 4 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Maximum query of a van Emde Boas tree · Membership in a van Emde Boas tree

Used byCorrectness of the van Emde Boas maximum query

TheoremWhen the van Emde Boas maximum query returns nothing#✓fully proved

Let \(m\) be a natural number and let \(t\) be a valid van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\). The maximum query on \(t\) returns no element if and only if no element of the universe is a member of \(t\).

public theorem max?_eq_none_iff {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) :
    t.max? = none ↔ ∀ y : Fin (m * m), t.member y = false

Uses 4 · Used by 2

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Maximum query of a van Emde Boas tree · Membership in a van Emde Boas tree

Used byMaximum query on the empty van Emde Boas tree · Correctness of the van Emde Boas maximum query

TheoremCorrectness of the van Emde Boas maximum query#✓fully proved

Let \(m\) be a natural number, let \(t\) be a valid van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) and let \(x\) be an element of the universe. The maximum query on \(t\) returns \(x\) if and only if \(x\) is a member of \(t\) and \(y \le x\) for every member \(y\) of \(t\).

public theorem max?_eq_some_iff_of_valid {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x : Fin (m * m)} :
    t.max? = some x ↔
      t.member x = true ∧
        ∀ y : Fin (m * m), t.member y = true → y.val ≤ x.val

Uses 7 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Maximum query of a van Emde Boas tree · Membership in a van Emde Boas tree

Proof usesWhen the van Emde Boas maximum query returns nothing · The van Emde Boas maximum query bounds every member · The maximum query of a van Emde Boas tree returns a member

Used byMaximum query on a one-element van Emde Boas tree

TheoremMaximum query on the empty van Emde Boas tree#✓fully proved

For every natural number \(m\), the maximum query on the empty van Emde Boas tree over the universe \(\{0, 1, \dots, m^2 - 1\}\) returns no element.

public theorem max?_empty {m : Nat} : (empty : VanEmdeBoas m).max? = none

Uses 6

Statement usesEmpty van Emde Boas tree · Maximum query of a van Emde Boas tree

Proof usesWhen the van Emde Boas maximum query returns nothing · Membership in a van Emde Boas tree · The empty van Emde Boas tree has no members · The empty van Emde Boas tree is valid

TheoremMaximum query on a one-element van Emde Boas tree#✓fully proved

Let \(m\) be a natural number and let \(x\) be an element of the universe \(\{0, 1, \dots, m^2 - 1\}\). The maximum query on the tree obtained by inserting \(x\) into the empty van Emde Boas tree over this universe returns \(x\).

public theorem max?_insert_empty {m : Nat} (x : Fin (m * m)) :
    (insert x empty).max? = some x

Uses 10

Statement usesEmpty van Emde Boas tree · Insertion into a van Emde Boas tree · Maximum query of a van Emde Boas tree

Proof usesCorrectness of the van Emde Boas maximum query · Membership in a van Emde Boas tree · The empty van Emde Boas tree has no members · Membership after insertion into a van Emde Boas tree · An inserted element is a member of a van Emde Boas tree · The empty van Emde Boas tree is valid · Insertion preserves validity of van Emde Boas trees

DefinitionSuccessor query in a two-level van Emde Boas tree#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) and let \(x = hm + \ell\) with \(0 \le h, \ell < m\), so that \(x\) sits at position \(\ell\) of cluster \(h\). If cluster \(h\) has a set position after \(\ell\), the successor of \(x\) in \(T\) is \(hm + \ell'\) for the least such position \(\ell'\). Otherwise, let \(h'\) be the least cluster index with \(h < h'\) whose summary bit is set; the successor is \(h'm + \ell''\) for the least position \(\ell''\) set in cluster \(h'\). If there is no such \(h'\), or cluster \(h'\) has no set position, \(x\) has no successor.

In a valid tree, the successor of \(x\) is the least member of \(T\) greater than \(x\).

public def successor {m : Nat} (t : VanEmdeBoas m) (x : Fin (m * m)) :
    Option (Fin (m * m)) :=
  match firstFin? (succClusterPred t x) with
  | some lo => some (combine (high x) lo)
  | none =>
    match firstFin? (succSummaryPred t x) with
    | none => none
    | some hi =>
      match firstFin? (t.clusters hi) with
      | none => none
      | some lo => some (combine hi lo)

Uses 1 · Used by 6

Statement usesTwo-level van Emde Boas tree

Used byThe empty van Emde Boas tree has no successors · A van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member · The van Emde Boas successor is strictly larger than its argument · No member lies strictly between an element and its van Emde Boas successor · The van Emde Boas successor is stored

TheoremThe van Emde Boas successor is stored#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), not necessarily valid, and let \(x\) and \(y\) be elements of the universe. If the successor of \(x\) in \(T\) is \(y\), then \(y\) is a member of \(T\).

public theorem successor_mem {m : Nat} {t : VanEmdeBoas m}
    {x y : Fin (m * m)} (h : t.successor x = some y) :
    t.member y = true

Uses 3 · Used by 2

Statement usesTwo-level van Emde Boas tree · Membership in a van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Used byA van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member

TheoremThe van Emde Boas successor is strictly larger than its argument#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), not necessarily valid, and let \(x\) and \(y\) be elements of the universe. If the successor of \(x\) in \(T\) is \(y\), then \(x < y\).

public theorem successor_gt {m : Nat} {t : VanEmdeBoas m}
    {x y : Fin (m * m)} (h : t.successor x = some y) :
    x.val < y.val

Uses 2 · Used by 2

Statement usesTwo-level van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Used byA van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is the least larger member

TheoremNo member lies strictly between an element and its van Emde Boas successor#✓fully proved

Let \(T\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) and let \(x\), \(y\), \(z\) be elements of the universe. If the successor of \(x\) in \(T\) is \(y\) and \(z\) is a member of \(T\) with \(x < z\), then \(y \le z\).

public theorem successor_least {m : Nat} {t : VanEmdeBoas m} (hv : t.Valid)
    {x y z : Fin (m * m)} (h : t.successor x = some y)
    (hz : t.member z = true) (hxz : x.val < z.val) :
    y.val ≤ z.val

Uses 4 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Used byThe van Emde Boas successor is the least larger member

TheoremA van Emde Boas successor is missing exactly when nothing larger is stored#✓fully proved

Let \(T\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) and let \(x\) be an element of the universe. Then \(x\) has no successor in \(T\) if and only if every member \(z\) of \(T\) satisfies \(z \le x\).

public theorem successor_eq_none_iff {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x : Fin (m * m)} :
    t.successor x = none ↔
      ∀ z : Fin (m * m), t.member z = true → z.val ≤ x.val

Uses 6 · Used by 2

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Proof usesThe van Emde Boas successor is strictly larger than its argument · The van Emde Boas successor is stored

Used byThe empty van Emde Boas tree has no successors · The van Emde Boas successor is the least larger member

TheoremThe van Emde Boas successor is the least larger member#✓fully proved

Let \(T\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) and let \(x\) and \(y\) be elements of the universe. Then the successor of \(x\) in \(T\) is \(y\) if and only if \(y\) is a member of \(T\), \(x < y\), and \(y \le z\) for every member \(z\) of \(T\) with \(x < z\).

public theorem successor_eq_some_iff_of_valid {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x y : Fin (m * m)} :
    t.successor x = some y ↔
      t.member y = true ∧ x.val < y.val ∧
        ∀ z : Fin (m * m), t.member z = true → x.val < z.val →
          y.val ≤ z.val

Uses 8

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Proof usesA van Emde Boas successor is missing exactly when nothing larger is stored · The van Emde Boas successor is strictly larger than its argument · No member lies strictly between an element and its van Emde Boas successor · The van Emde Boas successor is stored

TheoremThe empty van Emde Boas tree has no successors#✓fully proved

For every \(m\) and every element \(x\) of the universe \(\{0, \dots, m^2 - 1\}\), \(x\) has no successor in the empty two-level van Emde Boas tree over that universe.

public theorem successor_empty {m : Nat} (x : Fin (m * m)) :
    (empty : VanEmdeBoas m).successor x = none

Uses 6

Statement usesEmpty van Emde Boas tree · Successor query in a two-level van Emde Boas tree

Proof usesMembership in a van Emde Boas tree · The empty van Emde Boas tree has no members · A van Emde Boas successor is missing exactly when nothing larger is stored · The empty van Emde Boas tree is valid

DefinitionPredecessor query in a two-level van Emde Boas tree#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\) and let \(x = hm + \ell\) with \(0 \le h, \ell < m\), so that \(x\) sits at position \(\ell\) of cluster \(h\). If cluster \(h\) has a set position before \(\ell\), the predecessor of \(x\) in \(T\) is \(hm + \ell'\) for the greatest such position \(\ell'\). Otherwise, let \(h'\) be the greatest cluster index with \(h' < h\) whose summary bit is set; the predecessor is \(h'm + \ell''\) for the greatest position \(\ell''\) set in cluster \(h'\). If there is no such \(h'\), or cluster \(h'\) has no set position, \(x\) has no predecessor.

In a valid tree, the predecessor of \(x\) is the greatest member of \(T\) less than \(x\).

public def predecessor {m : Nat} (t : VanEmdeBoas m) (x : Fin (m * m)) :
    Option (Fin (m * m)) :=
  match lastFin? (predClusterPred t x) with
  | some lo => some (combine (high x) lo)
  | none =>
    match lastFin? (predSummaryPred t x) with
    | none => none
    | some hi =>
      match lastFin? (t.clusters hi) with
      | none => none
      | some lo => some (combine hi lo)

Uses 1 · Used by 6

Statement usesTwo-level van Emde Boas tree

Used byPredecessor queries in the empty van Emde Boas tree · Empty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor · Maximality of the van Emde Boas predecessor · The van Emde Boas predecessor is strictly smaller than its argument · The van Emde Boas predecessor is stored

TheoremThe van Emde Boas predecessor is stored#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), not necessarily valid, and let \(x\) and \(y\) be elements of the universe. If the predecessor of \(x\) in \(T\) is \(y\), then \(y\) is a member of \(T\).

public theorem predecessor_mem {m : Nat} {t : VanEmdeBoas m}
    {x y : Fin (m * m)} (h : t.predecessor x = some y) :
    t.member y = true

Uses 3 · Used by 2

Statement usesTwo-level van Emde Boas tree · Membership in a van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Used byEmpty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor

TheoremThe van Emde Boas predecessor is strictly smaller than its argument#✓fully proved

Let \(T\) be a two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), not necessarily valid, and let \(x\) and \(y\) be elements of the universe. If the predecessor of \(x\) in \(T\) is \(y\), then \(y < x\).

public theorem predecessor_lt {m : Nat} {t : VanEmdeBoas m}
    {x y : Fin (m * m)} (h : t.predecessor x = some y) :
    y.val < x.val

Uses 2 · Used by 2

Statement usesTwo-level van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Used byEmpty predecessor query in a van Emde Boas tree · Characterization of the van Emde Boas predecessor

TheoremMaximality of the van Emde Boas predecessor#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), and let \(x\), \(y\) and \(z\) be in the universe. If the predecessor query for \(x\) in \(t\) returns \(y\), and \(z\) is stored in \(t\) with \(z < x\), then \(z \le y\).

public theorem predecessor_greatest {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x y z : Fin (m * m)} (h : t.predecessor x = some y)
    (hz : t.member z = true) (hxz : z.val < x.val) :
    z.val ≤ y.val

Uses 4 · Used by 1

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Used byCharacterization of the van Emde Boas predecessor

TheoremEmpty predecessor query in a van Emde Boas tree#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), and let \(x\) be in the universe. The predecessor query for \(x\) in \(t\) returns no element if and only if \(x \le z\) for every \(z\) stored in \(t\).

public theorem predecessor_eq_none_iff {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x : Fin (m * m)} :
    t.predecessor x = none ↔
      ∀ z : Fin (m * m), t.member z = true → x.val ≤ z.val

Uses 6 · Used by 2

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Proof usesThe van Emde Boas predecessor is strictly smaller than its argument · The van Emde Boas predecessor is stored

Used byPredecessor queries in the empty van Emde Boas tree · Characterization of the van Emde Boas predecessor

TheoremCharacterization of the van Emde Boas predecessor#✓fully proved

Let \(t\) be a valid two-level van Emde Boas tree over the universe \(\{0, \dots, m^2 - 1\}\), and let \(x\) and \(y\) be in the universe. The predecessor query for \(x\) in \(t\) returns \(y\) if and only if \(y\) is stored in \(t\), \(y < x\), and \(z \le y\) for every \(z\) stored in \(t\) with \(z < x\).

public theorem predecessor_eq_some_iff_of_valid {m : Nat} {t : VanEmdeBoas m}
    (hv : t.Valid) {x y : Fin (m * m)} :
    t.predecessor x = some y ↔
      t.member y = true ∧ y.val < x.val ∧
        ∀ z : Fin (m * m), t.member z = true → z.val < x.val →
          z.val ≤ y.val

Uses 8

Statement usesTwo-level van Emde Boas tree · Summary invariant of a van Emde Boas tree · Membership in a van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Proof usesEmpty predecessor query in a van Emde Boas tree · Maximality of the van Emde Boas predecessor · The van Emde Boas predecessor is strictly smaller than its argument · The van Emde Boas predecessor is stored

TheoremPredecessor queries in the empty van Emde Boas tree#✓fully proved

For every \(x\) in the universe \(\{0, \dots, m^2 - 1\}\), the predecessor query for \(x\) in the empty two-level van Emde Boas tree returns no element.

public theorem predecessor_empty {m : Nat} (x : Fin (m * m)) :
    (empty : VanEmdeBoas m).predecessor x = none

Uses 6

Statement usesEmpty van Emde Boas tree · Predecessor query in a two-level van Emde Boas tree

Proof usesMembership in a van Emde Boas tree · The empty van Emde Boas tree has no members · Empty predecessor query in a van Emde Boas tree · The empty van Emde Boas tree is valid

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.