CLRS-Lean
Chapter 6. Heapsort

Imports

import CLRSLean.Chapter_06.Section_06_1_Heaps
import CLRSLean.Chapter_06.Section_06_2_Maintaining_Heap_Property
import CLRSLean.Chapter_06.Section_06_3_Building_A_Heap
import CLRSLean.Chapter_06.Section_06_4_Heapsort
import CLRSLean.Chapter_06.Section_06_5_Priority_Queues

Chapter 6 - Heapsort

Chapter 6 introduces heaps, the heapsort algorithm, and max-priority queues. The current CLRS-Lean pass has two layers. The compact functional layer remains as a small mathematical scaffold for sortedness and permutation facts. The reader-facing array layer now contains the zero-based CLRS child/parent formulas, an indexed heap predicate, MAX-HEAPIFY's recursive repair theorem, bottom-up BUILD-MAX-HEAP by repeated heapify, the executable in-place HEAPSORT loop with a proved sorted-suffix invariant and sortedness theorem, and the array-level HEAP-MAXIMUM theorem.

Sections

6.1 Heaps: proved for the indexed heap predicate and root maximum. Main results: CLRS.Chapter06.parent_lt_self, CLRS.Chapter06.eq_left_or_right_parent, CLRS.Chapter06.ArrayMaxHeap.getElem_le_root, and CLRS.Chapter06.orderedDesc_arrayMaxHeap; localized predicates: CLRS.Chapter06.ArrayMaxHeapFrom.to_global and CLRS.Chapter06.ArrayMaxHeapExceptFrom.to_global.
6.2 Maintaining the heap property: proved for fuelled MAX-HEAPIFY recursive repair. Main results: CLRS.Chapter06.swapAt_perm, CLRS.Chapter06.maxHeapifyFuel_perm, CLRS.Chapter06.maxHeapifyFuel_valAt_of_heapSize_le, and CLRS.Chapter06.arrayMaxHeap_of_except_of_maxChildIndex_self; recursive repair: CLRS.Chapter06.maxHeapifyFuel_child_repair_after_swap, CLRS.Chapter06.maxHeapifyFuel_swap_branch_repair, CLRS.Chapter06.maxHeapifyFuel_repair_subtree and CLRS.Chapter06.maxHeapifyFuel_root_isMaxHeap.
6.3 Building a heap: proved for the bottom-up repeated MAX-HEAPIFY builder. Main results: CLRS.Chapter06.ArrayMaxHeapFrom.of_half, CLRS.Chapter06.buildMaxHeapLoop_isMaxHeap, CLRS.Chapter06.buildMaxHeapLoop_perm, CLRS.Chapter06.arrayBuildMaxHeap_isMaxHeap and CLRS.Chapter06.arrayBuildMaxHeap_correct.
6.4 The heapsort algorithm: proved for the in-place CLRS loop refinement. Loop facts: CLRS.Chapter06.arrayHeapSortInPlaceLoop_length, CLRS.Chapter06.arrayHeapSortInPlaceLoop_perm, CLRS.Chapter06.arrayHeapSortInPlace_length, and CLRS.Chapter06.arrayHeapSortInPlace_perm; invariant facts: CLRS.Chapter06.HeapSortLoopInvariant.initial, CLRS.Chapter06.arrayHeapSortStep_suffix_head_eq_root, CLRS.Chapter06.arrayHeapSortStep_suffix_head_bounds_prefix, CLRS.Chapter06.HeapSortLoopInvariant.step, CLRS.Chapter06.arrayHeapSortStep_state_correct, CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_shrink_invariant, CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlaceLoop_terminal_invariant, and CLRS.Chapter06.arrayHeapSortInPlaceLoop_orderedAsc; state package: CLRS.Chapter06.arrayHeapSortInPlaceLoop_state_correct and CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_state_correct. Main specification results: CLRS.Chapter06.arrayHeapSortInPlace_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlace_orderedAsc, CLRS.Chapter06.arrayHeapSortInPlace_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_exact_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_correct, CLRS.Chapter06.arrayHeapSort_eq_arrayHeapSortInPlace, CLRS.Chapter06.arrayHeapSort_terminal_invariant, CLRS.Chapter06.arrayHeapSort_state_correct, CLRS.Chapter06.arrayHeapSort_exact_state_correct, and CLRS.Chapter06.arrayHeapSort_correct.
6.5 Priority queues: proved for the functional heap interface, with array-level HEAP-MAXIMUM, full fuelled HEAP-INCREASE-KEY, HEAP-EXTRACT-MAX, and HEAP-DELETE state theorems. Main results: CLRS.Chapter06.heapInsert_orderedDesc, CLRS.Chapter06.heapInsert_perm, CLRS.Chapter06.heapIncreaseKey_orderedDesc, and CLRS.Chapter06.heapDelete_orderedDesc; array result: CLRS.Chapter06.arrayHeapMaximum?_max, CLRS.Chapter06.ArrayMaxHeap.set_increased_except_up, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubble_step, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubbleUpFuel_global, CLRS.Chapter06.arrayHeapIncreaseKey?_state_correct, CLRS.Chapter06.arrayHeapIncreaseKeyNoBubble?_state_correct, CLRS.Chapter06.arrayHeapExtractMax?_state_correct, and CLRS.Chapter06.arrayHeapDelete?_state_correct.

Current Gaps

Runtime/RAM semantics remain refinement targets.

              namespace CLRSnamespace Chapter06end Chapter06end CLRS