Segment tree

26 fully proved

Segment Tree

InductiveSegment tree#✓fully proved

A segment tree with values in \(\alpha\) is either empty, a leaf holding a value in \(\alpha\), or an internal node holding a cached segment aggregate in \(\alpha\), a cached segment length in \(\mathbb{N}\), a left child and a right child, both segment trees.

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

Used by 19

Used byAggregate of a segment tree · Aggregate of a valid segment tree · Building a segment tree from a list · Size of a valid segment tree · Range query on a segment tree · Correctness of range queries on a valid segment tree · Size of a segment tree · Point update preserves the size of a segment tree · Leaf list of a segment tree · Accumulator traversal of a segment tree · Accumulator traversal prepends the leaf list · Building a segment tree preserves the list · Leaf list of an internal node · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Point update of a segment tree · Point update preserves validity · Valid segment trees · Built segment trees are valid

DefinitionAggregate of a segment tree#✓fully proved

The aggregate of a segment tree with values in an additive monoid is \(0\) for the empty tree, \(x\) for a single leaf with value \(x\), and the aggregate cached at the root for an internal node.

def agg {α : Type u} [AddMonoid α] : SegmentTree α → α
  | .empty => 0
  | .leaf x => x
  | .node cached _ _ _ => cached

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 1 · Used by 14

Statement usesSegment tree

Used byAggregate of a built segment tree · Aggregate of a valid segment tree · Aggregate after a point update of a built segment tree · Building a segment tree from a list · Size of a valid segment tree · Correctness of range queries on a valid segment tree · Point update preserves the size of a segment tree · Building a segment tree preserves the list · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Point update of a segment tree · Point update preserves validity · Valid segment trees · Built segment trees are valid

DefinitionSize of a segment tree#✓fully proved

The size of a segment tree is \(0\) for the empty tree, \(1\) for a leaf, and, for an internal node, the segment length cached at that node.

When every cached length is the sum of the sizes of the node's children, this is the number of leaves, and internal nodes answer in constant time.

def size {α : Type u} : SegmentTree α → Nat
  | .empty => 0
  | .leaf _ => 1
  | .node _ cachedSize _ _ => cachedSize

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 1 · Used by 15

Statement usesSegment tree

Used byAggregate of a valid segment tree · Building a segment tree from a list · Size of a valid segment tree · Range query on a segment tree · Correctness of range queries on a valid segment tree · Size of a built segment tree · Point update preserves the size of a segment tree · Building a segment tree preserves the list · Point update of a built segment tree · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Point update of a segment tree · Point update preserves validity · Valid segment trees · Built segment trees are valid

DefinitionAccumulator traversal of a segment tree#✓fully proved

Given a segment tree and a list \(acc\), the accumulator traversal returns \(acc\) for the empty tree, the list \(acc\) with \(x\) prepended for a leaf with value \(x\), and, for an internal node with left child \(L\) and right child \(R\), the traversal of \(L\) starting from the result of the traversal of \(R\) starting from \(acc\).

Threading the output suffix this way collects the leaves of an \(n\)-leaf tree in linear time instead of repeatedly appending (and copying) left-subtree results.

def toListAux {α : Type u} : SegmentTree α → List α → List α
  | .empty, acc => acc
  | .leaf x, acc => x :: acc
  | .node _ _ left right, acc => left.toListAux (right.toListAux acc)

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 1 · Used by 3

Statement usesSegment tree

Used byLeaf list of a segment tree · Accumulator traversal prepends the leaf list · Leaf list of an internal node

DefinitionLeaf list of a segment tree#✓fully proved

The leaf list of a segment tree is the list of its leaf values from left to right: the empty list for the empty tree, \([x]\) for a leaf with value \(x\), and the leaf list of the left child followed by the leaf list of the right child for an internal node.

def toList {α : Type u} (t : SegmentTree α) : List α :=
  t.toListAux []

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 2 · Used by 15

Statement usesSegment tree · Accumulator traversal of a segment tree

Used byAggregate of a built segment tree · Aggregate of a valid segment tree · Aggregate after a point update of a built segment tree · Size of a valid segment tree · Range queries on a built segment tree · Correctness of range queries on a valid segment tree · Range queries after a point update of a built segment tree · Size of a built segment tree · Accumulator traversal prepends the leaf list · Building a segment tree preserves the list · Leaf list of an internal node · Point update of a built segment tree · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Built segment trees are valid

TheoremAccumulator traversal prepends the leaf list#✓fully proved

For every segment tree \(t\) and every list \(acc\), the accumulator traversal of \(t\) starting from \(acc\) returns the leaf list of \(t\) followed by \(acc\).

@[simp]
theorem toListAux_eq {α : Type u} (t : SegmentTree α) (acc : List α) :
    t.toListAux acc = t.toList ++ acc

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 3 · Used by 1

Statement usesSegment tree · Leaf list of a segment tree · Accumulator traversal of a segment tree

Used byLeaf list of an internal node

TheoremLeaf list of an internal node#✓fully proved

For every internal node of a segment tree, with any cached aggregate, any cached length, left child \(L\) and right child \(R\), its leaf list is the leaf list of \(L\) followed by the leaf list of \(R\).

With the accumulator definition of the leaf list this is a theorem, not a definitional unfolding.

@[simp]
theorem toList_node {α : Type u} (agg : α) (sz : Nat) (left right : SegmentTree α) :
    (SegmentTree.node agg sz left right).toList = left.toList ++ right.toList

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 4 · Used by 7

Statement usesSegment tree · Leaf list of a segment tree

Proof usesAccumulator traversal of a segment tree · Accumulator traversal prepends the leaf list

Used byAggregate of a valid segment tree · Size of a valid segment tree · Correctness of range queries on a valid segment tree · Building a segment tree preserves the list · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Built segment trees are valid

InductiveValid segment trees#✓fully proved

Validity of a segment tree over an additive monoid is defined inductively: the empty tree and every leaf are valid, and an internal node with valid left child \(L\) and valid right child \(R\) is valid when its cached aggregate is the aggregate of \(L\) plus the aggregate of \(R\) and its cached length is the size of \(L\) plus the size of \(R\). Here the aggregate and size of the empty tree are \(0\) and \(0\), of a leaf with value \(x\) are \(x\) and \(1\), and of an internal node are its cached aggregate and cached length.

inductive Valid {α : Type u} [AddMonoid α] : SegmentTree α → Prop where
  | empty : Valid .empty
  | leaf (x : α) : Valid (.leaf x)
  | node {left right : SegmentTree α} (hLeft : Valid left)
      (hRight : Valid right) :
      Valid (.node (left.agg + right.agg) (left.size + right.size) left right)

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 3 · Used by 8

Statement usesSegment tree · Aggregate of a segment tree · Size of a segment tree

Used byAggregate of a valid segment tree · Size of a valid segment tree · Correctness of range queries on a valid segment tree · Building a segment tree preserves the list · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Point update preserves validity · Built segment trees are valid

TheoremSize of a valid segment tree#✓fully proved

If \(t\) is a valid segment tree with values in an additive monoid, then the length of the list of leaf values of \(t\), read from left to right, equals the size of \(t\).

theorem length_toList_of_valid {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) : t.toList.length = t.size

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 6 · Used by 3

Statement usesSegment tree · Valid segment trees · Size of a segment tree · Leaf list of a segment tree

Proof usesAggregate of a segment tree · Leaf list of an internal node

Used byCorrectness of range queries on a valid segment tree · Size of a built segment tree · Leaf list after an in-range point update

TheoremAggregate of a valid segment tree#✓fully proved

If \(t\) is a valid segment tree with values in an additive monoid, then the aggregate of \(t\) equals the sum of the leaf values of \(t\), taken from left to right.

theorem agg_eq_sum_toList {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) : t.agg = t.toList.sum

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 6 · Used by 3

Statement usesSegment tree · Valid segment trees · Aggregate of a segment tree · Leaf list of a segment tree

Proof usesSize of a segment tree · Leaf list of an internal node

Used byAggregate of a built segment tree · Aggregate after a point update of a built segment tree · Correctness of range queries on a valid segment tree

DefinitionBuilding a segment tree from a list#✓fully proved

The segment tree built from a list \(L\) with entries in an additive monoid is the empty tree if \(L\) is empty, and a single leaf with value \(x\) if \(L = (x)\). If \(L\) has length \(n \ge 2\), it is the internal node whose left child is the tree built from the first \(\lfloor n/2 \rfloor\) entries of \(L\), whose right child is the tree built from the remaining entries, and which caches the aggregate of the left child plus the aggregate of the right child, in that order, and the sum of the sizes of its children.

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 3 · Used by 8

Statement usesSegment tree · Aggregate of a segment tree · Size of a segment tree

Used byAggregate of a built segment tree · Aggregate after a point update of a built segment tree · Range queries on a built segment tree · Range queries after a point update of a built segment tree · Size of a built segment tree · Building a segment tree preserves the list · Point update of a built segment tree · Built segment trees are valid

TheoremBuilt segment trees are valid#✓fully proved

For every list \(xs\) over an additive monoid, the segment tree built from \(xs\) is valid.

theorem valid_build {α : Type u} [AddMonoid α] (xs : List α) :
    (build xs).Valid

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 7 · Used by 6

Statement usesValid segment trees · Building a segment tree from a list

Proof usesSegment tree · Aggregate of a segment tree · Size of a segment tree · Leaf list of a segment tree · Leaf list of an internal node

Used byAggregate of a built segment tree · Aggregate after a point update of a built segment tree · Range queries on a built segment tree · Range queries after a point update of a built segment tree · Size of a built segment tree · Point update of a built segment tree

TheoremBuilding a segment tree preserves the list#✓fully proved

For every list \(xs\) with entries in an additive monoid, the leaf list of the segment tree built from \(xs\) is \(xs\).

@[simp]
theorem toList_build {α : Type u} [AddMonoid α] (xs : List α) :
    (build xs).toList = xs

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 7 · Used by 4

Statement usesBuilding a segment tree from a list · Leaf list of a segment tree

Proof usesSegment tree · Valid segment trees · Aggregate of a segment tree · Size of a segment tree · Leaf list of an internal node

Used byAggregate of a built segment tree · Range queries on a built segment tree · Size of a built segment tree · Point update of a built segment tree

TheoremSize of a built segment tree#✓fully proved

For every list \(xs\) with entries in an additive monoid, the segment tree built from \(xs\) has size equal to the length of \(xs\).

@[simp]
theorem size_build {α : Type u} [AddMonoid α] (xs : List α) :
    (build xs).size = xs.length

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 6 · Used by 1

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

Proof usesSize of a valid segment tree · Leaf list of a segment tree · Building a segment tree preserves the list · Built segment trees are valid

Used byPoint update of a built segment tree

TheoremAggregate of a built segment tree#✓fully proved

For every list \(L\) with entries in an additive monoid, the aggregate of the segment tree built from \(L\) equals the sum of the entries of \(L\), taken from left to right.

theorem agg_build {α : Type u} [AddMonoid α] (xs : List α) :
    (build xs).agg = xs.sum

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 6

Statement usesAggregate of a segment tree · Building a segment tree from a list

Proof usesAggregate of a valid segment tree · Leaf list of a segment tree · Building a segment tree preserves the list · Built segment trees are valid

DefinitionRange query on a segment tree#✓fully proved

For a segment tree \(t\) with values in an additive monoid and natural numbers \(l, r\), the range query over \([l, r)\), with positions counted from the start of the segment of \(t\), is defined recursively. On the empty tree it is \(0\). On a leaf with value \(x\) it is \(x\) if \(l = 0 < r\), and \(0\) otherwise. On an internal node with cached aggregate \(a\), cached size \(s\) and children \(t_1, t_2\), it is \(0\) if \(r \le l\) or \(s \le l\); otherwise it is \(a\) if \(l = 0\) and \(s \le r\); and in all remaining cases it is the query over \([l, r)\) on \(t_1\) plus the query over \([l - m, r - m)\) on \(t_2\), where \(m\) is the size of \(t_1\) and subtraction is truncated at \(0\).

An empty range and a node disjoint from the range contribute \(0\) without descending, and a fully covered node contributes its cached aggregate.

def query {α : Type u} [AddMonoid α] : SegmentTree α → Nat → Nat → α
  | .empty, _, _ => 0
  | .leaf x, l, r => if l = 0 ∧ 0 < r then x else 0
  | .node cached segmentSize left right, l, r =>
      if r ≤ l then 0
      else if segmentSize ≤ l then 0
      else if l = 0 ∧ segmentSize ≤ r then cached
      else query left l r + query right (l - left.size) (r - left.size)

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 2 · Used by 3

Statement usesSegment tree · Size of a segment tree

Used byRange queries on a built segment tree · Correctness of range queries on a valid segment tree · Range queries after a point update of a built segment tree

TheoremCorrectness of range queries on a valid segment tree#✓fully proved

Let \(t\) be a valid segment tree with values in an additive monoid, let \((x_0, \dots, x_{n-1})\) be its leaf values from left to right, and let \(l, r\) be natural numbers. The range query over \([l, r)\) on \(t\) returns \(\sum_{l \le k < \min(r, n)} x_k\), the sum taken in increasing order of \(k\); it is \(0\) when \(\min(r, n) \le l\).

theorem query_eq {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) (l r : Nat) :
    t.query l r = ((t.toList.drop l).take (r - l)).sum

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 9 · Used by 2

Statement usesSegment tree · Valid segment trees · Range query on a segment tree · Leaf list of a segment tree

Proof usesAggregate of a segment tree · Aggregate of a valid segment tree · Size of a valid segment tree · Size of a segment tree · Leaf list of an internal node

Used byRange queries on a built segment tree · Range queries after a point update of a built segment tree

TheoremRange queries on a built segment tree#✓fully proved

Let \(L = (x_0, \dots, x_{n-1})\) be a list with entries in an additive monoid and let \(l, r\) be natural numbers. The range query over \([l, r)\) on the segment tree built from \(L\) returns \(\sum_{l \le k < \min(r, n)} x_k\), the sum taken in increasing order of \(k\); it is \(0\) when \(\min(r, n) \le l\).

theorem query_build {α : Type u} [AddMonoid α] (xs : List α) (l r : Nat) :
    (build xs).query l r = ((xs.drop l).take (r - l)).sum

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 6

Statement usesBuilding a segment tree from a list · Range query on a segment tree

Proof usesCorrectness of range queries on a valid segment tree · Leaf list of a segment tree · Building a segment tree preserves the list · Built segment trees are valid

DefinitionPoint update of a segment tree#✓fully proved

The point update of a segment tree over an additive monoid at an index \(i \in \mathbb{N}\), relative to the tree's segment, with a value \(y\) is defined recursively. The empty tree stays empty. A leaf becomes a leaf with value \(y\) if \(i = 0\) and is unchanged otherwise. At an internal node with left child \(L\) and right child \(R\): if \(i\) is less than the size of \(L\), then \(L\) is replaced by its point update at \(i\) with \(y\), and otherwise \(R\) is replaced by its point update at \(i\) minus the size of \(L\) with \(y\); the node keeps its cached length, and its cached aggregate becomes the aggregate of the new left child plus the aggregate of the new right child.

def update {α : Type u} [AddMonoid α] : SegmentTree α → Nat → α → SegmentTree α
  | .empty, _, _ => .empty
  | .leaf x, i, y => if i = 0 then .leaf y else .leaf x
  | .node _ segmentSize left right, i, y =>
      if i < left.size then
        let left' := left.update i y
        .node (left'.agg + right.agg) segmentSize left' right
      else
        let right' := right.update (i - left.size) y
        .node (left.agg + right'.agg) segmentSize left right'

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 3 · Used by 7

Statement usesSegment tree · Aggregate of a segment tree · Size of a segment tree

Used byAggregate after a point update of a built segment tree · Range queries after a point update of a built segment tree · Point update preserves the size of a segment tree · Point update of a built segment tree · Out-of-range point update leaves the leaf list unchanged · Leaf list after an in-range point update · Point update preserves validity

TheoremPoint update preserves the size of a segment tree#✓fully proved

For every segment tree \(t\) over an additive monoid, every index \(i\) and every value \(y\), the point update of \(t\) at \(i\) with \(y\) has the same size as \(t\).

Every node on the update path keeps its cached segment length.

@[simp]
theorem size_update {α : Type u} [AddMonoid α] (t : SegmentTree α)
    (i : Nat) (y : α) : (t.update i y).size = t.size

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 4 · Used by 1

Statement usesSegment tree · Size of a segment tree · Point update of a segment tree

Proof usesAggregate of a segment tree

Used byPoint update preserves validity

TheoremPoint update preserves validity#✓fully proved

If \(t\) is a valid segment tree over an additive monoid, then for every natural number \(i\) and every value \(y\), the point update of \(t\) at \(i\) with \(y\) is valid.

theorem Valid.update {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) (i : Nat) (y : α) : (t.update i y).Valid

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 6 · Used by 2

Statement usesSegment tree · Valid segment trees · Point update of a segment tree

Proof usesAggregate of a segment tree · Size of a segment tree · Point update preserves the size of a segment tree

Used byAggregate after a point update of a built segment tree · Range queries after a point update of a built segment tree

TheoremLeaf list after an in-range point update#✓fully proved

Let \(t\) be a valid segment tree over an additive monoid and let \(i\) be a natural number less than the size of \(t\). Then for every value \(y\), the leaf list of the point update of \(t\) at \(i\) with \(y\) is the leaf list of \(t\) with its entry at position \(i\) (counting from \(0\)) replaced by \(y\).

Validity is what ties the cached sizes used for routing to the leaf list.

theorem toList_update_of_lt {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) {i : Nat} (hi : i < t.size) (y : α) :
    (t.update i y).toList = t.toList.set i y

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 8 · Used by 1

Statement usesSegment tree · Valid segment trees · Size of a segment tree · Leaf list of a segment tree · Point update of a segment tree

Proof usesAggregate of a segment tree · Size of a valid segment tree · Leaf list of an internal node

Used byPoint update of a built segment tree

TheoremOut-of-range point update leaves the leaf list unchanged#✓fully proved

For every valid segment tree \(t\) over an additive monoid, every index \(i\) at least the size of \(t\) and every value \(y\), the point update of \(t\) at \(i\) with \(y\) has the same leaf list as \(t\).

theorem toList_update_of_le {α : Type u} [AddMonoid α] {t : SegmentTree α}
    (h : t.Valid) {i : Nat} (hi : t.size ≤ i) (y : α) :
    (t.update i y).toList = t.toList

inductive SegmentTree (α : Type u) where
  | empty : SegmentTree α
  | leaf : α → SegmentTree α
  | node : α → Nat → SegmentTree α → SegmentTree α → SegmentTree α

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:42

Uses 7

Statement usesSegment tree · Valid segment trees · Size of a segment tree · Leaf list of a segment tree · Point update of a segment tree

Proof usesAggregate of a segment tree · Leaf list of an internal node

TheoremPoint update of a built segment tree#✓fully proved

For every list \(xs\) with entries in an additive monoid, every index \(i\) smaller than the length of \(xs\) and every value \(y\), the leaf list of the segment tree built from \(xs\), after the point update at \(i\) with \(y\), is \(xs\) with its entry at position \(i\) (counting from \(0\)) replaced by \(y\).

theorem toList_update_build {α : Type u} [AddMonoid α] {xs : List α}
    {i : Nat} (hi : i < xs.length) (y : α) :
    ((build xs).update i y).toList = xs.set i y

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 8 · Used by 2

Statement usesBuilding a segment tree from a list · Leaf list of a segment tree · Point update of a segment tree

Proof usesSize of a segment tree · Size of a built segment tree · Building a segment tree preserves the list · Leaf list after an in-range point update · Built segment trees are valid

Used byAggregate after a point update of a built segment tree · Range queries after a point update of a built segment tree

TheoremAggregate after a point update of a built segment tree#✓fully proved

Let \(L = (x_0, \dots, x_{n-1})\) be a list with entries in an additive monoid, let \(i < n\), and let \(y\) be an element of the monoid. Applying the point update at index \(i\) with value \(y\) to the segment tree built from \(L\) gives a tree whose aggregate is the sum, taken from left to right, of the list obtained from \(L\) by replacing \(x_i\) with \(y\).

theorem agg_update_build {α : Type u} [AddMonoid α] {xs : List α}
    {i : Nat} (hi : i < xs.length) (y : α) :
    ((build xs).update i y).agg = (xs.set i y).sum

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 8

Statement usesAggregate of a segment tree · Building a segment tree from a list · Point update of a segment tree

Proof usesPoint update preserves validity · Aggregate of a valid segment tree · Leaf list of a segment tree · Point update of a built segment tree · Built segment trees are valid

TheoremRange queries after a point update of a built segment tree#✓fully proved

Let \(L = (x_0, \dots, x_{n-1})\) be a list with entries in an additive monoid, let \(i < n\), let \(y\) be an element of the monoid, and let \(L'\) be the list obtained from \(L\) by replacing \(x_i\) with \(y\), with entries \(x'_0, \dots, x'_{n-1}\). Apply the point update at index \(i\) with value \(y\) to the segment tree built from \(L\). For all natural numbers \(l, r\), the range query over \([l, r)\) on the result returns \(\sum_{l \le k < \min(r, n)} x'_k\), the sum taken in increasing order of \(k\); it is \(0\) when \(\min(r, n) \le l\).

theorem query_update_build {α : Type u} [AddMonoid α] {xs : List α}
    {i : Nat} (hi : i < xs.length) (y : α) (l r : Nat) :
    ((build xs).update i y).query l r =
      (((xs.set i y).drop l).take (r - l)).sum

def build {α : Type u} [AddMonoid α] : List α → SegmentTree α
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (left.agg + right.agg) (left.size + right.size) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

CSLibExt/Algorithms/Lean/DataStructures/SegmentTree.lean:139

Uses 8

Statement usesBuilding a segment tree from a list · Range query on a segment tree · Point update of a segment tree

Proof usesPoint update preserves validity · Correctness of range queries on a valid segment tree · Leaf list of a segment tree · Point update of a built segment tree · Built segment trees are valid

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.