Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 14. Dynamic Programming
Browse chapters

Chapter 14 — Dynamic Programming

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports
import CLRSLean.FourthEdition.Chapter_14.Section_14_1_Rod_Cutting.Execution

14.1. Rod Cutting

This section completes the fourth-edition §14.1 algorithm boundary for rod cutting on top of the legacy recurrence and bottom-up table (CLRSLean.Chapter_15.Section_15_1_Rod_Cutting). It adds the optimal-cut reconstruction of EXTENDED-BOTTOM-UP-CUT-ROD, the top-down MEMOIZED-CUT-ROD cache-threading algorithm, and the explicit O(n²) step count of BOTTOM-UP-CUT-ROD.

Main results:

  • Definition rodCutFirstCut and theorems rodCutFirstCut_mem, rodCutFirstCut_le, rodCutFirstCut_value: the optimal first cut s of EXTENDED-BOTTOM-UP-CUT-ROD is a valid cut in 1 .. n and attains the recurrence maximum.

  • Definition rodCutPlan and theorems rodCutPlan_correct, rodCutPlan_optimal: PRINT-CUT-ROD-SOLUTION rebuilds an optimal cutting plan of length n.

  • CLRS.­Chapter15.­RodExecution.­execute fills an array using a single stored prefix per outer iteration. rodExecution_candidates_eq connects its candidate counter to rodCutStepCount; rodExecution_candidates_le_quadratic bounds those executed candidate visits. Price lookup, array access, and arithmetic are primitive events; their internals are excluded.

  • Definition memoizedRodCut and theorems memoizedRodCut_value, memoizedRodCut_correct: the top-down MEMOIZED-CUT-ROD cache-threading algorithm returns the optimal revenue and keeps its cache consistent.

Status: proved for cut reconstruction, top-down memoization, and the O(n²) step-count cost analysis. The mutable-array bottom-up refinement and the Bellman recurrence remain in the legacy source.

Notation conventions used in this section:

  • price : the price table price n = revenue of an uncut piece of length n

  • n : the rod length

namespace CLRSnamespace Chapter15

Optimal-cut reconstruction (CLRS §14.1 EXTENDED-BOTTOM-UP-CUT-ROD)

The candidate first cuts for a rod of length n, listed in increasing order as [1, 2, ..., n].

def rodCutCandidates (n : Nat) : List Nat := (List.range n).map (fun i => i + 1)

Membership in the candidate list is exactly a valid first cut in 1 .. n.

theorem mem_rodCutCandidates (n cut : Nat) : cut ∈ rodCutCandidates n ↔ cut ∈ Finset.Icc 1 n := by simp [rodCutCandidates, List.mem_map, List.mem_range, Finset.mem_Icc] constructor · rintro ⟨i, hi, rfl⟩ omega · intro h refine ⟨cut - 1, ?_, ?_⟩ · omega · omega

Pick the first cut with the larger first-cut revenue, breaking ties toward the smaller cut.

def betterRodCut (price : Nat → Nat) (n : Nat) (a b : Nat) : Nat := if FirstCutValue price (bottomUpRodRevenue price) n a < FirstCutValue price (bottomUpRodRevenue price) n b then b else a

The best first cut among a list of candidate cuts, or none for an empty list.

def bestRodCutOf (price : Nat → Nat) (n : Nat) : List Nat → Option Nat | [] => none | cut :: rest => match bestRodCutOf price n rest with | none => some cut | some best => some (betterRodCut price n cut best)

The list-based selector returns an element of the candidate list whose first-cut revenue is at least every candidate's.

theorem bestRodCutOf_correct (price : Nat → Nat) (n : Nat) {best : Nat} {cuts : List Nat} (hbest : bestRodCutOf price n cuts = some best) : best ∈ cuts ∧ ∀ cut, cut ∈ cuts → FirstCutValue price (bottomUpRodRevenue price) n cut ≤ FirstCutValue price (bottomUpRodRevenue price) n best := by induction cuts generalizing best with | nil => simp [bestRodCutOf] at hbest | cons cut rest ih => simp [bestRodCutOf] at hbest cases hrest : bestRodCutOf price n rest with | none => have hrestNil : rest = [] := by cases rest with | nil => rfl | cons restCut restTail => cases htail : bestRodCutOf price n restTail <;> simp [bestRodCutOf, htail] at hrest simp [hrest] at hbest subst best subst rest constructor · simp · intro other hother simp at hother subst other exact le_rfl | some restBest => simp [hrest] at hbest have hrestCorrect := ih hrest by_cases hlt : FirstCutValue price (bottomUpRodRevenue price) n cut < FirstCutValue price (bottomUpRodRevenue price) n restBest · simp [betterRodCut, hlt] at hbest subst best constructor · simp [hrestCorrect.1] · intro other hother simp at hother rcases hother with hsame | hinRest · subst other exact le_of_lt hlt · exact hrestCorrect.2 other hinRest · simp [betterRodCut, hlt] at hbest subst best constructor · simp · intro other hother simp at hother rcases hother with hsame | hinRest · subst other exact le_rfl · exact le_trans (hrestCorrect.2 other hinRest) (le_of_not_gt hlt)

Every nonempty candidate list has a selected best first cut.

theorem bestRodCutOf_exists_of_ne_nil (price : Nat → Nat) (n : Nat) {cuts : List Nat} (hc : cuts ≠ []) : ∃ best, bestRodCutOf price n cuts = some best := by cases cuts with | nil => exact False.elim (hc rfl) | cons cut rest => simp [bestRodCutOf] cases hrest : bestRodCutOf price n rest with | none => exact ⟨cut, rfl⟩ | some restBest => exact ⟨betterRodCut price n cut restBest, rfl⟩

The optimal first cut for a rod of length n (junk value 0 when n = 0).

def rodCutFirstCut (price : Nat → Nat) (n : Nat) : Nat := (bestRodCutOf price n (rodCutCandidates n)).getD 0

The chosen first cut is a valid first cut for a positive-length rod.

theorem rodCutFirstCut_mem (price : Nat → Nat) {n : Nat} (hn : 0 < n) : rodCutFirstCut price n ∈ rodCutCandidates n := by unfold rodCutFirstCut have hne : rodCutCandidates n ≠ [] := by cases n with | zero => omega | succ m => simp [rodCutCandidates] rcases bestRodCutOf_exists_of_ne_nil price n hne with ⟨best, hbest⟩ rw [hbest] simp exact (bestRodCutOf_correct price n hbest).1

The chosen first cut has revenue at least every candidate's.

theorem rodCutFirstCut_le (price : Nat → Nat) {n : Nat} (hn : 0 < n) (cut : Nat) (hcut : cut ∈ rodCutCandidates n) : FirstCutValue price (bottomUpRodRevenue price) n cut ≤ FirstCutValue price (bottomUpRodRevenue price) n (rodCutFirstCut price n) := by unfold rodCutFirstCut have hne : rodCutCandidates n ≠ [] := by cases n with | zero => omega | succ m => simp [rodCutCandidates] rcases bestRodCutOf_exists_of_ne_nil price n hne with ⟨best, hbest⟩ rw [hbest] simp exact (bestRodCutOf_correct price n hbest).2 cut hcut

The chosen first cut achieves the optimal revenue (CLRS §14.1: the s entry attains the maximum in the recurrence).

theorem rodCutFirstCut_value (price : Nat → Nat) {n : Nat} (hn : 0 < n) : FirstCutValue price (bottomUpRodRevenue price) n (rodCutFirstCut price n) = bottomUpRodRevenue price n := by have hs_mem : rodCutFirstCut price n ∈ Finset.Icc 1 n := (mem_rodCutCandidates n _).mp (rodCutFirstCut_mem price hn) rcases n with _ | m · omega · rw [bottomUpRodRevenue_succ price m] apply le_antisymm · exact Finset.le_sup hs_mem · refine Finset.sup_le ?_ intro cut hcut exact rodCutFirstCut_le price hn cut ((mem_rodCutCandidates (m + 1) cut).mpr hcut)

Reconstruct an optimal cutting plan for a rod of length n by repeatedly taking the optimal first cut (CLRS §14.1 PRINT-CUT-ROD-SOLUTION).

def rodCutPlan (price : Nat → Nat) : Nat → List Nat | 0 => [] | n@(_ + 1) => rodCutFirstCut price n :: rodCutPlan price (n - rodCutFirstCut price n) termination_by n => n decreasing_by simp_wf have hmem : rodCutFirstCut price n ∈ rodCutCandidates n := rodCutFirstCut_mem price (by omega) have hIcc := (mem_rodCutCandidates n (rodCutFirstCut price n)).mp hmem have hpos : 1 ≤ rodCutFirstCut price n := (Finset.mem_Icc.mp hIcc).1 omega

The reconstructed plan for a rod of length n has total length n and attains the optimal revenue.

theorem rodCutPlan_correct (price : Nat → Nat) (n : Nat) : planLength (rodCutPlan price n) = n ∧ planValue price (rodCutPlan price n) = bottomUpRodRevenue price n := by induction n using Nat.strong_induction_on with | h n ih => cases n with | zero => rw [rodCutPlan] simp [planLength, planValue] | succ m => set s : Nat := rodCutFirstCut price (m + 1) with hs_def have hs_mem : s ∈ rodCutCandidates (m + 1) := by rw [hs_def] exact rodCutFirstCut_mem price (by omega) have hs_Icc : s ∈ Finset.Icc 1 (m + 1) := (mem_rodCutCandidates (m + 1) s).mp hs_mem have hs_pos : 1 ≤ s := (Finset.mem_Icc.mp hs_Icc).1 have hs_le : s ≤ m + 1 := (Finset.mem_Icc.mp hs_Icc).2 have hs_sub : m + 1 - s < m + 1 := by omega have ih' := ih (m + 1 - s) hs_sub have hs_value : FirstCutValue price (bottomUpRodRevenue price) (m + 1) s = bottomUpRodRevenue price (m + 1) := by rw [hs_def] exact rodCutFirstCut_value price (by omega) constructor · rw [rodCutPlan] simp only [planLength, List.sum_cons] rw [← hs_def] change s + planLength (rodCutPlan price (m + 1 - s)) = m + 1 rw [ih'.1] omega · rw [rodCutPlan] simp only [planValue, List.map_cons, List.sum_cons] rw [← hs_def] change price s + planValue price (rodCutPlan price (m + 1 - s)) = bottomUpRodRevenue price (m + 1) rw [ih'.2] simpa [FirstCutValue] using hs_value

The reconstructed plan is optimal among all positive-piece plans of the same total length.

theorem rodCutPlan_optimal (price : Nat → Nat) (n : Nat) {other : List Nat} (hother_pos : PositivePieces other) (hlen : planLength other = n) : planValue price other ≤ planValue price (rodCutPlan price n) := by have hc := rodCutPlan_correct price n apply planValue_le_optimalPlanValue_of_same_length (price := price) (revenue := bottomUpRodRevenue price) (bottomUpRodRevenue_rodCutRecurrence price) hother_pos · rw [hc.1] exact hlen · rw [hc.2, hc.1]

Cost analysis: BOTTOM-UP-CUT-ROD runs in O(n^2)

The total number of first-cut candidates examined by BOTTOM-UP-CUT-ROD for a rod of length n: rod length j scans all j possible first cuts, so the total is ∑_{j = 1}^{n} j = n (n + 1) / 2.

def rodCutStepCount (n : Nat) : Nat := (Finset.range (n + 1)).sum (fun j => j)

Closed form: the bottom-up step count is n (n + 1) / 2.

theorem rodCutStepCount_eq (n : Nat) : rodCutStepCount n = n * (n + 1) / 2 := by unfold rodCutStepCount have h : (Finset.range (n + 1)).sum (fun j => j) * 2 = (n + 1) * n := by simpa using (Finset.sum_range_id_mul_two (n + 1)) rw [Nat.mul_comm n (n + 1)] rw [← h] omega

The bottom-up rod-cutting algorithm performs O(n²) work: its step count is at most n².

theorem rodCutStepCount_le_quadratic (n : Nat) : rodCutStepCount n ≤ n ^ 2 := by rw [rodCutStepCount_eq] by_cases hn : n = 0 · simp [hn] · have hpos : 1 ≤ n := Nat.succ_le_of_lt (Nat.pos_of_ne_zero hn) have hprod : n * (n + 1) ≤ 2 * n ^ 2 := by nlinarith have hdiv : n * (n + 1) / 2 ≤ (2 * n ^ 2) / 2 := by gcongr have htwo : (2 * n ^ 2) / 2 = n ^ 2 := by omega rwa [htwo] at hdiv

The candidate first cuts [1, ..., n] as a list of subtypes carrying the bounds 1 ≤ c and c ≤ n, used to thread the memoized cache through the scan.

def rodCutCandidatesBounded (n : Nat) : List {c : Nat // 1 ≤ c ∧ c ≤ n} := (List.range n).attach.map (fun i => ⟨i.1 + 1, Nat.succ_pos i.1, by have hi : i.1 < n := List.mem_range.mp i.2 omega⟩)

A rod of length zero has no first-cut candidates.

@[simp] theorem rodCutCandidatesBounded_zero : rodCutCandidatesBounded 0 = [] := by simp [rodCutCandidatesBounded]

Projecting the bounded candidates recovers the plain candidate list.

theorem rodCutCandidatesBounded_map_val (n : Nat) : (rodCutCandidatesBounded n).map (fun cut => cut.1) = rodCutCandidates n := by simp [rodCutCandidatesBounded, rodCutCandidates]

A memoized cache is consistent when every stored revenue is the true optimal revenue for its rod length.

def ConsistentCache (price : Nat → Nat) (cache : Nat → Option Nat) : Prop := ∀ k v, cache k = some v → v = bottomUpRodRevenue price k

A single memoized step, given the sub-computation result.

def memoizedRodCutStep (price : Nat → Nat) (cur : Nat) (subval : Nat) (cacheSub : Nat → Option Nat) (cut : Nat) : Nat × (Nat → Option Nat) := (max cur (price cut + subval), cacheSub)

Top-down memoized rod cutting (CLRS MEMOIZED-CUT-ROD). memoizedRodCut price n cache returns the optimal revenue for a rod of length n together with a cache extended with the revenue of n and every subproblem it needed. Entries already present in cache are reused without recomputation.

def memoizedRodCut (price : Nat → Nat) : Nat → (Nat → Option Nat) → Nat × (Nat → Option Nat) | n, cache => match cache n with | some v => (v, cache) | none => let res := (rodCutCandidatesBounded n).foldl (fun acc cut => let (cur, cacheAcc) := acc let (subval, cacheSub) := memoizedRodCut price (n - cut.1) cacheAcc memoizedRodCutStep price cur subval cacheSub cut.1) (0, cache) (res.1, Function.update res.2 n (some res.1)) termination_by n _ => n decreasing_by simp_wf omega

The memoized cache-threading fold over the candidate cuts of rod length n. Exposed so its correctness can be stated and proved by induction.

def memoizedRodCutFold (price : Nat → Nat) (n : Nat) (initVal : Nat) (cache : Nat → Option Nat) (cuts : List {c : Nat // 1 ≤ c ∧ c ≤ n}) : Nat × (Nat → Option Nat) := cuts.foldl (fun acc cut => let (cur, cacheAcc) := acc let (subval, cacheSub) := memoizedRodCut price (n - cut.1) cacheAcc memoizedRodCutStep price cur subval cacheSub cut.1) (initVal, cache)

List max helpers

Folding max is monotone in the accumulator.

theorem foldl_max_mono_init {l : List Nat} {a b : Nat} (h : a ≤ b) : l.foldl max a ≤ l.foldl max b := by induction l generalizing a b with | nil => simpa using h | cons c as ih => simp only [List.foldl] exact ih (max_le_max_right c h)

Folding max with an upper-bound accumulator keeps the result below the bound provided every element is below it.

theorem foldl_max_le_general {l : List Nat} {b init : Nat} (hb : init ≤ b) (h : ∀ x ∈ l, x ≤ b) : l.foldl max init ≤ b := by induction l generalizing init with | nil => simpa using hb | cons a as ih => simp only [List.foldl] exact ih (max_le hb (h a (by simp))) (by intro x hx exact h x (by simp [hx]))

Folding max from zero is bounded by any upper bound of the elements.

theorem foldl_max_le {l : List Nat} {b : Nat} (h : ∀ x ∈ l, x ≤ b) : l.foldl max 0 ≤ b := foldl_max_le_general (b := b) (init := 0) (by omega) h

Folding max from x stays above x.

theorem foldl_max_ge_init (l : List Nat) (x : Nat) : x ≤ l.foldl max x := by induction l with | nil => simp | cons a as ih => simp only [List.foldl] exact le_trans ih (foldl_max_mono_init (l := as) (le_max_left x a))

Any element of a list is below the fold-max value.

theorem foldl_max_mem {l : List Nat} {x : Nat} (hx : x ∈ l) : x ≤ l.foldl max 0 := by induction l with | nil => simp at hx | cons a as ih => simp only [List.foldl] at hx ⊢ rcases List.mem_cons.mp hx with hxa | has · subst x have h0a : max 0 a = a := by simp rw [h0a] exact foldl_max_ge_init as a · exact le_trans (ih has) (foldl_max_mono_init (l := as) (le_max_left 0 a))

The maximum over the first-cut candidates for rod length n is the optimal revenue (this is exactly the CLRS first-cut recurrence).

theorem candidatesMax_eq_rev (price : Nat → Nat) (n : Nat) : ((rodCutCandidatesBounded n).map (fun cut => FirstCutValue price (bottomUpRodRevenue price) n cut.1)).foldl max 0 = bottomUpRodRevenue price n := by apply le_antisymm · refine foldl_max_le ?_ intro v hv rcases List.mem_map.mp hv with ⟨cut, hcut, rfl⟩ exact firstCutValue_le_of_rodCutRecurrence (bottomUpRodRevenue_rodCutRecurrence price) (Finset.mem_Icc.mpr cut.2) · by_cases hn : n = 0 · simp [hn, bottomUpRodRevenue_zero] · have hpos : 0 < n := Nat.pos_of_ne_zero hn have hs_value : FirstCutValue price (bottomUpRodRevenue price) n (rodCutFirstCut price n) = bottomUpRodRevenue price n := rodCutFirstCut_value price hpos rw [← hs_value] apply foldl_max_mem have hproj : (rodCutCandidatesBounded n).map (fun cut => cut.1) = rodCutCandidates n := rodCutCandidatesBounded_map_val n have hrc : rodCutFirstCut price n ∈ (rodCutCandidatesBounded n).map (fun cut => cut.1) := by rw [hproj] exact rodCutFirstCut_mem price hpos rcases List.mem_map.mp hrc with ⟨cut, hcut, hval⟩ apply List.mem_map.mpr exact ⟨cut, hcut, by rw [← hval]⟩

Memoization correctness

The memoized fold accumulates the best first-cut value and threads a consistent cache.

theorem memoizedRodCut_fold_correct (price : Nat → Nat) (n : Nat) (cuts : List {c : Nat // 1 ≤ c ∧ c ≤ n}) (initVal : Nat) (cache : Nat → Option Nat) (hcons : ConsistentCache price cache) (hrec : ∀ cut ∈ cuts, ∀ c', ConsistentCache price c' → (memoizedRodCut price (n - cut.1) c').1 = bottomUpRodRevenue price (n - cut.1) ∧ ConsistentCache price (memoizedRodCut price (n - cut.1) c').2) : (memoizedRodCutFold price n initVal cache cuts).1 = (cuts.map (fun cut => price cut.1 + bottomUpRodRevenue price (n - cut.1))).foldl max initVal ∧ ConsistentCache price (memoizedRodCutFold price n initVal cache cuts).2 := by unfold memoizedRodCutFold induction cuts generalizing initVal cache with | nil => constructor · simp · simpa using hcons | cons head rest ih => have hval_head : (memoizedRodCut price (n - head.1) cache).1 = bottomUpRodRevenue price (n - head.1) := (hrec head (by simp) cache hcons).1 have hcons_head : ConsistentCache price (memoizedRodCut price (n - head.1) cache).2 := (hrec head (by simp) cache hcons).2 let s : Nat × (Nat → Option Nat) := memoizedRodCutStep price initVal (memoizedRodCut price (n - head.1) cache).1 (memoizedRodCut price (n - head.1) cache).2 head.1 have hcons_s : ConsistentCache price s.2 := by simpa [s, memoizedRodCutStep] using hcons_head have ih' := ih s.1 s.2 hcons_s (fun cut' hcut' c'' hc'' => hrec cut' (List.mem_cons.mpr (Or.inr hcut')) c'' hc'') simp only [List.foldl] constructor · rw [ih'.1] have hs1 : s.1 = max initVal (price head.1 + bottomUpRodRevenue price (n - head.1)) := by simp [s, memoizedRodCutStep, hval_head] rw [hs1] simp only [List.map, List.foldl] · exact ih'.2

When the cache misses length n, the uncached computation reduces to the cache-threading fold: its revenue component is the fold's first component.

theorem memoizedRodCut_none_fst {price : Nat → Nat} {n : Nat} {cache : Nat → Option Nat} (hc : cache n = none) : (memoizedRodCut price n cache).1 = (memoizedRodCutFold price n 0 cache (rodCutCandidatesBounded n)).1 := by rw [memoizedRodCut, hc] rfl

When the cache misses length n, the uncached computation reduces to the cache-threading fold: its cache is the fold's cache with the entry at n stored.

theorem memoizedRodCut_none_snd {price : Nat → Nat} {n : Nat} {cache : Nat → Option Nat} (hc : cache n = none) : (memoizedRodCut price n cache).2 = Function.update (memoizedRodCutFold price n 0 cache (rodCutCandidatesBounded n)).2 n (some (memoizedRodCutFold price n 0 cache (rodCutCandidatesBounded n)).1) := by rw [memoizedRodCut, hc] rfl

Memoized top-down rod cutting is correct: it returns the optimal revenue and its output cache remains consistent.

theorem memoizedRodCut_correct (price : Nat → Nat) (n : Nat) (cache : Nat → Option Nat) (hcons : ConsistentCache price cache) : (memoizedRodCut price n cache).1 = bottomUpRodRevenue price n ∧ ConsistentCache price (memoizedRodCut price n cache).2 := by revert hcons cache induction n using Nat.strong_induction_on with | h n ih => intro cache hcons by_cases hc : cache n = none · rcases n with _ | m · -- n = 0, uncached constructor · rw [memoizedRodCut_none_fst hc] simp [memoizedRodCutFold] · rw [memoizedRodCut_none_snd hc] intro k v hkv by_cases hk : k = 0 · subst k have hkv0 : 0 = v := by simpa [Function.update, memoizedRodCutFold] using hkv rw [← hkv0] simp · simp [Function.update, hk] at hkv exact hcons k v hkv · -- n = m + 1, uncached have hrec : ∀ cut ∈ rodCutCandidatesBounded (m + 1), ∀ c', ConsistentCache price c' → (memoizedRodCut price (m + 1 - cut.1) c').1 = bottomUpRodRevenue price (m + 1 - cut.1) ∧ ConsistentCache price (memoizedRodCut price (m + 1 - cut.1) c').2 := by intro cut hcut c' hc' have hlt : m + 1 - cut.1 < m + 1 := by have h1 : 1 ≤ cut.1 := cut.2.1 omega exact ih (m + 1 - cut.1) hlt c' hc' have hfold := memoizedRodCut_fold_correct price (m + 1) (rodCutCandidatesBounded (m + 1)) 0 cache hcons hrec constructor · rw [memoizedRodCut_none_fst hc, hfold.1] exact candidatesMax_eq_rev price (m + 1) · rw [memoizedRodCut_none_snd hc] intro k v hkv by_cases hk : k = m + 1 · subst k simp [Function.update] at hkv rw [← hkv] rw [hfold.1] exact candidatesMax_eq_rev price (m + 1) · simp [Function.update, hk] at hkv exact hfold.2 k v hkv · -- cached cases hcv : cache n with | none => exact False.elim (hc hcv) | some v => have hv' : v = bottomUpRodRevenue price n := hcons n v hcv constructor · rw [memoizedRodCut, hcv] simp exact hv' · rw [memoizedRodCut, hcv] simp exact hcons

Memoized top-down rod cutting returns the optimal revenue.

theorem memoizedRodCut_value (price : Nat → Nat) (n : Nat) (cache : Nat → Option Nat) (hcons : ConsistentCache price cache) : (memoizedRodCut price n cache).1 = bottomUpRodRevenue price n := (memoizedRodCut_correct price n cache hcons).1

The bottom-up execution realizes the previously defined triangular budget.

theorem rodExecution_candidates_eq (price : Nat → Nat) (n : Nat) : (RodExecution.execute price n).candidates = rodCutStepCount n := RodExecution.execute_candidates price n

Quadratic bound on actual candidate visits, independently of price values.

theorem rodExecution_candidates_le_quadratic (price : Nat → Nat) (n : Nat) : (RodExecution.execute price n).candidates ≤ n ^ 2 := by rw [rodExecution_candidates_eq] exact rodCutStepCount_le_quadratic n
end Chapter15end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_14.Section_14_1_Rod_Cutting.Execution

Counted bottom-up rod cutting

The outer loop computes its preceding array once. The inner loop reads that stored array once per candidate, retaining its running maximum. Counters record candidate evaluations and appended table entries in that same execution. Array access, price lookup, and natural-number operations are primitive events; their implementation internals and persistent-array copying are not counted.

namespace CLRS.Chapter15.RodExecutionstructure Scan where value : Nat candidates : Nat deriving Repr

Scan cuts 1..k using an already computed revenue array.

def scan (price : Nat → Nat) (previous : Array Nat) (n : Nat) : Nat → Scan | 0 => ⟨0, 0⟩ | k + 1 => let rest := scan price previous n k let candidate := price (k + 1) + arrGet previous (n - (k + 1)) ⟨max rest.value candidate, rest.candidates + 1⟩
theorem scan_candidates (price : Nat → Nat) (previous : Array Nat) (n k : Nat) : (scan price previous n k).candidates = k := by induction k with | zero => rfl | succ k ih => simp [scan, ih] theorem scan_value (price : Nat → Nat) (previous : Array Nat) (n k : Nat) : (scan price previous n k).value = (Finset.Icc 1 k).sup (fun i => price i + arrGet previous (n - i)) := by induction k with | zero => simp [scan] | succ k ih => have hs : Finset.Icc 1 (k + 1) = insert (k + 1) (Finset.Icc 1 k) := by ext i simp only [Finset.mem_Icc, Finset.mem_insert] omega simp only [scan, ih, hs, Finset.sup_insert] exact max_comm _ _structure Run where array : Array Nat candidates : Nat writes : Nat deriving Repr

Append each new optimum once, using only the previously stored prefix.

def execute (price : Nat → Nat) : Nat → Run | 0 => ⟨#[0], 0, 1⟩ | j + 1 => let previous := execute price j let row := scan price previous.array (j + 1) (j + 1) ⟨previous.array.push row.value, previous.candidates + row.candidates, previous.writes + 1⟩

The actual stored array refines the previously proved revenue table.

theorem execute_array (price : Nat → Nat) (n : Nat) : (execute price n).array = rodRevenueArrayAux price n := by induction n with | zero => rfl | succ n ih => simp only [execute, ih, scan_value, rodRevenueArrayAux]
theorem execute_entry (price : Nat → Nat) (n k : Nat) (hk : k ≤ n) : arrGet (execute price n).array k = bottomUpRodRevenue price k := by rw [execute_array] exact arrGet_rodRevenueArrayAux price n k hk

Exact candidate visits obtained by adding counters of the executed scans.

theorem execute_candidates (price : Nat → Nat) (n : Nat) : (execute price n).candidates = (Finset.range (n + 1)).sum (fun j => j) := by induction n with | zero => simp [execute] | succ n ih => simp only [execute, ih, scan_candidates, Finset.sum_range_succ]

Includes the boundary entry at length zero.

theorem execute_writes (price : Nat → Nat) (n : Nat) : (execute price n).writes = n + 1 := by induction n with | zero => rfl | succ n ih => simp [execute, ih]
theorem execute_size (price : Nat → Nat) (n : Nat) : (execute price n).array.size = n + 1 := by rw [execute_array, rodRevenueArrayAux_size]end CLRS.Chapter15.RodExecution

CLRSLean.Chapter_15.Section_15_1_Rod_Cutting

CLRS Section 15.1 - Rod cutting

This section formalizes the mathematical core of the rod-cutting dynamic program. Instead of committing immediately to one array implementation, it defines the Bellman first-cut recurrence as a specification for a revenue function. The main theorem proves that any revenue function satisfying that recurrence upper-bounds the value of every concrete cutting plan. Consequently, any plan whose value attains the recurrence value is optimal among plans of the same total length.

Main results:

  • Theorem firstCutValue_le_of_rodCutRecurrence: every admissible first cut is bounded by the recurrence value.

  • Theorem rodRevenue_le_of_firstCutValue_bounds: the recurrence value is the least upper bound induced by first-cut candidates.

  • Theorem bottomUpRodRevenue_rodCutRecurrence: the executable recurrence-valued rod-cutting function satisfies the CLRS Bellman recurrence.

  • Theorem planValue_le_table_of_rodCutTableRecurrence: any finite table filled by the bottom-up recurrence is an upper bound for every positive-piece cutting plan within its filled prefix.

  • Theorem planValue_le_revenue_of_rodCutRecurrence: every positive-piece cutting plan is bounded by the recurrence value of its total length.

  • Theorem planValue_le_optimalPlanValue_of_same_length: a plan attaining the recurrence value is optimal among plans of the same length.

  • Definition rodRevenueArray: the CLRS BOTTOM-UP-CUT-ROD table built as a mutable Array Nat, whose entry k is filled from the earlier stored entries exactly as the imperative algorithm fills r[0 .. n].

  • Theorem rodRevenueArray_correct: the mutable-array bottom-up table refines the pure recurrence value bottomUpRodRevenue at every filled index.

  • Theorem rodRevenueArray_rodCutTableRecurrence: reading the mutable-array table is a correct finite bottom-up table in the sense of RodCutTableRecurrence.

  • Theorem planValue_le_rodRevenueArray: every positive-piece cutting plan is bounded by the value the mutable-array table stores at its total length.

Status: proved for the mathematical cut-optimality layer and the mutable-array bottom-up implementation refinement.

Deferred refinements:

  • A top-down memoized-cache refinement and explicit RAM cost semantics remain future implementation-level targets. The sibling dynamic-programming sections (matrix chain, LCS, optimal BST) follow the same mutable-array bottom-up pattern established here.

namespace CLRSnamespace Chapter15
Rod-cutting model

The total length of a concrete cutting plan.

def planLength (pieces : List Nat) : Nat := pieces.sum

The value of a cutting plan under the given price table.

def planValue (price : Nat → Nat) (pieces : List Nat) : Nat := (pieces.map price).sum

Every piece in the cutting plan has positive length.

def PositivePieces (pieces : List Nat) : Prop := ∀ piece, piece ∈ pieces → 0 < piece

The value obtained by making cut the first cut of a rod of length n.

def FirstCutValue (price revenue : Nat → Nat) (n cut : Nat) : Nat := price cut + revenue (n - cut)

The CLRS rod-cutting recurrence: length zero has value zero, and every positive length is the maximum over all possible first cuts.

def RodCutRecurrence (price revenue : Nat → Nat) : Prop := revenue 0 = 0 ∧ ∀ n, revenue (n + 1) = (Finset.Icc 1 (n + 1)).sup (fun cut => FirstCutValue price revenue (n + 1) cut)
Bottom-up table and executable recurrence

A finite bottom-up rod-cutting table is correct through limit when entry zero is zero and every positive entry up to limit is filled by the CLRS first-cut recurrence using earlier table entries.

def RodCutTableRecurrence (price table : Nat → Nat) (limit : Nat) : Prop := table 0 = 0 ∧ ∀ n, n < limit → table (n + 1) = (Finset.Icc 1 (n + 1)).sup (fun cut => FirstCutValue price table (n + 1) cut)

The canonical executable rod-cutting value function obtained by recursively evaluating the CLRS first-cut recurrence. The recurrence is written over Finset.attach so Lean sees that each recursive call is made at a strictly smaller rod length.

def bottomUpRodRevenue (price : Nat → Nat) : Nat → Nat | 0 => 0 | n + 1 => (Finset.Icc 1 (n + 1)).attach.sup (fun cut => price cut.1 + bottomUpRodRevenue price ((n + 1) - cut.1)) termination_by n => n decreasing_by simp_wf exact (Finset.mem_Icc.mp cut.2).1
private theorem finset_attach_sup_eq (s : Finset Nat) (f : Nat → Nat) : s.attach.sup (fun x => f x.1) = s.sup f := by apply le_antisymm · refine Finset.sup_le ?_ intro x _hx exact Finset.le_sup (f := f) x.2 · refine Finset.sup_le ?_ intro x hx exact Finset.le_sup (f := fun x : {x // x ∈ s} => f x.1) (Finset.mem_attach s ⟨x, hx⟩) @[simp] theorem bottomUpRodRevenue_zero (price : Nat → Nat) : bottomUpRodRevenue price 0 = 0 := by rw [bottomUpRodRevenue]

The executable recurrence unfolds to the textbook first-cut maximum.

theorem bottomUpRodRevenue_succ (price : Nat → Nat) (n : Nat) : bottomUpRodRevenue price (n + 1) = (Finset.Icc 1 (n + 1)).sup (fun cut => FirstCutValue price (bottomUpRodRevenue price) (n + 1) cut) := by rw [bottomUpRodRevenue] change (Finset.Icc 1 (n + 1)).attach.sup (fun cut => price cut.1 + bottomUpRodRevenue price ((n + 1) - cut.1)) = (Finset.Icc 1 (n + 1)).sup (fun cut => price cut + bottomUpRodRevenue price ((n + 1) - cut)) simpa [FirstCutValue] using (finset_attach_sup_eq (Finset.Icc 1 (n + 1)) (fun cut => price cut + bottomUpRodRevenue price ((n + 1) - cut)))

The executable recurrence-valued function satisfies the CLRS recurrence.

theorem bottomUpRodRevenue_rodCutRecurrence (price : Nat → Nat) : RodCutRecurrence price (bottomUpRodRevenue price) := by constructor · exact bottomUpRodRevenue_zero price · intro n exact bottomUpRodRevenue_succ price n

A global recurrence function induces a correct finite table prefix.

theorem rodCutTableRecurrence_of_rodCutRecurrence {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) (limit : Nat) : RodCutTableRecurrence price revenue limit := by constructor · exact hrec.1 · intro n _hn exact hrec.2 n

Every prefix of the executable recurrence-valued function is a correct table.

theorem bottomUpRodRevenue_rodCutTableRecurrence (price : Nat → Nat) (limit : Nat) : RodCutTableRecurrence price (bottomUpRodRevenue price) limit := rodCutTableRecurrence_of_rodCutRecurrence (bottomUpRodRevenue_rodCutRecurrence price) limit
First-cut recurrence facts

Every admissible first cut is bounded by the recurrence value.

theorem firstCutValue_le_of_rodCutRecurrence {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) {n cut : Nat} (hcut : cut ∈ Finset.Icc 1 n) : FirstCutValue price revenue n cut ≤ revenue n := by cases n with | zero => simp at hcut | succ n => rw [hrec.2 n] exact Finset.le_sup hcut

If a number bounds every first-cut candidate, then it bounds the recurrence value. This is the upper-bound half of the Bellman maximum principle.

theorem rodRevenue_le_of_firstCutValue_bounds {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) {n bound : Nat} (hbound : ∀ cut, cut ∈ Finset.Icc 1 n → FirstCutValue price revenue n cut ≤ bound) : revenue n ≤ bound := by cases n with | zero => rw [hrec.1] exact Nat.zero_le bound | succ n => rw [hrec.2 n] exact Finset.sup_le hbound

Selling the whole rod as one piece is one admissible first-cut candidate.

theorem price_le_revenue_of_rodCutRecurrence {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) {n : Nat} (hn : 1 ≤ n) : price n ≤ revenue n := by have hmem : n ∈ Finset.Icc 1 n := by rw [Finset.mem_Icc] exact ⟨hn, le_rfl⟩ have hcut := firstCutValue_le_of_rodCutRecurrence (price := price) (revenue := revenue) hrec hmem have hprice : price n ≤ FirstCutValue price revenue n n := by unfold FirstCutValue omega exact Nat.le_trans hprice hcut
Bottom-up table facts

Every admissible first cut is bounded by the value stored in a correct finite bottom-up table, provided the queried rod length lies inside the filled prefix.

theorem firstCutValue_le_of_rodCutTableRecurrence {price table : Nat → Nat} {limit n cut : Nat} (htable : RodCutTableRecurrence price table limit) (hn : n ≤ limit) (hcut : cut ∈ Finset.Icc 1 n) : FirstCutValue price table n cut ≤ table n := by cases n with | zero => simp at hcut | succ n => rw [htable.2 n (Nat.lt_of_succ_le hn)] exact Finset.le_sup hcut

If a number bounds every first-cut candidate inside a correct finite table prefix, then it bounds the stored table value.

theorem rodTableValue_le_of_firstCutValue_bounds {price table : Nat → Nat} {limit n bound : Nat} (htable : RodCutTableRecurrence price table limit) (hn : n ≤ limit) (hbound : ∀ cut, cut ∈ Finset.Icc 1 n → FirstCutValue price table n cut ≤ bound) : table n ≤ bound := by cases n with | zero => rw [htable.1] exact Nat.zero_le bound | succ n => rw [htable.2 n (Nat.lt_of_succ_le hn)] exact Finset.sup_le hbound

Selling the whole rod is also bounded by a correct finite table prefix.

theorem price_le_table_of_rodCutTableRecurrence {price table : Nat → Nat} {limit n : Nat} (htable : RodCutTableRecurrence price table limit) (hn : 1 ≤ n) (hlimit : n ≤ limit) : price n ≤ table n := by have hmem : n ∈ Finset.Icc 1 n := by rw [Finset.mem_Icc] exact ⟨hn, le_rfl⟩ have hcut := firstCutValue_le_of_rodCutTableRecurrence (price := price) (table := table) (limit := limit) htable hlimit hmem have hprice : price n ≤ FirstCutValue price table n n := by unfold FirstCutValue omega exact Nat.le_trans hprice hcut
Plan optimality

Every concrete cutting plan with positive pieces is bounded by the recurrence value of its total length.

theorem planValue_le_revenue_of_rodCutRecurrence {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) : ∀ pieces, PositivePieces pieces → planValue price pieces ≤ revenue (planLength pieces) | [], _hpos => by simp [planValue, planLength, hrec.1] | piece :: rest, hpos => by have hpiece_pos : 0 < piece := by exact hpos piece (by simp) have hrest_pos : PositivePieces rest := by intro x hx exact hpos x (by simp [hx]) have ih := planValue_le_revenue_of_rodCutRecurrence (price := price) (revenue := revenue) hrec rest hrest_pos have hmem : piece ∈ Finset.Icc 1 (piece + planLength rest) := by rw [Finset.mem_Icc] exact ⟨Nat.succ_le_of_lt hpiece_pos, Nat.le_add_right piece (planLength rest)⟩ have hcut := firstCutValue_le_of_rodCutRecurrence (price := price) (revenue := revenue) hrec hmem have hcut' : price piece + revenue (planLength rest) ≤ revenue (piece + planLength rest) := by simpa [FirstCutValue, Nat.add_sub_cancel_left] using hcut have hmono : price piece + planValue price rest ≤ price piece + revenue (planLength rest) := Nat.add_le_add_left ih (price piece) simpa [planValue, planLength] using Nat.le_trans hmono hcut'

Every concrete cutting plan whose total length is inside a correct finite bottom-up table prefix is bounded by the table value at that total length.

theorem planValue_le_table_of_rodCutTableRecurrence {price table : Nat → Nat} {limit : Nat} (htable : RodCutTableRecurrence price table limit) : ∀ pieces, PositivePieces pieces → planLength pieces ≤ limit → planValue price pieces ≤ table (planLength pieces) | [], _hpos, _hlen => by simp [planValue, planLength, htable.1] | piece :: rest, hpos, hlen => by have hpiece_pos : 0 < piece := by exact hpos piece (by simp) have hrest_pos : PositivePieces rest := by intro x hx exact hpos x (by simp [hx]) have htotal : piece + planLength rest ≤ limit := by simpa [planLength] using hlen have hrest_limit : planLength rest ≤ limit := by omega have ih : planValue price rest ≤ table (planLength rest) := planValue_le_table_of_rodCutTableRecurrence (price := price) (table := table) (limit := limit) htable rest hrest_pos hrest_limit have hmem : piece ∈ Finset.Icc 1 (piece + planLength rest) := by rw [Finset.mem_Icc] exact ⟨Nat.succ_le_of_lt hpiece_pos, Nat.le_add_right piece (planLength rest)⟩ have hfirst := firstCutValue_le_of_rodCutTableRecurrence (price := price) (table := table) (limit := limit) htable htotal hmem have hfirstBound : price piece + table (planLength rest) ≤ table (piece + planLength rest) := by simpa [FirstCutValue, Nat.add_sub_cancel_left] using hfirst have hmono : price piece + planValue price rest ≤ price piece + table (planLength rest) := Nat.add_le_add_left ih (price piece) simpa [planValue, planLength] using Nat.le_trans hmono hfirstBound

Every positive-piece cutting plan is bounded by the executable recurrence value of its total length.

theorem planValue_le_bottomUpRodRevenue (price : Nat → Nat) : ∀ pieces, PositivePieces pieces → planValue price pieces ≤ bottomUpRodRevenue price (planLength pieces) := planValue_le_revenue_of_rodCutRecurrence (price := price) (revenue := bottomUpRodRevenue price) (bottomUpRodRevenue_rodCutRecurrence price)

If a cutting plan attains the recurrence value for its length, then every other positive-piece plan of the same total length has value at most that plan.

theorem planValue_le_optimalPlanValue_of_same_length {price revenue : Nat → Nat} (hrec : RodCutRecurrence price revenue) {candidate other : List Nat} (hother_pos : PositivePieces other) (hlen : planLength other = planLength candidate) (hcandidate_value : planValue price candidate = revenue (planLength candidate)) : planValue price other ≤ planValue price candidate := by have hother_bound := planValue_le_revenue_of_rodCutRecurrence (price := price) (revenue := revenue) hrec other hother_pos rw [hlen, ← hcandidate_value] at hother_bound exact hother_bound

If a cutting plan attains the table value inside a correct finite bottom-up prefix, then every other positive-piece plan of the same length has value at most that plan.

theorem planValue_le_tablePlanValue_of_same_length {price table : Nat → Nat} {limit : Nat} (htable : RodCutTableRecurrence price table limit) {candidate other : List Nat} (hother_pos : PositivePieces other) (hlen : planLength other = planLength candidate) (hcandidate_value : planValue price candidate = table (planLength candidate)) (hcandidate_len : planLength candidate ≤ limit) : planValue price other ≤ planValue price candidate := by have hother_len : planLength other ≤ limit := by rw [hlen] exact hcandidate_len have hother_bound := planValue_le_table_of_rodCutTableRecurrence (price := price) (table := table) (limit := limit) htable other hother_pos hother_len rw [hlen, ← hcandidate_value] at hother_bound exact hother_bound

If a cutting plan attains the executable recurrence value for its length, then every other positive-piece plan of the same length has value at most that plan.

theorem planValue_le_bottomUpRodPlanValue_of_same_length {price : Nat → Nat} {candidate other : List Nat} (hother_pos : PositivePieces other) (hlen : planLength other = planLength candidate) (hcandidate_value : planValue price candidate = bottomUpRodRevenue price (planLength candidate)) : planValue price other ≤ planValue price candidate := planValue_le_optimalPlanValue_of_same_length (price := price) (revenue := bottomUpRodRevenue price) (bottomUpRodRevenue_rodCutRecurrence price) hother_pos hlen hcandidate_value
Mutable-array bottom-up implementation

This block refines the pure recurrence-valued rod-cutting function to CLRS's BOTTOM-UP-CUT-ROD, which fills a physical revenue table r[0 .. n] from the bottom up. We model the table as an actual Array Nat grown one slot at a time with Array.­push, reusing the mutable-Array pattern of Section 17.4, and prove a refinement theorem: reading the mutable table at any filled index returns exactly the pure recurrence value bottomUpRodRevenue. As a corollary the array read satisfies RodCutTableRecurrence, so the mutable table inherits the plan-optimality guarantees proved above.

Total read from a Nat-valued array, returning 0 for out-of-range indices. This models the invariant-guarded reads a bottom-up dynamic-programming table performs: every access made by the algorithm is in range, and the default never fires during a real fill.

def arrGet (a : Array Nat) (i : Nat) : Nat := (a[i]?).getD 0

Reading an in-range index is unaffected by pushing a new trailing element.

theorem arrGet_push_lt (a : Array Nat) (x i : Nat) (h : i < a.size) : arrGet (a.push x) i = arrGet a i := by unfold arrGet rw [Array.getElem?_push, if_neg (Nat.ne_of_lt h)]

Reading the freshly pushed slot returns the pushed element.

theorem arrGet_push_size (a : Array Nat) (x : Nat) : arrGet (a.push x) a.size = x := by unfold arrGet rw [Array.getElem?_push, if_pos rfl] rfl

Bottom-up mutable-array construction of the rod-cutting revenue table. The value rodRevenueArrayAux price n is an Array Nat of length n + 1 whose entry k is the best revenue for a rod of length k. Each new entry is computed as the CLRS first-cut maximum over Finset.Icc 1 (j + 1), reading the earlier revenues that are already stored in the array - the imperative BOTTOM-UP-CUT-ROD inner loop q = max(q, p[i] + r[j - i]).

def rodRevenueArrayAux (price : Nat → Nat) : Nat → Array Nat | 0 => #[0] | j + 1 => let previous := rodRevenueArrayAux price j previous.push ((Finset.Icc 1 (j + 1)).sup (fun i => price i + arrGet previous ((j + 1) - i)))

The bottom-up table for rod length n stores exactly n + 1 entries.

theorem rodRevenueArrayAux_size (price : Nat → Nat) (n : Nat) : (rodRevenueArrayAux price n).size = n + 1 := by induction n with | zero => rfl | succ j ih => simp only [rodRevenueArrayAux, Array.size_push, ih]

Refinement of the mutable-array fill to the recurrence value. Every filled entry of the bottom-up array equals the pure recurrence value bottomUpRodRevenue at the same index. The proof is an induction on the table length whose step reads back the earlier entries the fill relied upon.

theorem arrGet_rodRevenueArrayAux (price : Nat → Nat) : ∀ n k, k ≤ n → arrGet (rodRevenueArrayAux price n) k = bottomUpRodRevenue price k := by intro n induction n with | zero => intro k hk obtain rfl : k = 0 := Nat.le_zero.mp hk simp only [rodRevenueArrayAux, bottomUpRodRevenue_zero] rfl | succ j ih => intro k hk have hsize : (rodRevenueArrayAux price j).size = j + 1 := rodRevenueArrayAux_size price j simp only [rodRevenueArrayAux] rcases Nat.eq_or_lt_of_le hk with heq | hlt · -- k is the newly pushed top entry j + 1 have hk_size : k = (rodRevenueArrayAux price j).size := by rw [hsize]; exact heq rw [hk_size, arrGet_push_size, ← hk_size, heq] have hsup : (Finset.Icc 1 (j + 1)).sup (fun i => price i + arrGet (rodRevenueArrayAux price j) ((j + 1) - i)) = (Finset.Icc 1 (j + 1)).sup (fun i => price i + bottomUpRodRevenue price ((j + 1) - i)) := by apply Finset.sup_congr rfl intro i hi have hle : (j + 1) - i ≤ j := by have := (Finset.mem_Icc.mp hi).1 omega rw [ih ((j + 1) - i) hle] rw [hsup, bottomUpRodRevenue_succ] simp only [FirstCutValue] · -- k lies inside the already-filled prefix have hkj : k ≤ j := Nat.lt_succ_iff.mp hlt have hk_lt : k < (rodRevenueArrayAux price j).size := by rw [hsize]; omega rw [arrGet_push_lt _ _ _ hk_lt] exact ih k hkj

The CLRS BOTTOM-UP-CUT-ROD revenue table for a rod of length n, materialized as a mutable Array Nat of length n + 1.

def rodRevenueArray (price : Nat → Nat) (n : Nat) : Array Nat := rodRevenueArrayAux price n

The materialized table has one entry per rod length in 0 .. n.

theorem rodRevenueArray_size (price : Nat → Nat) (n : Nat) : (rodRevenueArray price n).size = n + 1 := rodRevenueArrayAux_size price n

Correctness of the mutable-array bottom-up rod cutting. For every rod length k inside the filled prefix, the entry the imperative table stores equals the pure recurrence value bottomUpRodRevenue. This is the refinement theorem requested by the mutable-array dynamic-programming layer of CLRS Chapter 15.

theorem rodRevenueArray_correct (price : Nat → Nat) (n k : Nat) (hk : k ≤ n) : arrGet (rodRevenueArray price n) k = bottomUpRodRevenue price k := arrGet_rodRevenueArrayAux price n k hk

The top table entry is the best revenue for the full rod of length n.

theorem rodRevenueArray_full (price : Nat → Nat) (n : Nat) : arrGet (rodRevenueArray price n) n = bottomUpRodRevenue price n := rodRevenueArray_correct price n n (le_refl n)

Reading the mutable-array table is a correct finite bottom-up table: its entry zero is zero and every positive entry inside the filled prefix is the CLRS first-cut maximum over earlier table entries. This connects the imperative computation to the abstract RodCutTableRecurrence interface.

theorem rodRevenueArray_rodCutTableRecurrence (price : Nat → Nat) (n : Nat) : RodCutTableRecurrence price (fun k => arrGet (rodRevenueArray price n) k) n := by constructor · show arrGet (rodRevenueArray price n) 0 = 0 rw [rodRevenueArray_correct price n 0 (Nat.zero_le n), bottomUpRodRevenue_zero] · intro m hm show arrGet (rodRevenueArray price n) (m + 1) = (Finset.Icc 1 (m + 1)).sup (fun cut => FirstCutValue price (fun k => arrGet (rodRevenueArray price n) k) (m + 1) cut) rw [rodRevenueArray_correct price n (m + 1) hm, bottomUpRodRevenue_succ] apply Finset.sup_congr rfl intro cut hcut unfold FirstCutValue have hle : (m + 1) - cut ≤ n := by have := (Finset.mem_Icc.mp hcut).1 omega show price cut + bottomUpRodRevenue price ((m + 1) - cut) = price cut + arrGet (rodRevenueArray price n) ((m + 1) - cut) rw [rodRevenueArray_correct price n ((m + 1) - cut) hle]

Plan optimality through the mutable-array table. Every positive-piece cutting plan whose total length lies inside the filled prefix is bounded by the value the mutable-array bottom-up table stores at that length. This lifts the refinement to the same end-to-end optimality statement proved for the pure recurrence table.

theorem planValue_le_rodRevenueArray (price : Nat → Nat) (n : Nat) : ∀ pieces, PositivePieces pieces → planLength pieces ≤ n → planValue price pieces ≤ arrGet (rodRevenueArray price n) (planLength pieces) := planValue_le_table_of_rodCutTableRecurrence (rodRevenueArray_rodCutTableRecurrence price n)
end Chapter15end CLRS
Imports
import CLRSLean.Chapter_15.Section_15_2_Matrix_Chain_Multiplication
open Finsetopen scoped BigOperators

14.2. Matrix-Chain Multiplication

The legacy CLRS.­Chapter15.­matrixChainOpt and CLRS.­Chapter15.­matrixChainSplit recursively evaluate an optimization specification; they do not store a dynamic-programming table. This section retains their arithmetic table-size and candidate-budget formulas.

The Execution companion supplies MatrixChainExecution.execute: actual arrays of interval-length rows storing costs and selected splits. Each candidate reads strictly shorter stored intervals. Its correctness theorem identifies every stored cost and proves the selected split attains it. Table reconstruction reads those stored splits without rerunning the recurrence. The cell and candidate counters are accumulated by that same fill execution.

The parameter N in the execution is the largest matrix index, so indices 0..N describe N + 1 matrices. Array access, dimension lookup, and arithmetic are primitive events; allocation/copying and arithmetic bit costs are excluded. The formulas below alone are not execution-cost proofs; use the companion's execute_cells and execute_candidateVisits interfaces.

Notation conventions used in this section:

  • dims : the dimension table, dims i = the number of rows of matrix Aᵢ

  • n : the number of matrices

namespace CLRSnamespace Chapter15

Space and time of the table algorithm

The number of distinct (i, j) subproblems with 0 ≤ i ≤ j ≤ n, an arithmetic interval-count formula.

def matrixChainSpace (n : Nat) : Nat := (n + 1) * (n + 2) / 2

An abstract split-count formula: for each interval [i, j] there are j - i candidate split points.

def matrixChainTime (n : Nat) : Nat := (Finset.range (n + 1)).sum (fun j => (Finset.range j).sum (fun i => j - i))

The table has (n + 1)(n + 2) / 2 entries.

theorem matrixChainSpace_eq (n : Nat) : matrixChainSpace n = (n + 1) * (n + 2) / 2 := rfl

Quadratic bound on the interval-count formula.

theorem matrixChainSpace_le_square (n : Nat) : matrixChainSpace n ≤ (n + 2) ^ 2 := by unfold matrixChainSpace calc (n + 1) * (n + 2) / 2 ≤ (n + 1) * (n + 2) := Nat.div_le_self _ _ _ ≤ (n + 2) * (n + 2) := Nat.mul_le_mul_right _ (by omega : n + 1 ≤ n + 2) _ = (n + 2) ^ 2 := by rw [pow_two]

Cubic bound on the abstract split-count formula.

theorem matrixChainTime_le_cubic (n : Nat) : matrixChainTime n ≤ (n + 1) ^ 3 := by unfold matrixChainTime calc (Finset.range (n + 1)).sum (fun j => (Finset.range j).sum (fun i => j - i)) ≤ (Finset.range (n + 1)).sum (fun j => j ^ 2) := by apply Finset.sum_le_sum intro j hj calc (Finset.range j).sum (fun i => j - i) ≤ (Finset.range j).sum (fun _ => j) := by apply Finset.sum_le_sum intro i hi omega _ = j * j := by simp [Finset.sum_const, Finset.card_range] _ = j ^ 2 := by rw [pow_two] _ ≤ (n + 1) * n ^ 2 := by have hbound : ∀ j ∈ Finset.range (n + 1), j ^ 2 ≤ n ^ 2 := by intro j hj have hjle : j ≤ n := by simpa [mem_range] using hj exact Nat.pow_le_pow_left hjle 2 simpa [Finset.card_range, nsmul_eq_mul] using (Finset.sum_le_card_nsmul (Finset.range (n + 1)) (fun j => j ^ 2) (n ^ 2) (by intro j hj; exact hbound j hj)) _ ≤ (n + 1) ^ 3 := by have h : n ^ 2 ≤ (n + 1) ^ 2 := Nat.pow_le_pow_left (Nat.le_succ n) 2 have h' : (n + 1) * n ^ 2 ≤ (n + 1) * (n + 1) ^ 2 := Nat.mul_le_mul_left (n + 1) h rw [show (n + 1) ^ 3 = (n + 1) * (n + 1) ^ 2 by rw [pow_succ, mul_comm]] exact h'
end Chapter15end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_14.Section_14_2_Matrix_Chain_Multiplication.Execution

Stored matrix-chain costs and splits

The endpoint N denotes matrices indexed 0 through N, hence N+1 matrices. Layer l stores intervals [i,i+l]; only shorter layers are read. Every split candidate is evaluated once, and its minimizing index is stored with its cost. The old recursive optimum is used only in proofs.

namespace CLRS.Chapter15.MatrixChainExecutionopen DPExecutionstructure Cell where cost : Nat split : Nat deriving Inhabited, Repr, DecidableEqdef candidate (dims : Nat → Nat) (rows : Array (Array Cell)) (i l k : Nat) : Nat := (get rows (k-i) i).cost + (get rows (i+l-(k+1)) (k+1)).cost + dims i * dims (k+1) * dims (i+l+1)def step (dims : Nat → Nat) : Nat → Array (Array Cell) → Nat → Cell × Nat | 0, _, i => (⟨0, i⟩, 0) | l+1, rows, i => let best := minimum (candidate dims rows i (l+1)) i l (⟨best.value, best.index⟩, best.visits)

Compute and retain all intervals 0≤i≤j≤N.

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

The stored split is in range and attains the independently defined optimum.

def CorrectCell (dims : Nat → Nat) (l i : Nat) (cell : Cell) : Prop := cell.cost = matrixChainOpt dims i (i+l) ∧ (0 < l → i ≤ cell.split ∧ cell.split < i+l ∧ cell.cost = matrixSplitCost dims (matrixChainOpt dims) i (i+l) cell.split)
private theorem candidate_correct (dims : Nat → Nat) (N l i : Nat) (rows : Array (Array Cell)) (hprev : ∀ k, k < l → ∀ i, i < N+1-k → CorrectCell dims k i (get rows k i)) (hi : i < N+1-l) (k : Nat) (hk : i ≤ k) (hk' : k < i+l) : candidate dims rows i l k = matrixSplitCost dims (matrixChainOpt dims) i (i+l) k := by have hleft := (hprev (k-i) (by omega) i (by omega)).1 have hright := (hprev (i+l-(k+1)) (by omega) (k+1) (by omega)).1 have he : i + (k-i) = k := by omega have he' : k+1+(i+l-(k+1)) = i+l := by omega rw [he] at hleft rw [he'] at hright simp only [candidate, matrixSplitCost, hleft, hright] private theorem step_correct (dims : Nat → Nat) (N l : Nat) (rows : Array (Array Cell)) (hprev : ∀ k, k < l → ∀ i, i < N+1-k → CorrectCell dims k i (get rows k i)) (i : Nat) (hi : i < N+1-l) : CorrectCell dims l i (step dims l rows i).1 := by cases l with | zero => simp [CorrectCell, step, matrixChainOpt] | succ l => have hc := candidate_correct dims N (l+1) i rows hprev hi let f := candidate dims rows i (l+1) have hbest : (minimum f i l).value = matrixChainOpt dims i (i+(l+1)) := by apply minimum_value_eq · intro k hk hk' dsimp only [f] rw [hc k hk (by omega)] exact (matrixChainOpt_lowerBound dims).2 (by simp [Finset.mem_Icc]; omega) · obtain ⟨hk, heq⟩ := matrixChainSplit_optimal dims i (i+(l+1)) (by omega) have hb := Finset.mem_Icc.mp hk refine ⟨matrixChainSplit dims i (i+(l+1)), hb.1, by omega, ?_⟩ exact (hc _ hb.1 (by omega)).trans heq.symm obtain ⟨hlo, hhi, heq, _⟩ := minimum_spec f i l change (minimum f i l).value = _ ∧ (0 < l+1 → i ≤ (minimum f i l).index ∧ (minimum f i l).index < i+(l+1) ∧ (minimum f i l).value = _) refine ⟨hbest, fun _ => ⟨hlo, by omega, ?_⟩⟩ exact heq.trans (hc _ hlo (by omega))

Every stored entry is the optimum, with a valid tight stored split.

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

A direct cost-table refinement for interval [i,j].

theorem execute_cost (dims : Nat → Nat) (N i j : Nat) (hij : i ≤ j) (hj : j ≤ N) : (get (execute dims N).rows (j-i) i).cost = matrixChainOpt dims i j := by have h := (execute_get_correct dims N (j-i) i (by omega) (by omega)).1 simpa [Nat.add_sub_of_le hij] using h
@[simp] theorem step_visits (dims : Nat → Nat) (l : Nat) (rows : Array (Array Cell)) (i : Nat) : (step dims l rows i).2 = l := by cases l <;> simp [step]

Each interval cell is written once by the actual layered execution.

theorem execute_cells (dims : Nat → Nat) (N : Nat) : (execute dims N).cellWrites = ∑ l ∈ Finset.range (N+1), (N+1-l) := buildLayers_cellWrites _ _ _

Candidate visits come from the returned minimum-scan counters.

theorem execute_candidateVisits (dims : Nat → Nat) (N : Nat) : (execute dims N).candidateVisits = ∑ l ∈ Finset.range (N+1), (N+1-l)*l := buildLayers_candidateVisits _ id _ (step_visits dims) _

A finite stored table has the certified cost/split contract on its domain.

def CorrectTable (dims : Nat → Nat) (N : Nat) (rows : Array (Array Cell)) : Prop := ∀ l i, l ≤ N → i+l ≤ N → CorrectCell dims l i (get rows l i)
private theorem stored_split {dims : Nat → Nat} {N : Nat} {rows : Array (Array Cell)} (h : CorrectTable dims N rows) (i j : Nat) (hij : i < j) (hj : j ≤ N) : i ≤ (get rows (j-i) i).split ∧ (get rows (j-i) i).split < j ∧ matrixChainOpt dims i j = matrixSplitCost dims (matrixChainOpt dims) i j (get rows (j-i) i).split := by have hc := h (j-i) i (by omega) (by omega) have hs := hc.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 using stored indices only. The finite-domain proof is erased; no recursive optimum or legacy split selector is evaluated here.

def reconstruct (dims : Nat → Nat) (N : Nat) (rows : Array (Array Cell)) (h : CorrectTable dims N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) : ChainPlan i j := if ht : i < j then let k := (get rows (j-i) i).split have hs := stored_split h i j ht hj ChainPlan.split i k j (reconstruct dims N rows h i k hs.1 (by omega)) (reconstruct dims N rows h (k+1) j (by omega) hj) else have he : i = j := by omega he ▸ ChainPlan.single i termination_by j-i decreasing_by all_goals have _hs := stored_split h i j ht hj try dsimp only [k] at * omega

The plan follows the stored split in every subinterval.

theorem reconstruct_reconstructed (dims : Nat → Nat) (N : Nat) (rows : Array (Array Cell)) (h : CorrectTable dims N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) : ChainPlan.ReconstructedBy (fun i j => (get rows (j-i) i).split) (reconstruct dims N rows h i j hij hj) := by rw [reconstruct] split next ht => have hs := stored_split h i j ht hj exact ChainPlan.ReconstructedBy.split i _ j rfl (reconstruct_reconstructed dims N rows h i _ hs.1 (by omega)) (reconstruct_reconstructed dims N rows h _ j (by omega) hj) next ht => have he : i = j := by omega subst j exact ChainPlan.ReconstructedBy.single i termination_by j-i decreasing_by all_goals omega

Stored-table reconstruction attains the independent optimum.

theorem reconstruct_cost (dims : Nat → Nat) (N : Nat) (rows : Array (Array Cell)) (h : CorrectTable dims N rows) (i j : Nat) (hij : i ≤ j) (hj : j ≤ N) : ChainPlan.cost dims (reconstruct dims N rows h i j hij hj) = matrixChainOpt dims i j := by rw [reconstruct] split next ht => have hs := stored_split h i j ht hj rw [ChainPlan.cost, reconstruct_cost dims N rows h i _ hs.1 (by omega), reconstruct_cost dims N rows h _ j (by omega) hj] exact hs.2.2.symm next ht => have he : i = j := by omega subst j simp [ChainPlan.cost, matrixChainOpt] termination_by j-i decreasing_by all_goals omega

Build a table once and reconstruct the complete chain from that same table.

def executePlan (dims : Nat → Nat) (N : Nat) : ChainPlan 0 N × Table Cell := let table := execute dims N (reconstruct dims N table.rows (fun l i hl hi => execute_get_correct dims N l i hl hi) 0 N (Nat.zero_le _) le_rfl, table)
theorem executePlan_correct (dims : Nat → Nat) (N : Nat) : MatrixChainOptimalPlan dims (executePlan dims N).1 := by intro other have he := reconstruct_cost dims N (execute dims N).rows (fun l i hl hi => execute_get_correct dims N l i hl hi) 0 N (Nat.zero_le _) le_rfl change ChainPlan.cost dims (reconstruct dims N (execute dims N).rows _ 0 N _ _) ≤ _ rw [he] exact matrixChain_opt_le_planCost (matrixChainOpt_lowerBound dims) other

Every actual interval-evaluation event is unique.

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

The actual evaluation trace covers exactly the valid interval states.

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

Quadratic storage from actual interval writes.

theorem execute_cells_le (dims : Nat → Nat) (N : Nat) : (execute dims 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 (dims : Nat → Nat) (N : Nat) : (execute dims N).candidateVisits ≤ (N+1)^3 := by rw [execute_candidateVisits] exact interval_visits_le_cube N

The reconstructed plan's cost equals the optimum in the same returned table.

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

Exact quadratic count of stored interval cells.

theorem execute_cells_closed (dims : Nat → Nat) (N : Nat) : 2 * (execute dims 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 (dims : Nat → Nat) (N : Nat) : 6 * (execute dims 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 (dims : Nat → Nat) (N : Nat) : (N+1)^2 ≤ 2 * (execute dims N).cellWrites ∧ (execute dims N).cellWrites ≤ (N+1)^2 := by refine ⟨?_, execute_cells_le dims N⟩ rw [execute_cells_closed] nlinarith

Two-sided cubic candidate bounds.

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

CLRSLean.Chapter_15.Section_15_2_Matrix_Chain_Multiplication

CLRS Section 15.2 - Matrix-chain multiplication

This section adds a first mathematical proof layer for matrix-chain multiplication. A parenthesization is represented by an inductive ChainPlan i j, and a candidate dynamic-programming cost table is specified by the usual split lower bound. The main theorem says every concrete parenthesization has cost at least the candidate optimum for its interval. The file also adds a reconstruction certificate: if a split table records a tight split for each nonsingleton interval, then any parenthesization rebuilt from that split table has exactly the candidate optimal cost, and therefore has cost no greater than any competing parenthesization. Any two plans reconstructed from the same tight split table for the same interval have the same cost.

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

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 Chapter15
Parenthesization model

A binary parenthesization of the matrix chain from index i to j.

inductive ChainPlan : Nat → Nat → Type where | single (i : Nat) : ChainPlan i i | split (i k j : Nat) : ChainPlan i k → ChainPlan (k + 1) j → ChainPlan i j
namespace ChainPlan

The left endpoint of a chain plan is at most the right endpoint.

theorem start_le_end {i j : Nat} (plan : ChainPlan i j) : i ≤ j := by induction plan with | single i => exact le_rfl | split i k j left right ihLeft ihRight => exact Nat.le_trans ihLeft (Nat.le_trans (Nat.le_succ k) ihRight)

The scalar multiplication cost of a parenthesization, using the CLRS dimension array convention: matrix A_i has dimensions dims i by dims (i+1).

def cost (dims : Nat → Nat) : {i j : Nat} → ChainPlan i j → Nat | _, _, single _ => 0 | _, _, split i k j left right => cost dims left + cost dims right + dims i * dims (k + 1) * dims (j + 1)

A parenthesization is reconstructed from a split table when every internal node uses the split index prescribed for its interval.

inductive ReconstructedBy (splitAt : Nat → Nat → Nat) : {i j : Nat} → ChainPlan i j → Prop where | single (i : Nat) : ReconstructedBy splitAt (single i) | split (i k j : Nat) {left : ChainPlan i k} {right : ChainPlan (k + 1) j} : k = splitAt i j → ReconstructedBy splitAt left → ReconstructedBy splitAt right → ReconstructedBy splitAt (ChainPlan.split i k j left right)
end ChainPlan
Optimality interface

The CLRS split cost for multiplying matrices i..j split after k.

def matrixSplitCost (dims : Nat → Nat) (opt : Nat → Nat → Nat) (i j k : Nat) : Nat := opt i k + opt (k + 1) j + dims i * dims (k + 1) * dims (j + 1)

A candidate cost table satisfies the matrix-chain lower-bound recurrence if every valid first split has cost at least the table entry.

def MatrixChainLowerBound (dims : Nat → Nat) (opt : Nat → Nat → Nat) : Prop := (∀ i, opt i i = 0) ∧ ∀ {i j k}, k ∈ Finset.Icc i (j - 1) → opt i j ≤ matrixSplitCost dims opt i j k

A split table is tight for a candidate matrix-chain cost table when each nonsingleton interval chooses a valid first split whose split cost is exactly the table entry.

def MatrixChainSplitOptimal (dims : Nat → Nat) (opt : Nat → Nat → Nat) (splitAt : Nat → Nat → Nat) : Prop := (∀ i, opt i i = 0) ∧ ∀ {i j}, i < j → splitAt i j ∈ Finset.Icc i (j - 1) ∧ opt i j = matrixSplitCost dims opt i j (splitAt i j)

A concrete parenthesization is optimal when no other plan has lower cost.

def MatrixChainOptimalPlan (dims : Nat → Nat) {i j : Nat} (plan : ChainPlan i j) : Prop := ∀ other : ChainPlan i j, ChainPlan.cost dims plan ≤ ChainPlan.cost dims other

Every concrete parenthesization has cost at least the candidate optimum specified by the recurrence lower-bound interface.

theorem matrixChain_opt_le_planCost {dims : Nat → Nat} {opt : Nat → Nat → Nat} (hopt : MatrixChainLowerBound dims opt) : ∀ {i j : Nat} (plan : ChainPlan i j), opt i j ≤ ChainPlan.cost dims plan := by intro i j plan induction plan with | single i => simpa [ChainPlan.cost] using hopt.1 i | split i k j left right ihLeft ihRight => have hik : i ≤ k := ChainPlan.start_le_end left have hkj : k + 1 ≤ j := ChainPlan.start_le_end right have hmem : k ∈ Finset.Icc i (j - 1) := by rw [Finset.mem_Icc] omega have hsplit := hopt.2 hmem unfold matrixSplitCost at hsplit simp [ChainPlan.cost] omega

Any plan reconstructed from a tight split table has exactly the candidate optimal cost.

theorem matrixChain_reconstructed_cost_eq {dims : Nat → Nat} {opt : Nat → Nat → Nat} {splitAt : Nat → Nat → Nat} (hsplit : MatrixChainSplitOptimal dims opt splitAt) : ∀ {i j : Nat} {plan : ChainPlan i j}, ChainPlan.ReconstructedBy splitAt plan → ChainPlan.cost dims plan = opt i j := by intro i j plan hrec induction hrec with | single i => simpa [ChainPlan.cost] using (hsplit.1 i).symm | split => rename_i i k j left right hk _hleft _hright ihLeft ihRight subst k have hij : i < j := by have hleftLe : i ≤ splitAt i j := ChainPlan.start_le_end left have hrightLe : splitAt i j + 1 ≤ j := ChainPlan.start_le_end right omega rcases hsplit.2 hij with ⟨_hmem, hcost⟩ simp [ChainPlan.cost, matrixSplitCost, ihLeft, ihRight, hcost]

Any two parenthesizations reconstructed from the same tight split table for the same interval have equal cost.

theorem matrixChain_reconstructed_cost_eq_of_reconstructed {dims : Nat → Nat} {opt : Nat → Nat → Nat} {splitAt : Nat → Nat → Nat} (hsplit : MatrixChainSplitOptimal dims opt splitAt) {i j : Nat} {left right : ChainPlan i j} (hleft : ChainPlan.ReconstructedBy splitAt left) (hright : ChainPlan.ReconstructedBy splitAt right) : ChainPlan.cost dims left = ChainPlan.cost dims right := by calc ChainPlan.cost dims left = opt i j := matrixChain_reconstructed_cost_eq hsplit hleft _ = ChainPlan.cost dims right := (matrixChain_reconstructed_cost_eq hsplit hright).symm

Combining a lower-bound table with a tight split-table reconstruction proves the reconstructed parenthesization is globally optimal.

theorem matrixChain_reconstructed_optimal {dims : Nat → Nat} {opt : Nat → Nat → Nat} {splitAt : Nat → Nat → Nat} (hlower : MatrixChainLowerBound dims opt) (hsplit : MatrixChainSplitOptimal dims opt splitAt) {i j : Nat} {plan : ChainPlan i j} (hrec : ChainPlan.ReconstructedBy splitAt plan) : MatrixChainOptimalPlan dims plan := by intro other have hcost : ChainPlan.cost dims plan = opt i j := matrixChain_reconstructed_cost_eq hsplit hrec have hother : opt i j ≤ ChainPlan.cost dims other := matrixChain_opt_le_planCost hlower other omega

Direct cost inequality form of the split-table reconstruction theorem: a plan rebuilt from a tight split table is no more expensive than any other parenthesization of the same interval.

theorem matrixChain_reconstructed_cost_le_planCost {dims : Nat → Nat} {opt : Nat → Nat → Nat} {splitAt : Nat → Nat → Nat} (hlower : MatrixChainLowerBound dims opt) (hsplit : MatrixChainSplitOptimal dims opt splitAt) {i j : Nat} {plan : ChainPlan i j} (hrec : ChainPlan.ReconstructedBy splitAt plan) (other : ChainPlan i j) : ChainPlan.cost dims plan ≤ ChainPlan.cost dims other := by exact matrixChain_reconstructed_optimal hlower hsplit hrec other
Recursive cost specification and final optimality
def matrixChainOpt (dims : Nat → Nat) : Nat → Nat → Nat | i, j => if h : i < j then (Finset.Icc i (j - 1)).attach.inf' (Finset.attach_nonempty_iff.mpr (by use i; simp [Finset.mem_Icc]; omega)) (fun k => matrixChainOpt dims i k.1 + matrixChainOpt dims (k.1 + 1) j + dims i * dims (k.1 + 1) * dims (j + 1)) else 0 termination_by i j => j - i decreasing_by all_goals have hk := Finset.mem_Icc.mp k.2 omega theorem matrixChainOpt_lowerBound (dims : Nat → Nat) : MatrixChainLowerBound dims (matrixChainOpt dims) := by refine ⟨?_, ?_⟩ · intro i; unfold matrixChainOpt; simp · intro i j k hk rcases Finset.mem_Icc.mp hk with ⟨hik, hkj⟩ by_cases hij : i < j · unfold matrixChainOpt; simp [hij] unfold matrixSplitCost have hm : (⟨k, Finset.mem_Icc.mpr ⟨hik, hkj⟩⟩ : {x // x ∈ Finset.Icc i (j - 1)}) ∈ (Finset.Icc i (j - 1)).attach := by simp -- Goal: attach.inf' (fun r => ... r.1 ...) ≤ matrixChainOpt i k + ... -- Finset.inf'_le gives: attach.inf' (fun r => ...) ≤ (fun r => ... r.1 ...) ⟨k, ...⟩ -- After beta reduction, RHS = matrixChainOpt i k + ... let f : {x // x ∈ Finset.Icc i (j - 1)} → ℕ := λ r => matrixChainOpt dims i r.1 + matrixChainOpt dims (r.1 + 1) j + dims i * dims (r.1 + 1) * dims (j + 1) simpa [f] using Finset.inf'_le f hm · have hzero : matrixChainOpt dims i j = 0 := by unfold matrixChainOpt; simp [hij] rw [hzero] exact Nat.zero_le _ private lemma bridge_attach_inf (dims : Nat → Nat) (i j : Nat) (hij : i < j) : matrixChainOpt dims i j = (Finset.Icc i (j - 1)).inf' (by use i; simp [Finset.mem_Icc]; omega) (λ k => matrixChainOpt dims i k + matrixChainOpt dims (k + 1) j + dims i * dims (k + 1) * dims (j + 1)) := by let s := Finset.Icc i (j - 1) have Hs : s.Nonempty := by use i; simp [s, Finset.mem_Icc]; omega let f (k : ℕ) := matrixChainOpt dims i k + matrixChainOpt dims (k + 1) j + dims i * dims (k + 1) * dims (j + 1) let g (r : {x // x ∈ s}) : ℕ := matrixChainOpt dims i r.1 + matrixChainOpt dims (r.1 + 1) j + dims i * dims (r.1 + 1) * dims (j + 1) have h1 : matrixChainOpt dims i j = s.attach.inf' (Finset.attach_nonempty_iff.mpr Hs) g := by unfold matrixChainOpt; simp [hij, s, g] have h2 : s.attach.inf' (Finset.attach_nonempty_iff.mpr Hs) g = s.inf' Hs f := by have h_att : s.attach.Nonempty := Finset.attach_nonempty_iff.mpr Hs apply le_antisymm · -- attach.inf' ≤ inf', via lower bound on inf' apply Finset.le_inf' Hs f intro x hx have hm : (⟨x, hx⟩ : {x // x ∈ s}) ∈ s.attach := by simp simpa [f, g] using Finset.inf'_le g hm · -- inf' ≤ attach.inf', via lower bound on attach.inf' apply Finset.le_inf' h_att g intro r hr -- r ∈ s.attach, so r.2 : r.1 ∈ s simpa [f, g] using Finset.inf'_le f r.2 rw [h1, h2] 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

The computable split-point selector for matrix-chain DP. For interval i < j, it selects the smallest k in [i, j-1] that attains the minimum split cost. This makes the entire reconstruction chain computable without Exists.choose.

def matrixChainSplit (dims : Nat → Nat) (i j : Nat) : Nat := if h : i < j then (Finset.Icc i (j - 1)).filter (fun k => matrixChainOpt dims i k + matrixChainOpt dims (k + 1) j + dims i * dims (k + 1) * dims (j + 1) = matrixChainOpt dims i j) |>.min' (by have h_nonempty : (Finset.Icc i (j - 1)).Nonempty := by use i; simp [Finset.mem_Icc]; omega let f (k : ℕ) := matrixChainOpt dims i k + matrixChainOpt dims (k + 1) j + dims i * dims (k + 1) * dims (j + 1) have h_eq : matrixChainOpt dims i j = (Finset.Icc i (j - 1)).inf' h_nonempty f := bridge_attach_inf dims i j h have h_exists := exists_inf'_eq (Finset.Icc i (j - 1)) h_nonempty f rw [← h_eq] at h_exists rcases h_exists with ⟨k, hk, hk_eq⟩ exact ⟨k, Finset.mem_filter.mpr ⟨hk, hk_eq⟩⟩) else i
theorem matrixChainSplit_optimal (dims : Nat → Nat) (i j : Nat) (hij : i < j) : matrixChainSplit dims i j ∈ Finset.Icc i (j - 1) ∧ matrixChainOpt dims i j = matrixSplitCost dims (matrixChainOpt dims) i j (matrixChainSplit dims i j) := by let s : Finset ℕ := Finset.Icc i (j - 1) have h_nonempty : s.Nonempty := by use i; simp [s, Finset.mem_Icc]; omega let f (k : ℕ) := matrixChainOpt dims i k + matrixChainOpt dims (k + 1) j + dims i * dims (k + 1) * dims (j + 1) have h_opt_eq : matrixChainOpt dims i j = s.inf' h_nonempty f := bridge_attach_inf dims i j hij have h_exists : ∃ k ∈ s, f k = matrixChainOpt dims i j := by rw [h_opt_eq]; exact exists_inf'_eq s h_nonempty f have h_filter_nonempty : (s.filter fun k => f k = matrixChainOpt dims i j).Nonempty := by rcases h_exists with ⟨k, hk, hk_eq⟩ exact ⟨k, Finset.mem_filter.mpr ⟨hk, hk_eq⟩⟩ set k := (s.filter fun k => f k = matrixChainOpt dims i j).min' h_filter_nonempty with hk_def have hk_mem_filter : k ∈ s.filter fun k => f k = matrixChainOpt dims i j := by rw [hk_def]; exact Finset.min'_mem _ h_filter_nonempty have hk_mem : k ∈ s := (Finset.mem_filter.mp hk_mem_filter).1 have hk_eq : f k = matrixChainOpt dims i j := (Finset.mem_filter.mp hk_mem_filter).2 have h_split_val : matrixChainSplit dims i j = k := by unfold matrixChainSplit simp [hij, s, f, hk_def] rw [h_split_val] refine ⟨hk_mem, ?_⟩ unfold matrixSplitCost dsimp [f] at hk_eq rw [← hk_eq]theorem matrixChainOpt_splitOptimal (dims : Nat → Nat) : MatrixChainSplitOptimal dims (matrixChainOpt dims) (matrixChainSplit dims) := by refine ⟨?_, ?_⟩ · intro i; simp [matrixChainOpt] · intro i j hij; exact matrixChainSplit_optimal dims i j hijdef matrixChainReconstruct (dims : Nat → Nat) (i j : Nat) (hbound : i ≤ j) : ChainPlan i j := if h : i < j then let k := matrixChainSplit dims i j ChainPlan.split i k j (matrixChainReconstruct dims i k (by have hsplit := matrixChainSplit_optimal dims i j h rcases hsplit with ⟨hmem, _⟩ rcases Finset.mem_Icc.mp hmem with ⟨hlo, hhi⟩ omega)) (matrixChainReconstruct dims (k + 1) j (by have hsplit := matrixChainSplit_optimal dims i j h rcases hsplit with ⟨hmem, _⟩ rcases Finset.mem_Icc.mp hmem with ⟨hlo, hhi⟩ omega)) else have heq : i = j := by omega heq ▸ ChainPlan.single j termination_by j - i decreasing_by · have hsplit := matrixChainSplit_optimal dims i j h rcases hsplit with ⟨hmem, _⟩ rcases Finset.mem_Icc.mp hmem with ⟨hlo, _hhi⟩ omega · have hsplit := matrixChainSplit_optimal dims i j h rcases hsplit with ⟨hmem, _⟩ rcases Finset.mem_Icc.mp hmem with ⟨hlo, _hhi⟩ omega theorem matrixChainReconstruct_reconstructed (dims : Nat → Nat) (i j : Nat) (hbound : i ≤ j) : ChainPlan.ReconstructedBy (matrixChainSplit dims) (matrixChainReconstruct dims i j hbound) := by unfold matrixChainReconstruct split · next h => have hsplit := matrixChainSplit_optimal dims i j h rcases hsplit with ⟨hmem, _⟩ rcases Finset.mem_Icc.mp hmem with ⟨hlo, hhi⟩ have h_left_bound : i ≤ matrixChainSplit dims i j := by omega have h_right_bound : matrixChainSplit dims i j + 1 ≤ j := by omega simp refine ChainPlan.ReconstructedBy.split i (matrixChainSplit dims i j) j rfl (matrixChainReconstruct_reconstructed dims i (matrixChainSplit dims i j) (by omega)) (matrixChainReconstruct_reconstructed dims (matrixChainSplit dims i j + 1) j (by omega)) · next h => have heq : i = j := by omega cases heq exact ChainPlan.ReconstructedBy.single i termination_by j - i decreasing_by · omega · omegatheorem matrixChain_correct (dims : Nat → Nat) (i j : Nat) (hbound : i ≤ j) : ∃ plan : ChainPlan i j, MatrixChainOptimalPlan dims plan := by let plan := matrixChainReconstruct dims i j hbound refine ⟨plan, matrixChain_reconstructed_optimal (matrixChainOpt_lowerBound dims) (matrixChainOpt_splitOptimal dims) (matrixChainReconstruct_reconstructed dims i j hbound)⟩end Chapter15end CLRS
Imports
import Mathlib

14.3. Elements of Dynamic Programming

This section defines cache-value consistency and a finite set-cardinality inequality. Neither property alone proves that an algorithm computes a state only once.

The Execution companion supplies a separate executable guarantee: DPExecution.buildLayers appends stored rows in dependency order. Its invariant lifts any cell property whose premises concern earlier rows. Actual cell-write and candidate counters are accumulated during filling. Matrix-chain and optimal-BST executions instantiate this builder with their own stored cells and recurrence proofs; those are the concrete once-per-state clients.

The historical distinctCacheStates_le_length remains a cardinality fact, not an execution or cache-miss bound. MemoCacheConsistent describes value correctness only; its use does not silently assume memoized runtime.

Notation conventions used in this section:

  • State : the type of subproblem states

  • Value : the type of subproblem answers

  • cache : the memoization table State → Option Value

namespace CLRSnamespace Chapter15

The generic memo-cache invariant

A memoization cache is consistent when every stored value agrees with the ground-truth value function correct. This is the reusable cache-value invariant. Execution and cache-miss bounds require separate proofs.

def MemoCacheConsistent {State Value : Type} (correct : State → Value) (cache : State → Option Value) : Prop := ∀ s v, cache s = some v → v = correct s

A consistent cache that stores a value at a state agrees with the ground-truth value at that state.

theorem MemoCacheConsistent_eq {State Value : Type} {correct : State → Value} {cache : State → Option Value} (h : MemoCacheConsistent correct cache) {s : State} {v : Value} (hstore : cache s = some v) : v = correct s := h s v hstore

Cardinality of the cached states

The number of distinct states with a stored value among the supplied list. This definition inspects a completed cache; it says nothing about how often those states were evaluated while constructing that cache.

def distinctCacheStates {State : Type} [DecidableEq State] (cache : State → Option Value) (states : List State) : Nat := ((states.filter (fun s => (cache s).isSome)).toFinset).card

The distinct cached-state count is at most the supplied list length. This elementary cardinality inequality does not establish any once-per-state execution guarantee.

theorem distinctCacheStates_le_length {State : Type} [DecidableEq State] (cache : State → Option Value) (states : List State) : distinctCacheStates cache states ≤ states.length := by unfold distinctCacheStates calc ((states.filter (fun s => (cache s).isSome)).toFinset).card ≤ (states.filter (fun s => (cache s).isSome)).length := List.toFinset_card_le _ _ ≤ states.length := List.length_filter_le (fun s => (cache s).isSome) states
end Chapter15end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_14.Section_14_3_Elements_Of_Dynamic_Programming.Execution

Stored dynamic-programming layers

A row is built by appending each cell once. A table is built by appending each row once; the evaluator receives only previously completed rows. Returned write and candidate-visit counters are accumulated by these executions. Array access, arithmetic, and comparisons are unit-cost primitives; this is not a persistent-array copying or bit-operation runtime model.

namespace CLRS.Chapter15.DPExecutionstructure Row (α : Type*) where cells : Array α writes : Nat visits : Nat evaluatedIndices : List Natdef buildRow (f : Nat → α × Nat) : Nat → Row α | 0 => ⟨#[], 0, 0, []⟩ | n + 1 => let prev := buildRow f n let next := f n ⟨prev.cells.push next.1, prev.writes + 1, prev.visits + next.2, n :: prev.evaluatedIndices⟩@[simp] theorem buildRow_cells (f : Nat → α × Nat) (n : Nat) : (buildRow f n).cells = ((List.range n).map (fun i => (f i).1)).toArray := by induction n with | zero => rfl | succ n ih => simp [buildRow, ih, List.range_succ]@[simp] theorem buildRow_writes (f : Nat → α × Nat) (n : Nat) : (buildRow f n).writes = n := by induction n with | zero => rfl | succ n ih => simp [buildRow, ih]theorem buildRow_visits (f : Nat → α × Nat) (n : Nat) : (buildRow f n).visits = ∑ i ∈ Finset.range n, (f i).2 := by induction n with | zero => simp [buildRow] | succ n ih => simp [buildRow, ih, Finset.sum_range_succ]structure Table (α : Type*) where rows : Array (Array α) cellWrites : Nat candidateVisits : Nat evaluatedStates : List (Nat × Nat)

Total lookup; correctness theorems establish that algorithmic reads are in range.

def get [Inhabited α] (rows : Array (Array α)) (l i : Nat) : α := ((rows[l]?).getD #[])[i]?.getD default

Complete layers 0 through n-1. Each newly evaluated cell is stored once.

def buildLayers (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) : Nat → Table α | 0 => ⟨#[], 0, 0, []⟩ | n + 1 => let prev := buildLayers width step n let row := buildRow (step n prev.rows) (width n) ⟨prev.rows.push row.cells, prev.cellWrites + row.writes, prev.candidateVisits + row.visits, row.evaluatedIndices.map (fun i => (n,i)) ++ prev.evaluatedStates⟩
@[simp] theorem buildLayers_size (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n : Nat) : (buildLayers width step n).rows.size = n := by induction n with | zero => rfl | succ n ih => simp [buildLayers, ih]lemma get_push_old [Inhabited α] (rows : Array (Array α)) (row : Array α) (l i : Nat) (hl : l < rows.size) : get (rows.push row) l i = get rows l i := by simp [get, Array.getElem?_push, hl, Nat.ne_of_lt hl]lemma get_push_new [Inhabited α] (rows : Array (Array α)) (f : Nat → α × Nat) (n i : Nat) (hi : i < n) : get (rows.push (buildRow f n).cells) rows.size i = (f i).1 := by simp [get, hi]

Dependency-order invariant: every completed cell equals its specification. The local obligation uses only earlier rows; it does not assume a final table.

theorem buildLayers_correct [Inhabited α] (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (correct : Nat → Nat → α) (hstep : ∀ l rows, rows.size = l → (∀ k, k < l → ∀ i, i < width k → get rows k i = correct k i) → ∀ i, i < width l → (step l rows i).1 = correct l i) (n : Nat) : ∀ l, l < n → ∀ i, i < width l → get (buildLayers width step n).rows l i = correct l i := by induction n with | zero => intros; omega | succ n ih => intro l hl i hi by_cases heq : l = n · subst l have hn := buildLayers_size width step n have hg := get_push_new (buildLayers width step n).rows (step n (buildLayers width step n).rows) (width n) i hi rw [hn] at hg change get ((buildLayers width step n).rows.push _) n i = _ rw [hg] exact hstep n _ hn ih i hi · have hln : l < n := by omega change get ((buildLayers width step n).rows.push _) l i = _ rw [get_push_old _ _ l i (by simpa using hln)] exact ih l hln i hi
theorem buildLayers_property [Inhabited α] (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (P : Nat → Nat → α → Prop) (hstep : ∀ l rows, rows.size = l → (∀ k, k < l → ∀ i, i < width k → P k i (get rows k i)) → ∀ i, i < width l → P l i (step l rows i).1) (n : Nat) : ∀ l, l < n → ∀ i, i < width l → P l i (get (buildLayers width step n).rows l i) := by induction n with | zero => intros; omega | succ n ih => intro l hl i hi by_cases heq : l = n · subst l have hn := buildLayers_size width step n have hg := get_push_new (buildLayers width step n).rows (step n (buildLayers width step n).rows) (width n) i hi rw [hn] at hg change P n i (get ((buildLayers width step n).rows.push _) n i) rw [hg] exact hstep n _ hn ih i hi · have hln : l < n := by omega change P l i (get ((buildLayers width step n).rows.push _) l i) rw [get_push_old _ _ l i (by simpa using hln)] exact ih l hln i hi

Exact writes from actual row construction, not a distinct-state estimate.

theorem buildLayers_cellWrites (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n : Nat) : (buildLayers width step n).cellWrites = ∑ l ∈ Finset.range n, width l := by induction n with | zero => simp [buildLayers] | succ n ih => simp [buildLayers, ih, Finset.sum_range_succ]

Sum the actual candidate visits when the cell evaluator visits charge(l) candidates in each state of layer l.

theorem buildLayers_candidateVisits (width charge : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (hstep : ∀ l rows i, (step l rows i).2 = charge l) (n : Nat) : (buildLayers width step n).candidateVisits = ∑ l ∈ Finset.range n, width l * charge l := by induction n with | zero => simp [buildLayers] | succ n ih => simp [buildLayers, ih, buildRow_visits, hstep, Finset.sum_range_succ]

Minimum value, first minimizing index, and actual candidate visits.

structure Minimum where value : Nat index : Nat visits : Nat deriving Repr, DecidableEq

Scan the inclusive range start,…,start+extra once, retaining the earlier index when values tie. Each candidate is evaluated exactly once.

def minimum (f : Nat → Nat) (start : Nat) : Nat → Minimum | 0 => ⟨f start, start, 1⟩ | extra + 1 => let prev := minimum f start extra let value := f (start + extra + 1) if value < prev.value then ⟨value, start + extra + 1, prev.visits + 1⟩ else ⟨prev.value, prev.index, prev.visits + 1⟩
@[simp] theorem minimum_visits (f : Nat → Nat) (start extra : Nat) : (minimum f start extra).visits = extra + 1 := by induction extra with | zero => rfl | succ n ih => simp only [minimum]; split <;> simp_all

A scanned minimum is attained in range and below every candidate.

theorem minimum_spec (f : Nat → Nat) (start extra : Nat) : start ≤ (minimum f start extra).index ∧ (minimum f start extra).index ≤ start + extra ∧ (minimum f start extra).value = f (minimum f start extra).index ∧ ∀ k, start ≤ k → k ≤ start + extra → (minimum f start extra).value ≤ f k := by induction extra with | zero => change start ≤ start ∧ start ≤ start + 0 ∧ f start = f start ∧ _ refine ⟨le_rfl, le_rfl, rfl, ?_⟩ intro k hk hk' have he : k = start := by omega subst k exact le_rfl | succ n ih => rcases ih with ⟨hlo, hhi, heq, hmin⟩ simp only [minimum] split next h => dsimp only refine ⟨by omega, by omega, rfl, ?_⟩ intro k hk hk' by_cases he : k = start + n + 1 · subst k; exact le_rfl · exact (Nat.le_of_lt h).trans (hmin k hk (by omega)) next h => dsimp only refine ⟨hlo, by omega, heq, ?_⟩ intro k hk hk' by_cases he : k = start + n + 1 · subst k; omega · exact hmin k hk (by omega)

The minimum equals a proposed value once its lower-bound and witness obligations have been established for the actual scanned candidates.

theorem minimum_value_eq (f : Nat → Nat) (start extra v : Nat) (hlower : ∀ k, start ≤ k → k ≤ start + extra → v ≤ f k) (hwitness : ∃ k, start ≤ k ∧ k ≤ start + extra ∧ f k = v) : (minimum f start extra).value = v := by obtain ⟨hi, hi', heq, hmin⟩ := minimum_spec f start extra obtain ⟨k, hk, hk', he⟩ := hwitness have hl := hlower _ hi hi' have hu := hmin k hk hk' omega

The row for a state length has exactly the scheduled number of cells.

theorem buildLayers_row_size (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n l : Nat) (hl : l < n) : (((buildLayers width step n).rows[l]?).getD #[]).size = width l := by induction n with | zero => omega | succ n ih => by_cases he : l = n · subst l change (((buildLayers width step n).rows.push _)[n]?.getD #[]).size = _ simp only [Array.getElem?_push, buildLayers_size] simp · have hln : l < n := by omega change (((buildLayers width step n).rows.push _)[l]?.getD #[]).size = _ simp only [Array.getElem?_push, buildLayers_size, he, if_false] exact ih hln

Append-only evaluation creates one stored slot for every counted cell write. Earlier rows are never overwritten by later evaluations.

theorem buildLayers_writes_eq_stored (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n : Nat) : (buildLayers width step n).cellWrites = ((buildLayers width step n).rows.toList.map Array.size).sum := by induction n with | zero => rfl | succ n ih => simp [buildLayers, ih]

Extending the table preserves every previously stored cell.

theorem buildLayers_get_old [Inhabited α] (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n l i : Nat) (hl : l < n) : get (buildLayers width step (n+1)).rows l i = get (buildLayers width step n).rows l i := by apply get_push_old simpa using hl

Quadratic cell bound for inclusive intervals in 0,…,N.

theorem interval_cells_le_square (N : Nat) : (∑ l ∈ Finset.range (N+1), (N+1-l)) ≤ (N+1)^2 := by calc _ ≤ ∑ _l ∈ Finset.range (N+1), (N+1) := Finset.sum_le_sum (fun l _ => Nat.sub_le _ _) _ = _ := by simp [pow_two]

Cubic candidate bound for scans of all splits/roots of every interval.

theorem interval_visits_le_cube (N : Nat) : (∑ l ∈ Finset.range (N+1), (N+1-l)*l) ≤ (N+1)^3 := by calc _ ≤ ∑ _l ∈ Finset.range (N+1), (N+1)*(N+1) := by apply Finset.sum_le_sum intro l hl exact Nat.mul_le_mul (Nat.sub_le _ _) (by simpa using (Finset.mem_range.mp hl).le) _ = _ := by simp; ring
@[simp] theorem buildRow_indices (f : Nat → α × Nat) (n : Nat) : (buildRow f n).evaluatedIndices = (List.range n).reverse := by induction n with | zero => rfl | succ n ih => simp [buildRow, ih, List.range_succ]

Exact domain of the evaluation events emitted by the cell loops.

theorem buildLayers_evaluatedStates_mem (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n l i : Nat) : (l,i) ∈ (buildLayers width step n).evaluatedStates ↔ l < n ∧ i < width l := by induction n with | zero => simp [buildLayers] | succ n ih => simp only [buildLayers, buildRow_indices, List.mem_append, List.mem_map, List.mem_reverse, List.mem_range] rw [ih] constructor · rintro (⟨j, hj, he⟩ | ⟨hl, hi⟩) · cases he exact ⟨by omega, hj⟩ · exact ⟨by omega, hi⟩ · rintro ⟨hl, hi⟩ by_cases he : l = n · subst l exact Or.inl ⟨i, hi, rfl⟩ · exact Or.inr ⟨by omega, hi⟩

No state is evaluated twice. This is a theorem about the execution's actual emitted events; no distinct-state assumption is supplied by clients.

theorem buildLayers_evaluatedStates_nodup (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n : Nat) : (buildLayers width step n).evaluatedStates.Nodup := by induction n with | zero => simp [buildLayers] | succ n ih => simp only [buildLayers, buildRow_indices] rw [List.nodup_append] refine ⟨?_, ih, ?_⟩ · apply List.Nodup.map · intro a b h; exact Prod.mk.inj h |>.2 · exact List.nodup_reverse.mpr List.nodup_range · intro x hx y hy he subst y obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx have h := (buildLayers_evaluatedStates_mem width step n n i).mp hy omega

The write counter counts exactly the actual evaluation events.

theorem buildLayers_cellWrites_eq_events (width : Nat → Nat) (step : Nat → Array (Array α) → Nat → α × Nat) (n : Nat) : (buildLayers width step n).cellWrites = (buildLayers width step n).evaluatedStates.length := by induction n with | zero => rfl | succ n ih => simp [buildLayers, buildRow_indices, ih, Nat.add_comm]
theorem interval_cells_closed (N : Nat) : 2 * (∑ l ∈ Finset.range (N+1), (N+1-l)) = (N+1)*(N+2) := by induction N with | zero => norm_num | succ N ih => have hsum : (∑ l ∈ Finset.range (N+1), (N+2-l)) = (∑ l ∈ Finset.range (N+1), (N+1-l)) + (N+1) := by calc _ = ∑ l ∈ Finset.range (N+1), ((N+1-l)+1) := by apply Finset.sum_congr rfl intro l hl have := Finset.mem_range.mp hl omega _ = _ := by rw [Finset.sum_add_distrib]; simp rw [show N+1+1 = N+2 by omega, Finset.sum_range_succ, hsum] have he : N+2-(N+1)=1 := by omega rw [he] nlinarith theorem interval_visits_closed (N : Nat) : 6 * (∑ l ∈ Finset.range (N+1), (N+1-l)*l) = N*(N+1)*(N+2) := by induction N with | zero => norm_num | succ N ih => have hsum : (∑ l ∈ Finset.range (N+1), (N+2-l)*l) = (∑ l ∈ Finset.range (N+1), (N+1-l)*l) + (∑ l ∈ Finset.range (N+1), l) := by calc _ = ∑ l ∈ Finset.range (N+1), ((N+1-l)*l+l) := by apply Finset.sum_congr rfl intro l hl have hh := Finset.mem_range.mp hl have he : N+2-l = N+1-l+1 := by omega rw [he]; ring _ = _ := Finset.sum_add_distrib rw [show N+1+1 = N+2 by omega, Finset.sum_range_succ, hsum] have htri := Finset.sum_range_id_mul_two (N+1) simp only [Nat.add_sub_cancel] at htri have he : N+2-(N+1)=1 := by omega rw [he] nlinarithend CLRS.Chapter15.DPExecution
Imports
import CLRSLean.FourthEdition.Chapter_14.Section_14_4_Longest_Common_Subsequence.Tabulation

14.4. Longest Common Subsequence

The public CLRS.­Chapter15.­lcsLengthTabulated computes rolling rows from stored predecessors. Its row invariant proves equality with the legacy recursive specification CLRS.­Chapter15.­lcsLength. The executed cell counter is exactly (m + 1)(n + 1); for positive lengths it lies between mn and 4mn.

Each cell uses constant many list/head, arithmetic, and equality operations. This is a cell-operation bound, excluding equality internals, allocation, and call-stack costs. The returned row has n + 1 entries; no peak-memory theorem is claimed. The legacy reconstruction is functionally correct but still uses the recursive length oracle, so its runtime is not bounded by this counter.

Main results:

Notation conventions used in this section:

  • xs, ys : the two input sequences

  • m, n : their lengths

namespace CLRSnamespace Chapter15

The Θ(mn) table bound

The number of table entries of the bottom-up LCS table: one cell for each prefix pair (i, j) with 0 ≤ i ≤ m and 0 ≤ j ≤ n.

def lcsTableCells (m n : Nat) : Nat := (m + 1) * (n + 1)

The LCS table has (m + 1)(n + 1) entries.

theorem lcsTableCells_eq (m n : Nat) : lcsTableCells m n = (m + 1) * (n + 1) := rfl

Arithmetic upper bound for the number of visited cells. Execution is linked to this formula by lcsExecution_cells_eq_tableCells below.

theorem lcsTableCells_le_four_mn (m n : Nat) (hm : 1 ≤ m) (hn : 1 ≤ n) : lcsTableCells m n ≤ 4 * m * n := by unfold lcsTableCells have h1 : m + 1 ≤ 2 * m := by omega have h2 : n + 1 ≤ 2 * n := by omega calc (m + 1) * (n + 1) ≤ (2 * m) * (2 * n) := Nat.mul_le_mul h1 h2 _ = 4 * m * n := by ring

Connect the dimension formula to the counter carried by the row execution.

theorem lcsExecution_cells_eq_tableCells [DecidableEq α] (xs ys : List α) : (LCSTabulation.execute xs ys).cells = lcsTableCells xs.length ys.length := LCSTabulation.execute_cells xs ys

Matching product bounds for the actual cell visits, for nonempty inputs.

theorem lcsExecution_cells_bounds [DecidableEq α] (xs ys : List α) (hx : 1 ≤ xs.length) (hy : 1 ≤ ys.length) : xs.length * ys.length ≤ (LCSTabulation.execute xs ys).cells ∧ (LCSTabulation.execute xs ys).cells ≤ 4 * xs.length * ys.length := by rw [lcsExecution_cells_eq_tableCells] exact ⟨Nat.mul_le_mul (Nat.le_succ _) (Nat.le_succ _), lcsTableCells_le_four_mn _ _ hx hy⟩
end Chapter15end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_14.Section_14_4_Longest_Common_Subsequence.Tabulation

LCS by computed rows

Process suffixes from the end of each input. Each row uses the already computed next row and the completed suffix of its own row. Executable code only reads list heads/tails and stored numbers; it never calls the recursive LCS oracle. The invariant identifies every entry of a completed row, not just its first entry. The counter records one visit per boundary or interior cell.

The returned table is a rolling row. Persistent list storage and call-stack allocation are not modeled as machine costs; each cell uses at most one equality test and constant many arithmetic/list operations. Reconstruction from this rolling table is a separate algorithmic layer.

namespace CLRS.Chapter15.LCSTabulationstructure Row where values : List Nat cells : Nat deriving Repr

Proof-only interpretation of all suffix entries in one row.

def specification [DecidableEq α] (xs : List α) : List α → List Nat | [] => [0] | y :: ys => lcsLength xs (y :: ys) :: specification xs ys
theorem specification_head [DecidableEq α] (xs ys : List α) : (specification xs ys).headD 0 = lcsLength xs ys := by cases ys with | nil => cases xs <;> simp [specification, lcsLength] | cons y ys => rfl

Initialize the empty-input row, visiting every boundary cell once.

def initial : List α → Row | [] => ⟨[0], 1⟩ | _ :: ys => let rest := initial ys; ⟨0 :: rest.values, rest.cells + 1⟩
theorem initial_values [DecidableEq α] (ys : List α) : (initial ys).values = specification ([] : List α) ys := by induction ys with | nil => rfl | cons y ys ih => simp [initial, specification, lcsLength, ih]theorem initial_cells (ys : List α) : (initial ys).cells = ys.length + 1 := by induction ys with | nil => rfl | cons y ys ih => simp [initial, ih]

Compute one row using only three stored predecessors per interior cell.

def nextRow [DecidableEq α] (x : α) : List α → List Nat → Row | [], _ => ⟨[0], 1⟩ | y :: ys, below => let rest := nextRow x ys below.tail let v := if x = y then below.tail.headD 0 + 1 else max (below.headD 0) (rest.values.headD 0) ⟨v :: rest.values, rest.cells + 1⟩

Every newly computed cell satisfies the LCS specification for its suffix.

theorem nextRow_values [DecidableEq α] (x : α) (xs ys : List α) : (nextRow x ys (specification xs ys)).values = specification (x :: xs) ys := by induction ys with | nil => rfl | cons y ys ih => simp only [nextRow, specification, List.tail_cons, List.headD_cons, ih] simp only [specification_head, lcsLength]
theorem nextRow_cells [DecidableEq α] (x : α) (ys : List α) (below : List Nat) : (nextRow x ys below).cells = ys.length + 1 := by induction ys generalizing below with | nil => rfl | cons y ys ih => simp [nextRow, ih]

Dynamic programming: compute a row once and pass its stored values to its predecessor.

def execute [DecidableEq α] : List α → List α → Row | [], ys => initial ys | x :: xs, ys => let below := execute xs ys let current := nextRow x ys below.values ⟨current.values, below.cells + current.cells⟩
theorem execute_row [DecidableEq α] (xs ys : List α) : (execute xs ys).values = specification xs ys := by induction xs with | nil => exact initial_values ys | cons x xs ih => simp only [execute, ih, nextRow_values]

The count comes from the actual row loops, including both boundary edges.

theorem execute_cells [DecidableEq α] (xs ys : List α) : (execute xs ys).cells = (xs.length + 1) * (ys.length + 1) := by induction xs with | nil => simp [execute, initial_cells] | cons x xs ih => simp only [execute, ih, nextRow_cells, List.length_cons] ring
theorem specification_length [DecidableEq α] (xs ys : List α) : (specification xs ys).length = ys.length + 1 := by induction ys with | nil => rfl | cons y ys ih => simp [specification, ih]

The returned row has only one entry per suffix of the second sequence.

theorem execute_row_length [DecidableEq α] (xs ys : List α) : (execute xs ys).values.length = ys.length + 1 := by rw [execute_row, specification_length]
end CLRS.Chapter15.LCSTabulationnamespace CLRS.Chapter15

The public tabulated length reads the first entry of the computed rolling row.

def lcsLengthTabulated [DecidableEq α] (xs ys : List α) : Nat := (LCSTabulation.execute xs ys).values.headD 0
theorem lcsLengthTabulated_correct [DecidableEq α] (xs ys : List α) : lcsLengthTabulated xs ys = lcsLength xs ys := by rw [lcsLengthTabulated, LCSTabulation.execute_row, LCSTabulation.specification_head] theorem lcsLengthTabulated_upper_bound [DecidableEq α] (xs ys zs : List α) (h : IsCommonSubsequence xs ys zs) : zs.length ≤ lcsLengthTabulated xs ys := by rw [lcsLengthTabulated_correct] exact lcsLength_upper_bound hend CLRS.Chapter15

CLRSLean.Chapter_15.Section_15_4_Longest_Common_Subsequence

CLRS Section 15.4 - Longest common subsequence

This section formalizes the CLRS longest-common-subsequence dynamic program. It defines the mathematical LCS certificate, a recursive evaluation of the recurrence, and a reconstruction procedure using that recursive evaluator. The main theorem proves that the reconstructed sequence is indeed a longest common subsequence.

Main results:

  • Theorem lcsLength_recurrence: the executable length function satisfies the CLRS recurrence.

  • Theorem lcsLength_upper_bound: every common subsequence has length at most the table entry.

  • Theorem lcsReconstruct_length_eq: the reconstructed sequence's length equals the computed table entry.

  • Theorem lcsReconstruct_common: the reconstructed sequence is a common subsequence of both inputs.

  • Theorem lcs_correct: there exists a longest common subsequence, and the reconstruction procedure computes one.

Status: proved for the functional LCS correctness layer.

Deferred refinements:

  • This length evaluator repeats subproblems; its recurrence correctness does not establish a polynomial runtime. Fourth-edition §14.4 provides a separate rolling-row execution with an exact cell counter. Reconstruction here still uses this recursive evaluator and has no quadratic runtime claim.

namespace CLRSnamespace Chapter15

A sequence is common to xs and ys when it is a subsequence of both.

def IsCommonSubsequence {α : Type u} (xs ys zs : List α) : Prop := List.Sublist zs xs ∧ List.Sublist zs ys

A certificate that seq is a longest common subsequence of two lists.

structure LCSCertificate {α : Type u} (xs ys : List α) where seq : List α common : IsCommonSubsequence xs ys seq optimal : ∀ zs, IsCommonSubsequence xs ys zs → zs.length ≤ seq.length
namespace LCSCertificatevariable {α : Type u} {xs ys : List α}

The length certified by an LCS certificate.

def length (cert : LCSCertificate xs ys) : Nat := cert.seq.length

The certified sequence is a common subsequence.

theorem seq_common (cert : LCSCertificate xs ys) : IsCommonSubsequence xs ys cert.seq := cert.common

Every common subsequence has length at most the certified LCS length.

theorem commonSubsequence_length_le (cert : LCSCertificate xs ys) {zs : List α} (hzs : IsCommonSubsequence xs ys zs) : zs.length ≤ cert.length := by exact cert.optimal zs hzs

Any two LCS certificates for the same inputs certify the same length.

theorem length_eq_of_certificates (left right : LCSCertificate xs ys) : left.length = right.length := by apply le_antisymm · exact commonSubsequence_length_le right left.common · exact commonSubsequence_length_le left right.common
end LCSCertificate

Swapping the two input sequences preserves common-subsequence status.

theorem isCommonSubsequence_comm {xs ys zs : List α} : IsCommonSubsequence xs ys zs ↔ IsCommonSubsequence ys xs zs := by constructor · intro h; exact ⟨h.2, h.1⟩ · intro h; exact ⟨h.2, h.1⟩
Table recurrence certificate

The CLRS LCS dynamic-programming recurrence for a supplied table. The table is indexed by the remaining suffixes of the two input lists.

def LCSTableRecurrence {α : Type u} [DecidableEq α] (table : List α → List α → Nat) : Prop := (∀ ys, table [] ys = 0) ∧ (∀ xs, table xs [] = 0) ∧ ∀ a xs b ys, table (a :: xs) (b :: ys) = if a = b then table xs ys + 1 else max (table xs (b :: ys)) (table (a :: xs) ys)
namespace LCSTableRecurrencevariable {α : Type u} [DecidableEq α]variable {table : List α → List α → Nat}

The empty-left boundary row of an LCS table is zero.

theorem nil_left (h : LCSTableRecurrence table) (ys : List α) : table [] ys = 0 := h.1 ys

The empty-right boundary column of an LCS table is zero.

theorem nil_right (h : LCSTableRecurrence table) (xs : List α) : table xs [] = 0 := h.2.1 xs

The cons/cons recurrence in its raw conditional form.

theorem cons_cons (h : LCSTableRecurrence table) (a : α) (xs : List α) (b : α) (ys : List α) : table (a :: xs) (b :: ys) = if a = b then table xs ys + 1 else max (table xs (b :: ys)) (table (a :: xs) ys) := h.2.2 a xs b ys

Matching heads use the diagonal table entry plus one.

theorem cons_cons_of_eq (h : LCSTableRecurrence table) {a b : α} (hab : a = b) (xs ys : List α) : table (a :: xs) (b :: ys) = table xs ys + 1 := by simpa [hab] using h.cons_cons a xs b ys

Equal heads use the diagonal table entry plus one.

theorem cons_cons_self (h : LCSTableRecurrence table) (a : α) (xs ys : List α) : table (a :: xs) (a :: ys) = table xs ys + 1 := by exact h.cons_cons_of_eq rfl xs ys

Matching heads strictly increase the diagonal subproblem value.

theorem diagonal_lt_cons_cons_of_eq (h : LCSTableRecurrence table) {a b : α} (hab : a = b) (xs ys : List α) : table xs ys < table (a :: xs) (b :: ys) := by rw [h.cons_cons_of_eq hab xs ys] omega

Distinct heads use the maximum of the two one-sided subproblems.

theorem cons_cons_of_ne (h : LCSTableRecurrence table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table (a :: xs) (b :: ys) = max (table xs (b :: ys)) (table (a :: xs) ys) := by simpa [hab] using h.cons_cons a xs b ys

In the nonmatching-head case, dropping the left head gives a lower subproblem.

theorem drop_left_le_of_ne (h : LCSTableRecurrence table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table xs (b :: ys) ≤ table (a :: xs) (b :: ys) := by rw [h.cons_cons_of_ne hab xs ys] exact Nat.le_max_left _ _

In the nonmatching-head case, dropping the right head gives a lower subproblem.

theorem drop_right_le_of_ne (h : LCSTableRecurrence table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table (a :: xs) ys ≤ table (a :: xs) (b :: ys) := by rw [h.cons_cons_of_ne hab xs ys] exact Nat.le_max_right _ _
end LCSTableRecurrence

A certified LCS table satisfies the CLRS recurrence and bounds the length of every common subsequence from above.

structure LCSTableCertificate {α : Type u} [DecidableEq α] (table : List α → List α → Nat) where recurrence : LCSTableRecurrence table upper_bound : ∀ {xs ys zs : List α}, IsCommonSubsequence xs ys zs → zs.length ≤ table xs ys
namespace LCSTableCertificatevariable {α : Type u} [DecidableEq α]variable {table : List α → List α → Nat}

A table certificate supplies the global upper bound promised by the table.

theorem commonSubsequence_length_le (cert : LCSTableCertificate table) {xs ys zs : List α} (hzs : IsCommonSubsequence xs ys zs) : zs.length ≤ table xs ys := cert.upper_bound hzs

A certified table has a zero empty-left boundary row.

theorem nil_left (cert : LCSTableCertificate table) (ys : List α) : table [] ys = 0 := by exact cert.recurrence.nil_left ys

A certified table has a zero empty-right boundary column.

theorem nil_right (cert : LCSTableCertificate table) (xs : List α) : table xs [] = 0 := by exact cert.recurrence.nil_right xs

A certified table satisfies the raw cons/cons CLRS recurrence.

theorem cons_cons (cert : LCSTableCertificate table) (a : α) (xs : List α) (b : α) (ys : List α) : table (a :: xs) (b :: ys) = if a = b then table xs ys + 1 else max (table xs (b :: ys)) (table (a :: xs) ys) := by exact cert.recurrence.cons_cons a xs b ys

In a certified table, matching heads use the diagonal entry plus one.

theorem cons_cons_of_eq (cert : LCSTableCertificate table) {a b : α} (hab : a = b) (xs ys : List α) : table (a :: xs) (b :: ys) = table xs ys + 1 := by exact cert.recurrence.cons_cons_of_eq hab xs ys

In a certified table, equal heads use the diagonal entry plus one.

theorem cons_cons_self (cert : LCSTableCertificate table) (a : α) (xs ys : List α) : table (a :: xs) (a :: ys) = table xs ys + 1 := by exact cert.recurrence.cons_cons_self a xs ys

In a certified table, matching heads strictly increase the diagonal subproblem value.

theorem diagonal_lt_cons_cons_of_eq (cert : LCSTableCertificate table) {a b : α} (hab : a = b) (xs ys : List α) : table xs ys < table (a :: xs) (b :: ys) := by exact cert.recurrence.diagonal_lt_cons_cons_of_eq hab xs ys

In a certified table, distinct heads use the maximum one-sided entry.

theorem cons_cons_of_ne (cert : LCSTableCertificate table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table (a :: xs) (b :: ys) = max (table xs (b :: ys)) (table (a :: xs) ys) := by exact cert.recurrence.cons_cons_of_ne hab xs ys

In a certified table, dropping the left head is bounded by the nonmatching case.

theorem drop_left_le_of_ne (cert : LCSTableCertificate table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table xs (b :: ys) ≤ table (a :: xs) (b :: ys) := by exact cert.recurrence.drop_left_le_of_ne hab xs ys

In a certified table, dropping the right head is bounded by the nonmatching case.

theorem drop_right_le_of_ne (cert : LCSTableCertificate table) {a b : α} (hab : a ≠ b) (xs ys : List α) : table (a :: xs) ys ≤ table (a :: xs) (b :: ys) := by exact cert.recurrence.drop_right_le_of_ne hab xs ys
end LCSTableCertificate

If a reconstructed common subsequence has exactly the value stored in a certified LCS table, then no common subsequence is longer.

theorem lcsTable_reconstruction_optimal {α : Type u} [DecidableEq α] {table : List α → List α → Nat} (cert : LCSTableCertificate table) {xs ys seq : List α} (hlen : seq.length = table xs ys) : ∀ zs, IsCommonSubsequence xs ys zs → zs.length ≤ seq.length := by intro zs hzs calc zs.length ≤ table xs ys := cert.commonSubsequence_length_le hzs _ = seq.length := hlen.symm

If a reconstructed common subsequence has exactly the value stored in a certified LCS table, then it packages as an LCS certificate.

def lcsCertificate_of_table_reconstruction {α : Type u} [DecidableEq α] {table : List α → List α → Nat} (cert : LCSTableCertificate table) {xs ys seq : List α} (hcommon : IsCommonSubsequence xs ys seq) (hlen : seq.length = table xs ys) : LCSCertificate xs ys where seq := seq common := hcommon optimal := lcsTable_reconstruction_optimal cert hlen

The LCS certificate produced from a table reconstruction certifies exactly the table entry as its length.

theorem lcsCertificate_of_table_reconstruction_length {α : Type u} [DecidableEq α] {table : List α → List α → Nat} (cert : LCSTableCertificate table) {xs ys seq : List α} (hcommon : IsCommonSubsequence xs ys seq) (hlen : seq.length = table xs ys) : (lcsCertificate_of_table_reconstruction cert hcommon hlen).length = table xs ys := by simpa [lcsCertificate_of_table_reconstruction, LCSCertificate.length] using hlen
Bottom-up LCS length computation

Recursive evaluation of the CLRS LCS recurrence. Unequal heads branch into two calls, repeating subproblems. This is a functional specification, not tabulation; the separately defined lcsLengthTabulated uses stored row entries.

def lcsLength {α : Type u} [DecidableEq α] : List α → List α → Nat | [], _ => 0 | _, [] => 0 | a :: xs, b :: ys => if a = b then lcsLength xs ys + 1 else max (lcsLength xs (b :: ys)) (lcsLength (a :: xs) ys)

lcsLength satisfies the CLRS LCS table recurrence.

theorem lcsLength_recurrence {α : Type u} [DecidableEq α] : LCSTableRecurrence (lcsLength (α := α)) := by refine ⟨?_, ?_, ?_⟩ · intro ys; simp [lcsLength] · intro xs; cases xs <;> simp [lcsLength] · intro a xs b ys; simp [lcsLength]
private lemma sublist_of_cons_sublist {α : Type u} {a : α} {l m : List α} (h : List.Sublist (a :: l) m) : List.Sublist l m := by cases h case cons h' => have ih := sublist_of_cons_sublist h' exact ih.cons _ case cons_cons h' => exact h'.cons a

Any common subsequence is bounded by lcsLength. The proof uses Nat strong induction on |xs| + |ys| and case analysis via List.cons_sublist_cons' to avoid dependent pattern matching on List.Sublist.

theorem lcsLength_upper_bound {α : Type u} [DecidableEq α] {xs ys zs : List α} (h : IsCommonSubsequence xs ys zs) : zs.length ≤ lcsLength xs ys := by obtain ⟨hsub_xs, hsub_ys⟩ := h let P (n : ℕ) : Prop := ∀ (xs ys zs : List α), xs.length + ys.length = n → List.Sublist zs xs → List.Sublist zs ys → zs.length ≤ lcsLength xs ys have hP : ∀ n, (∀ m < n, P m) → P n := by intro n ih xs ys zs hn hsub_xs hsub_ys match xs, ys with | [], _ => cases hsub_xs; simp [lcsLength] | _, [] => cases hsub_ys; simp [This simp argument is unused: lcsLength Hint: Omit it from the simp argument list. simp ̵[̵l̵c̵s̵L̵e̵n̵g̵t̵h̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`lcsLength] | a :: xs', b :: ys' => match zs with | [] => simp [lcsLength] | z :: zs' => have hx_cases := (List.cons_sublist_cons' (a := z) (b := a) (l₁ := zs') (l₂ := xs')).mp hsub_xs rcases hx_cases with (hx_skip | ⟨hz_eq_a, hx_match⟩) · -- Skip a in first list: (z :: zs') <+ xs' by_cases hab : a = b · subst hab have hy_cases' := (List.cons_sublist_cons' (a := z) (b := a) (l₁ := zs') (l₂ := ys')).mp hsub_ys rcases hy_cases' with (hy_skip' | ⟨hz_eq_a', hy_match'⟩) · -- (z :: zs') <+ ys': common subseq of xs', ys' have h_lt : xs'.length + ys'.length < n := by have h_lt' : xs'.length + ys'.length < (a :: xs').length + (a :: ys').length := by calc xs'.length + ys'.length < xs'.length + ys'.length + 2 := by omega _ = (xs'.length + 1) + (ys'.length + 1) := by omega _ = (a :: xs').length + (a :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih (xs'.length + ys'.length) h_lt xs' ys' (z :: zs') rfl hx_skip hy_skip' simpa [lcsLength] using hlen.trans (Nat.le_add_right _ 1) · -- z = a and zs' <+ ys' rw [hz_eq_a'] at * have hsub_tail : List.Sublist zs' xs' := sublist_of_cons_sublist hx_skip have h_lt : xs'.length + ys'.length < n := by have h_lt' : xs'.length + ys'.length < (a :: xs').length + (a :: ys').length := by calc xs'.length + ys'.length < xs'.length + ys'.length + 2 := by omega _ = (xs'.length + 1) + (ys'.length + 1) := by omega _ = (a :: xs').length + (a :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih (xs'.length + ys'.length) h_lt xs' ys' zs' rfl hsub_tail hy_match' simpa [lcsLength, List.length_cons] using Nat.add_le_add_right hlen 1 · -- a ≠ b have h_lt : xs'.length + (b :: ys').length < n := by have h_lt' : xs'.length + (b :: ys').length < (a :: xs').length + (b :: ys').length := by calc xs'.length + (b :: ys').length < (xs'.length + (b :: ys').length) + 1 := by omega _ = (xs'.length + 1) + (b :: ys').length := by omega _ = (a :: xs').length + (b :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih (xs'.length + (b :: ys').length) h_lt xs' (b :: ys') (z :: zs') rfl hx_skip hsub_ys simpa [lcsLength, hab] using hlen.trans (Nat.le_max_left _ _) · -- z = a and zs' <+ xs' rw [hz_eq_a] at hsub_ys ⊢ have hy_cases := (List.cons_sublist_cons' (a := a) (b := b) (l₁ := zs') (l₂ := ys')).mp hsub_ys rcases hy_cases with (hy_skip | ⟨ha_eq_b, hy_match⟩) · -- (a :: zs') <+ ys' (skip b) by_cases hab : a = b · subst hab have hsub_tail : List.Sublist zs' ys' := sublist_of_cons_sublist hy_skip have h_lt : xs'.length + ys'.length < n := by have h_lt' : xs'.length + ys'.length < (a :: xs').length + (a :: ys').length := by calc xs'.length + ys'.length < xs'.length + ys'.length + 2 := by omega _ = (xs'.length + 1) + (ys'.length + 1) := by omega _ = (a :: xs').length + (a :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih (xs'.length + ys'.length) h_lt xs' ys' zs' rfl hx_match hsub_tail simpa [lcsLength, List.length_cons] using Nat.add_le_add_right hlen 1 · -- a ≠ b have h_lt : (a :: xs').length + ys'.length < n := by have h_lt' : (a :: xs').length + ys'.length < (a :: xs').length + (b :: ys').length := by calc (a :: xs').length + ys'.length < (a :: xs').length + ys'.length + 1 := by omega _ = (a :: xs').length + (ys'.length + 1) := by omega _ = (a :: xs').length + (b :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih ((a :: xs').length + ys'.length) h_lt (a :: xs') ys' (a :: zs') rfl (List.Sublist.cons_cons a hx_match) hy_skip simpa [lcsLength, hab] using hlen.trans (Nat.le_max_right _ _) · -- a = b, zs' <+ ys' subst ha_eq_b have h_lt : xs'.length + ys'.length < n := by have h_lt' : xs'.length + ys'.length < (a :: xs').length + (a :: ys').length := by calc xs'.length + ys'.length < xs'.length + ys'.length + 2 := by omega _ = (xs'.length + 1) + (ys'.length + 1) := by omega _ = (a :: xs').length + (a :: ys').length := by simp exact lt_of_lt_of_eq h_lt' hn have hlen := ih (xs'.length + ys'.length) h_lt xs' ys' zs' rfl hx_match hy_match simpa [lcsLength, List.length_cons] using Nat.add_le_add_right hlen 1 let n := xs.length + ys.length have h_result : P n := Nat.strong_induction_on n hP exact h_result xs ys zs rfl hsub_xs hsub_ys

lcsLength paired with its upper-bound proof forms a certified LCS table.

Definition `lcsTable_certificate` is a proposition; use `theorem` instead of `def` Note: This linter can be disabled with `set_option linter.defProp false` def lcsTable_certificate {α : Type u} [DecidableEq α] : LCSTableCertificate (lcsLength (α := α)) where recurrence := lcsLength_recurrence upper_bound := lcsLength_upper_bound
Executable LCS reconstruction

Trace back through the computed length table to reconstruct one longest common subsequence. The reconstruction follows the CLRS textbook procedure: start from lcsLength xs ys and, at each step, decide whether the current characters match (emit the character) or whether the length came from the left or upper subproblem.

def lcsReconstruct {α : Type u} [DecidableEq α] : List α → List α → List α | [], _ => [] | _, [] => [] | a :: xs, b :: ys => if a = b then a :: lcsReconstruct xs ys else if lcsLength xs (b :: ys) ≥ lcsLength (a :: xs) ys then lcsReconstruct xs (b :: ys) else lcsReconstruct (a :: xs) ys

The reconstruction produces a sequence whose length equals the table entry.

theorem lcsReconstruct_length_eq {α : Type u} [DecidableEq α] (xs ys : List α) : (lcsReconstruct xs ys).length = lcsLength xs ys := by induction xs generalizing ys with | nil => simp [lcsReconstruct, lcsLength] | cons a xs ih_xs => induction ys with | nil => simp [lcsReconstruct, lcsLength] | cons b ys ih_ys => simp [lcsReconstruct, lcsLength] by_cases hab : a = b · subst hab; simp; simp [ih_xs ys] · simp [hab] split · next hge => have h_max : max (lcsLength xs (b :: ys)) (lcsLength (a :: xs) ys) = lcsLength xs (b :: ys) := Nat.max_eq_left hge rw [h_max] simp [ih_xs (b :: ys)] · next hlt => have h_max : max (lcsLength xs (b :: ys)) (lcsLength (a :: xs) ys) = lcsLength (a :: xs) ys := Nat.max_eq_right (Nat.le_of_lt (Nat.lt_of_not_ge hlt)) rw [h_max] simp [ih_ys]

The reconstructed sequence is a common subsequence of both inputs.

theorem lcsReconstruct_common {α : Type u} [DecidableEq α] (xs ys : List α) : IsCommonSubsequence xs ys (lcsReconstruct xs ys) := by induction xs generalizing ys with | nil => simp [lcsReconstruct, IsCommonSubsequence] | cons a xs ih_xs => induction ys with | nil => simp [lcsReconstruct, IsCommonSubsequence] | cons b ys ih_ys => simp [lcsReconstruct, IsCommonSubsequence] by_cases hab : a = b · subst hab obtain ⟨hx, hy⟩ := ih_xs ys have hpair : List.Sublist (a :: lcsReconstruct xs ys) (a :: xs) ∧ List.Sublist (a :: lcsReconstruct xs ys) (a :: ys) := ⟨List.Sublist.cons_cons a hx, List.Sublist.cons_cons a hy⟩ simpa [lcsReconstruct, IsCommonSubsequence] using hpair · simp [hab] split · next => obtain ⟨hx, hy⟩ := ih_xs (b :: ys) exact ⟨List.Sublist.cons a hx, hy⟩ · next => obtain ⟨hx, hy⟩ := ih_ys exact ⟨hx, List.Sublist.cons b hy⟩

Theorem (LCS correctness). There exists a longest common subsequence of xs and ys, and the executable reconstruction procedure computes one such sequence. This corresponds to the CLRS LCS optimal-substructure theorem (Theorem 15.1).

theorem lcs_correct {α : Type u} [DecidableEq α] (xs ys : List α) : ∃ seq : List α, IsCommonSubsequence xs ys seq ∧ ∀ zs, IsCommonSubsequence xs ys zs → zs.length ≤ seq.length := by refine ⟨lcsReconstruct xs ys, ?_, ?_⟩ · exact lcsReconstruct_common xs ys · intro zs hzs calc zs.length ≤ lcsLength xs ys := lcsLength_upper_bound hzs _ = (lcsReconstruct xs ys).length := (lcsReconstruct_length_eq xs ys).symm
end Chapter15end CLRS
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 + wdef 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

Scope and implementation notes

Imports
import CLRSLean.FourthEdition.Chapter_14.Section_14_2_Matrix_Chain_Multiplication.Execution import CLRSLean.FourthEdition.Chapter_14.Section_14_3_Elements_Of_Dynamic_Programming.Execution import CLRSLean.FourthEdition.Chapter_14.Section_14_5_Optimal_Binary_Search_Trees.Execution import CLRSLean.Chapter_15 import CLRSLean.FourthEdition.Chapter_14.Section_14_1_Rod_Cutting import CLRSLean.FourthEdition.Chapter_14.Section_14_2_Matrix_Chain_Multiplication import CLRSLean.FourthEdition.Chapter_14.Section_14_3_Elements_Of_Dynamic_Programming import CLRSLean.FourthEdition.Chapter_14.Section_14_4_Longest_Common_Subsequence import CLRSLean.FourthEdition.Chapter_14.Section_14_5_Optimal_Binary_Search_Trees

Current source

Sections 14.1–14.5 separate mathematical recurrences from stored-state executions with correctness and actual event counters:

  • Section 14.1 — Rod cutting: optimal-cut reconstruction and top-down cache-value correctness; a counted bottom-up array fill performs exactly n(n+1)/2 candidate evaluations and n+1 writes. This counter does not measure the separate top-down evaluator.

  • Section 14.2 — Matrix-chain multiplication: actual interval rows of costs/splits, stored-split reconstruction, recurrence refinement, and executed cell/candidate counters.

  • Section 14.3 — Elements of dynamic programming: a reusable append-only row builder, dependency-order invariant, and counters, instantiated by matrix-chain and optimal BST. The older distinct-cache cardinality inequality alone is not an execution guarantee.

  • Section 14.4 — Longest common subsequence: rolling-row length computation equal to the recursive specification, with exactly (m+1)(n+1) visited cells and a returned row of length n+1. Legacy reconstruction still uses the recursive oracle and has no such time bound.

  • Section 14.5 — Optimal binary search trees: stored cost/weight/root rows, cached weight updates, and reconstruction from stored roots, for nonnegative integer weights (not general real probabilities).

Declarations keep their legacy CLRS.Chapter15 namespaces; the third-edition-numbered imports CLRSLean.Chapter_15 and CLRSLean.Chapter_15.Section_15_* forward to these sources during the compatibility period.

Coverage boundary

The counted executions operate on stored predecessors, with constant many primitive operations per visited cell/candidate. The cost model excludes allocation/copying internals, key equality internals, and arithmetic bit costs. The legacy recursive functions remain mathematical reference specifications; their value correctness does not establish tabulated runtime. Cell counts and stored row sizes are not peak-memory or call-stack bounds.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 14 of 35