1. CLRS-Lean
  2. Chapter 6. Heapsort
  3. 6.4. The Heapsort Algorithm
Imports
import CLRSLean.Chapter_06.Section_06_3_Building_A_Heap

CLRS Section 6.4 - The Heapsort Algorithm

This section gives the array-level refinement of CLRS HEAPSORT. The older functional heapsort theorem is kept as a compact auxiliary scaffold, but the reader-facing theorem now follows the in-place loop shape directly: swap the heap root with the last heap element, shrink the heap prefix, then repair the prefix with MAX-HEAPIFY.

Main results:

  • Definition arrayHeapSortInPlaceLoop: the CLRS shrinking-heap loop.

  • Theorem arrayHeapSortInPlaceLoop_perm: the loop preserves the multiset of array elements.

  • Theorem arrayHeapSortInPlaceLoop_length: the loop preserves array length.

  • Definitions SortedSuffix, PrefixLeSuffix, and HeapSortLoopInvariant: the formal sorted-suffix loop invariant.

  • Theorems arrayHeapSortStep_suffix_head_eq_root and arrayHeapSortStep_suffix_head_bounds_prefix: one CLRS iteration moves the old heap root to the new sorted-suffix head and leaves it above the remaining heap prefix.

  • Theorem HeapSortLoopInvariant.step: one nontrivial CLRS loop iteration preserves the full heap-prefix / sorted-suffix invariant.

  • Theorem arrayHeapSortStep_state_correct: one nontrivial CLRS iteration bundles the next invariant, permutation, length preservation, and root-to- suffix-head fact.

  • Theorem arrayHeapSortInPlaceLoop_exact_shrink_invariant: after any admissible number of iterations, the heap prefix has exactly shrunk by that many cells.

  • Theorem arrayHeapSortInPlaceLoop_terminal_invariant: repeated loop iterations preserve the invariant until the heap prefix has size at most one.

  • Theorem arrayHeapSortInPlaceLoop_orderedAsc: the fuelled in-place loop returns ascending output when started with enough fuel and the invariant.

  • Theorem arrayHeapSortInPlaceLoop_state_correct: the same loop also exposes the final terminal invariant, sortedness, permutation, and length preservation as one CLRS-style state-correctness package.

  • Theorem arrayHeapSortInPlaceLoop_exact_state_correct: the exact partial-run invariant together with permutation and length preservation.

  • Theorem arrayHeapSortInPlace_orderedAsc: the CLRS in-place heapsort implementation returns ascending output.

  • Theorems arrayHeapSortInPlace_exact_state_correct and arrayHeapSort_exact_state_correct: non-existential exact terminal state packages for the in-place and public heapsort interfaces.

  • Theorem arrayHeapSort_orderedAsc: heapsort returns ascending output.

  • Theorem arrayHeapSort_perm: heapsort preserves the multiset of input elements.

  • Theorems arrayHeapSortInPlace_correct and arrayHeapSort_correct: reader-facing correctness specifications bundling sortedness, permutation, and length preservation.

Remaining refinements:

  • The in-place correctness proof is complete at the current functional-array level. Later work can add line-by-line RAM costs and share an imperative array semantics with other chapters.

namespace CLRSnamespace Chapter06

In-place heapsort loop scaffold

The suffix from heapSize to the end of the array is sorted in ascending order. The predicate is stated with valAt to keep later swap and heapify proofs free of repetitive in-bounds casts.

def SortedSuffix (a : List Nat) (heapSize : Nat) : Prop := ∀ {i j : Nat}, heapSize ≤ i → i ≤ j → j < a.length → valAt a i ≤ valAt a j

Every element in the heap prefix is at most every element in the sorted suffix. Together with ArrayMaxHeap on the prefix, this is the usual CLRS loop invariant for heapsort.

def PrefixLeSuffix (a : List Nat) (heapSize : Nat) : Prop := ∀ {i j : Nat}, i < heapSize → heapSize ≤ j → j < a.length → valAt a i ≤ valAt a j

Every element in the heap prefix is bounded by a fixed value.

def PrefixLeBound (a : List Nat) (heapSize bound : Nat) : Prop := ∀ {i : Nat}, i < heapSize → valAt a i ≤ bound

The array-level CLRS heapsort loop invariant.

structure HeapSortLoopInvariant (a : List Nat) (heapSize : Nat) : Prop where heap : ArrayMaxHeap a heapSize suffix_sorted : SortedSuffix a heapSize prefix_le_suffix : PrefixLeSuffix a heapSize

In a nonempty array heap, the root bounds every heap-prefix cell in valAt form.

The heap root is a bound for the whole heap prefix.

theorem PrefixLeBound.of_heap_root {a : List Nat} {heapSize : Nat} (hheap : ArrayMaxHeap a heapSize) : PrefixLeBound a heapSize (valAt a 0) :=

Swapping two in-prefix cells preserves a prefix-wide upper bound.

Fuelled heapify preserves any upper bound on the heap prefix.

After swapping the heap root with the last heap-prefix element and shrinking the prefix by one, every heap edge except possibly the new root edge is still valid.

After the root/last swap, the sorted suffix grows by one cell. The new suffix head contains the old heap root, and the old prefix/suffix boundary says that this root is at most every element of the old suffix.

After moving the old maximum to the new suffix head, the remaining heap prefix is still bounded above by that old maximum.

exact hinv.heap.valAt_le_root ( )

The initial sorted suffix is empty.

theorem SortedSuffix.empty (a : List Nat) : SortedSuffix a a.length :=

With an empty suffix, the prefix/suffix boundary condition is vacuous.

theorem PrefixLeSuffix.empty (a : List Nat) : PrefixLeSuffix a a.length :=

Heapifying inside the prefix does not disturb a sorted suffix to its right.

A zero-start sorted suffix is the ordinary ascending-order predicate.

The heap-built initial array satisfies the CLRS heapsort loop invariant.

theorem HeapSortLoopInvariant.initial (xs : List Nat) : HeapSortLoopInvariant (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length :=

At heap size zero, the loop invariant gives the final ascending order.

theorem HeapSortLoopInvariant.orderedAsc_of_zero {a : List Nat} (h : HeapSortLoopInvariant a 0) : OrderedAsc a := orderedAsc_of_sortedSuffix_zero h.suffix_sorted

When the heap prefix has size at most one, the loop invariant already implies that the whole array is sorted: either the suffix is the full array, or the single remaining prefix cell is bounded by every suffix cell.

One CLRS heapsort iteration. It moves the current maximum to the last cell of the heap prefix, shrinks the heap prefix, and repairs the new root.

def arrayHeapSortStep (a : List Nat) (heapSize : Nat) : List Nat := match heapSize with | 0 => a | 1 => a | newHeapSize + 2 => let last := newHeapSize + 1 maxHeapifyFuel (newHeapSize + 1) (swapAt a 0 last) (newHeapSize + 1) 0

One nontrivial CLRS heapsort iteration writes the old heap root into the new sorted-suffix head. This is the operational root/last-swap fact behind the textbook statement that each iteration moves the current maximum into final position.

One nontrivial CLRS heapsort iteration preserves the full loop invariant: the heap prefix shrinks by one, the sorted suffix grows by one, and every remaining prefix element is still bounded by the suffix.

Fuelled CLRS heapsort loop. The third argument is the current heap prefix size; the first argument is only a termination fuel and is instantiated with the input length by arrayHeapSortInPlace.

def arrayHeapSortInPlaceLoop : Nat → List Nat → Nat → List Nat | 0, a, _ => a | fuel + 1, a, heapSize => match heapSize with | 0 => a | 1 => a | newHeapSize + 2 => let next := arrayHeapSortStep a (newHeapSize + 2) arrayHeapSortInPlaceLoop fuel next (newHeapSize + 1)

If the fuel is at least the current heap size, the repeated CLRS in-place loop preserves the full loop invariant until the terminal heap prefix has size at most one. This is the loop-invariant statement behind the final sortedness theorem.

Exact partial-run form of the CLRS shrinking-heap invariant. Running fuel genuine loop iterations from a heap prefix of size heapSize leaves the invariant at precisely heapSize - fuel; the hypothesis rules out asking the loop to step past the terminal one-cell heap.

Terminal exact-run invariant for the CLRS loop: after exactly heapSize - 1 genuine iterations, the heap prefix is terminal (0 for an empty input, otherwise 1).

theorem arrayHeapSortInPlaceLoop_exact_terminal_invariant {a : List Nat} {heapSize : Nat} (hinv : HeapSortLoopInvariant a heapSize) : HeapSortLoopInvariant (arrayHeapSortInPlaceLoop (heapSize - 1) a heapSize) (heapSize - (heapSize - 1)) :=

If the fuel is at least the current heap size, the CLRS in-place heapsort loop finishes in an ascending array. The proof is the textbook loop-invariant argument: heap sizes 0 and 1 are terminal, while larger heap sizes use the single-step invariant theorem and recurse on the smaller heap prefix.

theorem arrayHeapSortInPlaceLoop_orderedAsc (fuel : Nat) {a : List Nat} {heapSize : Nat} (hfuel : heapSize ≤ fuel) (hinv : HeapSortLoopInvariant a heapSize) : OrderedAsc (arrayHeapSortInPlaceLoop fuel a heapSize) :=

In-place heapsort starts by building a max-heap, then runs the CLRS loop.

def arrayHeapSortInPlace (xs : List Nat) : List Nat := let heap := arrayBuildMaxHeap xs arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length

The top-level CLRS in-place heapsort run terminates with the loop invariant.

theorem arrayHeapSortInPlace_terminal_invariant (xs : List Nat) : ∃ heapSize, heapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSortInPlace xs) heapSize :=

One heapsort step preserves list length.

theorem arrayHeapSortStep_length (a : List Nat) (heapSize : Nat) : (arrayHeapSortStep a heapSize).length = a.length := cases heapSize with cases heapSize with

One heapsort step preserves the multiset of elements.

theorem arrayHeapSortStep_perm (a : List Nat) (heapSize : Nat) : (arrayHeapSortStep a heapSize).Perm a := cases heapSize with cases heapSize with

After one nontrivial CLRS heapsort iteration, the newly appended suffix head dominates every cell still inside the heap prefix.

Single-step state-correctness package for a nontrivial CLRS heapsort iteration: the next heap-prefix / sorted-suffix invariant holds, the array elements and length are preserved, and the old root is exactly the new suffix head.

theorem arrayHeapSortStep_state_correct {a : List Nat} {newHeapSize : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 2)) : HeapSortLoopInvariant (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) ∧ (arrayHeapSortStep a (newHeapSize + 2)).Perm a ∧ (arrayHeapSortStep a (newHeapSize + 2)).length = a.length ∧ valAt (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) = valAt a 0 :=

The in-place heapsort loop preserves list length.

theorem arrayHeapSortInPlaceLoop_length (fuel : Nat) (a : List Nat) (heapSize : Nat) : (arrayHeapSortInPlaceLoop fuel a heapSize).length = a.length := induction fuel generalizing a heapSize with cases heapSize with cases heapSize with

The in-place heapsort loop preserves the multiset of elements.

theorem arrayHeapSortInPlaceLoop_perm (fuel : Nat) (a : List Nat) (heapSize : Nat) : (arrayHeapSortInPlaceLoop fuel a heapSize).Perm a := induction fuel generalizing a heapSize with cases heapSize with cases heapSize with

Exact state-correctness package for a partial CLRS heapsort run. After fuel genuine iterations, the heap prefix has size exactly heapSize - fuel, while the loop has preserved both the input multiset and the array length.

theorem arrayHeapSortInPlaceLoop_exact_state_correct (fuel : Nat) {a : List Nat} {heapSize : Nat} (hfuel : fuel ≤ heapSize - 1) (hinv : HeapSortLoopInvariant a heapSize) : HeapSortLoopInvariant (arrayHeapSortInPlaceLoop fuel a heapSize) (heapSize - fuel) ∧ (arrayHeapSortInPlaceLoop fuel a heapSize).Perm a ∧ (arrayHeapSortInPlaceLoop fuel a heapSize).length = a.length :=

Reader-facing state-correctness theorem for the fuelled CLRS heapsort loop. Starting from the full heap-prefix / sorted-suffix invariant and enough fuel, the loop reaches a terminal heap prefix while preserving sortedness, permutation, and length.

theorem arrayHeapSortInPlaceLoop_state_correct (fuel : Nat) {a : List Nat} {heapSize : Nat} (hfuel : heapSize ≤ fuel) (hinv : HeapSortLoopInvariant a heapSize) : ∃ finalHeapSize, finalHeapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSortInPlaceLoop fuel a heapSize) finalHeapSize ∧ OrderedAsc (arrayHeapSortInPlaceLoop fuel a heapSize) ∧ (arrayHeapSortInPlaceLoop fuel a heapSize).Perm a ∧ (arrayHeapSortInPlaceLoop fuel a heapSize).length = a.length :=

In-place heapsort preserves list length.

theorem arrayHeapSortInPlace_length (xs : List Nat) : (arrayHeapSortInPlace xs).length = xs.length := exact (arrayHeapSortInPlaceLoop_length ((arrayBuildMaxHeap xs).length - 1) (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length).trans ( )

In-place heapsort preserves the multiset of input elements.

theorem arrayHeapSortInPlace_perm (xs : List Nat) : (arrayHeapSortInPlace xs).Perm xs :=

In-place heapsort returns ascending output.

theorem arrayHeapSortInPlace_orderedAsc (xs : List Nat) : OrderedAsc (arrayHeapSortInPlace xs) := exact hinv.orderedAsc_of_heapSize_le_one ( )

Reader-facing correctness theorem for the in-place CLRS heapsort refinement: the shrinking-heap loop returns sorted output, preserves the input multiset, and keeps the array length unchanged.

theorem arrayHeapSortInPlace_correct (xs : List Nat) : OrderedAsc (arrayHeapSortInPlace xs) ∧ (arrayHeapSortInPlace xs).Perm xs ∧ (arrayHeapSortInPlace xs).length = xs.length :=

State-correctness theorem for the concrete CLRS in-place heapsort implementation: the built heap enters the shrinking loop, exits with a terminal heap prefix, and the final array is sorted, a permutation of the input, and length-preserving.

exact hperm.trans ( ) exact hlen.trans ( )

Exact non-existential state-correctness theorem for the concrete CLRS in-place heapsort implementation. It records the terminal heap-prefix size produced by the exact shrinking loop, then bundles the final invariant, sortedness, permutation, and length preservation.

Array-level heapsort refinement theorems

Array-facing name for the CLRS in-place heapsort implementation.

def arrayHeapSort (xs : List Nat) : List Nat := arrayHeapSortInPlace xs

The public array-facing heapsort interface is the in-place CLRS loop.

theorem arrayHeapSort_eq_arrayHeapSortInPlace (xs : List Nat) : arrayHeapSort xs = arrayHeapSortInPlace xs :=

Public heapsort also exposes the terminal loop invariant of the in-place run.

theorem arrayHeapSort_terminal_invariant (xs : List Nat) : ∃ heapSize, heapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSort xs) heapSize :=

Public state-correctness theorem for Chapter 6 heapsort. This is the compact CLRS loop-invariant specification exposed by the array-facing interface.

theorem arrayHeapSort_state_correct (xs : List Nat) : ∃ heapSize, heapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSort xs) heapSize ∧ OrderedAsc (arrayHeapSort xs) ∧ (arrayHeapSort xs).Perm xs ∧ (arrayHeapSort xs).length = xs.length :=

Public non-existential exact state package for Chapter 6 heapsort.

theorem arrayHeapSort_exact_state_correct (xs : List Nat) : HeapSortLoopInvariant (arrayHeapSort xs) ((arrayBuildMaxHeap xs).length - ((arrayBuildMaxHeap xs).length - 1)) ∧ (arrayBuildMaxHeap xs).length - ((arrayBuildMaxHeap xs).length - 1) ≤ 1 ∧ OrderedAsc (arrayHeapSort xs) ∧ (arrayHeapSort xs).Perm xs ∧ (arrayHeapSort xs).length = xs.length :=

Array-facing heapsort returns ascending output.

theorem arrayHeapSort_orderedAsc (xs : List Nat) : OrderedAsc (arrayHeapSort xs) :=

Array-facing heapsort preserves the input elements.

theorem arrayHeapSort_perm (xs : List Nat) : (arrayHeapSort xs).Perm xs :=

Main Chapter 6 heapsort specification. The public arrayHeapSort interface is the in-place CLRS loop, and it returns a sorted permutation of the input with the same length.

theorem arrayHeapSort_correct (xs : List Nat) : OrderedAsc (arrayHeapSort xs) ∧ (arrayHeapSort xs).Perm xs ∧ (arrayHeapSort xs).length = xs.length := exact ⟨arrayHeapSort_orderedAsc xs, arrayHeapSort_perm xs, ⟩
end Chapter06end CLRS