Heapsort

DefinitionHeap sort#✓fully proved

For a list \(xs\) of elements of a linearly ordered type, heap sort inserts the entries of \(xs\) one at a time, from first to last, into the empty binary min-heap, and then extracts the minimum of the heap as many times as the heap has entries, each time continuing with the remaining heap. The output is the list of the extracted minima in the order in which they were extracted.

def heapSort (xs : List α) : List α :=
  let heap := xs.foldl (fun current value => current.push value) MinHeap.empty
  let rec loop : Nat → MinHeap α → List α
    | 0, _ => []
    | fuel + 1, current =>
        match current.extractMin with
        | none => []
        | some (minimum, rest) => minimum :: loop fuel rest
  loop heap.data.size heap

Uses 4 · Used by 4

Statement usesBinary min-heap · Empty binary min-heap · Extracting the minimum of a binary min-heap · Insertion into a binary min-heap

Used byCorrectness of heap sort · Heap sort preserves multiplicities · Heap sort permutes its input · Heap sort output is sorted

TheoremHeap sort preserves multiplicities#✓fully proved

For every list \(xs\) of elements of a linearly ordered type, the output of heap sort on \(xs\) and \(xs\) itself are equal as multisets: every value occurs in both lists the same number of times.

theorem heapSort_multiset (xs : List α) :
    (↑(heapSort xs) : Multiset α) = (↑xs : Multiset α)

Uses 13 · Used by 1

Statement usesHeap sort

Proof usesHeap order on a level-order array · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Empty binary min-heap · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is minimal · Insertion into a binary min-heap · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid

Used byHeap sort permutes its input

TheoremHeap sort permutes its input#✓fully proved

For every list \(xs\) of elements of a linearly ordered type, heap sort returns a permutation of \(xs\).

theorem heapSort_perm (xs : List α) : List.Perm (heapSort xs) xs

Uses 2 · Used by 1

Statement usesHeap sort

Proof usesHeap sort preserves multiplicities

Used byCorrectness of heap sort

TheoremHeap sort output is sorted#✓fully proved

For every list \(xs\) of elements of a linearly ordered type, heap sort returns a list sorted in nondecreasing order.

theorem heapSort_sorted (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (heapSort xs)

Uses 9 · Used by 1

Statement usesHeap sort

Proof usesBinary min-heap · Elements of a binary min-heap · Empty binary min-heap · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is minimal · Insertion into a binary min-heap

Used byCorrectness of heap sort

TheoremCorrectness of heap sort#✓fully proved

For every list \(xs\) of elements of a linearly ordered type, heap sort returns a list that is sorted in nondecreasing order and is a permutation of \(xs\).

theorem heapSort_correct (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (heapSort xs) ∧ List.Perm (heapSort xs) xs

Uses 3

Statement usesHeap sort

Proof usesHeap sort permutes its input · Heap sort output is sorted

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.