Selection sort

DefinitionMinimum extraction#✓fully proved

Given an initial candidate \(c\) in a linearly ordered type and a list \(L\), minimum extraction returns a pair \((m, r)\) together with a cost. If \(L\) is empty, it returns \(c\) with the empty list at cost \(0\). If \(L\) has head \(x\) and tail \(L'\), it compares \(x\) with \(c\) at cost one: if \(x < c\), it extracts from \(L'\) with candidate \(x\), obtaining \((m, r)\), and returns \(m\) with the list \(c\) followed by \(r\); otherwise it extracts from \(L'\) with candidate \(c\), obtaining \((m, r)\), and returns \(m\) with the list \(x\) followed by \(r\). The total cost is one plus the cost of the recursive extraction.

def extractMin (candidate : α) : List α → TimeM Nat (α × List α)
  | [] => pure (candidate, [])
  | x :: xs => do
      ✓
      if x < candidate then
        let (minimum, rest) ← extractMin x xs
        return (minimum, candidate :: rest)
      else
        let (minimum, rest) ← extractMin candidate xs
        return (minimum, x :: rest)

Used by 5

Used byCorrectness of minimum extraction · Cost of minimum extraction · Selection sort · Correctness of selection sort · Comparison count of selection sort

DefinitionSelection sort#✓fully proved

Selection sort of a list \(L\) over a linearly ordered type is defined recursively. If \(L\) is empty, the result is the empty list at cost \(0\). If \(L\) has head \(x\) and tail \(L'\), minimum extraction from \(L'\) with initial candidate \(x\) yields a minimum \(m\) and the list \(r\) of remaining elements, and the result is \(m\) followed by the selection sort of \(r\). The cost is the sum of the costs of all these minimum extractions.

def selectionSort (xs : List α) : TimeM Nat (List α) :=
  let rec loop : Nat → List α → TimeM Nat (List α)
    | 0, _ => pure []
    | _ + 1, [] => pure []
    | fuel + 1, x :: xs => do
        let (minimum, rest) ← extractMin x xs
        let sorted ← loop fuel rest
        return minimum :: sorted
  loop xs.length xs

Uses 1 · Used by 2

Statement usesMinimum extraction

Used byCorrectness of selection sort · Comparison count of selection sort

TheoremCost of minimum extraction#✓fully proved

For every element \(c\) of a linearly ordered type and every list \(L\) over it, minimum extraction from \(L\) with initial candidate \(c\) has cost exactly \(|L|\), the length of \(L\); that is, it performs exactly \(|L|\) order comparisons.

@[simp]
theorem extractMin_time (candidate : α) (xs : List α) :
    (extractMin candidate xs).time = xs.length

Uses 1 · Used by 1

Statement usesMinimum extraction

Used byComparison count of selection sort

TheoremCorrectness of minimum extraction#✓fully proved

Let \(c\) be an element of a linearly ordered type and \(L\) a list over it, and let \((m, r)\) be the pair returned by minimum extraction from \(L\) with initial candidate \(c\). Then the list \(m\) followed by \(r\) is a permutation of the list \(c\) followed by \(L\), \(m \le c\), and \(m \le x\) for every element \(x\) of \(L\).

theorem extractMin_correct (candidate : α) (xs : List α) :
    List.Perm
        ((extractMin candidate xs).ret.1 :: (extractMin candidate xs).ret.2)
        (candidate :: xs) ∧
      (extractMin candidate xs).ret.1 ≤ candidate ∧
      ∀ x ∈ xs, (extractMin candidate xs).ret.1 ≤ x

Uses 1

Statement usesMinimum extraction

TheoremCorrectness of selection sort#✓fully proved

For every list \(L\) over a linearly ordered type, the list returned by selection sort on \(L\) is sorted in nondecreasing order (each entry is \(\le\) every later entry) and is a permutation of \(L\), so it preserves duplicate multiplicities.

theorem selectionSort_correct (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (selectionSort xs).ret ∧
      List.Perm (selectionSort xs).ret xs

Uses 2

Statement usesSelection sort

Proof usesMinimum extraction

TheoremComparison count of selection sort#✓fully proved

For every list of length \(n\) over a linearly ordered type, selection sort has cost exactly \(n(n-1)/2\) in the model that charges one unit per order comparison; that is, it performs exactly \(n(n-1)/2\) comparisons.

theorem selectionSort_time (xs : List α) :
    (selectionSort xs).time = xs.length * (xs.length - 1) / 2

Uses 3

Statement usesSelection sort

Proof usesMinimum extraction · Cost of minimum extraction

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.