Skip to content

Quadtree carrier and structural invariants

5 fully proved

Quadtrees

InductiveRegion quadtree#✓fully proved

A finite region quadtree with a value leaf or four ordered quadrants.

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq
Used by 26
Used byQuadtree complementation preserves compression · Local compression of compressed children is compressed · Quadtree difference preserves compression · Quadtree union preserves compression · Six-part correctness of Boolean quadtree operations · Boolean quadtree lookup · Quadtree complementation negates lookup at sufficient scale · Local compression preserves lookup at positive scales · Quadtree difference is pointwise set difference at sufficient scale · Quadtree union is pointwise disjunction at sufficient scale · Quadtree complementation does not increase height · Local compression does not increase quadtree height · Height bound for quadtree difference · Height bound for quadtree union · Complement of a Boolean quadtree · Compressing branch constructor for Boolean quadtrees · Difference of Boolean quadtrees · Union of Boolean quadtrees · Polymorphic quadtree lookup · Sampled quadtree recovers the function on the represented square · Height of the quadtree sampled from a function · Full quadtree sampled from a function · Compressed quadtree · Height of a quadtree · Height bound for the children of a quadtree branch · Quadrant selection by coordinate flags

DefinitionHeight of a quadtree#✓fully proved

The maximum number of branches from the root to a leaf.

def height {α : Type u} : QTree α → Nat
  | .L _ => 0
  | .Q t0 t1 t2 t3 =>
      Nat.succ (max (max (height t0) (height t1))
        (max (height t2) (height t3)))
Uses 1 · Used by 10
Statement usesRegion quadtree
Used bySix-part correctness of Boolean quadtree operations · Quadtree complementation negates lookup at sufficient scale · Quadtree difference is pointwise set difference at sufficient scale · Quadtree union is pointwise disjunction at sufficient scale · Quadtree complementation does not increase height · Local compression does not increase quadtree height · Height bound for quadtree difference · Height bound for quadtree union · Height of the quadtree sampled from a function · Height bound for the children of a quadtree branch

DefinitionCompressed quadtree#✓fully proved

Every subtree is compressed and no branch has four identical leaves. Identical nonleaf children are allowed: they need not represent a constant.

def compressed {α : Type u} : QTree α → Prop
  | .L _ => True
  | .Q t0 t1 t2 t3 =>
      compressed t0 ∧ compressed t1 ∧ compressed t2 ∧ compressed t3 ∧
        ¬ (∃ x, t0 = .L x ∧ t1 = t0 ∧ t2 = t0 ∧ t3 = t0)
Uses 1 · Used by 5
Statement usesRegion quadtree
Used byQuadtree complementation preserves compression · Local compression of compressed children is compressed · Quadtree difference preserves compression · Quadtree union preserves compression · Six-part correctness of Boolean quadtree operations

DefinitionQuadrant selection by coordinate flags#✓fully proved

Selects low/low, low/high, high/low, or high/high, respectively, when (x, y) is (true, true), (true, false), (false, true), or (false, false). In lookup, true means that the corresponding coordinate is below the split.

def selectTree {α : Type u} (x y : Bool)
    (t0 t1 t2 t3 : QTree α) : QTree α :=
  if x then if y then t0 else t1 else if y then t2 else t3
Uses 1 · Used by 7
Statement usesRegion quadtree
Used byBoolean quadtree lookup · Quadtree complementation negates lookup at sufficient scale · Local compression preserves lookup at positive scales · Quadtree difference is pointwise set difference at sufficient scale · Quadtree union is pointwise disjunction at sufficient scale · Polymorphic quadtree lookup · Sampled quadtree recovers the function on the represented square

TheoremHeight bound for the children of a quadtree branch#✓fully proved

A bound on branch height bounds all four child heights one level lower.

theorem height_children_le {α : Type u} {t0 t1 t2 t3 : QTree α}
    {n : Nat} (h : height (.Q t0 t1 t2 t3) ≤ n + 1) :
    height t0 ≤ n ∧ height t1 ≤ n ∧ height t2 ≤ n ∧ height t3 ≤ n
Uses 2 · Used by 3
Statement usesRegion quadtree · Height of a quadtree
Used byQuadtree complementation negates lookup at sufficient scale · Quadtree difference is pointwise set difference at sufficient scale · Quadtree union is pointwise disjunction at sufficient scale

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.