CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 16. Amortized Analysis

Chapter 16 — Amortized Analysis

CLRS, fourth edition · Lean 4 formalization

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

Imports

import Mathlib

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

Definitions and proofs

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

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

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

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)


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

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

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

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

Imports

import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

16.3. The Potential Method

This fourth-edition reader facade presents the potential method independently from the aggregate and accounting methods.

Main results

CLRS.Chapter17.amortizedCost adds the change in potential to an operation's actual cost.
CLRS.Chapter17.potential_totalCost_eq_totalAmortized_sub_delta proves the exact telescoping identity for a finite trace.
CLRS.Chapter17.potential_totalCost_le_totalAmortized derives the standard upper bound when the endpoint potential does not decrease.

Status: proved for the finite-trace potential framework.

Definitions and proofs

CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

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

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

Imports

import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

16.4. Dynamic Tables

This first-pass section keeps dynamic tables at the abstract size/count level. It records the state invariant and a conservative potential wrapper that later resize-transition proofs can instantiate.

Main results:

Predicate DynamicTableState.Valid: the number of stored elements does not exceed allocated table size.
Theorem dynamicPotential_nonneg: the first-pass table potential is nonnegative.
Theorems dynamicTableInsert_potential_nonneg and dynamicTableDelete_potential_nonneg: concrete post-transition states have nonnegative first-pass potential.
Theorems dynamicTableInsertSize_fits and dynamicTableDeleteSize_fits: the first-pass capacity choices can hold the post-operation number of stored elements.
Theorems dynamicTableInsertSize_ge_size and dynamicTableDeleteSize_le_size: insertion never shrinks capacity, and deletion never grows capacity for a valid table.
Theorems dynamicTableInsertSize_ge_double_of_expand, dynamicTableInsert_capacity_ge_double_of_expand, dynamicTableDeleteSize_le_half_of_contract, and dynamicTableDelete_capacity_le_half_of_contract: direct capacity direction wrappers for resizing branches.
Theorems dynamicTableInsertSize_of_fits, dynamicTableInsertSize_of_expand, dynamicTableDeleteSize_of_contract, and dynamicTableDeleteSize_of_no_contract: direct case specifications for the first-pass capacity-choice definitions.
Theorems dynamicTableInsertCost_le_num_succ and dynamicTableDeleteCost_le_num: the first-pass transition costs are bounded by the natural element-count copying budgets.
Theorems dynamicTableInsertCost_pos and dynamicTableDeleteCost_pos_of_nonempty: first-pass nonempty transitions have positive actual cost.
Theorems dynamicTableDeleteCost_pos_iff_nonempty and dynamicTableDeleteCost_zero_iff_empty: deletion cost positivity and zero-cost behavior exactly match whether the table is nonempty.
Theorems dynamicTableInsertCost_of_fits, dynamicTableInsertCost_of_expand, dynamicTableDeleteCost_empty, dynamicTableDeleteCost_of_contract, and dynamicTableDeleteCost_of_no_contract: direct case specifications for the first-pass actual-cost definitions.
Theorems dynamicTableDeleteCost_eq_num_of_contract and dynamicTableDeleteCost_eq_one_of_no_contract: deletion actual-cost branch wrappers without an explicit nonempty-table premise.
Theorem dynamicTableInsert_valid: the first-pass insertion transition preserves the table-size invariant.
Theorem dynamicTableDelete_valid: the first-pass deletion/contraction transition preserves the table-size invariant.
Theorems dynamicTableInsert_num, dynamicTableInsert_size, dynamicTableDelete_num, and dynamicTableDelete_size: direct post-state field equations for the transition wrappers.
Theorems dynamicTableInsert_size_of_fits, dynamicTableInsert_size_of_expand, dynamicTableDelete_size_of_contract, and dynamicTableDelete_size_of_no_contract: direct post-state allocation-size case specifications for the transition wrappers.
Theorems dynamicTableInsert_num_gt, dynamicTableInsert_num_pos, dynamicTableInsert_num_ge, dynamicTableDelete_num_le, dynamicTableDelete_num_empty, and dynamicTableDelete_num_pos_of_one_lt, and dynamicTableDelete_num_lt_of_nonempty: direct post-state stored-count direction corollaries for insertion and deletion.
Theorems dynamicTableInsert_capacity_fits, dynamicTableInsert_capacity_pos, dynamicTableInsert_capacity_ge_size, dynamicTableDelete_capacity_fits, dynamicTableDelete_capacity_pos_of_one_lt, and dynamicTableDelete_capacity_le_size: direct post-state capacity corollaries for insertion and deletion.
Theorems dynamicTableInsert_amortizedBound and dynamicTableDelete_amortizedBound: the concrete first-pass transitions instantiate the generic amortized-cost wrapper.
Theorems dynamicTableInsert_amortizedCost_eq and dynamicTableDelete_amortizedCost_eq: concrete transition amortized costs unfold to actual cost plus the post-potential minus the pre-potential.
Theorem dynamicTable_amortizedBound: the abstract dynamic-table amortized cost is bounded by actual cost plus the post-operation potential.

Implementation details

The mutable-array refinement remains available outside the main sidebar:

Mutable-Array Tables and Sharper Potential

Current gaps:

Mutable-array copying and allocator semantics are deferred.

namespace CLRSnamespace Chapter17

Abstract dynamic-table state: stored element count and allocated size.

structure DynamicTableState where
  num : Nat
  size : Nat

namespace DynamicTableState

The table never stores more elements than its allocated size.

def Valid (s : DynamicTableState) : Prop :=
  s.num <= s.size

end DynamicTableState

A simple nonnegative potential for first-pass dynamic-table amortized wrappers. Later resize-specific proofs can replace this with the sharper CLRS potential.

def dynamicPotential (s : DynamicTableState) : Int :=
  Int.ofNat (2 * s.num + s.size)

The first-pass dynamic-table potential is nonnegative.

theorem dynamicPotential_nonneg (s : DynamicTableState) :
    0 <= dynamicPotential s := by
  unfold dynamicPotential
  exact Int.natCast_nonneg (2 * s.num + s.size)

Abstract dynamic-table amortized cost for one state transition.

def dynamicTableAmortizedCost
    (before after : DynamicTableState) (actual : Nat) : Int :=
  Int.ofNat actual + dynamicPotential after - dynamicPotential before

Allocated size after one insertion. If the existing table has room, keep its size; otherwise choose a capacity that both fits the new element and doubles the old allocation budget.

def dynamicTableInsertSize (s : DynamicTableState) : Nat :=
  if s.num + 1 <= s.size then
    s.size
  else
    max (s.num + 1) (2 * s.size)

First-pass dynamic-table insertion transition.

def dynamicTableInsert (s : DynamicTableState) : DynamicTableState :=
  { num := s.num + 1, size := dynamicTableInsertSize s }

First-pass insertion cost: one write plus copied elements on expansion.

def dynamicTableInsertCost (s : DynamicTableState) : Nat :=
  if s.num + 1 <= s.size then
    1
  else
    s.num + 1

Dynamic-table insertion has positive first-pass actual cost.

theorem dynamicTableInsertCost_pos (s : DynamicTableState) :
    0 < dynamicTableInsertCost s := by
  unfold dynamicTableInsertCost
  by_cases hfit : s.num + 1 <= s.size
  · simp [hfit]
  · simp [hfit]

Insertion into a table with spare capacity costs one write.

theorem dynamicTableInsertCost_of_fits (s : DynamicTableState)
    (hfit : s.num + 1 <= s.size) :
    dynamicTableInsertCost s = 1 := by
  simp [dynamicTableInsertCost, hfit]

Insertion into a full table costs the post-insertion element count.

theorem dynamicTableInsertCost_of_expand (s : DynamicTableState)
    (hfull : ¬ s.num + 1 <= s.size) :
    dynamicTableInsertCost s = s.num + 1 := by
  simp [dynamicTableInsertCost, hfull]

The first-pass insertion cost is bounded by the post-insertion element count.

theorem dynamicTableInsertCost_le_num_succ (s : DynamicTableState) :
    dynamicTableInsertCost s <= s.num + 1 := by
  unfold dynamicTableInsertCost
  by_cases hfit : s.num + 1 <= s.size
  · simp [hfit]
  · simp [hfit]

Insertion with spare capacity keeps the old allocation size.

theorem dynamicTableInsertSize_of_fits (s : DynamicTableState)
    (hfit : s.num + 1 <= s.size) :
    dynamicTableInsertSize s = s.size := by
  simp [dynamicTableInsertSize, hfit]

Insertion without spare capacity uses the first-pass expansion choice.

theorem dynamicTableInsertSize_of_expand (s : DynamicTableState)
    (hfull : ¬ s.num + 1 <= s.size) :
    dynamicTableInsertSize s = max (s.num + 1) (2 * s.size) := by
  simp [dynamicTableInsertSize, hfull]

The insertion capacity choice can hold the inserted element.

theorem dynamicTableInsertSize_fits (s : DynamicTableState) :
    s.num + 1 <= dynamicTableInsertSize s := by
  unfold dynamicTableInsertSize
  by_cases hfit : s.num + 1 <= s.size
  · simp [hfit]
  · simp [hfit]

The insertion capacity choice never shrinks the table.

theorem dynamicTableInsertSize_ge_size (s : DynamicTableState) :
    s.size <= dynamicTableInsertSize s := by
  unfold dynamicTableInsertSize
  by_cases hfit : s.num + 1 <= s.size
  · simp [hfit]
  · simp [hfit]
    exact Or.inr (by omega)

The insertion expansion branch allocates at least double the old capacity.


theorem dynamicTableInsertSize_ge_double_of_expand (s : DynamicTableState)
    (hfull : ¬ s.num + 1 <= s.size) :
    2 * s.size <= dynamicTableInsertSize s := by
  rw [dynamicTableInsertSize_of_expand s hfull]
  exact le_max_right (s.num + 1) (2 * s.size)

Dynamic-table insertion increments the stored-element count by one.

theorem dynamicTableInsert_num (s : DynamicTableState) :
    (dynamicTableInsert s).num = s.num + 1 := by
  rfl

Dynamic-table insertion sets the post-state capacity to the insertion capacity choice.

theorem dynamicTableInsert_size (s : DynamicTableState) :
    (dynamicTableInsert s).size = dynamicTableInsertSize s := by
  rfl

Insertion with spare capacity keeps the post-state allocation size.


theorem dynamicTableInsert_size_of_fits (s : DynamicTableState)
    (hfit : s.num + 1 <= s.size) :
    (dynamicTableInsert s).size = s.size := by
  rw [dynamicTableInsert_size, dynamicTableInsertSize_of_fits s hfit]

Insertion without spare capacity uses the expansion choice as the post-state size.


theorem dynamicTableInsert_size_of_expand (s : DynamicTableState)
    (hfull : ¬ s.num + 1 <= s.size) :
    (dynamicTableInsert s).size = max (s.num + 1) (2 * s.size) := by
  rw [dynamicTableInsert_size, dynamicTableInsertSize_of_expand s hfull]

Dynamic-table insertion strictly increases the stored-element count.


theorem dynamicTableInsert_num_gt (s : DynamicTableState) :
    s.num < (dynamicTableInsert s).num := by
  rw [dynamicTableInsert_num]
  exact Nat.lt_succ_self s.num

Dynamic-table insertion leaves a positive stored-element count.


theorem dynamicTableInsert_num_pos (s : DynamicTableState) :
    0 < (dynamicTableInsert s).num := by
  rw [dynamicTableInsert_num]
  exact Nat.succ_pos s.num

Dynamic-table insertion never decreases the stored-element count.

theorem dynamicTableInsert_num_ge (s : DynamicTableState) :
    s.num <= (dynamicTableInsert s).num := by
  exact Nat.le_of_lt (dynamicTableInsert_num_gt s)

Dynamic-table insertion leaves enough capacity for the post-insertion count.

theorem dynamicTableInsert_capacity_fits (s : DynamicTableState) :
    (dynamicTableInsert s).num <= (dynamicTableInsert s).size := by
  exact dynamicTableInsertSize_fits s

Dynamic-table insertion leaves a positive post-state capacity.

theorem dynamicTableInsert_capacity_pos (s : DynamicTableState) :
    0 < (dynamicTableInsert s).size := by
  have hnum : 0 < (dynamicTableInsert s).num :=
    dynamicTableInsert_num_pos s
  have hfit : (dynamicTableInsert s).num <= (dynamicTableInsert s).size :=
    dynamicTableInsert_capacity_fits s
  omega

Dynamic-table insertion never shrinks the post-state capacity below the old size.

theorem dynamicTableInsert_capacity_ge_size (s : DynamicTableState) :
    s.size <= (dynamicTableInsert s).size := by
  exact dynamicTableInsertSize_ge_size s

The insertion expansion branch leaves post-state capacity at least double the old capacity.


theorem dynamicTableInsert_capacity_ge_double_of_expand (s : DynamicTableState)
    (hfull : ¬ s.num + 1 <= s.size) :
    2 * s.size <= (dynamicTableInsert s).size := by
  rw [dynamicTableInsert_size]
  exact dynamicTableInsertSize_ge_double_of_expand s hfull

Dynamic-table insertion preserves the table-size invariant.

theorem dynamicTableInsert_valid (s : DynamicTableState)
    (_hvalid : DynamicTableState.Valid s) :
    DynamicTableState.Valid (dynamicTableInsert s) := by
  unfold DynamicTableState.Valid dynamicTableInsert
  exact dynamicTableInsertSize_fits s

Allocated size after one deletion. If the post-deletion load is low, shrink toward half the old allocation while keeping enough room for all stored elements.

def dynamicTableDeleteSize (s : DynamicTableState) : Nat :=
  let newNum := s.num - 1
  if 4 * newNum <= s.size then
    max newNum (s.size / 2)
  else
    s.size

First-pass dynamic-table deletion/contraction transition.

def dynamicTableDelete (s : DynamicTableState) : DynamicTableState :=
  { num := s.num - 1, size := dynamicTableDeleteSize s }

First-pass deletion cost: one deletion plus copied elements on contraction.

def dynamicTableDeleteCost (s : DynamicTableState) : Nat :=
  if s.num = 0 then
    0
  else if 4 * (s.num - 1) <= s.size then
    s.num
  else
    1

Insertion leaves a state with nonnegative first-pass potential.

theorem dynamicTableInsert_potential_nonneg (s : DynamicTableState) :
    0 <= dynamicPotential (dynamicTableInsert s) := by
  exact dynamicPotential_nonneg (dynamicTableInsert s)

Deletion leaves a state with nonnegative first-pass potential.

theorem dynamicTableDelete_potential_nonneg (s : DynamicTableState) :
    0 <= dynamicPotential (dynamicTableDelete s) := by
  exact dynamicPotential_nonneg (dynamicTableDelete s)

Deleting from a nonempty dynamic table has positive first-pass actual cost.

theorem dynamicTableDeleteCost_pos_of_nonempty (s : DynamicTableState)
    (hnum : s.num ≠ 0) :
    0 < dynamicTableDeleteCost s := by
  unfold dynamicTableDeleteCost
  simp [hnum]
  by_cases hcontract : 4 * (s.num - 1) <= s.size
  · simp [hcontract]
    omega
  · simp [hcontract]

Deleting from an empty table has zero first-pass cost.

theorem dynamicTableDeleteCost_empty (s : DynamicTableState)
    (hempty : s.num = 0) :
    dynamicTableDeleteCost s = 0 := by
  simp [dynamicTableDeleteCost, hempty]

Dynamic-table deletion has positive cost exactly when the table is nonempty.

theorem dynamicTableDeleteCost_pos_iff_nonempty (s : DynamicTableState) :
    0 < dynamicTableDeleteCost s <-> s.num ≠ 0 := by
  constructor
  · intro hpos hempty
    have hzero : dynamicTableDeleteCost s = 0 :=
      dynamicTableDeleteCost_empty s hempty
    omega
  · intro hnum
    exact dynamicTableDeleteCost_pos_of_nonempty s hnum

Dynamic-table deletion has zero cost exactly when the table is empty.

theorem dynamicTableDeleteCost_zero_iff_empty (s : DynamicTableState) :
    dynamicTableDeleteCost s = 0 <-> s.num = 0 := by
  constructor
  · intro hzero
    by_contra hnum
    have hpos : 0 < dynamicTableDeleteCost s :=
      dynamicTableDeleteCost_pos_of_nonempty s hnum
    omega
  · intro hempty
    exact dynamicTableDeleteCost_empty s hempty

Contracting after deletion costs copying the remaining represented elements.

theorem dynamicTableDeleteCost_of_contract (s : DynamicTableState)
    (hnum : s.num ≠ 0) (hcontract : 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteCost s = s.num := by
  simp [dynamicTableDeleteCost, hnum, hcontract]

Deletion without contraction costs one unit in the first-pass model.

theorem dynamicTableDeleteCost_of_no_contract (s : DynamicTableState)
    (hnum : s.num ≠ 0) (hcontract : ¬ 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteCost s = 1 := by
  simp [dynamicTableDeleteCost, hnum, hcontract]

The contraction branch costs the pre-deletion element count, including empty tables.


theorem dynamicTableDeleteCost_eq_num_of_contract (s : DynamicTableState)
    (hcontract : 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteCost s = s.num := by
  by_cases hnum : s.num = 0
  · rw [hnum]
    exact dynamicTableDeleteCost_empty s hnum
  · exact dynamicTableDeleteCost_of_contract s hnum hcontract

The no-contraction branch costs one unit and necessarily comes from a nonempty table.


theorem dynamicTableDeleteCost_eq_one_of_no_contract (s : DynamicTableState)
    (hcontract : ¬ 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteCost s = 1 := by
  have hnum : s.num ≠ 0 := by
    intro hempty
    apply hcontract
    rw [hempty]
    simp
  exact dynamicTableDeleteCost_of_no_contract s hnum hcontract

The first-pass deletion cost is bounded by the pre-deletion element count.

theorem dynamicTableDeleteCost_le_num (s : DynamicTableState) :
    dynamicTableDeleteCost s <= s.num := by
  unfold dynamicTableDeleteCost
  by_cases hempty : s.num = 0
  · simp [hempty]
  · simp [hempty]
    by_cases hcontract : 4 * (s.num - 1) <= s.size
    · simp [hcontract]
    · simp [hcontract]
      omega

Deletion with low post-deletion load uses the first-pass contraction choice.

theorem dynamicTableDeleteSize_of_contract (s : DynamicTableState)
    (hcontract : 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteSize s = max (s.num - 1) (s.size / 2) := by
  simp [dynamicTableDeleteSize, hcontract]

Deletion without contraction keeps the old allocation size.

theorem dynamicTableDeleteSize_of_no_contract (s : DynamicTableState)
    (hcontract : ¬ 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteSize s = s.size := by
  simp [dynamicTableDeleteSize, hcontract]

The deletion capacity choice can hold the remaining elements of a valid table.

theorem dynamicTableDeleteSize_fits (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    s.num - 1 <= dynamicTableDeleteSize s := by
  unfold DynamicTableState.Valid at hvalid
  unfold dynamicTableDeleteSize
  by_cases hcontract : 4 * (s.num - 1) <= s.size
  · simp [hcontract]
  · simp [hcontract]
    omega

The deletion capacity choice never grows a valid table.

theorem dynamicTableDeleteSize_le_size (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    dynamicTableDeleteSize s <= s.size := by
  unfold DynamicTableState.Valid at hvalid
  unfold dynamicTableDeleteSize
  by_cases hcontract : 4 * (s.num - 1) <= s.size
  · simp [hcontract]
    constructor
    · omega
    · exact Nat.div_le_self s.size 2
  · simp [hcontract]

The deletion contraction branch allocates no more than half the old capacity.


theorem dynamicTableDeleteSize_le_half_of_contract (s : DynamicTableState)
    (hcontract : 4 * (s.num - 1) <= s.size) :
    dynamicTableDeleteSize s <= s.size / 2 := by
  rw [dynamicTableDeleteSize_of_contract s hcontract]
  have hremaining : s.num - 1 <= s.size / 2 := by
    rw [Nat.le_div_iff_mul_le (by decide : 0 < 2)]
    omega
  exact max_le hremaining le_rfl

Dynamic-table deletion decrements the stored-element count, saturating at zero.

theorem dynamicTableDelete_num (s : DynamicTableState) :
    (dynamicTableDelete s).num = s.num - 1 := by
  rfl

Dynamic-table deletion sets the post-state capacity to the deletion capacity choice.

theorem dynamicTableDelete_size (s : DynamicTableState) :
    (dynamicTableDelete s).size = dynamicTableDeleteSize s := by
  rfl

Deletion with low post-deletion load uses the contraction choice as the post-state size.


theorem dynamicTableDelete_size_of_contract (s : DynamicTableState)
    (hcontract : 4 * (s.num - 1) <= s.size) :
    (dynamicTableDelete s).size = max (s.num - 1) (s.size / 2) := by
  rw [dynamicTableDelete_size, dynamicTableDeleteSize_of_contract s hcontract]

Deletion without contraction keeps the old allocation size as the post-state size.


theorem dynamicTableDelete_size_of_no_contract (s : DynamicTableState)
    (hcontract : ¬ 4 * (s.num - 1) <= s.size) :
    (dynamicTableDelete s).size = s.size := by
  rw [dynamicTableDelete_size, dynamicTableDeleteSize_of_no_contract s hcontract]

Dynamic-table deletion never increases the stored-element count.


theorem dynamicTableDelete_num_le (s : DynamicTableState) :
    (dynamicTableDelete s).num <= s.num := by
  rw [dynamicTableDelete_num]
  exact Nat.sub_le s.num 1

Deleting from an empty table leaves the stored-element count at zero.


theorem dynamicTableDelete_num_empty (s : DynamicTableState)
    (hempty : s.num = 0) :
    (dynamicTableDelete s).num = 0 := by
  rw [dynamicTableDelete_num, hempty]

Deleting from a table with at least two elements leaves a positive count.


theorem dynamicTableDelete_num_pos_of_one_lt (s : DynamicTableState)
    (hnum : 1 < s.num) :
    0 < (dynamicTableDelete s).num := by
  rw [dynamicTableDelete_num]
  omega

Deleting from a nonempty table strictly decreases the stored-element count.


theorem dynamicTableDelete_num_lt_of_nonempty (s : DynamicTableState)
    (hnum : s.num ≠ 0) :
    (dynamicTableDelete s).num < s.num := by
  rw [dynamicTableDelete_num]
  omega

Dynamic-table deletion leaves enough capacity for the post-deletion count.

theorem dynamicTableDelete_capacity_fits (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    (dynamicTableDelete s).num <= (dynamicTableDelete s).size := by
  exact dynamicTableDeleteSize_fits s hvalid

Deleting from a valid table with at least two elements leaves positive capacity.

theorem dynamicTableDelete_capacity_pos_of_one_lt (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) (hnum : 1 < s.num) :
    0 < (dynamicTableDelete s).size := by
  have hpost : 0 < (dynamicTableDelete s).num :=
    dynamicTableDelete_num_pos_of_one_lt s hnum
  have hfit : (dynamicTableDelete s).num <= (dynamicTableDelete s).size :=
    dynamicTableDelete_capacity_fits s hvalid
  omega

Dynamic-table deletion never grows the post-state capacity for a valid table.

theorem dynamicTableDelete_capacity_le_size (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    (dynamicTableDelete s).size <= s.size := by
  exact dynamicTableDeleteSize_le_size s hvalid

The deletion contraction branch leaves post-state capacity no more than half the old capacity.


theorem dynamicTableDelete_capacity_le_half_of_contract (s : DynamicTableState)
    (hcontract : 4 * (s.num - 1) <= s.size) :
    (dynamicTableDelete s).size <= s.size / 2 := by
  rw [dynamicTableDelete_size]
  exact dynamicTableDeleteSize_le_half_of_contract s hcontract

Dynamic-table deletion/contraction preserves the table-size invariant.

theorem dynamicTableDelete_valid (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    DynamicTableState.Valid (dynamicTableDelete s) := by
  unfold DynamicTableState.Valid dynamicTableDelete
  exact dynamicTableDeleteSize_fits s hvalid

Concrete insertion amortized cost unfolds to actual plus potential change.

theorem dynamicTableInsert_amortizedCost_eq (s : DynamicTableState) :
    dynamicTableAmortizedCost s (dynamicTableInsert s) (dynamicTableInsertCost s) =
      Int.ofNat (dynamicTableInsertCost s) +
        dynamicPotential (dynamicTableInsert s) - dynamicPotential s := by
  rfl

Concrete deletion amortized cost unfolds to actual plus potential change.

theorem dynamicTableDelete_amortizedCost_eq (s : DynamicTableState) :
    dynamicTableAmortizedCost s (dynamicTableDelete s) (dynamicTableDeleteCost s) =
      Int.ofNat (dynamicTableDeleteCost s) +
        dynamicPotential (dynamicTableDelete s) - dynamicPotential s := by
  rfl

The abstract amortized transition cost is bounded by actual cost plus the post-operation potential, because the pre-operation potential is nonnegative.

theorem dynamicTable_amortizedBound
    (before after : DynamicTableState) (actual : Nat) :
    dynamicTableAmortizedCost before after actual <=
      Int.ofNat actual + dynamicPotential after := by
  have hnonneg : 0 <= dynamicPotential before := dynamicPotential_nonneg before
  unfold dynamicTableAmortizedCost
  omega

The concrete first-pass insertion transition instantiates the generic bound.

theorem dynamicTableInsert_amortizedBound (s : DynamicTableState) :
    dynamicTableAmortizedCost s (dynamicTableInsert s) (dynamicTableInsertCost s) <=
      Int.ofNat (dynamicTableInsertCost s) + dynamicPotential (dynamicTableInsert s) := by
  exact dynamicTable_amortizedBound s (dynamicTableInsert s) (dynamicTableInsertCost s)

The concrete first-pass deletion transition instantiates the generic bound.

theorem dynamicTableDelete_amortizedBound (s : DynamicTableState) :
    dynamicTableAmortizedCost s (dynamicTableDelete s) (dynamicTableDeleteCost s) <=
      Int.ofNat (dynamicTableDeleteCost s) + dynamicPotential (dynamicTableDelete s) := by
  exact dynamicTable_amortizedBound s (dynamicTableDelete s) (dynamicTableDeleteCost s)

Total array-copy cost (amortized argument)

The total cost of element copying across n insertions into an initially empty dynamic table is bounded by 2n. Each expansion copies at most as many elements as were inserted since the last expansion, and the doubling strategy ensures that the sum of all copy costs telescopes to at most twice the final number of elements.

This is the textbook CLRS aggregate-analysis result.


theorem expansionCopyBound (n : Nat) : n + (Nat.log 2 n).succ ≤ 2 * n + 1 := by
  by_cases hn : n < 2
  · have hlog : Nat.log 2 n = 0 := Nat.log_of_lt hn
    simp [hlog]
    omega
  · have hn0 : n ≠ 0 := by omega
    have hlog_lt_n : Nat.log 2 n < n := Nat.log_lt_self 2 hn0
    omega

end Chapter17end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_16.Section_16_4_Dynamic_Tables.Section_16_4_Mutable_Array_Tables

CLRS Section 16.4 - Mutable-array dynamic tables and sharper load-factor potential

This nested section refines the size-level dynamic-table model of Section_16_4_Dynamic_Tables in two independent directions requested by CLRS Section 16.4.

Sub-issue A - mutable-array copying. We model the physical array-copy step that a real dynamic table performs on reallocation with growTo, an actual Array operation that allocates a larger backing store and copies every existing element. A concrete ArrayTable structure carries a backing Array together with its capacity, and its insertion projects onto the abstract dynamicTableInsert transition and matches the abstract dynamicTableInsertCost. The connecting theorem insert_copy_cost splits the abstract cost into copied elements plus one write, and dynamicTableCopyCount_eq_growCopyCost identifies the abstract copy count with the number of elements a physical growTo moves.

Sub-issue B - sharper load-factor potential. We define the CLRS load-factor potential Φ, whose value depends on whether the load factor α = num / size is at least 1/2, via a division-free doubled integer form sharpPotentialZ (Ψ = 2Φ) and its rational wrapper sharpPotential. A sharper contraction sharpDelete halves the table to exactly restore α = 1/2. We prove constant amortized bounds (≤ 3, the CLRS result) for both insertion and deletion, plus the CLRS guarantee that α is exactly 1/2 (hence at least 1/2) immediately after a contraction.

Main results:

Definition growTo: allocate a larger array and copy every element.
Theorems growTo_size and growTo_toList: the physical copy has the requested length and preserves every copied element in order.
Theorems arrayTable_toState_insert and arrayTable_insertCost_eq: the concrete mutable-array insertion refines the abstract transition and cost.
Theorem insert_copy_cost: abstract insertion cost equals copied elements plus one write.
Theorem dynamicTableCopyCount_eq_growCopyCost: the abstract copy count equals the number of elements a physical growTo moves.
Definitions sharpPotentialZ, sharpPotential, loadFactor: the CLRS load-factor potential and load factor.
Theorems sharpPotentialZ_nonneg and sharpPotential_nonneg: the sharper potential is nonnegative.
Theorems sharpInsert_amortized_le_three and sharpDelete_amortized_le_three: constant (≤ 3) amortized cost for insertion and deletion under the load-factor potential.
Theorem sharpDelete_loadFactor_eq_half_of_contract and its corollary sharpDelete_loadFactor_ge_half_of_contract: the load factor is exactly 1/2, hence at least 1/2, right after a contraction.
Definition TableOp (insert / delete) with tableStep, tableOpCost, execTrace, and traceCost: an executable interleaved insert/delete trace model.
Theorem tableOp_amortized_le_three: every single operation has amortized cost at most 3 under the load-factor potential.
Theorem trace_amortized_le: the whole-trace amortized cost telescopes, so a valid trace of n operations costs at most 3n + Φ(s₀).
Theorem trace_totalCost_le_three_mul: starting from the empty table, a trace of n operations has total actual cost at most 3n.

Notation conventions used in this section:

s : an abstract DynamicTableState (stored count num, capacity size)
t : a concrete ArrayTable
α : load factor num / size
Φ : CLRS load-factor potential; Ψ = 2Φ is its division-free integer form

Current gaps:

General allocator / RAM cost semantics remain out of scope.

namespace CLRSnamespace Chapter17

Sub-issue A: an actual array copy operation

Physical array-copy step of a dynamic table: allocate an array of length newSize, copy every element of old, and pad the remaining slots with dflt. This models CLRS's "copy the items into the new table" operation on reallocation.

def growTo {α : Type u} (old : Array α) (newSize : Nat) (dflt : α) : Array α :=
  old ++ (List.replicate (newSize - old.size) dflt).toArray

The physical copy preserves every existing element in order: its list of elements is exactly old followed by the padding. This certifies that growTo is a faithful copy rather than an arbitrary array.

theorem growTo_toList {α : Type u} (old : Array α) (newSize : Nat) (dflt : α) :
    (growTo old newSize dflt).toList
      = old.toList ++ List.replicate (newSize - old.size) dflt := by
  simp [growTo]

A copy into a table of size at least old.size has that size.


theorem growTo_size {α : Type u} (old : Array α) (newSize : Nat) (dflt : α)
    (h : old.size ≤ newSize) : (growTo old newSize dflt).size = newSize := by
  unfold growTo
  rw [Array.size_append]
  simp
  omega

Number of elements a physical copy of old moves: one per existing element. This is the per-element copy cost that CLRS charges on reallocation.

def growCopyCost {α : Type u} (old : Array α) : Nat := old.size

A concrete mutable-array dynamic table: a backing Array whose length is the allocated capacity, with the invariant that it is never overfilled. The number of stored elements is elements.size and the capacity is capacity.

Backing store; its length is the number of stored elements.

Allocated capacity.

The table never stores more elements than its capacity.

              structure ArrayTable (α : Type u) where  elements : Array α  capacity : Nat  hcap : elements.size ≤ capacity

The abstract size-level state of a concrete mutable-array table.

def ArrayTable.toState {α : Type u} (t : ArrayTable α) : DynamicTableState :=
  { num := t.elements.size, size := t.capacity }

Concrete mutable-array insertion of x. If there is spare capacity, write x in place; otherwise reallocate to a capacity that both fits the new element and at least doubles the old allocation (the value padded into new slots is x itself).


def ArrayTable.insert {α : Type u} (t : ArrayTable α) (x : α) : ArrayTable α :=
  if h : t.elements.size + 1 ≤ t.capacity then
    { elements := t.elements.push x
      capacity := t.capacity
      hcap := by rw [Array.size_push]; exact h }
  else
    { elements := t.elements.push x
      capacity := max (t.elements.size + 1) (2 * t.capacity)
      hcap := by rw [Array.size_push]; exact le_max_left _ _ }

Concrete insertion cost: one write, plus one copy per existing element on reallocation.

def ArrayTable.insertCost {α : Type u} (t : ArrayTable α) : Nat :=
  if t.elements.size + 1 ≤ t.capacity then 1 else t.elements.size + 1

The concrete mutable-array insertion refines the abstract size-level transition: its abstract state is exactly dynamicTableInsert of the abstract state.

theorem arrayTable_toState_insert {α : Type u} (t : ArrayTable α) (x : α) :
    (t.insert x).toState = dynamicTableInsert t.toState := by
  by_cases h : t.elements.size + 1 ≤ t.capacity
  · simp only [ArrayTable.insert, ArrayTable.toState, dynamicTableInsert,
      dynamicTableInsertSize, dif_pos h, if_pos h, Array.size_push]
  · simp only [ArrayTable.insert, ArrayTable.toState, dynamicTableInsert,
      dynamicTableInsertSize, dif_neg h, if_neg h, Array.size_push]

The concrete insertion cost matches the abstract size-level insertion cost.

theorem arrayTable_insertCost_eq {α : Type u} (t : ArrayTable α) :
    t.insertCost = dynamicTableInsertCost t.toState := by
  unfold ArrayTable.insertCost dynamicTableInsertCost ArrayTable.toState
  by_cases h : t.elements.size + 1 ≤ t.capacity <;> simp [h]

Number of elements a real reallocation copies for one abstract insertion: none when there is spare capacity, otherwise every stored element.

def dynamicTableCopyCount (s : DynamicTableState) : Nat :=
  if s.num + 1 ≤ s.size then 0 else s.num

Insertion-cost accounting matches copy calls. The abstract insertion cost is exactly the number of elements physically copied plus the single write of the new element. This is CLRS's decomposition of TABLE-INSERT cost into copy work and the constant insert step.

theorem insert_copy_cost (s : DynamicTableState) :
    dynamicTableInsertCost s = dynamicTableCopyCount s + 1 := by
  unfold dynamicTableInsertCost dynamicTableCopyCount
  by_cases h : s.num + 1 ≤ s.size <;> simp [h]

At a reallocation, the abstract copy count equals the number of elements a physical growTo moves out of the old backing store: one per stored element.


theorem dynamicTableCopyCount_eq_growCopyCost {α : Type u} (s : DynamicTableState)
    (t : ArrayTable α) (hcount : t.elements.size = s.num)
    (hexpand : ¬ s.num + 1 ≤ s.size) :
    dynamicTableCopyCount s = growCopyCost t.elements := by
  unfold dynamicTableCopyCount growCopyCost
  rw [if_neg hexpand, hcount]

Concrete form of insert_copy_cost for a real ArrayTable at a reallocation: the insertion cost is the number of elements the physical copy moves plus one write.

theorem arrayTable_insert_copy_cost_of_expand {α : Type u} (t : ArrayTable α)
    (hfull : ¬ t.elements.size + 1 ≤ t.capacity) :
    t.insertCost = growCopyCost t.elements + 1 := by
  unfold ArrayTable.insertCost growCopyCost
  simp [hfull]

Sub-issue B: the sharper load-factor potential

Load factor α = num / size of a dynamic table, as a rational number (with the Mathlib convention that division by zero yields zero for the empty allocation).

def loadFactor (s : DynamicTableState) : ℚ := (s.num : ℚ) / (s.size : ℚ)

Doubled, division-free integer form Ψ = 2Φ of the CLRS load-factor potential. When α ≥ 1/2 (equivalently size ≤ 2 * num) it is 4 * num - 2 * size; otherwise it is size - 2 * num. Doubling clears the size / 2 that appears in the textbook potential so that the branch algebra stays over the integers.

def sharpPotentialZ (s : DynamicTableState) : Int :=
  if s.size ≤ 2 * s.num then
    4 * (s.num : Int) - 2 * (s.size : Int)
  else
    (s.size : Int) - 2 * (s.num : Int)

The CLRS load-factor potential Φ = Ψ / 2: it is 2 * num - size when α ≥ 1/2 and size / 2 - num when α < 1/2.

def sharpPotential (s : DynamicTableState) : ℚ := (sharpPotentialZ s : ℚ) / 2

The doubled load-factor potential is nonnegative.

theorem sharpPotentialZ_nonneg (s : DynamicTableState) : 0 ≤ sharpPotentialZ s := by
  unfold sharpPotentialZ
  split <;> omega

The CLRS load-factor potential is nonnegative.

theorem sharpPotential_nonneg (s : DynamicTableState) : 0 ≤ sharpPotential s := by
  unfold sharpPotential
  apply div_nonneg _ (by norm_num)
  exact_mod_cast sharpPotentialZ_nonneg s

Sharper contraction capacity: on contraction, halve the table to exactly twice the post-deletion count so that the resulting load factor is exactly 1/2. Otherwise keep the current capacity.

def sharpDeleteSize (s : DynamicTableState) : Nat :=
  if 4 * (s.num - 1) ≤ s.size then 2 * (s.num - 1) else s.size

Sharper deletion/contraction transition.

def sharpDelete (s : DynamicTableState) : DynamicTableState :=
  { num := s.num - 1, size := sharpDeleteSize s }

Sharper deletion cost: one delete, plus one copy per remaining element on contraction.

def sharpDeleteCost (s : DynamicTableState) : Nat :=
  if s.num = 0 then 0
  else if 4 * (s.num - 1) ≤ s.size then s.num
  else 1

On contraction the sharper capacity halves to twice the post-deletion count.


theorem sharpDeleteSize_of_contract (s : DynamicTableState)
    (hc : 4 * (s.num - 1) ≤ s.size) :
    sharpDeleteSize s = 2 * (s.num - 1) := by
  unfold sharpDeleteSize; rw [if_pos hc]

Without contraction the sharper capacity is unchanged.


theorem sharpDeleteSize_of_no_contract (s : DynamicTableState)
    (hc : ¬ 4 * (s.num - 1) ≤ s.size) :
    sharpDeleteSize s = s.size := by
  unfold sharpDeleteSize; rw [if_neg hc]

Sharper deletion decrements the stored-element count, saturating at zero.

theorem sharpDelete_num (s : DynamicTableState) : (sharpDelete s).num = s.num - 1 := rfl

Sharper deletion sets the post-state capacity to the sharper capacity choice.

theorem sharpDelete_size (s : DynamicTableState) :
    (sharpDelete s).size = sharpDeleteSize s := rfl

Sharper deletion/contraction preserves the table-size invariant.


theorem sharpDelete_valid (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    DynamicTableState.Valid (sharpDelete s) := by
  unfold DynamicTableState.Valid at hvalid ⊢
  unfold sharpDelete sharpDeleteSize
  by_cases hc : 4 * (s.num - 1) ≤ s.size
  · rw [if_pos hc]
    simpa [mul_comm] using Nat.mul_le_mul (le_refl (s.num - 1)) (by decide : 1 ≤ 2)
  · rw [if_neg hc]
    exact Nat.le_trans (Nat.sub_le s.num 1) hvalid

Doubled insertion amortized bound. For a valid table, twice the actual insertion cost plus the change in the doubled load-factor potential is at most 6. Dividing by two gives the CLRS amortized bound of 3.


theorem sharpInsert_doubledAmortized_le_six (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    2 * (dynamicTableInsertCost s : Int)
      + sharpPotentialZ (dynamicTableInsert s) - sharpPotentialZ s ≤ 6 := by
  unfold DynamicTableState.Valid at hvalid
  by_cases hfit : s.num + 1 ≤ s.size
  · have hc : dynamicTableInsertCost s = 1 := dynamicTableInsertCost_of_fits s hfit
    have hsz : (dynamicTableInsert s).size = s.size := dynamicTableInsert_size_of_fits s hfit
    have hn : (dynamicTableInsert s).num = s.num + 1 := dynamicTableInsert_num s
    rw [hc]
    unfold sharpPotentialZ
    rw [hsz, hn]
    split <;> split <;> omega
  · have hfull := hfit
    have hc : dynamicTableInsertCost s = s.num + 1 := dynamicTableInsertCost_of_expand s hfull
    have hn : (dynamicTableInsert s).num = s.num + 1 := dynamicTableInsert_num s
    have hnum : s.num = s.size := by omega
    rcases Nat.eq_zero_or_pos s.size with hz | hpos
    · have hsz : (dynamicTableInsert s).size = 1 := by
        rw [dynamicTableInsert_size_of_expand s hfull, hnum, hz]; decide
      rw [hc]
      unfold sharpPotentialZ
      rw [hsz, hn]
      split <;> split <;> omega
    · have hsz : (dynamicTableInsert s).size = 2 * s.size := by
        rw [dynamicTableInsert_size_of_expand s hfull, hnum, max_eq_right (by omega)]
      rw [hc]
      unfold sharpPotentialZ
      rw [hsz, hn]
      split <;> split <;> omega

Insertion is O(1) amortized under the load-factor potential. For a valid table, the amortized cost of TABLE-INSERT - actual cost plus the change in the CLRS load-factor potential Φ - is at most 3. In particular this covers the low-load case α < 1, where the actual cost is a single write.

This is CLRS Theorem 16.4-style amortized analysis for insertion.


theorem sharpInsert_amortized_le_three (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    (dynamicTableInsertCost s : ℚ)
      + sharpPotential (dynamicTableInsert s) - sharpPotential s ≤ 3 := by
  have h := sharpInsert_doubledAmortized_le_six s hvalid
  have hq : (2 * (dynamicTableInsertCost s : Int)
      + sharpPotentialZ (dynamicTableInsert s) - sharpPotentialZ s : ℚ) ≤ (6 : ℚ) := by
    exact_mod_cast h
  unfold sharpPotential
  push_cast at hq
  linarith

Doubled deletion amortized bound. For a valid nonempty table, twice the actual deletion cost plus the change in the doubled load-factor potential is at most 6. Dividing by two gives the CLRS amortized bound of 3.


theorem sharpDelete_doubledAmortized_le_six (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) (hne : s.num ≠ 0) :
    2 * (sharpDeleteCost s : Int)
      + sharpPotentialZ (sharpDelete s) - sharpPotentialZ s ≤ 6 := by
  unfold DynamicTableState.Valid at hvalid
  by_cases hc : 4 * (s.num - 1) ≤ s.size
  · have hcost : sharpDeleteCost s = s.num := by
      unfold sharpDeleteCost; simp [hne, hc]
    have hsz : (sharpDelete s).size = 2 * (s.num - 1) := by
      rw [sharpDelete_size, sharpDeleteSize_of_contract s hc]
    have hn : (sharpDelete s).num = s.num - 1 := sharpDelete_num s
    rw [hcost]
    unfold sharpPotentialZ
    rw [hsz, hn]
    split <;> split <;> omega
  · have hcost : sharpDeleteCost s = 1 := by
      unfold sharpDeleteCost; simp [hne, hc]
    have hsz : (sharpDelete s).size = s.size := by
      rw [sharpDelete_size, sharpDeleteSize_of_no_contract s hc]
    have hn : (sharpDelete s).num = s.num - 1 := sharpDelete_num s
    rw [hcost]
    unfold sharpPotentialZ
    rw [hsz, hn]
    split <;> split <;> omega

Deletion is O(1) amortized under the load-factor potential. For a valid nonempty table, the amortized cost of TABLE-DELETE - actual cost plus the change in the CLRS load-factor potential Φ - is at most 3. In particular this covers the high-load case α > 1/4, where the actual cost is a single delete.

This is CLRS Theorem 16.4-style amortized analysis for deletion.


theorem sharpDelete_amortized_le_three (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) (hne : s.num ≠ 0) :
    (sharpDeleteCost s : ℚ)
      + sharpPotential (sharpDelete s) - sharpPotential s ≤ 3 := by
  have h := sharpDelete_doubledAmortized_le_six s hvalid hne
  have hq : (2 * (sharpDeleteCost s : Int)
      + sharpPotentialZ (sharpDelete s) - sharpPotentialZ s : ℚ) ≤ (6 : ℚ) := by
    exact_mod_cast h
  unfold sharpPotential
  push_cast at hq
  linarith

Load-factor guarantee after contraction. When a table with at least two elements contracts, the sharper contraction restores the load factor to exactly 1/2: the new count num - 1 sits in a table of capacity 2 * (num - 1).

This is the CLRS invariant that a contraction leaves the table half full.


theorem sharpDelete_loadFactor_eq_half_of_contract (s : DynamicTableState)
    (hnum : 2 ≤ s.num) (hc : 4 * (s.num - 1) ≤ s.size) :
    loadFactor (sharpDelete s) = 1 / 2 := by
  unfold loadFactor
  rw [sharpDelete_num, sharpDelete_size, sharpDeleteSize_of_contract s hc]
  push_cast
  have ha : (s.num : ℚ) - 1 ≠ 0 := by
    intro h
    have hq : (s.num : ℚ) = 1 := by linarith
    have hn : s.num = 1 := by exact_mod_cast hq
    omega
  field_simp [ha]

The load factor is at least 1/2 immediately after a contraction, a direct corollary of sharpDelete_loadFactor_eq_half_of_contract.


theorem sharpDelete_loadFactor_ge_half_of_contract (s : DynamicTableState)
    (hnum : 2 ≤ s.num) (hc : 4 * (s.num - 1) ≤ s.size) :
    1 / 2 ≤ loadFactor (sharpDelete s) := by
  rw [sharpDelete_loadFactor_eq_half_of_contract s hnum hc]

Interleaved insert/delete trace amortization

A dynamic-table operation: an insertion or a deletion.

inductive TableOp where
  | insert
  | delete
  deriving DecidableEq

Apply one operation to an abstract dynamic-table state.

def tableStep (op : TableOp) (s : DynamicTableState) : DynamicTableState :=
  match op with
  | .insert => dynamicTableInsert s
  | .delete => sharpDelete s

Actual cost of one operation in the abstract model.

def tableOpCost (op : TableOp) (s : DynamicTableState) : ℚ :=
  match op with
  | .insert => (dynamicTableInsertCost s : ℚ)
  | .delete => (sharpDeleteCost s : ℚ)

The final state after executing a whole trace, one operation at a time.

def execTrace : List TableOp → DynamicTableState → DynamicTableState
  | [], s => s
  | op :: rest, s => execTrace rest (tableStep op s)

The total actual cost of a whole trace.

def traceCost : List TableOp → DynamicTableState → ℚ
  | [], _ => 0
  | op :: rest, s => tableOpCost op s + traceCost rest (tableStep op s)

Every operation preserves the table-size invariant.

theorem tableStep_valid (op : TableOp) (s : DynamicTableState)
    (h : DynamicTableState.Valid s) : DynamicTableState.Valid (tableStep op s) := by
  cases op with
  | insert => simpa [tableStep] using dynamicTableInsert_valid s h
  | delete => simpa [tableStep] using sharpDelete_valid s h

Deleting from an empty table is free and leaves a table of capacity zero, so its amortized cost is trivially at most 3.


theorem sharpDelete_amortized_le_three_of_empty (s : DynamicTableState) (hempty : s.num = 0) :
    (sharpDeleteCost s : ℚ) + sharpPotential (sharpDelete s) - sharpPotential s ≤ 3 := by
  have hcost : (sharpDeleteCost s : ℚ) = 0 := by
    unfold sharpDeleteCost
    simp [hempty]
  have hfinal : sharpDelete s = { num := 0, size := 0 } := by
    unfold sharpDelete sharpDeleteSize
    rw [hempty]
    simp
  have hΦ0 : sharpPotential { num := 0, size := 0 } = 0 := by
    unfold sharpPotential sharpPotentialZ
    norm_num
  have hpot : sharpPotential (sharpDelete s) = 0 := by
    rw [hfinal, hΦ0]
  have hnonneg : 0 ≤ sharpPotential s := sharpPotential_nonneg s
  linarith

Single-operation amortized bound. Every dynamic-table operation — an insertion or a deletion — has amortized cost at most 3 under the CLRS load-factor potential: actual cost plus the potential change is ≤ 3.

theorem tableOp_amortized_le_three (op : TableOp) (s : DynamicTableState)
    (hvalid : DynamicTableState.Valid s) :
    tableOpCost op s + sharpPotential (tableStep op s) - sharpPotential s ≤ 3 := by
  cases op with
  | insert => simpa [tableOpCost, tableStep] using sharpInsert_amortized_le_three s hvalid
  | delete =>
      by_cases hne : s.num = 0
      · simpa [tableOpCost, tableStep] using sharpDelete_amortized_le_three_of_empty s hne
      · simpa [tableOpCost, tableStep] using sharpDelete_amortized_le_three s hvalid hne

Whole-trace amortized bound. The per-operation amortized bounds telescope: for a valid initial table, a trace of n insertions and deletions has total amortized cost (actual cost plus the potential change) at most 3n. This is the interleaved insert/delete amortized analysis of CLRS Section 16.4.

theorem trace_amortized_le (s : DynamicTableState) (hvalid : DynamicTableState.Valid s)
    (ops : List TableOp) :
    traceCost ops s + sharpPotential (execTrace ops s) - sharpPotential s ≤ 3 * (ops.length : ℚ) := by
  induction ops generalizing s hvalid with
  | nil => simp [traceCost, execTrace]
  | cons op rest ih =>
      have hstep_valid : DynamicTableState.Valid (tableStep op s) := tableStep_valid op s hvalid
      have hstep : tableOpCost op s + sharpPotential (tableStep op s) - sharpPotential s ≤ 3 :=
        tableOp_amortized_le_three op s hvalid
      have hrest := ih (tableStep op s) hstep_valid
      calc
        traceCost (op :: rest) s + sharpPotential (execTrace (op :: rest) s) - sharpPotential s
            = tableOpCost op s + traceCost rest (tableStep op s)
                + sharpPotential (execTrace rest (tableStep op s)) - sharpPotential s := rfl
        _ = tableOpCost op s
              + (traceCost rest (tableStep op s)
                + sharpPotential (execTrace rest (tableStep op s))
                - sharpPotential (tableStep op s))
              + (sharpPotential (tableStep op s) - sharpPotential s) := by ring
        _ ≤ 3 + 3 * (rest.length : ℚ) := by linarith [hstep, hrest]
        _ = 3 * ((op :: rest).length : ℚ) := by
            simp [List.length_cons]
            ring

The empty table has zero potential.

theorem sharpPotential_empty : sharpPotential { num := 0, size := 0 } = 0 := by
  unfold sharpPotential sharpPotentialZ
  norm_num

The empty table satisfies the table-size invariant.

theorem emptyState_valid : DynamicTableState.Valid { num := 0, size := 0 } := by
  unfold DynamicTableState.Valid
  decide

Interleaved trace cost is linear. Starting from the empty table, any trace of n insertions and deletions has total actual cost at most 3n: the CLRS O(1) amortized bound for a sequence of dynamic-table operations.

theorem trace_totalCost_le_three_mul (ops : List TableOp) :
    traceCost ops { num := 0, size := 0 } ≤ 3 * (ops.length : ℚ) := by
  have h := trace_amortized_le { num := 0, size := 0 } emptyState_valid ops
  have hfinal : 0 ≤ sharpPotential (execTrace ops { num := 0, size := 0 }) :=
    sharpPotential_nonneg _
  have hinit : sharpPotential { num := 0, size := 0 } = 0 := sharpPotential_empty
  linarith

end Chapter17end CLRS

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework.Section_16_2_Stack_And_Counter.StackExecution
import CLRSLean.Chapter_17
import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework
import CLRSLean.FourthEdition.Chapter_16.Section_16_2_The_Accounting_Method
import CLRSLean.FourthEdition.Chapter_16.Section_16_3_The_Potential_Method
import CLRSLean.FourthEdition.Chapter_16.Section_16_4_Dynamic_Tables
import CLRSLean.FourthEdition.Chapter_16.Section_16_4_Dynamic_Tables.Section_16_4_Mutable_Array_Tables

Current source

Sections 16.1--16.4 are native fourth-edition sections. Each method now has a canonical reader page: aggregate analysis, the accounting method, the potential method, and dynamic tables. The stack and counter proofs are presented with the accounting method. Declarations retain the legacy CLRS.Chapter17 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_17 and CLRSLean.Chapter_17.Section_17_* forward to these sources.

Implementation details

The supporting implementation pages remain available outside the main sidebar:

Coverage boundary

The native sections supply the fourth-edition amortized-analysis facade (§16.1 aggregate analysis, §16.2 the accounting method, §16.3 the potential method, §16.4 dynamic tables). The mixed stack executor returns the final stack, removed values per command, and actual successful PUSH/POP counts. Its exact conservation law proves that from empty, total popped cells cannot exceed pushed cells, even with arbitrary interleaved MULTIPOP requests. Counting one event per command and per pushed/popped cell gives at most 3n charged work. This excludes allocation and element-representation internals.

§16.4 includes the sharper load-factor potential with constant ≤ 3 insert/delete amortized bounds and the interleaved insert/delete trace amortized analysis (≤ 3n total cost from the empty table). The namespace migration CLRS.Chapter17 → CLRS.Chapter16 is tracked chapter by chapter.

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

CLRS, fourth edition · Chapter 16 of 35