Imports
CLRS Section 6.2 - Maintaining the Heap Property
This section isolates the executable pieces around CLRS MAX-HEAPIFY.
Main results:
-
Theorem
swapAt_perm: swapping two array cells preserves the multiset of elements. -
Theorems
valAt_swapAt_leftandvalAt_swapAt_right: after an in-bounds swap, the two exchanged cells contain each other's old values. -
Theorem
valAt_swapAt_of_ne: every non-swapped index is unchanged. -
Theorem
maxHeapifyFuel_perm: the fuelled executable heapify loop preserves the multiset of elements. -
Theorem
maxHeapifyFuel_valAt_of_heapSize_le: fuelled heapify does not change cells outside the heap prefix. -
Theorems
valAt_i_le_maxChildIndex,valAt_left_le_maxChildIndex, andvalAt_right_le_maxChildIndex: the CLRSlargestchoice is locally maximal among the root and in-heap children. -
Theorem
arrayMaxHeap_of_except_of_maxChildIndex_self: the no-swap branch ofMAX-HEAPIFYrepairs the only potentially bad parent. -
Theorem
arrayMaxHeapExceptFrom_after_swap_at_root: a nontrivial swap repairs the current parent and moves the local exception down to the selected child. -
Theorem
maxHeapifyFuel_swap_branch_repair: in the nontrivial recursive branch, swapping with the selected child and recursively heapifying repairs the original localized heap. -
Theorem
arrayMaxHeapFrom_of_maxHeapifyFuel_succ: one fuelled heapify step is correct once the recursive branch supplies the child postcondition. -
Theorem
maxHeapifyFuel_repair_subtree: enough fuel recursively repairs the localized subtree rooted ati. -
Theorem
maxHeapifyFuel_root_isMaxHeap: root heapify with enough fuel produces a global max-heap.
Remaining refinements:
-
The recursive fuelled
MAX-HEAPIFYrepair theorem is proved and consumed by Section 6.3's bottom-upBUILD-MAX-HEAPand Section 6.4's in-placeHEAPSORTloop. Later work can add a shared imperative array semantics and line-by-line runtime costs.
namespace CLRSnamespace Chapter06
Swaps and fuelled MAX-HEAPIFY
Read an array cell with fallback zero outside the list.
def valAt (a : List Nat) (i : Nat) : Nat :=
a.getD i 0
Inside bounds, valAt is the ordinary list-backed array read.
theorem valAt_eq_getElem (a : List Nat) {i : Nat} (hi : i < a.length) :
valAt a i = a[i] :=
Swap two array cells when both indices are in bounds; otherwise leave the list unchanged.
def swapAt (a : List Nat) (i j : Nat) : List Nat :=
match a[i]?, a[j]? with
| some ai, some aj => (a.set i aj).set j ai
| _, _ => aAuxiliary permutation lemma for swapping the head with a later cell.
theorem cons_set_perm_of_get? {xs : List Nat} {j x y : Nat}
(h : xs[j]? = some y) : (y :: xs.set j x).Perm (x :: xs) :=
induction xs generalizing j with
cases j with
Swapping two cells preserves list length.
theorem swapAt_length (a : List Nat) (i j : Nat) :
(swapAt a i j).length = a.length :=
Swapping two cells preserves the multiset of elements.
theorem swapAt_perm (a : List Nat) (i j : Nat) :
(swapAt a i j).Perm a :=
induction a generalizing i j with
cases i with
cases j with
cases h : xs[j]? with
cases j with
cases h : xs[i]? with
cases hi : xs[i]? with
cases hj : xs[j]? with
After an in-bounds swap, the first index contains the old value at the second.
After an in-bounds swap, the second index contains the old value at the first.
After an in-bounds swap, every index outside the swapped pair is unchanged.
Path invariant for recursive heapify. If the current bad node is below the
localized root start, the value at its parent already dominates both
children of the bad node. This is the extra fact that keeps the incoming edge
valid when the bad node swaps with its largest child.
def BadChildrenLeParent (a : List Nat) (heapSize start i : Nat) : Prop :=
start < i →
(∀ _ : left i < heapSize, valAt a (left i) ≤ valAt a (parent i)) ∧
(∀ _ : right i < heapSize, valAt a (right i) ≤ valAt a (parent i))At the localized root, the path-bound condition is vacuous.
theorem BadChildrenLeParent.self (a : List Nat) (heapSize i : Nat) :
BadChildrenLeParent a heapSize i i :=
Choose between a current largest index and a candidate child.
def largerIndex (a : List Nat) (heapSize current candidate : Nat) : Nat :=
if candidate < heapSize then
if valAt a current < valAt a candidate then candidate else current
else
current
The CLRS choice of the largest among i, left i, and right i.
def maxChildIndex (a : List Nat) (heapSize i : Nat) : Nat :=
largerIndex a heapSize (largerIndex a heapSize i (left i)) (right i)
A largerIndex result is at least the current index's key.
theorem valAt_current_le_largerIndex (a : List Nat)
(heapSize current candidate : Nat) :
valAt a current ≤ valAt a (largerIndex a heapSize current candidate) :=
If the candidate is in the heap, a largerIndex result is at least it.
theorem valAt_candidate_le_largerIndex {a : List Nat}
{heapSize current candidate : Nat} (hcandidate : candidate < heapSize) :
valAt a candidate ≤ valAt a (largerIndex a heapSize current candidate) :=
If the current index is inside the heap, the selected larger index is too.
theorem largerIndex_lt_heapSize {a : List Nat}
{heapSize current candidate : Nat} (hcurrent : current < heapSize) :
largerIndex a heapSize current candidate < heapSize :=
If the root is inside the heap, the CLRS largest index is inside too.
theorem maxChildIndex_lt_heapSize {a : List Nat} {heapSize i : Nat}
(hi : i < heapSize) : maxChildIndex a heapSize i < heapSize :=
A largerIndex call returns either the current index or the candidate.
theorem largerIndex_eq_current_or_candidate (a : List Nat)
(heapSize current candidate : Nat) :
largerIndex a heapSize current candidate = current ∨
largerIndex a heapSize current candidate = candidate :=
The CLRS largest index is one of the root, left child, or right child.
theorem maxChildIndex_eq_self_or_left_or_right (a : List Nat)
(heapSize i : Nat) :
maxChildIndex a heapSize i = i ∨
maxChildIndex a heapSize i = left i ∨
maxChildIndex a heapSize i = right i :=
If MAX-HEAPIFY swaps, the selected index is one of the two children.
theorem maxChildIndex_eq_left_or_right_of_ne {a : List Nat} {heapSize i : Nat}
(h : maxChildIndex a heapSize i ≠ i) :
maxChildIndex a heapSize i = left i ∨
maxChildIndex a heapSize i = right i :=
A swapping MAX-HEAPIFY step moves strictly down the array heap.
A nontrivial heapify step strictly decreases the remaining index distance.
theorem heapSize_sub_maxChildIndex_lt_of_ne {a : List Nat} {heapSize i : Nat}
(hi : i < heapSize) (h : maxChildIndex a heapSize i ≠ i) :
heapSize - maxChildIndex a heapSize i < heapSize - i :=
The selected CLRS largest key is at least the original root key.
theorem valAt_i_le_maxChildIndex (a : List Nat) (heapSize i : Nat) :
valAt a i ≤ valAt a (maxChildIndex a heapSize i) :=
The selected CLRS largest key is at least the left child's key.
theorem valAt_left_le_maxChildIndex {a : List Nat} {heapSize i : Nat}
(hl : left i < heapSize) :
valAt a (left i) ≤ valAt a (maxChildIndex a heapSize i) :=
The selected CLRS largest key is at least the right child's key.
theorem valAt_right_le_maxChildIndex {a : List Nat} {heapSize i : Nat}
(hr : right i < heapSize) :
valAt a (right i) ≤ valAt a (maxChildIndex a heapSize i) :=
A left child index is strictly different from its parent index.
theorem left_ne_self (i : Nat) : left i ≠ i :=
A right child index is strictly different from its parent index.
theorem right_ne_self (i : Nat) : right i ≠ i :=
After a nontrivial heapify swap, the value moved into i dominates the
old left child.
After a nontrivial heapify swap, the value moved into i dominates the
old right child.
One nontrivial MAX-HEAPIFY swap repairs the current parent and moves the
single local exception down to the selected child. This is the local
swap-branch certificate used by the recursive proof.
After a nontrivial swap, the new bad node satisfies the path-bound invariant: its children remain below the value that was moved into its parent.
Generalized one-swap certificate for recursive heapify. If the incoming path
edge is protected by BadChildrenLeParent, swapping with the selected
child moves the exception down while preserving all localized obligations from
the original start.
Fuelled executable version of MAX-HEAPIFY. Each recursive call swaps the
current root with its largest in-heap child and continues at that child.
def maxHeapifyFuel : Nat → List Nat → Nat → Nat → List Nat
| 0, a, _, _ => a
| fuel + 1, a, heapSize, i =>
let largest := maxChildIndex a heapSize i
if largest = i then
a
else
maxHeapifyFuel fuel (swapAt a i largest) heapSize largestFuelled heapify preserves list length.
theorem maxHeapifyFuel_length (fuel : Nat) (a : List Nat)
(heapSize i : Nat) :
(maxHeapifyFuel fuel a heapSize i).length = a.length :=
induction fuel generalizing a i with
Fuelled heapify preserves the multiset of elements.
theorem maxHeapifyFuel_perm (fuel : Nat) (a : List Nat)
(heapSize i : Nat) :
(maxHeapifyFuel fuel a heapSize i).Perm a :=
induction fuel generalizing a i with
Fuelled heapify only swaps cells inside the heap prefix. Therefore every cell
at an index k ≥ heapSize keeps the same value.
If a largerIndex call returns a target different from its candidate, then the
target must have been the current index. CLRS uses the same case split when
reasoning about the variable largest.
theorem largerIndex_eq_target_forces_current {a : List Nat}
{heapSize current candidate target : Nat}
(h : largerIndex a heapSize current candidate = target)
(hcandidate : candidate ≠ target) : current = target :=
If largerIndex keeps the current index and the candidate is in the heap, then
the candidate's key is no larger than the current key.
theorem largerIndex_eq_current_le {a : List Nat}
{heapSize current candidate : Nat}
(h : largerIndex a heapSize current candidate = current)
(hcandidate : candidate < heapSize) :
valAt a candidate ≤ valAt a current :=
If MAX-HEAPIFY chooses not to swap, the left-child inequality at i holds.
If MAX-HEAPIFY chooses not to swap, the right-child inequality at i holds.
No-swap correctness for MAX-HEAPIFY: if all heap edges except those outgoing
from i are already valid, and MAX-HEAPIFY leaves i in place, the entire
prefix is a max-heap.
Localized no-swap correctness for MAX-HEAPIFY: if all heap edges whose
parents lie in start ..< heapSize are already valid except possibly those
outgoing from i, and MAX-HEAPIFY does not swap at i, then the
localized heap property is fully restored.
One fuelled MAX-HEAPIFY step is correct once the recursive swap branch has
provided the postcondition for the selected child. This packages the control
flow of the recursive proof while keeping the deeper path invariant explicit.
theorem arrayMaxHeapFrom_of_maxHeapifyFuel_succ {fuel : Nat} {a : List Nat}
{heapSize start i : Nat}
(hexcept : ArrayMaxHeapExceptFrom a heapSize start i)
(hrec : ∀ _ : maxChildIndex a heapSize i ≠ i,
ArrayMaxHeapFrom
(maxHeapifyFuel fuel (swapAt a i (maxChildIndex a heapSize i))
heapSize (maxChildIndex a heapSize i))
heapSize start) :
ArrayMaxHeapFrom (maxHeapifyFuel (fuel + 1) a heapSize i) heapSize start :=
Recursive repair theorem for fuelled MAX-HEAPIFY. The proof follows the
CLRS path argument: each nontrivial swap moves the only local exception to a
strictly larger child index, and heapSize - i is enough fuel for that
strict descent.
)
Child-call form of the recursive MAX-HEAPIFY swap branch. Once
largest ≠ i, the root/child swap moves the unique exception to
largest; enough fuel for that child call repairs the original localized
heap region.
Named CLRS swap-branch theorem for MAX-HEAPIFY. If the selected
largest child differs from the current root, then one executable step
performs the root/child swap and the recursive child call repairs the localized
heap.
theorem maxHeapifyFuel_swap_branch_repair {fuel : Nat} {a : List Nat}
{heapSize start i : Nat}
(hexcept : ArrayMaxHeapExceptFrom a heapSize start i)
(hstart : start ≤ i) (hi : i < heapSize)
(hneq : maxChildIndex a heapSize i ≠ i)
(hbound : BadChildrenLeParent a heapSize start i)
(hfuel : heapSize - maxChildIndex a heapSize i ≤ fuel) :
ArrayMaxHeapFrom (maxHeapifyFuel (fuel + 1) a heapSize i) heapSize start :=
Subtree form of MAX-HEAPIFY correctness: if the localized subtree rooted
at i has at most one bad parent, enough fuel repairs that subtree.
theorem maxHeapifyFuel_repair_subtree {fuel : Nat} {a : List Nat}
{heapSize i : Nat}
(hexcept : ArrayMaxHeapExceptFrom a heapSize i i)
(hi : i < heapSize) (hfuel : heapSize - i ≤ fuel) :
ArrayMaxHeapFrom (maxHeapifyFuel fuel a heapSize i) heapSize i :=
arrayMaxHeapFrom_of_maxHeapifyFuel hexcept (Nat.le_refl i) hi
(BadChildrenLeParent.self a heapSize i) hfuel
Root form of MAX-HEAPIFY correctness: when the only possible bad parent is
the root, enough fuel produces a global max-heap.
end Chapter06end CLRS