Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 14. Dynamic Programming
  4. 14.1. Rod Cutting
Browse chapters
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