Fenwick tree

26 fully proved

Fenwick Tree

StructureFenwick tree#✓fully proved

A Fenwick tree (binary indexed tree) over a commutative additive monoid \(\alpha\) is an array of elements of \(\alpha\), read as one-indexed interval sums with an unused dummy entry at index \(0\). The structure itself imposes no condition on the entries, and the underlying array it represents is not stored; the relation saying that a tree represents a given array is defined separately.

public structure FenwickTree (α : Type u) [AddCommMonoid α] where
  /-- The one-indexed stored interval sums, with a dummy entry at index `0`,
  backed by an `Array` for constant-time reads; writes are constant-time
  only when the array is uniquely referenced (a shared array is copied
  first). -/
  bit : Array α

Used by 15

Used byPoint update of a Fenwick tree · Out-of-range point updates leave a Fenwick tree unchanged · Building a Fenwick tree from a list · Fenwick tree prefix sum · Prefix sums after a point update · Correctness of Fenwick tree prefix sums · The empty prefix sum is zero · Fenwick tree range sum · Correctness of Fenwick tree range sums · Size of a Fenwick tree · Size of a built Fenwick tree · A Fenwick tree has the length of the list it represents · Fenwick tree representing a list · Point update preserves representation · Building a Fenwick tree yields a valid representation

DefinitionLowest set bit#✓fully proved

For a natural number \(n > 0\), \(\operatorname{lowbit}(n)\) is the largest power of two dividing \(n\); for \(n = 0\) it is defined as \(\operatorname{lowbit}(0) = 0\).

public def lowbit (n : Nat) : Nat :=
  if n = 0 then 0 else lowbitAux n n

Used by 14

Used byPoint update of a Fenwick tree · Out-of-range point updates leave a Fenwick tree unchanged · Fenwick-tree interval sum of a list · Interval sum read from an array · Dividing out the lowest set bit leaves an odd number · The lowest set bit divides the number · The lowest set bit is at most the number · The lowest set bit of a positive number is positive · The lowest set bit is a power of two · Lowbit of zero · Fenwick tree prefix sum · Correctness of Fenwick tree prefix sums · Point update preserves representation · Building a Fenwick tree yields a valid representation

TheoremLowbit of zero#✓fully proved

By convention, \(\operatorname{lowbit}(0) = 0\).

public theorem lowbit_zero : lowbit 0 = 0

Uses 1

Statement usesLowest set bit

TheoremThe lowest set bit of a positive number is positive#✓fully proved

For every natural number \(n > 0\), \(\operatorname{lowbit}(n) > 0\), where \(\operatorname{lowbit}(n)\) is the value of the lowest set bit of \(n\) in binary.

public theorem lowbit_pos {n : Nat} (hn : 0 < n) : 0 < lowbit n

Uses 1 · Used by 2

Statement usesLowest set bit

Used byCorrectness of Fenwick tree prefix sums · Point update preserves representation

TheoremThe lowest set bit is at most the number#✓fully proved

For every natural number \(n\), \(\operatorname{lowbit}(n) \le n\), where \(\operatorname{lowbit}(n)\) is the value of the lowest set bit of \(n\) in binary (with \(\operatorname{lowbit}(0) = 0\)).

public theorem lowbit_le (n : Nat) : lowbit n ≤ n

Uses 1 · Used by 2

Statement usesLowest set bit

Used byCorrectness of Fenwick tree prefix sums · Point update preserves representation

TheoremThe lowest set bit divides the number#✓fully proved

For every natural number \(n > 0\), \(\operatorname{lowbit}(n)\) divides \(n\), where \(\operatorname{lowbit}(n)\) is the value of the lowest set bit of \(n\) in binary.

public theorem lowbit_dvd {n : Nat} (hn : 0 < n) : lowbit n ∣ n

Uses 1 · Used by 1

Statement usesLowest set bit

Used byPoint update preserves representation

TheoremThe lowest set bit is a power of two#✓fully proved

For every natural number \(n > 0\), \(\operatorname{lowbit}(n)\) is a power of two: \(\operatorname{lowbit}(n) = 2^k\) for some natural number \(k\).

public theorem lowbit_two_pow {n : Nat} (hn : 0 < n) : ∃ k, lowbit n = 2 ^ k

Uses 1 · Used by 1

Statement usesLowest set bit

Used byPoint update preserves representation

TheoremDividing out the lowest set bit leaves an odd number#✓fully proved

For every natural number \(n > 0\), the quotient \(n / \operatorname{lowbit}(n)\) is odd, where \(\operatorname{lowbit}(n)\) is the value of the lowest set bit of \(n\) in binary.

public theorem lowbit_div_odd {n : Nat} (hn : 0 < n) : (n / lowbit n) % 2 = 1

Uses 1 · Used by 1

Statement usesLowest set bit

Used byPoint update preserves representation

DefinitionFenwick-tree interval sum of a list#✓fully proved

For a list \(a\) of elements of a commutative additive monoid \(\alpha\) and a natural number \(j\), the interval sum at the one-indexed position \(j\) is the sum of the \(\operatorname{lowbit}(j)\) entries of \(a\) ending at zero-indexed position \(j - 1\), where \(\operatorname{lowbit}(j)\) is the largest power of two dividing \(j\) (with \(\operatorname{lowbit}(0) = 0\)) and entries past the end of \(a\) count as \(0\).

@[expose] public def blockSum {α : Type u} [AddCommMonoid α] (arr : List α) (j : Nat) : α :=
  ((List.range' (j - lowbit j) (lowbit j)).map (fun i => arr.getD i 0)).sum

Uses 1 · Used by 5

Statement usesLowest set bit

Used byCorrectness of Fenwick tree prefix sums · A Fenwick tree has the length of the list it represents · Fenwick tree representing a list · Point update preserves representation · Building a Fenwick tree yields a valid representation

DefinitionInterval sum read from an array#✓fully proved

For an array \(a\) of elements of a commutative additive monoid \(\alpha\) and a natural number \(j\), this is the sum of the \(\operatorname{lowbit}(j)\) entries of \(a\) ending at zero-indexed position \(j - 1\), where \(\operatorname{lowbit}(j)\) is the largest power of two dividing \(j\) (with \(\operatorname{lowbit}(0) = 0\)) and entries past the end of \(a\) count as \(0\).

It has the same value as the list-based interval sum but reads each entry in constant time; Fenwick-tree construction uses it, so building takes \(O(n \log n)\) reads rather than quadratic list indexing.

@[expose] public def blockSumArray {α : Type u} [AddCommMonoid α]
    (arr : Array α) (j : Nat) : α :=
  ((List.range' (j - lowbit j) (lowbit j)).map (fun i => arr.getD i 0)).sum

Uses 1 · Used by 3

Statement usesLowest set bit

Used byBuilding a Fenwick tree from a list · Size of a built Fenwick tree · Building a Fenwick tree yields a valid representation

DefinitionFenwick tree representing a list#✓fully proved

A Fenwick tree \(t\) over an additive commutative monoid represents a list \(a\) of length \(n\) when its stored array has length \(n + 1\) (a dummy entry at index \(0\) plus one entry per element of \(a\)) and, for every \(j\) with \(1 \le j \le n\), the stored entry at index \(j\) equals the block sum of \(a\) at \(j\): the sum of the \(\operatorname{lowbit}(j)\) entries of \(a\) ending at position \(j - 1\) (positions counted from \(0\)), where \(\operatorname{lowbit}(j)\) is the largest power of two dividing \(j\).

The underlying list itself is not stored at runtime; it appears only in this specification relation.

@[expose] public def Valid {α : Type u} [AddCommMonoid α] (t : FenwickTree α)
    (arr : List α) : Prop :=
  t.bit.size = arr.length + 1 ∧
    ∀ j, 1 ≤ j → j ≤ arr.length → t.bit.getD j 0 = blockSum arr j

Uses 2 · Used by 6

Statement usesFenwick tree · Fenwick-tree interval sum of a list

Used byPrefix sums after a point update · Correctness of Fenwick tree prefix sums · Correctness of Fenwick tree range sums · A Fenwick tree has the length of the list it represents · Point update preserves representation · Building a Fenwick tree yields a valid representation

DefinitionSize of a Fenwick tree#✓fully proved

The size of a Fenwick tree is the length of its stored array minus one, truncated at \(0\); the one accounts for the dummy entry at index \(0\). It is read off the stored array in constant time.

public def size {α : Type u} [AddCommMonoid α] (t : FenwickTree α) : Nat :=
  t.bit.size - 1

Uses 1 · Used by 7

Statement usesFenwick tree

Used byPoint update of a Fenwick tree · Out-of-range point updates leave a Fenwick tree unchanged · Fenwick tree prefix sum · Correctness of Fenwick tree prefix sums · Size of a built Fenwick tree · A Fenwick tree has the length of the list it represents · Point update preserves representation

TheoremA Fenwick tree has the length of the list it represents#✓fully proved

If a Fenwick tree \(t\) over an additive commutative monoid represents a list \(a\), then the size of \(t\) equals the length of \(a\).

public theorem size_eq_length_of_valid {α : Type u} [AddCommMonoid α]
    {t : FenwickTree α} {arr : List α} (hv : Valid t arr) :
    t.size = arr.length

Uses 4 · Used by 2

Statement usesFenwick tree · Fenwick tree representing a list · Size of a Fenwick tree

Proof usesFenwick-tree interval sum of a list

Used byCorrectness of Fenwick tree prefix sums · Point update preserves representation

DefinitionBuilding a Fenwick tree from a list#✓fully proved

For a list \(a\) of length \(n\) over a commutative additive monoid \(\alpha\), the Fenwick tree built from \(a\) stores the array of length \(n + 1\) whose entry at index \(0\) is \(0\) and whose entry at each one-indexed position \(j\) with \(1 \le j \le n\) is the sum of the \(\operatorname{lowbit}(j)\) entries of \(a\) ending at zero-indexed position \(j - 1\), where \(\operatorname{lowbit}(j)\) is the largest power of two dividing \(j\).

The input is converted to an array once, so each entry read is constant-time and construction is \(O(n \log n)\).

public def build {α : Type u} [AddCommMonoid α] (arr : List α) : FenwickTree α where
  bit :=
    let a := arr.toArray
    (0 :: (List.range arr.length).map
      (fun i => blockSumArray a (i + 1))).toArray

Uses 2 · Used by 3

Statement usesFenwick tree · Interval sum read from an array

Used byPrefix sums of a built Fenwick tree · Size of a built Fenwick tree · Building a Fenwick tree yields a valid representation

TheoremSize of a built Fenwick tree#✓fully proved

For every list \(a\) over an additive commutative monoid, the Fenwick tree built from \(a\) has size equal to the length of \(a\).

public theorem size_build {α : Type u} [AddCommMonoid α] (arr : List α) :
    (build arr).size = arr.length

Uses 4

Statement usesBuilding a Fenwick tree from a list · Size of a Fenwick tree

Proof usesFenwick tree · Interval sum read from an array

TheoremBuilding a Fenwick tree yields a valid representation#✓fully proved

For every list \(a\) over an additive commutative monoid, the Fenwick tree built from \(a\) represents \(a\).

public theorem valid_build {α : Type u} [AddCommMonoid α] (arr : List α) :
    Valid (build arr) arr

Uses 6 · Used by 1

Statement usesFenwick tree representing a list · Building a Fenwick tree from a list

Proof usesFenwick tree · Fenwick-tree interval sum of a list · Interval sum read from an array · Lowest set bit

Used byPrefix sums of a built Fenwick tree

DefinitionFenwick tree prefix sum#✓fully proved

Let \(t\) be a Fenwick tree over an additive commutative monoid with \(n\) underlying entries, let \(k\) be a natural number and let \(m = \min(k, n)\). The prefix sum of length \(k\) of \(t\) is the sum of the stored entries of \(t\) at the positions \(j_0 = m\), \(j_{r+1} = j_r - \operatorname{lowbit}(j_r)\), taken for as long as \(j_r > 0\).

When \(t\) represents a list, this is the sum of its first \(m\) entries, so queries past the end are clamped.

public def prefixSum {α : Type u} [AddCommMonoid α] (t : FenwickTree α) (k : Nat) :
    α :=
  prefixAux t.bit (min k t.size) (min k t.size)

Uses 3 · Used by 6

Statement usesFenwick tree · Lowest set bit · Size of a Fenwick tree

Used byPrefix sums after a point update · Prefix sums of a built Fenwick tree · Correctness of Fenwick tree prefix sums · The empty prefix sum is zero · Fenwick tree range sum · Correctness of Fenwick tree range sums

TheoremThe empty prefix sum is zero#✓fully proved

For every Fenwick tree \(t\) over an additive commutative monoid, the prefix sum of length \(0\) of \(t\) is \(0\).

@[simp]
public theorem prefixSum_zero {α : Type u} [AddCommMonoid α] (t : FenwickTree α) :
    prefixSum t 0 = 0

Uses 2

Statement usesFenwick tree · Fenwick tree prefix sum

TheoremCorrectness of Fenwick tree prefix sums#✓fully proved

Let \(t\) be a Fenwick tree representing a list \(a\) of elements of an additive commutative monoid. Then for every natural number \(k\), including \(k > |a|\), the prefix sum of length \(k\) of \(t\) equals the sum of the first \(\min(k, |a|)\) entries of \(a\).

public theorem prefixSum_eq_take_sum {α : Type u} [AddCommMonoid α]
    (t : FenwickTree α) {arr : List α} (hv : Valid t arr) (k : Nat) :
    prefixSum t k = (arr.take k).sum

Uses 9 · Used by 3

Statement usesFenwick tree · Fenwick tree representing a list · Fenwick tree prefix sum

Proof usesFenwick-tree interval sum of a list · Lowest set bit · The lowest set bit is at most the number · The lowest set bit of a positive number is positive · Size of a Fenwick tree · A Fenwick tree has the length of the list it represents

Used byPrefix sums after a point update · Prefix sums of a built Fenwick tree · Correctness of Fenwick tree range sums

TheoremPrefix sums of a built Fenwick tree#✓fully proved

For every list \(a\) of elements of an additive commutative monoid and every natural number \(k\), the prefix sum of length \(k\) of the Fenwick tree built from \(a\) equals the sum of the first \(\min(k, |a|)\) entries of \(a\).

public theorem prefixSum_build {α : Type u} [AddCommMonoid α] (arr : List α)
    (k : Nat) : prefixSum (build arr) k = (arr.take k).sum

Uses 4

Statement usesBuilding a Fenwick tree from a list · Fenwick tree prefix sum

Proof usesCorrectness of Fenwick tree prefix sums · Building a Fenwick tree yields a valid representation

DefinitionPoint update of a Fenwick tree#✓fully proved

Let \(t\) be a Fenwick tree over a commutative additive monoid \(\alpha\), let \(n\) be its size (the length of its stored array minus one), let \(i\) be a natural number and let \(\delta \in \alpha\). Adding \(\delta\) at underlying position \(i\) adds \(\delta\) to the stored entries at the one-indexed positions \(j_1 = i + 1\) and \(j_{k+1} = j_k + \operatorname{lowbit}(j_k)\), for as long as \(j_k \le n\), where \(\operatorname{lowbit}(j)\) is the largest power of two dividing \(j\); every other stored entry is left unchanged. In particular, if \(i \ge n\) the tree is unchanged.

Each write is constant-time only when the stored array is uniquely referenced, since a shared array is copied by the first persistent write. The walk is fuelled by the size, which always suffices because the visited positions strictly increase.

public def add {α : Type u} [AddCommMonoid α] (t : FenwickTree α) (i : Nat)
    (δ : α) : FenwickTree α where
  bit := (walk t.size t.size (i + 1)).foldl (fun b j => addAt b j δ) t.bit

Uses 3 · Used by 3

Statement usesFenwick tree · Lowest set bit · Size of a Fenwick tree

Used byOut-of-range point updates leave a Fenwick tree unchanged · Prefix sums after a point update · Point update preserves representation

TheoremOut-of-range point updates leave a Fenwick tree unchanged#✓fully proved

Let \(t\) be a Fenwick tree over a commutative additive monoid \(\alpha\), and let \(n\) be its size (the length of its stored array minus one). For every natural number \(i \ge n\) and every \(\delta \in \alpha\), the point update of \(t\) adding \(\delta\) at position \(i\) returns \(t\) itself.

public theorem add_eq_self_of_le {α : Type u} [AddCommMonoid α]
    (t : FenwickTree α) {i : Nat} (hi : t.size ≤ i) (δ : α) :
    add t i δ = t

Uses 4

Statement usesFenwick tree · Point update of a Fenwick tree · Size of a Fenwick tree

Proof usesLowest set bit

TheoremPoint update preserves representation#✓fully proved

Let \(t\) be a Fenwick tree over an additive commutative monoid that represents a list \(a\) of length \(n\). For every index \(i < n\) (counting from \(0\)) and every element \(\delta\), the tree obtained from \(t\) by adding \(\delta\) at position \(i\) represents the list obtained from \(a\) by replacing its entry \(a_i\) with \(a_i + \delta\).

public theorem valid_add {α : Type u} [AddCommMonoid α] {t : FenwickTree α}
    {arr : List α} (hv : Valid t arr) {i : Nat} (hi : i < arr.length) (δ : α) :
    Valid (add t i δ) (arr.set i (arr.getD i 0 + δ))

Uses 12 · Used by 1

Statement usesFenwick tree · Fenwick tree representing a list · Point update of a Fenwick tree

Proof usesFenwick-tree interval sum of a list · Lowest set bit · Dividing out the lowest set bit leaves an odd number · The lowest set bit divides the number · The lowest set bit is at most the number · The lowest set bit of a positive number is positive · The lowest set bit is a power of two · Size of a Fenwick tree · A Fenwick tree has the length of the list it represents

Used byPrefix sums after a point update

TheoremPrefix sums after a point update#✓fully proved

Let \(t\) be a Fenwick tree representing a list \(a\) of elements of an additive commutative monoid, let \(i < |a|\) be a position, let \(\delta\) be an element of the monoid, and let \(k\) be any natural number, possibly larger than \(|a|\). Then the prefix sum of length \(k\) of the tree obtained from \(t\) by adding \(\delta\) at position \(i\) equals the prefix sum of length \(k\) of \(t\) plus \(\delta\) if \(i < k\), and equals the prefix sum of length \(k\) of \(t\) if \(k \le i\).

public theorem prefixSum_add {α : Type u} [AddCommMonoid α] {t : FenwickTree α}
    {arr : List α} (hv : Valid t arr) {i : Nat} (hi : i < arr.length) (δ : α)
    (k : Nat) :
    prefixSum (add t i δ) k = prefixSum t k + (if i < k then δ else 0)

Uses 6

Statement usesFenwick tree · Fenwick tree representing a list · Point update of a Fenwick tree · Fenwick tree prefix sum

Proof usesCorrectness of Fenwick tree prefix sums · Point update preserves representation

DefinitionFenwick tree range sum#✓fully proved

For a Fenwick tree \(t\) over an additive commutative group and natural numbers \(\mathit{lo}\) and \(\mathit{hi}\), the range sum of \(t\) over \([\mathit{lo}, \mathit{hi})\) is \(0\) if \(\mathit{hi} \le \mathit{lo}\), and otherwise the prefix sum of length \(\mathit{hi}\) of \(t\) minus the prefix sum of length \(\mathit{lo}\) of \(t\).

When \(t\) represents a list, this is the sum of its entries with indices in \([\mathit{lo}, \mathit{hi})\). This is the only Fenwick tree operation that needs additive inverses.

public def rangeSum {α : Type u} [AddCommGroup α] (t : FenwickTree α)
    (lo hi : Nat) : α :=
  if hi ≤ lo then 0 else prefixSum t hi - prefixSum t lo

Uses 2 · Used by 1

Statement usesFenwick tree · Fenwick tree prefix sum

Used byCorrectness of Fenwick tree range sums

TheoremCorrectness of Fenwick tree range sums#✓fully proved

Let \(t\) be a Fenwick tree representing a list \(a = (a_0, \dots, a_{n-1})\) of elements of an additive commutative group. Then for all natural numbers \(\mathit{lo}\) and \(\mathit{hi}\), the range sum of \(t\) over \([\mathit{lo}, \mathit{hi})\) equals \(\sum_{\mathit{lo} \le i < \min(\mathit{hi}, n)} a_i\); in particular it is \(0\) when \(\mathit{hi} \le \mathit{lo}\).

public theorem rangeSum_eq {α : Type u} [AddCommGroup α] {t : FenwickTree α}
    {arr : List α} (hv : Valid t arr) (lo hi : Nat) :
    rangeSum t lo hi = ((arr.take hi).drop lo).sum

Uses 5

Statement usesFenwick tree · Fenwick tree representing a list · Fenwick tree range sum

Proof usesFenwick tree prefix sum · Correctness of Fenwick tree prefix sums

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.