CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 8. Sorting in Linear Time

Chapter 8 — Sorting in Linear Time

CLRS, fourth edition · Lean 4 formalization

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

Imports

import Mathlib

open scoped BigOperators

8.1. Lower Bounds for Sorting

This section formalizes the decision-tree lower bound of CLRS §8.1: any comparison-based sorting algorithm on n distinct elements performs at least log₂(n!) comparisons in the worst case, which is Ω(n log n).

A comparison sort on n elements is modelled as a binary decision tree SortTree n. Internal nodes compare the elements stored in two positions; leaves are labelled with an output permutation of Fin n. Running the tree on an input arrangement π : Equiv.Perm (Fin n) follows the outcome of each comparison and reaches a leaf. A tree CorrectSort-sorts every input if the leaf reached on π is labelled with the sorted arrangement π⁻¹.

The lower bound then follows from three independent facts:

Correctness needs n! leaves: distinct input arrangements π have distinct sorted arrangements π⁻¹, so a correct tree maps the n! permutations injectively to distinct leaves (run_injective_of_correctSort + card_le_leafCount_of_injective give factorial_le_leafCount_of_correctSort).
A binary tree of height h has at most 2^h leaves (leafCount_le_two_pow_height), so n! ≤ 2^h and hence h ≥ log₂(n!) (height_le_logb_factorial).
log₂(n!) ≥ (n/2)·log₂ n via the pairing bound (n!)² ≥ nⁿ: the factors k and n+1-k multiply to at least n (factorial_sq_ge_pow_self + logb_factorial_ge_half_mul_logb).

Combining these yields the structural-height theorem comparisonSort_worstCase_lowerBound. The companion Execution module adds a counted interpreter and proves comparisonSort_exists_run_lowerBound: for every correct sorter on n ≥ 2 distinct elements, some input actually performs at least (n/2)·log₂ n comparisons, even when other branches are unreachable.

Main results

Theorem leafCount_le_two_pow_height: a binary tree of height h has at most 2^h leaves
Theorem run_injective_of_correctSort: a correct sorter maps distinct inputs to distinct leaves
Theorem factorial_le_leafCount_of_correctSort: a correct sorter has at least n! leaves
Theorem height_le_logb_factorial: log₂(n!) ≤ h
Theorem factorial_sq_ge_pow_self: (n!)² ≥ nⁿ
Theorem logb_factorial_ge_half_mul_logb: log₂(n!) ≥ (n/2)·log₂ n
Theorem comparisonSort_worstCase_lowerBound: the historical structural-height lower bound.
Theorem comparisonSort_exists_run_lowerBound in Execution: an actual input attains at least (n/2)·log₂ n comparisons.

Current gaps

None for the decision-tree model of comparison sorts over Fin n. The companion interpreter charges each executed comparison once. Other RAM bookkeeping and non-comparison lower-bound analysis for counting/radix/bucket sort remain outside this model.

namespace CLRSnamespace Chapter08

Comparison decision trees

A binary decision tree for comparison sorting of n distinct elements. An internal node compares the elements in positions i and j (0-indexed) and branches on the outcome; a leaf is labelled with the claimed output permutation. The number of comparisons performed on a run is the number of internal nodes on its root-to-leaf path.

inductive SortTree (n : ℕ) : Type where
  | leaf : Equiv.Perm (Fin n) → SortTree n
  | node : (i j : Fin n) → SortTree n → SortTree n → SortTree n

The number of leaves of a decision tree, counting each leaf node.

def SortTree.leafCount : SortTree n → ℕ
  | leaf _ => 1
  | node _ _ l r => l.leafCount + r.leafCount

The height of a decision tree: the largest number of internal nodes on a root-to-leaf path. It bounds every run from above, but an infeasible branch can make it larger than the maximum reachable comparison count.

def SortTree.height : SortTree n → ℕ
  | leaf _ => 0
  | node _ _ l r => 1 + max l.height r.height

t is a leaf node occurring in the tree T.

def SortTree.isLeafNodeOf (T : SortTree n) (t : SortTree n) : Prop :=
  match T with
  | leaf p => t = SortTree.leaf p
  | node _ _ l r => SortTree.isLeafNodeOf l t ∨ SortTree.isLeafNodeOf r t

A binary tree of height h has at most 2^h leaves.


theorem leafCount_le_two_pow_height (T : SortTree n) : T.leafCount ≤ 2 ^ T.height := by
  induction T with
  | leaf p =>
      simp [SortTree.leafCount, SortTree.height]
  | node _ _ l r ih_l ih_r =>
      have hmax_l : l.height ≤ max l.height r.height := Nat.le_max_left l.height r.height
      have hmax_r : r.height ≤ max l.height r.height := Nat.le_max_right l.height r.height
      have hpow_l : 2 ^ l.height ≤ 2 ^ max l.height r.height :=
        pow_le_pow_right₀ (by norm_num : 1 ≤ 2) hmax_l
      have hpow_r : 2 ^ r.height ≤ 2 ^ max l.height r.height :=
        pow_le_pow_right₀ (by norm_num : 1 ≤ 2) hmax_r
      have hsum_le : l.leafCount + r.leafCount ≤ 2 ^ l.height + 2 ^ r.height :=
        Nat.add_le_add ih_l ih_r
      have hsum : 2 ^ l.height + 2 ^ r.height ≤ 2 * 2 ^ max l.height r.height := by
        rw [two_mul]
        exact Nat.add_le_add hpow_l hpow_r
      have hgoal : l.leafCount + r.leafCount ≤ 2 ^ (max l.height r.height + 1) := by
        calc
          l.leafCount + r.leafCount ≤ 2 ^ l.height + 2 ^ r.height := hsum_le
          _ ≤ 2 * 2 ^ max l.height r.height := hsum
          _ = 2 ^ (max l.height r.height + 1) := by
            rw [pow_succ]
            ring_nf
      simpa [SortTree.leafCount, SortTree.height, Nat.add_comm] using hgoal

Run the decision tree on the input arrangement π (position k holds the value π k). At an internal node comparing positions i and j, take the left branch when π i ≤ π j. Returns the leaf reached.

def SortTree.run (T : SortTree n) (π : Equiv.Perm (Fin n)) : SortTree n :=
  match T with
  | leaf p => SortTree.leaf p
  | node i j l r =>
      if π i ≤ π j then SortTree.run l π else SortTree.run r π

A decision tree correctly sorts every input if, on input arrangement π, it reaches the leaf labelled with the sorted arrangement π⁻¹ (the unique permutation σ with π (σ k) = k).

def CorrectSort (T : SortTree n) : Prop :=
  ∀ π : Equiv.Perm (Fin n), SortTree.run T π = SortTree.leaf (π⁻¹)

A correct sorter maps distinct input arrangements to distinct leaves.


theorem run_injective_of_correctSort {T : SortTree n} (hT : CorrectSort T) :
    Function.Injective (SortTree.run T) := by
  intro π₁ π₂ h
  have h1 : SortTree.run T π₁ = SortTree.leaf (π₁⁻¹) := hT π₁
  have h2 : SortTree.run T π₂ = SortTree.leaf (π₂⁻¹) := hT π₂
  have hleaves : SortTree.leaf (π₁⁻¹) = SortTree.leaf (π₂⁻¹) := by
    rw [← h1, ← h2]
    exact h
  have hinv : π₁⁻¹ = π₂⁻¹ := by
    injection hleaves
  calc
    π₁ = (π₁⁻¹)⁻¹ := by simp
    _ = (π₂⁻¹)⁻¹ := by rw [hinv]
    _ = π₂ := by simp

The run of a tree always ends at a leaf of that tree.

theorem run_isLeafNodeOf (T : SortTree n) (π : Equiv.Perm (Fin n)) :
    SortTree.isLeafNodeOf T (SortTree.run T π) := by
  induction T with
  | leaf p =>
      simp [SortTree.isLeafNodeOf, SortTree.run]
  | node i j l r ih_l ih_r =>
      by_cases h : π i ≤ π j
      · simp [SortTree.run, SortTree.isLeafNodeOf, h]
        exact Or.inl ih_l
      · simp [SortTree.run, SortTree.isLeafNodeOf, h]
        exact Or.inr ih_r

A finite set of leaves of T has cardinality at most the leaf count of T.


theorem card_le_leafCount_of_leaves
    {T : SortTree n} (S : Finset (SortTree n))
    (hS : ∀ t ∈ S, SortTree.isLeafNodeOf T t) :
    S.card ≤ T.leafCount := by
  classical
  induction T generalizing S with
  | leaf p =>
      have hsub : S ⊆ {SortTree.leaf p} := by
        intro t ht
        simp
        exact hS t ht
      exact (Finset.card_le_card hsub).trans (by simp [SortTree.leafCount])
  | node _ _ l r ih_l ih_r =>
      let Sl : Finset (SortTree n) := S.filter (fun t => SortTree.isLeafNodeOf l t)
      let Sr : Finset (SortTree n) := S.filter (fun t => SortTree.isLeafNodeOf r t)
      have hcover : S ⊆ Sl ∪ Sr := by
        intro t ht
        have hleaf := hS t ht
        rw [SortTree.isLeafNodeOf] at hleaf
        rcases hleaf with hl | hr
        · simp [Sl, ht, hl]
        · simp [Sr, ht, hr]
      have hcard_cover : S.card ≤ Sl.card + Sr.card := by
        exact le_trans (Finset.card_le_card hcover) (Finset.card_union_le Sl Sr)
      have hcard_l : Sl.card ≤ l.leafCount := by
        exact ih_l Sl (fun t ht => by
          simp [Sl] at ht
          exact ht.2)
      have hcard_r : Sr.card ≤ r.leafCount := by
        exact ih_r Sr (fun t ht => by
          simp [Sr] at ht
          exact ht.2)
      have hfinal : S.card ≤ l.leafCount + r.leafCount := by
        omega
      simpa [SortTree.leafCount] using hfinal

If an injective map sends a finite type into the leaves of T, then its cardinality is at most the leaf count of T.


theorem card_le_leafCount_of_injective
    {n : ℕ} {T : SortTree n} {β : Type} [Fintype β]
    (f : β → SortTree n)
    (hf : Function.Injective f)
    (hmem : ∀ x, SortTree.isLeafNodeOf T (f x)) :
    Fintype.card β ≤ T.leafCount := by
  classical
  let S : Finset (SortTree n) := Finset.univ.image f
  have hcard : S.card = Fintype.card β := by
    change (Finset.univ.image f).card = Fintype.card β
    rw [Finset.card_image_of_injective (Finset.univ : Finset β) hf]
    simp
  have hS : ∀ t ∈ S, SortTree.isLeafNodeOf T t := by
    intro t ht
    rcases Finset.mem_image.mp ht with ⟨x, _, rfl⟩
    exact hmem x
  calc
    Fintype.card β = S.card := hcard.symm
    _ ≤ T.leafCount := card_le_leafCount_of_leaves S hS

A correct comparison sorter on n distinct elements has at least n! leaves.


theorem factorial_le_leafCount_of_correctSort {T : SortTree n} (hT : CorrectSort T) :
    n.factorial ≤ T.leafCount := by
  have hcard : Fintype.card (Equiv.Perm (Fin n)) = n.factorial := by
    simp [Fintype.card_perm]
  rw [← hcard]
  exact card_le_leafCount_of_injective (SortTree.run T) (run_injective_of_correctSort hT)
    (fun π => run_isLeafNodeOf T π)

A correct sorter for n distinct elements has structural height at least log₂(n!): its decision tree needs n! leaves and a tree of height h has at most 2^h leaves. The companion Execution module proves a separate lower bound attained by an actual input.


theorem height_le_logb_factorial {T : SortTree n} (hT : CorrectSort T) :
    Real.logb 2 (n.factorial : ℝ) ≤ (T.height : ℝ) := by
  have hfac : n.factorial ≤ T.leafCount := factorial_le_leafCount_of_correctSort hT
  have hlc : T.leafCount ≤ 2 ^ T.height := leafCount_le_two_pow_height T
  have hmain : (n.factorial : ℝ) ≤ ((2 : ℝ) ^ T.height) := by
    exact_mod_cast (le_trans hfac hlc)
  have hpos : (0 : ℝ) < (n.factorial : ℝ) := by positivity
  have hmono := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2) hpos hmain
  have hrhs : Real.logb 2 ((2 : ℝ) ^ T.height) = (T.height : ℝ) := by
    simp [Real.logb_pow, Real.logb_self_eq_one]
  simpa [hrhs] using hmono

Factorial growth

The pairing bound (n!)² ≥ nⁿ: the factors k and n + 1 - k of n! are both at least n in aggregate, since k · (n + 1 - k) ≥ n for 1 ≤ k ≤ n.


theorem factorial_sq_ge_pow_self (n : ℕ) : n ^ n ≤ (n.factorial) ^ 2 := by
  have h1 : (∏ k ∈ Finset.Icc 1 n, k) = n.factorial := by
    induction n with
    | zero =>
        simp
    | succ n ih =>
        have hrec : (∏ k ∈ Finset.Icc 1 (n + 1), k) = (∏ k ∈ Finset.Icc 1 n, k) * (n + 1) := by
          exact Finset.prod_Icc_succ_top (by omega) (fun k => k)
        rw [hrec, ih]
        simp [Nat.factorial_succ, mul_comm]
  have h2 : (∏ k ∈ Finset.Icc 1 n, (n + 1 - k)) = n.factorial := by
    rw [← h1]
    exact Finset.prod_bij' (s := Finset.Icc 1 n) (t := Finset.Icc 1 n)
      (fun k _ => n + 1 - k) (fun k _ => n + 1 - k)
      (by intro k hk; rw [Finset.mem_Icc] at hk ⊢; omega)
      (by intro k hk; rw [Finset.mem_Icc] at hk ⊢; omega)
      (by intro k hk; rw [Finset.mem_Icc] at hk; omega)
      (by intro k hk; rw [Finset.mem_Icc] at hk; omega)
      (by intro k hk; rfl)
  have hfactor : ∀ k ∈ Finset.Icc 1 n, n ≤ k * (n + 1 - k) := by
    intro k hk
    have hk1 : 1 ≤ k := (Finset.mem_Icc.mp hk).1
    have hkn : k ≤ n := (Finset.mem_Icc.mp hk).2
    have hsub1 : n + 1 - k = (n - k) + 1 := by omega
    have hsub2 : n = (n - k) + k := by omega
    have hk2 : k = (k - 1) + 1 := by omega
    have hmain : k * (n + 1 - k) = n + (k - 1) * (n - k) := by
      nlinarith
    rw [hmain]
    exact Nat.le_add_right n ((k - 1) * (n - k))
  have hcard_Icc : (Finset.Icc 1 n).card = n := by
    rw [Nat.card_Icc]
    omega
  calc
    n ^ n = (∏ k ∈ Finset.Icc 1 n, n) := by
      rw [Finset.prod_const, hcard_Icc]
    _ ≤ ∏ k ∈ Finset.Icc 1 n, k * (n + 1 - k) := by
      exact Finset.prod_le_prod' (fun k hk => hfactor k hk)
    _ = (n.factorial) ^ 2 := by
      rw [Finset.prod_mul_distrib, h1, h2, pow_two]

log₂(n!) ≥ (n/2) · log₂ n, from the pairing bound (n!)² ≥ nⁿ.


theorem logb_factorial_ge_half_mul_logb (n : ℕ) (hn : 0 < n) :
    ((n : ℝ) / 2) * Real.logb 2 (n : ℝ) ≤ Real.logb 2 (n.factorial : ℝ) := by
  have hpow : (n : ℝ) ^ n ≤ ((n.factorial : ℕ) : ℝ) ^ 2 := by
    exact_mod_cast (factorial_sq_ge_pow_self n)
  have hpos : (0 : ℝ) < (n : ℝ) ^ n := by positivity
  have hmono := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2) hpos hpow
  have hl : Real.logb 2 (((n.factorial : ℕ) : ℝ) ^ 2) = 2 * Real.logb 2 (n.factorial : ℝ) := by
    rw [Real.logb_pow]
    norm_num
  have hr : Real.logb 2 ((n : ℝ) ^ n) = (n : ℝ) * Real.logb 2 (n : ℝ) := by
    rw [Real.logb_pow]
  have h2 : (n : ℝ) * Real.logb 2 (n : ℝ) ≤ 2 * Real.logb 2 (n.factorial : ℝ) := by
    rw [← hr, ← hl]
    exact hmono
  rw [div_mul_eq_mul_div]
  rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]
  simpa [mul_comm] using h2

The lower bound

Structural-height lower bound (CLRS §8.1): any correct comparison tree on n ≥ 2 distinct elements has height at least (n/2)·(log₂ n - 1). The historical name is retained; comparisonSort_exists_run_lowerBound in the companion Execution module strengthens this to an actual input's comparison count.


theorem comparisonSort_worstCase_lowerBound (n : ℕ) (hn : 2 ≤ n)
    {T : SortTree n} (hT : CorrectSort T) :
    ((n : ℝ) / 2) * (Real.logb 2 (n : ℝ) - 1) ≤ (T.height : ℝ) := by
  have hn0 : 0 < n := by omega
  have h2a : ((n : ℝ) / 2) * (Real.logb 2 (n : ℝ) - 1) ≤ ((n : ℝ) / 2) * Real.logb 2 (n : ℝ) := by
    exact mul_le_mul_of_nonneg_left
      (by linarith : Real.logb 2 (n : ℝ) - 1 ≤ Real.logb 2 (n : ℝ))
      (by positivity : 0 ≤ (n : ℝ) / 2)
  have h2b : ((n : ℝ) / 2) * Real.logb 2 (n : ℝ) ≤ Real.logb 2 (n.factorial : ℝ) :=
    logb_factorial_ge_half_mul_logb n hn0
  have h2c : Real.logb 2 (n.factorial : ℝ) ≤ (T.height : ℝ) :=
    height_le_logb_factorial hT
  exact le_trans (le_trans h2a h2b) h2c

end Chapter08end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_08.Section_08_1_Lower_Bound_For_Sorting.Execution

A comparison lower bound attained by a reachable run

Structural height can include infeasible branches. The counted interpreter follows the actual comparisons of the original interpreter. Truncating a tree at a uniform bound on these runs preserves every answer, so the factorial leaf argument applies to that bound. Maximizing the counter over the finite input permutations then gives an actual witness.

namespace CLRS.Chapter08

Interpret the comparison tree, returning the reached leaf and comparison count.

def SortTree.runWithCost (T : SortTree n) (π : Equiv.Perm (Fin n)) : SortTree n × Nat :=
  match T with
  | .leaf p => (.leaf p, 0)
  | .node i j l r =>
      let result := if π i ≤ π j then l.runWithCost π else r.runWithCost π
      (result.1, result.2 + 1)

theorem SortTree.runWithCost_result (T : SortTree n) (π : Equiv.Perm (Fin n)) :
    (T.runWithCost π).1 = T.run π := by
  induction T with
  | leaf p => rfl
  | node i j l r ihl ihr =>
      by_cases h : π i ≤ π j <;> simp [runWithCost, run, h, ihl, ihr]

Truncate only for the counting argument, using an arbitrary leaf at the cutoff.

private def truncate (d : Nat) (T : SortTree n) : SortTree n :=
  match d, T with
  | _, .leaf p => .leaf p
  | 0, .node _ _ _ _ => .leaf 1
  | d + 1, .node i j l r => .node i j (truncate d l) (truncate d r)

private theorem truncate_height (d : Nat) (T : SortTree n) :
    (truncate d T).height ≤ d := by
  induction d generalizing T with
  | zero => cases T <;> simp [truncate, SortTree.height]
  | succ d ih =>
      cases T with
      | leaf p => simp [truncate, SortTree.height]
      | node i j l r =>
          simp only [truncate, SortTree.height]
          have hl := ih l
          have hr := ih r
          omega

private theorem truncate_run (d : Nat) (T : SortTree n) (π : Equiv.Perm (Fin n))
    (h : (T.runWithCost π).2 ≤ d) : (truncate d T).run π = T.run π := by
  induction d generalizing T with
  | zero =>
      cases T with
      | leaf p => rfl
      | node i j l r =>
          by_cases hc : π i ≤ π j <;> simp [SortTree.runWithCost, hc] at h
  | succ d ih =>
      cases T with
      | leaf p => rfl
      | node i j l r =>
          by_cases hc : π i ≤ π j
          · simp only [SortTree.runWithCost, hc, if_true, Nat.add_le_add_iff_right] at h
            simpa only [truncate, SortTree.run, hc, if_true] using ih l h
          · simp only [SortTree.runWithCost, hc, if_false, Nat.add_le_add_iff_right] at h
            simpa only [truncate, SortTree.run, hc, if_false] using ih r h

Any bound on all reachable comparison counts must accommodate all input permutations.


theorem factorial_le_two_pow_run_bound {T : SortTree n} (hT : CorrectSort T)
    (d : Nat) (hbound : ∀ π, (T.runWithCost π).2 ≤ d) : n.factorial ≤ 2 ^ d := by
  have htr : CorrectSort (truncate d T) := by
    intro π
    rw [truncate_run d T π (hbound π)]
    exact hT π
  exact (factorial_le_leafCount_of_correctSort htr).trans
    ((leafCount_le_two_pow_height _).trans
      (Nat.pow_le_pow_right (by norm_num) (truncate_height d T)))

There is an input attaining the information-theoretic comparison lower bound.


theorem comparisonSort_exists_run_log_factorial {T : SortTree n} (hT : CorrectSort T) :
    ∃ π : Equiv.Perm (Fin n),
      Real.logb 2 (n.factorial : ℝ) ≤ ((T.runWithCost π).2 : ℝ) := by
  classical
  obtain ⟨π, _, hmax⟩ := Finset.exists_max_image
    (Finset.univ : Finset (Equiv.Perm (Fin n))) (fun π => (T.runWithCost π).2)
    Finset.univ_nonempty
  refine ⟨π, ?_⟩
  have hfac := factorial_le_two_pow_run_bound hT (T.runWithCost π).2
    (fun ρ => hmax ρ (Finset.mem_univ _))
  have hreal : (n.factorial : ℝ) ≤ (2 : ℝ) ^ (T.runWithCost π).2 := by
    exact_mod_cast hfac
  have hlog := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2)
    (by positivity : (0 : ℝ) < (n.factorial : ℝ)) hreal
  simpa [Real.logb_pow, Real.logb_self_eq_one] using hlog

The comparison lower bound concerns an actual input, even with unreachable branches.

theorem comparisonSort_exists_run_lowerBound (n : Nat) (hn : 2 ≤ n)
    {T : SortTree n} (hT : CorrectSort T) :
    ∃ π : Equiv.Perm (Fin n),
      ((n : ℝ) / 2) * Real.logb 2 (n : ℝ) ≤ ((T.runWithCost π).2 : ℝ) := by
  obtain ⟨π, hπ⟩ := comparisonSort_exists_run_log_factorial hT
  exact ⟨π, (logb_factorial_ge_half_mul_logb n (by omega)).trans hπ⟩

end CLRS.Chapter08

Imports

import Mathlib

8.2. Counting Sort

This file starts Chapter 8 with the stable bucket view of counting sort. CLRS implements the algorithm with a count array and prefix sums; the mathematical content is that keys are emitted in increasing order and that each equal-key subsequence is copied in its original order.

We model that proof spine directly. Given a key function into natural numbers and a maximum key, countingSortBy scans the key values in order and emits the corresponding input bucket. The main theorem packages the three facts used by the textbook proof:

the output is ordered by key;
every key bucket is exactly the corresponding input bucket, hence stable;
membership is preserved when all input keys are at most the declared maximum.

The companion Execution module refines this stable specification with one indexed distribution and one output traversal, returning controller and indexed-operation counters. MutableOutput.countingSortArray and radix passes execute that controller. The existing count-table/scatter helpers remain specification developments; the new linear controller does not execute the literal cumulative-counter decrement program.

Implementation details

The executable refinement pages remain available outside the main sidebar:

namespace CLRSnamespace Chapter08

Ordered lists by key

A compact sortedness predicate for lists ordered by a natural-number key.

def OrderedBy (key : α → Nat) : List α → Prop
  | [] => True
  | [_] => True
  | x :: y :: ys => key x ≤ key y ∧ OrderedBy key (y :: ys)

Every element in a list has key at most upper.

def AllKeysLe (key : α → Nat) (xs : List α) (upper : Nat) : Prop :=
  ∀ x ∈ xs, key x ≤ upper

Every element in a list has key at least lower.

def AllKeysGe (key : α → Nat) (lower : Nat) (xs : List α) : Prop :=
  ∀ x ∈ xs, lower ≤ key x

              theorem orderedBy_tail {key : α → Nat} {x : α} {xs : List α}
    (h : OrderedBy key (x :: xs)) : OrderedBy key xs := by
  cases xs with
  | nil =>
      trivial
  | cons _ _ =>
      exact h.2theorem orderedBy_allKeysGe_tail {key : α → Nat} {x : α} {xs : List α}
    (h : OrderedBy key (x :: xs)) : AllKeysGe key (key x) xs := by
  induction xs generalizing x with
  | nil =>
      intro y hy
      simp at hy
  | cons y ys ih =>
      intro z hz
      simp at hz
      rcases hz with rfl | hz
      · exact h.1
      · exact Nat.le_trans h.1 (ih h.2 z hz)theorem orderedBy_cons_of_allKeysGe {key : α → Nat} {x : α} {xs : List α}
    (hxs : OrderedBy key xs) (hall : AllKeysGe key (key x) xs) :
    OrderedBy key (x :: xs) := by
  cases xs with
  | nil =>
      trivial
  | cons y ys =>
      exact ⟨hall y (by simp), hxs⟩

theorem orderedBy_append_of_rel {key : α → Nat} {xs ys : List α}
    (hxs : OrderedBy key xs) (hys : OrderedBy key ys)
    (hrel : ∀ x ∈ xs, ∀ y ∈ ys, key x ≤ key y) :
    OrderedBy key (xs ++ ys) := by
  induction xs with
  | nil =>
      simpa using hys
  | cons x xs ih =>
      have htail : OrderedBy key (xs ++ ys) := by
        refine ih (orderedBy_tail hxs) ?_
        intro a ha b hb
        exact hrel a (by simp [ha]) b hb
      have hall : AllKeysGe key (key x) (xs ++ ys) := by
        intro z hz
        simp at hz
        rcases hz with hzxs | hzys
        · exact orderedBy_allKeysGe_tail hxs z hzxs
        · exact hrel x (by simp) z hzys
      simpa using orderedBy_cons_of_allKeysGe htail hall

theorem orderedBy_of_all_keys_eq {key : α → Nat} {xs : List α} {k : Nat}
    (h : ∀ x ∈ xs, key x = k) : OrderedBy key xs := by
  induction xs with
  | nil =>
      trivial
  | cons x xs ih =>
      cases xs with
      | nil =>
          trivial
      | cons y ys =>
          have hxy : key x ≤ key y := by
            rw [h x (by simp), h y (by simp)]
          have htail : OrderedBy key (y :: ys) := by
            refine ih ?_
            intro z hz
            exact h z (by simp [hz])
          exact ⟨hxy, htail⟩

Stable buckets

The input bucket whose elements have key k, preserving input order.

def bucket (key : α → Nat) (xs : List α) (k : Nat) : List α :=
  xs.filter fun x => key x == k

              theorem bucket_append (key : α → Nat) (xs ys : List α) (k : Nat) :
    bucket key (xs ++ ys) k = bucket key xs k ++ bucket key ys k := by
  simp [bucket]theorem mem_bucket_iff {key : α → Nat} {xs : List α} {k : Nat} {x : α} :
    x ∈ bucket key xs k ↔ x ∈ xs ∧ key x = k := by
  simp [bucket]theorem bucket_all_keys_eq (key : α → Nat) (xs : List α) (k : Nat) :
    ∀ x ∈ bucket key xs k, key x = k := by
  intro x hx
  exact (mem_bucket_iff.mp hx).2theorem bucket_orderedBy (key : α → Nat) (xs : List α) (k : Nat) :
    OrderedBy key (bucket key xs k) :=
  orderedBy_of_all_keys_eq (bucket_all_keys_eq key xs k)theorem count_bucket_self [DecidableEq α]
    (key : α → Nat) (xs : List α) (x : α) :
    List.count x (bucket key xs (key x)) = List.count x xs := by
  simp [bucket]

Filtering a bucket by a second key keeps it only when the keys agree.

theorem bucket_bucket_eq (key : α → Nat) (xs : List α) (j k : Nat) :
    bucket key (bucket key xs j) k =
      if j = k then bucket key xs k else [] := by
  by_cases hjk : j = k
  · subst hjk
    simp [bucket, List.filter_filter]
  · simp [hjk]
    apply List.eq_nil_iff_forall_not_mem.mpr
    intro x hx
    have hxj : key x = j := (mem_bucket_iff.mp (mem_bucket_iff.mp hx).1).2
    have hxk : key x = k := (mem_bucket_iff.mp hx).2
    exact hjk (hxj ▸ hxk)

theorem bucket_eq_nil_of_allKeysLe_lt {key : α → Nat} {xs : List α}
    {upper k : Nat} (hxs : AllKeysLe key xs upper) (hgt : upper < k) :
    bucket key xs k = [] := by
  apply List.eq_nil_iff_forall_not_mem.mpr
  intro x hx
  have hxmem : x ∈ xs := (mem_bucket_iff.mp hx).1
  have hxkey : key x = k := (mem_bucket_iff.mp hx).2
  exact (Nat.not_lt_of_ge (hxs x hxmem)) (hxkey ▸ hgt)

Counting sort by stable buckets

Stable counting sort by natural-number keys bounded by maxKey.

The function emits the bucket for key 0, then key 1, and so on through maxKey.

def countingSortBy (maxKey : Nat) (key : α → Nat) (xs : List α) : List α :=
  (List.range (maxKey + 1)).flatMap (bucket key xs)

theorem countingSortBy_succ (maxKey : Nat) (key : α → Nat) (xs : List α) :
    countingSortBy (maxKey + 1) key xs =
      countingSortBy maxKey key xs ++ bucket key xs (maxKey + 1) := by
  simp [countingSortBy, List.range_succ, List.flatMap_append]



theorem countingSortBy_allKeysLe (maxKey : Nat) (key : α → Nat) (xs : List α) :
    AllKeysLe key (countingSortBy maxKey key xs) maxKey := by
  intro x hx
  rw [countingSortBy, List.mem_flatMap] at hx
  rcases hx with ⟨k, hk_range, hx_bucket⟩
  have hk_le : k ≤ maxKey := by
    have hk_lt : k < maxKey + 1 := (List.mem_range.mp hk_range)
    exact Nat.le_of_lt_succ hk_lt
  have hxkey : key x = k := (mem_bucket_iff.mp hx_bucket).2
  exact hxkey ▸ hk_le

If k ≤ maxKey, the k-bucket of the output is exactly the k-bucket of the input. This is the stable-copy theorem for in-range keys.


theorem countingSortBy_bucket_eq_of_le
    (maxKey : Nat) (key : α → Nat) (xs : List α) {k : Nat}
    (hk : k ≤ maxKey) :
    bucket key (countingSortBy maxKey key xs) k = bucket key xs k := by
  induction maxKey with
  | zero =>
      have hk0 : k = 0 := Nat.eq_zero_of_le_zero hk
      subst hk0
      simp [countingSortBy, bucket_bucket_eq]
  | succ maxKey ih =>
      rw [countingSortBy_succ, bucket_append]
      by_cases hlast : k = maxKey + 1
      · subst hlast
        have hprev_empty :
            bucket key (countingSortBy maxKey key xs) (maxKey + 1) = [] := by
          exact bucket_eq_nil_of_allKeysLe_lt
            (countingSortBy_allKeysLe maxKey key xs) (Nat.lt_succ_self maxKey)
        rw [hprev_empty, bucket_bucket_eq]
        simp
      · have hk_prev : k ≤ maxKey := by
          exact Nat.le_of_lt_succ (Nat.lt_of_le_of_ne hk hlast)
        have hlast_empty : bucket key (bucket key xs (maxKey + 1)) k = [] := by
          have hne : maxKey + 1 ≠ k := by
            intro h
            exact hlast h.symm
          simp [bucket_bucket_eq, hne]
        rw [ih hk_prev, hlast_empty, List.append_nil]

theorem countingSortBy_bucket_eq_of_gt
    (maxKey : Nat) (key : α → Nat) (xs : List α) {k : Nat}
    (hk : maxKey < k) :
    bucket key (countingSortBy maxKey key xs) k = [] := by
  apply List.eq_nil_iff_forall_not_mem.mpr
  intro x hx
  have hxle := countingSortBy_allKeysLe maxKey key xs x (mem_bucket_iff.mp hx).1
  have hxkey := (mem_bucket_iff.mp hx).2
  exact (Nat.not_lt_of_ge hxle) (hxkey ▸ hk)

Counting sort preserves every equal-key subsequence when the input keys are bounded by maxKey. This is the stability statement.


theorem countingSortBy_bucket_eq
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (k : Nat) :
    bucket key (countingSortBy maxKey key xs) k = bucket key xs k := by
  by_cases hk : k ≤ maxKey
  · exact countingSortBy_bucket_eq_of_le maxKey key xs hk
  · have hgt : maxKey < k := Nat.lt_of_not_ge hk
    rw [countingSortBy_bucket_eq_of_gt maxKey key xs hgt,
      bucket_eq_nil_of_allKeysLe_lt hxs hgt]

              

theorem countingSortBy_ordered (maxKey : Nat) (key : α → Nat) (xs : List α) :
    OrderedBy key (countingSortBy maxKey key xs) := by
  induction maxKey with
  | zero =>
      simpa [countingSortBy] using bucket_orderedBy key xs 0
  | succ maxKey ih =>
      rw [countingSortBy_succ]
      refine orderedBy_append_of_rel ih (bucket_orderedBy key xs (maxKey + 1)) ?_
      intro a ha b hb
      have hale := countingSortBy_allKeysLe maxKey key xs a ha
      have hbkey := (mem_bucket_iff.mp hb).2
      exact Nat.le_trans hale (by simp [hbkey])

theorem countingSortBy_mem_iff
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (x : α) :
    x ∈ countingSortBy maxKey key xs ↔ x ∈ xs := by
  constructor
  · intro hx
    rw [countingSortBy, List.mem_flatMap] at hx
    rcases hx with ⟨k, _hk, hx_bucket⟩
    exact (mem_bucket_iff.mp hx_bucket).1
  · intro hx
    have hxkey_le : key x ≤ maxKey := hxs x hx
    have hbucket : bucket key (countingSortBy maxKey key xs) (key x) =
        bucket key xs (key x) :=
      countingSortBy_bucket_eq maxKey key xs hxs (key x)
    have hx_bucket_input : x ∈ bucket key xs (key x) := by
      exact mem_bucket_iff.mpr ⟨hx, rfl⟩
    have hx_bucket_output : x ∈ bucket key (countingSortBy maxKey key xs) (key x) := by
      simpa [hbucket] using hx_bucket_input
    exact (mem_bucket_iff.mp hx_bucket_output).1

theorem countingSortBy_perm [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    (countingSortBy maxKey key xs).Perm xs := by
  classical
  apply List.perm_iff_count.mpr
  intro x
  have hbucket := countingSortBy_bucket_eq maxKey key xs hxs (key x)
  calc
    List.count x (countingSortBy maxKey key xs)
        = List.count x (bucket key (countingSortBy maxKey key xs) (key x)) := by
            rw [count_bucket_self]
    _ = List.count x (bucket key xs (key x)) := by
            rw [hbucket]
    _ = List.count x xs := by
            rw [count_bucket_self]

Reader-facing correctness theorem for stable counting sort.

theorem countingSortBy_correct [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    OrderedBy key (countingSortBy maxKey key xs) ∧
      (∀ k, bucket key (countingSortBy maxKey key xs) k = bucket key xs k) ∧
      (∀ x, x ∈ countingSortBy maxKey key xs ↔ x ∈ xs) ∧
      (countingSortBy maxKey key xs).Perm xs :=
  ⟨countingSortBy_ordered maxKey key xs,
    countingSortBy_bucket_eq maxKey key xs hxs,
    countingSortBy_mem_iff maxKey key xs hxs,
    countingSortBy_perm maxKey key xs hxs⟩

end Chapter08end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.CountTables

This file adds the count-table layer that sits between the stable bucket specification of countingSortBy and the array implementation in CLRS COUNTING-SORT.

The point of this layer is deliberately modest and proof-friendly:

countTable records the length of each stable bucket;
cumulativeCounts records prefix-count boundaries;
countingSortByTable uses the count table to drive the same emitted key range as countingSortBy;
reverseBucket models the right-to-left scan for one key by folding from the right and prepending matching elements;
the table-driven and reverse-bucket wrappers are proved equal to the existing stable bucket specification, so they inherit orderedness, stability, membership, and permutation correctness.

The remaining imperative refinement is to replace the per-key reverse-bucket view with a single mutable output array and mutable cumulative counters.

namespace CLRSnamespace Chapter08

Count table certificates

Count table entry k is the length of the stable input bucket for key k.

def countTable (key : α → Nat) (xs : List α) (maxKey : Nat) : Array Nat :=
  ((List.range (maxKey + 1)).map fun k => (bucket key xs k).length).toArray

The count table is exactly the list of bucket lengths for keys 0..maxKey.

theorem countTable_toList (key : α → Nat) (xs : List α) (maxKey : Nat) :
    (countTable key xs maxKey).toList =
      (List.range (maxKey + 1)).map fun k => (bucket key xs k).length := by
  simp [countTable]

The count table has one slot for every key 0..maxKey.

theorem countTable_size (key : α → Nat) (xs : List α) (maxKey : Nat) :
    (countTable key xs maxKey).size = maxKey + 1 := by
  simp [countTable]

Summing the count table gives the length of the bucket-specification output.

theorem countTable_sum_eq_countingSortBy_length
    (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (countTable key xs maxKey).toList.sum =
      (countingSortBy maxKey key xs).length := by
  simp [countTable, countingSortBy, List.length_flatMap]

Cumulative-count boundaries

Prefix sums of a count table. For counts [c0, c1, ...], this returns [c0, c0 + c1, ...], matching the cumulative array in CLRS.

def cumulativeCounts : List Nat → List Nat
  | [] => []
  | c :: cs => c :: (cumulativeCounts cs).map (fun n => c + n)

Cumulative counts preserve the number of table slots.

theorem cumulativeCounts_length (counts : List Nat) :
    (cumulativeCounts counts).length = counts.length := by
  induction counts with
  | nil =>
      simp [cumulativeCounts]
  | cons c counts ih =>
      simp [cumulativeCounts, ih]

The empty count table has no cumulative boundaries.

theorem cumulativeCounts_nil :
    cumulativeCounts ([] : List Nat) = [] := rfl

The first cumulative boundary is the first count; later boundaries are shifted by it.

theorem cumulativeCounts_cons (c : Nat) (counts : List Nat) :
    cumulativeCounts (c :: counts) =
      c :: (cumulativeCounts counts).map (fun n => c + n) := rfl

Cumulative counts for the counting-sort table have one slot per key.

def cumulativeCountTable (key : α → Nat) (xs : List α) (maxKey : Nat) : List Nat :=
  cumulativeCounts (countTable key xs maxKey).toList

theorem cumulativeCountTable_length (key : α → Nat) (xs : List α) (maxKey : Nat) :
    (cumulativeCountTable key xs maxKey).length = maxKey + 1 := by
  simp [cumulativeCountTable, cumulativeCounts_length, countTable_size]

Table-driven wrapper

Counting sort driven by the count-table size.

This is still a pure bucket specification, but the emitted key range now comes from the count table, matching the first table-building phase of CLRS COUNTING-SORT.

def countingSortByTable (maxKey : Nat) (key : α → Nat) (xs : List α) : List α :=
  (List.range (countTable key xs maxKey).size).flatMap (bucket key xs)

The count-table wrapper is extensionally the existing stable bucket sort.

theorem countingSortByTable_eq_countingSortBy
    (maxKey : Nat) (key : α → Nat) (xs : List α) :
    countingSortByTable maxKey key xs = countingSortBy maxKey key xs := by
  simp [countingSortByTable, countTable_size, countingSortBy]

              

theorem countingSortByTable_ordered (maxKey : Nat) (key : α → Nat) (xs : List α) :
    OrderedBy key (countingSortByTable maxKey key xs) := by
  rw [countingSortByTable_eq_countingSortBy]
  exact countingSortBy_ordered maxKey key xs

theorem countingSortByTable_bucket_eq
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (k : Nat) :
    bucket key (countingSortByTable maxKey key xs) k = bucket key xs k := by
  rw [countingSortByTable_eq_countingSortBy]
  exact countingSortBy_bucket_eq maxKey key xs hxs k

theorem countingSortByTable_mem_iff
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (x : α) :
    x ∈ countingSortByTable maxKey key xs ↔ x ∈ xs := by
  rw [countingSortByTable_eq_countingSortBy]
  exact countingSortBy_mem_iff maxKey key xs hxs x

theorem countingSortByTable_perm [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    (countingSortByTable maxKey key xs).Perm xs := by
  rw [countingSortByTable_eq_countingSortBy]
  exact countingSortBy_perm maxKey key xs hxs

Reader-facing correctness theorem for the count-table refinement layer.

theorem countingSortByTable_correct [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    OrderedBy key (countingSortByTable maxKey key xs) ∧
      (∀ k, bucket key (countingSortByTable maxKey key xs) k = bucket key xs k) ∧
      (∀ x, x ∈ countingSortByTable maxKey key xs ↔ x ∈ xs) ∧
      (countingSortByTable maxKey key xs).Perm xs :=
  ⟨countingSortByTable_ordered maxKey key xs,
    countingSortByTable_bucket_eq maxKey key xs hxs,
    countingSortByTable_mem_iff maxKey key xs hxs,
    countingSortByTable_perm maxKey key xs hxs⟩

namespace ReverseScan

Build the stable bucket for one key by scanning from right to left and prepending each matching element.

This is the one-key functional core of CLRS COUNTING-SORT's final loop: placing from the right side of a key segment is equivalent to a right fold that prepends matches into that segment.

def reverseBucket (key : α → Nat) (xs : List α) (k : Nat) : List α :=
  xs.foldr (fun x acc => if key x == k then x :: acc else acc) []

The right-to-left bucket builder is exactly the stable input bucket.


theorem reverseBucket_eq_bucket (key : α → Nat) (xs : List α) (k : Nat) :
    reverseBucket key xs k = bucket key xs k := by
  unfold reverseBucket bucket
  rw [List.filter_eq_foldr]
  simp [Bool.cond_eq_ite]



theorem mem_reverseBucket_iff {key : α → Nat} {xs : List α} {k : Nat} {x : α} :
    x ∈ reverseBucket key xs k ↔ x ∈ xs ∧ key x = k := by
  rw [reverseBucket_eq_bucket]
  exact mem_bucket_iff

Counting sort via per-key reverse buckets.

This is not yet the single mutable output array of CLRS, but it captures the stability-critical reverse-scan behavior for every key segment.

def countingSortByReverse (maxKey : Nat) (key : α → Nat) (xs : List α) : List α :=
  (List.range (maxKey + 1)).flatMap (reverseBucket key xs)

The reverse-scan bucket wrapper is extensionally the count-table wrapper.


theorem countingSortByReverse_eq_countingSortByTable
    (maxKey : Nat) (key : α → Nat) (xs : List α) :
    countingSortByReverse maxKey key xs = countingSortByTable maxKey key xs := by
  rw [countingSortByTable_eq_countingSortBy]
  unfold countingSortByReverse countingSortBy
  apply List.flatMap_congr
  intro k _hk
  exact reverseBucket_eq_bucket key xs k

              

theorem countingSortByReverse_ordered (maxKey : Nat) (key : α → Nat) (xs : List α) :
    OrderedBy key (countingSortByReverse maxKey key xs) := by
  rw [countingSortByReverse_eq_countingSortByTable]
  exact countingSortByTable_ordered maxKey key xs

theorem countingSortByReverse_bucket_eq
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (k : Nat) :
    bucket key (countingSortByReverse maxKey key xs) k = bucket key xs k := by
  rw [countingSortByReverse_eq_countingSortByTable]
  exact countingSortByTable_bucket_eq maxKey key xs hxs k

theorem countingSortByReverse_mem_iff
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (x : α) :
    x ∈ countingSortByReverse maxKey key xs ↔ x ∈ xs := by
  rw [countingSortByReverse_eq_countingSortByTable]
  exact countingSortByTable_mem_iff maxKey key xs hxs x

theorem countingSortByReverse_perm [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    (countingSortByReverse maxKey key xs).Perm xs := by
  rw [countingSortByReverse_eq_countingSortByTable]
  exact countingSortByTable_perm maxKey key xs hxs

Reader-facing correctness theorem for the reverse-scan bucket refinement.

theorem countingSortByReverse_correct [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    OrderedBy key (countingSortByReverse maxKey key xs) ∧
      (∀ k, bucket key (countingSortByReverse maxKey key xs) k = bucket key xs k) ∧
      (∀ x, x ∈ countingSortByReverse maxKey key xs ↔ x ∈ xs) ∧
      (countingSortByReverse maxKey key xs).Perm xs :=
  ⟨countingSortByReverse_ordered maxKey key xs,
    countingSortByReverse_bucket_eq maxKey key xs hxs,
    countingSortByReverse_mem_iff maxKey key xs hxs,
    countingSortByReverse_perm maxKey key xs hxs⟩

Cumulative segment counts

Number of elements in the leading key segments 0..k.

def cumulativeCount (key : α → Nat) (xs : List α) (k : Nat) : Nat :=
  ((List.range (k + 1)).map fun i => (bucket key xs i).length).sum

theorem cumulativeCount_zero (key : α → Nat) (xs : List α) :
    cumulativeCount key xs 0 = (bucket key xs 0).length := by
  simp [cumulativeCount]

The cumulative segment count grows by exactly the next stable bucket length.

theorem cumulativeCount_succ (key : α → Nat) (xs : List α) (k : Nat) :
    cumulativeCount key xs (k + 1) =
      cumulativeCount key xs k + (bucket key xs (k + 1)).length := by
  simp [cumulativeCount, List.range_succ, add_assoc]

Cumulative segment count at maxKey is the counting-sort output length.

theorem cumulativeCount_eq_countingSortBy_length
    (maxKey : Nat) (key : α → Nat) (xs : List α) :
    cumulativeCount key xs maxKey = (countingSortBy maxKey key xs).length := by
  simp [cumulativeCount, countingSortBy, List.length_flatMap]

The reverse-scan wrapper has the same length as the cumulative final boundary.


theorem countingSortByReverse_length
    (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (countingSortByReverse maxKey key xs).length =
      cumulativeCount key xs maxKey := by
  rw [countingSortByReverse_eq_countingSortByTable,
    countingSortByTable_eq_countingSortBy,
    cumulativeCount_eq_countingSortBy_length]

              end ReverseScanend Chapter08end CLRS

CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.Execution

Counting sort through one stable indexed distribution

The input is traversed once, storing each element in an indexed list bucket. The output loop traverses these stored buckets and pushes each emitted element once. The returned counters count the visits to these actual loops. A separate indexed-work ledger expands each accepted distribution step into its key, check, indexed-read, cons, and indexed-write operations.

This is an indexed stable-bucket refinement of counting sort. It does not run the textbook cumulative-counter decrement program. Indexed array operations are unit-cost primitives here; persistent-array copying, array/list view conversion, allocation internals, and machine instructions are not modeled by this controller ledger.

namespace CLRS.Chapter08.CountingExecution

structure Distribution (α : Type*) where
  buckets : Array (List α)
  inputs : Nat
  updates : Nat
  deriving Repr

Initialize buckets with one array push per slot.

def initializeBuckets : Nat → Array (List α) × Nat
  | 0 => (#[], 0)
  | n + 1 => let prev := initializeBuckets n; (prev.1.push [], prev.2 + 1)

@[simp] theorem initializeBuckets_array (n : Nat) :
    (initializeBuckets (α := α) n).1 = Array.replicate n [] := by
  induction n with
  | zero => simp [initializeBuckets]
  | succ n ih => simp [initializeBuckets, ih, Array.replicate_succ]

@[simp] theorem initializeBuckets_visits (n : Nat) : (initializeBuckets (α := α) n).2 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [initializeBuckets, ih]

Scan from right to left, evaluating each input key once. Each successful index check performs one bucket read, one cons, and one bucket write.

def distribute (key : α → Nat) : List α → Array (List α) → Distribution α
  | [], acc => ⟨acc, 0, 0⟩
  | x :: xs, acc =>
      let rest := distribute key xs acc
      let k := key x
      if h : k < rest.buckets.size then
        ⟨rest.buckets.set k (x :: rest.buckets[k]), rest.inputs + 1, rest.updates + 1⟩
      else ⟨rest.buckets, rest.inputs + 1, rest.updates⟩

              @[simp] theorem distribute_size (key : α → Nat) (xs : List α) (acc : Array (List α)) :
    (distribute key xs acc).buckets.size = acc.size := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp only [distribute]; split <;> simp_all@[simp] theorem distribute_inputs (key : α → Nat) (xs : List α) (acc : Array (List α)) :
    (distribute key xs acc).inputs = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp only [distribute]; split <;> simp_alltheorem distribute_updates_le (key : α → Nat) (xs : List α) (acc : Array (List α)) :
    (distribute key xs acc).updates ≤ xs.length := by
  induction xs with
  | nil => simp [distribute]
  | cons x xs ih => simp only [distribute]; split <;> simp_all; omega

theorem distribute_updates_eq (key : α → Nat) (xs : List α) (acc : Array (List α))
    (hkeys : ∀ x ∈ xs, key x < acc.size) :
    (distribute key xs acc).updates = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      have hx := hkeys x (by simp)
      have ht : ∀ y ∈ xs, key y < acc.size := fun y hy => hkeys y (by simp [hy])
      simp [distribute, hx, ih ht]

Every bucket preserves input order, even with an arbitrary initial table.


theorem distribute_get (key : α → Nat) (xs : List α) (acc : Array (List α))
    (k : Nat) (hk : k < acc.size) :
    (distribute key xs acc).buckets[k]'(by simpa using hk) = bucket key xs k ++ acc[k] := by
  induction xs with
  | nil => simp [distribute, bucket]
  | cons x xs ih =>
      have hk' : k < (distribute key xs acc).buckets.size := by simpa using hk
      simp only [distribute]
      split
      next h =>
        by_cases heq : key x = k
        · subst k
          simp [bucket, ih, Bool.beq_eq_decide_eq]
        · simp [Array.getElem_set, heq, bucket, Bool.beq_eq_decide_eq] at ih ⊢
          exact ih
      next h =>
        have heq : key x ≠ k := by intro he; apply h; simpa [he] using hk'
        simpa [bucket, List.filter_cons, Bool.beq_eq_decide_eq, heq] using ih

structure Output (α : Type*) where
  value : Array α
  writes : Nat

Push each supplied element once into the output.

def pushList : List α → Array α → Output α
  | [], out => ⟨out, 0⟩
  | x :: xs, out =>
      let rest := pushList xs (out.push x)
      ⟨rest.value, rest.writes + 1⟩

              @[simp] theorem pushList_value (xs : List α) (out : Array α) :
    (pushList xs out).value.toList = out.toList ++ xs := by
  induction xs generalizing out with
  | nil => simp [pushList]
  | cons x xs ih => simp [pushList, ih, List.append_assoc]@[simp] theorem pushList_writes (xs : List α) (out : Array α) :
    (pushList xs out).writes = xs.length := by
  induction xs generalizing out with
  | nil => rfl
  | cons x xs ih => simp [pushList, ih]structure Emission (α : Type*) where
  output : Array α
  bucketVisits : Nat
  outputWrites : Nat

Visit each stored bucket once and push its elements in order.

def emit : List (List α) → Array α → Emission α
  | [], out => ⟨out, 0, 0⟩
  | b :: bs, out =>
      let pushed := pushList b out
      let rest := emit bs pushed.value
      ⟨rest.output, rest.bucketVisits + 1, pushed.writes + rest.outputWrites⟩

              @[simp] theorem emit_value (bs : List (List α)) (out : Array α) :
    (emit bs out).output.toList = out.toList ++ bs.flatten := by
  induction bs generalizing out with
  | nil => simp [emit]
  | cons b bs ih => simp [emit, ih, List.append_assoc]@[simp] theorem emit_visits (bs : List (List α)) (out : Array α) :
    (emit bs out).bucketVisits = bs.length := by
  induction bs generalizing out with
  | nil => rfl
  | cons b bs ih => simp [emit, ih]@[simp] theorem emit_writes (bs : List (List α)) (out : Array α) :
    (emit bs out).outputWrites = bs.flatten.length := by
  induction bs generalizing out with
  | nil => rfl
  | cons b bs ih => simp [emit, ih]structure Execution (α : Type*) where
  output : Array α
  initializationWrites : Nat
  inputVisits : Nat
  bucketUpdates : Nat
  bucketVisits : Nat
  outputWrites : Nat

The number of visits to the four controller loops.

def Execution.controllerVisits (run : Execution α) : Nat :=
  run.initializationWrites + run.inputVisits + run.bucketVisits + run.outputWrites

Explicit indexed-operation ledger: initialization pushes, one key evaluation and index check per input, a read/cons/write triple per accepted input, bucket visits, and output pushes. This does not model persistent-array machine time.

def Execution.indexedWork (run : Execution α) : Nat :=
  run.initializationWrites + 2 * run.inputVisits + 3 * run.bucketUpdates +
    run.bucketVisits + run.outputWrites

Stable indexed-bucket counting sort and the counters produced by its loops.

def execute (maxKey : Nat) (key : α → Nat) (xs : List α) : Execution α :=
  let initial := initializeBuckets (α := α) (maxKey + 1)
  let distributed := distribute key xs initial.1
  let emitted := emit distributed.buckets.toList #[]
  ⟨emitted.output, initial.2, distributed.inputs, distributed.updates,
    emitted.bucketVisits, emitted.outputWrites⟩



theorem distribute_toList (bucketCount : Nat) (key : α → Nat) (xs : List α) :
    (distribute key xs (Array.replicate bucketCount [])).buckets.toList =
      (List.range bucketCount).map (bucket key xs) := by
  apply List.ext_getElem
  · simp
  · intro i hi hj
    simp only [List.getElem_map, List.getElem_range, Array.getElem_toList]
    have he := distribute_get key xs (Array.replicate bucketCount []) i (by simpa using hj)
    simpa using he

The new execution refines the stable bucket specification, including its out-of-range-key behavior.

theorem execute_result (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (execute maxKey key xs).output.toList = countingSortBy maxKey key xs := by
  simp [execute, distribute_toList, countingSortBy, List.flatMap]

theorem execute_counts (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (execute maxKey key xs).initializationWrites = maxKey + 1 ∧
    (execute maxKey key xs).inputVisits = xs.length ∧
    (execute maxKey key xs).bucketVisits = maxKey + 1 ∧
    (execute maxKey key xs).outputWrites = (countingSortBy maxKey key xs).length := by
  simp [execute, distribute_toList, countingSortBy, List.flatMap]

theorem execute_updates (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hkeys : AllKeysLe key xs maxKey) :
    (execute maxKey key xs).bucketUpdates = xs.length := by
  apply distribute_updates_eq
  simpa [AllKeysLe, Nat.lt_succ_iff] using hkeys

Under bounded keys, all four loop visits total the traditional linear ledger.

theorem execute_controllerVisits [DecidableEq α] (maxKey : Nat) (key : α → Nat)
    (xs : List α) (hkeys : AllKeysLe key xs maxKey) :
    (execute maxKey key xs).controllerVisits = 2 * xs.length + 2 * (maxKey + 1) := by
  rcases execute_counts maxKey key xs with ⟨hi, hn, hb, ho⟩
  have hl := (countingSortBy_perm maxKey key xs hkeys).length_eq
  simp only [Execution.controllerVisits, hi, hn, hb, ho, hl]
  omega

The explicitly listed key/index/list operations also have linear total work.


theorem execute_indexedWork [DecidableEq α] (maxKey : Nat) (key : α → Nat)
    (xs : List α) (hkeys : AllKeysLe key xs maxKey) :
    (execute maxKey key xs).indexedWork = 6 * xs.length + 2 * (maxKey + 1) := by
  rcases execute_counts maxKey key xs with ⟨hi, hn, hb, ho⟩
  have hl := (countingSortBy_perm maxKey key xs hkeys).length_eq
  rw [Execution.indexedWork, hi, hn, hb, ho, hl, execute_updates maxKey key xs hkeys]
  omega

end CLRS.Chapter08.CountingExecution

CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.MutableOutputArray

The public countingSortArray calls CountingExecution.execute: one initialization loop, one right-to-left indexed distribution, and one output loop visiting the stored buckets and pushing their elements. Its array output equals the existing countingSortBy specification, preserving orderedness, per-key stability, membership, and permutation contracts.

The older scatter remains a per-key-filter specification helper. It is not called by the public sorter. Cumulative counts describe output segment boundaries; the executable does not run the textbook cumulative-counter decrement program. This is an indexed stable-bucket refinement.

The execution returns counters accumulated in its loops. countingSortArrayCost is their controller-visit total on bounded keys, while CountingExecution.execute_indexedWork counts key evaluations, index checks, reads, cons operations, writes, bucket visits, and output pushes. These unit-cost ledgers do not model persistent-array copying or machine time.

              namespace CLRSnamespace Chapter08namespace MutableOutput

The mutable output array

Per-key-filter scatter specification. This helper rescans the input for every requested key and is not the public linear controller.

def scatter (key : α → Nat) (xs : List α) (ks : List Nat) : Array α :=
  ks.foldl (fun out k => out ++ (ReverseScan.reverseBucket key xs k).toArray) #[]

Reading the scattered output back as a list gives the concatenation of the per-key reverse-scan buckets. This is the correctness bridge between the mutable Array fill and the functional bucket specification.


theorem scatter_toList (key : α → Nat) (xs : List α) (ks : List Nat) :
    (scatter key xs ks).toList = ks.flatMap (ReverseScan.reverseBucket key xs) := by
  unfold scatter
  suffices h : ∀ init : Array α,
      (ks.foldl (fun out k => out ++ (ReverseScan.reverseBucket key xs k).toArray)
          init).toList
        = init.toList ++ ks.flatMap (ReverseScan.reverseBucket key xs) by
    simpa using h #[]
  intro init
  induction ks generalizing init with
  | nil => simp
  | cons k ks ih =>
      rw [List.foldl_cons,
        ih (init ++ (ReverseScan.reverseBucket key xs k).toArray)]
      simp [List.flatMap_cons, List.append_assoc]

Stable output array from the actual indexed distribution and emission loops.

def countingSortArray (maxKey : Nat) (key : α → Nat) (xs : List α) : Array α :=
  (CountingExecution.execute maxKey key xs).output

Array-to-array wrapper of the indexed stable-bucket refinement: read the input array and return a new sorted output array.

def countingSortInPlace (maxKey : Nat) (key : α → Nat) (a : Array α) : Array α :=
  countingSortArray maxKey key a.toList

Mutable output-array refinement. Reading the mutable output array back as a list yields exactly the stable bucket specification countingSortBy. All correctness properties transfer through this extensional equality.

theorem countingSortArray_toList (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (countingSortArray maxKey key xs).toList = countingSortBy maxKey key xs := by
  exact CountingExecution.execute_result maxKey key xs

The linear controller is extensionally equal to the older per-key scatter helper.


theorem countingSortArray_eq_scatter (maxKey : Nat) (key : α → Nat) (xs : List α) :
    countingSortArray maxKey key xs = scatter key xs (List.range (maxKey + 1)) := by
  apply Array.toList_inj.mp
  rw [countingSortArray_toList, scatter_toList]
  unfold countingSortBy
  apply List.flatMap_congr
  intro k hk
  exact (ReverseScan.reverseBucket_eq_bucket key xs k).symm

The array wrapper reads back as the stable bucket specification of its input.

theorem countingSortInPlace_toList (maxKey : Nat) (key : α → Nat) (a : Array α) :
    (countingSortInPlace maxKey key a).toList = countingSortBy maxKey key a.toList := by
  unfold countingSortInPlace
  exact countingSortArray_toList maxKey key a.toList

The mutable output array is ordered by key.


theorem countingSortArray_ordered (maxKey : Nat) (key : α → Nat) (xs : List α) :
    OrderedBy key (countingSortArray maxKey key xs).toList := by
  rw [countingSortArray_toList]
  exact countingSortBy_ordered maxKey key xs

Per-key stability: for keys bounded by maxKey, filtering the mutable output array by any key returns exactly the same list as filtering the input.


theorem countingSortArray_bucket_eq
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (k : Nat) :
    bucket key (countingSortArray maxKey key xs).toList k = bucket key xs k := by
  rw [countingSortArray_toList]
  exact countingSortBy_bucket_eq maxKey key xs hxs k

Membership in the mutable output list matches membership in the input.


theorem countingSortArray_mem_toList_iff
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (x : α) :
    x ∈ (countingSortArray maxKey key xs).toList ↔ x ∈ xs := by
  rw [countingSortArray_toList]
  exact countingSortBy_mem_iff maxKey key xs hxs x

Membership in the mutable output array matches membership in the input.


theorem countingSortArray_mem_iff
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) (x : α) :
    x ∈ countingSortArray maxKey key xs ↔ x ∈ xs := by
  rw [← Array.mem_toList_iff]
  exact countingSortArray_mem_toList_iff maxKey key xs hxs x

The mutable output array is a permutation of the input.


theorem countingSortArray_perm [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    (countingSortArray maxKey key xs).toList.Perm xs := by
  rw [countingSortArray_toList]
  exact countingSortBy_perm maxKey key xs hxs

Reader-facing correctness theorem for the mutable output-array refinement.

theorem countingSortArray_correct [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    OrderedBy key (countingSortArray maxKey key xs).toList ∧
      (∀ k, bucket key (countingSortArray maxKey key xs).toList k = bucket key xs k) ∧
      (∀ x, x ∈ (countingSortArray maxKey key xs).toList ↔ x ∈ xs) ∧
      (countingSortArray maxKey key xs).toList.Perm xs :=
  ⟨countingSortArray_ordered maxKey key xs,
    fun k => countingSortArray_bucket_eq maxKey key xs hxs k,
    fun x => countingSortArray_mem_toList_iff maxKey key xs hxs x,
    countingSortArray_perm maxKey key xs hxs⟩

Cumulative-count fill offsets

After filling keys 0..j, exactly cumulativeCount key xs j output slots are used. This is the cumulative-count boundary semantics of CLRS's prefix-count array C: the fill offset for key j + 1 is the number of elements with key at most j.


theorem scatter_range_size (key : α → Nat) (xs : List α) (j : Nat) :
    (scatter key xs (List.range (j + 1))).size = ReverseScan.cumulativeCount key xs j := by
  rw [← Array.length_toList, scatter_toList]
  unfold ReverseScan.cumulativeCount
  simp [List.length_flatMap, ReverseScan.reverseBucket_eq_bucket]

The full mutable output array has as many slots as the final cumulative count, i.e. the total number of in-range elements.


theorem countingSortArray_size (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (countingSortArray maxKey key xs).size = ReverseScan.cumulativeCount key xs maxKey := by
  rw [countingSortArray_eq_scatter]
  exact scatter_range_size key xs maxKey

Under the CLRS precondition that every key lies in 0..maxKey, the scatter performs exactly n writes: the output array has the input length.


theorem countingSortArray_size_of_allKeysLe [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α)
    (hxs : AllKeysLe key xs maxKey) :
    (countingSortArray maxKey key xs).size = xs.length := by
  rw [← Array.length_toList]
  exact (countingSortArray_perm maxKey key xs hxs).length_eq

Linear work bound

Controller-visit ledger: initialize each bucket, visit each input once, visit each stored bucket once, and push each output element once. Bounded keys make the number of output pushes equal to the input length.

def countingSortArrayCost (maxKey : Nat) (n : Nat) : Nat :=
  (maxKey + 1) + n + (maxKey + 1) + n

The work is the linear expression 2 * n + 2 * (maxKey + 1).

theorem countingSortArrayCost_eq (maxKey : Nat) (n : Nat) :
    countingSortArrayCost maxKey n = 2 * n + 2 * (maxKey + 1) := by
  unfold countingSortArrayCost
  omega

The work is bounded by 2 * (n + maxKey + 1), exhibiting linearity in n + k.

theorem countingSortArrayCost_le (maxKey : Nat) (n : Nat) :
    countingSortArrayCost maxKey n ≤ 2 * (n + (maxKey + 1)) := by
  unfold countingSortArrayCost
  omega

Linear O(n + k) work bound. There is a constant c (here 2) such that the counting-sort work is at most c * (n + k + 1) for every input length n and maximum key k = maxKey.

theorem countingSortArrayCost_bigO :
    ∃ c : Nat, ∀ maxKey n : Nat,
      countingSortArrayCost maxKey n ≤ c * (n + maxKey + 1) := by
  refine ⟨2, ?_⟩
  intro maxKey n
  unfold countingSortArrayCost
  omega

The actual controller returns the advertised ledger on bounded keys.


theorem countingSortArray_execution_cost [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α) (hxs : AllKeysLe key xs maxKey) :
    (CountingExecution.execute maxKey key xs).controllerVisits =
      countingSortArrayCost maxKey xs.length := by
  rw [CountingExecution.execute_controllerVisits maxKey key xs hxs,
    countingSortArrayCost_eq]

Return the output and the controller visits from the same execution.

def countingSortArrayWithCost (maxKey : Nat) (key : α → Nat) (xs : List α) : Array α × Nat :=
  let run := CountingExecution.execute maxKey key xs
  (run.output, run.controllerVisits)

theorem countingSortArrayWithCost_result (maxKey : Nat) (key : α → Nat) (xs : List α) :
    (countingSortArrayWithCost maxKey key xs).1 = countingSortArray maxKey key xs := rfl

theorem countingSortArrayWithCost_cost [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α) (hxs : AllKeysLe key xs maxKey) :
    (countingSortArrayWithCost maxKey key xs).2 = countingSortArrayCost maxKey xs.length :=
  countingSortArray_execution_cost maxKey key xs hxs

The expanded indexed-operation ledger remains linear.


theorem countingSortArray_indexedWork_le [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α) (hxs : AllKeysLe key xs maxKey) :
    (CountingExecution.execute maxKey key xs).indexedWork ≤
      6 * (xs.length + maxKey + 1) := by
  rw [CountingExecution.execute_indexedWork maxKey key xs hxs]
  omega

              end MutableOutputend Chapter08end CLRS

Imports

import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort
import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.Execution
import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.MutableOutputArray

8.3. Radix Sort

This file proves the pure correctness spine for radix sort from the stable counting-sort theorem in Section 8.2.

The model is intentionally abstract. A list of digit functions is supplied in least-significant to most-significant order. Each pass executes the stable indexed counting controller and refines countingSortBy over its digit. The final theorems say that the result is ordered by the corresponding most-significant-first lexicographic relation, preserves membership, preserves the input order inside each complete digit signature, and hence captures the CLRS stable-pass proof spine.

The final layer instantiates the abstract digit interface with concrete base-b digits for natural-number keys, packages ordinary key ordering behind a named digit-order bridge, and discharges that bridge for bounded fixed-width keys. The final concrete theorem therefore says radix sort returns a list ordered by the ordinary natural-number key when every key is represented inside the supplied digit window.

The execution layer calls CountingExecution.execute for every digit. radixSortByWithCost sums controller visits read from those executions; radixSortByWithIndexedWork expands the key/index/list-operation ledger. Both erase to the public radixSortBy, whose passes also call the same indexed controller. Bounded digits give exact returned-counter formulas and O(d(n+k)) bounds.

The stable-bucket controller is a refinement of counting sort, not the literal cumulative-counter decrement program. Indexed operations and key evaluation are unit-cost primitives; persistent-array copying and machine time remain outside this ledger.

              namespace CLRSnamespace Chapter08universe uvariable {α : Type u}

Relation-ordered lists and digit lexicographic order

Pairwise list ordering by a relation. This is stronger than adjacent ordering and is convenient for stable bucket proofs, since filtering a pairwise-ordered list preserves the order relation.

abbrev OrderedRel (rel : α → α → Prop) (xs : List α) : Prop :=
  xs.Pairwise rel

A single higher-priority digit extends an existing lower-priority order.

def LexWith (digit : α → Nat) (rel : α → α → Prop) (x y : α) : Prop :=
  digit x < digit y ∨ (digit x = digit y ∧ rel x y)

Accumulate a radix lexicographic relation from digits supplied least-significant first. Each later digit becomes higher priority.

def RadixRel : List (α → Nat) → (α → α → Prop) → α → α → Prop
  | [], rel => rel
  | digit :: digits, rel => RadixRel digits (LexWith digit rel)

The public lexicographic relation induced by low-to-high radix digits.

def RadixLex (digitsLow : List (α → Nat)) : α → α → Prop :=
  RadixRel digitsLow (fun _ _ => True)

theorem orderedRel_trivial (xs : List α) :
    OrderedRel (fun _ _ => True) xs := by
  induction xs with
  | nil =>
      exact List.Pairwise.nil
  | cons _ xs ih =>
      exact List.Pairwise.cons (by simp) ih

theorem orderedRel_append_of_rel {rel : α → α → Prop} {xs ys : List α}
    (hxs : OrderedRel rel xs) (hys : OrderedRel rel ys)
    (hrel : ∀ x ∈ xs, ∀ y ∈ ys, rel x y) :
    OrderedRel rel (xs ++ ys) := by
  exact List.pairwise_append.mpr ⟨hxs, hys, hrel⟩

Turn a pairwise relation order into the adjacent key-order predicate used by the counting-sort section, provided the relation implies key monotonicity on the same list.

theorem orderedBy_of_orderedRel_on {rel : α → α → Prop} {key : α → Nat}
    {xs : List α} (hxs : OrderedRel rel xs)
    (hrel : ∀ x ∈ xs, ∀ y ∈ xs, rel x y → key x ≤ key y) :
    OrderedBy key xs := by
  induction xs with
  | nil =>
      trivial
  | cons x xs ih =>
      cases xs with
      | nil =>
          trivial
      | cons y ys =>
          cases hxs with
          | cons hhead htail =>
              refine ⟨?_, ih htail ?_⟩
              · exact hrel x (by simp) y (by simp) (hhead y (by simp))
              · intro a ha b hb hab
                exact hrel a (by simp [ha]) b (by simp [hb]) hab

theorem orderedRel_bucket {rel : α → α → Prop} {key : α → Nat}
    {xs : List α} (k : Nat) (hxs : OrderedRel rel xs) :
    OrderedRel rel (bucket key xs k) := by
  exact List.Pairwise.filter (fun x => key x == k) hxs



theorem orderedRel_of_same_digit {rel : α → α → Prop} {digit : α → Nat}
    {xs : List α} {k : Nat}
    (hxs : OrderedRel rel xs) (hall : ∀ x ∈ xs, digit x = k) :
    OrderedRel (LexWith digit rel) xs := by
  induction xs with
  | nil =>
      exact List.Pairwise.nil
  | cons x xs ih =>
      cases hxs with
      | cons hhead htail =>
          refine List.Pairwise.cons ?_ (ih htail ?_)
          · intro y hy
            exact Or.inr ⟨by rw [hall x (by simp), hall y (by simp [hy])],
              hhead y hy⟩
          · intro y hy
            exact hall y (by simp [hy])

One stable radix pass

A stable counting-sort pass by a new digit upgrades a lower-priority relation to a lexicographic relation with the new digit as the most significant criterion.


theorem radixPass_orderedRel
    (maxDigit : Nat) (digit : α → Nat) (rel : α → α → Prop) (xs : List α)
    (hxs : OrderedRel rel xs) :
    OrderedRel (LexWith digit rel) (countingSortBy maxDigit digit xs) := by
  induction maxDigit with
  | zero =>
      simpa [countingSortBy] using
        orderedRel_of_same_digit
          (orderedRel_bucket (key := digit) 0 hxs)
          (bucket_all_keys_eq digit xs 0)
  | succ maxDigit ih =>
      rw [countingSortBy_succ]
      refine orderedRel_append_of_rel ih ?_ ?_
      · exact orderedRel_of_same_digit
          (orderedRel_bucket (key := digit) (maxDigit + 1) hxs)
          (bucket_all_keys_eq digit xs (maxDigit + 1))
      · intro x hx y hy
        have hxle : digit x ≤ maxDigit :=
          countingSortBy_allKeysLe maxDigit digit xs x hx
        have hykey : digit y = maxDigit + 1 := (mem_bucket_iff.mp hy).2
        exact Or.inl (Nat.lt_of_le_of_lt hxle (by simp [hykey]))

Radix sort

Radix sort by stable counting-sort passes. Digits are supplied in least-significant to most-significant order.

def radixSortBy (maxDigit : Nat) : List (α → Nat) → List α → List α
  | [], xs => xs
  | digit :: digits, xs =>
      radixSortBy maxDigit digits (CountingExecution.execute maxDigit digit xs).output.toList

All digit functions are bounded by the declared maximum digit.

def AllDigitsLe (digitsLow : List (α → Nat)) (xs : List α)
    (maxDigit : Nat) : Prop :=
  ∀ digit ∈ digitsLow, AllKeysLe digit xs maxDigit

Stability by complete digit signatures

The subsequence of elements whose values match sample on every radix digit, preserving the ambient list order.

Equality of this list before and after radix sort is the direct stability statement: items with the same complete digit signature appear in their original relative order.

def digitClass (digitsLow : List (α → Nat)) (sample : α) (xs : List α) :
    List α :=
  xs.filter fun x => digitsLow.all fun digit => digit x == digit sample

              theorem digitClass_cons_filter (digit : α → Nat)
    (digitsLow : List (α → Nat)) (sample : α) (xs : List α) :
    digitClass (digit :: digitsLow) sample xs =
      (digitClass digitsLow sample xs).filter
        (fun x => digit x == digit sample) := by
  simp [digitClass, List.filter_filter]theorem digitClass_cons_bucket (digit : α → Nat)
    (digitsLow : List (α → Nat)) (sample : α) (xs : List α) :
    digitClass (digit :: digitsLow) sample xs =
      digitClass digitsLow sample (bucket digit xs (digit sample)) := by
  simp [digitClass, bucket, List.filter_filter, Bool.and_comm]

theorem countingSortBy_digitClass_cons_eq
    (maxDigit : Nat) (digit : α → Nat) (digitsLow : List (α → Nat))
    (sample : α) (xs : List α) (hxs : AllKeysLe digit xs maxDigit) :
    digitClass (digit :: digitsLow) sample
        (countingSortBy maxDigit digit xs) =
      digitClass (digit :: digitsLow) sample xs := by
  rw [digitClass_cons_bucket, countingSortBy_bucket_eq maxDigit digit xs hxs,
    digitClass_cons_bucket]theorem allDigitsLe_of_mem_iff {digitsLow : List (α → Nat)}
    {xs ys : List α} {maxDigit : Nat}
    (h : AllDigitsLe digitsLow xs maxDigit)
    (hmem : ∀ x, x ∈ ys ↔ x ∈ xs) :
    AllDigitsLe digitsLow ys maxDigit := by
  intro digit hdigit x hx
  exact h digit hdigit x ((hmem x).mp hx)theorem radixSortBy_ordered_aux
    (maxDigit : Nat) (digitsLow : List (α → Nat))
    (rel : α → α → Prop) (xs : List α)
    (hxs : OrderedRel rel xs) :
    OrderedRel (RadixRel digitsLow rel)
      (radixSortBy maxDigit digitsLow xs) := by
  induction digitsLow generalizing rel xs with
  | nil =>
      simpa [radixSortBy, CountingExecution.execute_result, RadixRel] using hxs
  | cons digit digits ih =>
      have hpass : OrderedRel (LexWith digit rel)
          (countingSortBy maxDigit digit xs) :=
        radixPass_orderedRel maxDigit digit rel xs hxs
      simpa [radixSortBy, CountingExecution.execute_result, RadixRel] using
        ih (LexWith digit rel) (countingSortBy maxDigit digit xs) hpass

Radix sort returns a list ordered by the induced digit lexicographic order.

theorem radixSortBy_ordered
    (maxDigit : Nat) (digitsLow : List (α → Nat)) (xs : List α) :
    OrderedRel (RadixLex digitsLow)
      (radixSortBy maxDigit digitsLow xs) := by
  simpa [RadixLex] using
    radixSortBy_ordered_aux maxDigit digitsLow (fun _ _ => True) xs
      (orderedRel_trivial xs)

              

theorem radixSortBy_mem_iff
    (maxDigit : Nat) :
    ∀ (digitsLow : List (α → Nat)) (xs : List α),
      AllDigitsLe digitsLow xs maxDigit →
      ∀ x, x ∈ radixSortBy maxDigit digitsLow xs ↔ x ∈ xs := by
  intro digitsLow
  induction digitsLow with
  | nil =>
      intro xs _ x
      simp [radixSortBy]
  | cons digit digits ih =>
      intro xs hdigits x
      have hdigit : AllKeysLe digit xs maxDigit :=
        hdigits digit (by simp)
      have hpass_mem :
          ∀ y, y ∈ countingSortBy maxDigit digit xs ↔ y ∈ xs :=
        countingSortBy_mem_iff maxDigit digit xs hdigit
      have hrest : AllDigitsLe digits
          (countingSortBy maxDigit digit xs) maxDigit := by
        refine allDigitsLe_of_mem_iff ?_ hpass_mem
        intro d hd
        exact hdigits d (by simp [hd])
      have htail := ih (countingSortBy maxDigit digit xs) hrest x
      simpa only [radixSortBy, CountingExecution.execute_result] using htail.trans (hpass_mem x)

theorem radixSortBy_perm [DecidableEq α]
    (maxDigit : Nat) :
    ∀ (digitsLow : List (α → Nat)) (xs : List α),
      AllDigitsLe digitsLow xs maxDigit →
      (radixSortBy maxDigit digitsLow xs).Perm xs := by
  intro digitsLow
  induction digitsLow with
  | nil =>
      intro xs _
      simp [radixSortBy]
  | cons digit digits ih =>
      intro xs hdigits
      have hdigit : AllKeysLe digit xs maxDigit :=
        hdigits digit (by simp)
      have hpass_perm : (countingSortBy maxDigit digit xs).Perm xs :=
        countingSortBy_perm maxDigit digit xs hdigit
      have hpass_mem :
          ∀ y, y ∈ countingSortBy maxDigit digit xs ↔ y ∈ xs := by
        intro y
        exact hpass_perm.mem_iff
      have hrest : AllDigitsLe digits
          (countingSortBy maxDigit digit xs) maxDigit := by
        refine allDigitsLe_of_mem_iff ?_ hpass_mem
        intro d hd
        exact hdigits d (by simp [hd])
      simpa only [radixSortBy, CountingExecution.execute_result] using
        (ih (countingSortBy maxDigit digit xs) hrest).trans hpass_perm

theorem radixSortBy_digitClass_eq
    (maxDigit : Nat) :
    ∀ (digitsLow : List (α → Nat)) (xs : List α),
      AllDigitsLe digitsLow xs maxDigit →
      ∀ sample,
        digitClass digitsLow sample (radixSortBy maxDigit digitsLow xs) =
          digitClass digitsLow sample xs := by
  intro digitsLow
  induction digitsLow with
  | nil =>
      intro xs _ sample
      simp [radixSortBy, digitClass]
  | cons digit digits ih =>
      intro xs hdigits sample
      let pass := countingSortBy maxDigit digit xs
      have hdigit : AllKeysLe digit xs maxDigit :=
        hdigits digit (by simp)
      have hpass_mem :
          ∀ y, y ∈ pass ↔ y ∈ xs := by
        intro y
        exact countingSortBy_mem_iff maxDigit digit xs hdigit y
      have hrest : AllDigitsLe digits pass maxDigit := by
        refine allDigitsLe_of_mem_iff ?_ hpass_mem
        intro d hd
        exact hdigits d (by simp [hd])
      have htail :
          digitClass digits sample (radixSortBy maxDigit digits pass) =
            digitClass digits sample pass :=
        ih pass hrest sample
      calc
        digitClass (digit :: digits) sample
            (radixSortBy maxDigit (digit :: digits) xs)
            =
          digitClass (digit :: digits) sample
            (radixSortBy maxDigit digits pass) := by
              simp [radixSortBy, CountingExecution.execute_result, pass]
        _ =
          (digitClass digits sample
              (radixSortBy maxDigit digits pass)).filter
            (fun x => digit x == digit sample) := by
              rw [digitClass_cons_filter]
        _ =
          (digitClass digits sample pass).filter
            (fun x => digit x == digit sample) := by
              rw [htail]
        _ = digitClass (digit :: digits) sample pass := by
              rw [digitClass_cons_filter]
        _ = digitClass (digit :: digits) sample xs :=
              countingSortBy_digitClass_cons_eq maxDigit digit digits sample xs
                hdigit

Radix sort is stable with respect to complete digit signatures: filtering the output to all elements matching a fixed sample on every digit gives exactly the same ordered subsequence as filtering the input.

theorem radixSortBy_stable
    (maxDigit : Nat) (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) (sample : α) :
    digitClass digitsLow sample (radixSortBy maxDigit digitsLow xs) =
      digitClass digitsLow sample xs :=
  radixSortBy_digitClass_eq maxDigit digitsLow xs hdigits sample

Reader-facing correctness theorem for abstract radix sort.

theorem radixSortBy_correct [DecidableEq α]
    (maxDigit : Nat) (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    OrderedRel (RadixLex digitsLow)
        (radixSortBy maxDigit digitsLow xs) ∧
      (∀ x, x ∈ radixSortBy maxDigit digitsLow xs ↔ x ∈ xs) ∧
      (radixSortBy maxDigit digitsLow xs).Perm xs :=
  ⟨radixSortBy_ordered maxDigit digitsLow xs,
    radixSortBy_mem_iff maxDigit digitsLow xs hdigits,
    radixSortBy_perm maxDigit digitsLow xs hdigits⟩

Reader-facing correctness theorem including the explicit stability clause.

theorem radixSortBy_correct_stable [DecidableEq α]
    (maxDigit : Nat) (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    OrderedRel (RadixLex digitsLow)
        (radixSortBy maxDigit digitsLow xs) ∧
      (∀ sample,
        digitClass digitsLow sample (radixSortBy maxDigit digitsLow xs) =
          digitClass digitsLow sample xs) ∧
      (∀ x, x ∈ radixSortBy maxDigit digitsLow xs ↔ x ∈ xs) ∧
      (radixSortBy maxDigit digitsLow xs).Perm xs :=
  ⟨radixSortBy_ordered maxDigit digitsLow xs,
    radixSortBy_stable maxDigit digitsLow xs hdigits,
    radixSortBy_mem_iff maxDigit digitsLow xs hdigits,
    radixSortBy_perm maxDigit digitsLow xs hdigits⟩

Concrete base-b digit extraction

The ith least-significant base-base digit of a natural number.

For example, digit 0 is the units digit and digit 1 is the next more significant digit. The definition is intentionally small so the abstract radix-sort theorem above can be reused without changing its proof.

def baseDigit (base i n : Nat) : Nat :=
  (n / base ^ i) % base

The low-to-high list of concrete base-base digit functions.

def baseDigitsLow (base digitCount : Nat) (key : α → Nat) :
    List (α → Nat) :=
  (List.range digitCount).map fun i x => baseDigit base i (key x)

Every extracted base digit is bounded by base - 1.

theorem baseDigit_le_max (base i n : Nat) (hbase : 0 < base) :
    baseDigit base i n ≤ base - 1 := by
  simpa [baseDigit, Nat.pred_eq_sub_one] using
    Nat.le_pred_of_lt (Nat.mod_lt (n / base ^ i) hbase)

For a one-digit key smaller than the base, the extracted digit is the key.

theorem baseDigit_zero_eq_self_of_lt {base n : Nat} (hn : n < base) :
    baseDigit base 0 n = n := by
  simpa [baseDigit] using Nat.mod_eq_of_lt hn

The concrete digit list satisfies the abstract bounded-digit hypothesis.


theorem baseDigitsLow_allDigitsLe
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base) :
    AllDigitsLe (baseDigitsLow base digitCount key) xs (base - 1) := by
  intro digit hdigit x _hx
  rw [baseDigitsLow] at hdigit
  rcases List.mem_map.mp hdigit with ⟨i, _hi, rfl⟩
  exact baseDigit_le_max base i (key x) hbase

Reinterpreting the first digitCount extracted low-to-high digits gives the corresponding residue modulo base ^ digitCount.


theorem baseDigitsLow_value_eq_mod_pow
    (base digitCount : Nat) (key : α → Nat) (x : α) :
    Nat.ofDigits base
        ((baseDigitsLow base digitCount key).map fun digit => digit x) =
      key x % base ^ digitCount := by
  simp [baseDigitsLow]
  induction digitCount with
  | zero =>
      simp [Nat.mod_one]
  | succ k ih =>
      rw [List.range_succ, List.map_append, Nat.ofDigits_append, ih]
      simp [baseDigit, Nat.pow_succ]
      conv_rhs =>
        rw [← Nat.mod_add_div ((key x) % (base ^ k * base)) (base ^ k)]
      rw [Nat.mod_mul_right_mod, Nat.mod_mul_right_div_self]

If a key fits into the declared fixed-width digit window, the extracted digits reconstruct the key exactly.


theorem baseDigitsLow_value_eq_self_of_lt
    (base digitCount : Nat) (key : α → Nat) (x : α)
    (hkey : key x < base ^ digitCount) :
    Nat.ofDigits base
        ((baseDigitsLow base digitCount key).map fun digit => digit x) =
      key x := by
  rw [baseDigitsLow_value_eq_mod_pow, Nat.mod_eq_of_lt hkey]

Accumulator form of the radix lexicographic value lemma. The accumulator low stores lower-priority digits and is assumed to be smaller than the current place-value scale.


theorem radixRel_accValue_le
    (base scale : Nat) (digitsLow : List (α → Nat))
    (low : α → Nat) (rel : α → α → Prop)
    (hbase : 0 < base) (hscale : 0 < scale)
    (hlow : ∀ z, low z < scale)
    (hrel : ∀ ⦃x y⦄, rel x y → low x ≤ low y)
    (hdigits : ∀ digit ∈ digitsLow, ∀ z, digit z < base) :
    ∀ ⦃x y : α⦄,
      RadixRel digitsLow rel x y →
        low x + scale * Nat.ofDigits base
            (digitsLow.map fun digit => digit x) ≤
        low y + scale * Nat.ofDigits base
            (digitsLow.map fun digit => digit y) := by
  induction digitsLow generalizing low rel scale with
  | nil =>
      intro x y hxy
      simpa using hrel hxy
  | cons digit digits ih =>
      intro x y hxy
      have hdigit : ∀ z, digit z < base := hdigits digit (by simp)
      have hdigits_tail : ∀ d ∈ digits, ∀ z, d z < base := by
        intro d hd z
        exact hdigits d (by simp [hd]) z
      have hscale' : 0 < scale * base := Nat.mul_pos hscale hbase
      have hlow' :
          ∀ z, low z + scale * digit z < scale * base := by
        intro z
        have hlt1 :
            low z + scale * digit z < scale * (digit z + 1) := by
          simpa [Nat.mul_succ, Nat.add_comm, Nat.add_left_comm,
            Nat.add_assoc] using
            Nat.add_lt_add_right (hlow z) (scale * digit z)
        have hle2 : scale * (digit z + 1) ≤ scale * base :=
          Nat.mul_le_mul_left scale (Nat.succ_le_of_lt (hdigit z))
        exact Nat.lt_of_lt_of_le hlt1 hle2
      have hrel' :
          ∀ ⦃a b⦄, LexWith digit rel a b →
            low a + scale * digit a ≤ low b + scale * digit b := by
        intro a b hab
        rcases hab with hlt | ⟨heq, hr⟩
        · have hlt1 :
              low a + scale * digit a < scale * (digit a + 1) := by
            simpa [Nat.mul_succ, Nat.add_comm, Nat.add_left_comm,
              Nat.add_assoc] using
              Nat.add_lt_add_right (hlow a) (scale * digit a)
          have hle2 : scale * (digit a + 1) ≤ scale * digit b :=
            Nat.mul_le_mul_left scale (Nat.succ_le_of_lt hlt)
          exact Nat.le_trans (Nat.le_of_lt hlt1)
            (Nat.le_trans hle2 (Nat.le_add_left _ _))
        · rw [heq]
          exact Nat.add_le_add_right (hrel hr) _
      have hmain := ih (low := fun z => low z + scale * digit z)
        (rel := LexWith digit rel) (scale := scale * base)
        hscale' hlow' hrel' hdigits_tail hxy
      simpa [Nat.ofDigits, Nat.mul_add, Nat.mul_assoc, Nat.add_assoc,
        Nat.add_comm, Nat.add_left_comm] using hmain

Radix lexicographic order on bounded digits is monotone for the natural number obtained by reinterpreting the low-to-high digit list.


theorem radixLex_value_le
    (base : Nat) (digitsLow : List (α → Nat)) (x y : α)
    (hbase : 0 < base)
    (hdigits : ∀ digit ∈ digitsLow, ∀ z, digit z < base)
    (hxy : RadixLex digitsLow x y) :
    Nat.ofDigits base (digitsLow.map fun digit => digit x) ≤
      Nat.ofDigits base (digitsLow.map fun digit => digit y) := by
  have hmain := radixRel_accValue_le base 1 digitsLow
    (fun _ : α => 0) (fun _ _ : α => True)
    hbase (by decide) (by intro _; decide)
    (by intro _ _ _; exact Nat.zero_le _) hdigits hxy
  simpa using hmain

Concrete base digits satisfy the bounded-digit side condition needed by radixLex_value_le.


theorem baseDigitsLow_digits_lt
    (base digitCount : Nat) (key : α → Nat) (hbase : 0 < base) :
    ∀ digit ∈ baseDigitsLow base digitCount key, ∀ z, digit z < base := by
  intro digit hdigit z
  rw [baseDigitsLow] at hdigit
  rcases List.mem_map.mp hdigit with ⟨i, _hi, rfl⟩
  simpa [baseDigit] using Nat.mod_lt (key z / base ^ i) hbase

The arithmetic bridge needed to turn digit-lexicographic order into ordinary key order on a concrete input domain.

def RadixDigitOrderRespectsKey
    (base digitCount : Nat) (key : α → Nat) (domain : List α) : Prop :=
  ∀ x ∈ domain, ∀ y ∈ domain,
    RadixLex (baseDigitsLow base digitCount key) x y → key x ≤ key y

For fixed-width bounded keys, the concrete radix digit order respects ordinary natural-number key order.


theorem radixDigitOrderRespectsKey_of_bounded
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base)
    (hkeys : ∀ x ∈ xs, key x < base ^ digitCount) :
    RadixDigitOrderRespectsKey base digitCount key xs := by
  intro x hx y hy hxy
  have hvalue := radixLex_value_le base
    (baseDigitsLow base digitCount key) x y hbase
    (baseDigitsLow_digits_lt base digitCount key hbase) hxy
  rw [baseDigitsLow_value_eq_self_of_lt base digitCount key x
      (hkeys x hx),
    baseDigitsLow_value_eq_self_of_lt base digitCount key y
      (hkeys y hy)] at hvalue
  exact hvalue

Concrete radix sort for natural-number keys, using the low-to-high base digits of key.

def radixSortNatBy (base digitCount : Nat) (key : α → Nat) (xs : List α) :
    List α :=
  radixSortBy (base - 1) (baseDigitsLow base digitCount key) xs

Reader-facing concrete radix-sort correctness theorem.

The ordering clause is still the digit-lexicographic relation induced by the chosen concrete digits. A later arithmetic refinement can identify this relation with ordinary natural-number ordering under a bounded-key hypothesis.

theorem radixSortNatBy_correct_stable [DecidableEq α]
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base) :
    OrderedRel (RadixLex (baseDigitsLow base digitCount key))
        (radixSortNatBy base digitCount key xs) ∧
      (∀ sample,
        digitClass (baseDigitsLow base digitCount key) sample
          (radixSortNatBy base digitCount key xs) =
          digitClass (baseDigitsLow base digitCount key) sample xs) ∧
      (∀ x, x ∈ radixSortNatBy base digitCount key xs ↔ x ∈ xs) ∧
      (radixSortNatBy base digitCount key xs).Perm xs := by
  simpa [radixSortNatBy] using
    radixSortBy_correct_stable (base - 1) (baseDigitsLow base digitCount key)
      xs (baseDigitsLow_allDigitsLe base digitCount key xs hbase)

If every key in the input fits in one base-base digit, then the concrete radix digit order is already ordinary key order.


theorem radixDigitOrderRespectsKey_singleDigit
    (base : Nat) (key : α → Nat) (xs : List α)
    (hkeys : ∀ x ∈ xs, key x < base) :
    RadixDigitOrderRespectsKey base 1 key xs := by
  intro x hx y hy hxy
  have hx_digit :
      baseDigit base 0 (key x) = key x :=
    baseDigit_zero_eq_self_of_lt (hkeys x hx)
  have hy_digit :
      baseDigit base 0 (key y) = key y :=
    baseDigit_zero_eq_self_of_lt (hkeys y hy)
  change LexWith (fun z => baseDigit base 0 (key z)) (fun _ _ => True) x y at hxy
  dsimp [LexWith] at hxy
  rw [hx_digit, hy_digit] at hxy
  rcases hxy with hlt | ⟨heq, _⟩
  · exact Nat.le_of_lt hlt
  · exact Nat.le_of_eq heq

If the concrete digit lexicographic relation respects the natural key order on the input domain, concrete radix sort returns a list ordered by that key.

theorem radixSortNatBy_keyOrdered_of_digitOrder [DecidableEq α]
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base)
    (hdigit_order : RadixDigitOrderRespectsKey base digitCount key xs) :
    OrderedBy key (radixSortNatBy base digitCount key xs) := by
  have hcorrect := radixSortNatBy_correct_stable base digitCount key xs hbase
  have hmem :
      ∀ x, x ∈ radixSortNatBy base digitCount key xs ↔ x ∈ xs :=
    hcorrect.2.2.1
  exact orderedBy_of_orderedRel_on hcorrect.1
    (by
      intro x hx y hy hxy
      exact hdigit_order x ((hmem x).mp hx) y ((hmem y).mp hy) hxy)

Concrete radix-sort correctness theorem with ordinary key ordering separated from the remaining base-b arithmetic obligation.

theorem radixSortNatBy_correct_keyOrdered_of_digitOrder [DecidableEq α]
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base)
    (hdigit_order : RadixDigitOrderRespectsKey base digitCount key xs) :
    OrderedBy key (radixSortNatBy base digitCount key xs) ∧
      (∀ sample,
        digitClass (baseDigitsLow base digitCount key) sample
          (radixSortNatBy base digitCount key xs) =
          digitClass (baseDigitsLow base digitCount key) sample xs) ∧
      (∀ x, x ∈ radixSortNatBy base digitCount key xs ↔ x ∈ xs) ∧
      (radixSortNatBy base digitCount key xs).Perm xs := by
  have hcorrect := radixSortNatBy_correct_stable base digitCount key xs hbase
  exact ⟨radixSortNatBy_keyOrdered_of_digitOrder base digitCount key xs hbase
      hdigit_order,
    hcorrect.2.1,
    hcorrect.2.2.1,
    hcorrect.2.2.2⟩

Concrete one-pass radix-sort correctness when all keys are already below the base. This is the smallest arithmetic discharge of RadixDigitOrderRespectsKey.

theorem radixSortNatBy_correct_keyOrdered_singleDigit [DecidableEq α]
    (base : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base) (hkeys : ∀ x ∈ xs, key x < base) :
    OrderedBy key (radixSortNatBy base 1 key xs) ∧
      (∀ sample,
        digitClass (baseDigitsLow base 1 key) sample
          (radixSortNatBy base 1 key xs) =
          digitClass (baseDigitsLow base 1 key) sample xs) ∧
      (∀ x, x ∈ radixSortNatBy base 1 key xs ↔ x ∈ xs) ∧
      (radixSortNatBy base 1 key xs).Perm xs :=
  radixSortNatBy_correct_keyOrdered_of_digitOrder base 1 key xs hbase
    (radixDigitOrderRespectsKey_singleDigit base key xs hkeys)

Concrete fixed-width radix-sort correctness for bounded natural-number keys. The bound key x < base ^ digitCount says the supplied digit window is wide enough to represent every input key.

theorem radixSortNatBy_correct_keyOrdered_of_bounded [DecidableEq α]
    (base digitCount : Nat) (key : α → Nat) (xs : List α)
    (hbase : 0 < base)
    (hkeys : ∀ x ∈ xs, key x < base ^ digitCount) :
    OrderedBy key (radixSortNatBy base digitCount key xs) ∧
      (∀ sample,
        digitClass (baseDigitsLow base digitCount key) sample
          (radixSortNatBy base digitCount key xs) =
          digitClass (baseDigitsLow base digitCount key) sample xs) ∧
      (∀ x, x ∈ radixSortNatBy base digitCount key xs ↔ x ∈ xs) ∧
      (radixSortNatBy base digitCount key xs).Perm xs :=
  radixSortNatBy_correct_keyOrdered_of_digitOrder base digitCount key xs hbase
    (radixDigitOrderRespectsKey_of_bounded base digitCount key xs hbase hkeys)

Running-time / cost layer

Counting sort preserves length when every key is at most maxKey.

theorem countingSortBy_length_eq_of_allKeysLe [DecidableEq α]
    (maxKey : Nat) (key : α → Nat) (xs : List α) (hxs : AllKeysLe key xs maxKey) :
    (countingSortBy maxKey key xs).length = xs.length :=
  (countingSortBy_perm maxKey key xs hxs).length_eq

Each pass runs the indexed counting controller once. The supplied ledger reads counters from that same returned execution record.

def radixSortByWithLedger (maxDigit : Nat) (ledger : CountingExecution.Execution α → Nat) :
    List (α → Nat) → List α → List α × Nat
  | [], xs => (xs, 0)
  | digit :: digits, xs =>
      let pass := CountingExecution.execute maxDigit digit xs
      let rest := radixSortByWithLedger maxDigit ledger digits pass.output.toList
      (rest.1, ledger pass + rest.2)

Actual controller visits accumulated across stable indexed counting passes.

def radixSortByWithCost (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α) : List α × Nat :=
  radixSortByWithLedger maxDigit CountingExecution.Execution.controllerVisits digitsLow xs

Expanded key/index/list-operation ledger from those same counting passes.

def radixSortByWithIndexedWork (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α) : List α × Nat :=
  radixSortByWithLedger maxDigit CountingExecution.Execution.indexedWork digitsLow xs

theorem radixSortByWithLedger_result (maxDigit : Nat)
    (ledger : CountingExecution.Execution α → Nat)
    (digitsLow : List (α → Nat)) (xs : List α) :
    (radixSortByWithLedger maxDigit ledger digitsLow xs).1 =
      radixSortBy maxDigit digitsLow xs := by
  induction digitsLow generalizing xs with
  | nil => rfl
  | cons digit digits ih =>
      simp only [radixSortByWithLedger, radixSortBy]
      exact ih _

Erasing the cost preserves the public radix-sort result.

theorem radixSortByWithCost_result (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α) :
    (radixSortByWithCost maxDigit digitsLow xs).1 =
      radixSortBy maxDigit digitsLow xs :=
  radixSortByWithLedger_result maxDigit _ digitsLow xs

theorem radixSortByWithIndexedWork_result (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α) :
    (radixSortByWithIndexedWork maxDigit digitsLow xs).1 =
      radixSortBy maxDigit digitsLow xs :=
  radixSortByWithLedger_result maxDigit _ digitsLow xs



private theorem radixSortByWithLedger_cost_eq [DecidableEq α] (maxDigit : Nat)
    (ledger : CountingExecution.Execution α → Nat) (passCost : Nat → Nat)
    (hledger : ∀ digit ys, AllKeysLe digit ys maxDigit →
      ledger (CountingExecution.execute maxDigit digit ys) = passCost ys.length)
    (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    (radixSortByWithLedger maxDigit ledger digitsLow xs).2 =
      digitsLow.length * passCost xs.length := by
  induction digitsLow generalizing xs with
  | nil => simp [radixSortByWithLedger]
  | cons digit digits ih =>
      have hdigit : AllKeysLe digit xs maxDigit := hdigits digit (by simp)
      have hlen : (countingSortBy maxDigit digit xs).length = xs.length :=
        countingSortBy_length_eq_of_allKeysLe maxDigit digit xs hdigit
      have hrest : AllDigitsLe digits (countingSortBy maxDigit digit xs) maxDigit := by
        intro d hd x hx
        exact hdigits d (by simp [hd]) x
          ((countingSortBy_mem_iff maxDigit digit xs hdigit x).mp hx)
      simp only [radixSortByWithLedger, CountingExecution.execute_result]
      rw [hledger digit xs hdigit, ih _ hrest, hlen]
      simp only [List.length_cons]
      ring

Under bounded digits, length preservation makes every pass return the same controller-visit total.


theorem radixSortByWithCost_cost_eq [DecidableEq α] (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    (radixSortByWithCost maxDigit digitsLow xs).2 =
      digitsLow.length * MutableOutput.countingSortArrayCost maxDigit xs.length := by
  apply radixSortByWithLedger_cost_eq maxDigit _ _ ?_ digitsLow xs hdigits
  intro digit ys hy
  rw [CountingExecution.execute_controllerVisits maxDigit digit ys hy,
    MutableOutput.countingSortArrayCost_eq]

The expanded operation ledger is also linear per digit pass.

theorem radixSortByWithIndexedWork_cost_eq [DecidableEq α] (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    (radixSortByWithIndexedWork maxDigit digitsLow xs).2 =
      digitsLow.length * (6 * xs.length + 2 * (maxDigit + 1)) := by
  exact radixSortByWithLedger_cost_eq maxDigit CountingExecution.Execution.indexedWork
    (fun n => 6 * n + 2 * (maxDigit + 1))
    (fun digit ys hy => CountingExecution.execute_indexedWork maxDigit digit ys hy)
    digitsLow xs hdigits

Uniform bound on the returned expanded operation ledger.


theorem radixSortByWithIndexedWork_cost_le [DecidableEq α] (maxDigit : Nat)
    (digitsLow : List (α → Nat)) (xs : List α)
    (hdigits : AllDigitsLe digitsLow xs maxDigit) :
    (radixSortByWithIndexedWork maxDigit digitsLow xs).2 ≤
      6 * digitsLow.length * (xs.length + maxDigit + 1) := by
  rw [radixSortByWithIndexedWork_cost_eq maxDigit digitsLow xs hdigits]
  calc
    digitsLow.length * (6 * xs.length + 2 * (maxDigit + 1)) ≤
        digitsLow.length * (6 * (xs.length + maxDigit + 1)) := by gcongr; omega
    _ = _ := by ring

Total indexed counting-controller visits of concrete base-base radix sort over n keys: digitCount passes, each using the stable indexed controller with alphabet size base.

def radixSortNatByCost (base digitCount n : Nat) : Nat :=
  digitCount * MutableOutput.countingSortArrayCost (base - 1) n

The concrete cost equals the cost of the costed radix-sort execution on the concrete digit list. The bounded-digit hypothesis is discharged by baseDigitsLow_allDigitsLe.


theorem radixSortNatBy_cost_eq [DecidableEq α] (base digitCount : Nat)
    (key : α → Nat) (xs : List α) (hbase : 0 < base) :
    (radixSortByWithCost (base - 1) (baseDigitsLow base digitCount key) xs).2 =
      radixSortNatByCost base digitCount xs.length := by
  unfold radixSortNatByCost
  rw [radixSortByWithCost_cost_eq (base - 1) (baseDigitsLow base digitCount key) xs
    (baseDigitsLow_allDigitsLe base digitCount key xs hbase)]
  simp [baseDigitsLow]

The mutable counting-sort work for alphabet size base is at most 2 * (n + base + 1).

theorem countingSortArrayCost_le_two_mul (base n : Nat) :
    MutableOutput.countingSortArrayCost (base - 1) n ≤ 2 * (n + base + 1) := by
  calc
    MutableOutput.countingSortArrayCost (base - 1) n
        ≤ 2 * (n + ((base - 1) + 1)) :=
          MutableOutput.countingSortArrayCost_le (base - 1) n
    _ ≤ 2 * (n + base + 1) := by
      apply Nat.mul_le_mul_left
      omega

The concrete radix-sort cost is at most 2 * (digitCount * (n + base + 1)).

theorem radixSortNatByCost_le (base digitCount n : Nat) :
    radixSortNatByCost base digitCount n ≤ 2 * (digitCount * (n + base + 1)) := by
  unfold radixSortNatByCost
  have h := countingSortArrayCost_le_two_mul base n
  calc
    digitCount * MutableOutput.countingSortArrayCost (base - 1) n
        ≤ digitCount * (2 * (n + base + 1)) := Nat.mul_le_mul_left digitCount h
    _ = 2 * (digitCount * (n + base + 1)) := by ring

Linear O(d(n+k)) work bound. There is a constant c (here 2) such that the concrete radix-sort work is at most c * (d * (n + k + 1)) for every alphabet size k = base, digit count d = digitCount, and input length n.

theorem radixSortNatByCost_bigO :
    ∃ c : Nat, ∀ base digitCount n : Nat,
      radixSortNatByCost base digitCount n ≤ c * (digitCount * (n + base + 1)) := by
  refine ⟨2, ?_⟩
  intro base digitCount n
  exact radixSortNatByCost_le base digitCount n

end Chapter08end CLRS

Imports

import CLRSLean.FourthEdition.Chapter_08.Section_08_3_Radix_Sort
import CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort.Execution
import CLRSLean.Chapter_03.Section_03_1_Asymptotic_Notation
import CLRSLean.Probability.FiniteExpectation
import Mathlib

8.4. Bucket Sort

This file adds a deterministic correctness layer for bucket sort and a first finite-uniform probability interface for the expected-time argument.

The full probabilistic expected-time analysis in CLRS depends on a distributional assumption about the input. Here we isolate the pure correctness spine:

distribute values into buckets by a bucket-index function;
sort each bucket by the final key;
concatenate buckets in increasing bucket-index order;
prove the result is ordered and is a permutation of the input.

The theorem is intentionally parametric in the bucket-index function. A separate cross-bucket assumption states that every value in an earlier bucket is at most every value in a later bucket according to the final sort key.

The finite-uniform layer proves the collision fact behind the textbook expected time argument: two independently chosen uniform buckets collide with probability 1/m; therefore the expected quadratic bucket-occupancy cost for n independent samples into n buckets is at most linear in n. The final wrapper adds the linear scan/distribution term used by the CLRS expected-time proof and obtains a concrete ≤ 3n bound for this abstract cost expression.

Beyond the definitional layer, we also prove the CLRS second moment E[Σ_j n_j²] = n + n(n-1)/m as a true expectation over the explicit independent uniform input distribution Fin n → Fin m (each key hashed independently and uniformly to a bucket), reusing CLRS.Probability.expect_mul_of_indep for the independence step (expectedBucketQuadraticCost_eq_secondMoment). The textbook random variable is textbookBucketSortCost; its expectation is identified with the existing abstract expression by fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost and shown to be O(n) by expectedTextbookBucketSortCost_isBigO.

The execution layer uses CountingExecution.distribute to build stable indexed buckets in one input pass. BucketExecution.execute then runs counted insertion sort in each stored bucket and pushes its output elements. The public bucketSortByRank and bucketSortByRankWithCost both project that same execution. Work includes initialization, distribution, bucket visits, output pushes, comparisons, and insertion list-node construction under an indexed primitive model; it excludes persistent-array copying and scalar/key implementation costs.

bucketSortByRankWithCost_work_le bounds returned work by 2m + 6n + 2Σⱼ nⱼ², including the number of buckets m. The legacy bucketSortByRankCost remains the abstract occupancy budget n + Σⱼ nⱼ²; its existing expectation theorems retain that meaning. The companion ExpectedExecution module proves actual expected work at most 12n when m = n and bucket assignments are independently uniform. Final output correctness separately requires cross-bucket rank order.

              namespace CLRSnamespace Chapter08universe u vvariable {α : Type u}

Bucket-sort model

Every element in a list has bucket index strictly below upper.

def AllKeysLt (key : α → Nat) (xs : List α) (upper : Nat) : Prop :=
  ∀ x ∈ xs, key x < upper

Bucket sort with an abstract per-bucket sorter.

The buckets are scanned in increasing order 0, 1, ..., bucketCount - 1.

def bucketSortBy (bucketCount : Nat) (bucketOf : α → Nat)
    (sortBucket : List α → List α) (xs : List α) : List α :=
  (List.range bucketCount).flatMap fun k => sortBucket (bucket bucketOf xs k)

              theorem bucketSortBy_succ (bucketCount : Nat) (bucketOf : α → Nat)
    (sortBucket : List α → List α) (xs : List α) :
    bucketSortBy (bucketCount + 1) bucketOf sortBucket xs =
      bucketSortBy bucketCount bucketOf sortBucket xs ++
        sortBucket (bucket bucketOf xs bucketCount) := by
  simp [bucketSortBy, List.range_succ, List.flatMap_append]theorem orderedBy_of_pairwise {key : α → Nat} :
    ∀ {xs : List α}, xs.Pairwise (fun x y => key x ≤ key y) →
      OrderedBy key xs
  | [], _ => by
      trivial
  | [_], _ => by
      trivial
  | x :: y :: ys, h => by
      cases h with
      | cons hhead htail =>
          exact ⟨hhead y (by simp), orderedBy_of_pairwise htail⟩theorem flatMap_perm_of_forall {β : Type v} (ks : List β)
    (f g : β → List α)
    (h : ∀ k ∈ ks, (f k).Perm (g k)) :
    (ks.flatMap f).Perm (ks.flatMap g) := by
  induction ks with
  | nil =>
      simp
  | cons k ks ih =>
      simp at h ⊢
      exact List.Perm.append h.1 (ih h.2)theorem bucketSortBy_perm_bucket_scan (bucketCount : Nat)
    (bucketOf : α → Nat) (sortBucket : List α → List α) (xs : List α)
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys) :
    (bucketSortBy bucketCount bucketOf sortBucket xs).Perm
      ((List.range bucketCount).flatMap fun k => bucket bucketOf xs k) := by
  unfold bucketSortBy
  apply flatMap_perm_of_forall
  intro k _hk
  exact hsort_perm _

theorem bucketSortBy_allKeysLt (bucketCount : Nat) (bucketOf : α → Nat)
    (sortBucket : List α → List α) (xs : List α)
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys) :
    AllKeysLt bucketOf (bucketSortBy bucketCount bucketOf sortBucket xs)
      bucketCount := by
  intro x hx
  rw [bucketSortBy, List.mem_flatMap] at hx
  rcases hx with ⟨k, hk_range, hx_sort⟩
  have hx_bucket : x ∈ bucket bucketOf xs k :=
    (hsort_perm (bucket bucketOf xs k)).mem_iff.mp hx_sort
  have hxkey : bucketOf x = k := (mem_bucket_iff.mp hx_bucket).2
  exact hxkey ▸ List.mem_range.mp hk_range

theorem bucketSortBy_ordered (bucketCount : Nat)
    (bucketOf rank : α → Nat) (sortBucket : List α → List α) (xs : List α)
    (hsort_ordered :
      ∀ k, OrderedBy rank (sortBucket (bucket bucketOf xs k)))
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys)
    (hcross : ∀ {x y : α}, bucketOf x < bucketOf y → rank x ≤ rank y) :
    OrderedBy rank (bucketSortBy bucketCount bucketOf sortBucket xs) := by
  induction bucketCount with
  | zero =>
      simp [bucketSortBy, OrderedBy]
  | succ bucketCount ih =>
      rw [bucketSortBy_succ]
      refine orderedBy_append_of_rel ih (hsort_ordered bucketCount) ?_
      intro x hx y hy
      have hxlt :
          bucketOf x < bucketCount :=
        bucketSortBy_allKeysLt bucketCount bucketOf sortBucket xs hsort_perm x hx
      have hy_bucket : y ∈ bucket bucketOf xs bucketCount :=
        (hsort_perm (bucket bucketOf xs bucketCount)).mem_iff.mp hy
      have hykey : bucketOf y = bucketCount :=
        (mem_bucket_iff.mp hy_bucket).2
      exact hcross (by simpa [hykey] using hxlt)

theorem bucketSortBy_perm [DecidableEq α] (bucketCount : Nat)
    (bucketOf : α → Nat) (sortBucket : List α → List α) (xs : List α)
    (hxs : AllKeysLt bucketOf xs bucketCount)
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys) :
    (bucketSortBy bucketCount bucketOf sortBucket xs).Perm xs := by
  cases bucketCount with
  | zero =>
      have hnil : xs = [] := by
        apply List.eq_nil_iff_forall_not_mem.mpr
        intro x hx
        exact Nat.not_lt_zero _ (hxs x hx)
      simp [bucketSortBy, hnil]
  | succ maxKey =>
      have hscan :
          (bucketSortBy (maxKey + 1) bucketOf sortBucket xs).Perm
            (countingSortBy maxKey bucketOf xs) := by
        have hperm_scan :=
          bucketSortBy_perm_bucket_scan (maxKey + 1) bucketOf sortBucket xs
            hsort_perm
        simpa [countingSortBy, bucketSortBy] using hperm_scan
      have hle : AllKeysLe bucketOf xs maxKey := by
        intro x hx
        exact Nat.le_of_lt_succ (hxs x hx)
      exact hscan.trans (countingSortBy_perm maxKey bucketOf xs hle)theorem bucketSortBy_mem_iff [DecidableEq α] (bucketCount : Nat)
    (bucketOf : α → Nat) (sortBucket : List α → List α) (xs : List α)
    (hxs : AllKeysLt bucketOf xs bucketCount)
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys) (x : α) :
    x ∈ bucketSortBy bucketCount bucketOf sortBucket xs ↔ x ∈ xs :=
  (bucketSortBy_perm bucketCount bucketOf sortBucket xs hxs hsort_perm).mem_iff

Reader-facing correctness theorem for abstract deterministic bucket sort.

theorem bucketSortBy_correct [DecidableEq α] (bucketCount : Nat)
    (bucketOf rank : α → Nat) (sortBucket : List α → List α) (xs : List α)
    (hxs : AllKeysLt bucketOf xs bucketCount)
    (hsort_ordered :
      ∀ k, OrderedBy rank (sortBucket (bucket bucketOf xs k)))
    (hsort_perm : ∀ ys, (sortBucket ys).Perm ys)
    (hcross : ∀ {x y : α}, bucketOf x < bucketOf y → rank x ≤ rank y) :
    OrderedBy rank (bucketSortBy bucketCount bucketOf sortBucket xs) ∧
      (∀ x, x ∈ bucketSortBy bucketCount bucketOf sortBucket xs ↔ x ∈ xs) ∧
      (bucketSortBy bucketCount bucketOf sortBucket xs).Perm xs :=
  ⟨bucketSortBy_ordered bucketCount bucketOf rank sortBucket xs
      hsort_ordered hsort_perm hcross,
    bucketSortBy_mem_iff bucketCount bucketOf sortBucket xs hxs hsort_perm,
    bucketSortBy_perm bucketCount bucketOf sortBucket xs hxs hsort_perm⟩

Executable bucket sorter using merge sort inside each bucket

Sort one bucket by the final natural-number rank.

def sortBucketByRank (rank : α → Nat) (xs : List α) : List α :=
  (BucketExecution.insertionWithCost rank xs).value

theorem sortBucketByRank_perm (rank : α → Nat) (xs : List α) :
    (sortBucketByRank rank xs).Perm xs :=
  BucketExecution.insertionWithCost_perm rank xs

theorem sortBucketByRank_ordered (rank : α → Nat) (xs : List α) :
    OrderedBy rank (sortBucketByRank rank xs) :=
  orderedBy_of_pairwise (BucketExecution.insertionWithCost_pairwise rank xs)

Bucket sort using one indexed distribution followed by counted insertion sort.

def bucketSortByRank (bucketCount : Nat) (bucketOf rank : α → Nat)
    (xs : List α) : List α :=
  (BucketExecution.execute bucketCount bucketOf rank xs).output.toList

The indexed execution refines the stable bucket specification.

theorem bucketSortByRank_eq_spec (bucketCount : Nat) (bucketOf rank : α → Nat)
    (xs : List α) :
    bucketSortByRank bucketCount bucketOf rank xs =
      bucketSortBy bucketCount bucketOf (sortBucketByRank rank) xs :=
  BucketExecution.execute_value bucketCount bucketOf rank xs

Reader-facing correctness theorem for the executable bucket-sort model.

The cross-bucket hypothesis is the deterministic analogue of the CLRS bucket interval fact: every item in an earlier bucket is no larger than every item in a later bucket.


theorem bucketSortByRank_correct [DecidableEq α] (bucketCount : Nat)
    (bucketOf rank : α → Nat) (xs : List α)
    (hxs : AllKeysLt bucketOf xs bucketCount)
    (hcross : ∀ {x y : α}, bucketOf x < bucketOf y → rank x ≤ rank y) :
    OrderedBy rank (bucketSortByRank bucketCount bucketOf rank xs) ∧
      (∀ x, x ∈ bucketSortByRank bucketCount bucketOf rank xs ↔ x ∈ xs) ∧
      (bucketSortByRank bucketCount bucketOf rank xs).Perm xs := by
  rw [bucketSortByRank_eq_spec]
  exact bucketSortBy_correct bucketCount bucketOf rank (sortBucketByRank rank)
    xs hxs
    (fun k => sortBucketByRank_ordered rank (bucket bucketOf xs k))
    (sortBucketByRank_perm rank)
    hcross

Finite-uniform expected-cost interface

open CLRS.Probability

A real-valued 0/1 indicator for finite bucket probabilities. Alias for CLRS.Probability.indicator.

def probabilityIndicator (P : Prop) [Decidable P] : ℝ :=
  CLRS.Probability.indicator P

Uniform average over the finite bucket set Fin m.

noncomputable def uniformAverageFin {m : Nat} (X : Fin m → ℝ) : ℝ :=
  (∑ i : Fin m, X i) / (m : ℝ)

Uniform average over two independent finite bucket choices.

noncomputable def uniformAverageFin2 {m : Nat} (X : Fin m → Fin m → ℝ) : ℝ :=
  uniformAverageFin fun i => uniformAverageFin fun j => X i j

The finite-uniform bucket average is the shared CLRS.Probability.fintypeExpect toolkit specialised to Fin m. This bridge lets the algebraic lemmas below reuse the toolkit instead of re-deriving them.

theorem uniformAverageFin_eq_fintypeExpect {m : Nat} (X : Fin m → ℝ) :
    uniformAverageFin X = fintypeExpect X := by
  simp [uniformAverageFin, fintypeExpect, Fintype.card_fin]

A fixed bucket has probability 1/m under the finite-uniform bucket model.


theorem uniformAverageFin_indicator_singleton {m : Nat} (j : Fin m) :
    uniformAverageFin (fun i => probabilityIndicator (i = j)) = 1 / (m : ℝ) := by
  rw [uniformAverageFin_eq_fintypeExpect,
    show (fun i : Fin m => probabilityIndicator (i = j))
        = (fun i => CLRS.Probability.indicator (i = j)) from rfl,
    fintypeExpect_indicator_singleton, Fintype.card_fin]

Two independently chosen uniform buckets collide with probability 1/m. This is the probability fact used in the CLRS bucket-sort second-moment calculation.


theorem uniformAverageFin2_collision {m : Nat} (hm : 0 < m) :
    uniformAverageFin2 (fun i j : Fin m => probabilityIndicator (i = j)) =
      1 / (m : ℝ) := by
  classical
  have hden : (m : ℝ) ≠ 0 := by
    exact_mod_cast Nat.ne_of_gt hm
  have hinner :
      ∀ i : Fin m,
        uniformAverageFin (fun j : Fin m => probabilityIndicator (i = j)) =
          1 / (m : ℝ) := by
    intro i
    simpa [eq_comm] using uniformAverageFin_indicator_singleton (m := m) i
  calc
    uniformAverageFin2 (fun i j : Fin m => probabilityIndicator (i = j))
        = uniformAverageFin (fun _i : Fin m => 1 / (m : ℝ)) := by
          simp [uniformAverageFin2, hinner]
    _ = 1 / (m : ℝ) := by
          simp [uniformAverageFin, Finset.sum_const, Fintype.card_fin]
          field_simp [hden]

The textbook second-moment bucket-occupancy expression for n independent samples into m uniform buckets: E[Σ_i n_i^2] = n + n(n-1)/m.

noncomputable def expectedBucketQuadraticCost (m n : Nat) : ℝ :=
  (n : ℝ) + (n : ℝ) * ((n : ℝ) - 1) / (m : ℝ)

With as many buckets as input elements, the quadratic bucket-occupancy expectation is 2n - 1.


theorem expectedBucketQuadraticCost_self_eq (n : Nat) (hn : 0 < n) :
    expectedBucketQuadraticCost n n = 2 * (n : ℝ) - 1 := by
  have hden : (n : ℝ) ≠ 0 := by
    exact_mod_cast Nat.ne_of_gt hn
  unfold expectedBucketQuadraticCost
  field_simp [hden]
  ring

With n buckets for n elements, the expected quadratic bucket-occupancy cost is at most 2n.


theorem expectedBucketQuadraticCost_self_linear_bound (n : Nat) (hn : 0 < n) :
    expectedBucketQuadraticCost n n ≤ 2 * (n : ℝ) := by
  rw [expectedBucketQuadraticCost_self_eq n hn]
  linarith

Abstract CLRS bucket-sort expected cost: a linear scan/distribution term plus the expected quadratic bucket-occupancy cost for sorting the buckets.

noncomputable def expectedBucketSortCost (n : Nat) : ℝ :=
  (n : ℝ) + expectedBucketQuadraticCost n n

With n buckets for n elements, the abstract expected bucket-sort cost is 3n - 1.


theorem expectedBucketSortCost_self_eq (n : Nat) (hn : 0 < n) :
    expectedBucketSortCost n = 3 * (n : ℝ) - 1 := by
  unfold expectedBucketSortCost
  rw [expectedBucketQuadraticCost_self_eq n hn]
  ring

CLRS-facing linear expected-cost bound for the finite-uniform bucket-sort cost interface.


theorem expectedBucketSortCost_linear_bound (n : Nat) (hn : 0 < n) :
    expectedBucketSortCost n ≤ 3 * (n : ℝ) := by
  rw [expectedBucketSortCost_self_eq n hn]
  linarith

The abstract finite-uniform bucket-sort cost is O(n).


theorem expectedBucketSortCost_isBigO :
    CLRS.Chapter03.isBigO (fun n => expectedBucketSortCost n) (fun n => (n : ℝ)) := by
  rw [CLRS.Chapter03.isBigO_iff]
  refine ⟨3, by norm_num, 1, fun n hn => ?_⟩
  have hn' : 0 < n := hn
  have hle := expectedBucketSortCost_linear_bound n hn'
  have hnonneg : 0 ≤ expectedBucketSortCost n := by
    rw [expectedBucketSortCost_self_eq n hn']
    have : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn'
    linarith
  rw [abs_of_nonneg hnonneg, abs_of_nonneg (by positivity : (0 : ℝ) ≤ (n : ℝ))]
  linarith

The second moment as a true expectation over an independent input

The finite-uniform layer above is definitional. We now make the CLRS second-moment calculation a genuine expectation. The explicit independent uniform input distribution is Fin n → Fin m: each of the n keys is assigned a bucket in Fin m independently and uniformly. We prove E[Σ_j n_j²] = n + n(n-1)/m as CLRS.Probability.fintypeExpect over this distribution, reusing CLRS.Probability.expect_mul_of_indep for the independence step.

Split a bucket assignment a : Fin n → Fin m into the pair of buckets it sends two distinct keys i ≠ k to, together with the assignment of the remaining keys. This is the product decomposition witnessing that the two coordinates are independent of the rest.

open scoped Classical in

noncomputable def bucketPairSplit {m n : Nat} (i k : Fin n) (h : i ≠ k) :
    (Fin n → Fin m) ≃ (Fin m × Fin m) × ({x : Fin n // x ≠ i ∧ x ≠ k} → Fin m) where
  toFun a := ((a i, a k), fun x => a x.val)
  invFun q := fun x =>
    if hx : x = i then q.1.1
    else if hy : x = k then q.1.2
    else q.2 ⟨x, hx, hy⟩
  left_inv a := by
    funext x
    by_cases hx : x = i
    · subst hx; simp
    · by_cases hy : x = k
      · subst hy; simp [hx]
      · simp [hx, hy]
  right_inv q := by
    obtain ⟨⟨b, c⟩, rest⟩ := q
    simp only [Prod.mk.injEq]
    refine ⟨⟨?_, ?_⟩, ?_⟩
    · simp
    · simp [h.symm]
    · funext x
      obtain ⟨xv, hxi, hxk⟩ := x
      simp [hxi, hxk]

Marginalisation: the expectation of a function of two distinct coordinates of a uniform assignment equals the expectation over the two-bucket product space Fin m × Fin m (the joint law of two independent uniform keys).

open CLRS.Probability in


theorem fintypeExpect_bucketPair {m n : Nat} (i k : Fin n) (h : i ≠ k) (hm : 0 < m)
    (F : Fin m → Fin m → ℝ) :
    fintypeExpect (fun a : Fin n → Fin m => F (a i) (a k)) =
      fintypeExpect (fun p : Fin m × Fin m => F p.1 p.2) := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  have hcard : Fintype.card ({x : Fin n // x ≠ i ∧ x ≠ k} → Fin m) ≠ 0 :=
    Fintype.card_ne_zero
  have he := fintypeExpect_equiv (bucketPairSplit (m := m) i k h)
    (fun q : (Fin m × Fin m) × ({x : Fin n // x ≠ i ∧ x ≠ k} → Fin m) => F q.1.1 q.1.2)
  simp only [bucketPairSplit, Equiv.coe_fn_mk] at he
  rw [he]
  exact fintypeExpect_fst hcard (fun p : Fin m × Fin m => F p.1 p.2)

Two independent uniform keys collide with probability 1/m over the product sample space Fin m × Fin m.

open CLRS.Probability in


theorem collisionProb_pair {m : Nat} (hm : 0 < m) :
    fintypeExpect (fun p : Fin m × Fin m => indicator (p.1 = p.2)) = 1 / (m : ℝ) := by
  have hden : (m : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hm
  unfold fintypeExpect indicator
  rw [Fintype.card_prod, Fintype.card_fin]
  have hsum : (∑ p : Fin m × Fin m, (if p.1 = p.2 then (1 : ℝ) else 0)) = (m : ℝ) := by
    rw [Fintype.sum_prod_type]; simp
  rw [hsum]; push_cast; field_simp

The expected collision indicator for two keys i, k: 1 on the diagonal i = k, and 1/m off-diagonal (using independence).

open CLRS.Probability in


theorem expected_collision {m n : Nat} (i k : Fin n) (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => indicator (a i = a k)) =
      if i = k then 1 else 1 / (m : ℝ) := by
  by_cases h : i = k
  · subst h
    have hfun : (fun a : Fin n → Fin m => indicator (a i = a i)) = (fun _ => (1 : ℝ)) := by
      funext a; simp [indicator]
    rw [if_pos rfl, hfun]
    haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
    exact fintypeExpect_const Fintype.card_ne_zero 1
  · rw [if_neg h, fintypeExpect_bucketPair i k h hm (fun b c => indicator (b = c))]
    exact collisionProb_pair hm

Occupancy of bucket j: the number of keys assigned to it.

open CLRS.Probability in

noncomputable def bucketOccupancy {m n : Nat} (a : Fin n → Fin m) (j : Fin m) : ℝ :=
  ∑ i : Fin n, indicator (a i = j)

The bucket-occupancy second moment Σ_j n_j² for an assignment a.

open CLRS.Probability in

noncomputable def bucketSecondMoment {m n : Nat} (a : Fin n → Fin m) : ℝ :=
  ∑ j : Fin m, (bucketOccupancy a j) ^ 2

Per-bucket collision identity: ∑_j 1[a i = j]·1[a k = j] = 1[a i = a k].

open CLRS.Probability in


theorem collisionSum {m n : Nat} (a : Fin n → Fin m) (i k : Fin n) :
    ∑ j : Fin m, indicator (a i = j) * indicator (a k = j) = indicator (a i = a k) := by
  rw [Finset.sum_eq_single (a i)]
  · simp only [indicator]
    by_cases h : a i = a k
    · rw [if_pos h.symm, if_pos h, if_true, one_mul]
    · rw [if_neg (Ne.symm h), if_neg h, mul_zero]
  · intro j _ hj
    simp only [indicator]
    rw [if_neg (Ne.symm hj), zero_mul]
  · intro hcontra; exact absurd (Finset.mem_univ (a i)) hcontra

The second moment equals the double sum of pairwise collision indicators (CLRS: Σ_j n_j² = Σ_i Σ_k 1[a i = a k]).

open CLRS.Probability in


theorem bucketSecondMoment_eq_collisions {m n : Nat} (a : Fin n → Fin m) :
    bucketSecondMoment a = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) := by
  unfold bucketSecondMoment bucketOccupancy
  have step : ∀ j : Fin m, (∑ i : Fin n, indicator (a i = j)) ^ 2
      = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
    intro j; rw [sq, Finset.sum_mul_sum]
  simp_rw [step]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl (fun i _ => ?_)
  rw [Finset.sum_comm]
  exact Finset.sum_congr rfl (fun k _ => collisionSum a i k)

Bucket-sort second moment (true expectation). Over the explicit independent uniform input distribution Fin n → Fin m, the expected bucket-occupancy second moment is exactly n + n(n-1)/m, i.e. CLRS.Chapter08.expectedBucketQuadraticCost. This is CLRS's key second-moment computation (equation for E[Σ n_i²]) as a genuine expectation.

open CLRS.Probability in


theorem expectedBucketQuadraticCost_eq_secondMoment {m n : Nat} (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => bucketSecondMoment a) =
      expectedBucketQuadraticCost m n := by
  have hden : (m : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hm
  have h1 : (fun a : Fin n → Fin m => bucketSecondMoment a)
      = (fun a => ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k)) := by
    funext a; exact bucketSecondMoment_eq_collisions a
  rw [h1]
  simp only [fintypeExpect_sum]
  have h2 : ∀ i k : Fin n,
      fintypeExpect (fun a : Fin n → Fin m => indicator (a i = a k))
        = if i = k then (1 : ℝ) else 1 / (m : ℝ) := fun i k => expected_collision i k hm
  simp only [h2]
  have hinner : ∀ i : Fin n,
      (∑ k : Fin n, (if i = k then (1 : ℝ) else 1 / (m : ℝ)))
        = (n : ℝ) * (1 / (m : ℝ)) + (1 - 1 / (m : ℝ)) := by
    intro i
    have hsplit : ∀ k : Fin n, (if i = k then (1 : ℝ) else 1 / (m : ℝ))
        = 1 / (m : ℝ) + (if i = k then (1 - 1 / (m : ℝ)) else 0) := by
      intro k; by_cases h : i = k
      · rw [if_pos h, if_pos h]; ring
      · rw [if_neg h, if_neg h]; ring
    simp_rw [hsplit]
    rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_ite_eq]
    simp [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  simp only [hinner]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  unfold expectedBucketQuadraticCost
  field_simp
  ring

Textbook abstract bucket-sort cost

The CLRS unit-cost random variable charges n + Σ_j n_j² for an assignment of n keys to n buckets: n for the scan and distribution term, and the occupancy-square sum for the textbook per-bucket sorting bound. This is an abstract model over uniformly random bucket assignments. It does not instrument the current executable bucketSortByRank, whose implementation repeatedly filters the input to construct its buckets.

open Chapter03

The CLRS abstract unit-cost random variable n + Σ_j n_j².

noncomputable def textbookBucketSortCost (n : ℕ) (a : Fin n → Fin n) : ℝ :=
  (n : ℝ) + bucketSecondMoment a

The expectation of the textbook random variable is exactly the existing abstract expected-cost expression. The second-moment term is discharged by expectedBucketQuadraticCost_eq_secondMoment.


theorem fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost
    (n : ℕ) (hn : 0 < n) :
    fintypeExpect (textbookBucketSortCost n) = expectedBucketSortCost n := by
  classical
  unfold textbookBucketSortCost
  rw [fintypeExpect_add]
  have h_const : fintypeExpect (fun _ : Fin n → Fin n => (n : ℝ)) = (n : ℝ) := by
    simp [fintypeExpect]
  rw [h_const, expectedBucketQuadraticCost_eq_secondMoment hn]
  rfl

The CLRS abstract unit-cost random variable has linear expectation.


theorem expectedTextbookBucketSortCost_isBigO :
    isBigO (fun n : ℕ => fintypeExpect (textbookBucketSortCost n))
      (fun n : ℕ => (n : ℝ)) := by
  rw [isBigO_iff]
  refine ⟨3, by norm_num, 1, fun n hn => ?_⟩
  have hn_pos : 0 < n := by omega
  rw [fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost n hn_pos]
  have hle : expectedBucketSortCost n ≤ 3 * (n : ℝ) := expectedBucketSortCost_linear_bound n hn_pos
  have h_nonneg : 0 ≤ expectedBucketSortCost n := by
    rw [expectedBucketSortCost_self_eq n hn_pos]
    have : 1 ≤ (n : ℝ) := by exact_mod_cast hn_pos
    nlinarith
  rw [abs_of_nonneg h_nonneg, abs_of_nonneg (Nat.cast_nonneg _)]
  exact hle

Single-pass executable bucket builder

One step of the single-pass distribution: cons x onto the bucket indexed by bucketOf x, leaving every other bucket unchanged.

def distributeCons (bucketOf : α → Nat) (x : α) (acc : Array (List α)) : Array (List α) :=
  let b := bucketOf x
  if h : b < acc.size then acc.set b (x :: acc[b]) else acc

A distribution step does not change the number of buckets.

theorem distributeCons_size (bucketOf : α → Nat) (x : α) (acc : Array (List α)) :
    (distributeCons bucketOf x acc).size = acc.size := by
  unfold distributeCons
  by_cases h : bucketOf x < acc.size
  · simp [h, Array.size_set]
  · simp [h]

Auxiliary left-to-right bucket distribution. It conses each element onto its bucket and keeps reverse input order. The public sorter uses the shared stable CountingExecution.distribute instead, whose contents are proved equal to the stable bucket specification.

def distributeBuckets (bucketCount : Nat) (bucketOf : α → Nat) (xs : List α) :
    Array (List α) :=
  xs.foldl (fun acc x => distributeCons bucketOf x acc) (Array.replicate bucketCount [])

The single-pass distribution keeps one bucket per index 0..bucketCount-1.


theorem distributeBuckets_size (bucketCount : Nat) (bucketOf : α → Nat) (xs : List α) :
    (distributeBuckets bucketCount bucketOf xs).size = bucketCount := by
  unfold distributeBuckets
  have hmain : ∀ acc : Array (List α),
      (xs.foldl (fun acc x => distributeCons bucketOf x acc) acc).size = acc.size := by
    induction xs with
    | nil => intro acc; rfl
    | cons x xs ih =>
        intro acc
        rw [List.foldl_cons, ih (distributeCons bucketOf x acc)]
        exact distributeCons_size bucketOf x acc
  rw [hmain (Array.replicate bucketCount [])]
  simp [Array.size_replicate]

The stable input bucket bucket key xs k is exactly the filter by key x = k (the == on Nat coincides with equality).

theorem bucket_eq_filter_eq (key : α → Nat) (xs : List α) (k : Nat) :
    bucket key xs k = xs.filter (fun x => key x = k) := by
  unfold bucket
  simp only [Bool.beq_eq_decide_eq]

Costed per-bucket sorter

Execute insertion sort and expose its accumulated work.

def sortBucketByRankWithCost (rank : α → Nat) (xs : List α) : List α × Nat :=
  let run := BucketExecution.insertionWithCost rank xs
  (run.value, run.work)

Erasing per-bucket work recovers the public insertion sorter.

theorem sortBucketByRankWithCost_result (rank : α → Nat) (xs : List α) :
    (sortBucketByRankWithCost rank xs).1 = sortBucketByRank rank xs := rfl

The actual data-dependent work is bounded by twice the squared bucket length.

theorem sortBucketByRankWithCost_cost (rank : α → Nat) (xs : List α) :
    (sortBucketByRankWithCost rank xs).2 ≤ 2 * xs.length ^ 2 :=
  BucketExecution.insertionWithCost_work_le_sq rank xs

Occupancy budget and actual bucket execution

Abstract occupancy budget, retained for the finite-expectation interface. It excludes bucket-count overhead and is not the actual returned work.

def bucketSortByRankCost (bucketCount : Nat) (bucketOf : α → Nat) (xs : List α) : Nat :=
  xs.length + ∑ j : Fin bucketCount, ((bucket bucketOf xs (j : Nat)).length) ^ 2

Return the output and the work of the same indexed bucket execution.

def bucketSortByRankWithCost (bucketCount : Nat) (bucketOf rank : α → Nat) (xs : List α) :
    List α × Nat :=
  let run := BucketExecution.execute bucketCount bucketOf rank xs
  (run.output.toList, run.work)

theorem bucketSortByRankWithCost_result (bucketCount : Nat) (bucketOf rank : α → Nat)
    (xs : List α) :
    (bucketSortByRankWithCost bucketCount bucketOf rank xs).1 =
      bucketSortByRank bucketCount bucketOf rank xs := rfl

The returned work includes bucket-count overhead as well as the occupancy budget.


theorem bucketSortByRankWithCost_work_le [DecidableEq α] (bucketCount : Nat)
    (bucketOf rank : α → Nat) (xs : List α) (hkeys : AllKeysLt bucketOf xs bucketCount) :
    (bucketSortByRankWithCost bucketCount bucketOf rank xs).2 ≤
      2 * bucketCount + 4 * xs.length + 2 * bucketSortByRankCost bucketCount bucketOf xs := by
  have h := BucketExecution.execute_work_le bucketCount bucketOf rank xs
  have hperm := bucketSortBy_perm bucketCount bucketOf id xs hkeys
    (fun b => List.Perm.refl b)
  have hlen : ((List.range bucketCount).map (bucket bucketOf xs)).flatten.length = xs.length := by
    simpa [bucketSortBy, List.flatMap] using hperm.length_eq
  have hsum : ((List.range bucketCount).map
      (fun k => (bucket bucketOf xs k).length ^ 2)).sum =
      ∑ j : Fin bucketCount, (bucket bucketOf xs (j : Nat)).length ^ 2 := by
    rw [Fin.sum_univ_eq_sum_range (fun k => (bucket bucketOf xs k).length ^ 2)]
    clear hkeys h hperm hlen
    induction bucketCount with
    | zero => simp
    | succ m ih => simp [List.range_succ, Finset.sum_range_succ, ih]
  rw [hlen, hsum] at h
  change (BucketExecution.execute bucketCount bucketOf rank xs).work ≤ _
  unfold bucketSortByRankCost
  omega

Refinement to the abstract expected-cost model

Filtering the canonical enumeration of Fin n by a decidable predicate counts the elements of the subtype.


theorem finRange_filter_length_eq_card {n : Nat} (p : Fin n → Prop) [DecidablePred p] :
    ((List.finRange n).filter (fun i => decide (p i))).length =
      Nat.card {i : Fin n // p i} := by
  classical
  let l : List (Fin n) := (List.finRange n).filter (fun i => decide (p i))
  have hnodup : l.Nodup := List.Nodup.filter (fun i => decide (p i)) (List.nodup_finRange n)
  have hdedup : l.dedup = l := (List.dedup_eq_self).mpr hnodup
  have hcard : l.toFinset.card = l.length := by
    rw [List.card_toFinset, hdedup]
  rw [← hcard]
  have htofinset : l.toFinset = Finset.univ.filter (fun i : Fin n => p i) := by
    ext i
    simp [l, List.toFinset_filter, List.toFinset_finRange, Finset.mem_filter]
  rw [htofinset]
  rw [Nat.card_eq_fintype_card]
  rw [Fintype.card_subtype p]

The bucket length for an assignment enumerated as List.finRange n is the cardinality of the keys mapped to j.


theorem bucket_length_eq_card (a : Fin n → Fin m) (j : Fin m) :
    (bucket (fun i : Fin n => (a i : Nat)) (List.finRange n) (j : Nat)).length =
      Nat.card {i : Fin n // a i = j} := by
  rw [bucket_eq_filter_eq]
  -- (List.finRange n).filter (fun i => (a i : Nat) = (j : Nat))
  have hfilter :
      (List.finRange n).filter (fun i : Fin n => (a i : Nat) = (j : Nat)) =
        (List.finRange n).filter (fun i => decide (a i = j)) := by
    congr
    funext i
    simp [Fin.val_inj]
  rw [hfilter]
  exact finRange_filter_length_eq_card (fun i : Fin n => a i = j)

The abstract real-valued occupancy of bucket j is the cardinality of the keys mapped to j.


theorem bucketOccupancy_eq_card (a : Fin n → Fin m) (j : Fin m) :
    bucketOccupancy a j = (Nat.card {i : Fin n // a i = j} : ℝ) := by
  classical
  unfold bucketOccupancy
  simp only [CLRS.Probability.indicator]
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, Finset.card_filter]
  norm_cast

Bucket-sort cost refinement. The cost of the executable bucket sort over the canonical enumeration of n keys, read as a real, equals the textbook unit-cost random variable n + Σⱼ nⱼ².


theorem bucketSortByRankCost_eq_textbookBucketSortCost (a : Fin n → Fin n) :
    (bucketSortByRankCost n (fun i : Fin n => (a i : Nat)) (List.finRange n) : ℝ) =
      textbookBucketSortCost n a := by
  unfold bucketSortByRankCost textbookBucketSortCost bucketSecondMoment
  rw [List.length_finRange]
  push_cast
  congr 1
  refine Finset.sum_congr rfl ?_
  intro j _hj
  have hlen := bucket_length_eq_card a j
  have hocc := bucketOccupancy_eq_card a j
  rw [hlen, hocc]

Pointwise-equal random variables have equal finite expectation.

theorem fintypeExpect_congr {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X Y : Ω → ℝ)
    (h : ∀ ω, X ω = Y ω) :
    CLRS.Probability.fintypeExpect X = CLRS.Probability.fintypeExpect Y := by
  unfold CLRS.Probability.fintypeExpect
  congr 1
  exact Finset.sum_congr rfl (fun ω _ => h ω)

The expectation of the abstract occupancy budget over the independent uniform input model is exactly expectedBucketSortCost n.


theorem fintypeExpect_bucketSortByRankCost_eq_expectedBucketSortCost (n : Nat) (hn : 0 < n) :
    CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
      (bucketSortByRankCost n (fun i : Fin n => (a i : Nat)) (List.finRange n) : ℝ)) =
      expectedBucketSortCost n := by
  have hcongr : CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
      (bucketSortByRankCost n (fun i : Fin n => (a i : Nat)) (List.finRange n) : ℝ)) =
      CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n => textbookBucketSortCost n a) :=
    fintypeExpect_congr _ _ (fun a => bucketSortByRankCost_eq_textbookBucketSortCost a)
  rw [hcongr]
  exact fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost n hn

The abstract occupancy budget has linear expectation (O(n)).


theorem expectedBucketSortByRankCost_isBigO :
    Chapter03.isBigO (fun n : Nat =>
      CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
        (bucketSortByRankCost n (fun i : Fin n => (a i : Nat)) (List.finRange n) : ℝ)))
      (fun n : Nat => (n : ℝ)) := by
  rw [Chapter03.isBigO_iff]
  refine ⟨3, by norm_num, 1, fun n hn => ?_⟩
  have hn_pos : 0 < n := by omega
  rw [fintypeExpect_bucketSortByRankCost_eq_expectedBucketSortCost n hn_pos]
  have hle : expectedBucketSortCost n ≤ 3 * (n : ℝ) :=
    expectedBucketSortCost_linear_bound n hn_pos
  have h_nonneg : 0 ≤ expectedBucketSortCost n := by
    rw [expectedBucketSortCost_self_eq n hn_pos]
    have : 1 ≤ (n : ℝ) := by exact_mod_cast hn_pos
    nlinarith
  rw [abs_of_nonneg h_nonneg, abs_of_nonneg (Nat.cast_nonneg _)]
  exact hle

end Chapter08end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort.Execution

Single-distribution bucket sorting with insertion work

The shared indexed distributor traverses the input once, keeping each bucket in input order. This controller visits each stored bucket, executes counted insertion sort, and pushes its output elements. Initialization, input key/index operations, bucket visits, output writes, and insertion work all contribute to the returned counter. Indexed operations use the declared unit-cost model; allocation internals, persistent-array copying, array/list view conversion, and key-function internals are excluded.

              namespace CLRS.Chapter08.BucketExecutionstructure Emission (α : Type*) where
  output : Array α
  bucketVisits : Nat
  outputWrites : Nat
  sortingWork : Natdef sortEmit (rank : α → Nat) : List (List α) → Array α → Emission α
  | [], out => ⟨out, 0, 0, 0⟩
  | b :: bs, out =>
      let sorted := insertionWithCost rank b
      let pushed := CountingExecution.pushList sorted.value out
      let rest := sortEmit rank bs pushed.value
      ⟨rest.output, rest.bucketVisits + 1, pushed.writes + rest.outputWrites,
        sorted.work + rest.sortingWork⟩theorem sortEmit_value (rank : α → Nat) (bs : List (List α)) (out : Array α) :
    (sortEmit rank bs out).output.toList =
      out.toList ++ bs.flatMap (fun b => (insertionWithCost rank b).value) := by
  induction bs generalizing out with
  | nil => simp [sortEmit]
  | cons b bs ih => simp [sortEmit, ih, List.append_assoc]theorem sortEmit_visits (rank : α → Nat) (bs : List (List α)) (out : Array α) :
    (sortEmit rank bs out).bucketVisits = bs.length := by
  induction bs generalizing out with
  | nil => rfl
  | cons b bs ih => simp [sortEmit, ih]theorem sortEmit_writes (rank : α → Nat) (bs : List (List α)) (out : Array α) :
    (sortEmit rank bs out).outputWrites = bs.flatten.length := by
  induction bs generalizing out with
  | nil => rfl
  | cons b bs ih => simp [sortEmit, ih, insertionWithCost_length]theorem sortEmit_work_le (rank : α → Nat) (bs : List (List α)) (out : Array α) :
    (sortEmit rank bs out).sortingWork ≤ 2 * (bs.map (fun b => b.length ^ 2)).sum := by
  induction bs generalizing out with
  | nil => simp [sortEmit]
  | cons b bs ih =>
      simp only [sortEmit, List.map_cons, List.sum_cons]
      have hrest := ih (CountingExecution.pushList (insertionWithCost rank b).value out).value
      have hb := insertionWithCost_work_le_sq rank b
      omegastructure Result (α : Type*) where
  output : Array α
  work : Nat

The public bucket execution calls the distributor and both counted output loops.

def execute (bucketCount : Nat) (bucketOf rank : α → Nat) (xs : List α) : Result α :=
  let initial := CountingExecution.initializeBuckets (α := α) bucketCount
  let distributed := CountingExecution.distribute bucketOf xs initial.1
  let emitted := sortEmit rank distributed.buckets.toList #[]
  ⟨emitted.output, initial.2 + 2 * distributed.inputs + 3 * distributed.updates +
    emitted.bucketVisits + emitted.outputWrites + emitted.sortingWork⟩

theorem execute_value (bucketCount : Nat) (bucketOf rank : α → Nat) (xs : List α) :
    (execute bucketCount bucketOf rank xs).output.toList =
      (List.range bucketCount).flatMap
        (fun k => (insertionWithCost rank (bucket bucketOf xs k)).value) := by
  simp [execute, sortEmit_value, CountingExecution.distribute_toList, List.flatMap_map]

The bound includes the number of buckets even when the input is empty.

theorem execute_work_le (bucketCount : Nat) (bucketOf rank : α → Nat) (xs : List α) :
    (execute bucketCount bucketOf rank xs).work ≤
      2 * bucketCount + 5 * xs.length +
        ((List.range bucketCount).map (bucket bucketOf xs)).flatten.length +
        2 * ((List.range bucketCount).map
          (fun k => (bucket bucketOf xs k).length ^ 2)).sum := by
  let bs := (List.range bucketCount).map (bucket bucketOf xs)
  have hs := sortEmit_work_le rank bs #[]
  have hu := CountingExecution.distribute_updates_le bucketOf xs
    (Array.replicate bucketCount [])
  simp only [execute, CountingExecution.initializeBuckets_array,
    CountingExecution.initializeBuckets_visits, CountingExecution.distribute_inputs,
    CountingExecution.distribute_toList, sortEmit_visits, sortEmit_writes, List.length_map,
    List.length_range]
  simpa only [bs, List.map_map, Function.comp_def] using (by omega :
    bucketCount + 2 * xs.length +
      3 * (CountingExecution.distribute bucketOf xs (Array.replicate bucketCount [])).updates +
      bucketCount + bs.flatten.length + (sortEmit rank bs #[]).sortingWork ≤
      2 * bucketCount + 5 * xs.length + bs.flatten.length +
      2 * (bs.map (fun b => b.length ^ 2)).sum)

end CLRS.Chapter08.BucketExecution

CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort.ExpectedExecution

Expected work of the indexed bucket execution

The random assignment gives independent uniform bucket indices. Final ranks may depend arbitrarily on the assignment: the insertion work bound holds for every order within each bucket. The expected-work theorem is separate from output sortedness, which additionally requires the cross-bucket rank condition.

namespace CLRS.Chapter08

The actual run is bounded by a linear term and twice the occupancy budget.


theorem bucketExecutionWork_le_budget (a : Fin n → Fin n) (rank : Fin n → Nat) :
    ((bucketSortByRankWithCost n (fun i => (a i : Nat)) rank (List.finRange n)).2 : ℝ) ≤
      6 * (n : ℝ) + 2 * textbookBucketSortCost n a := by
  have h := bucketSortByRankWithCost_work_le n (fun i : Fin n => (a i : Nat)) rank
    (List.finRange n) (fun i _ => (a i).isLt)
  rw [List.length_finRange] at h
  have hc : ((bucketSortByRankWithCost n (fun i => (a i : Nat)) rank
      (List.finRange n)).2 : ℝ) ≤ 2 * (n : ℝ) + 4 * n +
      2 * (bucketSortByRankCost n (fun i => (a i : Nat)) (List.finRange n) : ℝ) := by
    exact_mod_cast h
  rw [bucketSortByRankCost_eq_textbookBucketSortCost] at hc
  linarith

At most twelve work units per input element in expectation under uniform buckets.


theorem expectedBucketExecutionWork_le (n : Nat) (hn : 0 < n)
    (rank : (Fin n → Fin n) → Fin n → Nat) :
    CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
      ((bucketSortByRankWithCost n (fun i => (a i : Nat)) (rank a)
        (List.finRange n)).2 : ℝ)) ≤ 12 * (n : ℝ) := by
  classical
  letI : Nonempty (Fin n → Fin n) := ⟨id⟩
  have hm : CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
      ((bucketSortByRankWithCost n (fun i => (a i : Nat)) (rank a)
        (List.finRange n)).2 : ℝ)) ≤
      CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
        6 * (n : ℝ) + 2 * textbookBucketSortCost n a) := by
    unfold CLRS.Probability.fintypeExpect
    apply div_le_div_of_nonneg_right _ (by positivity)
    exact Finset.sum_le_sum (fun a _ => bucketExecutionWork_le_budget a (rank a))
  have hlin : CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
      6 * (n : ℝ) + 2 * textbookBucketSortCost n a) =
      6 * (n : ℝ) + 2 * expectedBucketSortCost n := by
    rw [CLRS.Probability.fintypeExpect_add]
    rw [CLRS.Probability.fintypeExpect_const (by exact Fintype.card_ne_zero)]
    have hmul : CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
        2 * textbookBucketSortCost n a) =
        2 * CLRS.Probability.fintypeExpect (textbookBucketSortCost n) := by
      simp only [CLRS.Probability.fintypeExpect, ← Finset.mul_sum, mul_div_assoc]
    rw [hmul, fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost n hn]
  rw [hlin] at hm
  have hbudget := expectedBucketSortCost_linear_bound n hn
  linarith

Uniform bucket assignments give linear expected work for the actual execution.


theorem expectedBucketExecutionWork_isBigO
    (rank : ∀ n, (Fin n → Fin n) → Fin n → Nat) :
    Chapter03.isBigO (fun n : Nat =>
      CLRS.Probability.fintypeExpect (fun a : Fin n → Fin n =>
        ((bucketSortByRankWithCost n (fun i => (a i : Nat)) (rank n a)
          (List.finRange n)).2 : ℝ))) (fun n : Nat => (n : ℝ)) := by
  rw [Chapter03.isBigO_iff]
  refine ⟨12, by norm_num, 1, ?_⟩
  intro n hn
  rw [abs_of_nonneg (CLRS.Probability.fintypeExpect_nonneg (by intro a; positivity)),
    abs_of_nonneg (Nat.cast_nonneg n)]
  exact expectedBucketExecutionWork_le n (by omega) (rank n)

end CLRS.Chapter08

CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort.InsertionExecution

Instrumented insertion sorting within a bucket

The same recursive execution constructs the output and records controller work. One unit pays for each rank comparison and each newly constructed list node; each outer sorting iteration pays one additional controller unit. Existing suffixes may be shared. Rank evaluation and list allocation use unit costs; this is not a bit-level or allocator runtime model.

The public results identify the value with generic insertion sort and prove permutation, ordering, and the quadratic bound needed by bucket sort.

              namespace CLRS.Chapter08.BucketExecutionuniverse uvariable {α : Type u}

One list result and the work accumulated while constructing that result.

structure InsertionExecution (α : Type u) where
  value : List α
  work : Nat
  deriving Repr, DecidableEq

Insert one value into a sorted bucket. The empty branch constructs one node; the early-stop branch compares ranks and constructs two nodes; a recursive branch compares ranks and constructs one node after its recursive call.

def insertWithCost (rank : α → Nat) (x : α) : List α → InsertionExecution α
  | [] => ⟨[x], 1⟩
  | y :: ys =>
      if rank x ≤ rank y then
        ⟨x :: y :: ys, 3⟩
      else
        let rest := insertWithCost rank x ys
        ⟨y :: rest.value, rest.work + 2⟩

Sort a bucket by recursively sorting its tail and inserting its head. Each nonempty outer iteration contributes one controller unit in addition to the insertion work.

def insertionWithCost (rank : α → Nat) : List α → InsertionExecution α
  | [] => ⟨[], 0⟩
  | x :: xs =>
      let tail := insertionWithCost rank xs
      let inserted := insertWithCost rank x tail.value
      ⟨inserted.value, tail.work + inserted.work + 1⟩

Erasing insertion work gives the verified generic ordered insertion.

theorem insertWithCost_value (rank : α → Nat) (x : α) (xs : List α) :
    (insertWithCost rank x xs).value =
      List.orderedInsert (fun x y => rank x ≤ rank y) x xs := by
  induction xs with
  | nil => rfl
  | cons y ys ih =>
      simp only [insertWithCost, List.orderedInsert_cons]
      split <;> simp_all

Erasing the accumulated work gives generic insertion sort.

theorem insertionWithCost_value (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).value =
      List.insertionSort (fun x y => rank x ≤ rank y) xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      simp only [insertionWithCost, List.insertionSort_cons, insertWithCost_value, ih]

The executed sorter preserves every payload, including duplicate ranks.


theorem insertionWithCost_perm (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).value.Perm xs := by
  rw [insertionWithCost_value]
  exact List.perm_insertionSort _ _

The execution returns a list ordered by its final rank.


theorem insertionWithCost_pairwise (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).value.Pairwise (fun x y => rank x ≤ rank y) := by
  rw [insertionWithCost_value]
  exact List.pairwise_insertionSort _ _

The executed output has the same length as the input bucket.

theorem insertionWithCost_length (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).value.length = xs.length :=
  (insertionWithCost_perm rank xs).length_eq

Insertion visits at most the existing bucket length, constructing at most one replacement node per recursive visit and its new final node.

theorem insertWithCost_work_le (rank : α → Nat) (x : α) (xs : List α) :
    (insertWithCost rank x xs).work ≤ 2 * xs.length + 1 := by
  induction xs with
  | nil => simp [insertWithCost]
  | cons y ys ih =>
      simp only [insertWithCost, List.length_cons]
      split <;> simp_all
      omega

The actual insertion execution uses at most n(n+1) work.


theorem insertionWithCost_work_le (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).work ≤ xs.length * (xs.length + 1) := by
  induction xs with
  | nil => simp [insertionWithCost]
  | cons x xs ih =>
      have hi := insertWithCost_work_le rank x (insertionWithCost rank xs).value
      rw [insertionWithCost_length] at hi
      simp only [insertionWithCost, List.length_cons]
      nlinarith

A uniform quadratic bound, including an empty bucket with zero work.


theorem insertionWithCost_work_le_sq (rank : α → Nat) (xs : List α) :
    (insertionWithCost rank xs).work ≤ 2 * xs.length ^ 2 := by
  have h := insertionWithCost_work_le rank xs
  have hn : xs.length ≤ xs.length ^ 2 := by
    cases xs.length with
    | zero => norm_num
    | succ n => nlinarith
  nlinarith

end CLRS.Chapter08.BucketExecution

CLRSLean.Probability.FiniteExpectation

Generic Fintype wrapper.

noncomputable def fintypeExpect {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℝ) : ℝ :=
  (∑ ω : Ω, X ω) / (Fintype.card Ω : ℝ)

Product expectation under independence.

If X depends only on the first coordinate and Y only on the second of a product sample space Ω₁ × Ω₂, then the expectation of the product factors as the product of the expectations. This is the finite-uniform form of E[XY] = E[X] · E[Y] for independent X, Y (CLRS Appendix C, equation (C.24)), and is the missing primitive for the bucket-sort second moment and the SUHA chained-hash analysis.


theorem expect_mul_of_indep {Ω₁ Ω₂ : Type} [Fintype Ω₁] [Fintype Ω₂]
    [DecidableEq Ω₁] [DecidableEq Ω₂] (X : Ω₁ → ℝ) (Y : Ω₂ → ℝ) :
    fintypeExpect (fun p : Ω₁ × Ω₂ => X p.1 * Y p.2) =
      fintypeExpect X * fintypeExpect Y := by
  unfold fintypeExpect
  have hnum : (∑ p : Ω₁ × Ω₂, X p.1 * Y p.2) =
      (∑ a : Ω₁, X a) * (∑ b : Ω₂, Y b) := by
    rw [Finset.sum_mul_sum, Fintype.sum_prod_type]
  rw [hnum, Fintype.card_prod]
  push_cast
  rw [div_mul_div_comm]

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_08.Section_08_1_Lower_Bound_For_Sorting
import CLRSLean.FourthEdition.Chapter_08.Section_08_1_Lower_Bound_For_Sorting.Execution
import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort
import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.CountTables
import CLRSLean.FourthEdition.Chapter_08.Section_08_2_Counting_Sort.MutableOutputArray
import CLRSLean.FourthEdition.Chapter_08.Section_08_3_Radix_Sort
import CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort
import CLRSLean.FourthEdition.Chapter_08.Section_08_4_Bucket_Sort.ExpectedExecution

Current source

Sections 8.1--8.4 are native fourth-edition sections (lower bounds for sorting, counting sort, radix sort, and bucket sort), imported directly from Section 8.1, Section 8.2, Section 8.3, and Section 8.4. Section 8.2 includes the nested count-table and mutable output-array refinements. Declarations retain the CLRS.Chapter08 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_08 and CLRSLean.Chapter_08.Section_08_* forward to these sources.

Coverage boundary

The comparison-tree interpreter returns its actual leaf and comparison count; comparisonSort_exists_run_lowerBound gives a reachable input witness. Counting sort uses one indexed stable-bucket distribution and one output traversal. Its output refines the original stable filter specification, including out-of-range omissions, and radix passes consume that same execution. This is an indexed stable-bucket implementation, not the literal cumulative-counter decrement program; the old count-table and scatter developments remain specification helpers.

The public bucket sorter shares the stable distributor, executes counted insertion sort, and emits the sorted buckets. Its actual work is bounded by 2m + 6n + 2Σ n_j²; with m = n independent uniform bucket choices, expectedBucketExecutionWork_isBigO proves linear expected work. Output sortedness additionally assumes the cross-bucket rank condition. The legacy bucketSortByRankCost denotes the abstract occupancy budget.

All these ledgers count declared controller/indexed primitives. Persistent-array copying, array/list view conversion, allocation internals, and key-function implementation costs are outside the model.

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 8 of 35

8.1. Lower Bounds for Sorting

Main results

Current gaps

Comparison decision trees

Factorial growth

The lower bound

Definitions and proofs

A comparison lower bound attained by a reachable run

8.2. Counting Sort

Implementation details

Ordered lists by key

Stable buckets

Counting sort by stable buckets

Definitions and proofs

CLRS Section 8.2 - Counting sort count-table refinement

Count table certificates

Cumulative-count boundaries

Table-driven wrapper

Reverse-scan bucket refinement

Cumulative segment counts

Counting sort through one stable indexed distribution

CLRS Section 8.2 - Stable indexed-bucket output-array refinement

The mutable output array

Refinement of the stable bucket specification

Cumulative-count fill offsets

Linear work bound

8.3. Radix Sort

Relation-ordered lists and digit lexicographic order

One stable radix pass

Radix sort

Stability by complete digit signatures

Concrete base-b digit extraction

Running-time / cost layer

8.4. Bucket Sort

Bucket-sort model

Executable bucket sorter using merge sort inside each bucket

Finite-uniform expected-cost interface

The second moment as a true expectation over an independent input

Textbook abstract bucket-sort cost

Single-pass executable bucket builder

Costed per-bucket sorter

Occupancy budget and actual bucket execution

Refinement to the abstract expected-cost model

Definitions and proofs

Single-distribution bucket sorting with insertion work

Expected work of the indexed bucket execution

Instrumented insertion sorting within a bucket

Scope and implementation notes

Current source

Coverage boundary