Counting sort

DefinitionCounting sort#✓fully proved

Let \(k\) be a natural number and let \(\mathrm{key}\) assign to each record a key in \(\{0, \dots, k-1\}\). Counting sort of an array \(A\) of records returns an array together with a count of charged operations. It starts \(k\) counters at zero, counts the records of \(A\) with each key, replaces the counters by cumulative counts so that the counter of key \(q\) holds the number of records with key at most \(q\), and then scans \(A\) from right to left: for each record it decrements the counter of the record's key and writes the record at the resulting position of the output, which starts as a copy of \(A\). One operation is charged for each counter initialization, key evaluation, counter read, counter write and output write.

Cslib.Algorithms.Lean.TimeM.countingSort · 55 lines

def countingSort {α : Type u} {k : Nat} (key : α → Fin k)
    (input : Array α) : TimeM Nat (Array α) :=
  let rec initCounters : (n : Nat) → TimeM Nat {a : Array Nat // a.size = n}
    | 0 => pure ⟨#[], rfl⟩
    | n + 1 => do
        let counters ← initCounters n
        ✓
        return ⟨counters.val.push 0, by simp [counters.property]⟩
  let rec countKeys :
      List α → {a : Array Nat // a.size = k} → TimeM Nat {a : Array Nat // a.size = k}
    | [], counters => pure counters
    | x :: xs, counters => do
        ✓
        let q := key x
        let hq : q.val < counters.val.size := counters.property.symm ▸ q.isLt
        ✓
        let count := counters.val[q.val]'hq
        ✓
        let next := counters.val.set q.val (count + 1) hq
        countKeys xs ⟨next, by simp [next, counters.property]⟩
  let rec cumulativeCounts :
      (remaining start : Nat) → start + remaining = k →
        {a : Array Nat // a.size = k} → Nat → TimeM Nat {a : Array Nat // a.size = k}
    | 0, _, _, counters, _ => pure counters
    | remaining + 1, start, hsize, counters, total => do
        let q : Fin k := ⟨start, by omega⟩
        let hq : q.val < counters.val.size := counters.property.symm ▸ q.isLt
        ✓
        let nextTotal := total + counters.val[q.val]'hq
        ✓
        let next := counters.val.set q.val nextTotal hq
        cumulativeCounts remaining (start + 1) (by omega)
          ⟨next, by simp [next, counters.property]⟩ nextTotal
  let rec placeRecords :
      List α → ({a : Array Nat // a.size = k} × Array α) →
        TimeM Nat ({a : Array Nat // a.size = k} × Array α)
    | [], state => pure state
    | x :: xs, state => do
        let state ← placeRecords xs state
        ✓
        let q := key x
        let hq : q.val < state.1.val.size := state.1.property.symm ▸ q.isLt
        ✓
        let ending := state.1.val[q.val]'hq
        ✓
        let position := ending - 1
        let nextCounters := state.1.val.set q.val position hq
        ✓
        return (⟨nextCounters, by simp [nextCounters, state.1.property]⟩,
          state.2.setIfInBounds position x)
  let initialized := initCounters k
  let counted := countKeys input.toList initialized.ret
  let cumulative := cumulativeCounts k 0 (by omega) counted.ret 0
  let placed := placeRecords input.toList (cumulative.ret, input)
  ⟨placed.ret.2, initialized.time + counted.time + cumulative.time + placed.time⟩

Used by 5

Used byCorrectness of counting sort · Running time of counting sort · Radix sort · Correctness of radix sort · Cost bound for radix sort

TheoremCorrectness of counting sort#✓fully proved

Let \(k\) be a natural number, let \(\mathrm{key}\) assign to each record a key in \(\{0, \dots, k-1\}\), and let \(A\) be an array of records. The array that counting sort returns on \(A\) lists its records in nondecreasing order of key, is a permutation of \(A\), and is stable: for every key \(q < k\), the records of the output with key \(q\), read from left to right, form the same sequence as the records of \(A\) with key \(q\).

theorem countingSort_correct {α : Type u} {k : Nat} (key : α → Fin k)
    (input : Array α) :
    List.Pairwise (fun x y => key x ≤ key y) (countingSort key input).ret.toList ∧
      List.Perm (countingSort key input).ret.toList input.toList ∧
      ∀ q : Fin k,
        (countingSort key input).ret.toList.filter (fun x => key x == q) =
          input.toList.filter fun x => key x == q

Uses 1 · Used by 2

Statement usesCounting sort

Used byCorrectness of radix sort · Cost bound for radix sort

TheoremRunning time of counting sort#✓fully proved

Let \(k\) be a natural number, let \(\mathrm{key}\) assign to each record a key in \(\{0, \dots, k-1\}\), and let \(A\) be an array of \(n\) records. Counting sort on \(A\) with this key is charged at most \(7n + 3k\) operations, where one operation is charged for each counter initialization, key evaluation, counter read, counter write and output write.

theorem countingSort_time {α : Type u} {k : Nat} (key : α → Fin k)
    (input : Array α) :
    (countingSort key input).time ≤ 7 * input.size + 3 * k

Uses 1 · Used by 1

Statement usesCounting sort

Used byCost bound for radix sort

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.