Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 6. Heapsort
  4. 6.4. The Heapsort Algorithm
Browse chapters
Imports
import CLRSLean.FourthEdition.Chapter_06.Section_06_3_Building_A_Heap

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.

Implementation details

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.

theorem ArrayMaxHeap.valAt_le_root {a : List Nat} {heapSize i : Nat} (hheap : ArrayMaxHeap a heapSize) (hi : i < heapSize) : valAt a i ≤ valAt a 0 := by have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hheap.heapSize_le_length have h0_heap : 0 < heapSize := Nat.zero_lt_of_lt hi have h0_len : 0 < a.length := Nat.lt_of_lt_of_le h0_heap hheap.heapSize_le_length have hval := hheap.getElem_le_root hi rw [← valAt_eq_getElem a hi_len, ← valAt_eq_getElem a h0_len] at hval exact hval

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) := by intro i hi exact hheap.valAt_le_root hi

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

theorem PrefixLeBound.of_swapAt {a : List Nat} {heapSize bound i j : Nat} (hbound : PrefixLeBound a heapSize bound) (hlen : heapSize ≤ a.length) (hi : i < heapSize) (hj : j < heapSize) : PrefixLeBound (swapAt a i j) heapSize bound := by intro k hk have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hlen have hj_len : j < a.length := Nat.lt_of_lt_of_le hj hlen by_cases hki : k = i · subst k rw [valAt_swapAt_left hi_len hj_len] exact hbound hj · by_cases hkj : k = j · subst k rw [valAt_swapAt_right hi_len hj_len] exact hbound hi · rw [valAt_swapAt_of_ne hi_len hj_len hki hkj] exact hbound hk

Fuelled heapify preserves any upper bound on the heap prefix.

theorem PrefixLeBound.of_maxHeapifyFuel {fuel : Nat} {a : List Nat} {heapSize i bound : Nat} (hbound : PrefixLeBound a heapSize bound) (hlen : heapSize ≤ a.length) (hi : i < heapSize) : PrefixLeBound (maxHeapifyFuel fuel a heapSize i) heapSize bound := by intro k hk induction fuel generalizing a i k with | zero => simpa [maxHeapifyFuel] using hbound hk | succ fuel ih => by_cases hmax : maxChildIndex a heapSize i = i · simpa [maxHeapifyFuel, hmax] using hbound hk · let largest := maxChildIndex a heapSize i have hlargest : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hswap_len : heapSize ≤ (swapAt a i largest).length := by simpa [largest, swapAt_length] using hlen have hswap_bound : PrefixLeBound (swapAt a i largest) heapSize bound := PrefixLeBound.of_swapAt (a := a) (heapSize := heapSize) (bound := bound) (i := i) (j := largest) hbound hlen hi hlargest have hrec := ih (a := swapAt a i largest) (i := largest) (k := k) hswap_bound hswap_len hlargest hk simpa [maxHeapifyFuel, hmax, largest] using hrec

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.

theorem ArrayMaxHeapExcept.of_swap_root_last {a : List Nat} {newHeapSize : Nat} (hheap : ArrayMaxHeap a (newHeapSize + 1)) : ArrayMaxHeapExcept (swapAt a 0 newHeapSize) newHeapSize 0 := by have hlen_old : newHeapSize + 1 ≤ a.length := hheap.heapSize_le_length have hlen_swapped : newHeapSize ≤ (swapAt a 0 newHeapSize).length := by rw [swapAt_length] omega have h0_len : 0 < a.length := by have hpos : 0 < newHeapSize + 1 := by omega exact Nat.lt_of_lt_of_le hpos hheap.heapSize_le_length have hlast_len : newHeapSize < a.length := by omega refine ⟨hlen_swapped, ?_, ?_⟩ · intro i hi hbad hl have hi_old : i < newHeapSize + 1 := by omega have hl_old : left i < newHeapSize + 1 := by omega have hchild_old_len : left i < a.length := Nat.lt_of_lt_of_le hl_old hheap.heapSize_le_length have hparent_old_len : i < a.length := Nat.lt_of_lt_of_le hi_old hheap.heapSize_le_length have hchild_ne_zero : left i ≠ 0 := by unfold left omega have hchild_ne_last : left i ≠ newHeapSize := by omega have hparent_ne_last : i ≠ newHeapSize := by omega have hchild_read : valAt (swapAt a 0 newHeapSize) (left i) = valAt a (left i) := valAt_swapAt_of_ne h0_len hlast_len hchild_ne_zero hchild_ne_last have hparent_read : valAt (swapAt a 0 newHeapSize) i = valAt a i := valAt_swapAt_of_ne h0_len hlast_len hbad hparent_ne_last have hold := hheap.left_le hi_old hl_old rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a 0 newHeapSize) (left i) ≤ valAt (swapAt a 0 newHeapSize) i := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a 0 newHeapSize) (Nat.lt_of_lt_of_le hl hlen_swapped), valAt_eq_getElem (swapAt a 0 newHeapSize) (Nat.lt_of_lt_of_le hi hlen_swapped)] at hval exact hval · intro i hi hbad hr have hi_old : i < newHeapSize + 1 := by omega have hr_old : right i < newHeapSize + 1 := by omega have hchild_old_len : right i < a.length := Nat.lt_of_lt_of_le hr_old hheap.heapSize_le_length have hparent_old_len : i < a.length := Nat.lt_of_lt_of_le hi_old hheap.heapSize_le_length have hchild_ne_zero : right i ≠ 0 := by unfold right omega have hchild_ne_last : right i ≠ newHeapSize := by omega have hparent_ne_last : i ≠ newHeapSize := by omega have hchild_read : valAt (swapAt a 0 newHeapSize) (right i) = valAt a (right i) := valAt_swapAt_of_ne h0_len hlast_len hchild_ne_zero hchild_ne_last have hparent_read : valAt (swapAt a 0 newHeapSize) i = valAt a i := valAt_swapAt_of_ne h0_len hlast_len hbad hparent_ne_last have hold := hheap.right_le hi_old hr_old rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a 0 newHeapSize) (right i) ≤ valAt (swapAt a 0 newHeapSize) i := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a 0 newHeapSize) (Nat.lt_of_lt_of_le hr hlen_swapped), valAt_eq_getElem (swapAt a 0 newHeapSize) (Nat.lt_of_lt_of_le hi hlen_swapped)] at hval exact hval

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.

theorem SortedSuffix.of_swap_root_last {a : List Nat} {newHeapSize : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 1)) : SortedSuffix (swapAt a 0 newHeapSize) newHeapSize := by have hlen_old : newHeapSize + 1 ≤ a.length := hinv.heap.heapSize_le_length have h0_len : 0 < a.length := by have hpos : 0 < newHeapSize + 1 := by omega exact Nat.lt_of_lt_of_le hpos hlen_old have hlast_len : newHeapSize < a.length := by omega intro p q hp hpq hq have hq_old : q < a.length := by simpa [swapAt_length] using hq by_cases hp_last : p = newHeapSize · subst p by_cases hq_last : q = newHeapSize · subst q exact Nat.le_refl _ · have hq_old_suffix : newHeapSize + 1 ≤ q := by omega have hq_ne_zero : q ≠ 0 := by omega have hq_read : valAt (swapAt a 0 newHeapSize) q = valAt a q := valAt_swapAt_of_ne h0_len hlast_len hq_ne_zero hq_last have hhead_read : valAt (swapAt a 0 newHeapSize) newHeapSize = valAt a 0 := valAt_swapAt_right h0_len hlast_len have hle := hinv.prefix_le_suffix (i := 0) (j := q) (by omega) hq_old_suffix hq_old rw [hhead_read, hq_read] exact hle · have hp_old_suffix : newHeapSize + 1 ≤ p := by omega have hq_old_suffix : newHeapSize + 1 ≤ q := Nat.le_trans hp_old_suffix hpq have hp_ne_zero : p ≠ 0 := by omega have hq_ne_zero : q ≠ 0 := by omega have hq_ne_last : q ≠ newHeapSize := by omega have hp_read : valAt (swapAt a 0 newHeapSize) p = valAt a p := valAt_swapAt_of_ne h0_len hlast_len hp_ne_zero hp_last have hq_read : valAt (swapAt a 0 newHeapSize) q = valAt a q := valAt_swapAt_of_ne h0_len hlast_len hq_ne_zero hq_ne_last have hle := hinv.suffix_sorted hp_old_suffix hpq hq_old rw [hp_read, hq_read] exact hle

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

theorem PrefixLeBound.of_swap_root_last {a : List Nat} {newHeapSize : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 1)) : PrefixLeBound (swapAt a 0 newHeapSize) newHeapSize (valAt a 0) := by have hlen_old : newHeapSize + 1 ≤ a.length := hinv.heap.heapSize_le_length have h0_len : 0 < a.length := by have hpos : 0 < newHeapSize + 1 := by omega exact Nat.lt_of_lt_of_le hpos hlen_old have hlast_len : newHeapSize < a.length := by omega intro k hk by_cases hk_zero : k = 0 · subst k have hread : valAt (swapAt a 0 newHeapSize) 0 = valAt a newHeapSize := valAt_swapAt_left h0_len hlast_len rw [hread] exact hinv.heap.valAt_le_root (by omega) · have hk_last : k ≠ newHeapSize := by omega have hread : valAt (swapAt a 0 newHeapSize) k = valAt a k := valAt_swapAt_of_ne h0_len hlast_len hk_zero hk_last rw [hread] exact hinv.heap.valAt_le_root (by omega)

The initial sorted suffix is empty.

theorem SortedSuffix.empty (a : List Nat) : SortedSuffix a a.length := by intro i j hi _ hj omega

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

theorem PrefixLeSuffix.empty (a : List Nat) : PrefixLeSuffix a a.length := by intro i j _ hj hjlen omega

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

theorem SortedSuffix.maxHeapifyFuel {fuel : Nat} {a : List Nat} {heapSize i suffixStart : Nat} (hlen : heapSize ≤ a.length) (hi : i < heapSize) (hboundary : heapSize ≤ suffixStart) (hsuffix : SortedSuffix a suffixStart) : SortedSuffix (CLRS.Chapter06.maxHeapifyFuel fuel a heapSize i) suffixStart := by intro p q hp hpq hq have hq_old : q < a.length := by simpa [CLRS.Chapter06.maxHeapifyFuel_length fuel a heapSize i] using hq have hp_heap : heapSize ≤ p := Nat.le_trans hboundary hp have hq_heap : heapSize ≤ q := Nat.le_trans hp_heap hpq have hp_read : valAt (CLRS.Chapter06.maxHeapifyFuel fuel a heapSize i) p = valAt a p := maxHeapifyFuel_valAt_of_heapSize_le (fuel := fuel) (a := a) (heapSize := heapSize) (i := i) (k := p) hlen hi hp_heap have hq_read : valAt (CLRS.Chapter06.maxHeapifyFuel fuel a heapSize i) q = valAt a q := maxHeapifyFuel_valAt_of_heapSize_le (fuel := fuel) (a := a) (heapSize := heapSize) (i := i) (k := q) hlen hi hq_heap rw [hp_read, hq_read] exact hsuffix hp hpq hq_old

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

theorem orderedAsc_of_sortedSuffix_zero {a : List Nat} (hsuffix : SortedSuffix a 0) : OrderedAsc a := by rw [OrderedAsc, List.pairwise_iff_getElem] intro i j hi hj hij have hval := hsuffix (i := i) (j := j) (Nat.zero_le i) (Nat.le_of_lt hij) hj simpa [valAt, List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] using hval

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

theorem HeapSortLoopInvariant.initial (xs : List Nat) : HeapSortLoopInvariant (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length := by refine ⟨arrayBuildMaxHeap_isMaxHeap xs, ?_, ?_⟩ · exact SortedSuffix.empty (arrayBuildMaxHeap xs) · exact PrefixLeSuffix.empty (arrayBuildMaxHeap xs)

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.

theorem HeapSortLoopInvariant.orderedAsc_of_heapSize_le_one {a : List Nat} {heapSize : Nat} (h : HeapSortLoopInvariant a heapSize) (hsmall : heapSize ≤ 1) : OrderedAsc a := by rw [OrderedAsc, List.pairwise_iff_getElem] intro i j hi hj hij by_cases hi_suffix : heapSize ≤ i · have hval := h.suffix_sorted hi_suffix (Nat.le_of_lt hij) hj simpa [valAt, List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] using hval · have hi_heap : i < heapSize := Nat.lt_of_not_ge hi_suffix have hj_suffix : heapSize ≤ j := by omega have hval := h.prefix_le_suffix hi_heap hj_suffix hj simpa [valAt, List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] using hval

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.

theorem arrayHeapSortStep_suffix_head_eq_root {a : List Nat} {newHeapSize : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 2)) : valAt (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) = valAt a 0 := by let newSize := newHeapSize + 1 have hinv' : HeapSortLoopInvariant a (newSize + 1) := by simpa [newSize, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hinv have hlen_old : newSize + 1 ≤ a.length := hinv'.heap.heapSize_le_length have h0_len : 0 < a.length := by have hpos : 0 < newSize + 1 := by omega exact Nat.lt_of_lt_of_le hpos hlen_old have hlast_len : newSize < a.length := by omega have hswapped_len : newSize ≤ (swapAt a 0 newSize).length := by rw [swapAt_length] omega have hpos_new : 0 < newSize := by simp [newSize] have hheapify_read : valAt (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize = valAt (swapAt a 0 newSize) newSize := maxHeapifyFuel_valAt_of_heapSize_le (fuel := newSize) (a := swapAt a 0 newSize) (heapSize := newSize) (i := 0) (k := newSize) hswapped_len hpos_new (Nat.le_refl newSize) have hswap_read : valAt (swapAt a 0 newSize) newSize = valAt a 0 := valAt_swapAt_right h0_len hlast_len change valAt (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize = valAt a 0 exact hheapify_read.trans hswap_read

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.

theorem HeapSortLoopInvariant.step {a : List Nat} {newHeapSize : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 2)) : HeapSortLoopInvariant (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) := by let newSize := newHeapSize + 1 have hinv' : HeapSortLoopInvariant a (newSize + 1) := by simpa [newSize, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hinv have hlen_old : newSize + 1 ≤ a.length := by exact hinv'.heap.heapSize_le_length have h0_len : 0 < a.length := by have hpos : 0 < newSize + 1 := by omega exact Nat.lt_of_lt_of_le hpos hlen_old have hlast_len : newSize < a.length := by omega have hswapped_len : newSize ≤ (swapAt a 0 newSize).length := by rw [swapAt_length] omega have hpos_new : 0 < newSize := by simp [newSize] have hexcept : ArrayMaxHeapExcept (swapAt a 0 newSize) newSize 0 := by exact ArrayMaxHeapExcept.of_swap_root_last (a := a) (newHeapSize := newSize) hinv'.heap have hheap : ArrayMaxHeap (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize := maxHeapifyFuel_root_isMaxHeap hexcept hpos_new (Nat.le_refl newSize) have hswap_suffix : SortedSuffix (swapAt a 0 newSize) newSize := by exact SortedSuffix.of_swap_root_last (a := a) (newHeapSize := newSize) hinv' have hsuffix : SortedSuffix (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize := SortedSuffix.maxHeapifyFuel (fuel := newSize) (a := swapAt a 0 newSize) (heapSize := newSize) (i := 0) (suffixStart := newSize) hswapped_len hpos_new (Nat.le_refl newSize) hswap_suffix have hswap_bound : PrefixLeBound (swapAt a 0 newSize) newSize (valAt a 0) := by exact PrefixLeBound.of_swap_root_last (a := a) (newHeapSize := newSize) hinv' have hprefix_bound : PrefixLeBound (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize (valAt a 0) := PrefixLeBound.of_maxHeapifyFuel (fuel := newSize) (a := swapAt a 0 newSize) (heapSize := newSize) (i := 0) (bound := valAt a 0) hswap_bound hswapped_len hpos_new have hpref : PrefixLeSuffix (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize := by intro i j hi hj hjlen have hstep_len : (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0).length = a.length := (maxHeapifyFuel_length newSize (swapAt a 0 newSize) newSize 0).trans (swapAt_length a 0 newSize) have hj_old : j < a.length := by rwa [hstep_len] at hjlen have hheapify_read : valAt (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) j = valAt (swapAt a 0 newSize) j := maxHeapifyFuel_valAt_of_heapSize_le (fuel := newSize) (a := swapAt a 0 newSize) (heapSize := newSize) (i := 0) (k := j) hswapped_len hpos_new hj have hbound_i := hprefix_bound hi have hroot_le_suffix : valAt a 0 ≤ valAt (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) j := by by_cases hj_last : j = newSize · subst j have hswap_read : valAt (swapAt a 0 newSize) newSize = valAt a 0 := valAt_swapAt_right h0_len hlast_len rw [hheapify_read, hswap_read] · have hj_old_suffix : newSize + 1 ≤ j := by omega have hj_ne_zero : j ≠ 0 := by omega have hswap_read : valAt (swapAt a 0 newSize) j = valAt a j := valAt_swapAt_of_ne h0_len hlast_len hj_ne_zero hj_last have hle := hinv.prefix_le_suffix (i := 0) (j := j) (by omega) hj_old_suffix hj_old rw [hheapify_read, hswap_read] exact hle exact Nat.le_trans hbound_i hroot_le_suffix change HeapSortLoopInvariant (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize exact ⟨hheap, hsuffix, hpref⟩

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.

theorem arrayHeapSortInPlaceLoop_terminal_invariant (fuel : Nat) {a : List Nat} {heapSize : Nat} (hfuel : heapSize ≤ fuel) (hinv : HeapSortLoopInvariant a heapSize) : ∃ finalHeapSize, finalHeapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSortInPlaceLoop fuel a heapSize) finalHeapSize := by induction fuel generalizing a heapSize with | zero => refine ⟨heapSize, ?_, ?_⟩ · omega · simpa [arrayHeapSortInPlaceLoop] using hinv | succ fuel ih => cases heapSize with | zero => refine ⟨0, ?_, ?_⟩ · omega · simpa [arrayHeapSortInPlaceLoop] using hinv | succ heapSize => cases heapSize with | zero => refine ⟨1, ?_, ?_⟩ · omega · simpa [arrayHeapSortInPlaceLoop] using hinv | succ newHeapSize => have hfuel' : newHeapSize + 1 ≤ fuel := by omega have hstep : HeapSortLoopInvariant (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) := HeapSortLoopInvariant.step (a := a) (newHeapSize := newHeapSize) hinv simpa [arrayHeapSortInPlaceLoop] using ih (a := arrayHeapSortStep a (newHeapSize + 2)) (heapSize := newHeapSize + 1) hfuel' hstep

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.

theorem arrayHeapSortInPlaceLoop_exact_shrink_invariant (fuel : Nat) {a : List Nat} {heapSize : Nat} (hfuel : fuel ≤ heapSize - 1) (hinv : HeapSortLoopInvariant a heapSize) : HeapSortLoopInvariant (arrayHeapSortInPlaceLoop fuel a heapSize) (heapSize - fuel) := by induction fuel generalizing a heapSize with | zero => simpa [arrayHeapSortInPlaceLoop] using hinv | succ fuel ih => cases heapSize with | zero => omega | succ heapSize => cases heapSize with | zero => omega | succ newHeapSize => have hfuel' : fuel ≤ (newHeapSize + 1) - 1 := by omega have hstep : HeapSortLoopInvariant (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) := HeapSortLoopInvariant.step (a := a) (newHeapSize := newHeapSize) hinv have hrec := ih (a := arrayHeapSortStep a (newHeapSize + 2)) (heapSize := newHeapSize + 1) hfuel' hstep have hsize : newHeapSize + 2 - (fuel + 1) = newHeapSize + 1 - fuel := by omega rw [hsize] simpa [arrayHeapSortInPlaceLoop] using hrec

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)) := by exact arrayHeapSortInPlaceLoop_exact_shrink_invariant (fuel := heapSize - 1) (a := a) (heapSize := heapSize) (Nat.le_refl _) hinv

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) := by rcases arrayHeapSortInPlaceLoop_terminal_invariant (fuel := fuel) (a := a) (heapSize := heapSize) hfuel hinv with ⟨finalHeapSize, hsmall, hfinal⟩ exact hfinal.orderedAsc_of_heapSize_le_one hsmall

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 := by unfold arrayHeapSortInPlace refine ⟨(arrayBuildMaxHeap xs).length - ((arrayBuildMaxHeap xs).length - 1), ?_, ?_⟩ · omega · exact arrayHeapSortInPlaceLoop_exact_terminal_invariant (a := arrayBuildMaxHeap xs) (heapSize := (arrayBuildMaxHeap xs).length) (HeapSortLoopInvariant.initial xs)

One heapsort step preserves list length.

theorem arrayHeapSortStep_length (a : List Nat) (heapSize : Nat) : (arrayHeapSortStep a heapSize).length = a.length := by cases heapSize with | zero => simp [arrayHeapSortStep] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortStep] | succ newHeapSize => simp [arrayHeapSortStep] exact (maxHeapifyFuel_length (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0).trans (swapAt_length a 0 (newHeapSize + 1))

One heapsort step preserves the multiset of elements.

theorem arrayHeapSortStep_perm (a : List Nat) (heapSize : Nat) : (arrayHeapSortStep a heapSize).Perm a := by cases heapSize with | zero => simp [arrayHeapSortStep] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortStep] | succ newHeapSize => simp [arrayHeapSortStep] exact (maxHeapifyFuel_perm (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0).trans (swapAt_perm a 0 (newHeapSize + 1))

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

theorem arrayHeapSortStep_suffix_head_bounds_prefix {a : List Nat} {newHeapSize i : Nat} (hinv : HeapSortLoopInvariant a (newHeapSize + 2)) (hi : i < newHeapSize + 1) : valAt (arrayHeapSortStep a (newHeapSize + 2)) i ≤ valAt (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) := by have hstep : HeapSortLoopInvariant (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1) := HeapSortLoopInvariant.step (a := a) (newHeapSize := newHeapSize) hinv have hlast_len : newHeapSize + 1 < (arrayHeapSortStep a (newHeapSize + 2)).length := by rw [arrayHeapSortStep_length] have hlen : newHeapSize + 2 ≤ a.length := hinv.heap.heapSize_le_length omega exact hstep.prefix_le_suffix hi (Nat.le_refl (newHeapSize + 1)) hlast_len

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 := by exact ⟨HeapSortLoopInvariant.step (a := a) (newHeapSize := newHeapSize) hinv, arrayHeapSortStep_perm a (newHeapSize + 2), arrayHeapSortStep_length a (newHeapSize + 2), arrayHeapSortStep_suffix_head_eq_root (a := a) (newHeapSize := newHeapSize) hinv⟩

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 := by induction fuel generalizing a heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ fuel ih => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ newHeapSize => simp [arrayHeapSortInPlaceLoop] exact (ih (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1)).trans (arrayHeapSortStep_length a (newHeapSize + 2))

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 := by induction fuel generalizing a heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ fuel ih => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoop] | succ newHeapSize => exact (ih (arrayHeapSortStep a (newHeapSize + 2)) (newHeapSize + 1)).trans (arrayHeapSortStep_perm a (newHeapSize + 2))

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 := by exact ⟨arrayHeapSortInPlaceLoop_exact_shrink_invariant (fuel := fuel) (a := a) (heapSize := heapSize) hfuel hinv, arrayHeapSortInPlaceLoop_perm fuel a heapSize, arrayHeapSortInPlaceLoop_length fuel a heapSize⟩

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 := by rcases arrayHeapSortInPlaceLoop_terminal_invariant (fuel := fuel) (a := a) (heapSize := heapSize) hfuel hinv with ⟨finalHeapSize, hsmall, hfinal⟩ refine ⟨finalHeapSize, hsmall, hfinal, ?_, ?_, ?_⟩ · exact hfinal.orderedAsc_of_heapSize_le_one hsmall · exact arrayHeapSortInPlaceLoop_perm fuel a heapSize · exact arrayHeapSortInPlaceLoop_length fuel a heapSize

In-place heapsort preserves list length.

theorem arrayHeapSortInPlace_length (xs : List Nat) : (arrayHeapSortInPlace xs).length = xs.length := by unfold arrayHeapSortInPlace exact (arrayHeapSortInPlaceLoop_length ((arrayBuildMaxHeap xs).length - 1) (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length).trans (by simp [arrayBuildMaxHeap, buildMaxHeapLoop_length])

In-place heapsort preserves the multiset of input elements.

theorem arrayHeapSortInPlace_perm (xs : List Nat) : (arrayHeapSortInPlace xs).Perm xs := by unfold arrayHeapSortInPlace exact (arrayHeapSortInPlaceLoop_perm ((arrayBuildMaxHeap xs).length - 1) (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length).trans (arrayBuildMaxHeap_perm xs)

In-place heapsort returns ascending output.

theorem arrayHeapSortInPlace_orderedAsc (xs : List Nat) : OrderedAsc (arrayHeapSortInPlace xs) := by unfold arrayHeapSortInPlace have hinv := arrayHeapSortInPlaceLoop_exact_terminal_invariant (a := arrayBuildMaxHeap xs) (heapSize := (arrayBuildMaxHeap xs).length) (HeapSortLoopInvariant.initial xs) exact hinv.orderedAsc_of_heapSize_le_one (by omega)

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 := by exact ⟨arrayHeapSortInPlace_orderedAsc xs, arrayHeapSortInPlace_perm xs, arrayHeapSortInPlace_length xs⟩

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.

theorem arrayHeapSortInPlace_state_correct (xs : List Nat) : ∃ heapSize, heapSize ≤ 1 ∧ HeapSortLoopInvariant (arrayHeapSortInPlace xs) heapSize ∧ OrderedAsc (arrayHeapSortInPlace xs) ∧ (arrayHeapSortInPlace xs).Perm xs ∧ (arrayHeapSortInPlace xs).length = xs.length := by unfold arrayHeapSortInPlace let heap := arrayBuildMaxHeap xs let finalHeapSize := heap.length - (heap.length - 1) have hinv : HeapSortLoopInvariant (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length) finalHeapSize := by simpa [heap, finalHeapSize] using arrayHeapSortInPlaceLoop_exact_terminal_invariant (a := heap) (heapSize := heap.length) (HeapSortLoopInvariant.initial xs) have hsmall : finalHeapSize ≤ 1 := by omega have hsorted : OrderedAsc (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length) := hinv.orderedAsc_of_heapSize_le_one hsmall have hperm : (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).Perm heap := arrayHeapSortInPlaceLoop_perm (heap.length - 1) heap heap.length have hlen : (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).length = heap.length := arrayHeapSortInPlaceLoop_length (heap.length - 1) heap heap.length refine ⟨finalHeapSize, hsmall, hinv, hsorted, ?_, ?_⟩ · exact hperm.trans (by simpa [heap] using arrayBuildMaxHeap_perm xs) · exact hlen.trans (by simp [heap, arrayBuildMaxHeap, buildMaxHeapLoop_length])

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.

theorem arrayHeapSortInPlace_exact_state_correct (xs : List Nat) : HeapSortLoopInvariant (arrayHeapSortInPlace xs) ((arrayBuildMaxHeap xs).length - ((arrayBuildMaxHeap xs).length - 1)) ∧ (arrayBuildMaxHeap xs).length - ((arrayBuildMaxHeap xs).length - 1) ≤ 1 ∧ OrderedAsc (arrayHeapSortInPlace xs) ∧ (arrayHeapSortInPlace xs).Perm xs ∧ (arrayHeapSortInPlace xs).length = xs.length := by let heap := arrayBuildMaxHeap xs have hstate : HeapSortLoopInvariant (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length) (heap.length - (heap.length - 1)) ∧ (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).Perm heap ∧ (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).length = heap.length := arrayHeapSortInPlaceLoop_exact_state_correct (fuel := heap.length - 1) (a := heap) (heapSize := heap.length) (Nat.le_refl _) (by simpa [heap] using HeapSortLoopInvariant.initial xs) rcases hstate with ⟨hinv, hperm_heap, hlen_heap⟩ have hsmall : heap.length - (heap.length - 1) ≤ 1 := by omega have hsorted : OrderedAsc (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length) := hinv.orderedAsc_of_heapSize_le_one hsmall refine ⟨?_, ?_, ?_, ?_, ?_⟩ · simpa [arrayHeapSortInPlace, heap] using hinv · simpa [heap] using hsmall · simpa [arrayHeapSortInPlace, heap] using hsorted · have hperm : (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).Perm xs := hperm_heap.trans (by simpa [heap] using arrayBuildMaxHeap_perm xs) simpa [arrayHeapSortInPlace, heap] using hperm · have hlen : (arrayHeapSortInPlaceLoop (heap.length - 1) heap heap.length).length = xs.length := hlen_heap.trans (by simp [heap, arrayBuildMaxHeap, buildMaxHeapLoop_length]) simpa [arrayHeapSortInPlace, heap] using hlen

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 := by rfl

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 := by simpa [arrayHeapSort] using arrayHeapSortInPlace_terminal_invariant xs

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 := by simpa [arrayHeapSort] using arrayHeapSortInPlace_state_correct xs

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 := by simpa [arrayHeapSort] using arrayHeapSortInPlace_exact_state_correct xs

Array-facing heapsort returns ascending output.

theorem arrayHeapSort_orderedAsc (xs : List Nat) : OrderedAsc (arrayHeapSort xs) := by simpa [arrayHeapSort] using arrayHeapSortInPlace_orderedAsc xs

Array-facing heapsort preserves the input elements.

theorem arrayHeapSort_perm (xs : List Nat) : (arrayHeapSort xs).Perm xs := by simpa [arrayHeapSort] using arrayHeapSortInPlace_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 := by exact ⟨arrayHeapSort_orderedAsc xs, arrayHeapSort_perm xs, by simpa [arrayHeapSort] using arrayHeapSortInPlace_length xs⟩
end Chapter06end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_06.Section_06_4_Heapsort.CostedExecution

Costed execution for CLRS heapsort

This module instruments the executable Chapter 6 heap operations with an abstract unit control-step count. Projecting the first component recovers the existing execution exactly. The metric counts visited MAX-HEAPIFY frames and one extraction/swap transition for each nontrivial heapsort step. Build- loop orchestration, guards, list reads/writes, allocation, and function calls are not charged separately; this is not a RAM-cost model for Lean lists.

The tight algorithm-level bounds are proved against this same metric:

  • Theorem maxHeapifyFuelWithCost_cost_le_height / ..._cost_le_log: a heapify run visits at most one frame per level of the repaired subtree, so it costs at most ⌊log₂ heapSize⌋ + 1.

  • Theorem buildMaxHeapLoopWithCost_cost_le_linear: the bottom-up build charges at most 3 · heapSize steps, via the CLRS double-counting of node heights.

  • Theorem arrayHeapSortInPlaceWithCost_cost_le_log: the full heapsort execution satisfies the O(n log n) envelope heapSortNLogNBound.

Erasure theorems (*_result) show the costed functions project to the existing executable algorithms.

namespace CLRSnamespace Chapter06open Chapter03

Costed MAX-HEAPIFY

MAX-HEAPIFY paired with the number of visited recursive frames.

def maxHeapifyFuelWithCost : Nat → List Nat → Nat → Nat → List Nat × Nat | 0, a, _, _ => (a, 0) | fuel + 1, a, heapSize, i => let largest := maxChildIndex a heapSize i if largest = i then (a, 1) else let next := maxHeapifyFuelWithCost fuel (swapAt a i largest) heapSize largest (next.1, next.2 + 1)

Erasing the control-step count recovers the existing fuelled heapify.

theorem maxHeapifyFuelWithCost_result (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (maxHeapifyFuelWithCost fuel a heapSize i).1 = maxHeapifyFuel fuel a heapSize i := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuelWithCost, maxHeapifyFuel] | succ fuel ih => simp only [maxHeapifyFuelWithCost, maxHeapifyFuel] split · rfl · exact ih _ _

A heapify run visits at most one recursive frame per unit of fuel.

theorem maxHeapifyFuelWithCost_cost_le_fuel (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (maxHeapifyFuelWithCost fuel a heapSize i).2 ≤ fuel := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuelWithCost] | succ fuel ih => simp only [maxHeapifyFuelWithCost] split · simp · have hrec := ih (swapAt a i (maxChildIndex a heapSize i)) (maxChildIndex a heapSize i) omega

Costed bottom-up heap construction

Bottom-up heap construction paired with the sum of heapify frame counts.

def buildMaxHeapLoopWithCost : Nat → List Nat → Nat → List Nat × Nat | 0, a, _ => (a, 0) | count + 1, a, heapSize => let repaired := maxHeapifyFuelWithCost heapSize a heapSize count let rest := buildMaxHeapLoopWithCost count repaired.1 heapSize (rest.1, repaired.2 + rest.2)

Erasing build-loop cost recovers the existing bottom-up builder.

theorem buildMaxHeapLoopWithCost_result (count : Nat) (a : List Nat) (heapSize : Nat) : (buildMaxHeapLoopWithCost count a heapSize).1 = buildMaxHeapLoop count a heapSize := by induction count generalizing a with | zero => simp [buildMaxHeapLoopWithCost, buildMaxHeapLoop] | succ count ih => simp only [buildMaxHeapLoopWithCost, buildMaxHeapLoop] rw [ih, maxHeapifyFuelWithCost_result]

The bottom-up build loop uses at most count * heapSize control steps.

theorem buildMaxHeapLoopWithCost_cost_le (count : Nat) (a : List Nat) (heapSize : Nat) : (buildMaxHeapLoopWithCost count a heapSize).2 ≤ count * heapSize := by induction count generalizing a with | zero => simp [buildMaxHeapLoopWithCost] | succ count ih => simp only [buildMaxHeapLoopWithCost] have hrepair := maxHeapifyFuelWithCost_cost_le_fuel heapSize a heapSize count have hrest := ih (maxHeapifyFuelWithCost heapSize a heapSize count).1 simpa [Nat.succ_mul, Nat.add_comm] using Nat.add_le_add hrepair hrest

Top-level bottom-up heap construction with its unit control-step cost.

def arrayBuildMaxHeapWithCost (xs : List Nat) : List Nat × Nat := buildMaxHeapLoopWithCost (xs.length / 2) xs xs.length

Erasing cost from the costed builder recovers arrayBuildMaxHeap.

theorem arrayBuildMaxHeapWithCost_result (xs : List Nat) : (arrayBuildMaxHeapWithCost xs).1 = arrayBuildMaxHeap xs := by simpa [arrayBuildMaxHeapWithCost, arrayBuildMaxHeap] using buildMaxHeapLoopWithCost_result (xs.length / 2) xs xs.length

The costed builder returns a full max-heap and preserves the input multiset.

theorem arrayBuildMaxHeapWithCost_correct (xs : List Nat) : ArrayMaxHeap (arrayBuildMaxHeapWithCost xs).1 xs.length ∧ (arrayBuildMaxHeapWithCost xs).1.Perm xs := by rw [arrayBuildMaxHeapWithCost_result] constructor · simpa [arrayBuildMaxHeap, buildMaxHeapLoop_length] using arrayBuildMaxHeap_isMaxHeap xs · exact arrayBuildMaxHeap_perm xs

Costed heapsort extraction and shrinking loop

One heapsort extraction step paired with its heapify and swap-transition cost.

def arrayHeapSortStepWithCost (a : List Nat) (heapSize : Nat) : List Nat × Nat := match heapSize with | 0 => (a, 0) | 1 => (a, 0) | newHeapSize + 2 => let repaired := maxHeapifyFuelWithCost (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0 (repaired.1, repaired.2 + 1)

Erasing one costed extraction step recovers arrayHeapSortStep.

theorem arrayHeapSortStepWithCost_result (a : List Nat) (heapSize : Nat) : (arrayHeapSortStepWithCost a heapSize).1 = arrayHeapSortStep a heapSize := by cases heapSize with | zero => rfl | succ heapSize => cases heapSize with | zero => rfl | succ newHeapSize => simpa [arrayHeapSortStepWithCost, arrayHeapSortStep] using maxHeapifyFuelWithCost_result (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0

A single extraction step costs at most the current heap-prefix size.

theorem arrayHeapSortStepWithCost_cost_le_heapSize (a : List Nat) (heapSize : Nat) : (arrayHeapSortStepWithCost a heapSize).2 ≤ heapSize := by cases heapSize with | zero => simp [arrayHeapSortStepWithCost] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortStepWithCost] | succ newHeapSize => have hheapify := maxHeapifyFuelWithCost_cost_le_fuel (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0 simpa [arrayHeapSortStepWithCost] using Nat.add_le_add_right hheapify 1

The shrinking heapsort loop paired with accumulated extraction-step cost.

def arrayHeapSortInPlaceLoopWithCost : Nat → List Nat → Nat → List Nat × Nat | 0, a, _ => (a, 0) | fuel + 1, a, heapSize => match heapSize with | 0 => (a, 0) | 1 => (a, 0) | newHeapSize + 2 => let step := arrayHeapSortStepWithCost a (newHeapSize + 2) let rest := arrayHeapSortInPlaceLoopWithCost fuel step.1 (newHeapSize + 1) (rest.1, step.2 + rest.2)

Erasing loop cost recovers the existing fuelled shrinking loop.

theorem arrayHeapSortInPlaceLoopWithCost_result (fuel : Nat) (a : List Nat) (heapSize : Nat) : (arrayHeapSortInPlaceLoopWithCost fuel a heapSize).1 = arrayHeapSortInPlaceLoop fuel a heapSize := by induction fuel generalizing a heapSize with | zero => rfl | succ fuel ih => cases heapSize with | zero => rfl | succ heapSize => cases heapSize with | zero => rfl | succ newHeapSize => simp only [arrayHeapSortInPlaceLoopWithCost, arrayHeapSortInPlaceLoop] rw [ih, arrayHeapSortStepWithCost_result]

A fuelled shrinking run has a coarse rectangular control-step envelope.

theorem arrayHeapSortInPlaceLoopWithCost_cost_le (fuel : Nat) (a : List Nat) (heapSize : Nat) : (arrayHeapSortInPlaceLoopWithCost fuel a heapSize).2 ≤ fuel * (heapSize + 1) := by induction fuel generalizing a heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ fuel ih => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ newHeapSize => simp only [arrayHeapSortInPlaceLoopWithCost] have hstep := arrayHeapSortStepWithCost_cost_le_heapSize a (newHeapSize + 2) have hrest := ih (arrayHeapSortStepWithCost a (newHeapSize + 2)).1 (newHeapSize + 1) have hsum := Nat.add_le_add hstep hrest calc (arrayHeapSortStepWithCost a (newHeapSize + 2)).2 + (arrayHeapSortInPlaceLoopWithCost fuel (arrayHeapSortStepWithCost a (newHeapSize + 2)).1 (newHeapSize + 1)).2 ≤ (newHeapSize + 2) + fuel * (newHeapSize + 2) := hsum _ ≤ (fuel + 1) * (newHeapSize + 2 + 1) := by nlinarith

Top-level heapsort execution paired with build and extraction-step costs.

def arrayHeapSortInPlaceWithCost (xs : List Nat) : List Nat × Nat := let built := arrayBuildMaxHeapWithCost xs let sorted := arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length (sorted.1, built.2 + sorted.2)

Erasing the top-level cost recovers the existing in-place heapsort.

theorem arrayHeapSortInPlaceWithCost_result (xs : List Nat) : (arrayHeapSortInPlaceWithCost xs).1 = arrayHeapSortInPlace xs := by unfold arrayHeapSortInPlaceWithCost arrayHeapSortInPlace rw [arrayHeapSortInPlaceLoopWithCost_result, arrayBuildMaxHeapWithCost_result]

Concrete control-step envelopes

Linear envelope for the visited frames of one fuelled heapify run.

def maxHeapifyControlBound (n : Nat) : Nat := n

Coarse quadratic envelope for bottom-up heap construction.

def buildMaxHeapControlBound (n : Nat) : Nat := n * n

Coarse quadratic envelope for heap construction plus all extraction steps.

def heapSortControlBound (n : Nat) : Nat := 2 * n * n + n

The fuel bound on heapify is exactly its named linear envelope.

theorem maxHeapifyFuelWithCost_cost_le_controlBound (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (maxHeapifyFuelWithCost fuel a heapSize i).2 ≤ maxHeapifyControlBound fuel := by simpa [maxHeapifyControlBound] using maxHeapifyFuelWithCost_cost_le_fuel fuel a heapSize i

A costed bottom-up build is bounded by the named quadratic envelope.

theorem arrayBuildMaxHeapWithCost_cost_le (xs : List Nat) : (arrayBuildMaxHeapWithCost xs).2 ≤ buildMaxHeapControlBound xs.length := by unfold arrayBuildMaxHeapWithCost buildMaxHeapControlBound exact (buildMaxHeapLoopWithCost_cost_le (xs.length / 2) xs xs.length).trans (Nat.mul_le_mul_right xs.length (Nat.div_le_self xs.length 2))

A full costed heapsort run is bounded by the named quadratic envelope.

theorem arrayHeapSortInPlaceWithCost_cost_le (xs : List Nat) : (arrayHeapSortInPlaceWithCost xs).2 ≤ heapSortControlBound xs.length := by let built := arrayBuildMaxHeapWithCost xs have hbuiltLength : built.1.length = xs.length := by rw [show built.1 = arrayBuildMaxHeap xs by simpa [built] using arrayBuildMaxHeapWithCost_result xs] exact (arrayBuildMaxHeap_correct xs).2.2 have hbuild : built.2 ≤ xs.length * xs.length := by simpa [built, buildMaxHeapControlBound] using arrayBuildMaxHeapWithCost_cost_le xs have hloopRaw := arrayHeapSortInPlaceLoopWithCost_cost_le (built.1.length - 1) built.1 built.1.length have hloop : (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ xs.length * (xs.length + 1) := by calc (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ (built.1.length - 1) * (built.1.length + 1) := hloopRaw _ = (xs.length - 1) * (xs.length + 1) := by rw [hbuiltLength] _ ≤ xs.length * (xs.length + 1) := Nat.mul_le_mul_right (xs.length + 1) (Nat.sub_le xs.length 1) unfold arrayHeapSortInPlaceWithCost change built.2 + (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ heapSortControlBound xs.length calc built.2 + (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ xs.length * xs.length + xs.length * (xs.length + 1) := Nat.add_le_add hbuild hloop _ = heapSortControlBound xs.length := by unfold heapSortControlBound ring

The costed run is a sorted permutation and satisfies its concrete envelope.

theorem arrayHeapSortInPlaceWithCost_correct_and_cost (xs : List Nat) : OrderedAsc (arrayHeapSortInPlaceWithCost xs).1 ∧ (arrayHeapSortInPlaceWithCost xs).1.Perm xs ∧ (arrayHeapSortInPlaceWithCost xs).2 ≤ heapSortControlBound xs.length := by rw [arrayHeapSortInPlaceWithCost_result] exact ⟨arrayHeapSortInPlace_orderedAsc xs, arrayHeapSortInPlace_perm xs, arrayHeapSortInPlaceWithCost_cost_le xs⟩

Honest asymptotic wrappers for the coarse envelopes

The linear heapify control envelope is O(n).

theorem maxHeapifyControlBound_isBigO_n : isBigO (fun n : Nat => (maxHeapifyControlBound n : ℝ)) (fun n : Nat => (n : ℝ)) := by rw [isBigO_iff] refine ⟨1, by norm_num, 1, fun n _ => ?_⟩ simp [maxHeapifyControlBound]

The coarse build-heap control envelope is O(n²).

theorem buildMaxHeapControlBound_isBigO_nsq : isBigO (fun n : Nat => (buildMaxHeapControlBound n : ℝ)) (fun n : Nat => (n : ℝ) * n) := by rw [isBigO_iff] refine ⟨1, by norm_num, 1, fun n _ => ?_⟩ simp [buildMaxHeapControlBound, Nat.cast_mul]

The coarse heapsort control envelope is O(n²).

theorem heapSortControlBound_isBigO_nsq : isBigO (fun n : Nat => (heapSortControlBound n : ℝ)) (fun n : Nat => (n : ℝ) * n) := by rw [isBigO_iff] refine ⟨3, by norm_num, 1, fun n hn => ?_⟩ simp only [heapSortControlBound, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)] have hnReal : (1 : ℝ) ≤ n := by exact_mod_cast hn have hnNonneg : (0 : ℝ) ≤ n := by positivity nlinarith [mul_nonneg hnNonneg (sub_nonneg.mpr hnReal)]

Tight textbook cost bounds

The coarse envelopes above are regression bounds only. This section charges the same unit control-step metric (visited MAX-HEAPIFY frames plus one swap transition per nontrivial heapsort extraction) and proves the tight algorithm-level bounds: each heapify run is logarithmic in the heap segment, the bottom-up build is linear in aggregate, and the connected heapsort execution is O(n log n).

Height of node i in a heapSize-cell array heap, bounded by ⌊log₂ heapSize⌋ - ⌊log₂ (i + 1)⌋. A leaf node (no in-heap children) has height zero.

def heapHeight (heapSize i : Nat) : Nat := Nat.log 2 heapSize - Nat.log 2 (i + 1)

Node height never exceeds ⌊log₂ heapSize⌋.

theorem heapHeight_le_log (heapSize i : Nat) : heapHeight heapSize i ≤ Nat.log 2 heapSize := by simp [heapHeight]
private lemma sub_add_one_le_sub (X Y Z : Nat) (h1 : Y + 1 ≤ Z) (h2 : Z ≤ X) : X - Z + 1 ≤ X - Y := by omega

Moving from i to a child index j ≥ 2·i + 1 drops the node height by one.

theorem heapHeight_child_add_one_le {heapSize i j : Nat} (hchild : 2 * i + 1 ≤ j) (hj : j < heapSize) : heapHeight heapSize j + 1 ≤ heapHeight heapSize i := by have hlog_child : Nat.log 2 (i + 1) + 1 ≤ Nat.log 2 (j + 1) := by have hmul : 2 * (i + 1) ≤ j + 1 := by omega have hlogmul : Nat.log 2 (2 * (i + 1)) ≤ Nat.log 2 (j + 1) := Nat.log_mono_right hmul have hlog2 : Nat.log 2 (2 * (i + 1)) = Nat.log 2 (i + 1) + 1 := by rw [Nat.mul_comm 2 (i + 1)] exact Nat.log_mul_base (by norm_num) (by omega) rwa [hlog2] at hlogmul have hlog_le : Nat.log 2 (j + 1) ≤ Nat.log 2 heapSize := Nat.log_mono_right (by omega) simpa [heapHeight] using sub_add_one_le_sub (Nat.log 2 heapSize) (Nat.log 2 (i + 1)) (Nat.log 2 (j + 1)) hlog_child hlog_le

A fuelled heapify run visits at most one frame per level of the subtree rooted at i: every swap moves to a child index, which at least doubles i + 1. This is the CLRS observation that MAX-HEAPIFY runs in time proportional to the node's height.

theorem maxHeapifyFuelWithCost_cost_le_height (fuel : Nat) (a : List Nat) (heapSize i : Nat) (hi : i < heapSize) : (maxHeapifyFuelWithCost fuel a heapSize i).2 ≤ heapHeight heapSize i + 1 := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuelWithCost] | succ fuel ih => simp only [maxHeapifyFuelWithCost] split_ifs with hmax · omega · have hlargest : maxChildIndex a heapSize i < heapSize := maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) (i := i) hi have hchild := ih (swapAt a i (maxChildIndex a heapSize i)) (maxChildIndex a heapSize i) hlargest have hge : 2 * i + 1 ≤ maxChildIndex a heapSize i := by rcases maxChildIndex_eq_left_or_right_of_ne (a := a) (heapSize := heapSize) (i := i) hmax with h | h · rw [h] unfold left omega · rw [h] unfold right omega have hdrop := heapHeight_child_add_one_le (i := i) (j := maxChildIndex a heapSize i) hge hlargest omega

On a valid heap index, a heapify run costs at most ⌊log₂ heapSize⌋ + 1 control steps. This is the logarithmic MAX-HEAPIFY bound.

theorem maxHeapifyFuelWithCost_cost_le_log (fuel : Nat) (a : List Nat) (heapSize i : Nat) (hi : i < heapSize) : (maxHeapifyFuelWithCost fuel a heapSize i).2 ≤ Nat.log 2 heapSize + 1 := by have h := maxHeapifyFuelWithCost_cost_le_height fuel a heapSize i hi exact h.trans (Nat.add_le_add_right (heapHeight_le_log heapSize i) 1)

Linear aggregate build bound

A level h strictly below node i witnesses 2 ^ h * (i + 1) ≤ heapSize.

theorem pow_two_mul_le_of_lt_heapHeight {heapSize i h : Nat} (hi : i < heapSize) (hlt : h < heapHeight heapSize i) : 2 ^ h * (i + 1) ≤ heapSize := by have hlog_le : Nat.log 2 (i + 1) ≤ Nat.log 2 heapSize := Nat.log_mono_right (by omega) have h_add : h + Nat.log 2 (i + 1) < Nat.log 2 heapSize := by unfold heapHeight at hlt omega have hpow_succ : h + Nat.log 2 (i + 1) + 1 ≤ Nat.log 2 heapSize := by omega have hself : i + 1 ≤ 2 ^ (Nat.log 2 (i + 1) + 1) := Nat.le_of_lt (Nat.lt_pow_succ_log_self (by norm_num) (i + 1)) have hmul_le : 2 ^ h * (i + 1) ≤ 2 ^ (h + Nat.log 2 (i + 1) + 1) := by calc 2 ^ h * (i + 1) ≤ 2 ^ h * 2 ^ (Nat.log 2 (i + 1) + 1) := Nat.mul_le_mul_left (2 ^ h) hself _ = 2 ^ (h + Nat.log 2 (i + 1) + 1) := by rw [← pow_add] rfl have hpow_n : 2 ^ (h + Nat.log 2 (i + 1) + 1) ≤ heapSize := by exact (Nat.pow_le_pow_right (by norm_num : 0 < 2) hpow_succ).trans (Nat.pow_log_le_self 2 (by omega : heapSize ≠ 0)) exact Nat.le_trans hmul_le hpow_n

Every node of height exceeding h lies below index heapSize / 2 ^ h.

theorem mem_range_div_pow_of_lt_heapHeight {heapSize i h : Nat} (hi : i < heapSize) (hlt : h < heapHeight heapSize i) : i < heapSize / 2 ^ h := by have hpow := pow_two_mul_le_of_lt_heapHeight hi hlt have hi1 : i + 1 ≤ heapSize / 2 ^ h := by rw [Nat.le_div_iff_mul_le (Nat.pow_pos (by norm_num))] rwa [Nat.mul_comm] omega

At most heapSize / 2 ^ h nodes have height strictly exceeding h.

theorem card_lt_heapHeight_le (heapSize h : Nat) : ({i ∈ Finset.range heapSize | h < heapHeight heapSize i}.card) ≤ heapSize / 2 ^ h := by have hsub : {i ∈ Finset.range heapSize | h < heapHeight heapSize i} ⊆ Finset.range (heapSize / 2 ^ h) := by intro i hi have hi' : i < heapSize := Finset.mem_range.mp (Finset.mem_filter.mp hi).1 have hlt : h < heapHeight heapSize i := (Finset.mem_filter.mp hi).2 exact Finset.mem_range.mpr (mem_range_div_pow_of_lt_heapHeight hi' hlt) simpa [Finset.card_range] using Finset.card_le_card hsub

A node's height is the number of levels strictly below it.

theorem heapHeight_eq_sum_levels (heapSize i : Nat) : heapHeight heapSize i = ∑ h ∈ Finset.range (Nat.log 2 heapSize + 1), if h < heapHeight heapSize i then 1 else 0 := by rw [← Finset.card_filter (fun h => h < heapHeight heapSize i) (Finset.range (Nat.log 2 heapSize + 1))] have hfilter : {h ∈ Finset.range (Nat.log 2 heapSize + 1) | h < heapHeight heapSize i} = Finset.range (heapHeight heapSize i) := by ext h simp only [Finset.mem_filter, Finset.mem_range] constructor · intro hmem exact hmem.2 · intro hlt have hle := heapHeight_le_log heapSize i exact ⟨Nat.lt_of_lt_of_le hlt (by omega), hlt⟩ rw [hfilter, Finset.card_range]
private lemma sub_add_le_sub_of_two_add_le (a x y : Nat) (hy : y ≤ a) (hxy : x + x ≤ y) : (a - y) + x ≤ a - x := by omega

Geometric tail: Σ_{h < m} heapSize / 2 ^ h ≤ 2 * heapSize.

theorem sum_div_pow_two_le (heapSize m : Nat) : (∑ h ∈ Finset.range m, heapSize / 2 ^ h) ≤ 2 * heapSize := by cases m with | zero => simp | succ k => have hstrong : (∑ h ∈ Finset.range (k + 1), heapSize / 2 ^ h) ≤ 2 * heapSize - heapSize / 2 ^ k := by induction k with | zero => simp omega | succ k ih => rw [Finset.sum_range_succ] have hle : heapSize / 2 ^ (k + 1) + heapSize / 2 ^ (k + 1) ≤ heapSize / 2 ^ k := by have hdiv : heapSize / 2 ^ (k + 1) = heapSize / 2 ^ k / 2 := by rw [pow_succ] rw [Nat.div_div_eq_div_mul] rw [hdiv] simpa [two_mul] using Nat.mul_div_le (heapSize / 2 ^ k) 2 calc (∑ h ∈ Finset.range (k + 1), heapSize / 2 ^ h) + heapSize / 2 ^ (k + 1) ≤ (2 * heapSize - heapSize / 2 ^ k) + heapSize / 2 ^ (k + 1) := Nat.add_le_add_right ih _ _ ≤ 2 * heapSize - heapSize / 2 ^ (k + 1) := by have hy : heapSize / 2 ^ k ≤ 2 * heapSize := Nat.le_trans (Nat.div_le_self heapSize (2 ^ k)) (by omega) exact sub_add_le_sub_of_two_add_le (2 * heapSize) (heapSize / 2 ^ (k + 1)) (heapSize / 2 ^ k) hy hle exact hstrong.trans (Nat.sub_le (2 * heapSize) (heapSize / 2 ^ k))

Summing node heights over a heap is at most 2 * heapSize (the CLRS double-counting argument for linear BUILD-MAX-HEAP).

theorem sum_heapHeight_le (heapSize : Nat) : (∑ i ∈ Finset.range heapSize, heapHeight heapSize i) ≤ 2 * heapSize := by calc (∑ i ∈ Finset.range heapSize, heapHeight heapSize i) = ∑ i ∈ Finset.range heapSize, ∑ h ∈ Finset.range (Nat.log 2 heapSize + 1), if h < heapHeight heapSize i then 1 else 0 := by apply Finset.sum_congr rfl intro i hi exact heapHeight_eq_sum_levels heapSize i _ = ∑ h ∈ Finset.range (Nat.log 2 heapSize + 1), ∑ i ∈ Finset.range heapSize, if h < heapHeight heapSize i then 1 else 0 := by rw [Finset.sum_comm] _ = ∑ h ∈ Finset.range (Nat.log 2 heapSize + 1), ({i ∈ Finset.range heapSize | h < heapHeight heapSize i}.card) := by apply Finset.sum_congr rfl intro h hh exact (Finset.card_filter (fun i => h < heapHeight heapSize i) (Finset.range heapSize)).symm _ ≤ ∑ h ∈ Finset.range (Nat.log 2 heapSize + 1), heapSize / 2 ^ h := by apply Finset.sum_le_sum intro h hh exact card_lt_heapHeight_le heapSize h _ ≤ 2 * heapSize := sum_div_pow_two_le heapSize (Nat.log 2 heapSize + 1)

The bottom-up build loop's cost is the sum of per-node heapify costs.

theorem buildMaxHeapLoopWithCost_cost_le_height_sum (count : Nat) (a : List Nat) (heapSize : Nat) (hcount : count ≤ heapSize) : (buildMaxHeapLoopWithCost count a heapSize).2 ≤ ∑ j ∈ Finset.range count, (heapHeight heapSize j + 1) := by induction count generalizing a with | zero => simp [buildMaxHeapLoopWithCost] | succ count ih => simp only [buildMaxHeapLoopWithCost] have hrepair : (maxHeapifyFuelWithCost heapSize a heapSize count).2 ≤ heapHeight heapSize count + 1 := maxHeapifyFuelWithCost_cost_le_height heapSize a heapSize count (by omega) have hrest := ih (maxHeapifyFuelWithCost heapSize a heapSize count).1 (by omega) rw [Finset.sum_range_succ] simpa [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm] using Nat.add_le_add hrepair hrest

Restricting the per-node height sum to a shorter prefix only decreases it.

theorem sum_heapHeight_range_mono {n m : Nat} (h : n ≤ m) : (∑ j ∈ Finset.range n, (heapHeight m j + 1)) ≤ ∑ j ∈ Finset.range m, (heapHeight m j + 1) := by have hsub : Finset.range n ⊆ Finset.range m := by intro x hx exact Finset.mem_range.mpr (Nat.lt_of_lt_of_le (Finset.mem_range.mp hx) h) exact Finset.sum_le_sum_of_subset_of_nonneg hsub (by intro x hx2 hx1; omega)

Bottom-up heap construction charges at most 3 * heapSize control steps.

theorem buildMaxHeapLoopWithCost_cost_le_linear (count : Nat) (a : List Nat) (heapSize : Nat) (hcount : count ≤ heapSize) : (buildMaxHeapLoopWithCost count a heapSize).2 ≤ 3 * heapSize := by have hsum := buildMaxHeapLoopWithCost_cost_le_height_sum count a heapSize hcount have hsum_sub := sum_heapHeight_range_mono (n := count) (m := heapSize) hcount have htotal : (∑ j ∈ Finset.range heapSize, (heapHeight heapSize j + 1)) ≤ 3 * heapSize := by calc (∑ j ∈ Finset.range heapSize, (heapHeight heapSize j + 1)) = (∑ j ∈ Finset.range heapSize, heapHeight heapSize j) + heapSize := by rw [Finset.sum_add_distrib] simp [Finset.card_range] _ ≤ 2 * heapSize + heapSize := Nat.add_le_add_right (sum_heapHeight_le heapSize) heapSize _ = 3 * heapSize := by omega exact hsum.trans (hsum_sub.trans htotal)

Named linear envelope for bottom-up heap construction.

def buildMaxHeapLinearBound (n : Nat) : Nat := 3 * n

The costed builder satisfies the named linear envelope.

theorem arrayBuildMaxHeapWithCost_cost_le_linear (xs : List Nat) : (arrayBuildMaxHeapWithCost xs).2 ≤ buildMaxHeapLinearBound xs.length := by unfold arrayBuildMaxHeapWithCost buildMaxHeapLinearBound exact buildMaxHeapLoopWithCost_cost_le_linear (xs.length / 2) xs xs.length (Nat.div_le_self xs.length 2)

O(n log n) heapsort bound

A single extraction step costs at most ⌊log₂ heapSize⌋ + 2 control steps.

theorem arrayHeapSortStepWithCost_cost_le_log (a : List Nat) (heapSize : Nat) : (arrayHeapSortStepWithCost a heapSize).2 ≤ Nat.log 2 heapSize + 2 := by cases heapSize with | zero => simp [arrayHeapSortStepWithCost] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortStepWithCost] | succ newHeapSize => have hh := maxHeapifyFuelWithCost_cost_le_log (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0 (by omega) have hmono : Nat.log 2 (newHeapSize + 1) ≤ Nat.log 2 (newHeapSize + 2) := Nat.log_mono_right (by omega) simpa [arrayHeapSortStepWithCost] using (calc (maxHeapifyFuelWithCost (newHeapSize + 1) (swapAt a 0 (newHeapSize + 1)) (newHeapSize + 1) 0).2 + 1 ≤ (Nat.log 2 (newHeapSize + 1) + 1) + 1 := Nat.add_le_add_right hh 1 _ = Nat.log 2 (newHeapSize + 1) + 2 := by omega _ ≤ Nat.log 2 (newHeapSize + 2) + 2 := Nat.add_le_add_right hmono 2)

The shrinking heapsort loop charges at most fuel * (⌊log₂ heapSize⌋ + 2) control steps.

theorem arrayHeapSortInPlaceLoopWithCost_cost_le_log (fuel : Nat) (a : List Nat) (heapSize : Nat) : (arrayHeapSortInPlaceLoopWithCost fuel a heapSize).2 ≤ fuel * (Nat.log 2 heapSize + 2) := by induction fuel generalizing a heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ fuel ih => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ heapSize => cases heapSize with | zero => simp [arrayHeapSortInPlaceLoopWithCost] | succ newHeapSize => simp only [arrayHeapSortInPlaceLoopWithCost] have hstep := arrayHeapSortStepWithCost_cost_le_log a (newHeapSize + 2) have hrest := ih (arrayHeapSortStepWithCost a (newHeapSize + 2)).1 (newHeapSize + 1) have hmono : Nat.log 2 (newHeapSize + 1) + 2 ≤ Nat.log 2 (newHeapSize + 2) + 2 := Nat.add_le_add_right (Nat.log_mono_right (by omega)) 2 have hrest' : (arrayHeapSortInPlaceLoopWithCost fuel (arrayHeapSortStepWithCost a (newHeapSize + 2)).1 (newHeapSize + 1)).2 ≤ fuel * (Nat.log 2 (newHeapSize + 2) + 2) := hrest.trans (Nat.mul_le_mul_left fuel hmono) calc (arrayHeapSortStepWithCost a (newHeapSize + 2)).2 + (arrayHeapSortInPlaceLoopWithCost fuel (arrayHeapSortStepWithCost a (newHeapSize + 2)).1 (newHeapSize + 1)).2 ≤ (Nat.log 2 (newHeapSize + 2) + 2) + fuel * (Nat.log 2 (newHeapSize + 2) + 2) := Nat.add_le_add hstep hrest' _ = (fuel + 1) * (Nat.log 2 (newHeapSize + 2) + 2) := by ring

Named O(n log n) envelope for the full costed heapsort execution.

def heapSortNLogNBound (n : Nat) : Nat := n * Nat.log 2 n + 5 * n

The full costed heapsort run satisfies the named O(n log n) envelope.

theorem arrayHeapSortInPlaceWithCost_cost_le_log (xs : List Nat) : (arrayHeapSortInPlaceWithCost xs).2 ≤ heapSortNLogNBound xs.length := by let built := arrayBuildMaxHeapWithCost xs have hbuiltLength : built.1.length = xs.length := by rw [show built.1 = arrayBuildMaxHeap xs by simpa [built] using arrayBuildMaxHeapWithCost_result xs] exact (arrayBuildMaxHeap_correct xs).2.2 have hbuild : built.2 ≤ 3 * xs.length := by simpa [built, buildMaxHeapLinearBound] using arrayBuildMaxHeapWithCost_cost_le_linear xs have hloopRaw := arrayHeapSortInPlaceLoopWithCost_cost_le_log (built.1.length - 1) built.1 built.1.length have hloop : (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ xs.length * (Nat.log 2 xs.length + 2) := by calc (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ (built.1.length - 1) * (Nat.log 2 built.1.length + 2) := hloopRaw _ = (xs.length - 1) * (Nat.log 2 xs.length + 2) := by rw [hbuiltLength] _ ≤ xs.length * (Nat.log 2 xs.length + 2) := Nat.mul_le_mul_right (Nat.log 2 xs.length + 2) (Nat.sub_le xs.length 1) unfold arrayHeapSortInPlaceWithCost change built.2 + (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ heapSortNLogNBound xs.length calc built.2 + (arrayHeapSortInPlaceLoopWithCost (built.1.length - 1) built.1 built.1.length).2 ≤ 3 * xs.length + xs.length * (Nat.log 2 xs.length + 2) := Nat.add_le_add hbuild hloop _ = heapSortNLogNBound xs.length := by unfold heapSortNLogNBound ring

Sortedness, permutation, and the tight O(n log n) envelope together.

theorem arrayHeapSortInPlaceWithCost_correct_and_log_cost (xs : List Nat) : OrderedAsc (arrayHeapSortInPlaceWithCost xs).1 ∧ (arrayHeapSortInPlaceWithCost xs).1.Perm xs ∧ (arrayHeapSortInPlaceWithCost xs).2 ≤ heapSortNLogNBound xs.length := by rw [arrayHeapSortInPlaceWithCost_result] exact ⟨arrayHeapSortInPlace_orderedAsc xs, arrayHeapSortInPlace_perm xs, arrayHeapSortInPlaceWithCost_cost_le_log xs⟩

Honest asymptotic wrappers for the tight bounds

Named O(log n) envelope for a root MAX-HEAPIFY run.

def maxHeapifyLogBound (n : Nat) : Nat := Nat.log 2 n + 1

The logarithmic heapify envelope is O(log n).

theorem maxHeapifyLogBound_isBigO_log : isBigO (fun n : Nat => (maxHeapifyLogBound n : ℝ)) (fun n : Nat => (Nat.log 2 n : ℝ)) := by rw [isBigO_iff] refine ⟨2, by norm_num, 2, fun n hn => ?_⟩ have hnlog : 1 ≤ Nat.log 2 n := Nat.log_pos (by norm_num : 1 < 2) (by omega : 2 ≤ n) simp only [maxHeapifyLogBound, Nat.cast_add, Nat.cast_one] rw [abs_of_nonneg (by positivity : 0 ≤ (Nat.log 2 n : ℝ) + 1), abs_of_nonneg (by positivity : 0 ≤ (Nat.log 2 n : ℝ))] have hnat : Nat.log 2 n + 1 ≤ 2 * Nat.log 2 n := by omega exact_mod_cast hnat

The linear build-heap envelope is O(n).

theorem buildMaxHeapLinearBound_isBigO_n : isBigO (fun n : Nat => (buildMaxHeapLinearBound n : ℝ)) (fun n : Nat => (n : ℝ)) := by rw [isBigO_iff] refine ⟨3, by norm_num, 0, fun n _ => ?_⟩ simp [buildMaxHeapLinearBound, Nat.cast_mul, abs_of_nonneg]

The O(n log n) heapsort envelope is indeed O(n log n).

theorem heapSortNLogNBound_isBigO_nlogn : isBigO (fun n : Nat => (heapSortNLogNBound n : ℝ)) (fun n : Nat => (n : ℝ) * (Nat.log 2 n : ℝ)) := by rw [isBigO_iff] refine ⟨6, by norm_num, 2, fun n hn => ?_⟩ have hlog : (1 : ℝ) ≤ (Nat.log 2 n : ℝ) := by exact_mod_cast (Nat.log_pos (by norm_num : 1 < 2) (by omega : 2 ≤ n)) simp only [heapSortNLogNBound, Nat.cast_add, Nat.cast_mul] rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)] have hn' : (0 : ℝ) ≤ n := by positivity have hmul : (n : ℝ) ≤ (n : ℝ) * (Nat.log 2 n : ℝ) := by calc (n : ℝ) = 1 * (n : ℝ) := by ring _ ≤ (Nat.log 2 n : ℝ) * (n : ℝ) := mul_le_mul_of_nonneg_right hlog hn' _ = (n : ℝ) * (Nat.log 2 n : ℝ) := by ring have h5 : 5 * (n : ℝ) ≤ 5 * ((n : ℝ) * (Nat.log 2 n : ℝ)) := mul_le_mul_of_nonneg_left hmul (by norm_num) calc (n : ℝ) * (Nat.log 2 n : ℝ) + 5 * (n : ℝ) ≤ (n : ℝ) * (Nat.log 2 n : ℝ) + 5 * ((n : ℝ) * (Nat.log 2 n : ℝ)) := add_le_add_right h5 ((n : ℝ) * (Nat.log 2 n : ℝ)) _ = 6 * ((n : ℝ) * (Nat.log 2 n : ℝ)) := by ring
end Chapter06end CLRS