Skip to content

k-d tree

28 fully proved

k-d tree

InductiveKd-trees#✓fully proved

A kd-tree over points of \(\mathbb{Z}^d\) is either empty, a leaf holding one point of \(\mathbb{Z}^d\), or a split node holding a split axis \(a \in \{0, \dots, d-1\}\), a split value \(s \in \mathbb{Z}\) and two kd-trees, its left and right subtrees.

inductive KdTree (d : Nat) where
  | empty : KdTree d
  | leaf : (Fin d → Int) → KdTree d
  | node : Fin d → Int → KdTree d → KdTree d → KdTree d
Used by 16
Used byKd-tree construction by median splits · Kd-tree construction from the first axis · Length of the point list of a kd-tree · Range report of a valid kd-tree · Orthogonal range report of a kd-tree · Accumulator range report of a kd-tree · Accumulator range report of a valid kd-tree · Correctness of the kd-tree range report · Size of a kd-tree · Point list of a kd-tree · Kd-tree point traversal with an accumulator · Accumulator traversal of a kd-tree · Building a kd-tree preserves its points · Point list of a kd-tree split node · Kd invariant · Median-split kd-trees satisfy the kd invariant

DefinitionKd-tree point traversal with an accumulator#✓fully proved

For a kd-tree \(t\) over points of \(\mathbb{Z}^d\) and a list \(\mathit{acc}\) of such points, the accumulator traversal of \(t\) onto \(\mathit{acc}\) is \(\mathit{acc}\) when \(t\) is empty, the point \(p\) followed by \(\mathit{acc}\) when \(t\) is a leaf holding \(p\), and, when \(t\) is a split node with left subtree \(L\) and right subtree \(R\), the traversal of \(L\) onto the traversal of \(R\) onto \(\mathit{acc}\).

Threading the output suffix avoids repeatedly appending (and copying) left-subtree results.

def toListAux : KdTree d → List (Fin d → Int) → List (Fin d → Int)
  | .empty, acc => acc
  | .leaf p, acc => p :: acc
  | .node _ _ left right, acc => left.toListAux (right.toListAux acc)
Uses 1 · Used by 3
Statement usesKd-trees
Used byPoint list of a kd-tree · Accumulator traversal of a kd-tree · Point list of a kd-tree split node

DefinitionPoint list of a kd-tree#✓fully proved

The point list of a kd-tree is the list of the points stored at its leaves, from left to right.

def toList (t : KdTree d) : List (Fin d → Int) :=
  t.toListAux []
Uses 2 · Used by 15
Statement usesKd-trees · Kd-tree point traversal with an accumulator
Used byLength of the point list of a kd-tree · Membership in the range report of a built kd-tree · Range report of a valid kd-tree · A built kd-tree holds the same points as its input · Accumulator range report of a valid kd-tree · Range report of a built kd-tree as a filter · Range report of a built kd-tree up to order · Correctness of the kd-tree range report · Size of a built kd-tree · Accumulator traversal of a kd-tree · Building a kd-tree preserves its points · Building a kd-tree from axis 0 preserves its points · Point list of a kd-tree split node · Kd invariant · Median-split kd-trees satisfy the kd invariant

TheoremAccumulator traversal of a kd-tree#✓fully proved

For every kd-tree \(t\) over \(\mathbb{Z}^d\) and every list \(acc\) of points, the accumulator traversal of \(t\) onto \(acc\) equals the list of points of \(t\) in left-to-right order followed by \(acc\).

@[simp]
theorem toListAux_eq (t : KdTree d) (acc : List (Fin d → Int)) :
    t.toListAux acc = t.toList ++ acc
Uses 3 · Used by 1
Statement usesKd-trees · Point list of a kd-tree · Kd-tree point traversal with an accumulator
Used byPoint list of a kd-tree split node

TheoremPoint list of a kd-tree split node#✓fully proved

For a split node with axis \(a\), split value \(s\), left subtree \(L\) and right subtree \(R\), the point list of the node is the point list of \(L\) followed by the point list of \(R\).

@[simp]
theorem toList_node (a : Fin d) (s : Int) (left right : KdTree d) :
    (KdTree.node a s left right).toList = left.toList ++ right.toList
Uses 4 · Used by 4
Statement usesKd-trees · Point list of a kd-tree
Proof usesKd-tree point traversal with an accumulator · Accumulator traversal of a kd-tree
Used byLength of the point list of a kd-tree · Accumulator range report of a valid kd-tree · Building a kd-tree preserves its points · Median-split kd-trees satisfy the kd invariant

DefinitionSize of a kd-tree#✓fully proved

The size of a kd-tree is defined by recursion: the empty tree has size \(0\), a leaf has size \(1\), and a split node has the sum of the sizes of its two children. Since points are stored only at leaves, this is the number of points stored in the tree, counted with multiplicity.

def size : KdTree d → Nat
  | .empty => 0
  | .leaf _ => 1
  | .node _ _ left right => left.size + right.size
Uses 1 · Used by 2
Statement usesKd-trees
Used byLength of the point list of a kd-tree · Size of a built kd-tree

TheoremLength of the point list of a kd-tree#✓fully proved

For every kd-tree \(t\), the list of the points stored in \(t\), read from left to right, has length equal to the size of \(t\), the number of points stored in \(t\).

@[simp]
theorem length_toList (t : KdTree d) : t.toList.length = t.size
Uses 4 · Used by 1
Statement usesKd-trees · Size of a kd-tree · Point list of a kd-tree
Proof usesPoint list of a kd-tree split node
Used bySize of a built kd-tree

DefinitionNext split axis of a kd-tree#✓fully proved

For a dimension \(d \ge 1\) and an axis \(a \in \{0, \dots, d - 1\}\), the next split axis is \((a + 1) \bmod d\), so the axes are visited cyclically.

def nextAxis [NeZero d] (a : Fin d) : Fin d :=
  Fin.ofNat d (a.val + 1)
Used by 3
Used byKd-tree construction by median splits · Building a kd-tree preserves its points · Median-split kd-trees satisfy the kd invariant

AbbreviationMembership in an axis-aligned box#✓fully proved

For \(lo, hi, p \in \mathbb{Z}^d\), the point \(p\) lies in the closed axis-aligned box \([lo, hi]\) when \(lo_i \le p_i \le hi_i\) for every coordinate \(i \in \{0, \dots, d-1\}\).

abbrev inBox (lo hi p : Fin d → Int) : Prop :=
  ∀ i, lo i ≤ p i ∧ p i ≤ hi i
Used by 8
Used byMembership in the range report of a built kd-tree · Range report of a kd-tree built from the first axis · Range report of a valid kd-tree · Accumulator range report of a kd-tree · Accumulator range report of a valid kd-tree · Range report of a built kd-tree as a filter · Range report of a built kd-tree up to order · Correctness of the kd-tree range report

DefinitionAccumulator range report of a kd-tree#✓fully proved

Points are vectors in \(\mathbb{Z}^d\) with coordinates \(p_0, \dots, p_{d-1}\); the box \([lo, hi]\) consists of the points \(p\) with \(lo_i \le p_i \le hi_i\) for every \(i\). For a kd-tree \(t\) and a list \(acc\) of points, the accumulator report of \(t\) for \([lo, hi]\) onto \(acc\) is defined by recursion on \(t\). For the empty tree it is \(acc\). For a leaf \(p\) it is \(p\) followed by \(acc\) if \(p\) lies in the box, and \(acc\) otherwise. For a split node with axis \(a\), split value \(s\), left child \(L\) and right child \(R\), let \(acc'\) be \(acc\) if \(hi_a < s\) and the report of \(R\) onto \(acc\) otherwise; the result is \(acc'\) if \(s < lo_a\) and the report of \(L\) onto \(acc'\) otherwise.

The accumulator avoids repeatedly appending the results of left subtrees, so building the output list costs work linear in the number of reported points; the traversal still visits every node that pruning does not cut, which can be the whole tree even for an empty report. No complexity bound is formalized.

def reportAux : KdTree d → (Fin d → Int) → (Fin d → Int) →
    List (Fin d → Int) → List (Fin d → Int)
  | .empty, _, _, acc => acc
  | .leaf p, lo, hi, acc => if inBox lo hi p then p :: acc else acc
  | .node a s left right, lo, hi, acc =>
      let rightAcc := if hi a < s then acc else reportAux right lo hi acc
      if s < lo a then rightAcc else reportAux left lo hi rightAcc
Uses 2 · Used by 3
Statement usesKd-trees · Membership in an axis-aligned box
Used byOrthogonal range report of a kd-tree · Accumulator range report of a valid kd-tree · Correctness of the kd-tree range report

DefinitionOrthogonal range report of a kd-tree#✓fully proved

For a kd-tree \(t\) over \(\mathbb{Z}^d\) and \(lo, hi \in \mathbb{Z}^d\), the range report of \(t\) for the box \([lo, hi]\) is the accumulator range report of \(t\) for \([lo, hi]\) onto the empty list.

def report (t : KdTree d) (lo hi : Fin d → Int) : List (Fin d → Int) :=
  reportAux t lo hi []
Uses 2 · Used by 6
Statement usesKd-trees · Accumulator range report of a kd-tree
Used byMembership in the range report of a built kd-tree · Range report of a kd-tree built from the first axis · Range report of a valid kd-tree · Range report of a built kd-tree as a filter · Range report of a built kd-tree up to order · Correctness of the kd-tree range report

InductiveKd invariant#✓fully proved

A kd-tree satisfies the kd invariant when at every split node, with axis \(a\) and split value \(s\), every point of the left subtree has \(a\)-coordinate at most \(s\) and every point of the right subtree has \(a\)-coordinate at least \(s\).

inductive Valid : KdTree d → Prop where
  | empty : Valid .empty
  | leaf (p : Fin d → Int) : Valid (.leaf p)
  | node {a : Fin d} {s : Int} {left right : KdTree d} (hLeft : Valid left)
      (hRight : Valid right) (hL : ∀ p ∈ left.toList, p a ≤ s)
      (hR : ∀ p ∈ right.toList, s ≤ p a) : Valid (.node a s left right)
Uses 2 · Used by 6
Statement usesKd-trees · Point list of a kd-tree
Used byRange report of a valid kd-tree · Accumulator range report of a valid kd-tree · Correctness of the kd-tree range report · Building a kd-tree preserves its points · Median-split kd-trees satisfy the kd invariant · Kd-trees built from axis 0 satisfy the kd invariant

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

Let \(t\) be a valid kd-tree over \(\mathbb{Z}^d\), let \(lo, hi \in \mathbb{Z}^d\), and let \(acc\) be a list of points. The accumulator range report of \(t\) for the box \([lo, hi]\) onto \(acc\) equals the list of points of \(t\), in left-to-right order, that lie in the box (the points \(p\) with \(lo_i \le p_i \le hi_i\) for every coordinate \(i\)), followed by \(acc\).

theorem reportAux_eq_filter_append {t : KdTree d} (h : t.Valid)
    (lo hi : Fin d → Int) (acc : List (Fin d → Int)) :
    t.reportAux lo hi acc =
      t.toList.filter (fun p => inBox lo hi p) ++ acc
Uses 6 · Used by 1
Statement usesKd-trees · Kd invariant · Membership in an axis-aligned box · Accumulator range report of a kd-tree · Point list of a kd-tree
Proof usesPoint list of a kd-tree split node
Used byCorrectness of the kd-tree range report

TheoremCorrectness of the kd-tree range report#✓fully proved

For every valid kd-tree \(t\) over \(\mathbb{Z}^d\) and all \(lo, hi \in \mathbb{Z}^d\), the range report of \(t\) for the box \([lo, hi]\) equals the list of points of \(t\), in left-to-right order, that lie in the box, that is, the points \(p\) with \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem report_eq_filter {t : KdTree d} (h : t.Valid)
    (lo hi : Fin d → Int) :
    t.report lo hi = t.toList.filter (fun p => inBox lo hi p)
Uses 7 · Used by 2
Statement usesKd-trees · Kd invariant · Membership in an axis-aligned box · Orthogonal range report of a kd-tree · Point list of a kd-tree
Proof usesAccumulator range report of a kd-tree · Accumulator range report of a valid kd-tree
Used byRange report of a valid kd-tree · Range report of a built kd-tree as a filter

TheoremRange report of a valid kd-tree#✓fully proved

Let \(t\) be a kd-tree over \(\mathbb{Z}^d\) that satisfies the kd invariant, and let \(lo, hi, p \in \mathbb{Z}^d\). Then \(p\) occurs in the range report of \(t\) for the box \([lo, hi]\) if and only if \(p\) is one of the points stored in \(t\) and \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem mem_report_iff {t : KdTree d} (h : t.Valid)
    {lo hi p : Fin d → Int} :
    p ∈ t.report lo hi ↔ p ∈ t.toList ∧ inBox lo hi p
Uses 6 · Used by 1
Statement usesKd-trees · Kd invariant · Membership in an axis-aligned box · Orthogonal range report of a kd-tree · Point list of a kd-tree
Proof usesCorrectness of the kd-tree range report
Used byMembership in the range report of a built kd-tree

DefinitionFirst-point coordinate#✓fully proved

For an axis \(a \in \{0, \dots, d-1\}\) and a list of points in \(\mathbb{Z}^d\), this is the \(a\)-coordinate of the first point of the list, or \(0\) if the list is empty.

def headCoord (a : Fin d) (xs : List (Fin d → Int)) : Int :=
  (xs.head?.map (fun p => p a)).getD 0
Used by 3
Used byKd-tree construction by median splits · Building a kd-tree preserves its points · Median-split kd-trees satisfy the kd invariant

DefinitionKd-tree construction by median splits#✓fully proved

Let \(d \ge 1\), let \(a \in \{0, \dots, d-1\}\) be an axis and let \(P\) be a list of points in \(\mathbb{Z}^d\). The kd-tree built from \(P\) starting at axis \(a\) is the empty tree if \(P\) is empty and the leaf holding \(p\) if \(P = [p]\). If \(P\) has \(n \ge 2\) points, sort \(P\) by \(a\)-coordinate with merge sort, let \(L\) be the first \(\lfloor n/2 \rfloor\) points of the sorted list and \(R\) the remaining ones. The result is the split node with axis \(a\) whose split value is the \(a\)-coordinate of the first point of \(R\), whose left subtree is built from \(L\) and whose right subtree is built from \(R\), both starting at the next axis \((a + 1) \bmod d\).

Cslib.Algorithms.Lean.KdTree.build · 15 lines 
def build [NeZero d] : Fin d → List (Fin d → Int) → KdTree d
  | _, [] => .empty
  | _, [p] => .leaf p
  | a, pts@(_ :: _ :: _) =>
      let sorted := pts.mergeSort (fun p q => p a ≤ q a)
      let k := sorted.length / 2
      .node a (headCoord a (sorted.drop k))
        (build (nextAxis a) (sorted.take k))
        (build (nextAxis a) (sorted.drop k))
termination_by _ pts => pts.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_mergeSort,
      List.length_cons]
    omega
Uses 3 · Used by 8
Statement usesKd-trees · First-point coordinate · Next split axis of a kd-tree
Used byKd-tree construction from the first axis · Membership in the range report of a built kd-tree · A built kd-tree holds the same points as its input · Range report of a built kd-tree as a filter · Range report of a built kd-tree up to order · Size of a built kd-tree · Building a kd-tree preserves its points · Median-split kd-trees satisfy the kd invariant

TheoremMedian-split kd-trees satisfy the kd invariant#✓fully proved

For \(d \ge 1\), every axis \(a\) and every list of points of \(\mathbb{Z}^d\), the kd-tree built from the list by median splits starting at axis \(a\) satisfies the kd invariant.

theorem valid_build [NeZero d] (a : Fin d) (pts : List (Fin d → Int)) :
    (build a pts).Valid
Uses 7 · Used by 3
Statement usesKd invariant · Kd-tree construction by median splits
Proof usesKd-trees · First-point coordinate · Next split axis of a kd-tree · Point list of a kd-tree · Point list of a kd-tree split node
Used byMembership in the range report of a built kd-tree · Range report of a built kd-tree as a filter · Kd-trees built from axis 0 satisfy the kd invariant

TheoremBuilding a kd-tree preserves its points#✓fully proved

For \(d \ge 1\), every axis \(a\) and every list of points of \(\mathbb{Z}^d\), the point list of the kd-tree built from the list by median splits starting at axis \(a\) is a permutation of the list.

theorem toList_build_perm [NeZero d] (a : Fin d) (pts : List (Fin d → Int)) :
    (build a pts).toList.Perm pts
Uses 7 · Used by 4
Statement usesKd-tree construction by median splits · Point list of a kd-tree
Proof usesKd-trees · Kd invariant · First-point coordinate · Next split axis of a kd-tree · Point list of a kd-tree split node
Used byA built kd-tree holds the same points as its input · Range report of a built kd-tree up to order · Size of a built kd-tree · Building a kd-tree from axis 0 preserves its points

TheoremA built kd-tree holds the same points as its input#✓fully proved

Let \(d \ge 1\), let \(a \in \{0, \dots, d-1\}\) and let \(P\) be a list of points in \(\mathbb{Z}^d\). A point \(p \in \mathbb{Z}^d\) is stored in the kd-tree built from \(P\) by median splits starting at axis \(a\) if and only if \(p\) occurs in \(P\).

theorem mem_toList_build_iff [NeZero d] (a : Fin d) (pts : List (Fin d → Int))
    (p : Fin d → Int) :
    p ∈ (build a pts).toList ↔ p ∈ pts
Uses 3 · Used by 1
Statement usesKd-tree construction by median splits · Point list of a kd-tree
Proof usesBuilding a kd-tree preserves its points
Used byMembership in the range report of a built kd-tree

TheoremSize of a built kd-tree#✓fully proved

Let \(d \ge 1\). For every starting axis \(a\) and every list \(P\) of points of \(\mathbb{Z}^d\), the size of the kd-tree built from \(P\) starting at axis \(a\) equals the length of \(P\) (repeated points counted with multiplicity).

@[simp]
theorem size_build [NeZero d] (a : Fin d) (pts : List (Fin d → Int)) :
    (build a pts).size = pts.length
Uses 5
Statement usesKd-tree construction by median splits · Size of a kd-tree
Proof usesLength of the point list of a kd-tree · Point list of a kd-tree · Building a kd-tree preserves its points

DefinitionKd-tree construction from the first axis#✓fully proved

For \(d \ge 1\) and a list of points in \(\mathbb{Z}^d\), this is the kd-tree built from the list by alternating-axis median splits, starting with split axis \(0\).

def buildRoot [NeZero d] (pts : List (Fin d → Int)) : KdTree d :=
  build (Fin.ofNat d 0) pts
Uses 2 · Used by 3
Statement usesKd-trees · Kd-tree construction by median splits
Used byRange report of a kd-tree built from the first axis · Building a kd-tree from axis 0 preserves its points · Kd-trees built from axis 0 satisfy the kd invariant

TheoremKd-trees built from axis 0 satisfy the kd invariant#✓fully proved

For \(d \ge 1\) and every list of points of \(\mathbb{Z}^d\), the kd-tree built from the list by median splits starting at axis \(0\) satisfies the kd invariant.

theorem valid_buildRoot [NeZero d] (pts : List (Fin d → Int)) :
    (buildRoot pts).Valid
Uses 3
Statement usesKd invariant · Kd-tree construction from the first axis
Proof usesMedian-split kd-trees satisfy the kd invariant

TheoremBuilding a kd-tree from axis 0 preserves its points#✓fully proved

For \(d \ge 1\) and every list of points of \(\mathbb{Z}^d\), the point list of the kd-tree built from the list by median splits starting at axis \(0\) is a permutation of the list.

theorem toList_buildRoot_perm [NeZero d] (pts : List (Fin d → Int)) :
    (buildRoot pts).toList.Perm pts
Uses 3
Statement usesKd-tree construction from the first axis · Point list of a kd-tree
Proof usesBuilding a kd-tree preserves its points

TheoremRange report of a built kd-tree as a filter#✓fully proved

Let \(d \ge 1\). For every starting axis \(a\), every list \(P\) of points of \(\mathbb{Z}^d\) and all \(lo, hi \in \mathbb{Z}^d\), let \(T\) be the kd-tree built from \(P\) starting at axis \(a\). The range report of \(T\) for the box \([lo, hi]\) equals the list of points of \(T\), in left-to-right order, that lie in the box, that is, the points \(p\) with \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem report_build [NeZero d] (a : Fin d) (pts : List (Fin d → Int))
    (lo hi : Fin d → Int) :
    (build a pts).report lo hi =
      (build a pts).toList.filter (fun p => inBox lo hi p)
Uses 6 · Used by 1
Statement usesKd-tree construction by median splits · Membership in an axis-aligned box · Orthogonal range report of a kd-tree · Point list of a kd-tree
Proof usesCorrectness of the kd-tree range report · Median-split kd-trees satisfy the kd invariant
Used byRange report of a built kd-tree up to order

TheoremRange report of a built kd-tree up to order#✓fully proved

Let \(d \ge 1\). For every starting axis \(a\), every list \(P\) of points of \(\mathbb{Z}^d\) and all \(lo, hi \in \mathbb{Z}^d\), the range report for the box \([lo, hi]\) of the kd-tree built from \(P\) starting at axis \(a\) is a permutation of the list of entries of \(P\) that lie in the box, that is, the points \(p\) with \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem report_build_perm [NeZero d] (a : Fin d) (pts : List (Fin d → Int))
    (lo hi : Fin d → Int) :
    ((build a pts).report lo hi).Perm
      (pts.filter (fun p => inBox lo hi p))
Uses 6
Statement usesKd-tree construction by median splits · Membership in an axis-aligned box · Orthogonal range report of a kd-tree
Proof usesRange report of a built kd-tree as a filter · Point list of a kd-tree · Building a kd-tree preserves its points

TheoremMembership in the range report of a built kd-tree#✓fully proved

Let \(d \ge 1\), let \(a \in \{0, \dots, d-1\}\), let \(P\) be a list of points in \(\mathbb{Z}^d\) and let \(lo, hi, p \in \mathbb{Z}^d\). Then \(p\) occurs in the range report, for the box \([lo, hi]\), of the kd-tree built from \(P\) by median splits starting at axis \(a\) if and only if \(p\) occurs in \(P\) and \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem mem_report_build_iff [NeZero d] (a : Fin d) (pts : List (Fin d → Int))
    {lo hi p : Fin d → Int} :
    p ∈ (build a pts).report lo hi ↔ p ∈ pts ∧ inBox lo hi p
Uses 7 · Used by 1
Statement usesKd-tree construction by median splits · Membership in an axis-aligned box · Orthogonal range report of a kd-tree
Proof usesRange report of a valid kd-tree · A built kd-tree holds the same points as its input · Point list of a kd-tree · Median-split kd-trees satisfy the kd invariant
Used byRange report of a kd-tree built from the first axis

TheoremRange report of a kd-tree built from the first axis#✓fully proved

Let \(d \ge 1\), let \(P\) be a list of points in \(\mathbb{Z}^d\) and let \(lo, hi, p \in \mathbb{Z}^d\). Then \(p\) occurs in the range report, for the box \([lo, hi]\), of the kd-tree built from \(P\) by median splits starting at axis \(0\) if and only if \(p\) occurs in \(P\) and \(lo_i \le p_i \le hi_i\) for every coordinate \(i\).

theorem mem_report_buildRoot_iff [NeZero d] (pts : List (Fin d → Int))
    {lo hi p : Fin d → Int} :
    p ∈ (buildRoot pts).report lo hi ↔ p ∈ pts ∧ inBox lo hi p
Uses 4
Statement usesKd-tree construction from the first axis · Membership in an axis-aligned box · Orthogonal range report of a kd-tree
Proof usesMembership in the range report of a built kd-tree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.