Sparse table

19 fully proved

Sparse Table

StructureSparse table#✓fully proved

A sparse table over a type \(\alpha\) consists of an array of elements of \(\alpha\), called its data, and an array of arrays of elements of \(\alpha\), called its levels.

The intended meaning is that level \(k\) stores the minima of the length-\(2^k\) slices of the data; data and levels are stored as arrays so that entry lookup is random access. Arbitrary values need not relate data and levels at all; validity ties every stored level to this specification, tables produced by the construction are valid, and query correctness is stated for valid tables.

structure SparseTable (α : Type u) where
  data : Array α
  levels : Array (Array α)

Used by 11

Used byBuilding a sparse table · Built sparse tables are valid · Sparse-table entries · Entries of a built sparse table are interval minima · Entries of a valid sparse table are interval minima · Rows of a valid sparse table are its levels · Sparse table range-minimum query · Correctness of sparse table queries · Whole-range sparse table query · Correctness of queries on valid sparse tables · Valid sparse table

DefinitionOption minimum#✓fully proved

For a type \(\alpha\) with a minimum operation, the option minimum extends \(\min\) to optional values (elements of \(\alpha\) or none): on two elements \(a, b\) of \(\alpha\) it returns \(\min(a, b)\), and none is a neutral element on either side.

def omin {α : Type u} [Min α] : Option α → Option α → Option α
  | none, b => b
  | some a, none => some a
  | some a, some b => some (min a b)

Used by 19

Used byBrute-force closest pair · Cost of the brute-force closest-pair scan · Divide and conquer agrees with brute force · Closest-pair recursion · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion · Least squared distance from a point to a list · The nearest-point scan returns the least squared distance · Strip scan from a point · Cost of the scan from one strip point · Closest-pair strip scan · The strip scan bounds every pair with a small vertical gap · Cost of the strip scan · Entries of a built sparse table are interval minima · Levels hold interval minima · Idempotence of the option minimum · Sparse table range-minimum query · Whole-range sparse table query · Correctness of queries on valid sparse tables

TheoremIdempotence of the option minimum#✓fully proved

For every linearly ordered type \(\alpha\) and every optional value \(a\) (an element of \(\alpha\) or none), the option minimum of \(a\) with itself is \(a\).

This is what lets two overlapping query intervals count their overlap twice.

theorem omin_self {α : Type u} [LinearOrder α] (a : Option α) : omin a a = a

Uses 1 · Used by 2

Statement usesOption minimum

Used byWhole-range sparse table query · Correctness of queries on valid sparse tables

DefinitionLevels of a sparse table#✓fully proved

For a list \(a\) over a type with a minimum operation \(\min\), the levels of \(a\) are defined recursively: level \(0\) is \(a\), and if level \(k\) is \(\ell = (\ell_0, \dots, \ell_{m-1})\), then level \(k + 1\) is the list of the values \(\min(\ell_i, \ell_{i+2^k})\) for \(0 \le i < m - 2^k\) (empty when \(m \le 2^k\)).

Over a linear order, element \(i\) of level \(k\) is the minimum of the \(2^k\) consecutive elements of \(a\) starting at index \(i\), and only start indices whose interval fits in \(a\) get an element.

def level {α : Type u} [Min α] (a : List α) : Nat → List α
  | 0 => a
  | k + 1 => List.zipWith min (level a k) ((level a k).drop (2 ^ k))

Used by 9

Used byBuilt sparse tables are valid · Entries of a built sparse table are interval minima · Entries of a valid sparse table are interval minima · Rows of a valid sparse table are its levels · Levels hold interval minima · Length of a level · Whole-range sparse table query · Correctness of queries on valid sparse tables · Valid sparse table

TheoremLength of a level#✓fully proved

For a list \(a\) of length \(n\) over a type with a minimum operation and a natural number \(k\), level \(k\) of \(a\) has length \(\max(n + 1 - 2^k, 0)\): one element for each start index \(i\) with \(i + 2^k \le n\).

theorem level_length {α : Type u} [Min α] (a : List α) (k : Nat) :
    (level a k).length = a.length + 1 - 2 ^ k

Uses 1

Statement usesLevels of a sparse table

TheoremLevels hold interval minima#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be a list over a linearly ordered type, and let \(k\) and \(i\) be natural numbers with \(i + 2^k \le n\). Then level \(k\) of \(a\) has an element at index \(i\), and it equals \(\min(a_i, a_{i+1}, \dots, a_{i+2^k-1})\).

theorem getElem?_level {α : Type u} [LinearOrder α] (a : List α) (k i : Nat)
    (h : i + 2 ^ k ≤ a.length) :
    (level a k)[i]? = ((a.drop i).take (2 ^ k)).min?

Uses 2 · Used by 1

Statement usesLevels of a sparse table

Proof usesOption minimum

Used byEntries of a valid sparse table are interval minima

DefinitionNext level of a sparse table row#✓fully proved

For a type with a minimum operation, an array \((r_0, \dots, r_{n-1})\) and a natural number \(k\), the next level is the array of length \(n - 2^k\) (empty when \(2^k \ge n\)) whose entry \(i\) is \(\min(r_i, r_{i + 2^k})\).

The construction of a sparse table computes each level once from the previous one this way.

def nextLevel {α : Type u} [Min α] (row : Array α) (k : Nat) : Array α :=
  Array.zipWith min row (row.extract (2 ^ k) row.size)

Used by 2

Used byOne step of the sparse-table construction · Built sparse tables are valid

DefinitionOne step of the sparse-table construction#✓fully proved

Work over a type with a minimum operation \(\min\). Given a pair \((r, L)\) of a current row \(r\) (an array of length \(|r|\)) and an array \(L\) of the rows recorded so far, and a natural number \(k\), the build step returns the pair \((r', L')\), where \(L'\) is \(L\) with \(r\) appended at the end, and \(r'\) is the array whose entry \(i\) is \(\min(r_i, r_{i+2^k})\) for each \(i\) with \(i + 2^k < |r|\).

def buildStep {α : Type u} [Min α] (state : Array α × Array (Array α)) (k : Nat) :
    Array α × Array (Array α) :=
  (nextLevel state.1 k, state.2.push state.1)

Uses 1 · Used by 2

Statement usesNext level of a sparse table row

Used byBuilding a sparse table · Built sparse tables are valid

DefinitionBuilding a sparse table#✓fully proved

For a list \(a\) of length \(n\) over a type with a minimum operation \(\min\), the sparse table built from \(a\) has data \(a\) and \(\lfloor \log_2 n \rfloor + 1\) stored rows, where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\). The rows are produced by iterating the build step for \(k = 0, 1, \dots, \lfloor \log_2 n \rfloor\), starting from the current row \(a\) and no recorded rows. So row \(0\) is \(a\), and entry \(i\) of row \(k + 1\) is \(\min(x_i, x_{i+2^k})\), where \(x\) is row \(k\) and \(i + 2^k\) is less than the length of \(x\). Each row is computed once, from its predecessor.

def build {α : Type u} [Min α] (a : List α) : SparseTable α :=
  let data := a.toArray
  let final := (List.range (Nat.log2 a.length + 1)).foldl buildStep (data, #[])
  ⟨data, final.2⟩

Uses 2 · Used by 4

Statement usesSparse table · One step of the sparse-table construction

Used byBuilt sparse tables are valid · Entries of a built sparse table are interval minima · Correctness of sparse table queries · Whole-range sparse table query

DefinitionValid sparse table#✓fully proved

A sparse table over a type with a minimum operation, whose data is a list \(a\) of length \(n\), is valid when it has exactly \(m + 1\) levels, where \(m = \lfloor \log_2 n \rfloor\) for \(n \ge 1\) and \(m = 0\) for \(n = 0\), and for each \(k \le m\) its level \(k\) is the list \(L_k\) defined by \(L_0 = a\) and, for \(x = L_j\), \(L_{j+1}\) is the list of length \(|x| - 2^j\) (empty when \(2^j \ge |x|\)) whose entry \(i\) is \(\min(x_i, x_{i + 2^j})\). For a linear order, \(L_k\) is the list of minima of the length-\(2^k\) slices of \(a\).

Tables produced by the construction are valid, an arbitrary value such as data \((1)\) with the single level \((99)\) is not, and query correctness is stated only for valid tables.

def Valid {α : Type u} [Min α] (t : SparseTable α) : Prop :=
  t.levels.toList.map Array.toList =
    (List.range (Nat.log2 t.data.toList.length + 1)).map (level t.data.toList)

Uses 2 · Used by 5

Statement usesSparse table · Levels of a sparse table

Used byBuilt sparse tables are valid · Entries of a valid sparse table are interval minima · Rows of a valid sparse table are its levels · Whole-range sparse table query · Correctness of queries on valid sparse tables

TheoremBuilt sparse tables are valid#✓fully proved

For every list \(a\) over a type with a minimum operation, the sparse table built from \(a\) is valid: its stored rows are exactly the levels \(0, 1, \dots, \lfloor \log_2 n \rfloor\) of \(a\), in this order, where \(n\) is the length of \(a\) and \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\).

theorem build_valid {α : Type u} [Min α] (a : List α) : (build a).Valid

Uses 6 · Used by 3

Statement usesValid sparse table · Building a sparse table

Proof usesSparse table · One step of the sparse-table construction · Levels of a sparse table · Next level of a sparse table row

Used byEntries of a built sparse table are interval minima · Correctness of sparse table queries · Whole-range sparse table query

DefinitionSparse-table entries#✓fully proved

For a sparse table \(t\) and natural numbers \(k\) and \(i\), the entry of \(t\) at row \(k\) and index \(i\) is element \(i\) of the \(k\)-th stored row of \(t\) (both counted from \(0\)) when \(t\) has a \(k\)-th row and that row has an element at index \(i\); otherwise the entry is undefined. Both lookups are random-access array lookups.

def entry {α : Type u} (t : SparseTable α) (k i : Nat) : Option α :=
  t.levels[k]?.bind (fun row => row[i]?)

Uses 1 · Used by 6

Statement usesSparse table

Used byEntries of a built sparse table are interval minima · Entries of a valid sparse table are interval minima · Rows of a valid sparse table are its levels · Sparse table range-minimum query · Whole-range sparse table query · Correctness of queries on valid sparse tables

TheoremRows of a valid sparse table are its levels#✓fully proved

Let \(t\) be a valid sparse table over a type with a minimum operation, with data \(d\) of length \(n\), and let \(k \le \lfloor \log_2 n \rfloor\), where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\). Then for every index \(i\), the entry of \(t\) at row \(k\) and index \(i\) is defined exactly when level \(k\) of \(d\) has an element at index \(i\), and in that case the two are equal.

theorem entry_eq_of_valid {α : Type u} [Min α] {t : SparseTable α}
    (hValid : t.Valid) {k : Nat} (hk : k ≤ Nat.log2 t.data.toList.length)
    (i : Nat) :
    t.entry k i = (level t.data.toList k)[i]?

Uses 4 · Used by 4

Statement usesSparse table · Valid sparse table · Sparse-table entries · Levels of a sparse table

Used byEntries of a built sparse table are interval minima · Entries of a valid sparse table are interval minima · Whole-range sparse table query · Correctness of queries on valid sparse tables

TheoremEntries of a built sparse table are interval minima#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be a list over a linearly ordered type, and let \(k\) and \(i\) be natural numbers with \(i + 2^k \le n\). Then the entry of the sparse table built from \(a\) at row \(k\) and index \(i\) is defined and equals \(\min(a_i, a_{i+1}, \dots, a_{i+2^k-1})\).

No separate bound on \(k\) is needed: \(i + 2^k \le n\) already implies \(k \le \lfloor \log_2 n \rfloor\).

theorem entry_build_eq_min? {α : Type u} [LinearOrder α] (a : List α) (k i : Nat)
    (h : i + 2 ^ k ≤ a.length) :
    (build a).entry k i = ((a.drop i).take (2 ^ k)).min?

Uses 7

Statement usesBuilding a sparse table · Sparse-table entries

Proof usesSparse table · Built sparse tables are valid · Rows of a valid sparse table are its levels · Levels of a sparse table · Option minimum

TheoremEntries of a valid sparse table are interval minima#✓fully proved

Let \(t\) be a valid sparse table over a linearly ordered type, with data \(d = (d_0, \dots, d_{n-1})\), and let \(k\) and \(i\) be natural numbers with \(i + 2^k \le n\). Then the entry of \(t\) at row \(k\) and index \(i\) is defined and equals \(\min(d_i, d_{i+1}, \dots, d_{i+2^k-1})\).

theorem entry_eq_min?_of_valid {α : Type u} [LinearOrder α] {t : SparseTable α}
    (hValid : t.Valid) (k i : Nat) (h : i + 2 ^ k ≤ t.data.toList.length) :
    t.entry k i = ((t.data.toList.drop i).take (2 ^ k)).min?

Uses 6

Statement usesSparse table · Valid sparse table · Sparse-table entries

Proof usesRows of a valid sparse table are its levels · Levels hold interval minima · Levels of a sparse table

DefinitionSparse table range-minimum query#✓fully proved

For a sparse table \(t\) over a type with a minimum operation and natural numbers \(l, r\), the query over \([l, r)\) returns none when \(r \le l\). Otherwise, with \(k = \lfloor \log_2 (r - l) \rfloor\), it returns the option minimum (the minimum, with none as a neutral element on either side) of the entries of \(t\) at level \(k\) and indices \(l\) and \(r - 2^k\), in this order, where an entry not stored in \(t\) counts as none.

def query {α : Type u} [Min α] (t : SparseTable α) (l r : Nat) : Option α :=
  if r ≤ l then none
  else omin (t.entry (Nat.log2 (r - l)) l)
    (t.entry (Nat.log2 (r - l)) (r - 2 ^ (Nat.log2 (r - l))))

Uses 3 · Used by 3

Statement usesSparse table · Sparse-table entries · Option minimum

Used byCorrectness of sparse table queries · Whole-range sparse table query · Correctness of queries on valid sparse tables

TheoremCorrectness of queries on valid sparse tables#✓fully proved

Let \(t\) be a valid sparse table over a linearly ordered type whose data is the list \((a_0, \dots, a_{n-1})\), and let \(l, r\) be natural numbers with \(r \le n\). Then the range-minimum query over \([l, r)\) on \(t\) returns the minimum of the slice \((a_l, \dots, a_{r-1})\) (none when \(r \le l\), where the slice is empty).

Only the premise \(r \le n\) is needed: for reversed bounds \(r \le l\) both sides are none.

theorem query_eq_of_valid {α : Type u} [LinearOrder α] {t : SparseTable α}
    (hValid : t.Valid) {l r : Nat} (hr : r ≤ t.data.toList.length) :
    t.query l r = ((t.data.toList.drop l).take (r - l)).min?

Uses 8 · Used by 1

Statement usesSparse table · Valid sparse table · Sparse table range-minimum query

Proof usesSparse-table entries · Rows of a valid sparse table are its levels · Levels of a sparse table · Option minimum · Idempotence of the option minimum

Used byCorrectness of sparse table queries

TheoremCorrectness of sparse table queries#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be a list over a linearly ordered type and let \(l, r\) be natural numbers with \(r \le n\). Then the range-minimum query over \([l, r)\) on the sparse table built from \(a\) returns the minimum of the slice \((a_l, \dots, a_{r-1})\) (none when \(r \le l\), where the slice is empty).

No ordering premise \(l \le r\) is needed.

theorem query_build {α : Type u} [LinearOrder α] (a : List α) {l r : Nat}
    (hr : r ≤ a.length) :
    (build a).query l r = ((a.drop l).take (r - l)).min?

Uses 5

Statement usesBuilding a sparse table · Sparse table range-minimum query

Proof usesSparse table · Built sparse tables are valid · Correctness of queries on valid sparse tables

TheoremWhole-range sparse table query#✓fully proved

For every list \(a\) of length \(n\) over a linearly ordered type, the range-minimum query over \([0, n)\) on the sparse table built from \(a\) returns the minimum of \(a\) (none when \(a\) is empty).

theorem query_build_all {α : Type u} [LinearOrder α] (a : List α) :
    (build a).query 0 a.length = a.min?

Uses 10

Statement usesBuilding a sparse table · Sparse table range-minimum query

Proof usesSparse table · Valid sparse table · Built sparse tables are valid · Sparse-table entries · Rows of a valid sparse table are its levels · Levels of a sparse table · Option minimum · Idempotence of the option minimum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.