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