Function reconstruction by quadtrees

DefinitionSquare region represented by a quadtree#✓fully proved

The represented square: both natural coordinates are below 2 ^ n.

def sqReg (n : Nat) : Set (Nat × Nat) :=
  { p | p.1 < 2 ^ n ∧ p.2 < 2 ^ n }

Used by 3

Used byCorrectness of function reconstruction by quadtrees · Sampled quadtree recovers the function on the represented square · Membership in the represented square

TheoremMembership in the represented square#✓fully proved

Membership in the represented square is a pair of strict bounds.

@[simp]
theorem mem_sqReg (n : Nat) (p : Nat × Nat) :
    p ∈ sqReg n ↔ p.1 < 2 ^ n ∧ p.2 < 2 ^ n

Uses 1

Statement usesSquare region represented by a quadtree

DefinitionPolymorphic quadtree lookup#✓fully proved

Polymorphic lookup. A leaf is constant; at zero scale a branch follows its first child at (0, 0). Positive scales select quadrants by the split.

def get {α : Type u} : Nat → QTree α → Nat → Nat → α
  | _, .L b, _, _ => b
  | 0, .Q t0 _ _ _, _, _ => get 0 t0 0 0
  | 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)

Uses 2 · Used by 2

Statement usesRegion quadtree · Quadrant selection by coordinate flags

Used byCorrectness of function reconstruction by quadtrees · Sampled quadtree recovers the function on the represented square

DefinitionFull quadtree sampled from a function#✓fully proved

Samples f into a full tree. Every branch splits its coordinate square into four equal quadrants, without compressing equal leaves.

def qt_of_fun {α : Type u} (f : Nat → Nat → α) : Nat → QTree α
  | 0 => .L (f 0 0)
  | Nat.succ n =>
      let t0 := qt_of_fun (fun i j => f i j) n
      let t1 := qt_of_fun (fun i j => f i (j + 2 ^ n)) n
      let t2 := qt_of_fun (fun i j => f (i + 2 ^ n) j) n
      let t3 := qt_of_fun (fun i j => f (i + 2 ^ n) (j + 2 ^ n)) n
      .Q t0 t1 t2 t3

Uses 1 · Used by 3

Statement usesRegion quadtree

Used byCorrectness of function reconstruction by quadtrees · Sampled quadtree recovers the function on the represented square · Height of the quadtree sampled from a function

TheoremHeight of the quadtree sampled from a function#✓fully proved

Reconstruction builds exactly the requested number of branch levels.

@[simp]
theorem height_qt_of_fun {α : Type u} (f : Nat → Nat → α) (n : Nat) :
    height (qt_of_fun f n) = n

Uses 3

Statement usesHeight of a quadtree · Full quadtree sampled from a function

Proof usesRegion quadtree

TheoremSampled quadtree recovers the function on the represented square#✓fully proved

Reading a sampled function recovers its value within the represented square.

theorem get_qt_of_fun {α : Type u} (f : Nat → Nat → α) (n i j : Nat)
    (h : (i, j) ∈ sqReg n) : get n (qt_of_fun f n) i j = f i j

Uses 5 · Used by 1

Statement usesPolymorphic quadtree lookup · Full quadtree sampled from a function · Square region represented by a quadtree

Proof usesRegion quadtree · Quadrant selection by coordinate flags

Used byCorrectness of function reconstruction by quadtrees

TheoremCorrectness of function reconstruction by quadtrees#✓fully proved

The original graded reconstruction theorem, under its original name.

theorem fdsa_chap13_ex02 {α : Type u} (f : Nat → Nat → α) (n i j : Nat) :
    (i, j) ∈ sqReg n → get n (qt_of_fun f n) i j = f i j

Uses 4

Statement usesPolymorphic quadtree lookup · Full quadtree sampled from a function · Square region represented by a quadtree

Proof usesSampled quadtree recovers the function on the represented square

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.