Imports

import CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework

CLRS Section 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