Rod cutting

DefinitionRevenue of a rod composition#✓fully proved

Let \(p = (p_0, \dots, p_{n-1})\) be a price vector with entries in an additive commutative monoid, where \(p_{\ell - 1}\) is the price of a piece of length \(\ell\). For \(k \le n\) and a composition \((b_1, \dots, b_m)\) of \(k\) into positive parts, its revenue is \(p_{b_1 - 1} + \dots + p_{b_m - 1}\), the total price of its pieces.

@[expose] public def compositionRevenue {α : Type u} [AddCommMonoid α] {n k : Nat}
    (prices : Vector α n) (parts : Composition k) (hk : k ≤ n) : α :=
  (parts.blocks.pmap
    (fun i (hi : 0 < i ∧ i ≤ n) => prices[i - 1]'(by omega))
    (fun i hi => ⟨parts.blocks_pos hi, (parts.blocks_le hi).trans hk⟩)).sum

Used by 11

Used byCorrectness of bottom-up rod cutting · Revenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing · Rod-cutting reconstruction is optimal · Reconstruction earns the final saved revenue · Saved revenues are optimal · The memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · Correctness of memoized rod cutting · Correctness of recursive CUT-ROD

TheoremThe empty rod earns nothing#✓fully proved

Let \(p = (p_1, \dots, p_n)\) be prices in an additive commutative monoid. Every composition of \(0\), namely the empty one, has revenue \(0\) with respect to \(p\).

@[simp] public theorem compositionRevenue_zero {α : Type u} [AddCommMonoid α] {n : Nat}
    (prices : Vector α n) (parts : Composition 0) :
    compositionRevenue prices parts (Nat.zero_le n) = 0

Uses 1 · Used by 7

Statement usesRevenue of a rod composition

Used byCorrectness of bottom-up rod cutting · Reconstruction earns the final saved revenue · Saved revenues are optimal · The memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · Correctness of memoized rod cutting · Correctness of recursive CUT-ROD

TheoremRevenue of an uncut rod#✓fully proved

Let \(p = (p_1, \dots, p_n)\) be prices in an additive commutative monoid, \(p_i\) being the price of a piece of length \(i\). For \(0 < k \le n\), the revenue of the one-part composition \((k)\) of \(k\) is \(p_k\).

@[simp] public theorem compositionRevenue_single {α : Type u} [AddCommMonoid α]
    {n k : Nat} (prices : Vector α n) (hk : k ≤ n) (hpos : 0 < k) :
    compositionRevenue prices (Composition.single k hpos) hk =
      prices[k - 1]'(by omega)

Uses 1 · Used by 7

Statement usesRevenue of a rod composition

Used byCorrectness of bottom-up rod cutting · Reconstruction earns the final saved revenue · Saved revenues are optimal · The memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · Correctness of memoized rod cutting · Correctness of recursive CUT-ROD

TheoremRevenue is additive under concatenation#✓fully proved

Let \(p = (p_1, \dots, p_n)\) be prices in an additive commutative monoid, and define the revenue of a composition \((b_1, \dots, b_m)\) of some \(k \le n\) to be \(p_{b_1} + \dots + p_{b_m}\). If \(c\) is a composition of \(k\) and \(d\) is a composition of \(l\) with \(k + l \le n\), then the revenue of their concatenation, a composition of \(k + l\), is the revenue of \(c\) plus the revenue of \(d\).

public theorem compositionRevenue_append {α : Type u} [AddCommMonoid α]
    {n k l : Nat} (prices : Vector α n) (left : Composition k) (right : Composition l)
    (hkl : k + l ≤ n) :
    compositionRevenue prices (left.append right) hkl =
      compositionRevenue prices left (by omega) +
      compositionRevenue prices right (by omega)

Uses 1 · Used by 7

Statement usesRevenue of a rod composition

Used byCorrectness of bottom-up rod cutting · Reconstruction earns the final saved revenue · Saved revenues are optimal · The memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · Correctness of memoized rod cutting · Correctness of recursive CUT-ROD

DefinitionBottom-up rod cutting#✓fully proved

Given prices \(p = (p_1, \dots, p_n)\) in an additive commutative monoid \(\alpha\) with a linear order, \(p_i\) being the price of a piece of length \(i\), bottom-up rod cutting fills a table \(r_0, \dots, r_n\) in increasing order by \(r_0 = 0\) and \(r_j = \max_{1 \le i \le j} (p_i + r_{j-i})\) for \(1 \le j \le n\), and returns \(r_n\). Its cost is the number of candidates \(p_i + r_{j-i}\) it evaluates, one for each pair \(1 \le i \le j \le n\).

public def bottomUpCutRod {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) : TimeM Nat α := do
  let table ← fillRows prices n le_rfl
  pure (table.get (Fin.last n))

Used by 8

Used byCorrectness of bottom-up rod cutting · Exact cost of bottom-up rod cutting · Bottom-up rod cutting takes quadratic time · Cost of bottom-up rod cutting as a sum over rows · Twice the cost of bottom-up rod cutting · Bottom-up rod cutting on the empty rod · The extended algorithm computes the same revenue · Running time of extended bottom-up rod cutting

TheoremCorrectness of bottom-up rod cutting#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order in which addition is monotone, and let \(p = (p_1, \dots, p_n)\) be prices in \(\alpha\), \(p_i\) being the price of a piece of length \(i\). The value returned by bottom-up rod cutting on \(p\) is the greatest revenue of a composition of \(n\): it equals \(p_{b_1} + \dots + p_{b_m}\) for some composition \((b_1, \dots, b_m)\) of \(n\) into positive parts, and it is at least this sum for every such composition.

Prices may be negative; every piece of the rod must be sold, so there is no option to discard material.

theorem bottomUpCutRod_correct {α : Type u} [AddCommMonoid α] [LinearOrder α]
    [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) :
    IsGreatest (Set.range fun parts : Composition n => compositionRevenue prices parts le_rfl)
      (bottomUpCutRod prices).ret

Uses 5

Statement usesBottom-up rod cutting · Revenue of a rod composition

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing

TheoremBottom-up rod cutting on the empty rod#✓fully proved

For the empty price vector (\(n = 0\)) over an additive commutative monoid with a linear order, bottom-up rod cutting returns \(0\) at cost \(0\).

@[simp] theorem bottomUpCutRod_zero {α : Type u} [AddCommMonoid α] [LinearOrder α]
    (prices : Vector α 0) : bottomUpCutRod prices = pure 0

Uses 1

Statement usesBottom-up rod cutting

TheoremCost of bottom-up rod cutting as a sum over rows#✓fully proved

For prices \(p = (p_1, \dots, p_n)\) in an additive commutative monoid with a linear order, the cost of bottom-up rod cutting on \(p\) (the number of first-piece candidates it evaluates) equals \(\sum_{j=0}^{n} j\).

Row \(j\) of the table contributes the \(j\) candidates of its scan.

theorem bottomUpCutRod_time_sum {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    (bottomUpCutRod prices).time = ∑ j ∈ Finset.range (n + 1), j

Uses 1 · Used by 3

Statement usesBottom-up rod cutting

Used byExact cost of bottom-up rod cutting · Bottom-up rod cutting takes quadratic time · Twice the cost of bottom-up rod cutting

TheoremTwice the cost of bottom-up rod cutting#✓fully proved

For prices \(p = (p_1, \dots, p_n)\) in an additive commutative monoid with a linear order, the cost \(T\) of bottom-up rod cutting on \(p\) (the number of first-piece candidates it evaluates) satisfies \(2T = n(n + 1)\).

theorem bottomUpCutRod_time_twice {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    2 * (bottomUpCutRod prices).time = n * (n + 1)

Uses 2 · Used by 1

Statement usesBottom-up rod cutting

Proof usesCost of bottom-up rod cutting as a sum over rows

Used byBottom-up rod cutting takes quadratic time

TheoremExact cost of bottom-up rod cutting#✓fully proved

For prices \(p = (p_1, \dots, p_n)\) in an additive commutative monoid with a linear order, the cost of bottom-up rod cutting on \(p\) (the number of first-piece candidates it evaluates) is the triangular number \(n(n + 1)/2\), whatever the prices.

theorem bottomUpCutRod_time {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    (bottomUpCutRod prices).time = n * (n + 1) / 2

Uses 2 · Used by 1

Statement usesBottom-up rod cutting

Proof usesCost of bottom-up rod cutting as a sum over rows

Used byRunning time of extended bottom-up rod cutting

TheoremBottom-up rod cutting takes quadratic time#✓fully proved

For prices \(p = (p_1, \dots, p_n)\) in an additive commutative monoid with a linear order, the cost \(T\) of bottom-up rod cutting on \(p\), the number of first-piece candidates it evaluates, satisfies \(n^2 \le 2T\) and \(T \le n^2\).

theorem bottomUpCutRod_time_bounds {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    n ^ 2 ≤ 2 * (bottomUpCutRod prices).time ∧ (bottomUpCutRod prices).time ≤ n ^ 2

Uses 3

Statement usesBottom-up rod cutting

Proof usesCost of bottom-up rod cutting as a sum over rows · Twice the cost of bottom-up rod cutting

DefinitionExtended bottom-up rod cutting#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, and let \(p_1, \dots, p_n \in \alpha\) be the prices of pieces of length \(1, \dots, n\) (the price vector's entry \(i - 1\) is \(p_i\)). The algorithm fills a revenue table \(r_0, \dots, r_n\) and a first-cut table \(s_1, \dots, s_n\) for the lengths \(j = 0, 1, \dots, n\) in increasing order: \(r_0 = 0\), and for \(j \ge 1\) it scans the candidates \(p_i + r_{j-i}\) for \(i = 1, \dots, j\) in increasing order of \(i\), starting from the candidate for \(i = 1\) and moving to a later candidate only when it is strictly larger than the current one. Then \(r_j\) is the largest candidate and \(s_j\) is the least \(i\) whose candidate equals \(r_j\). The result is the pair of tables, where \(r_j\) is the revenue vector's entry \(j\) and \(s_j\) is the cut vector's entry \(j - 1\), and the cost is one tick per evaluated candidate, so \(j\) ticks for length \(j\).

public def extendedBottomUpCutRod {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) : TimeM Nat (Vector α (n + 1) × Vector Nat n) :=
  fillRowsWithCuts prices n le_rfl

Used by 11

Used byRod cutting with reconstruction · Reconstructed pieces are the saved first cuts · Rod-cutting reconstruction is optimal · Reconstruction earns the final saved revenue · Cost of rod-cutting reconstruction · Rod-cutting reconstruction on the empty rod · Saved revenues are optimal · The saved first cut attains the saved revenue · The extended algorithm computes the same revenue · Running time of extended bottom-up rod cutting · Extended bottom-up rod cutting on the empty rod

TheoremSaved revenues are optimal#✓fully proved

Let \(p\) be a price vector of length \(n\) with entries in a linearly ordered additive commutative monoid (addition is monotone), and let \(r = (r_0, \dots, r_n)\) be the revenue table computed by the extended bottom-up rod-cutting algorithm. For every \(j \le n\), \(r_j\) is the greatest revenue of a composition of \(j\): some composition of \(j\) has revenue \(r_j\), and every composition of \(j\) has revenue at most \(r_j\).

public theorem extendedBottomUpCutRod_correct {α : Type u} [AddCommMonoid α]
    [LinearOrder α] [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n)
    (j : Nat) (hjn : j ≤ n) :
    IsGreatest (Set.range fun parts : Composition j => compositionRevenue prices parts hjn)
      (extendedBottomUpCutRod prices).ret.1[j]

Uses 5 · Used by 1

Statement usesRevenue of a rod composition · Extended bottom-up rod cutting

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing

Used byRod-cutting reconstruction is optimal

TheoremThe extended algorithm computes the same revenue#✓fully proved

For every price vector of length \(n\) with entries in an additive commutative monoid carrying a linear order, the last entry \(r_n\) of the revenue table computed by the extended bottom-up rod-cutting algorithm equals the value returned by the bottom-up rod-cutting algorithm.

public theorem extendedBottomUpCutRod_revenue_eq {α : Type u} [AddCommMonoid α]
    [LinearOrder α] {n : Nat} (prices : Vector α n) :
    (extendedBottomUpCutRod prices).ret.1[n] = (bottomUpCutRod prices).ret

Uses 2

Statement usesBottom-up rod cutting · Extended bottom-up rod cutting

TheoremRunning time of extended bottom-up rod cutting#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order. For every vector of \(n\) prices in \(\alpha\), the extended bottom-up rod-cutting algorithm has cost exactly \(n(n+1)/2\), whatever the prices are.

public theorem extendedBottomUpCutRod_time {α : Type u} [AddCommMonoid α]
    [LinearOrder α] {n : Nat} (prices : Vector α n) :
    (extendedBottomUpCutRod prices).time = n * (n + 1) / 2

Uses 3 · Used by 1

Statement usesExtended bottom-up rod cutting

Proof usesBottom-up rod cutting · Exact cost of bottom-up rod cutting

Used byCost of rod-cutting reconstruction

TheoremExtended bottom-up rod cutting on the empty rod#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order. On the empty price vector (rod length \(0\)), the extended bottom-up rod-cutting algorithm returns the revenue table whose single entry is \(0\) together with the empty first-cut table, at cost \(0\).

@[simp] public theorem extendedBottomUpCutRod_zero {α : Type u} [AddCommMonoid α]
    [LinearOrder α] (prices : Vector α 0) :
    extendedBottomUpCutRod prices = pure (Vector.replicate 1 0, Vector.replicate 0 0)

Uses 1

Statement usesExtended bottom-up rod cutting

TheoremThe saved first cut attains the saved revenue#✓fully proved

Let \(p = (p_0, \dots, p_{n-1})\) be a price vector with entries in an additive commutative monoid carrying a linear order, where \(p_{\ell - 1}\) is the price of a piece of length \(\ell\). Let \(r = (r_0, \dots, r_n)\) be the revenue table and \(s = (s_1, \dots, s_n)\) the saved first cuts computed by the extended bottom-up rod-cutting algorithm, with \(s_j\) stored as entry \(j - 1\) of the cut vector. For every \(j\) with \(0 < j \le n\), the cut \(\ell = s_j\) satisfies \(1 \le \ell \le j\) and \(p_{\ell - 1} + r_{j - \ell} = r_j\), and every \(\ell'\) with \(1 \le \ell' < \ell\) satisfies \(p_{\ell' - 1} + r_{j - \ell'} < r_j\).

public theorem extendedBottomUpCutRod_firstCut {α : Type u} [AddCommMonoid α]
    [LinearOrder α] {n : Nat} (prices : Vector α n) (j : Nat) (hpos : 0 < j)
    (hjn : j ≤ n) :
    ∃ i : Fin j, (extendedBottomUpCutRod prices).ret.2[j - 1]'(by omega) = i.val + 1 ∧
      prices[i.val]'(by omega) +
        (extendedBottomUpCutRod prices).ret.1[j - (i.val + 1)]'(by omega) =
        (extendedBottomUpCutRod prices).ret.1[j] ∧
      ∀ h : Fin j, h.val < i.val →
        prices[h.val]'(by omega) +
          (extendedBottomUpCutRod prices).ret.1[j - (h.val + 1)]'(by omega) <
          (extendedBottomUpCutRod prices).ret.1[j]

Uses 1 · Used by 5

Statement usesExtended bottom-up rod cutting

Used byRod cutting with reconstruction · Reconstructed pieces are the saved first cuts · Reconstruction earns the final saved revenue · Cost of rod-cutting reconstruction · Rod-cutting reconstruction on the empty rod

DefinitionRod cutting with reconstruction#✓fully proved

Given a price vector \(p\) of length \(n\) with entries in an additive commutative monoid carrying a linear order, where entry \(\ell - 1\) is the price of a piece of length \(\ell\), first run the extended bottom-up rod-cutting algorithm to obtain the saved first cuts \(s_1, \dots, s_n\) (with \(s_j\) stored as entry \(j - 1\) of its cut vector). Then, starting from the remaining length \(L = n\), repeatedly emit a piece of length \(s_L\) and replace \(L\) by \(L - s_L\) until \(L = 0\). The result is the composition of \(n\) formed by the emitted pieces in order. Its cost is the cost of the extended algorithm plus one event per emitted piece; allocation and arithmetic are free.

public def cutRodSolution {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) : TimeM Nat (Composition n) :=
  let tables := extendedBottomUpCutRod prices
  TimeM.bind tables fun _ =>
    reconstructCuts tables.ret.2 (extendedBottomUpCutRod_bounded prices) n le_rfl

Uses 2 · Used by 5

Statement usesExtended bottom-up rod cutting · The saved first cut attains the saved revenue

Used byReconstructed pieces are the saved first cuts · Rod-cutting reconstruction is optimal · Reconstruction earns the final saved revenue · Cost of rod-cutting reconstruction · Rod-cutting reconstruction on the empty rod

TheoremCost of rod-cutting reconstruction#✓fully proved

Let \(p\) be a price vector of length \(n\) with entries in an additive commutative monoid carrying a linear order. The rod-cutting reconstruction charges exactly \(n(n+1)/2 + m\) events, where \(m\) is the number of pieces of the composition of \(n\) it returns: one event per evaluated first-cut candidate and one per emitted piece.

public theorem cutRodSolution_time {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    (cutRodSolution prices).time = n * (n + 1) / 2 + (cutRodSolution prices).ret.length

Uses 4

Statement usesRod cutting with reconstruction

Proof usesExtended bottom-up rod cutting · The saved first cut attains the saved revenue · Running time of extended bottom-up rod cutting

TheoremReconstructed pieces are the saved first cuts#✓fully proved

Let \(p\) be a price vector of length \(n\) with entries in an additive commutative monoid carrying a linear order. Let \(s\) be the vector of saved first cuts computed by the extended bottom-up rod-cutting algorithm, of length \(n\), whose entry \(j - 1\) is the cut saved for length \(j\), and let \((b_0, \dots, b_{m-1})\) be the composition of \(n\) returned by the rod-cutting reconstruction. For every \(i < m\), the index \(n - (b_0 + \dots + b_{i-1}) - 1\) lies within \(s\) and the entry of \(s\) at this index is \(b_i\): the \(i\)-th piece is the first cut saved for the remaining length \(n - (b_0 + \dots + b_{i-1})\).

public theorem cutRodSolution_blocks {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) (i : Nat)
    (hi : i < (cutRodSolution prices).ret.length) :
    (extendedBottomUpCutRod prices).ret.2[n - (cutRodSolution prices).ret.sizeUpTo i - 1]? =
      some ((cutRodSolution prices).ret.blocks[i]'hi)

Uses 3

Statement usesRod cutting with reconstruction · Extended bottom-up rod cutting

Proof usesThe saved first cut attains the saved revenue

TheoremReconstruction earns the final saved revenue#✓fully proved

Let \(p\) be a price vector of length \(n\) with entries in an additive commutative monoid carrying a linear order, and let \(r = (r_0, \dots, r_n)\) be the revenue table computed by the extended bottom-up rod-cutting algorithm. The revenue of the composition of \(n\) returned by the rod-cutting reconstruction equals \(r_n\).

public theorem cutRodSolution_revenue {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    compositionRevenue prices (cutRodSolution prices).ret le_rfl =
      (extendedBottomUpCutRod prices).ret.1[n]

Uses 7 · Used by 1

Statement usesRevenue of a rod composition · Rod cutting with reconstruction · Extended bottom-up rod cutting

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing · The saved first cut attains the saved revenue

Used byRod-cutting reconstruction is optimal

TheoremRod-cutting reconstruction is optimal#✓fully proved

Let \(p\) be a price vector of length \(n\) with entries in a linearly ordered additive commutative monoid (addition is monotone). The composition of \(n\) returned by the rod-cutting reconstruction has the greatest revenue among all compositions of \(n\): its revenue is at least the revenue of every composition of \(n\).

public theorem cutRodSolution_correct {α : Type u} [AddCommMonoid α] [LinearOrder α]
    [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) :
    IsGreatest (Set.range fun parts : Composition n => compositionRevenue prices parts le_rfl)
      (compositionRevenue prices (cutRodSolution prices).ret le_rfl)

Uses 5

Statement usesRevenue of a rod composition · Rod cutting with reconstruction

Proof usesReconstruction earns the final saved revenue · Extended bottom-up rod cutting · Saved revenues are optimal

TheoremRod-cutting reconstruction on the empty rod#✓fully proved

For the empty price vector (rod length \(0\)) with entries in an additive commutative monoid carrying a linear order, the rod-cutting reconstruction returns the empty composition of \(0\) and charges no events.

public theorem cutRodSolution_zero {α : Type u} [AddCommMonoid α] [LinearOrder α] :
    cutRodSolution (#v[] : Vector α 0) = pure (Composition.ones 0)

Uses 3

Statement usesRod cutting with reconstruction

Proof usesExtended bottom-up rod cutting · The saved first cut attains the saved revenue

DefinitionRecursive CUT-ROD#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, and let \(p_1, \dots, p_n \in \alpha\) be prices, \(p_i\) being the price of a piece of length \(i\). Recursive CUT-ROD returns \(r(n)\), where \(r(0) = 0\) and, for \(1 \le j \le n\), \(r(j) = \max(p_1 + r(j - 1), p_2 + r(j - 2), \dots, p_j + r(0))\). The first cuts \(i = 1, \dots, j\) are scanned in increasing order and every \(r(j - i)\) is recomputed by a fresh recursive call, without memoization. One cost tick is charged at every invocation, including the root call and every call on an empty rod.

public def recursiveCutRod {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) : TimeM Nat α :=
  recursiveCutRodAux prices n le_rfl

Used by 2

Used byCorrectness of recursive CUT-ROD · Running time of recursive CUT-ROD

TheoremCorrectness of recursive CUT-ROD#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order for which addition is monotone, and let \(p_1, \dots, p_n \in \alpha\) be prices, \(p_i\) being the price of a piece of length \(i\). The value returned by recursive CUT-ROD on these prices is the greatest revenue of a composition of \(n\): it equals the revenue \(p_{i_1} + \dots + p_{i_k}\) of some composition \(n = i_1 + \dots + i_k\) into positive parts, and it is at least the revenue of every such composition.

Every piece is sold: negative prices do not create an option to discard part of the rod.

public theorem recursiveCutRod_correct {α : Type u} [AddCommMonoid α]
    [LinearOrder α] [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) :
    IsGreatest (Set.range fun parts : Composition n =>
      compositionRevenue prices parts le_rfl) (recursiveCutRod prices).ret

Uses 5

Statement usesRevenue of a rod composition · Recursive CUT-ROD

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing

TheoremRunning time of recursive CUT-ROD#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, and let \(p_1, \dots, p_n \in \alpha\) be prices. Recursive CUT-ROD on these prices, which charges one tick per invocation, makes exactly \(2^n\) invocations, counting the root call and every call on an empty rod, whatever the prices are.

public theorem recursiveCutRod_time {α : Type u} [AddCommMonoid α]
    [LinearOrder α] {n : Nat} (prices : Vector α n) :
    (recursiveCutRod prices).time = 2 ^ n

Uses 1

Statement usesRecursive CUT-ROD

DefinitionMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, let \(p = (p_1, \dots, p_n) \in \alpha^n\) be prices, where \(p_i\) is the price of a piece of length \(i\), and let \(c = (c_0, \dots, c_n)\) be a cache whose entries are each either unknown or a value in \(\alpha\). For \(j \le n\) the procedure returns a value and an updated cache, and counts events, as follows. It first charges one event for probing \(c_j\). If \(c_j\) is a known value \(v\), it returns \(v\) and the unchanged cache \(c\). Otherwise, if \(j = 0\), it charges one event for a write and returns \(0\) with \(c_0\) set to \(0\). If \(j \ge 1\), then for \(i = 1, \dots, j\) in turn it calls itself on length \(j - i\) with the cache returned by the previous call (starting from \(c\)), obtaining a value \(q_i\), and charges one event for the candidate \(p_i + q_i\). It then charges one event for a write and returns \(q = \max(p_1 + q_1, \dots, p_j + q_j)\) with entry \(j\) of the last returned cache set to \(q\). The event count is the total over the whole recursion.

Known entries are returned as they are, whatever their sign, including at length zero.

public def memoizedCutRodAux {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) (j : Nat) (hjn : j ≤ n)
    (cache : Vector (Option α) (n + 1)) :
    TimeM Nat (α × Vector (Option α) (n + 1)) :=
  memoizedAuxWorker prices j hjn cache

Used by 8

Used byThe memoized cut-rod procedure (CLRS MEMOIZED-CUT-ROD) · The memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · A cache hit in memoized rod cutting returns at once · The memoized auxiliary preserves known and higher cache entries · Correctness of memoized rod cutting · Event count of memoized rod cutting · Memoized rod cutting on the empty rod

DefinitionThe memoized cut-rod procedure (CLRS MEMOIZED-CUT-ROD)#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order and let \(p = (p_1, \dots, p_n) \in \alpha^n\) be prices, where \(p_i\) is the price of a piece of length \(i\). The procedure runs the memoized rod-cutting auxiliary on length \(n\) with the cache \((c_0, \dots, c_n)\) whose entries are all unknown, and returns the value it computes, discarding the final cache. Its event count is that of the auxiliary call.

public def memoizedCutRod {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) : TimeM Nat α := do
  let result ← memoizedCutRodAux prices n le_rfl (Vector.replicate (n + 1) none)
  pure result.1

Uses 1 · Used by 3

Statement usesMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

Used byCorrectness of memoized rod cutting · Event count of memoized rod cutting · Memoized rod cutting on the empty rod

TheoremA cache hit in memoized rod cutting returns at once#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, let \(p \in \alpha^n\) be a vector of prices, let \(c = (c_0, \dots, c_n)\) be a cache whose entries are each unknown or a value in \(\alpha\), and let \(j \le n\). If \(c_j\) is a known value \(v\), then the memoized rod-cutting auxiliary on length \(j\) and cache \(c\) returns \(v\) and the unchanged cache \(c\), and charges exactly one event.

public theorem memoizedCutRodAux_hit {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) (j : Nat) (hjn : j ≤ n)
    (cache : Vector (Option α) (n + 1)) (value : α)
    (hcache : cache[j]'(by omega) = some value) :
    memoizedCutRodAux prices j hjn cache = ⟨(value, cache), 1⟩

Uses 1 · Used by 5

Statement usesMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

Used byThe memoized auxiliary fills the cache up to the requested length · Correctness of the memoized rod-cutting auxiliary · The memoized auxiliary preserves known and higher cache entries · Correctness of memoized rod cutting · Event count of memoized rod cutting

TheoremThe memoized auxiliary preserves known and higher cache entries#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order, let \(p \in \alpha^n\) be a vector of prices, let \(c = (c_0, \dots, c_n)\) be a cache whose entries are each unknown or a value in \(\alpha\), let \(j \le n\), and let \(c'\) be the cache returned by the memoized rod-cutting auxiliary on length \(j\) and cache \(c\). Then for every \(k \le n\), if \(c_k\) is a known value \(v\), then \(c'_k = v\); and for every \(k\) with \(j < k \le n\), \(c'_k = c_k\).

public theorem memoizedCutRodAux_preserves {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) (j : Nat) (hjn : j ≤ n)
    (cache : Vector (Option α) (n + 1)) :
    (∀ (k : Nat) (hkn : k ≤ n) (value : α), cache[k]'(by omega) = some value →
      (memoizedCutRodAux prices j hjn cache).ret.2[k]'(by omega) = some value) ∧
    ∀ (k : Nat) (hkn : k ≤ n), j < k →
      (memoizedCutRodAux prices j hjn cache).ret.2[k]'(by omega) = cache[k]

Uses 2 · Used by 2

Statement usesMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

Proof usesA cache hit in memoized rod cutting returns at once

Used byThe memoized auxiliary fills the cache up to the requested length · Event count of memoized rod cutting

TheoremMemoized rod cutting on the empty rod#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order. For the empty price vector (\(n = 0\)), the memoized cut-rod procedure returns \(0\) and charges exactly \(2\) events: one cache probe and one cache write.

public theorem memoizedCutRod_zero {α : Type u} [AddCommMonoid α] [LinearOrder α]
    (prices : Vector α 0) : memoizedCutRod prices = ⟨0, 2⟩

Uses 2

Statement usesThe memoized cut-rod procedure (CLRS MEMOIZED-CUT-ROD)

Proof usesMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

TheoremCorrectness of the memoized rod-cutting auxiliary#✓fully proved

Let \(\alpha\) be a linearly ordered additive commutative monoid (that is, \(a \le b\) implies \(a + c \le b + c\)) and let \(p = (p_1, \dots, p_n) \in \alpha^n\) be prices, where \(p_i\) is the price of a piece of length \(i\). Call a cache \(c = (c_0, \dots, c_n)\), whose entries are each unknown or a value in \(\alpha\), valid if for every known entry \(c_k = v\) the value \(v\) is the greatest composition revenue over compositions of \(k\). If \(c\) is valid, \(j \le n\), and the memoized rod-cutting auxiliary on length \(j\) and cache \(c\) returns the value \(q\) and the cache \(c'\), then \(q\) is the greatest composition revenue over compositions of \(j\), the cache \(c'\) is valid, and \(c'_j = q\).

public theorem memoizedCutRodAux_correct {α : Type u} [AddCommMonoid α] [LinearOrder α]
    [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) (j : Nat) (hjn : j ≤ n)
    (cache : Vector (Option α) (n + 1))
    (hvalid : ∀ (k : Nat) (hk : k ≤ n) (value : α), cache[k]'(by omega) = some value →
      IsGreatest (Set.range fun parts : Composition k => compositionRevenue prices parts hk)
        value) :
    IsGreatest (Set.range fun parts : Composition j => compositionRevenue prices parts hjn)
      (memoizedCutRodAux prices j hjn cache).ret.1 ∧
    (∀ (k : Nat) (hk : k ≤ n) (value : α),
      (memoizedCutRodAux prices j hjn cache).ret.2[k]'(by omega) = some value →
        IsGreatest (Set.range fun parts : Composition k => compositionRevenue prices parts hk)
          value) ∧
    (memoizedCutRodAux prices j hjn cache).ret.2[j]'(by omega) =
      some (memoizedCutRodAux prices j hjn cache).ret.1

Uses 6

Statement usesRevenue of a rod composition · Memoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing · A cache hit in memoized rod cutting returns at once

TheoremCorrectness of memoized rod cutting#✓fully proved

Let \(\alpha\) be a linearly ordered additive commutative monoid (that is, \(a \le b\) implies \(a + c \le b + c\)) and let \(p = (p_1, \dots, p_n) \in \alpha^n\) be prices, where \(p_i\) is the price of a piece of length \(i\). The value returned by the memoized cut-rod procedure on \(p\) is the greatest composition revenue over compositions of \(n\): it is the revenue of some composition of \(n\), and it is at least the revenue of every composition of \(n\).

public theorem memoizedCutRod_correct {α : Type u} [AddCommMonoid α] [LinearOrder α]
    [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) :
    IsGreatest (Set.range fun parts : Composition n => compositionRevenue prices parts le_rfl)
      (memoizedCutRod prices).ret

Uses 7

Statement usesRevenue of a rod composition · The memoized cut-rod procedure (CLRS MEMOIZED-CUT-ROD)

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing · Memoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX) · A cache hit in memoized rod cutting returns at once

TheoremThe memoized auxiliary fills the cache up to the requested length#✓fully proved

Let \(\alpha\) be a linearly ordered additive commutative monoid (that is, \(a \le b\) implies \(a + c \le b + c\)), let \(p = (p_1, \dots, p_n) \in \alpha^n\) be prices, where \(p_i\) is the price of a piece of length \(i\), and let \(j \le n\). If the memoized rod-cutting auxiliary is run on length \(j\) with the cache \((c_0, \dots, c_n)\) whose entries are all unknown, then for every \(k \le j\) entry \(k\) of the returned cache is a known value, and that value is the greatest composition revenue over compositions of \(k\).

public theorem memoizedCutRodAux_complete {α : Type u} [AddCommMonoid α] [LinearOrder α]
    [IsOrderedAddMonoid α] {n : Nat} (prices : Vector α n) (j : Nat) (hjn : j ≤ n) :
    ∀ (k : Nat) (hk : k ≤ j), ∃ value : α,
      (memoizedCutRodAux prices j hjn (Vector.replicate (n + 1) none)).ret.2[k]'(by omega) =
        some value ∧
      IsGreatest (Set.range fun parts : Composition k =>
        compositionRevenue prices parts (by omega)) value

Uses 7

Statement usesRevenue of a rod composition · Memoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX)

Proof usesRevenue is additive under concatenation · Revenue of an uncut rod · The empty rod earns nothing · A cache hit in memoized rod cutting returns at once · The memoized auxiliary preserves known and higher cache entries

TheoremEvent count of memoized rod cutting#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a linear order and let \(p \in \alpha^n\) be a vector of prices. The memoized cut-rod procedure on \(p\) charges exactly \(n^2 + 2n + 2\) events, where one event is charged per cache probe, per first-cut candidate, and per cache write.

Allocation, initialization, arithmetic, comparisons and control are not charged.

public theorem memoizedCutRod_time {α : Type u} [AddCommMonoid α] [LinearOrder α]
    {n : Nat} (prices : Vector α n) :
    (memoizedCutRod prices).time = n ^ 2 + 2 * n + 2

Uses 4

Statement usesThe memoized cut-rod procedure (CLRS MEMOIZED-CUT-ROD)

Proof usesMemoized rod-cutting auxiliary (CLRS MEMOIZED-CUT-ROD-AUX) · A cache hit in memoized rod cutting returns at once · The memoized auxiliary preserves known and higher cache entries

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.