Balanced aggregation trees for dynamic prefix sums

An array of 2 ^ h natural numbers is represented by a complete binary aggregation tree. The logical operations are addition at one position and summation of a prefix. Nodes are laid out in preorder in a contiguous region of 2 * 2 ^ h - 1 words. These definitions do not assign unit cost to a Lean operation: the concrete Word-RAM client supplies the execution and cost proofs.

Main definitions

• Tree: a complete binary tree with natural-number leaves.
• Tree.Rep: the contiguous memory representation, including every internal sum.
• Tree.prefixSum and Tree.add: prefix queries and point increments.

Main results

• Tree.prefixSum_eq_sum_take: the query is the sum of the corresponding leaf prefix.
• Tree.Rep.congr: representation depends only on its owned region.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms for balanced trees and aggregation invariants.

inductive Cslib.Algorithms.WordRAM.PrefixSums.Tree : ℕ → Type

A complete binary tree with 2 ^ h leaves.

• leaf (value : ℕ) : Tree 0

  A single array entry.

• node {h : ℕ} (left right : Tree h) : Tree (h + 1)

  Two equally sized consecutive subarrays.

def Cslib.Algorithms.WordRAM.PrefixSums.instDecidableEqTree.decEq {a✝ : ℕ} (x✝ x✝¹ : Tree a✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.PrefixSums.instDecidableEqTree {a✝ : ℕ} : DecidableEq (Tree a✝)

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.PrefixSums.instReprTree {a✝ : ℕ} : Repr (Tree a✝)

def Cslib.Algorithms.WordRAM.PrefixSums.instReprTree.repr {a✝ : ℕ} : Tree a✝ → ℕ → Std.Format

def Cslib.Algorithms.WordRAM.PrefixSums.increment : List ℕ → ℕ → ℕ → List ℕ

Add an increment at a list position; out-of-range positions leave the list unchanged.

theorem Cslib.Algorithms.WordRAM.PrefixSums.increment_append (as bs : List ℕ) (i δ : ℕ) : increment (as ++ bs) i δ = if i < as.length then increment as i δ ++ bs else as ++ increment bs (i - as.length) δ

Point increments split over concatenation at the left array's length.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.leaves {h : ℕ} : Tree h → List ℕ

The represented array, in its original order.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.total {h : ℕ} : Tree h → ℕ

The aggregate stored at the root.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.prefixSum {h : ℕ} : Tree h → ℕ → ℕ

The sum of the first k entries. Calls beyond the end are clamped.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.add {h : ℕ} : Tree h → ℕ → ℕ → Tree h

Add δ at zero-based position i. The machine interface requires i < 2 ^ h.

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.length_leaves {h : ℕ} (t : Tree h) : t.leaves.length = 2 ^ h

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.sum_leaves {h : ℕ} (t : Tree h) : t.leaves.sum = t.total

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.prefixSum_zero {h : ℕ} (t : Tree h) : t.prefixSum 0 = 0

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.prefixSum_length {h : ℕ} (t : Tree h) : t.prefixSum (2 ^ h) = t.total

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.prefixSum_eq_sum_take {h : ℕ} (t : Tree h) (k : ℕ) : t.prefixSum k = (List.take k t.leaves).sum

The tree query has the ordinary array-prefix meaning.

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.total_add {h : ℕ} (t : Tree h) (i δ : ℕ) : (t.add i δ).total = t.total + δ

Point increments raise the total by precisely the increment.

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.leaves_add {h : ℕ} (t : Tree h) (i δ : ℕ) (hi : i < 2 ^ h) : (t.add i δ).leaves = increment t.leaves i δ

The tree update is the ordinary point increment on the represented array.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.words (h : ℕ) : ℕ

Number of words occupied by a complete aggregation tree.

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.words_zero : words 0 = 1

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.words_succ (h : ℕ) : words (h + 1) = 1 + words h + words h

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.Rep {h : ℕ} : Tree h → ℕ → (ℕ → ℕ) → Prop

The memory stores each subtree's aggregate at its root, followed by its left and right subtrees. No assertion is made about memory outside the occupied interval.

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.Rep.root {h b : ℕ} {mem : ℕ → ℕ} {t : Tree h} (ht : t.Rep b mem) : mem b = t.total

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.Rep.congr {h b : ℕ} {mem mem' : ℕ → ℕ} {t : Tree h} (ht : t.Rep b mem) (he : ∀ (a : ℕ), b ≤ a → a < b + words h → mem' a = mem a) : t.Rep b mem'

A frame rule for the tree representation: only its contiguous footprint matters.

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.Rep.update_of_outside {h a b : ℕ} {mem : ℕ → ℕ} {t : Tree h} (ht : t.Rep b mem) (ha : a < b ∨ b + words h ≤ a) (v : ℕ) : t.Rep b (Function.update mem a v)

Writing outside the representation's region preserves it.

def Cslib.Algorithms.WordRAM.PrefixSums.Tree.zero (h : ℕ) : Tree h

The all-zero array has a concrete, nonempty representation in zero memory.

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.total_zero (h : ℕ) : (zero h).total = 0

theorem Cslib.Algorithms.WordRAM.PrefixSums.Tree.rep_zero (h b : ℕ) : (zero h).Rep b fun (x : ℕ) => 0