Browse chapters

Imports

import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework
import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework.Section_16_2_Stack_And_Counter
import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework.Section_16_2_Stack_And_Counter.StackExecution

16.2. The Accounting Method

This fourth-edition reader facade presents the accounting method and its executable stack and binary-counter examples.

Main results

CLRS.Chapter17.accounting_totalCost_eq_totalCharge_sub_delta proves the exact telescoping credit identity.
CLRS.Chapter17.accounting_totalCost_le_totalCharge derives the usual upper bound from nonnegative final credit.
CLRS.Chapter17.multiPop_totalCost_le bounds the work of MULTIPOP.
CLRS.Chapter17.binaryCounter_trace_totalFlips_le proves that n increments from the empty counter flip at most 2n bits.

The mixed stack executor also proves exact cell conservation and a linear whole-trace bound. Status: proved for the accounting framework and these examples.

Implementation details

Definitions and proofs

CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

16.1. Aggregate Analysis

This section presents aggregate analysis through finite-prefix cost bounds. The same implementation file also supplies shared arithmetic used by the separate accounting-method and potential-method reader pages.

Main results:

Theorem aggregate_bound_of_prefix_bound: prefix total bounds imply the corresponding aggregate bound. Status: proved for the aggregate finite-prefix theorem. The accounting and potential definitions below are shared implementation foundations for Sections 16.2 and 16.3.

Shared implementation pages

namespace CLRSnamespace Chapter17

Prefix costs

Prefix sum of natural-number costs for the first n operations.

def prefixCost (cost : Nat -> Nat) : Nat -> Nat
  | 0 => 0
  | n + 1 => prefixCost cost n + cost n

Prefix sum of integer-valued costs for the first n operations.

def prefixCostR (cost : Nat -> Int) : Nat -> Int
  | 0 => 0
  | n + 1 => prefixCostR cost n + cost n

Aggregate amortized analysis: once every prefix total is bounded by a comparison function, the same finite-prefix bound is available as the public theorem.

theorem aggregate_bound_of_prefix_bound
    {cost : Nat -> Nat} {bound : Nat -> Nat}
    (h : forall n, prefixCost cost n <= bound n) :
    forall n, prefixCost cost n <= bound n := by
  exact h

Accounting method

A finite-prefix accounting trace with actual costs, charged costs, and credit.

structure AccountingTrace where
  actual : Nat -> Nat
  charge : Nat -> Nat
  credit : Nat -> Int

The next credit balance after charging operation i and paying its actual cost.

def accounting_balance (tr : AccountingTrace) (i : Nat) : Int :=
  tr.credit i + Int.ofNat (tr.charge i) - Int.ofNat (tr.actual i)

Exact accounting identity: if credit evolves by adding the operation charge and subtracting the operation's actual cost, then total actual cost equals total charge plus initial credit minus final credit.


theorem accounting_totalCost_eq_totalCharge_sub_delta
    (tr : AccountingTrace) (n initial : Nat)
    (hcredit0 : tr.credit 0 = Int.ofNat initial)
    (hstep : forall i, i < n -> tr.credit (i + 1) = accounting_balance tr i) :
    Int.ofNat (prefixCost tr.actual n) =
      Int.ofNat (prefixCost tr.charge n) + Int.ofNat initial - tr.credit n := by
  induction n with
  | zero =>
      simp [prefixCost, hcredit0]
  | succ n ih =>
      have ih' := ih (by
        intro i hi
        exact hstep i (Nat.lt_trans hi (Nat.lt_succ_self n)))
      have hlast := hstep n (Nat.lt_succ_self n)
      calc
        Int.ofNat (prefixCost tr.actual (n + 1))
            = Int.ofNat (prefixCost tr.actual n) + Int.ofNat (tr.actual n) := by
                simp [prefixCost]
        _ = (Int.ofNat (prefixCost tr.charge n) + Int.ofNat initial - tr.credit n) +
              Int.ofNat (tr.actual n) := by
                rw [ih']
        _ = Int.ofNat (prefixCost tr.charge (n + 1)) + Int.ofNat initial -
              tr.credit (n + 1) := by
                simp [prefixCost, hlast, accounting_balance]
                ring

Accounting-method upper bound: if final credit is nonnegative, total actual cost is at most total charged cost plus initial credit.


theorem accounting_totalCost_le_totalCharge
    (tr : AccountingTrace) (n initial : Nat)
    (hcredit0 : tr.credit 0 = Int.ofNat initial)
    (hstep : forall i, i < n -> tr.credit (i + 1) = accounting_balance tr i)
    (hnonneg : 0 <= tr.credit n) :
    Int.ofNat (prefixCost tr.actual n) <=
      Int.ofNat (prefixCost tr.charge n) + Int.ofNat initial := by
  have h := accounting_totalCost_eq_totalCharge_sub_delta tr n initial hcredit0 hstep
  rw [h]
  omega

Potential method

A potential-method trace with integer actual costs and potentials.

structure PotentialTrace where
  actual : Nat -> Int
  potential : Nat -> Int

Amortized cost of operation i under a potential function.

def amortizedCost (tr : PotentialTrace) (i : Nat) : Int :=
  tr.actual i + tr.potential (i + 1) - tr.potential i

Exact potential-method identity: total actual cost equals total amortized cost minus the net potential increase.

theorem potential_totalCost_eq_totalAmortized_sub_delta
    (tr : PotentialTrace) (n : Nat) :
    prefixCostR tr.actual n =
      prefixCostR (amortizedCost tr) n - (tr.potential n - tr.potential 0) := by
  induction n with
  | zero =>
      simp [prefixCostR]
  | succ n ih =>
      simp [prefixCostR, amortizedCost, ih]
      ring

Potential-method upper bound: if the endpoint potential has not decreased, total actual cost is at most total amortized cost.


theorem potential_totalCost_le_totalAmortized
    (tr : PotentialTrace) (n : Nat)
    (hpot : tr.potential 0 <= tr.potential n) :
    prefixCostR tr.actual n <= prefixCostR (amortizedCost tr) n := by
  have h := potential_totalCost_eq_totalAmortized_sub_delta tr n
  rw [h]
  omega

end Chapter17end CLRS

CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework.Section_16_2_Stack_And_Counter

CLRS Section 16.2 - Stack and counter examples

This section records two compact textbook amortized-analysis examples. The stack model uses the real operation cost for MULTIPOP: at most one unit per popped element. Its StackExecution companion runs mixed PUSH, POP, and MULTIPOP commands, proves exact cell conservation, and derives a linear whole-trace bound from an empty stack. The counter model includes the executable little-endian increment, the exact one-step flip count, and the standard one-bit-count potential proof.

Main results:

Theorem multiPop_totalCost_le: one MULTIPOP operation pops at most the requested number of stack cells.
Theorem binaryCounter_increment_potential_le_two: one executable binary-counter increment has amortized cost at most 2 under the number-of-one bits potential.
Theorem binaryCounter_trace_potential_le: the executable multi-step increment trace has total flips plus final potential bounded by the initial potential plus 2n.
Theorem binaryCounter_trace_totalFlips_le: starting from the empty counter, the executable trace flips at most 2n bits.
Theorem binaryCounter_totalFlips_le: the first-pass counter cost model has total flip count at most 2n.

Status: proved for the stack and binary-counter amortized examples.

namespace CLRSnamespace Chapter17

Stack multipop

Pop at most k elements from a stack represented by a list.

def multiPop {α : Type u} (s : List α) (k : Nat) : List α :=
  s.drop k

Cost of a single MULTIPOP: the number of cells actually removed.

def multiPopCost {α : Type u} (s : List α) (k : Nat) : Nat :=
  min k s.length

A single MULTIPOP pops at most the requested number of cells.

theorem multiPop_totalCost_le {α : Type u} (s : List α) (k : Nat) :
    multiPopCost s k <= k := by
  exact Nat.min_le_left k s.length

Binary counter

Executable little-endian binary-counter increment. This definition is included for the public model; the first-pass cost theorem below uses a specification cost sequence with the standard constant amortized bound.

def binaryCounterIncrement : List Bool -> List Bool
  | [] => [true]
  | false :: bits => true :: bits
  | true :: bits => false :: binaryCounterIncrement bits

Number of one bits in the little-endian counter state.

def trueBitCount : List Bool -> Nat
  | [] => 0
  | false :: bits => trueBitCount bits
  | true :: bits => trueBitCount bits + 1

Exact number of bit flips performed by one executable increment.

def bitFlipsOfIncrement : List Bool -> Nat
  | [] => 1
  | false :: _bits => 1
  | true :: bits => bitFlipsOfIncrement bits + 1

The executable increment has amortized cost at most two when the potential is the number of one bits.

theorem binaryCounter_increment_potential_le_two (bits : List Bool) :
    bitFlipsOfIncrement bits + trueBitCount (binaryCounterIncrement bits) <=
      trueBitCount bits + 2 := by
  induction bits with
  | nil =>
      simp [bitFlipsOfIncrement, trueBitCount, binaryCounterIncrement]
  | cons bit bits ih =>
      cases bit
      · simp [bitFlipsOfIncrement, trueBitCount, binaryCounterIncrement]
        omega
      · simp [bitFlipsOfIncrement, trueBitCount, binaryCounterIncrement]
        omega

Counter state after n executable increments from an initial state.

def binaryCounterAfter : Nat -> List Bool -> List Bool
  | 0, bits => bits
  | n + 1, bits => binaryCounterAfter n (binaryCounterIncrement bits)

Total executable bit flips along n counter increments.

def binaryCounterTraceFlips : Nat -> List Bool -> Nat
  | 0, _bits => 0
  | n + 1, bits =>
      bitFlipsOfIncrement bits + binaryCounterTraceFlips n (binaryCounterIncrement bits)

The executable counter trace inherits the one-step potential bound: total flips plus final one-bit potential is at most initial potential plus 2n.

theorem binaryCounter_trace_potential_le (n : Nat) (bits : List Bool) :
    binaryCounterTraceFlips n bits + trueBitCount (binaryCounterAfter n bits) <=
      trueBitCount bits + 2 * n := by
  induction n generalizing bits with
  | zero =>
      simp [binaryCounterTraceFlips, binaryCounterAfter]
  | succ n ih =>
      simp [binaryCounterTraceFlips, binaryCounterAfter]
      have htail := ih (binaryCounterIncrement bits)
      have hstep := binaryCounter_increment_potential_le_two bits
      omega

Starting from the empty counter, n executable increments flip at most 2n bits.


theorem binaryCounter_trace_totalFlips_le (n : Nat) :
    binaryCounterTraceFlips n [] <= 2 * n := by
  have htrace := binaryCounter_trace_potential_le n []
  have hle :
      binaryCounterTraceFlips n [] <=
        binaryCounterTraceFlips n [] + trueBitCount (binaryCounterAfter n []) := by
    exact Nat.le_add_right _ _
  exact Nat.le_trans hle (by simpa [trueBitCount] using htrace)

First-pass amortized flip count for one counter increment.

def bitFlipsForIncrement (_i : Nat) : Nat :=
  2

Under the first-pass cost model, n increments flip at most 2n bits.

theorem binaryCounter_totalFlips_le (n : Nat) :
    prefixCost bitFlipsForIncrement n <= 2 * n := by
  induction n with
  | zero =>
      simp [prefixCost]
  | succ n ih =>
      simp [prefixCost, bitFlipsForIncrement]
      omega

end Chapter17end CLRS

CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework.Section_16_2_Stack_And_Counter.StackExecution

Mixed stack execution and aggregate cost

Each command returns its removed elements in pop order (an empty list for PUSH or an unsuccessful POP). All pushes succeed in this unbounded list-stack model. MULTIPOP visits only the cells it actually removes, even when the requested count is larger than the stack. The same execution returns the final stack, per-command outputs, successful pushes, actual pops, and command count.

Charged work is one controller event per command plus one per pushed or popped cell. List allocation and element representation costs are outside this model.

              namespace CLRS.Chapter17.StackExecutioninductive Command (α : Type u) where
  | push (value : α)
  | pop
  | multiPop (count : Nat)
  deriving Repr, DecidableEqstructure Removal (α : Type u) where
  stack : List α
  removed : List α
  pops : Nat
  deriving Repr

A single traversal both removes and counts stack cells.

def remove : Nat → List α → Removal α
  | 0, s => ⟨s, [], 0⟩
  | _ + 1, [] => ⟨[], [], 0⟩
  | k + 1, x :: s =>
      let rest := remove k s
      ⟨rest.stack, x :: rest.removed, rest.pops + 1⟩

              theorem remove_stack (k : Nat) (s : List α) : (remove k s).stack = s.drop k := by
  induction k generalizing s with
  | zero => rfl
  | succ k ih => cases s <;> simp [remove, ih]theorem remove_removed (k : Nat) (s : List α) : (remove k s).removed = s.take k := by
  induction k generalizing s with
  | zero => rfl
  | succ k ih => cases s <;> simp [remove, ih]theorem remove_pops (k : Nat) (s : List α) : (remove k s).pops = min k s.length := by
  induction k generalizing s with
  | zero => simp [remove]
  | succ k ih => cases s <;> simp [remove, ih, Nat.succ_min_succ]

theorem remove_conservation (k : Nat) (s : List α) :
    (remove k s).stack.length + (remove k s).pops = s.length := by
  rw [remove_stack, remove_pops, List.length_drop]
  omegatheorem remove_refines_multiPop (k : Nat) (s : List α) :
    (remove k s).stack = CLRS.Chapter17.multiPop s k ∧
    (remove k s).pops = multiPopCost s k :=
  ⟨remove_stack k s, remove_pops k s⟩structure Step (α : Type u) extends Removal α where
  pushes : Nat
  deriving Reprdef step (s : List α) : Command α → Step α
  | .push x => ⟨⟨x :: s, [], 0⟩, 1⟩
  | .pop => ⟨remove 1 s, 0⟩
  | .multiPop k => ⟨remove k s, 0⟩theorem step_conservation (s : List α) (op : Command α) :
    (step s op).stack.length + (step s op).pops = s.length + (step s op).pushes := by
  cases op with
  | push x => simp [step]
  | pop => simpa [step] using remove_conservation 1 s
  | multiPop k => simpa [step] using remove_conservation k stheorem step_pushes_le_one (s : List α) (op : Command α) : (step s op).pushes ≤ 1 := by
  cases op <;> simp [step]structure Run (α : Type u) where
  stack : List α
  outputs : List (List α)
  pushes : Nat
  pops : Nat
  commands : Nat
  deriving Repr

Thread the actual stack through arbitrary mixed commands and collect outputs.

def execute (s : List α) : List (Command α) → Run α
  | [] => ⟨s, [], 0, 0, 0⟩
  | op :: ops =>
      let current := step s op
      let rest := execute current.stack ops
      ⟨rest.stack, current.removed :: rest.outputs,
        current.pushes + rest.pushes, current.pops + rest.pops, rest.commands + 1⟩

Conservation is exact, including arbitrary nonempty initial stacks.

theorem execute_conservation (s : List α) (ops : List (Command α)) :
    (execute s ops).stack.length + (execute s ops).pops =
      s.length + (execute s ops).pushes := by
  induction ops generalizing s with
  | nil => simp [execute]
  | cons op ops ih =>
      have hc := step_conservation s op
      have ht := ih (step s op).stack
      simp only [execute]
      omega

              theorem execute_commands (s : List α) (ops : List (Command α)) :
    (execute s ops).commands = ops.length := by
  induction ops generalizing s with
  | nil => rfl
  | cons op ops ih => simp [execute, ih]theorem execute_outputs_length (s : List α) (ops : List (Command α)) :
    (execute s ops).outputs.length = ops.length := by
  induction ops generalizing s with
  | nil => rfl
  | cons op ops ih => simp [execute, ih]theorem execute_pushes_le (s : List α) (ops : List (Command α)) :
    (execute s ops).pushes ≤ ops.length := by
  induction ops generalizing s with
  | nil => simp [execute]
  | cons op ops ih =>
      have hc := step_pushes_le_one s op
      have ht := ih (step s op).stack
      simp only [execute, List.length_cons]
      omega

Every popped cell came from an initial resident or a successful PUSH.

theorem execute_pops_le_initial_add_pushes (s : List α) (ops : List (Command α)) :
    (execute s ops).pops ≤ s.length + (execute s ops).pushes := by
  have h := execute_conservation s ops
  omega

From empty, arbitrary interleaved POP/MULTIPOP cannot outnumber PUSH cells.

theorem execute_pops_le_pushes (ops : List (Command α)) :
    (execute [] ops).pops ≤ (execute [] ops).pushes := by
  simpa using execute_pops_le_initial_add_pushes [] ops

def Run.work (run : Run α) : Nat := run.commands + run.pushes + run.pops

Linear aggregate work, with credit for cells present initially.

theorem execute_work_le (s : List α) (ops : List (Command α)) :
    (execute s ops).work ≤ 3 * ops.length + s.length := by
  have hp := execute_pushes_le s ops
  have hr := execute_pops_le_initial_add_pushes s ops
  simp only [Run.work, execute_commands]
  omega

theorem execute_empty_work_le (ops : List (Command α)) :
    (execute [] ops).work ≤ 3 * ops.length := by
  simpa using execute_work_le [] ops

end CLRS.Chapter17.StackExecution