Traversal of implicit binary trees

DefinitionDepth-cut frontier of a binary branching step#✓fully proved

The frontier below s, left to right, cut at depth k. At depth zero it is [s], even when step s branches. Duplicate occurrences are retained.

def leaves : ℕ → σ → List σ
  | 0, s => [s]
  | k + 1, s =>
    match step s with
    | none => [s]
    | some (l, h) => leaves k l ++ leaves k h

Used by 13

Used byFrontier occurrences satisfy the resource invariant · Branch-split properties hold at the root iff at some leaf · Deepening the cut past a terminal frontier changes nothing · Depth-cut frontiers are nonempty · Commuting maps transport the ordered frontier · Invariant-restricted step transport of the frontier · Binomial bound on the frontier size under depth and heavy budgets · Final count of counting rounds is the frontier weight · Exact round count for traversing a terminal frontier · Enough rounds empty the stack and collect the frontier · A large enough depth cut yields only terminal states · Additive weight of the root is the sum over the frontier · Pending plus collected occurrences are bounded by the frontier length

DefinitionOne depth-first round of binary branching#✓fully proved

One depth-first round on (stack, output). Terminal states are prepended to the output; a branching state is replaced by its left child followed by its right child.

def round : List σ × List σ → List σ × List σ
  | ([], out) => ([], out)
  | (s :: r, out) =>
    match step s with
    | none => (r, s :: out)
    | some (l, h) => (l :: h :: r, out)

Used by 11

Used byStack invariants hold for every collected leaf · Counting rounds project list-output rounds · Final count of counting rounds is the frontier weight · Exact round count for traversing a terminal frontier · Commuting maps transport any number of rounds · Enough rounds empty the stack and collect the frontier · Commuting maps transport one depth-first round · An empty work stack is fixed by every round · Depth budget bounds the depth-first stack size · Pending plus collected occurrences are bounded by the frontier length · A round does not decrease pending plus collected occurrences

TheoremDepth-cut frontiers are nonempty#✓fully proved

Every depth-cut frontier is nonempty.

theorem leaves_length_pos (k : ℕ) (s : σ) : 0 < (leaves step k s).length

Uses 1 · Used by 1

Statement usesDepth-cut frontier of a binary branching step

Used byExact round count for traversing a terminal frontier

TheoremAn empty work stack is fixed by every round#✓fully proved

An empty work stack is fixed by any number of rounds.

theorem round_nil_iterate (m : ℕ) (out : List σ) : (round step)^[m] ([], out) = ([], out)

Uses 1 · Used by 1

Statement usesOne depth-first round of binary branching

Used byEnough rounds empty the stack and collect the frontier

TheoremExact round count for traversing a terminal frontier#✓fully proved

If every frontier occurrence is terminal, exactly 2 * length - 1 rounds process the tree below s, preserving the tail r and prepending its reversed frontier to out. The terminal-frontier hypothesis is essential: a depth cut may contain branching states.

theorem round_iterate (k : ℕ) (s : σ) (hk : ∀ x ∈ leaves step k s, step x = none) (r out : List σ) :
    (round step)^[2 * (leaves step k s).length - 1] (s :: r, out) =
      (r, (leaves step k s).reverse ++ out)

Uses 3 · Used by 1

Statement usesDepth-cut frontier of a binary branching step · One depth-first round of binary branching

Proof usesDepth-cut frontiers are nonempty

Used byEnough rounds empty the stack and collect the frontier

TheoremEnough rounds empty the stack and collect the frontier#✓fully proved

After at least 2 * length - 1 rounds from [s], the stack is empty and all terminal frontier occurrences have been collected in reverse order.

theorem round_iterate_of_le (k : ℕ) (s : σ) (hk : ∀ x ∈ leaves step k s, step x = none) (R : ℕ)
    (hR : 2 * (leaves step k s).length - 1 ≤ R) :
    (round step)^[R] ([s], []) = ([], (leaves step k s).reverse)

Uses 4 · Used by 2

Statement usesDepth-cut frontier of a binary branching step · One depth-first round of binary branching

Proof usesExact round count for traversing a terminal frontier · An empty work stack is fixed by every round

Used byFinal count of counting rounds is the frontier weight · Pending plus collected occurrences are bounded by the frontier length

TheoremAdditive weight of the root is the sum over the frontier#✓fully proved

A natural-valued weight additive across each branch equals the sum of the frontier weights, even when the frontier is cut before termination.

theorem sum_leaves {σ : Type*} (step : σ → Option (σ × σ)) (f : σ → ℕ)
    (hf : ∀ s l h, step s = some (l, h) → f s = f l + f h)
    (k : ℕ) (s : σ) : f s = ((leaves step k s).map f).sum

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremCommuting maps transport the ordered frontier#✓fully proved

A map commuting with both steps transports the ordered frontier, preserving multiplicity.

theorem leaves_map (h : ∀ x, s₂ (f x) = (s₁ x).map fun lh => (f lh.1, f lh.2))
    (d : ℕ) (x : σ) : leaves s₂ d (f x) = (leaves s₁ d x).map f

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremCommuting maps transport one depth-first round#✓fully proved

A commuting node map transports one stack round and its accumulated output.

theorem round_map (h : ∀ x, s₂ (f x) = (s₁ x).map fun lh => (f lh.1, f lh.2))
    (p : List σ × List σ) :
    round s₂ (p.1.map f, p.2.map f) = ((round s₁ p).1.map f, (round s₁ p).2.map f)

Uses 1 · Used by 1

Statement usesOne depth-first round of binary branching

Used byCommuting maps transport any number of rounds

TheoremCommuting maps transport any number of rounds#✓fully proved

A commuting node map transports any number of rounds. No injectivity is required.

theorem round_iterate_map
    (h : ∀ x, s₂ (f x) = (s₁ x).map fun lh => (f lh.1, f lh.2))
    (i : ℕ) (p : List σ × List σ) :
    (round s₂)^[i] (p.1.map f, p.2.map f) =
      (((round s₁)^[i] p).1.map f, ((round s₁)^[i] p).2.map f)

Uses 2

Statement usesOne depth-first round of binary branching

Proof usesCommuting maps transport one depth-first round

DefinitionWeight-counting depth-first round#✓fully proved

One stack round accumulating natural weights rather than a list of terminal states. The previous count is retained, and each terminal occurrence contributes its weight.

def roundCount {σ : Type*} (step : σ → Option (σ × σ)) (val : σ → ℕ) : List σ × ℕ → List σ × ℕ
  | ([], c) => ([], c)
  | (s :: r, c) =>
    match step s with
    | none => (r, c + val s)
    | some (l, h) => (l :: h :: r, c)

Used by 2

Used byCounting rounds project list-output rounds · Final count of counting rounds is the frontier weight

TheoremCounting rounds project list-output rounds#✓fully proved

Counting rounds are the projection of list-output rounds to the sum of output weights.

theorem roundCount_iterate {σ : Type*} (step : σ → Option (σ × σ)) (val : σ → ℕ)
    (i : ℕ) (st out : List σ) :
    (roundCount step val)^[i] (st, (out.map val).sum) =
      (((round step)^[i] (st, out)).1,
        (((round step)^[i] (st, out)).2.map val).sum)

Uses 2 · Used by 1

Statement usesOne depth-first round of binary branching · Weight-counting depth-first round

Used byFinal count of counting rounds is the frontier weight

TheoremFinal count of counting rounds is the frontier weight#✓fully proved

With a terminal frontier and enough rounds, the final count is its total weight.

theorem roundCount_iterate_of_le {σ : Type*} (step : σ → Option (σ × σ)) (val : σ → ℕ)
    (d : ℕ) (s : σ)
    (hd : ∀ x ∈ leaves step d s, step x = none) (R : ℕ)
    (hR : 2 * (leaves step d s).length - 1 ≤ R) :
    (roundCount step val)^[R] ([s], 0) = ([], ((leaves step d s).map val).sum)

Uses 5

Statement usesDepth-cut frontier of a binary branching step · Weight-counting depth-first round

Proof usesOne depth-first round of binary branching · Counting rounds project list-output rounds · Enough rounds empty the stack and collect the frontier

TheoremBinomial bound on the frontier size under depth and heavy budgets#✓fully proved

With at most d further depth steps and h further heavy steps, the frontier has at most ∑ j ∈ range (h + 1), d.choose j occurrences. The source budget hypotheses are retained, including the strict heavy-budget inequality.

theorem length_leaves_le (hb : ∀ s p t, G s p t → p ≤ D ∧ t ≤ T)
    (hs : ∀ s p t l h, G s p t → step s = some (l, h) → G l (p + 1) t ∧ G h (p + 1) (t + q))
    (k d h : ℕ) (s : σ) (p t : ℕ) (hG : G s p t) (hd : D ≤ p + d) (hh : T < t + (h + 1) * q) :
    (leaves step k s).length ≤ ∑ j ∈ range (h + 1), d.choose j

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremA large enough depth cut yields only terminal states#✓fully proved

A depth allowance covering the remaining depth budget produces only terminal states.

theorem step_eq_none_of_mem_leaves (hb : ∀ s p t, G s p t → p ≤ D ∧ t ≤ T)
    (hs : ∀ s p t l h, G s p t → step s = some (l, h) → G l (p + 1) t ∧ G h (p + 1) (t + q))
    (k : ℕ) (s : σ) (p t : ℕ) (hG : G s p t) (hk : D ≤ p + k) :
    ∀ x ∈ leaves step k s, step x = none

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremFrontier occurrences satisfy the resource invariant#✓fully proved

Every frontier occurrence satisfies the resource invariant at some budgets.

theorem exists_of_mem_leaves
    (hs : ∀ s p t l h, G s p t → step s = some (l, h) → G l (p + 1) t ∧ G h (p + 1) (t + q))
    (k : ℕ) (s : σ) (p t : ℕ) (hG : G s p t) : ∀ x ∈ leaves step k s, ∃ p' t', G x p' t'

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremBranch-split properties hold at the root iff at some leaf#✓fully proved

A property split by branches holds at the root iff it holds at some frontier occurrence.

theorem iff_exists_mem_leaves
    (hs : ∀ s p t l h, G s p t → step s = some (l, h) → G l (p + 1) t ∧ G h (p + 1) (t + q))
    (S : σ → Prop) (hS : ∀ s p t l h, G s p t → step s = some (l, h) → (S s ↔ S l ∨ S h))
    (k : ℕ) (s : σ) (p t : ℕ) (hG : G s p t) : S s ↔ ∃ x ∈ leaves step k s, S x

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremDepth budget bounds the depth-first stack size#✓fully proved

The depth budget bounds the stack by D + 1 at every round; each pending state satisfies the resource invariant. This is a list-size bound, not a machine-space model.

theorem stack_bound (hb : ∀ s p t, G s p t → p ≤ D ∧ t ≤ T)
    (hs : ∀ s p t l h, G s p t → step s = some (l, h) → G l (p + 1) t ∧ G h (p + 1) (t + q))
    (s : σ) (p t : ℕ) (hG : G s p t) (i : ℕ) :
    ((round step)^[i] ([s], [])).1.length ≤ D + 1 ∧
      ∀ x ∈ ((round step)^[i] ([s], [])).1, ∃ p' t', G x p' t'

Uses 1

Statement usesOne depth-first round of binary branching

TheoremInvariant-restricted step transport of the frontier#✓fully proved

Step transport restricted to a preserved invariant transports the frontier and records that all its occurrences satisfy the invariant.

theorem leaves_sim (hsim : ∀ s, I s → (step' s).map (Prod.map f f) = step (f s))
    (hinv : ∀ s l h, I s → step' s = some (l, h) → I l ∧ I h) (k : ℕ) (s : σ') (hs : I s) :
    (leaves step' k s).map f = leaves step k (f s) ∧ ∀ x ∈ leaves step' k s, I x

Uses 1

Statement usesDepth-cut frontier of a binary branching step

TheoremA round does not decrease pending plus collected occurrences#✓fully proved

One round does not decrease the combined number of pending and collected occurrences.

theorem total_le_round (st : List σ × List σ) :
    st.1.length + st.2.length ≤ (round step st).1.length + (round step st).2.length

Uses 1 · Used by 1

Statement usesOne depth-first round of binary branching

Used byPending plus collected occurrences are bounded by the frontier length

TheoremPending plus collected occurrences are bounded by the frontier length#✓fully proved

With a terminal frontier, pending and collected occurrences together never exceed its length, including before traversal is complete.

theorem total_le_leaves (d : ℕ) (s : σ) (hd : ∀ x ∈ leaves step d s, step x = none) (i : ℕ) :
    ((round step)^[i] ([s], [])).1.length + ((round step)^[i] ([s], [])).2.length ≤
      (leaves step d s).length

Uses 4

Statement usesDepth-cut frontier of a binary branching step · One depth-first round of binary branching

Proof usesEnough rounds empty the stack and collect the frontier · A round does not decrease pending plus collected occurrences

TheoremStack invariants hold for every collected leaf#✓fully proved

A property of every state ever on the stack holds of each collected leaf.

theorem out_of_stack (P : σ → Prop) (s : σ)
    (h : ∀ i, ∀ x ∈ ((round step)^[i] ([s], [])).1, P x) (i : ℕ) :
    ∀ x ∈ ((round step)^[i] ([s], [])).2, P x

Uses 1

Statement usesOne depth-first round of binary branching

TheoremDeepening the cut past a terminal frontier changes nothing#✓fully proved

Increasing a depth cut beyond a terminal frontier leaves the list unchanged.

theorem leaves_eq_of_le {σ : Type*} (step : σ → Option (σ × σ)) (D₀ : ℕ) :
    ∀ (D : ℕ) (r : σ), D₀ ≤ D →
    (∀ x ∈ leaves step D₀ r, step x = none) → leaves step D r = leaves step D₀ r

Uses 1

Statement usesDepth-cut frontier of a binary branching step

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.