Browse chapters

Imports

import CLRSLean.Chapter_15.Section_15_5_Optimal_Binary_Search_Trees
import CLRSLean.FourthEdition.Chapter_14.Section_14_2_Matrix_Chain_Multiplication

14.5. Optimal Binary Search Trees

The legacy CLRS.Chapter15.OBST.bottomUpOBST evaluates a recursive optimal-cost specification and repeats intervals. The obstRoot and obstReconstruct interfaces here are likewise specification-based selectors/reconstruction; the dimension formulas alone do not bound their runtime.

The Execution companion stores interval costs, weights, and selected roots in arrays, using strictly shorter previously stored intervals. Each interval computes its weight by one cached weight update before scanning roots. Reconstruction reads those stored roots and never reruns the old recursive oracle. The execution refines the recurrence and gives optimal plans, with cell/candidate counts attached to the same fill.

Weights p q : Nat → Nat are nonnegative integer frequencies, including zero. They are not arbitrary normalized real probabilities, and no general scaling-to-probabilities theorem is provided. Natural arithmetic and array access are primitive events; bit arithmetic, persistent copying, and allocation are outside the cost model.

Notation conventions used in this section:

p : successful-search integer weights
q : unsuccessful-search (dummy key) integer weights
i, j : the interval of keys i+1, ..., j

              namespace CLRSnamespace Chapter15namespace OBSTopen Finset

The computable root table



private lemma exists_inf'_eq (s : Finset ℕ) (h : s.Nonempty) (f : ℕ → ℕ) :
    ∃ a ∈ s, f a = s.inf' h f := by
  induction' s using Finset.induction with a s has ih
  · exact absurd h (by simp)
  · by_cases hs : s.Nonempty
    · rcases ih hs with ⟨b, hb, hb_eq⟩
      rw [Finset.inf'_insert hs f]
      by_cases hle : f a ≤ s.inf' hs f
      · rw [min_eq_left hle]
        exact ⟨a, Finset.mem_insert_self a s, rfl⟩
      · rw [min_eq_right (by omega : s.inf' hs f ≤ f a)]
        rw [← hb_eq]
        exact ⟨b, Finset.mem_insert_of_mem hb, rfl⟩
    · have hsingleton : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
      subst hsingleton
      simp

A recurrence-based root selector (not a cached table): for interval i < j, it selects the smallest admissible root r ∈ [i+1, j] that attains the recurrence minimum; the diagonal is the junk value i.


def obstRoot (p q : Nat → Nat) (i j : Nat) : Nat :=
  if h : i < j then
    (Finset.Icc (i + 1) j).filter
      (fun r =>
        bottomUpOBST p q i (r - 1) + bottomUpOBST p q r j + weight p q i j =
          bottomUpOBST p q i j) |>.min'
      (by
        have h_nonempty : (Finset.Icc (i + 1) j).Nonempty := by
          use i + 1; simp [Finset.mem_Icc]; exact h
        let f (r : ℕ) := bottomUpOBST p q i (r - 1) + bottomUpOBST p q r j + weight p q i j
        have h_rec : bottomUpOBST p q i j = (Finset.Icc (i + 1) j).inf' h_nonempty f :=
          (bottomUpOBST_obstRecurrence p q).2 h
        have h_exists := exists_inf'_eq (Finset.Icc (i + 1) j) h_nonempty f
        rw [← h_rec] at h_exists
        rcases h_exists with ⟨r, hr, hr_eq⟩
        exact ⟨r, Finset.mem_filter.mpr ⟨hr, hr_eq⟩⟩)
  else
    i

The computable root table is tight for CLRS.Chapter15.OBST.bottomUpOBST: each non-singleton interval chooses an admissible root that attains the recurrence equality.


theorem obstRoot_optimal (p q : Nat → Nat) :
    OBSTRootOptimal p q (bottomUpOBST p q) (obstRoot p q) := by
  refine ⟨?_, ?_⟩
  · intro i
    rw [bottomUpOBST]
    simp
  · intro i j hij
    let s : Finset ℕ := Finset.Icc (i + 1) j
    have h_nonempty : s.Nonempty := by use i + 1; simp [s, Finset.mem_Icc]; exact hij
    let f (r : ℕ) := bottomUpOBST p q i (r - 1) + bottomUpOBST p q r j + weight p q i j
    have h_rec : bottomUpOBST p q i j = s.inf' h_nonempty f :=
      (bottomUpOBST_obstRecurrence p q).2 hij
    have h_exists : ∃ r ∈ s, f r = bottomUpOBST p q i j := by
      rw [h_rec]; exact exists_inf'_eq s h_nonempty f
    have h_filter_nonempty : (s.filter fun r => f r = bottomUpOBST p q i j).Nonempty := by
      rcases h_exists with ⟨r, hr, hr_eq⟩
      exact ⟨r, Finset.mem_filter.mpr ⟨hr, hr_eq⟩⟩
    set r := (s.filter fun r => f r = bottomUpOBST p q i j).min' h_filter_nonempty with hr_def
    have hr_mem_filter : r ∈ s.filter fun r => f r = bottomUpOBST p q i j := by
      rw [hr_def]; exact Finset.min'_mem _ h_filter_nonempty
    have hr_mem : r ∈ s := (Finset.mem_filter.mp hr_mem_filter).1
    have hr_eq : f r = bottomUpOBST p q i j := (Finset.mem_filter.mp hr_mem_filter).2
    have h_root_val : obstRoot p q i j = r := by
      unfold obstRoot
      simp [hij, s, f, hr_def]
    rw [h_root_val]
    refine ⟨hr_mem, ?_⟩
    dsimp [f] at hr_eq
    rw [← hr_eq]

Public reconstruction

Construct a CLRS.Chapter15.OBST.BSTPlan recursively following the computable root table CLRS.Chapter15.OBST.obstRoot.


def obstReconstruct (p q : Nat → Nat) (i j : Nat) (hij : i ≤ j) : BSTPlan i j :=
  if h : i < j then
    let r := obstRoot p q i j
    have hmem := Finset.mem_Icc.mp ((obstRoot_optimal p q).2 h).1
    have h_lt_r : i < r := by omega
    have h_left_bound : i ≤ r - 1 := by omega
    BSTPlan.node r h_lt_r hmem.2
      (obstReconstruct p q i (r - 1) h_left_bound)
      (obstReconstruct p q r j hmem.2)
  else
    have heq : i = j := by omega
    heq ▸ BSTPlan.empty j
termination_by j - i
decreasing_by
  · have Variable name `hhi` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hhi : obstRoot p q i j ≤ j := (Finset.mem_Icc.mp ((obstRoot_optimal p q).2 h).1).2
    omega
  · have Variable name `hlo` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hlo : i + 1 ≤ obstRoot p q i j := (Finset.mem_Icc.mp ((obstRoot_optimal p q).2 h).1).1
    omega

The plan built by CLRS.Chapter15.OBST.obstReconstruct follows the root table.


theorem obstReconstruct_reconstructed (p q : Nat → Nat) (i j : Nat) (hij : i ≤ j) :
    ReconstructedBy (obstRoot p q) (obstReconstruct p q i j hij) := by
  unfold obstReconstruct
  split
  · next h =>
    have hmem := Finset.mem_Icc.mp ((obstRoot_optimal p q).2 h).1
    have h_left_bound : i ≤ obstRoot p q i j - 1 := by omega
    have h_lt : (obstRoot p q i j - 1) - i < j - i := by
      have hhi : obstRoot p q i j ≤ j := hmem.2
      omega
    have h_rt : j - obstRoot p q i j < j - i := by
      have hlo : i + 1 ≤ obstRoot p q i j := hmem.1
      omega
    simp
    exact ⟨rfl,
      obstReconstruct_reconstructed p q i (obstRoot p q i j - 1) h_left_bound,
      obstReconstruct_reconstructed p q (obstRoot p q i j) j hmem.2⟩
  · next h =>
    have heq : i = j := by omega
    subst heq
    simp [ReconstructedBy]
termination_by j - i
decreasing_by
  exact h_lt
  exact h_rt

Time and space bounds

OPTIMAL-BST stores O(n²) table entries (the same triangular table as MATRIX-CHAIN-ORDER).

theorem obstTableSpace_le_square (n : Nat) : matrixChainSpace n ≤ (n + 2) ^ 2 :=
  matrixChainSpace_le_square n

OPTIMAL-BST performs O(n³) root evaluations (the same triangular scan as MATRIX-CHAIN-ORDER).

theorem obstTableTime_le_cubic (n : Nat) : matrixChainTime n ≤ (n + 1) ^ 3 :=
  matrixChainTime_le_cubic n

              end OBSTend Chapter15end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_14.Section_14_5_Optimal_Binary_Search_Trees.Execution

Stored optimal-BST costs, weights, and roots

For N keys, layer l contains intervals [i,i+l] with keys i+1 through i+l. Each weight is updated once from the previous layer; each admissible root is scanned once using stored child costs. Nonnegative natural weights are used, without a claim of arbitrary real probability normalization.

              namespace CLRS.Chapter15.OBST.Executionopen DPExecutionstructure Cell where
  cost : Nat
  weight : Nat
  root : Nat
  deriving Inhabited, Repr, DecidableEq

A constant-work weight update, independent of the number of candidate roots.

def nextWeight (p q : Nat → Nat) (rows : Array (Array Cell)) (i l : Nat) : Nat :=
  (get rows l i).weight + p (i+l+1) + q (i+l+1)

def candidate (rows : Array (Array Cell)) (i l w r : Nat) : Nat :=
  (get rows (r-1-i) i).cost + (get rows (i+l-r) r).cost + w

def step (p q : Nat → Nat) : Nat → Array (Array Cell) → Nat → Cell × Nat
  | 0, _, i => (⟨q i, q i, i⟩, 0)
  | l+1, rows, i =>
      let w := nextWeight p q rows i l
      let best := minimum (candidate rows i (l+1) w) (i+1) l
      (⟨best.value, w, best.index⟩, best.visits)

Compute all cost, weight, and root entries for N keys.

def execute (p q : Nat → Nat) (N : Nat) : Table Cell :=
  buildLayers (fun l => N+1-l) (step p q) (N+1)

              def CorrectCell (p q : Nat → Nat) (l i : Nat) (cell : Cell) : Prop :=
  cell.cost = bottomUpOBST p q i (i+l) ∧ cell.weight = OBST.weight p q i (i+l) ∧
  (0 < l → i < cell.root ∧ cell.root ≤ i+l ∧
    cell.cost = bottomUpOBST p q i (cell.root-1) +
      bottomUpOBST p q cell.root (i+l) + OBST.weight p q i (i+l))

private theorem weight_succ (p q : Nat → Nat) (i l : Nat) :
    OBST.weight p q i (i+l+1) = OBST.weight p q i (i+l) + p (i+l+1) + q (i+l+1) := by
  unfold OBST.weight
  rw [Finset.sum_Icc_succ_top (by omega), Finset.sum_Icc_succ_top (by omega)]
  ring

private theorem candidate_correct (p q : Nat → Nat) (N l i : Nat)
    (rows : Array (Array Cell))
    (hprev : ∀ k, k < l → ∀ i, i < N+1-k → CorrectCell p q k i (get rows k i))
    (hi : i < N+1-l) (r : Nat) (hr : i < r) (hr' : r ≤ i+l) :
    candidate rows i l (OBST.weight p q i (i+l)) r =
      bottomUpOBST p q i (r-1) + bottomUpOBST p q r (i+l) + OBST.weight p q i (i+l) := by
  have hleft := (hprev (r-1-i) (by omega) i (by omega)).1
  have hright := (hprev (i+l-r) (by omega) r (by omega)).1
  have he : i+(r-1-i) = r-1 := by omega
  have he' : r+(i+l-r) = i+l := by omega
  rw [he] at hleft
  rw [he'] at hright
  simp only [candidate, hleft, hright]

private theorem step_correct (p q : Nat → Nat) (N l : Nat)
    (rows : Array (Array Cell))
    (hprev : ∀ k, k < l → ∀ i, i < N+1-k → CorrectCell p q k i (get rows k i))
    (i : Nat) (hi : i < N+1-l) : CorrectCell p q l i (step p q l rows i).1 := by
  cases l with
  | zero =>
      change q i = bottomUpOBST p q i (i+0) ∧ q i = OBST.weight p q i (i+0) ∧ _
      refine ⟨by simpa using ((bottomUpOBST_obstRecurrence p q).1 i).symm, ?_, by simp⟩
      simp [OBST.weight]
  | succ l =>
      have hw : nextWeight p q rows i l = OBST.weight p q i (i+(l+1)) := by
        have h := (hprev l (by omega) i (by omega)).2.1
        simp only [nextWeight, h]
        simpa [Nat.add_assoc] using (weight_succ p q i l).symm
      have hc := candidate_correct p q N (l+1) i rows hprev hi
      let f := candidate rows i (l+1) (nextWeight p q rows i l)
      have hf (r : Nat) (hr : i < r) (hr' : r ≤ i+(l+1)) :
          f r = bottomUpOBST p q i (r-1) + bottomUpOBST p q r (i+(l+1)) +
            OBST.weight p q i (i+(l+1)) := by
        dsimp only [f]
        rw [hw]
        exact hc r hr hr'
      have hbest : (minimum f (i+1) l).value = bottomUpOBST p q i (i+(l+1)) := by
        apply minimum_value_eq
        · intro r hr hr'
          rw [hf r (by omega) (by omega), (bottomUpOBST_obstRecurrence p q).2 (by omega)]
          exact Finset.inf'_le _ (by simp [Finset.mem_Icc]; omega)
        · obtain ⟨hr, he⟩ := (obstRoot_optimal p q).2 (show i < i+(l+1) by omega)
          have hb := Finset.mem_Icc.mp hr
          refine ⟨obstRoot p q i (i+(l+1)), hb.1, by omega, ?_⟩
          exact (hf _ (by omega) hb.2).trans he.symm
      obtain ⟨hlo, hhi, heq, _⟩ := minimum_spec f (i+1) l
      change (minimum f (i+1) l).value = _ ∧ nextWeight p q rows i l = _ ∧
        (0 < l+1 → i < (minimum f (i+1) l).index ∧
          (minimum f (i+1) l).index ≤ i+(l+1) ∧ (minimum f (i+1) l).value = _)
      refine ⟨hbest, hw, fun _ => ⟨by omega, by omega, ?_⟩⟩
      exact heq.trans (hf _ (by omega) (by omega))

Every stored cost/weight is correct, and its stored root attains the optimum.

theorem execute_get_correct (p q : Nat → Nat) (N l i : Nat)
    (hl : l ≤ N) (hi : i+l ≤ N) :
    CorrectCell p q l i (get (execute p q N).rows l i) := by
  apply buildLayers_property (fun l => N+1-l) (step p q) (CorrectCell p q)
    (fun l rows _ hp i hi => step_correct p q N l rows hp i hi) (N+1) l (by omega) i
      (by omega)

              

theorem execute_cost (p q : Nat → Nat) (N i j : Nat) (hij : i ≤ j) (hj : j ≤ N) :
    (get (execute p q N).rows (j-i) i).cost = bottomUpOBST p q i j := by
  have h := (execute_get_correct p q N (j-i) i (by omega) (by omega)).1
  simpa [Nat.add_sub_of_le hij] using h@[simp] theorem step_visits (p q : Nat → Nat) (l : Nat) (rows : Array (Array Cell)) (i : Nat) :
    (step p q l rows i).2 = l := by cases l <;> simp [step]theorem execute_cells (p q : Nat → Nat) (N : Nat) :
    (execute p q N).cellWrites = ∑ l ∈ Finset.range (N+1), (N+1-l) :=
  buildLayers_cellWrites _ _ _theorem execute_candidateVisits (p q : Nat → Nat) (N : Nat) :
    (execute p q N).candidateVisits = ∑ l ∈ Finset.range (N+1), (N+1-l)*l :=
  buildLayers_candidateVisits _ id _ (step_visits p q) _

Correctness of the finite stored table on its represented intervals.

def CorrectTable (p q : Nat → Nat) (N : Nat) (rows : Array (Array Cell)) : Prop :=
  ∀ l i, l ≤ N → i+l ≤ N → CorrectCell p q l i (get rows l i)



private theorem stored_root {p q : Nat → Nat} {N : Nat} {rows : Array (Array Cell)}
    (h : CorrectTable p q N rows) (i j : Nat) (hij : i < j) (hj : j ≤ N) :
    i < (get rows (j-i) i).root ∧ (get rows (j-i) i).root ≤ j ∧
    bottomUpOBST p q i j = bottomUpOBST p q i ((get rows (j-i) i).root-1) +
      bottomUpOBST p q (get rows (j-i) i).root j + OBST.weight p q i j := by
  have hc := h (j-i) i (by omega) (by omega)
  have hs := hc.2.2 (by omega)
  have he : i+(j-i) = j := by omega
  dsimp only [CorrectCell] at hc
  rw [he] at hc hs
  exact ⟨hs.1, hs.2.1, hc.1.symm.trans hs.2.2⟩

Reconstruct solely by reading the stored root table. Correctness proofs are erased and do not evaluate the independent optimum or its root selector.

def reconstruct (p q : Nat → Nat) (N : Nat) (rows : Array (Array Cell))
    (h : CorrectTable p q N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) : BSTPlan i j :=
  if ht : i < j then
    let r := (get rows (j-i) i).root
    have hs := stored_root h i j ht hj
    BSTPlan.node r hs.1 hs.2.1
      (reconstruct p q N rows h i (r-1) (by omega) (by omega))
      (reconstruct p q N rows h r j hs.2.1 hj)
  else
    have he : i = j := by omega
    he ▸ BSTPlan.empty i
termination_by j-i

decreasing_by
  all_goals
    have _hs := stored_root h i j ht hj
    try dsimp only [r] at *
    omega

Every node follows its stored root.


theorem reconstruct_reconstructed (p q : Nat → Nat) (N : Nat) (rows : Array (Array Cell))
    (h : CorrectTable p q N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) :
    ReconstructedBy (fun i j => (get rows (j-i) i).root)
      (reconstruct p q N rows h i j hij hj) := by
  rw [reconstruct]
  split
  next ht =>
    have hs := stored_root h i j ht hj
    exact ⟨rfl,
      reconstruct_reconstructed p q N rows h i _ (by omega) (by omega),
      reconstruct_reconstructed p q N rows h _ j hs.2.1 hj⟩
  next ht =>
    have he : i = j := by omega
    subst j
    trivial
termination_by j-i

decreasing_by all_goals omega

The reconstructed plan attains the independent expected-cost recurrence.


theorem reconstruct_cost (p q : Nat → Nat) (N : Nat) (rows : Array (Array Cell))
    (h : CorrectTable p q N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) :
    expectedCost p q (reconstruct p q N rows h i j hij hj) = bottomUpOBST p q i j := by
  rw [reconstruct]
  split
  next ht =>
    have hs := stored_root h i j ht hj
    rw [expectedCost, reconstruct_cost p q N rows h i _ (by omega) (by omega),
      reconstruct_cost p q N rows h _ j hs.2.1 hj]
    exact hs.2.2.symm
  next ht =>
    have he : i = j := by omega
    subst j
    exact ((bottomUpOBST_obstRecurrence p q).1 i).symm
termination_by j-i

decreasing_by all_goals omega

Build all three tables once, then reconstruct using that returned table.

def executePlan (p q : Nat → Nat) (N : Nat) : BSTPlan 0 N × Table Cell :=
  let table := execute p q N
  (reconstruct p q N table.rows (fun l i hl hi => execute_get_correct p q N l i hl hi)
    0 N (Nat.zero_le _) le_rfl, table)

Optimality among every typed competitor, using only natural nonnegative weights.


theorem executePlan_correct (p q : Nat → Nat) (N : Nat) (other : BSTPlan 0 N) :
    expectedCost p q (executePlan p q N).1 ≤ expectedCost p q other := by
  have he := reconstruct_cost p q N (execute p q N).rows
    (fun l i hl hi => execute_get_correct p q N l i hl hi) 0 N (Nat.zero_le _) le_rfl
  change expectedCost p q (reconstruct p q N (execute p q N).rows _ 0 N _ _) ≤ _
  rw [he]
  apply obst_opt_le_planCost (opt := bottomUpOBST p q) ?_ other
  refine ⟨fun i => ((bottomUpOBST_obstRecurrence p q).1 i).le, ?_⟩
  intro i j r hij hr
  rw [(bottomUpOBST_obstRecurrence p q).2 hij]
  exact Finset.inf'_le _ hr

Every actual interval-evaluation event is unique.

theorem execute_once (p q : Nat → Nat) (N : Nat) :
    (execute p q N).evaluatedStates.Nodup :=
  buildLayers_evaluatedStates_nodup _ _ _

The actual evaluation trace covers exactly the valid interval states.


theorem execute_state_iff (p q : Nat → Nat) (N l i : Nat) :
    (l,i) ∈ (execute p q N).evaluatedStates ↔ i+l ≤ N := by
  rw [execute, buildLayers_evaluatedStates_mem]
  omega

Quadratic storage from actual interval writes.


theorem execute_cells_le (p q : Nat → Nat) (N : Nat) :
    (execute p q N).cellWrites ≤ (N+1)^2 := by
  rw [execute_cells]
  exact interval_cells_le_square N

Cubic bound on the actual candidate-scan counter.


theorem execute_candidateVisits_le (p q : Nat → Nat) (N : Nat) :
    (execute p q N).candidateVisits ≤ (N+1)^3 := by
  rw [execute_candidateVisits]
  exact interval_visits_le_cube N

Reconstruction attains the cost stored in the same returned table.


theorem executePlan_cost (p q : Nat → Nat) (N : Nat) :
    expectedCost p q (executePlan p q N).1 =
      (get (executePlan p q N).2.rows N 0).cost := by
  dsimp only [executePlan]
  rw [reconstruct_cost]
  simpa using (execute_cost p q N 0 N (Nat.zero_le _) le_rfl).symm

Exact quadratic count of stored interval cells.


theorem execute_cells_closed (p q : Nat → Nat) (N : Nat) :
    2 * (execute p q N).cellWrites = (N+1)*(N+2) := by
  rw [execute_cells]
  exact interval_cells_closed N

Exact cubic count of executed candidates.


theorem execute_candidateVisits_closed (p q : Nat → Nat) (N : Nat) :
    6 * (execute p q N).candidateVisits = N*(N+1)*(N+2) := by
  rw [execute_candidateVisits]
  exact interval_visits_closed N

Two-sided quadratic storage bounds, including the diagonal boundary.


theorem execute_cells_bounds (p q : Nat → Nat) (N : Nat) :
    (N+1)^2 ≤ 2 * (execute p q N).cellWrites ∧
      (execute p q N).cellWrites ≤ (N+1)^2 := by
  refine ⟨?_, execute_cells_le p q N⟩
  rw [execute_cells_closed]
  nlinarith

Two-sided cubic candidate bounds.


theorem execute_candidateVisits_bounds (p q : Nat → Nat) (N : Nat) :
    N^3 ≤ 6 * (execute p q N).candidateVisits ∧
      (execute p q N).candidateVisits ≤ (N+1)^3 := by
  refine ⟨?_, execute_candidateVisits_le p q N⟩
  rw [execute_candidateVisits_closed]
  nlinarith [sq_nonneg (N : ℤ)]

end CLRS.Chapter15.OBST.Execution

CLRSLean.Chapter_15.Section_15_5_Optimal_Binary_Search_Trees

CLRS Section 15.5 - Optimal binary search trees

This section formalizes the mathematical core of optimal binary search trees. We use a zero-based internal indexing convention:

BSTPlan i j with i ≤ j represents a BST containing keys i+1, ..., j and dummy keys i, ..., j.
empty i : BSTPlan i i is the singleton dummy-only tree for dummy key i.
node r left right chooses key r (i < r ≤ j) as the root, with left subtree BSTPlan i (r-1) and right subtree BSTPlan r j.

The expected search cost is defined recursively by summing the cost of both children plus the total weight w(i,j) of the current subtree, because every search that reaches this subtree pays one extra comparison at its root.

The main results mirror the matrix-chain pattern:

obst_opt_le_planCost: every concrete BST plan has expected cost at least the value prescribed by the OBST recurrence.
obst_reconstructed_cost_eq: a plan reconstructed from a tight root table attains the recurrence value, hence is optimal.
bottomUpOBST_obstRecurrence: the recursive evaluator satisfies the CLRS recurrence; this does not establish tabulated runtime.

Status: proved for the mathematical optimal-cost layer, recursive recurrence evaluation, and optimal rooted-tree construction.

Deferred refinements:

The recurrence evaluator repeats subintervals and is not a cached table. Fourth-edition Chapter 14 supplies separate interval-array executions and stored-selector reconstruction with attached cell/candidate counters.

              namespace CLRSnamespace Chapter15namespace OBST

BST plan model and expected cost

A BST plan containing keys i+1, ..., j and dummy keys i, ..., j. empty i is the dummy-only tree for dummy key i. node r left right has key r as root, with i < r ≤ j.

inductive BSTPlan : Nat → Nat → Type where
  | empty (i : Nat) : BSTPlan i i
  | node {i j : Nat} (r : Nat) :
      i < r → r ≤ j →
      BSTPlan i (r - 1) → BSTPlan r j → BSTPlan i j

namespace BSTPlan

Every valid plan satisfies i ≤ j.

theorem start_le_end {i j : Nat} (plan : BSTPlan i j) : i ≤ j := by
  induction plan with
  | empty i => exact le_rfl
  | node r hi _ left _ ihLeft ihRight =>
      exact Nat.le_trans (Nat.le_of_lt hi) ihRight

end BSTPlan

Total weight of the subtree containing keys i+1, ..., j and dummy keys i, ..., j. This is the sum of all successful- and unsuccessful-search nonnegative integer weights in the subtree.

def weight (p q : Nat → Nat) (i j : Nat) : Nat :=
  (Finset.Icc (i + 1) j).sum p + (Finset.Icc i j).sum q

Weighted search cost under nonnegative integer success weights p and dummy-key weights q. The historical name is retained; this does not model arbitrary normalized real probabilities or prove a scaling bridge.

def expectedCost (p q : Nat → Nat) : {i j : Nat} → BSTPlan i j → Nat
  | i, _, BSTPlan.empty _ => q i
  | i, j, BSTPlan.node _ _ _ left right =>
      expectedCost p q left + expectedCost p q right + weight p q i j

Recurrence and lower-bound interface

A candidate cost table satisfies the OBST lower-bound recurrence:

singleton dummy intervals have cost at most q i;
for any admissible root r, the table entry is bounded by the sum of the two subproblems plus the subtree weight.

def OBSTLowerBound (p q : Nat → Nat) (opt : Nat → Nat → Nat) : Prop :=
  (∀ i, opt i i ≤ q i) ∧
    ∀ {i j r} (_hij : i < j) (_hr : r ∈ Finset.Icc (i + 1) j),
      opt i j ≤ opt i (r - 1) + opt r j + weight p q i j

A candidate cost table satisfies the exact OBST recurrence:

singleton dummy intervals have cost exactly q i;
for i < j, the entry is the minimum over all admissible roots.

def OBSTRecurrence (p q : Nat → Nat) (opt : Nat → Nat → Nat) : Prop :=
  (∀ i, opt i i = q i) ∧
    ∀ {i j} (hij : i < j),
      opt i j = (Finset.Icc (i + 1) j).inf'
        (show (Finset.Icc (i + 1) j).Nonempty from
          ⟨i + 1, by simp [Finset.mem_Icc]; omega⟩)
        (fun r => opt i (r - 1) + opt r j + weight p q i j)

A root table is tight for a candidate cost table when each non-singleton interval chooses an admissible root that attains the recurrence equality.

def OBSTRootOptimal (p q : Nat → Nat) (opt : Nat → Nat → Nat)
    (rootAt : Nat → Nat → Nat) : Prop :=
  (∀ i, opt i i = q i) ∧
    ∀ {i j} (_hij : i < j),
      rootAt i j ∈ Finset.Icc (i + 1) j ∧
        opt i j = opt i (rootAt i j - 1) + opt (rootAt i j) j + weight p q i j

A concrete BST plan is reconstructed from a root table when every internal node uses the root index prescribed for its interval.

def ReconstructedBy (rootAt : Nat → Nat → Nat) : {i j : Nat} → BSTPlan i j → Prop
  | _, _, BSTPlan.empty _ => True
  | i, j, BSTPlan.node r _ _ left right =>
      r = rootAt i j ∧ ReconstructedBy rootAt left ∧ ReconstructedBy rootAt right

Optimality theorems

Every concrete plan costs at least the recurrence lower bound.

theorem obst_opt_le_planCost {p q : Nat → Nat} {opt : Nat → Nat → Nat}
    (hopt : OBSTLowerBound p q opt) :
    ∀ {i j : Nat} (plan : BSTPlan i j), opt i j ≤ expectedCost p q plan := by
  intro i j plan
  induction plan with
  | empty i =>
      simpa [expectedCost] using hopt.1 i
  | node r hi hj left right ihLeft ihRight =>
      have h := hopt.2 (Nat.lt_of_lt_of_le hi hj)
        (Finset.mem_Icc.mpr ⟨Nat.succ_le_of_lt hi, hj⟩)
      simp [expectedCost]
      linarith

A plan reconstructed from a tight root table attains the optimum.


theorem obst_reconstructed_cost_eq {p q : Nat → Nat} {opt : Nat → Nat → Nat}
    {rootAt : Nat → Nat → Nat} (hroot : OBSTRootOptimal p q opt rootAt) :
    ∀ {i j : Nat} (plan : BSTPlan i j),
      ReconstructedBy rootAt plan → expectedCost p q plan = opt i j := by
  intro i j plan hrec
  induction plan with
  | empty i =>
      simpa [expectedCost] using (hroot.1 i).symm
  | node r hi hj left right ihLeft ihRight =>
      rcases hrec with ⟨hr, hrecLeft, hrecRight⟩
      have h := (hroot.2 (Nat.lt_of_lt_of_le hi hj)).2
      simp [expectedCost, h] at ⊢
      rw [ihLeft hrecLeft, ihRight hrecRight]
      rw [hr]

A reconstructed plan is optimal among all plans for the same interval.


theorem obst_reconstructed_optimal {p q : Nat → Nat} {opt : Nat → Nat → Nat}
    {rootAt : Nat → Nat → Nat} (hrec : OBSTRecurrence p q opt)
    (hroot : OBSTRootOptimal p q opt rootAt) {i j : Nat} {plan : BSTPlan i j}
    (hplan : ReconstructedBy rootAt plan) :
    ∀ other : BSTPlan i j,
      expectedCost p q plan ≤ expectedCost p q other := by
  intro other
  have hlb : OBSTLowerBound p q opt := by
    constructor
    · intro i; rw [hrec.1 i]
    · intro i j r hij hr
      rw [(hrec.2 hij)]
      exact Finset.inf'_le _ hr
  have heq := obst_reconstructed_cost_eq hroot plan hplan
  rw [heq]
  exact obst_opt_le_planCost hlb other

Recursive recurrence evaluator

The canonical executable OBST value function obtained by recursively evaluating the CLRS recurrence. The recursion is over the interval length j - i.

def bottomUpOBST (p q : Nat → Nat) : Nat → Nat → Nat
  | i, j =>
      if h : i < j then
        (Finset.Icc (i + 1) j).attach.inf'
          (Finset.attach_nonempty_iff.mpr
            (by use i + 1; simp [Finset.mem_Icc]; exact h))
          (fun r =>
            bottomUpOBST p q i (r.1 - 1) +
              bottomUpOBST p q r.1 j +
              weight p q i j)
      else
        q i
termination_by i j => j - i
decreasing_by
  all_goals
    have hr := Finset.mem_Icc.mp r.2
    omega

The recursive evaluator satisfies the OBST recurrence.


theorem bottomUpOBST_obstRecurrence (p q : Nat → Nat) :
    OBSTRecurrence p q (bottomUpOBST p q) := by
  constructor
  · intro i
    rw [bottomUpOBST]
    simp
  · intro i j hij
    have H : (Finset.Icc (i + 1) j).Nonempty := by
      use i + 1
      simp [Finset.mem_Icc]
      exact hij
    rw [bottomUpOBST]
    simp [hij]
    apply le_antisymm
    · -- The attached inf is a lower bound for every value taken on `Finset.Icc`.
      apply Finset.le_inf' H
        (fun x => bottomUpOBST p q i (x - 1) + bottomUpOBST p q x j + weight p q i j)
      intro x hx
      exact Finset.inf'_le _ (Finset.mem_attach _ ⟨x, hx⟩)
    · -- The plain inf is a lower bound for every value taken on `Finset.attach`.
      apply Finset.le_inf' (Finset.attach_nonempty_iff.mpr H)
        (fun r : {r // r ∈ Finset.Icc (i + 1) j} =>
          bottomUpOBST p q i (r.1 - 1) + bottomUpOBST p q r.1 j + weight p q i j)
      intro r hr
      exact Finset.inf'_le _ r.2

Optimal root existence and final correctness

open Finset



private lemma exists_inf'_eq (s : Finset ℕ) (h : s.Nonempty) (f : ℕ → ℕ) :
    ∃ a ∈ s, f a = s.inf' h f := by
  induction' s using Finset.induction with a s has ih
  · exact absurd h (by simp)
  · by_cases hs : s.Nonempty
    · rcases ih hs with ⟨b, hb, hb_eq⟩
      rw [Finset.inf'_insert hs f]
      by_cases hle : f a ≤ s.inf' hs f
      · rw [min_eq_left hle]
        exact ⟨a, mem_insert_self a s, rfl⟩
      · rw [min_eq_right (by omega : s.inf' hs f ≤ f a)]
        rw [← hb_eq]
        exact ⟨b, mem_insert_of_mem hb, rfl⟩
    · have hsingleton : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs
      subst hsingleton
      simp

There exists a tight root table for bottomUpOBST. The proof uses Classical.choice together with exists_inf'_eq.


theorem exists_obstRootOptimal (p q : Nat → Nat) :
    ∃ rootAt : Nat → Nat → Nat,
      OBSTRootOptimal p q (bottomUpOBST p q) rootAt := by
  have h_rec : OBSTRecurrence p q (bottomUpOBST p q) :=
    bottomUpOBST_obstRecurrence p q
  have h_diag : ∀ i, bottomUpOBST p q i i = q i := h_rec.1
  have h_exists_root (i j : Nat) (hij : i < j) : ∃ r, r ∈ Finset.Icc (i + 1) j ∧
      bottomUpOBST p q i j =
        bottomUpOBST p q i (r - 1) + bottomUpOBST p q r j + weight p q i j := by
    rw [h_rec.2 hij]
    let s := Finset.Icc (i + 1) j
    have h_nonempty : s.Nonempty := by
      use i + 1; simp [s, Finset.mem_Icc]; omega
    let f (r : ℕ) := bottomUpOBST p q i (r - 1) + bottomUpOBST p q r j + weight p q i j
    rcases exists_inf'_eq s h_nonempty f with ⟨r, hr, heq⟩
    exact ⟨r, hr, heq.symm⟩
  -- Build rootAt pointwise using Exists.choose
  let rootAt (i j : Nat) : Nat :=
    if h : i < j then Exists.choose (h_exists_root i j h) else i
  refine ⟨rootAt, h_diag, ?_⟩
  intro i j hij
  have h_rootAt : rootAt i j = Exists.choose (h_exists_root i j hij) := by
    unfold rootAt; simp [hij]
  rw [h_rootAt]
  exact Exists.choose_spec (h_exists_root i j hij)

Construct a BSTPlan recursively following a tight root table.


private def obstBuildPlan (rootAt : Nat → Nat → Nat)
    (hroot : OBSTRootOptimal p q (bottomUpOBST p q) rootAt) (i j : Nat) (hij : i ≤ j) :
    BSTPlan i j :=
  if h : i < j then
    have hmem := Finset.mem_Icc.mp (hroot.2 h).1
    have h_lt_r : i < rootAt i j := by omega
    have h_left_bound : i ≤ rootAt i j - 1 := by omega
    BSTPlan.node (rootAt i j) h_lt_r hmem.2
      (obstBuildPlan rootAt hroot i (rootAt i j - 1) h_left_bound)
      (obstBuildPlan rootAt hroot (rootAt i j) j hmem.2)
  else
    have heq : i = j := by omega
    heq ▸ BSTPlan.empty j
termination_by j - i
decreasing_by
  · -- first recursive call: (rootAt i j - 1) - i < j - i
    have Variable name `hhi` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hhi : rootAt i j ≤ j := (Finset.mem_Icc.mp (hroot.2 h).1).2
    omega
  · -- second recursive call: j - rootAt i j < j - i
    have Variable name `hlo` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hlo : i + 1 ≤ rootAt i j := (Finset.mem_Icc.mp (hroot.2 h).1).1
    omega

The plan built by obstBuildPlan follows the root table.


private theorem obstBuildPlan_reconstructed (rootAt : Nat → Nat → Nat)
    (hroot : OBSTRootOptimal p q (bottomUpOBST p q) rootAt) (i j : Nat) (hij : i ≤ j) :
    ReconstructedBy rootAt (obstBuildPlan rootAt hroot i j hij) := by
  unfold obstBuildPlan
  split
  · next h =>
    have hmem := Finset.mem_Icc.mp (hroot.2 h).1
    have h_left_bound : i ≤ rootAt i j - 1 := by omega
    have h_lt : (rootAt i j - 1) - i < j - i := by
      have hhi : rootAt i j ≤ j := hmem.2
      omega
    have h_rt : j - (rootAt i j) < j - i := by
      have hlo : i + 1 ≤ rootAt i j := hmem.1
      omega
    simp
    exact ⟨rfl,
      obstBuildPlan_reconstructed rootAt hroot i (rootAt i j - 1) h_left_bound,
      obstBuildPlan_reconstructed rootAt hroot (rootAt i j) j hmem.2⟩
  · next h =>
    have heq : i = j := by omega
    subst heq
    simp [ReconstructedBy]
termination_by j - i
decreasing_by
  exact h_lt
  exact h_rt

Theorem (Optimal BST). For any interval [i,j] with i ≤ j, there exists a binary search tree plan that minimizes expected search cost. This corresponds to CLRS Theorem 15.7.

theorem obst_correct (p q : Nat → Nat) (i j : Nat) (hij : i ≤ j) :
    ∃ plan : BSTPlan i j,
      ∀ other : BSTPlan i j,
        expectedCost p q plan ≤ expectedCost p q other := by
  rcases exists_obstRootOptimal p q with ⟨rootAt, hroot⟩
  have hrec : OBSTRecurrence p q (bottomUpOBST p q) :=
    bottomUpOBST_obstRecurrence p q
  let plan := obstBuildPlan rootAt hroot i j hij
  refine ⟨plan, λ other => ?_⟩
  have hplan : ReconstructedBy rootAt plan :=
    obstBuildPlan_reconstructed rootAt hroot i j hij
  exact obst_reconstructed_optimal hrec hroot hplan other