Boolean region quadtree operations

DefinitionCompressing branch constructor for Boolean quadtrees#✓fully proved

A branch constructor that collapses four identical Boolean leaves. This is local compression, not recursive normalization of its arguments.

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

Uses 1 · Used by 12

Statement usesRegion quadtree

Used byLocal compression of compressed children is compressed · 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 · Difference of Boolean quadtrees · Union of Boolean quadtrees

DefinitionBoolean quadtree lookup#✓fully proved

Boolean lookup with false on a nonleaf at scale zero. Leaves ignore coordinates; positive scales use the shared quadrant order.

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:70

Uses 2 · Used by 5

Statement usesRegion quadtree · Quadrant selection by coordinate flags

Used bySix-part correctness of Boolean quadtree operations · 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

DefinitionComplement of a Boolean quadtree#✓fully proved

Complements every leaf, compressing the rebuilt branches.

def neg : QTree Bool → QTree Bool
  | .L b => .L (!b)
  | .Q t0 t1 t2 t3 => Qc (neg t0) (neg t1) (neg t2) (neg t3)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 2 · Used by 6

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees

Used byQuadtree complementation preserves compression · Quadtree complementation negates lookup at sufficient scale · Quadtree difference is pointwise set difference at sufficient scale · Quadtree complementation does not increase height · Height bound for quadtree difference · Difference of Boolean quadtrees

DefinitionUnion of Boolean quadtrees#✓fully proved

Boolean union, short-circuiting constant regions and compressing branches when both inputs are branches.

def qtUnion : QTree Bool → QTree Bool → QTree Bool
  | .L true, _ => .L true
  | .L false, t => t
  | .Q _ _ _ _, .L true => .L true
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtUnion s0 t0) (qtUnion s1 t1) (qtUnion s2 t2) (qtUnion s3 t3)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 2 · Used by 4

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees

Used byQuadtree union preserves compression · Six-part correctness of Boolean quadtree operations · Quadtree union is pointwise disjunction at sufficient scale · Height bound for quadtree union

DefinitionDifference of Boolean quadtrees#✓fully proved

Ordered Boolean difference: cells in the first region but not the second. A full first region complements the second; an empty second returns the first.

def qtDiff : QTree Bool → QTree Bool → QTree Bool
  | .L false, _ => .L false
  | .L true, t => neg t
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q _ _ _ _, .L true => .L false
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtDiff s0 t0) (qtDiff s1 t1) (qtDiff s2 t2) (qtDiff s3 t3)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

def neg : QTree Bool → QTree Bool
  | .L b => .L (!b)
  | .Q t0 t1 t2 t3 => Qc (neg t0) (neg t1) (neg t2) (neg t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:64

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 3 · Used by 4

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees · Complement of a Boolean quadtree

Used byQuadtree difference preserves compression · Six-part correctness of Boolean quadtree operations · Quadtree difference is pointwise set difference at sufficient scale · Height bound for quadtree difference

TheoremLocal compression does not increase quadtree height#✓fully proved

Local compression never increases a branch's height.

theorem height_Qc_le (t0 t1 t2 t3 : QTree Bool) :
    height (Qc t0 t1 t2 t3) ≤
      Nat.succ (max (max (height t0) (height t1))
        (max (height t2) (height t3)))

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 3 · Used by 3

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees · Height of a quadtree

Used byQuadtree complementation does not increase height · Height bound for quadtree difference · Height bound for quadtree union

TheoremLocal compression of compressed children is compressed#✓fully proved

Four compressed children produce a compressed result.

theorem compressed_Qc (t0 t1 t2 t3 : QTree Bool)
    (h0 : compressed t0) (h1 : compressed t1)
    (h2 : compressed t2) (h3 : compressed t3) :
    compressed (Qc t0 t1 t2 t3)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:60

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 3 · Used by 3

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees · Compressed quadtree

Used byQuadtree complementation preserves compression · Quadtree difference preserves compression · Quadtree union preserves compression

TheoremLocal compression preserves lookup at positive scales#✓fully proved

Compression preserves positive-scale lookup. Scale zero is excluded: collapsing four true leaves changes a branch's zero-scale default.

theorem get_Qc_succ (n : Nat) (t0 t1 t2 t3 : QTree Bool) (i j : Nat) :
    get (n + 1) (Qc t0 t1 t2 t3) i j =
      get (n + 1) (QTree.Q t0 t1 t2 t3) i j

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:56

def Qc : QTree Bool → QTree Bool → QTree Bool → QTree Bool → QTree Bool
  | .L x0, .L x1, .L x2, .L x3 =>
      if x0 = x1 ∧ x1 = x2 ∧ x2 = x3 then .L x0
      else .Q (.L x0) (.L x1) (.L x2) (.L x3)
  | t0, t1, t2, t3 => .Q t0 t1 t2 t3

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:48

Uses 4 · Used by 3

Statement usesRegion quadtree · Compressing branch constructor for Boolean quadtrees · Boolean quadtree lookup

Proof usesQuadrant selection by coordinate flags

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

TheoremQuadtree complementation does not increase height#✓fully proved

Complementation does not increase height.

theorem height_neg_le (t : QTree Bool) : height (neg t) ≤ height t

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def neg : QTree Bool → QTree Bool
  | .L b => .L (!b)
  | .Q t0 t1 t2 t3 => Qc (neg t0) (neg t1) (neg t2) (neg t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:64

Uses 5 · Used by 1

Statement usesRegion quadtree · Complement of a Boolean quadtree · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression does not increase quadtree height

Used byHeight bound for quadtree difference

TheoremQuadtree complementation preserves compression#✓fully proved

Complementation preserves compression of the input.

theorem compressed_neg (t : QTree Bool) (hc : compressed t) :
    compressed (neg t)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:60

def neg : QTree Bool → QTree Bool
  | .L b => .L (!b)
  | .Q t0 t1 t2 t3 => Qc (neg t0) (neg t1) (neg t2) (neg t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:64

Uses 4 · Used by 1

Statement usesRegion quadtree · Complement of a Boolean quadtree · Compressed quadtree

Proof usesLocal compression of compressed children is compressed

Used byQuadtree difference preserves compression

TheoremQuadtree complementation negates lookup at sufficient scale#✓fully proved

Complementation negates each lookup whenever the scale bounds height.

theorem get_neg_correct (t : QTree Bool) (n i j : Nat)
    (h : height t ≤ n) : get n (neg t) i j = (!get n t i j)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:56

def neg : QTree Bool → QTree Bool
  | .L b => .L (!b)
  | .Q t0 t1 t2 t3 => Qc (neg t0) (neg t1) (neg t2) (neg t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:64

Uses 8 · Used by 1

Statement usesRegion quadtree · Boolean quadtree lookup · Complement of a Boolean quadtree · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression preserves lookup at positive scales · Height bound for the children of a quadtree branch · Quadrant selection by coordinate flags

Used byQuadtree difference is pointwise set difference at sufficient scale

TheoremHeight bound for quadtree union#✓fully proved

Union height is bounded by the maximum input height.

theorem height_qtUnion_le (t1 t2 : QTree Bool) :
    height (qtUnion t1 t2) ≤ max (height t1) (height t2)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def qtUnion : QTree Bool → QTree Bool → QTree Bool
  | .L true, _ => .L true
  | .L false, t => t
  | .Q _ _ _ _, .L true => .L true
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtUnion s0 t0) (qtUnion s1 t1) (qtUnion s2 t2) (qtUnion s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:70

Uses 5 · Used by 1

Statement usesRegion quadtree · Union of Boolean quadtrees · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression does not increase quadtree height

Used bySix-part correctness of Boolean quadtree operations

TheoremHeight bound for quadtree difference#✓fully proved

Difference height is bounded by the maximum input height.

theorem height_qtDiff_le (t1 t2 : QTree Bool) :
    height (qtDiff t1 t2) ≤ max (height t1) (height t2)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def qtDiff : QTree Bool → QTree Bool → QTree Bool
  | .L false, _ => .L false
  | .L true, t => neg t
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q _ _ _ _, .L true => .L false
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtDiff s0 t0) (qtDiff s1 t1) (qtDiff s2 t2) (qtDiff s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:81

Uses 7 · Used by 1

Statement usesRegion quadtree · Difference of Boolean quadtrees · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression does not increase quadtree height · Quadtree complementation does not increase height · Complement of a Boolean quadtree

Used bySix-part correctness of Boolean quadtree operations

TheoremQuadtree union preserves compression#✓fully proved

Union preserves compression when both inputs are compressed.

theorem compressed_qtUnion (t1 t2 : QTree Bool)
    (hc : compressed t1 ∧ compressed t2) : compressed (qtUnion t1 t2)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:60

def qtUnion : QTree Bool → QTree Bool → QTree Bool
  | .L true, _ => .L true
  | .L false, t => t
  | .Q _ _ _ _, .L true => .L true
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtUnion s0 t0) (qtUnion s1 t1) (qtUnion s2 t2) (qtUnion s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:70

Uses 4 · Used by 1

Statement usesRegion quadtree · Union of Boolean quadtrees · Compressed quadtree

Proof usesLocal compression of compressed children is compressed

Used bySix-part correctness of Boolean quadtree operations

TheoremQuadtree difference preserves compression#✓fully proved

Difference preserves compression when both inputs are compressed.

theorem compressed_qtDiff (t1 t2 : QTree Bool)
    (hc : compressed t1 ∧ compressed t2) : compressed (qtDiff t1 t2)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:60

def qtDiff : QTree Bool → QTree Bool → QTree Bool
  | .L false, _ => .L false
  | .L true, t => neg t
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q _ _ _ _, .L true => .L false
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtDiff s0 t0) (qtDiff s1 t1) (qtDiff s2 t2) (qtDiff s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:81

Uses 5 · Used by 1

Statement usesRegion quadtree · Difference of Boolean quadtrees · Compressed quadtree

Proof usesLocal compression of compressed children is compressed · Quadtree complementation preserves compression

Used bySix-part correctness of Boolean quadtree operations

TheoremQuadtree union is pointwise disjunction at sufficient scale#✓fully proved

Union is pointwise Boolean disjunction at a scale bounding both heights.

theorem get_qtUnion_correct (t1 t2 : QTree Bool) (n i j : Nat)
    (h : height t1 ≤ n ∧ height t2 ≤ n) :
    get n (qtUnion t1 t2) i j = (get n t1 i j || get n t2 i j)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:56

def qtUnion : QTree Bool → QTree Bool → QTree Bool
  | .L true, _ => .L true
  | .L false, t => t
  | .Q _ _ _ _, .L true => .L true
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtUnion s0 t0) (qtUnion s1 t1) (qtUnion s2 t2) (qtUnion s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:70

Uses 8 · Used by 1

Statement usesRegion quadtree · Boolean quadtree lookup · Union of Boolean quadtrees · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression preserves lookup at positive scales · Height bound for the children of a quadtree branch · Quadrant selection by coordinate flags

Used bySix-part correctness of Boolean quadtree operations

TheoremQuadtree difference is pointwise set difference at sufficient scale#✓fully proved

Difference is pointwise conjunction with the second region's complement, provided the scale bounds both heights.

theorem get_qtDiff_correct (t1 t2 : QTree Bool) (n i j : Nat)
    (h : height t1 ≤ n ∧ height t2 ≤ n) :
    get n (qtDiff t1 t2) i j = (get n t1 i j && !get n t2 i j)

inductive QTree (α : Type u) where
  | L : α → QTree α
  | Q : QTree α → QTree α → QTree α → QTree α → QTree α
  deriving DecidableEq

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:44

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:56

def qtDiff : QTree Bool → QTree Bool → QTree Bool
  | .L false, _ => .L false
  | .L true, t => neg t
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q _ _ _ _, .L true => .L false
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtDiff s0 t0) (qtDiff s1 t1) (qtDiff s2 t2) (qtDiff s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:81

Uses 10 · Used by 1

Statement usesRegion quadtree · Boolean quadtree lookup · Difference of Boolean quadtrees · Height of a quadtree

Proof usesCompressing branch constructor for Boolean quadtrees · Local compression preserves lookup at positive scales · Quadtree complementation negates lookup at sufficient scale · Complement of a Boolean quadtree · Height bound for the children of a quadtree branch · Quadrant selection by coordinate flags

Used bySix-part correctness of Boolean quadtree operations

TheoremSix-part correctness of Boolean quadtree operations#✓fully proved

The original graded six-part correctness statement, under its original name.

theorem fdsa_chap13_ex01 :
    (∀ n t1 t2 i j, height t1 ≤ n ∧ height t2 ≤ n →
      get n (qtUnion t1 t2) i j = (get n t1 i j || get n t2 i j)) ∧
    (∀ n t1 t2 i j, height t1 ≤ n ∧ height t2 ≤ n →
      get n (qtDiff t1 t2) i j = (get n t1 i j && !get n t2 i j)) ∧
    (∀ t1 t2, height (qtUnion t1 t2) ≤ max (height t1) (height t2)) ∧
    (∀ t1 t2, height (qtDiff t1 t2) ≤ max (height t1) (height t2)) ∧
    (∀ t1 t2, compressed t1 ∧ compressed t2 → compressed (qtUnion t1 t2)) ∧
    (∀ t1 t2, compressed t1 ∧ compressed t2 → compressed (qtDiff t1 t2))

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)))

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:52

def get : Nat → QTree Bool → Nat → Nat → Bool
  | _, .L b, _, _ => b
  | 0, .Q _ _ _ _, _, _ => false
  | Nat.succ n, .Q t0 t1 t2 t3, i, j =>
      get n (selectTree (decide (i < 2 ^ n)) (decide (j < 2 ^ n))
        t0 t1 t2 t3) (i % 2 ^ n) (j % 2 ^ n)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:56

def qtUnion : QTree Bool → QTree Bool → QTree Bool
  | .L true, _ => .L true
  | .L false, t => t
  | .Q _ _ _ _, .L true => .L true
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtUnion s0 t0) (qtUnion s1 t1) (qtUnion s2 t2) (qtUnion s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:70

def qtDiff : QTree Bool → QTree Bool → QTree Bool
  | .L false, _ => .L false
  | .L true, t => neg t
  | .Q s0 s1 s2 s3, .L false => .Q s0 s1 s2 s3
  | .Q _ _ _ _, .L true => .L false
  | .Q s0 s1 s2 s3, .Q t0 t1 t2 t3 =>
      Qc (qtDiff s0 t0) (qtDiff s1 t1) (qtDiff s2 t2) (qtDiff s3 t3)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Boolean.lean:81

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)

CSLibExt/Algorithms/Lean/DataStructures/Quadtree/Basic.lean:60

Uses 12

Statement usesRegion quadtree · Boolean quadtree lookup · Difference of Boolean quadtrees · Union of Boolean quadtrees · Compressed quadtree · Height of a quadtree

Proof usesQuadtree difference preserves compression · Quadtree union preserves compression · Quadtree difference is pointwise set difference at sufficient scale · Quadtree union is pointwise disjunction at sufficient scale · Height bound for quadtree difference · Height bound for quadtree union

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.