Range tree

29 fully proved

Range Tree

InductiveRange tree#✓fully proved

A one-dimensional range tree over the integers is either empty, a single leaf holding an integer, or a binary node made of two integers \(l\) and \(h\) together with a left and a right subtree. The integers \(l\) and \(h\) are meant to cache the interval \([l, h]\) spanned by the leaf values of the node's subtree; the type does not enforce this, the bounds-correctness predicate does.

inductive RangeTree where
  | empty : RangeTree
  | leaf : Int → RangeTree
  | node : Int → Int → RangeTree → RangeTree → RangeTree

Used by 23

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Bounds-valid range trees · Built range trees are bounds-valid · Building a range tree from a list · Range count · Range count of a bounds-valid tree · Length of the leaf list of a range tree · Membership in a range report · Valid range trees have sorted leaves · Range report · Accumulator range report · Accumulator range report of a bounds-valid range tree · Correctness of the range report · Number of leaves of a range tree · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range tree · Leaf traversal of a range tree with an accumulator · Range-tree leaf traversal appends to its accumulator · Building a range tree preserves the list · Leaf list of a range-tree node · Valid range tree

DefinitionLeaf traversal of a range tree with an accumulator#✓fully proved

For a range tree \(t\) and a list \(a\) of integers, \(\operatorname{aux}(t, a)\) is \(a\) if \(t\) is empty, the list \(x\) followed by \(a\) if \(t\) is a single leaf with value \(x\), and \(\operatorname{aux}(L, \operatorname{aux}(R, a))\) if \(t\) is a node with left subtree \(L\) and right subtree \(R\).

Equivalently, \(\operatorname{aux}(t, a)\) is the leaf list of \(t\) followed by \(a\), so the leaf list is computed in linear time rather than by repeatedly appending left leaf lists.

def toListAux : RangeTree → List Int → List Int
  | .empty, acc => acc
  | .leaf x, acc => x :: acc
  | .node _ _ left right, acc => toListAux left (toListAux right acc)

Uses 1 · Used by 5

Statement usesRange tree

Used byAccumulator range report · Accumulator range report of a bounds-valid range tree · Leaf list of a range tree · Range-tree leaf traversal appends to its accumulator · Leaf list of a range-tree node

DefinitionLeaf list of a range tree#✓fully proved

The leaf list of a range tree \(t\) is the list of the integers stored at its leaves, read from left to right and with repetitions.

def toList (t : RangeTree) : List Int :=
  toListAux t []

Uses 2 · Used by 19

Statement usesRange tree · Leaf traversal of a range tree with an accumulator

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Bounds-valid range trees · Built range trees are bounds-valid · Range counting on a built tree · Range count of a bounds-valid tree · Length of the leaf list of a range tree · Range report membership on a built tree · Membership in a range report · Valid range trees have sorted leaves · Accumulator range report of a bounds-valid range tree · Range report on a built tree · Correctness of the range report · Size of a built range tree · Range-tree leaf traversal appends to its accumulator · Building a range tree preserves the list · Leaf list of a range-tree node · Valid range tree · Building from a sorted list gives a valid range tree

TheoremRange-tree leaf traversal appends to its accumulator#✓fully proved

For every range tree \(t\) and every list \(a\) of integers, the accumulator leaf traversal of \(t\) started from \(a\) equals the leaf list of \(t\) followed by \(a\).

theorem toListAux_eq (t : RangeTree) (acc : List Int) :
    toListAux t acc = t.toList ++ acc

Uses 3 · Used by 2

Statement usesRange tree · Leaf list of a range tree · Leaf traversal of a range tree with an accumulator

Used byAccumulator range report of a bounds-valid range tree · Leaf list of a range-tree node

TheoremLeaf list of a range-tree node#✓fully proved

For all integers \(lo\), \(hi\) and range trees \(L\), \(R\), the leaf list of the node with stored bounds \(lo\), \(hi\), left subtree \(L\) and right subtree \(R\) is the leaf list of \(L\) followed by the leaf list of \(R\).

theorem toList_node (lo hi : Int) (left right : RangeTree) :
    (RangeTree.node lo hi left right).toList = left.toList ++ right.toList

Uses 4 · Used by 5

Statement usesRange tree · Leaf list of a range tree

Proof usesLeaf traversal of a range tree with an accumulator · Range-tree leaf traversal appends to its accumulator

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Length of the leaf list of a range tree · Accumulator range report of a bounds-valid range tree · Building a range tree preserves the list

DefinitionNumber of leaves of a range tree#✓fully proved

The size of a range tree is its number of leaves: \(0\) for the empty tree, \(1\) for a leaf, and the sum of the sizes of the two children for a node.

def size : RangeTree → Nat
  | .empty => 0
  | .leaf _ => 1
  | .node _ _ left right => left.size + right.size

Uses 1 · Used by 2

Statement usesRange tree

Used byLength of the leaf list of a range tree · Size of a built range tree

TheoremLength of the leaf list of a range tree#✓fully proved

For every range tree \(t\), the list of leaf values of \(t\) read from left to right has length equal to the number of leaves of \(t\).

@[simp]
theorem length_toList (t : RangeTree) : t.toList.length = t.size

Uses 4 · Used by 1

Statement usesRange tree · Number of leaves of a range tree · Leaf list of a range tree

Proof usesLeaf list of a range-tree node

Used bySize of a built range tree

DefinitionCached lower bound of a range tree#✓fully proved

For a range tree \(t\), \(\operatorname{tmin}(t)\) is \(0\) if \(t\) is empty, \(x\) if \(t\) is a single leaf with value \(x\), and the stored lower bound \(lo\) if \(t\) is a node with stored bounds \(lo\), \(hi\) and two subtrees.

The value \(0\) for the empty tree is a sentinel without meaning. Computing \(\operatorname{tmin}(t)\) takes constant time: it reads the bound cached at the root and does not traverse the tree.

def tmin : RangeTree → Int
  | .empty => 0
  | .leaf x => x
  | .node lo _ _ _ => lo

Uses 1 · Used by 7

Statement usesRange tree

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Bounds-valid range trees · Built range trees are bounds-valid · Building a range tree from a list · Accumulator range report of a bounds-valid range tree · Building a range tree preserves the list

DefinitionCached upper bound of a range tree#✓fully proved

For a range tree \(t\), \(\operatorname{tmax}(t)\) is \(0\) if \(t\) is empty, \(x\) if \(t\) is a single leaf with value \(x\), and the stored upper bound \(hi\) if \(t\) is a node with stored bounds \(lo\), \(hi\) and two subtrees.

The value \(0\) for the empty tree is a sentinel without meaning.

def tmax : RangeTree → Int
  | .empty => 0
  | .leaf x => x
  | .node _ hi _ _ => hi

Uses 1 · Used by 7

Statement usesRange tree

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Bounds-valid range trees · Built range trees are bounds-valid · Building a range tree from a list · Accumulator range report of a bounds-valid range tree · Building a range tree preserves the list

InductiveBounds-valid range trees#✓fully proved

For a range tree \(s\), write \(s_{\min}\) and \(s_{\max}\) for its cached lower and upper bounds: the stored interval endpoints at a node, the value itself at a leaf, and \(0\) for the empty tree. Bounds-validity is defined inductively: the empty tree and every leaf are bounds-valid, and a node with cached interval \([a, b]\), left child \(\ell\) and right child \(r\) is bounds-valid when \(\ell\) and \(r\) are bounds-valid, each of them has at least one leaf, \(a = \min(\ell_{\min}, r_{\min})\) and \(b = \max(\ell_{\max}, r_{\max})\).

The children must be nonempty because the empty tree has cached bounds \(0\): with an empty child the node cache would only enclose the leaves (a node over an empty child and the single leaf \(5\) could cache \([0, 5]\)), not equal their true interval. In a bounds-valid tree every leaf value lies in the cached interval, and if the tree has a leaf, both cached bounds are leaf values.

inductive BoundsOk : RangeTree → Prop where
  | empty : BoundsOk .empty
  | leaf (x : Int) : BoundsOk (.leaf x)
  | node {lo hi : Int} {left right : RangeTree} (hLeft : BoundsOk left)
      (hRight : BoundsOk right) (hLeftNe : left.toList ≠ [])
      (hRightNe : right.toList ≠ []) (hlo : lo = min left.tmin right.tmin)
      (hhi : hi = max left.tmax right.tmax) :
      BoundsOk (.node lo hi left right)

Uses 4 · Used by 10

Statement usesRange tree · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range tree

Used byThe cached bounds of a nonempty bounds-valid range tree are leaf values · Leaf values of a bounds-valid tree lie between the cached bounds · Built range trees are bounds-valid · Range count of a bounds-valid tree · Membership in a range report · Valid range trees have sorted leaves · Accumulator range report of a bounds-valid range tree · Correctness of the range report · Valid range tree · Building from a sorted list gives a valid range tree

DefinitionValid range tree#✓fully proved

A range tree \(t\) is valid when it has correct cached bounds (every node has two subtrees with nonempty leaf lists, and its stored lower and upper bounds are the minimum of the lower bounds and the maximum of the upper bounds of its two subtrees, recursively) and its leaf list is sorted in nondecreasing order.

def Valid (t : RangeTree) : Prop :=
  BoundsOk t ∧ t.toList.Pairwise (· ≤ ·)

Uses 3 · Used by 2

Statement usesRange tree · Bounds-valid range trees · Leaf list of a range tree

Used byValid range trees have sorted leaves · Building from a sorted list gives a valid range tree

TheoremValid range trees have sorted leaves#✓fully proved

If a range tree \(t\) is valid, then its list of leaf values, read from left to right, is sorted in nondecreasing order.

theorem Valid.pairwise_toList {t : RangeTree} (h : Valid t) :
    t.toList.Pairwise (· ≤ ·)

Uses 4

Statement usesRange tree · Valid range tree · Leaf list of a range tree

Proof usesBounds-valid range trees

TheoremLeaf values of a bounds-valid tree lie between the cached bounds#✓fully proved

Let \(t\) be a bounds-valid range tree, and write \(t_{\min}\) and \(t_{\max}\) for its cached lower and upper bounds. Then every leaf value \(x\) of \(t\) satisfies \(t_{\min} \le x \le t_{\max}\).

theorem bounds_of_mem {t : RangeTree} (hb : BoundsOk t) {x : Int}
    (hx : x ∈ t.toList) :
    t.tmin ≤ x ∧ x ≤ t.tmax

Uses 6 · Used by 1

Statement usesRange tree · Bounds-valid range trees · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range tree

Proof usesLeaf list of a range-tree node

Used byAccumulator range report of a bounds-valid range tree

TheoremThe cached bounds of a nonempty bounds-valid range tree are leaf values#✓fully proved

Let \(t\) be a bounds-valid range tree with at least one leaf. Then the cached lower bound of \(t\) and the cached upper bound of \(t\) are both leaf values of \(t\).

Together with the fact that every leaf value lies between the cached bounds, this shows that the cached interval is exactly the interval spanned by the leaves, not merely an enclosing one.

theorem bounds_mem_toList_of_ne_nil {t : RangeTree} (hb : BoundsOk t)
    (hne : t.toList ≠ []) :
    t.tmin ∈ t.toList ∧ t.tmax ∈ t.toList

Uses 6

Statement usesRange tree · Bounds-valid range trees · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range tree

Proof usesLeaf list of a range-tree node

DefinitionAccumulator range report#✓fully proved

For integers \(a\), \(b\) and a list \(\mathit{acc}\) of integers, the accumulator range report of a range tree for \([a, b]\) starting from \(\mathit{acc}\) is defined by recursion on the tree. The empty tree returns \(\mathit{acc}\). A leaf with value \(x\) returns \(x\) followed by \(\mathit{acc}\) if \(a \le x \le b\), and \(\mathit{acc}\) otherwise. A node with cached interval \([l, h]\) returns \(\mathit{acc}\) if \(h < a\) or \(b < l\); otherwise, if \(a \le l\) and \(h \le b\), it returns the node's leaf values from left to right followed by \(\mathit{acc}\); otherwise it returns the report of the left child starting from the report of the right child starting from \(\mathit{acc}\).

The cached bounds make each pruning test constant-time.

def reportAux : RangeTree → Int → Int → List Int → List Int
  | .empty, _, _, acc => acc
  | .leaf x, lo, hi, acc => if lo ≤ x ∧ x ≤ hi then x :: acc else acc
  | .node nlo nhi left right, lo, hi, acc =>
      if nhi < lo ∨ hi < nlo then acc
      else if lo ≤ nlo ∧ nhi ≤ hi then
        toListAux (.node nlo nhi left right) acc
      else reportAux left lo hi (reportAux right lo hi acc)

Uses 2 · Used by 3

Statement usesRange tree · Leaf traversal of a range tree with an accumulator

Used byRange report · Accumulator range report of a bounds-valid range tree · Correctness of the range report

DefinitionRange report#✓fully proved

The range report of a range tree \(t\) for integers \(a\) and \(b\) is the accumulator range report of \(t\) for \([a, b]\) starting from the empty list.

def report (t : RangeTree) (lo hi : Int) : List Int :=
  reportAux t lo hi []

Uses 2 · Used by 6

Statement usesRange tree · Accumulator range report

Used byRange count · Range count of a bounds-valid tree · Range report membership on a built tree · Membership in a range report · Range report on a built tree · Correctness of the range report

TheoremAccumulator range report of a bounds-valid range tree#✓fully proved

Let \(t\) be a bounds-valid range tree, let \(a\) and \(b\) be integers and let \(\mathit{acc}\) be a list of integers. Then the accumulator range report of \(t\) for \([a, b]\) starting from \(\mathit{acc}\) is the list of the leaf values \(x\) of \(t\) with \(a \le x \le b\), in left-to-right order and with repetitions, followed by \(\mathit{acc}\).

theorem reportAux_eq_filter_append {t : RangeTree} (hb : BoundsOk t)
    (lo hi : Int) (acc : List Int) :
    t.reportAux lo hi acc =
      t.toList.filter (fun x => lo ≤ x ∧ x ≤ hi) ++ acc

Uses 10 · Used by 1

Statement usesRange tree · Bounds-valid range trees · Accumulator range report · Leaf list of a range tree

Proof usesLeaf values of a bounds-valid tree lie between the cached bounds · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf traversal of a range tree with an accumulator · Range-tree leaf traversal appends to its accumulator · Leaf list of a range-tree node

Used byCorrectness of the range report

TheoremCorrectness of the range report#✓fully proved

Let \(t\) be a range tree satisfying the bounds-correctness predicate: every node has two subtrees with at least one leaf each and caches the least and the greatest leaf value of its subtree. For all integers \(a\) and \(b\), the range report of \(t\) for \([a, b]\) equals the list of leaf values \(x\) of \(t\) with \(a \le x \le b\), in left-to-right order.

theorem report_eq_filter {t : RangeTree} (hb : BoundsOk t) (lo hi : Int) :
    t.report lo hi = t.toList.filter (fun x => lo ≤ x ∧ x ≤ hi)

Uses 6 · Used by 3

Statement usesRange tree · Bounds-valid range trees · Range report · Leaf list of a range tree

Proof usesAccumulator range report · Accumulator range report of a bounds-valid range tree

Used byRange count of a bounds-valid tree · Membership in a range report · Range report on a built tree

TheoremMembership in a range report#✓fully proved

Let \(t\) be a range tree satisfying the bounds-correctness predicate: every node has two subtrees with at least one leaf each and caches the least and the greatest leaf value of its subtree. For all integers \(a\), \(b\) and \(x\), the value \(x\) occurs in the range report of \(t\) for \([a, b]\) if and only if \(x\) is a leaf value of \(t\) and \(a \le x \le b\).

theorem mem_report_iff {t : RangeTree} (hb : BoundsOk t) {lo hi x : Int} :
    x ∈ t.report lo hi ↔ x ∈ t.toList ∧ lo ≤ x ∧ x ≤ hi

Uses 5 · Used by 1

Statement usesRange tree · Bounds-valid range trees · Range report · Leaf list of a range tree

Proof usesCorrectness of the range report

Used byRange report membership on a built tree

DefinitionRange count#✓fully proved

For a range tree \(t\) and integers \(a\) and \(b\), the range count of \(t\) over \([a, b]\) is the length of the range report of \(t\) for \([a, b]\).

On a bounds-valid tree this is the number of leaves whose value lies in \([a, b]\).

def count (t : RangeTree) (lo hi : Int) : Nat :=
  (t.report lo hi).length

Uses 2 · Used by 2

Statement usesRange tree · Range report

Used byRange counting on a built tree · Range count of a bounds-valid tree

TheoremRange count of a bounds-valid tree#✓fully proved

Let \(t\) be a bounds-valid range tree and let \(a\) and \(b\) be integers. Then the range count of \(t\) over \([a, b]\) equals the number of leaves of \(t\) whose value lies in \([a, b]\).

theorem count_eq {t : RangeTree} (hb : BoundsOk t) (lo hi : Int) :
    t.count lo hi = (t.toList.filter (fun x => lo ≤ x ∧ x ≤ hi)).length

Uses 6 · Used by 1

Statement usesRange tree · Bounds-valid range trees · Range count · Leaf list of a range tree

Proof usesRange report · Correctness of the range report

Used byRange counting on a built tree

DefinitionBuilding a range tree from a list#✓fully proved

For a range tree \(s\), write \(s_{\min}\) and \(s_{\max}\) for its cached lower and upper bounds. The range tree built from a list \(L\) of integers of length \(n\) is defined by recursion on \(n\): the empty list gives the empty tree, a one-element list \([x]\) gives the leaf \(x\), and for \(n \ge 2\) it is the node whose left child \(\ell\) is the tree built from the first \(\lfloor n/2 \rfloor\) entries of \(L\), whose right child \(r\) is the tree built from the remaining entries, and whose cached interval is \([\min(\ell_{\min}, r_{\min}), \max(\ell_{\max}, r_{\max})]\).

The entries of \(L\) are kept in their given order; \(L\) is not sorted first.

def build : List Int → RangeTree
  | [] => .empty
  | [x] => .leaf x
  | xs@(_ :: _ :: _) =>
      let left := build (xs.take (xs.length / 2))
      let right := build (xs.drop (xs.length / 2))
      .node (min left.tmin right.tmin) (max left.tmax right.tmax) left right
termination_by xs => xs.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

Uses 3 · Used by 7

Statement usesRange tree · Cached upper bound of a range tree · Cached lower bound of a range tree

Used byBuilt range trees are bounds-valid · Range counting on a built tree · Range report membership on a built tree · Range report on a built tree · Size of a built range tree · Building a range tree preserves the list · Building from a sorted list gives a valid range tree

TheoremBuilding a range tree preserves the list#✓fully proved

For every list \(xs\) of integers, the leaf list of the range tree built from \(xs\) is \(xs\).

@[simp]
theorem toList_build : ∀ xs : List Int, (build xs).toList = xs

Uses 6 · Used by 6

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

Proof usesRange tree · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range-tree node

Used byBuilt range trees are bounds-valid · Range counting on a built tree · Range report membership on a built tree · Range report on a built tree · Size of a built range tree · Building from a sorted list gives a valid range tree

TheoremSize of a built range tree#✓fully proved

For every list \(\mathit{xs}\) of integers, the range tree built from \(\mathit{xs}\) has exactly as many leaves as \(\mathit{xs}\) has elements.

@[simp]
theorem size_build (xs : List Int) : (build xs).size = xs.length

Uses 5

Statement usesBuilding a range tree from a list · Number of leaves of a range tree

Proof usesLength of the leaf list of a range tree · Leaf list of a range tree · Building a range tree preserves the list

TheoremBuilt range trees are bounds-valid#✓fully proved

For every list \(L\) of integers, the range tree built from \(L\) by recursive halving is bounds-valid.

theorem boundsOk_build : ∀ xs : List Int, BoundsOk (build xs)

Uses 7 · Used by 4

Statement usesBounds-valid range trees · Building a range tree from a list

Proof usesRange tree · Cached upper bound of a range tree · Cached lower bound of a range tree · Leaf list of a range tree · Building a range tree preserves the list

Used byRange counting on a built tree · Range report membership on a built tree · Range report on a built tree · Building from a sorted list gives a valid range tree

TheoremBuilding from a sorted list gives a valid range tree#✓fully proved

For every list \(xs\) of integers that is sorted in nondecreasing order, the range tree built from \(xs\) is valid.

Without the sortedness hypothesis the built tree still has correct cached bounds, but it need not be valid.

theorem valid_build_of_sorted {xs : List Int} (h : xs.Pairwise (· ≤ ·)) :
    Valid (build xs)

Uses 6

Statement usesValid range tree · Building a range tree from a list

Proof usesBounds-valid range trees · Built range trees are bounds-valid · Leaf list of a range tree · Building a range tree preserves the list

TheoremRange report on a built tree#✓fully proved

For every list \(\mathit{xs}\) of integers and all integers \(a\) and \(b\), the range report for \([a, b]\) on the range tree built from \(\mathit{xs}\) equals the list of elements \(x\) of \(\mathit{xs}\) with \(a \le x \le b\), in their original order.

theorem report_build (xs : List Int) (lo hi : Int) :
    (build xs).report lo hi = xs.filter (fun x => lo ≤ x ∧ x ≤ hi)

Uses 6

Statement usesBuilding a range tree from a list · Range report

Proof usesBuilt range trees are bounds-valid · Correctness of the range report · Leaf list of a range tree · Building a range tree preserves the list

TheoremRange counting on a built tree#✓fully proved

For every list \(L\) of integers and all integers \(a\) and \(b\), the range count over \([a, b]\) of the range tree built from \(L\) equals the number of entries of \(L\), counted with multiplicity, that lie in \([a, b]\).

theorem count_build (xs : List Int) (lo hi : Int) :
    (build xs).count lo hi =
      (xs.filter (fun x => lo ≤ x ∧ x ≤ hi)).length

Uses 6

Statement usesBuilding a range tree from a list · Range count

Proof usesBuilt range trees are bounds-valid · Range count of a bounds-valid tree · Leaf list of a range tree · Building a range tree preserves the list

TheoremRange report membership on a built tree#✓fully proved

For every list \(L\) of integers and all integers \(a\), \(b\) and \(x\), the value \(x\) occurs in the range report for \([a, b]\) on the range tree built from \(L\) if and only if \(x\) is an entry of \(L\) and \(a \le x \le b\).

theorem mem_report_build_iff {xs : List Int} {lo hi x : Int} :
    x ∈ (build xs).report lo hi ↔ x ∈ xs ∧ lo ≤ x ∧ x ≤ hi

Uses 6

Statement usesBuilding a range tree from a list · Range report

Proof usesBuilt range trees are bounds-valid · Membership in a range report · Leaf list of a range tree · Building a range tree preserves the list

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.