Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 6. Heapsort
Browse chapters

Chapter 6 — Heapsort

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports
import Mathlib

6.1. Heaps

This section introduces the heap layer used by the rest of Chapter 6. It first records a compact functional heap scaffold based on descending lists, then introduces the array-indexed heap predicate and CLRS parent/child arithmetic. Lists play the role of arrays, and the CLRS indices use the ordinary zero-based formulas:

  • left child: 2 * i + 1;

  • right child: 2 * i + 2;

  • parent: (i - 1) / 2.

Main results:

  • Theorem parent_lt_self: every positive heap index has a smaller parent.

  • Theorem eq_left_or_right_parent: every positive index is either the left or right child of its parent.

  • Theorem ArrayMaxHeap.getElem_le_root: every element in an indexed max-heap prefix is bounded by the root.

  • Theorems ArrayMaxHeapFrom.to_global and ArrayMaxHeapExceptFrom.to_global: localized heap predicates bridge back to the original global predicates.

  • Theorem orderedDesc_arrayMaxHeap: the functional descending-list heap model refines the indexed max-heap predicate.

  • Theorems buildMaxHeap_orderedDesc, buildMaxHeap_perm, buildMaxHeap_max, heapSort_orderedAsc, and heapSort_perm: the compact functional heap scaffold used by later refinement wrappers.

Status: proved for the indexed heap predicate and array-heap scaffold. Executable refinements are in Sections 6.2--6.5.

namespace CLRSnamespace Chapter06

Ordered lists as functional heaps

Ascending sortedness, used for the final heapsort output.

def OrderedAsc (xs : List Nat) : Prop := xs.Pairwise (fun a b => a ≤ b)

Descending sortedness, used as the abstract max-heap invariant.

def OrderedDesc (xs : List Nat) : Prop := xs.Pairwise (fun a b => b ≤ a)

Every element of xs is at most upper.

def AllLe (upper : Nat) (xs : List Nat) : Prop := ∀ x ∈ xs, x ≤ upper

Insert an element into a descending list.

def insertDesc (x : Nat) : List Nat → List Nat | [] => [x] | y :: ys => if y ≤ x then x :: y :: ys else y :: insertDesc x ys

Build a functional max-heap by repeated descending insertion.

def buildMaxHeap : List Nat → List Nat | [] => [] | x :: xs => insertDesc x (buildMaxHeap xs)

Functional heapsort: build a max-heap, then read it from smallest to largest. For a descending-list heap this is just reverse.

def heapSort (xs : List Nat) : List Nat := (buildMaxHeap xs).reverse

Insertion and heap construction

theorem allLe_insertDesc {upper x : Nat} {xs : List Nat} (hx : x ≤ upper) (hxs : AllLe upper xs) : AllLe upper (insertDesc x xs) := by induction xs with | nil => intro z hz simp [insertDesc] at hz exact hz ▸ hx | cons y ys ih => by_cases hyx : y ≤ x · intro w hw simp [insertDesc, hyx] at hw rcases hw with rfl | hwy · exact hx · exact hxs w (by simp [hwy]) · intro w hw simp [insertDesc, hyx] at hw rcases hw with rfl | hwin · exact hxs w (by simp) · exact ih (fun z hz => hxs z (by simp [hz])) w hwin

Inserting into a descending list preserves descending order.

theorem insertDesc_orderedDesc {x : Nat} {xs : List Nat} (hxs : OrderedDesc xs) : OrderedDesc (insertDesc x xs) := by induction xs with | nil => simp [OrderedDesc, insertDesc] | cons y ys ih => by_cases hyx : y ≤ x · rcases List.pairwise_cons.mp hxs with ⟨hy_all, htail⟩ have hx_all : AllLe x (y :: ys) := by intro z hz simp at hz rcases hz with rfl | hzy · exact hyx · exact Nat.le_trans (hy_all z hzy) hyx simpa [OrderedDesc, insertDesc, hyx, AllLe] using List.Pairwise.cons (show ∀ z ∈ y :: ys, z ≤ x from hx_all) hxs · have hxy : x ≤ y := Nat.le_of_lt (Nat.lt_of_not_ge hyx) rcases List.pairwise_cons.mp hxs with ⟨hy_all, htail⟩ have hinsert : OrderedDesc (insertDesc x ys) := ih htail have hy_insert : AllLe y (insertDesc x ys) := allLe_insertDesc hxy hy_all simpa [OrderedDesc, insertDesc, hyx, AllLe] using List.Pairwise.cons (show ∀ z ∈ insertDesc x ys, z ≤ y from hy_insert) hinsert

Descending insertion preserves the elements up to permutation.

theorem insertDesc_perm (x : Nat) (xs : List Nat) : (insertDesc x xs).Perm (x :: xs) := by induction xs with | nil => simp [insertDesc] | cons y ys ih => by_cases hyx : y ≤ x · simp [insertDesc, hyx] · simpa [insertDesc, hyx] using (List.Perm.cons y ih).trans (List.Perm.swap y x ys).symm

Repeated insertion builds a descending heap.

theorem buildMaxHeap_orderedDesc (xs : List Nat) : OrderedDesc (buildMaxHeap xs) := by induction xs with | nil => simp [OrderedDesc, buildMaxHeap] | cons x xs ih => exact insertDesc_orderedDesc ih

Building the heap preserves the input elements up to permutation.

theorem buildMaxHeap_perm (xs : List Nat) : (buildMaxHeap xs).Perm xs := by induction xs with | nil => simp [buildMaxHeap] | cons x xs ih => exact (insertDesc_perm x (buildMaxHeap xs)).trans (List.Perm.cons x ih)

Heap maximum and heapsort correctness

Return the maximum element of a functional max-heap, if any.

def heapMaximum? : List Nat → Option Nat | [] => none | x :: _ => some x

Extract the maximum element and the remaining heap spine, if nonempty.

def heapExtractMax? : List Nat → Option (Nat × List Nat) | [] => none | x :: xs => some (x, xs)

The head of a nonempty descending heap bounds every element in the heap.

theorem heapMaximum?_max {h : List Nat} {m : Nat} (hord : OrderedDesc h) (hmax : heapMaximum? h = some m) : ∀ x ∈ h, x ≤ m := by cases h with | nil => simp [heapMaximum?] at hmax | cons y ys => simp [heapMaximum?] at hmax subst m intro x hx simp at hx rcases hx with rfl | htail · exact Nat.le_refl _ · exact (List.pairwise_cons.mp hord).1 x htail

The maximum of a built heap is maximal among the original input elements.

theorem buildMaxHeap_max {xs : List Nat} {m : Nat} (hmax : heapMaximum? (buildMaxHeap xs) = some m) : ∀ x ∈ xs, x ≤ m := by intro x hx have hxheap : x ∈ buildMaxHeap xs := (List.Perm.mem_iff (buildMaxHeap_perm xs)).2 hx exact heapMaximum?_max (buildMaxHeap_orderedDesc xs) hmax x hxheap

Extracting from a descending heap leaves a descending heap.

theorem heapExtractMax?_orderedDesc {h rest : List Nat} {m : Nat} (hord : OrderedDesc h) (hextract : heapExtractMax? h = some (m, rest)) : OrderedDesc rest := by cases h with | nil => simp [heapExtractMax?] at hextract | cons y ys => simp [heapExtractMax?] at hextract rcases hextract with ⟨rfl, rfl⟩ exact (List.pairwise_cons.mp hord).2

Extracting the maximum only decomposes the original heap into head and tail.

theorem heapExtractMax?_perm {h rest : List Nat} {m : Nat} (hextract : heapExtractMax? h = some (m, rest)) : h.Perm (m :: rest) := by cases h with | nil => simp [heapExtractMax?] at hextract | cons y ys => simp [heapExtractMax?] at hextract rcases hextract with ⟨rfl, rfl⟩ rfl

The element extracted from a descending heap bounds every remaining element.

theorem heapExtractMax?_max {h rest : List Nat} {m : Nat} (hord : OrderedDesc h) (hextract : heapExtractMax? h = some (m, rest)) : ∀ x ∈ rest, x ≤ m := by cases h with | nil => simp [heapExtractMax?] at hextract | cons y ys => simp [heapExtractMax?] at hextract rcases hextract with ⟨rfl, rfl⟩ exact (List.pairwise_cons.mp hord).1

Heapsort returns an ascending list.

theorem heapSort_orderedAsc (xs : List Nat) : OrderedAsc (heapSort xs) := by simpa [heapSort, OrderedAsc, OrderedDesc] using (buildMaxHeap_orderedDesc xs).reverse

Heapsort preserves the input elements up to permutation.

theorem heapSort_perm (xs : List Nat) : (heapSort xs).Perm xs := by exact (List.reverse_perm (buildMaxHeap xs)).trans (buildMaxHeap_perm xs)

CLRS array indices and heap predicate

Zero-based left-child index.

def left (i : Nat) : Nat := 2 * i + 1

Zero-based right-child index.

def right (i : Nat) : Nat := 2 * i + 2

Zero-based parent index, with parent 0 = 0 by natural subtraction.

def parent (i : Nat) : Nat := (i - 1) / 2

Every positive zero-based heap index has a strictly smaller parent.

theorem parent_lt_self {i : Nat} (hi : 0 < i) : parent i < i := by unfold parent omega

Every positive index is either the left or right child of its parent.

theorem eq_left_or_right_parent {i : Nat} (hi : 0 < i) : i = left (parent i) ∨ i = right (parent i) := by unfold parent left right omega

The parent of a left child is the original parent index.

theorem parent_left (i : Nat) : parent (left i) = i := by unfold parent left omega

The parent of a right child is the original parent index.

theorem parent_right (i : Nat) : parent (right i) = i := by unfold parent right omega

Indexed max-heap predicate over the prefix 0 ..< heapSize of a list-backed array. Every in-heap parent is at least each in-heap child.

structure ArrayMaxHeap (a : List Nat) (heapSize : Nat) : Prop where heapSize_le_length : heapSize ≤ a.length left_le : ∀ {i : Nat}, (hi : i < heapSize) → (hl : left i < heapSize) → a[left i]'(Nat.lt_of_lt_of_le hl heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length) right_le : ∀ {i : Nat}, (hi : i < heapSize) → (hr : right i < heapSize) → a[right i]'(Nat.lt_of_lt_of_le hr heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length)

The same heap predicate with one possible bad parent. This is the CLRS precondition for MAX-HEAPIFY: both child subtrees are already heaps, so every edge except the two outgoing edges from the root under repair is valid.

structure ArrayMaxHeapExcept (a : List Nat) (heapSize bad : Nat) : Prop where heapSize_le_length : heapSize ≤ a.length left_le : ∀ {i : Nat}, (hi : i < heapSize) → i ≠ bad → (hl : left i < heapSize) → a[left i]'(Nat.lt_of_lt_of_le hl heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length) right_le : ∀ {i : Nat}, (hi : i < heapSize) → i ≠ bad → (hr : right i < heapSize) → a[right i]'(Nat.lt_of_lt_of_le hr heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length)

For heapify-style proofs we use an index-suffix heap predicate. It checks all parent nodes with indices at least start, including nodes outside the descendant subtree of start. Thus it is stronger than the ordinary subtree condition. Parent indices below start are outside its obligation. This stronger invariant supports bottom-up heap construction; at start = 0 it is the global heap predicate.

Max-heap obligations restricted to parent indices start ..< heapSize.

structure ArrayMaxHeapFrom (a : List Nat) (heapSize start : Nat) : Prop where heapSize_le_length : heapSize ≤ a.length left_le : ∀ {i : Nat}, start ≤ i → (hi : i < heapSize) → (hl : left i < heapSize) → a[left i]'(Nat.lt_of_lt_of_le hl heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length) right_le : ∀ {i : Nat}, start ≤ i → (hi : i < heapSize) → (hr : right i < heapSize) → a[right i]'(Nat.lt_of_lt_of_le hr heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length)

Localized heap obligations with one parent index temporarily exempted.

structure ArrayMaxHeapExceptFrom (a : List Nat) (heapSize start bad : Nat) : Prop where heapSize_le_length : heapSize ≤ a.length left_le : ∀ {i : Nat}, start ≤ i → (hi : i < heapSize) → i ≠ bad → (hl : left i < heapSize) → a[left i]'(Nat.lt_of_lt_of_le hl heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length) right_le : ∀ {i : Nat}, start ≤ i → (hi : i < heapSize) → i ≠ bad → (hr : right i < heapSize) → a[right i]'(Nat.lt_of_lt_of_le hr heapSize_le_length) ≤ a[i]'(Nat.lt_of_lt_of_le hi heapSize_le_length)

A global heap satisfies every localized heap obligation.

theorem ArrayMaxHeap.from_start {a : List Nat} {heapSize start : Nat} (h : ArrayMaxHeap a heapSize) : ArrayMaxHeapFrom a heapSize start := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i _ hi hl exact h.left_le hi hl · intro i _ hi hr exact h.right_le hi hr

A localized heap starting at zero is the ordinary global heap predicate.

theorem ArrayMaxHeapFrom.to_global {a : List Nat} {heapSize : Nat} (h : ArrayMaxHeapFrom a heapSize 0) : ArrayMaxHeap a heapSize := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hi hl exact h.left_le (Nat.zero_le i) hi hl · intro i hi hr exact h.right_le (Nat.zero_le i) hi hr

A localized heap remains localized after forgetting one parent obligation.

theorem ArrayMaxHeapFrom.except {a : List Nat} {heapSize start bad : Nat} (h : ArrayMaxHeapFrom a heapSize start) : ArrayMaxHeapExceptFrom a heapSize start bad := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hstart hi _ hl exact h.left_le hstart hi hl · intro i hstart hi _ hr exact h.right_le hstart hi hr

Localized heap obligations may be restricted to a later start index.

theorem ArrayMaxHeapFrom.mono_start {a : List Nat} {heapSize start newStart : Nat} (h : ArrayMaxHeapFrom a heapSize start) (hle : start ≤ newStart) : ArrayMaxHeapFrom a heapSize newStart := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hnew hi hl exact h.left_le (Nat.le_trans hle hnew) hi hl · intro i hnew hi hr exact h.right_le (Nat.le_trans hle hnew) hi hr

Localized except-heap obligations may be restricted to a later start index.

theorem ArrayMaxHeapExceptFrom.mono_start {a : List Nat} {heapSize start newStart bad : Nat} (h : ArrayMaxHeapExceptFrom a heapSize start bad) (hle : start ≤ newStart) : ArrayMaxHeapExceptFrom a heapSize newStart bad := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hnew hi hbad hl exact h.left_le (Nat.le_trans hle hnew) hi hbad hl · intro i hnew hi hbad hr exact h.right_le (Nat.le_trans hle hnew) hi hbad hr

The old global-except predicate is the zero-start special case.

theorem ArrayMaxHeapExceptFrom.to_global {a : List Nat} {heapSize bad : Nat} (h : ArrayMaxHeapExceptFrom a heapSize 0 bad) : ArrayMaxHeapExcept a heapSize bad := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hi hbad hl exact h.left_le (Nat.zero_le i) hi hbad hl · intro i hi hbad hr exact h.right_le (Nat.zero_le i) hi hbad hr

A global-except heap can be weakened to any localized except heap.

theorem ArrayMaxHeapExcept.from_start {a : List Nat} {heapSize start bad : Nat} (h : ArrayMaxHeapExcept a heapSize bad) : ArrayMaxHeapExceptFrom a heapSize start bad := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i _ hi hbad hl exact h.left_le hi hbad hl · intro i _ hi hbad hr exact h.right_le hi hbad hr

A heap remains a heap after forgetting the obligations at one parent.

theorem ArrayMaxHeap.except {a : List Nat} {heapSize bad : Nat} (h : ArrayMaxHeap a heapSize) : ArrayMaxHeapExcept a heapSize bad := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro i hi _ hl exact h.left_le hi hl · intro i hi _ hr exact h.right_le hi hr

In an indexed max-heap, the root bounds every element in the heap prefix. This is the array-level proof behind CLRS HEAP-MAXIMUM.

theorem ArrayMaxHeap.getElem_le_root {a : List Nat} {heapSize : Nat} (h : ArrayMaxHeap a heapSize) {i : Nat} (hi : i < heapSize) : a[i]'(Nat.lt_of_lt_of_le hi h.heapSize_le_length) ≤ a[0]'(Nat.lt_of_lt_of_le (Nat.zero_lt_of_lt hi) h.heapSize_le_length) := by induction i using Nat.strong_induction_on with | h i ih => cases i with | zero => simp | succ k => let p := parent (Nat.succ k) have hpos : 0 < Nat.succ k := Nat.succ_pos k have hplt : p < Nat.succ k := parent_lt_self hpos have hpheap : p < heapSize := Nat.lt_trans hplt hi have hedge : a[Nat.succ k]'(Nat.lt_of_lt_of_le hi h.heapSize_le_length) ≤ a[p]'(Nat.lt_of_lt_of_le hpheap h.heapSize_le_length) := by rcases eq_left_or_right_parent hpos with hleft | hright · have hchildEq : left p = Nat.succ k := hleft.symm have hchild : left p < heapSize := by simpa [hchildEq] using hi have hle := h.left_le hpheap hchild simpa [p, hchildEq] using hle · have hchildEq : right p = Nat.succ k := hright.symm have hchild : right p < heapSize := by simpa [hchildEq] using hi have hle := h.right_le hpheap hchild simpa [p, hchildEq] using hle have hparent := ih p hplt hpheap exact Nat.le_trans hedge (by simpa using hparent)

In a descending list, a smaller index contains a value at least as large as any larger index. This bridges the first functional heap model to the indexed heap predicate used by the CLRS array layer.

theorem orderedDesc_getElem_le {xs : List Nat} (hxs : OrderedDesc xs) {i j : Nat} (hij : i < j) (hj : j < xs.length) : xs[j] ≤ xs[i] := by induction xs generalizing i j with | nil => simp at hj | cons x xs ih => cases j with | zero => omega | succ j => cases i with | zero => have hj' : j < xs.length := by simpa using hj have htailmem : xs[j] ∈ xs := List.getElem_mem hj' have hx := (List.pairwise_cons.mp hxs).1 (xs[j]'hj') htailmem simpa using hx | succ i => have htail : OrderedDesc xs := (List.pairwise_cons.mp hxs).2 have hij' : i < j := by omega have hj' : j < xs.length := by simpa using hj simpa using ih htail hij' hj'

A descending list is an indexed max-heap on any prefix.

theorem orderedDesc_arrayMaxHeap {a : List Nat} {heapSize : Nat} (hlen : heapSize ≤ a.length) (h : OrderedDesc a) : ArrayMaxHeap a heapSize := by refine ⟨hlen, ?_, ?_⟩ · intro i hi hl exact orderedDesc_getElem_le h (by simp [left]; omega) (Nat.lt_of_lt_of_le hl hlen) · intro i hi hr exact orderedDesc_getElem_le h (by simp [right]; omega) (Nat.lt_of_lt_of_le hr hlen)
end Chapter06end CLRS
Imports
import CLRSLean.FourthEdition.Chapter_06.Section_06_1_Heaps

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_left and valAt_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, and valAt_right_le_maxChildIndex: the CLRS largest choice is locally maximal among the root and in-heap children.

  • Theorem arrayMaxHeap_of_except_of_maxChildIndex_self: the no-swap branch of MAX-HEAPIFY repairs 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 heap obligations for every parent index at least i, using the stronger index-suffix precondition.

  • Theorem maxHeapifyFuel_root_isMaxHeap: root heapify with enough fuel produces a global max-heap.

Remaining refinements:

  • The recursive fuelled MAX-HEAPIFY repair theorem is proved and consumed by Section 6.3's bottom-up BUILD-MAX-HEAP and Section 6.4's in-place HEAPSORT loop. 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] := by simp [valAt, List.getElem?_eq_getElem hi]

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 | _, _ => a

Auxiliary 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) := by induction xs generalizing j with | nil => simp at h | cons z zs ih => cases j with | zero => simp at h subst y simp [List.set] exact List.Perm.swap x z zs | succ j => simp at h have ih' := ih h simp [List.set] exact ((List.Perm.swap y z (zs.set j x)).symm.trans (List.Perm.cons z ih')).trans (List.Perm.swap z x zs).symm

Swapping two cells preserves list length.

theorem swapAt_length (a : List Nat) (i j : Nat) : (swapAt a i j).length = a.length := by unfold swapAt cases a[i]? <;> cases a[j]? <;> simp

Swapping two cells preserves the multiset of elements.

theorem swapAt_perm (a : List Nat) (i j : Nat) : (swapAt a i j).Perm a := by induction a generalizing i j with | nil => simp [swapAt] | cons x xs ih => cases i with | zero => cases j with | zero => simp [swapAt] | succ j => unfold swapAt simp cases h : xs[j]? with | none => simp | some y => simpa [h, List.set] using cons_set_perm_of_get? (xs := xs) (j := j) (x := x) h | succ i => cases j with | zero => unfold swapAt simp cases h : xs[i]? with | none => simp | some y => simpa [h, List.set] using cons_set_perm_of_get? (xs := xs) (j := i) (x := x) h | succ j => cases hi : xs[i]? with | none => simp [swapAt, hi] | some ai => cases hj : xs[j]? with | none => simp [swapAt, hi, hj] | some aj => simpa [swapAt, hi, hj, List.set] using ih i j

After an in-bounds swap, the first index contains the old value at the second.

theorem valAt_swapAt_left {a : List Nat} {i j : Nat} (hi : i < a.length) (hj : j < a.length) : valAt (swapAt a i j) i = valAt a j := by by_cases hij : i = j · subst j simp [swapAt, valAt, List.getElem?_eq_getElem hi] · unfold swapAt rw [List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] simp [valAt, Ne.symm hij] rw [List.getElem?_set_self'] simp [List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj]

After an in-bounds swap, the second index contains the old value at the first.

theorem valAt_swapAt_right {a : List Nat} {i j : Nat} (hi : i < a.length) (hj : j < a.length) : valAt (swapAt a i j) j = valAt a i := by by_cases hij : i = j · subst j simp [swapAt, valAt, List.getElem?_eq_getElem hi] · unfold swapAt rw [List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] simp [valAt] rw [List.getElem?_set_self'] have hjset : j < (a.set i a[j]).length := by simpa [List.length_set] using hj simp [List.getElem?_eq_getElem hjset, List.getElem?_eq_getElem hi]

After an in-bounds swap, every index outside the swapped pair is unchanged.

theorem valAt_swapAt_of_ne {a : List Nat} {i j k : Nat} (hi : i < a.length) (hj : j < a.length) (hki : k ≠ i) (hkj : k ≠ j) : valAt (swapAt a i j) k = valAt a k := by unfold swapAt rw [List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] unfold valAt change (((a.set i a[j]).set j a[i])[k]?.getD 0 = a[k]?.getD 0) rw [List.getElem?_set] simp [show j ≠ k from Ne.symm hkj] rw [List.getElem?_set] simp [show i ≠ k from Ne.symm hki]

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 := by intro h omega

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) := by unfold largerIndex by_cases hc : candidate < heapSize · simp [hc] by_cases hlt : valAt a current < valAt a candidate · simp [hlt] exact Nat.le_of_lt hlt · simp [hlt] · simp [hc]

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) := by unfold largerIndex simp [hcandidate] by_cases hlt : valAt a current < valAt a candidate · simp [hlt] · simp [hlt] exact Nat.le_of_not_gt hlt

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 := by unfold largerIndex by_cases hc : candidate < heapSize · simp [hc] by_cases hlt : valAt a current < valAt a candidate · simp [hlt, hc] · simp [hlt, hcurrent] · simp [hc, hcurrent]

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 := by unfold maxChildIndex exact largerIndex_lt_heapSize (largerIndex_lt_heapSize hi)

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 := by unfold largerIndex by_cases hc : candidate < heapSize · simp [hc] by_cases hlt : valAt a current < valAt a candidate · simp [hlt] · simp [hlt] · simp [hc]

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 := by unfold maxChildIndex rcases largerIndex_eq_current_or_candidate a heapSize i (left i) with hleft | hleft · rcases largerIndex_eq_current_or_candidate a heapSize (largerIndex a heapSize i (left i)) (right i) with hright | hright · left simpa [hleft] using hright · right right exact hright · rcases largerIndex_eq_current_or_candidate a heapSize (largerIndex a heapSize i (left i)) (right i) with hright | hright · right left simpa [hleft] using hright · right right exact hright

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 := by rcases maxChildIndex_eq_self_or_left_or_right a heapSize i with hself | hchild · exact False.elim (h hself) · exact hchild

A swapping MAX-HEAPIFY step moves strictly down the array heap.

theorem lt_maxChildIndex_of_ne {a : List Nat} {heapSize i : Nat} (h : maxChildIndex a heapSize i ≠ i) : i < maxChildIndex a heapSize i := by rcases maxChildIndex_eq_left_or_right_of_ne h with hleft | hright · rw [hleft] unfold left omega · rw [hright] unfold right omega

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 := by have hdown : i < maxChildIndex a heapSize i := lt_maxChildIndex_of_ne h have hheap : maxChildIndex a heapSize i < heapSize := maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi omega

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) := by unfold maxChildIndex exact Nat.le_trans (valAt_current_le_largerIndex a heapSize i (left i)) (valAt_current_le_largerIndex a heapSize (largerIndex a heapSize i (left i)) (right 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) := by unfold maxChildIndex exact Nat.le_trans (valAt_candidate_le_largerIndex (a := a) (current := i) hl) (valAt_current_le_largerIndex a heapSize (largerIndex a heapSize i (left i)) (right 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) := by unfold maxChildIndex exact valAt_candidate_le_largerIndex (a := a) (current := largerIndex a heapSize i (left i)) hr

A left child index is strictly different from its parent index.

theorem left_ne_self (i : Nat) : left i ≠ i := by unfold left omega

A right child index is strictly different from its parent index.

theorem right_ne_self (i : Nat) : right i ≠ i := by unfold right omega

After a nontrivial heapify swap, the value moved into i dominates the old left child.

theorem valAt_swapAt_i_ge_left {a : List Nat} {heapSize i : Nat} (hlen : heapSize ≤ a.length) (hi : i < heapSize) (_hneq : maxChildIndex a heapSize i ≠ i) (hl : left i < heapSize) : valAt (swapAt a i (maxChildIndex a heapSize i)) (left i) ≤ valAt (swapAt a i (maxChildIndex a heapSize i)) i := by let largest := maxChildIndex a heapSize i have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hlargest_len : largest < a.length := Nat.lt_of_lt_of_le hlargest_heap hlen have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hlen have hparent : valAt (swapAt a i largest) i = valAt a largest := valAt_swapAt_left hi_len hlargest_len by_cases hleft : left i = largest · have hchild : valAt (swapAt a i largest) (left i) = valAt a i := by simpa [hleft] using valAt_swapAt_right hi_len hlargest_len rw [hchild, hparent] simpa [largest] using valAt_i_le_maxChildIndex a heapSize i · have hchild : valAt (swapAt a i largest) (left i) = valAt a (left i) := by exact valAt_swapAt_of_ne hi_len hlargest_len (left_ne_self i) hleft rw [hchild, hparent] simpa [largest] using valAt_left_le_maxChildIndex (a := a) (heapSize := heapSize) (i := i) hl

After a nontrivial heapify swap, the value moved into i dominates the old right child.

theorem valAt_swapAt_i_ge_right {a : List Nat} {heapSize i : Nat} (hlen : heapSize ≤ a.length) (hi : i < heapSize) (_hneq : maxChildIndex a heapSize i ≠ i) (hr : right i < heapSize) : valAt (swapAt a i (maxChildIndex a heapSize i)) (right i) ≤ valAt (swapAt a i (maxChildIndex a heapSize i)) i := by let largest := maxChildIndex a heapSize i have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hlargest_len : largest < a.length := Nat.lt_of_lt_of_le hlargest_heap hlen have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hlen have hparent : valAt (swapAt a i largest) i = valAt a largest := valAt_swapAt_left hi_len hlargest_len by_cases hright : right i = largest · have hchild : valAt (swapAt a i largest) (right i) = valAt a i := by simpa [hright] using valAt_swapAt_right hi_len hlargest_len rw [hchild, hparent] simpa [largest] using valAt_i_le_maxChildIndex a heapSize i · have hchild : valAt (swapAt a i largest) (right i) = valAt a (right i) := by exact valAt_swapAt_of_ne hi_len hlargest_len (right_ne_self i) hright rw [hchild, hparent] simpa [largest] using valAt_right_le_maxChildIndex (a := a) (heapSize := heapSize) (i := i) hr

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.

theorem arrayMaxHeapExceptFrom_after_swap_at_root {a : List Nat} {heapSize i : Nat} (hexcept : ArrayMaxHeapExceptFrom a heapSize i i) (hi : i < heapSize) (hneq : maxChildIndex a heapSize i ≠ i) : ArrayMaxHeapExceptFrom (swapAt a i (maxChildIndex a heapSize i)) heapSize i (maxChildIndex a heapSize i) := by let largest := maxChildIndex a heapSize i have hlen_swapped : heapSize ≤ (swapAt a i largest).length := by simpa [largest, swapAt_length] using hexcept.heapSize_le_length have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hexcept.heapSize_le_length have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hlargest_len : largest < a.length := Nat.lt_of_lt_of_le hlargest_heap hexcept.heapSize_le_length have hlargest_child : largest = left i ∨ largest = right i := by simpa [largest] using maxChildIndex_eq_left_or_right_of_ne hneq refine ⟨hlen_swapped, ?_, ?_⟩ · intro j hij hj hbad hl by_cases hji : j = i · subst j have hval := valAt_swapAt_i_ge_left (a := a) (heapSize := heapSize) (i := i) hexcept.heapSize_le_length hi hneq hl rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hl hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · have hleft_ne_i : left j ≠ i := by intro hEq unfold left at hEq omega have hleft_ne_largest : left j ≠ largest := by intro hEq rcases hlargest_child with hleft | hright · have : left j = left i := by simpa [hleft] using hEq unfold left at this omega · have : left j = right i := by simpa [hright] using hEq unfold left right at this omega have hchild_read : valAt (swapAt a i largest) (left j) = valAt a (left j) := valAt_swapAt_of_ne hi_len hlargest_len hleft_ne_i hleft_ne_largest have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hji hbad have hchild_old_len : left j < a.length := Nat.lt_of_lt_of_le hl hexcept.heapSize_le_length have hparent_old_len : j < a.length := Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length have hold := hexcept.left_le hij hj hji hl rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a i largest) (left j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hl hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · intro j hij hj hbad hr by_cases hji : j = i · subst j have hval := valAt_swapAt_i_ge_right (a := a) (heapSize := heapSize) (i := i) hexcept.heapSize_le_length hi hneq hr rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hr hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · have hright_ne_i : right j ≠ i := by intro hEq unfold right at hEq omega have hright_ne_largest : right j ≠ largest := by intro hEq rcases hlargest_child with hleft | hright · have : right j = left i := by simpa [hleft] using hEq unfold left right at this omega · have : right j = right i := by simpa [hright] using hEq unfold right at this omega have hchild_read : valAt (swapAt a i largest) (right j) = valAt a (right j) := valAt_swapAt_of_ne hi_len hlargest_len hright_ne_i hright_ne_largest have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hji hbad have hchild_old_len : right j < a.length := Nat.lt_of_lt_of_le hr hexcept.heapSize_le_length have hparent_old_len : j < a.length := Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length have hold := hexcept.right_le hij hj hji hr rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a i largest) (right j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hr hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval

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.

theorem badChildrenLeParent_after_swap {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) : BadChildrenLeParent (swapAt a i (maxChildIndex a heapSize i)) heapSize start (maxChildIndex a heapSize i) := by let largest := maxChildIndex a heapSize i have hdown : i < largest := by simpa [largest] using lt_maxChildIndex_of_ne hneq have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hexcept.heapSize_le_length have hlargest_len : largest < a.length := Nat.lt_of_lt_of_le hlargest_heap hexcept.heapSize_le_length have hparent_largest : parent largest = i := by rcases maxChildIndex_eq_left_or_right_of_ne hneq with hleft | hright · simpa [largest, hleft] using parent_left i · simpa [largest, hright] using parent_right i intro _ constructor · intro hl have hchild_ne_i : left largest ≠ i := by unfold left omega have hchild_ne_largest : left largest ≠ largest := left_ne_self largest have hchild_read : valAt (swapAt a i largest) (left largest) = valAt a (left largest) := valAt_swapAt_of_ne hi_len hlargest_len hchild_ne_i hchild_ne_largest have hparent_read : valAt (swapAt a i largest) (parent largest) = valAt a largest := by simpa [hparent_largest] using valAt_swapAt_left hi_len hlargest_len have hold := hexcept.left_le (Nat.le_trans hstart (Nat.le_of_lt hdown)) hlargest_heap (Ne.symm (ne_of_lt hdown)) hl rw [← valAt_eq_getElem a (Nat.lt_of_lt_of_le hl hexcept.heapSize_le_length), ← valAt_eq_getElem a (Nat.lt_of_lt_of_le hlargest_heap hexcept.heapSize_le_length)] at hold rw [hchild_read, hparent_read] exact hold · intro hr have hchild_ne_i : right largest ≠ i := by unfold right omega have hchild_ne_largest : right largest ≠ largest := right_ne_self largest have hchild_read : valAt (swapAt a i largest) (right largest) = valAt a (right largest) := valAt_swapAt_of_ne hi_len hlargest_len hchild_ne_i hchild_ne_largest have hparent_read : valAt (swapAt a i largest) (parent largest) = valAt a largest := by simpa [hparent_largest] using valAt_swapAt_left hi_len hlargest_len have hold := hexcept.right_le (Nat.le_trans hstart (Nat.le_of_lt hdown)) hlargest_heap (Ne.symm (ne_of_lt hdown)) hr rw [← valAt_eq_getElem a (Nat.lt_of_lt_of_le hr hexcept.heapSize_le_length), ← valAt_eq_getElem a (Nat.lt_of_lt_of_le hlargest_heap hexcept.heapSize_le_length)] at hold rw [hchild_read, hparent_read] exact hold

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.

theorem arrayMaxHeapExceptFrom_after_swap_path {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) : ArrayMaxHeapExceptFrom (swapAt a i (maxChildIndex a heapSize i)) heapSize start (maxChildIndex a heapSize i) := by let largest := maxChildIndex a heapSize i have hdown : i < largest := by simpa [largest] using lt_maxChildIndex_of_ne hneq have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hexcept.heapSize_le_length have hlargest_len : largest < a.length := Nat.lt_of_lt_of_le hlargest_heap hexcept.heapSize_le_length have hlen_swapped : heapSize ≤ (swapAt a i largest).length := by simpa [largest, swapAt_length] using hexcept.heapSize_le_length have hlargest_child : largest = left i ∨ largest = right i := by simpa [largest] using maxChildIndex_eq_left_or_right_of_ne hneq have hroot : ArrayMaxHeapExceptFrom (swapAt a i largest) heapSize i largest := arrayMaxHeapExceptFrom_after_swap_at_root (ArrayMaxHeapExceptFrom.mono_start hexcept hstart) hi (by simpa [largest] using hneq) refine ⟨hlen_swapped, ?_, ?_⟩ · intro j hsj hj hbad hl by_cases hij : i ≤ j · exact hroot.left_le hij hj hbad hl · have hji : j < i := Nat.lt_of_not_ge hij have hjne_i : j ≠ i := ne_of_lt hji by_cases hchild_i : left j = i · have hstart_lt_i : start < i := Nat.lt_of_le_of_lt hsj hji have hb := hbound hstart_lt_i have hlargest_le_parent_i : valAt a largest ≤ valAt a (parent i) := by rcases hlargest_child with hleft | hright · simpa [largest, hleft] using hb.1 (by simpa [largest, hleft] using hlargest_heap) · simpa [largest, hright] using hb.2 (by simpa [largest, hright] using hlargest_heap) have hparent_i : parent i = j := by rw [← hchild_i] exact parent_left j have hchild_read : valAt (swapAt a i largest) (left j) = valAt a largest := by simpa [hchild_i] using valAt_swapAt_left hi_len hlargest_len have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hjne_i hbad have hval : valAt (swapAt a i largest) (left j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] simpa [hparent_i] using hlargest_le_parent_i rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hl hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · by_cases hchild_largest : left j = largest · exfalso rcases hlargest_child with hleft | hright · have : left j = left i := by simpa [largest, hleft] using hchild_largest unfold left at this omega · have : left j = right i := by simpa [largest, hright] using hchild_largest unfold left right at this omega · have hchild_read : valAt (swapAt a i largest) (left j) = valAt a (left j) := valAt_swapAt_of_ne hi_len hlargest_len hchild_i hchild_largest have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hjne_i hbad have hchild_old_len : left j < a.length := Nat.lt_of_lt_of_le hl hexcept.heapSize_le_length have hparent_old_len : j < a.length := Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length have hold := hexcept.left_le hsj hj hjne_i hl rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a i largest) (left j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hl hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · intro j hsj hj hbad hr by_cases hij : i ≤ j · exact hroot.right_le hij hj hbad hr · have hji : j < i := Nat.lt_of_not_ge hij have hje_i : j ≠ i := ne_of_lt hji by_cases hchild_i : right j = i · have hstart_lt_i : start < i := Nat.lt_of_le_of_lt hsj hji have hb := hbound hstart_lt_i have hlargest_le_parent_i : valAt a largest ≤ valAt a (parent i) := by rcases hlargest_child with hleft | hright · simpa [largest, hleft] using hb.1 (by simpa [largest, hleft] using hlargest_heap) · simpa [largest, hright] using hb.2 (by simpa [largest, hright] using hlargest_heap) have hparent_i : parent i = j := by rw [← hchild_i] exact parent_right j have hchild_read : valAt (swapAt a i largest) (right j) = valAt a largest := by simpa [hchild_i] using valAt_swapAt_left hi_len hlargest_len have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hje_i hbad have hval : valAt (swapAt a i largest) (right j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] simpa [hparent_i] using hlargest_le_parent_i rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hr hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval · by_cases hchild_largest : right j = largest · exfalso rcases hlargest_child with hleft | hright · have : right j = left i := by simpa [largest, hleft] using hchild_largest unfold left right at this omega · have : right j = right i := by simpa [largest, hright] using hchild_largest unfold right at this omega · have hchild_read : valAt (swapAt a i largest) (right j) = valAt a (right j) := valAt_swapAt_of_ne hi_len hlargest_len hchild_i hchild_largest have hparent_read : valAt (swapAt a i largest) j = valAt a j := valAt_swapAt_of_ne hi_len hlargest_len hje_i hbad have hchild_old_len : right j < a.length := Nat.lt_of_lt_of_le hr hexcept.heapSize_le_length have hparent_old_len : j < a.length := Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length have hold := hexcept.right_le hsj hj hje_i hr rw [← valAt_eq_getElem a hchild_old_len, ← valAt_eq_getElem a hparent_old_len] at hold have hval : valAt (swapAt a i largest) (right j) ≤ valAt (swapAt a i largest) j := by rw [hchild_read, hparent_read] exact hold rw [valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hr hlen_swapped), valAt_eq_getElem (swapAt a i largest) (Nat.lt_of_lt_of_le hj hlen_swapped)] at hval simpa [largest] using hval

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 largest

Fuelled heapify preserves list length.

theorem maxHeapifyFuel_length (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (maxHeapifyFuel fuel a heapSize i).length = a.length := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuel] | succ fuel ih => simp [maxHeapifyFuel] split · rfl · trans (swapAt a i (maxChildIndex a heapSize i)).length · exact ih (swapAt a i (maxChildIndex a heapSize i)) (maxChildIndex a heapSize i) · exact swapAt_length a i (maxChildIndex a heapSize i)

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 := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuel] | succ fuel ih => simp [maxHeapifyFuel] split · rfl · exact (ih (swapAt a i (maxChildIndex a heapSize i)) (maxChildIndex a heapSize i)).trans (swapAt_perm a i (maxChildIndex a heapSize i))

Fuelled heapify only swaps cells inside the heap prefix. Therefore every cell at an index k ≥ heapSize keeps the same value.

theorem maxHeapifyFuel_valAt_of_heapSize_le {fuel : Nat} {a : List Nat} {heapSize i k : Nat} (hlen : heapSize ≤ a.length) (hi : i < heapSize) (hk : heapSize ≤ k) : valAt (maxHeapifyFuel fuel a heapSize i) k = valAt a k := by induction fuel generalizing a i with | zero => simp [maxHeapifyFuel] | succ fuel ih => by_cases hmax : maxChildIndex a heapSize i = i · simp [maxHeapifyFuel, hmax] · 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_read : valAt (swapAt a i largest) k = valAt a k := by exact valAt_swapAt_of_ne (Nat.lt_of_lt_of_le hi hlen) (Nat.lt_of_lt_of_le hlargest hlen) (by omega) (by omega) have hrec := ih (a := swapAt a i largest) (i := largest) hswap_len hlargest rw [maxHeapifyFuel, if_neg hmax] simpa [largest, hswap_read] using hrec

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 := by unfold largerIndex at h by_cases hin : candidate < heapSize · simp [hin] at h by_cases hlt : valAt a current < valAt a candidate · simp [hlt] at h exact False.elim (hcandidate h) · simpa [hlt] using h · simpa [hin] using h

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 := by unfold largerIndex at h simp [hcandidate] at h by_cases hlt : valAt a current < valAt a candidate · simp [hlt] at h subst candidate exact Nat.le_refl _ · exact Nat.le_of_not_gt hlt

If MAX-HEAPIFY chooses not to swap, the left-child inequality at i holds.

theorem maxChildIndex_eq_self_left_le {a : List Nat} {heapSize i : Nat} (hmax : maxChildIndex a heapSize i = i) (hl : left i < heapSize) : valAt a (left i) ≤ valAt a i := by have hleft : largerIndex a heapSize i (left i) = i := largerIndex_eq_target_forces_current (by simpa [maxChildIndex] using hmax) (right_ne_self i) exact largerIndex_eq_current_le hleft hl

If MAX-HEAPIFY chooses not to swap, the right-child inequality at i holds.

theorem maxChildIndex_eq_self_right_le {a : List Nat} {heapSize i : Nat} (hmax : maxChildIndex a heapSize i = i) (hr : right i < heapSize) : valAt a (right i) ≤ valAt a i := by have hleft : largerIndex a heapSize i (left i) = i := largerIndex_eq_target_forces_current (by simpa [maxChildIndex] using hmax) (right_ne_self i) have hright : largerIndex a heapSize i (right i) = i := by simpa [maxChildIndex, hleft] using hmax exact largerIndex_eq_current_le hright hr

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.

theorem arrayMaxHeap_of_except_of_maxChildIndex_self {a : List Nat} {heapSize i : Nat} (hexcept : ArrayMaxHeapExcept a heapSize i) (hmax : maxChildIndex a heapSize i = i) : ArrayMaxHeap a heapSize := by refine ⟨hexcept.heapSize_le_length, ?_, ?_⟩ · intro j hj hl by_cases hji : j = i · subst j have hval := maxChildIndex_eq_self_left_le hmax hl rw [valAt_eq_getElem a (Nat.lt_of_lt_of_le hl hexcept.heapSize_le_length), valAt_eq_getElem a (Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length)] at hval exact hval · exact hexcept.left_le hj hji hl · intro j hj hr by_cases hji : j = i · subst j have hval := maxChildIndex_eq_self_right_le hmax hr rw [valAt_eq_getElem a (Nat.lt_of_lt_of_le hr hexcept.heapSize_le_length), valAt_eq_getElem a (Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length)] at hval exact hval · exact hexcept.right_le hj hji hr

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.

theorem arrayMaxHeapFrom_of_exceptFrom_of_maxChildIndex_self {a : List Nat} {heapSize start i : Nat} (hexcept : ArrayMaxHeapExceptFrom a heapSize start i) (hmax : maxChildIndex a heapSize i = i) : ArrayMaxHeapFrom a heapSize start := by refine ⟨hexcept.heapSize_le_length, ?_, ?_⟩ · intro j hstart hj hl by_cases hji : j = i · subst j have hval := maxChildIndex_eq_self_left_le hmax hl rw [valAt_eq_getElem a (Nat.lt_of_lt_of_le hl hexcept.heapSize_le_length), valAt_eq_getElem a (Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length)] at hval exact hval · exact hexcept.left_le hstart hj hji hl · intro j hstart hj hr by_cases hji : j = i · subst j have hval := maxChildIndex_eq_self_right_le hmax hr rw [valAt_eq_getElem a (Nat.lt_of_lt_of_le hr hexcept.heapSize_le_length), valAt_eq_getElem a (Nat.lt_of_lt_of_le hj hexcept.heapSize_le_length)] at hval exact hval · exact hexcept.right_le hstart hj hji hr

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 := by by_cases hmax : maxChildIndex a heapSize i = i · simpa [maxHeapifyFuel, hmax] using arrayMaxHeapFrom_of_exceptFrom_of_maxChildIndex_self hexcept hmax · simpa [maxHeapifyFuel, hmax] using hrec hmax

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.

theorem arrayMaxHeapFrom_of_maxHeapifyFuel {fuel : Nat} {a : List Nat} {heapSize start i : Nat} (hexcept : ArrayMaxHeapExceptFrom a heapSize start i) (hstart : start ≤ i) (hi : i < heapSize) (hbound : BadChildrenLeParent a heapSize start i) (hfuel : heapSize - i ≤ fuel) : ArrayMaxHeapFrom (maxHeapifyFuel fuel a heapSize i) heapSize start := by induction fuel generalizing a start i with | zero => omega | succ fuel ih => exact arrayMaxHeapFrom_of_maxHeapifyFuel_succ (fuel := fuel) (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept (by intro hneq let largest := maxChildIndex a heapSize i have hstart_largest : start ≤ largest := by have hdown : i < largest := by simpa [largest] using lt_maxChildIndex_of_ne hneq exact Nat.le_trans hstart (Nat.le_of_lt hdown) have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hdecrease : heapSize - largest < heapSize - i := by simpa [largest] using heapSize_sub_maxChildIndex_lt_of_ne (a := a) (heapSize := heapSize) (i := i) hi hneq have hfuel_child : heapSize - largest ≤ fuel := by omega exact ih (arrayMaxHeapExceptFrom_after_swap_path (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept hstart hi hneq hbound) hstart_largest hlargest_heap (badChildrenLeParent_after_swap (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept hstart hi hneq) hfuel_child)

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.

theorem maxHeapifyFuel_child_repair_after_swap {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 (swapAt a i (maxChildIndex a heapSize i)) heapSize (maxChildIndex a heapSize i)) heapSize start := by let largest := maxChildIndex a heapSize i have hdown : i < largest := by simpa [largest] using lt_maxChildIndex_of_ne hneq have hstart_largest : start ≤ largest := Nat.le_trans hstart (Nat.le_of_lt hdown) have hlargest_heap : largest < heapSize := by simpa [largest] using maxChildIndex_lt_heapSize (a := a) (heapSize := heapSize) hi have hexcept_child : ArrayMaxHeapExceptFrom (swapAt a i largest) heapSize start largest := arrayMaxHeapExceptFrom_after_swap_path (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept hstart hi hneq hbound have hbound_child : BadChildrenLeParent (swapAt a i largest) heapSize start largest := badChildrenLeParent_after_swap (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept hstart hi hneq have hrepair := arrayMaxHeapFrom_of_maxHeapifyFuel (fuel := fuel) (a := swapAt a i largest) (heapSize := heapSize) (start := start) (i := largest) hexcept_child hstart_largest hlargest_heap hbound_child (by simpa [largest] using hfuel) simpa [largest] using hrepair

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 := by have hchild := maxHeapifyFuel_child_repair_after_swap (fuel := fuel) (a := a) (heapSize := heapSize) (start := start) (i := i) hexcept hstart hi hneq hbound hfuel simpa [maxHeapifyFuel, hneq] using hchild

Index-suffix form of MAX-HEAPIFY correctness: if every parent index at least i satisfies the heap inequalities except possibly i itself, enough fuel restores all those inequalities. The precondition includes nodes outside the descendant subtree of i. The historical theorem name is retained for compatibility; bottom-up construction uses this stronger invariant.

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.

theorem maxHeapifyFuel_root_isMaxHeap {fuel : Nat} {a : List Nat} {heapSize : Nat} (hexcept : ArrayMaxHeapExcept a heapSize 0) (hpos : 0 < heapSize) (hfuel : heapSize ≤ fuel) : ArrayMaxHeap (maxHeapifyFuel fuel a heapSize 0) heapSize := by have hfrom : ArrayMaxHeapFrom (maxHeapifyFuel fuel a heapSize 0) heapSize 0 := arrayMaxHeapFrom_of_maxHeapifyFuel (ArrayMaxHeapExcept.from_start (start := 0) hexcept) (Nat.le_refl 0) hpos (BadChildrenLeParent.self a heapSize 0) (by simpa using hfuel) exact ArrayMaxHeapFrom.to_global hfrom
end Chapter06end CLRS
Imports
import CLRSLean.FourthEdition.Chapter_06.Section_06_2_Maintaining_Heap_Property

6.3. Building a Heap

This section proves the indexed version of CLRS BUILD-MAX-HEAP. The main builder starts from the last internal-node layer and repeatedly calls the fuelled MAX-HEAPIFY theorem from Section 6.2.

Main results:

  • Theorem ArrayMaxHeapFrom.of_half: every node from heapSize / 2 onward is a leaf, so that suffix is already a localized max-heap.

  • Theorem buildMaxHeapLoop_isMaxHeap: the bottom-up repeated MAX-HEAPIFY loop returns a global indexed max-heap.

  • Theorem buildMaxHeapLoop_perm: the bottom-up loop preserves the input multiset.

  • Theorem arrayBuildMaxHeap_isMaxHeap: the array-facing builder returns an indexed max-heap over the whole list.

  • Theorem arrayBuildMaxHeap_perm: the builder preserves the multiset of input elements.

  • Theorem arrayBuildMaxHeap_correct: the reader-facing correctness theorem bundling heapness, permutation, and length preservation.

Remaining refinements:

  • This section proves the CLRS-style bottom-up heap construction used by the in-place heapsort loop. Later work can connect it to a shared imperative array semantics and cost model.

namespace CLRSnamespace Chapter06

Bottom-up heap construction

Array-facing name for the older compact functional heap builder.

def arrayBuildMaxHeapFunctional (xs : List Nat) : List Nat := buildMaxHeap xs

Bottom-up heap construction loop. With count k + 1, it first heapifies index k, then continues with k - 1, and so on down to zero.

def buildMaxHeapLoop : Nat → List Nat → Nat → List Nat | 0, a, _ => a | count + 1, a, heapSize => buildMaxHeapLoop count (maxHeapifyFuel heapSize a heapSize count) heapSize

The bottom-up build loop preserves list length.

theorem buildMaxHeapLoop_length (count : Nat) (a : List Nat) (heapSize : Nat) : (buildMaxHeapLoop count a heapSize).length = a.length := by induction count generalizing a with | zero => simp [buildMaxHeapLoop] | succ count ih => simp [buildMaxHeapLoop] exact (ih (maxHeapifyFuel heapSize a heapSize count)).trans (maxHeapifyFuel_length heapSize a heapSize count)

The bottom-up build loop preserves the multiset of elements.

theorem buildMaxHeapLoop_perm (count : Nat) (a : List Nat) (heapSize : Nat) : (buildMaxHeapLoop count a heapSize).Perm a := by induction count generalizing a with | zero => simp [buildMaxHeapLoop] | succ count ih => exact (ih (maxHeapifyFuel heapSize a heapSize count)).trans (maxHeapifyFuel_perm heapSize a heapSize count)

Every parent index from heapSize / 2 onward is a leaf. This is the zero-based version of the CLRS observation that nodes after ⌊heap-size / 2⌋ are leaves.

theorem ArrayMaxHeapFrom.of_half {a : List Nat} {heapSize : Nat} (hlen : heapSize ≤ a.length) : ArrayMaxHeapFrom a heapSize (heapSize / 2) := by refine ⟨hlen, ?_, ?_⟩ · intro i hhalf _ hl exfalso unfold left at hl omega · intro i hhalf _ hr exfalso unfold right at hr omega

If all localized heap obligations after i hold, then the same localized region starting at i has at most one bad parent, namely i itself.

theorem ArrayMaxHeapFrom.except_pred {a : List Nat} {heapSize i : Nat} (h : ArrayMaxHeapFrom a heapSize (i + 1)) : ArrayMaxHeapExceptFrom a heapSize i i := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro j hij hj hji hl have hnext : i + 1 ≤ j := by omega exact h.left_le hnext hj hl · intro j hij hj hji hr have hnext : i + 1 ≤ j := by omega exact h.right_le hnext hj hr

Correctness of the bottom-up build loop. If the suffix of parent obligations from count onward is already a localized heap, heapifying count - 1, ..., 0 produces a global max-heap.

theorem buildMaxHeapLoop_isMaxHeap {count : Nat} {a : List Nat} {heapSize : Nat} (hfrom : ArrayMaxHeapFrom a heapSize count) (hcount : count ≤ heapSize) : ArrayMaxHeap (buildMaxHeapLoop count a heapSize) heapSize := by induction count generalizing a with | zero => simpa [buildMaxHeapLoop] using ArrayMaxHeapFrom.to_global hfrom | succ count ih => have hi : count < heapSize := by omega have hrepair : ArrayMaxHeapFrom (maxHeapifyFuel heapSize a heapSize count) heapSize count := maxHeapifyFuel_repair_subtree (ArrayMaxHeapFrom.except_pred hfrom) hi (by omega) simpa [buildMaxHeapLoop] using ih hrepair (by omega)

CLRS-style array build: heapify all internal nodes from right to left.

def arrayBuildMaxHeap (xs : List Nat) : List Nat := buildMaxHeapLoop (xs.length / 2) xs xs.length

Array-level build refinement theorems

The older compact functional heap builder returns an indexed max-heap.

theorem arrayBuildMaxHeapFunctional_isMaxHeap (xs : List Nat) : ArrayMaxHeap (arrayBuildMaxHeapFunctional xs) (arrayBuildMaxHeapFunctional xs).length := by exact orderedDesc_arrayMaxHeap (Nat.le_refl _) (by simpa [arrayBuildMaxHeapFunctional] using buildMaxHeap_orderedDesc xs)

The older compact functional heap builder preserves the input elements.

theorem arrayBuildMaxHeapFunctional_perm (xs : List Nat) : (arrayBuildMaxHeapFunctional xs).Perm xs := by simpa [arrayBuildMaxHeapFunctional] using buildMaxHeap_perm xs

The array-facing heap builder returns an indexed max-heap.

theorem arrayBuildMaxHeap_isMaxHeap (xs : List Nat) : ArrayMaxHeap (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length := by have hheap : ArrayMaxHeap (arrayBuildMaxHeap xs) xs.length := by simpa [arrayBuildMaxHeap] using buildMaxHeapLoop_isMaxHeap (ArrayMaxHeapFrom.of_half (a := xs) (heapSize := xs.length) (Nat.le_refl _)) (Nat.div_le_self xs.length 2) simpa [arrayBuildMaxHeap, buildMaxHeapLoop_length] using hheap

Named repeated-heapify form of the array-facing build theorem, useful for status pages and later Section 6.4 refinements.

theorem arrayBuildMaxHeapRepeated_isMaxHeap (xs : List Nat) : ArrayMaxHeap (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length := arrayBuildMaxHeap_isMaxHeap xs

The array-facing heap builder preserves the input elements.

theorem arrayBuildMaxHeap_perm (xs : List Nat) : (arrayBuildMaxHeap xs).Perm xs := by simpa [arrayBuildMaxHeap] using buildMaxHeapLoop_perm (xs.length / 2) xs xs.length

Named repeated-heapify form of the array-facing permutation theorem.

theorem arrayBuildMaxHeapRepeated_perm (xs : List Nat) : (arrayBuildMaxHeap xs).Perm xs := arrayBuildMaxHeap_perm xs

Reader-facing correctness theorem for CLRS BUILD-MAX-HEAP: the bottom-up repeated-MAX-HEAPIFY builder returns an indexed max-heap over the full array, preserves the input multiset, and preserves array length.

theorem arrayBuildMaxHeap_correct (xs : List Nat) : ArrayMaxHeap (arrayBuildMaxHeap xs) (arrayBuildMaxHeap xs).length ∧ (arrayBuildMaxHeap xs).Perm xs ∧ (arrayBuildMaxHeap xs).length = xs.length := by exact ⟨arrayBuildMaxHeap_isMaxHeap xs, arrayBuildMaxHeap_perm xs, buildMaxHeapLoop_length (xs.length / 2) xs xs.length⟩
end Chapter06end CLRS
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
Imports
import CLRSLean.FourthEdition.Chapter_06.Section_06_4_Heapsort

6.5. Priority Queues

This file gives a functional priority-queue interface on top of the Chapter 6 descending-list heap model, then refines the main CLRS array operations for maximum, increase-key, extract-max, and delete. The functional interface remains a compact scaffold; the reader-facing array theorems track parent/child indices, key mutation, bubbling, heap-prefix size, length, and permutation.

Main results:

  • Theorem heapInsert_orderedDesc: inserting into a heap preserves the heap invariant.

  • Theorem heapInsert_perm: insertion adds exactly the inserted key.

  • Theorem heapIncreaseKey_orderedDesc: increasing one occurrence and rebuilding produces a heap.

  • Theorem heapDelete_orderedDesc: deleting one occurrence and rebuilding produces a heap.

  • Theorem arrayHeapMaximum?_max: the root returned by the array-level maximum operation bounds every key in the heap prefix.

  • Theorems ArrayMaxHeap.set_increased_except_up and ArrayMaxHeapExceptUp.bubble_step: the upward-bubbling proof spine for array-level HEAP-INCREASE-KEY.

  • Theorem arrayHeapIncreaseKey?_state_correct: the full fuelled array-level HEAP-INCREASE-KEY wrapper writes a larger key, repeatedly bubbles it toward the root, and returns a max-heap with the same backing-list length and swapped multiset.

  • Theorem arrayHeapInsert?_state_correct: checked insertion accepts any active prefix fitting in the backing list, inserts before the inactive tail, grows both heap size and list length by one, and adds exactly the requested key.

  • Theorem arrayHeapInsertWithCost?_state_correct_and_log_cost: the same state contract paired with an honest upward-bubbling control-frame count bounded by ⌊log₂(heapSize + 1)⌋ + 1.

  • Theorem arrayHeapIncreaseKeyNoBubble?_state_correct: the no-bubble branch of CLRS HEAP-INCREASE-KEY remains as a small readable corollary for the immediate-stop case.

  • Theorem arrayHeapExtractMax?_state_correct: the CLRS array-level extract-max step swaps the root with the last heap cell, shrinks the heap prefix, repairs the new root, and returns a state whose prefix is again a max-heap while the extracted key is the old maximum.

  • Theorem arrayHeapDelete?_state_correct: index-based CLRS HEAP-DELETE, implemented by raising the target cell to the current root maximum and then extracting the maximum, returns a shrunk heap prefix and records the deleted key.

Implementation detail:

Current gap:

  • The proved insertion cost counts visited bubbling frames; guard evaluation, persistent-list operations, allocation, and imperative RAM semantics remain outside this metric.

namespace CLRSnamespace Chapter06

Functional priority-queue operations

Insert a key into the functional max-priority queue.

def heapInsert (x : Nat) (h : List Nat) : List Nat := insertDesc x h

Increase one occurrence of old to new, then rebuild the abstract heap. If old is absent this inserts new; this total behavior avoids exceptions in the mathematical interface.

def heapIncreaseKey (old new : Nat) (h : List Nat) : List Nat := buildMaxHeap (new :: h.erase old)

Delete one occurrence of key, then rebuild the abstract heap.

def heapDelete (key : Nat) (h : List Nat) : List Nat := buildMaxHeap (h.erase key)

Correctness theorems

Priority-queue insertion preserves the heap invariant.

theorem heapInsert_orderedDesc {x : Nat} {h : List Nat} (hh : OrderedDesc h) : OrderedDesc (heapInsert x h) := by exact insertDesc_orderedDesc hh

Priority-queue insertion adds exactly the inserted key.

theorem heapInsert_perm (x : Nat) (h : List Nat) : (heapInsert x h).Perm (x :: h) := by exact insertDesc_perm x h

The maximum after insertion is maximal among the old keys and the new key.

theorem heapInsert_max {x m : Nat} {h : List Nat} (hh : OrderedDesc h) (hmax : heapMaximum? (heapInsert x h) = some m) : ∀ y ∈ x :: h, y ≤ m := by intro y hy have hyheap : y ∈ heapInsert x h := (List.Perm.mem_iff (heapInsert_perm x h)).2 hy exact heapMaximum?_max (heapInsert_orderedDesc hh) hmax y hyheap

Increasing a key and rebuilding returns a heap.

theorem heapIncreaseKey_orderedDesc (old new : Nat) (h : List Nat) : OrderedDesc (heapIncreaseKey old new h) := by exact buildMaxHeap_orderedDesc (new :: h.erase old)

Increasing a key preserves exactly the rebuilt multiset specification.

theorem heapIncreaseKey_perm (old new : Nat) (h : List Nat) : (heapIncreaseKey old new h).Perm (new :: h.erase old) := by exact buildMaxHeap_perm (new :: h.erase old)

Deleting one key occurrence and rebuilding returns a heap.

theorem heapDelete_orderedDesc (key : Nat) (h : List Nat) : OrderedDesc (heapDelete key h) := by exact buildMaxHeap_orderedDesc (h.erase key)

Deleting one key occurrence preserves exactly the rebuilt multiset specification.

theorem heapDelete_perm (key : Nat) (h : List Nat) : (heapDelete key h).Perm (h.erase key) := by exact buildMaxHeap_perm (h.erase key)

Array-level maximum operation

Array-level HEAP-MAXIMUM: return the root when the heap prefix is nonempty and within the backing list.

def arrayHeapMaximum? (a : List Nat) (heapSize : Nat) : Option Nat := if h : 0 < heapSize ∧ heapSize ≤ a.length then some (a[0]'(Nat.lt_of_lt_of_le h.1 h.2)) else none

The array-level maximum returned from the root bounds every heap element.

theorem arrayHeapMaximum?_max {a : List Nat} {heapSize m : Nat} (hheap : ArrayMaxHeap a heapSize) (hmax : arrayHeapMaximum? a heapSize = some m) : ∀ {i : Nat}, (hi : i < heapSize) → a[i]'(Nat.lt_of_lt_of_le hi hheap.heapSize_le_length) ≤ m := by intro i hi have hnonempty : 0 < heapSize := Nat.zero_lt_of_lt hi have hcond : 0 < heapSize ∧ heapSize ≤ a.length := ⟨hnonempty, hheap.heapSize_le_length⟩ have hroot : a[0]'(Nat.lt_of_lt_of_le hnonempty hheap.heapSize_le_length) = m := by simpa [arrayHeapMaximum?, hcond] using hmax rw [← hroot] exact hheap.getElem_le_root hi

Array-level no-bubble increase-key branch

Reading the cell just written by List.set.

theorem valAt_set_self {a : List Nat} {i x : Nat} (hi : i < a.length) : valAt (a.set i x) i = x := by simp [valAt, List.getElem?_set_self hi]

Reading any other cell after List.set.

theorem valAt_set_of_ne {a : List Nat} {i k x : Nat} (hki : k ≠ i) : valAt (a.set i x) k = valAt a k := by simp [valAt, show i ≠ k from Ne.symm hki]

For HEAP-INCREASE-KEY, the possible violation moves upward. Unlike MAX-HEAPIFY, where the possibly bad obligations are the outgoing child edges of a parent, here the possibly bad obligation is the incoming edge to the key currently bubbling up.

All heap edges are valid except possibly the edge whose child is badChild. The extra field says that the bad child's own children are already bounded by its parent; this is exactly the fact needed after swapping the bad child with its parent.

structure ArrayMaxHeapExceptUp (a : List Nat) (heapSize badChild : Nat) : Prop where heapSize_le_length : heapSize ≤ a.length left_le : ∀ {j : Nat}, j < heapSize → left j < heapSize → left j ≠ badChild → valAt a (left j) ≤ valAt a j right_le : ∀ {j : Nat}, j < heapSize → right j < heapSize → right j ≠ badChild → valAt a (right j) ≤ valAt a j bad_children_le_parent : 0 < badChild → badChild < heapSize → (∀ _ : left badChild < heapSize, valAt a (left badChild) ≤ valAt a (parent badChild)) ∧ (∀ _ : right badChild < heapSize, valAt a (right badChild) ≤ valAt a (parent badChild))

In an upward-exception heap, every non-exempt child is bounded by its parent.

theorem ArrayMaxHeapExceptUp.valAt_le_parent_of_ne {a : List Nat} {heapSize badChild i : Nat} (h : ArrayMaxHeapExceptUp a heapSize badChild) (hi : i < heapSize) (hpos : 0 < i) (hne : i ≠ badChild) : valAt a i ≤ valAt a (parent i) := by let p := parent i have hpheap : p < heapSize := Nat.lt_trans (parent_lt_self hpos) hi rcases eq_left_or_right_parent hpos with hleft | hright · have hchild : left p < heapSize := by simpa [p, hleft.symm] using hi have hchild_ne : left p ≠ badChild := by simpa [p, hleft.symm] using hne have hle := h.left_le hpheap hchild hchild_ne simpa [p, hleft.symm] using hle · have hchild : right p < heapSize := by simpa [p, hright.symm] using hi have hchild_ne : right p ≠ badChild := by simpa [p, hright.symm] using hne have hle := h.right_le hpheap hchild hchild_ne simpa [p, hright.symm] using hle

If the upward exception is absent or already bounded by its parent, the heap is global.

theorem ArrayMaxHeapExceptUp.to_global {a : List Nat} {heapSize badChild : Nat} (h : ArrayMaxHeapExceptUp a heapSize badChild) (hbad : badChild = 0 ∨ valAt a badChild ≤ valAt a (parent badChild)) : ArrayMaxHeap a heapSize := by refine ⟨h.heapSize_le_length, ?_, ?_⟩ · intro j hj hl have hchild_len : left j < a.length := Nat.lt_of_lt_of_le hl h.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj h.heapSize_le_length have hval : valAt a (left j) ≤ valAt a j := by by_cases hchild : left j = badChild · rcases hbad with hroot | hle · have hzero : left j = 0 := by simpa [hroot] using hchild unfold left at hzero omega · have hp : parent badChild = j := by rw [← hchild, parent_left] simpa [hchild, hp] using hle · exact h.left_le hj hl hchild rw [valAt_eq_getElem a hchild_len, valAt_eq_getElem a hparent_len] at hval exact hval · intro j hj hr have hchild_len : right j < a.length := Nat.lt_of_lt_of_le hr h.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj h.heapSize_le_length have hval : valAt a (right j) ≤ valAt a j := by by_cases hchild : right j = badChild · rcases hbad with hroot | hle · have hzero : right j = 0 := by simpa [hroot] using hchild unfold right at hzero omega · have hp : parent badChild = j := by rw [← hchild, parent_right] simpa [hchild, hp] using hle · exact h.right_le hj hr hchild rw [valAt_eq_getElem a hchild_len, valAt_eq_getElem a hparent_len] at hval exact hval

In a global heap, any positive node is bounded by its parent.

theorem ArrayMaxHeap.valAt_le_parent {a : List Nat} {heapSize i : Nat} (hheap : ArrayMaxHeap a heapSize) (hi : i < heapSize) (hpos : 0 < i) : valAt a i ≤ valAt a (parent i) := by let p := parent i have hpheap : p < heapSize := Nat.lt_trans (parent_lt_self hpos) hi have hp_len : p < a.length := Nat.lt_of_lt_of_le hpheap hheap.heapSize_le_length rcases eq_left_or_right_parent hpos with hleft | hright · have hchild : left p < heapSize := by simpa [p, hleft.symm] using hi have hchild_len : left p < a.length := Nat.lt_of_lt_of_le hchild hheap.heapSize_le_length have hle := hheap.left_le hpheap hchild have hleVal : valAt a (left p) ≤ valAt a p := by rw [valAt_eq_getElem a hchild_len, valAt_eq_getElem a hp_len] exact hle simpa [p, hleft.symm] using hleVal · have hchild : right p < heapSize := by simpa [p, hright.symm] using hi have hchild_len : right p < a.length := Nat.lt_of_lt_of_le hchild hheap.heapSize_le_length have hle := hheap.right_le hpheap hchild have hleVal : valAt a (right p) ≤ valAt a p := by rw [valAt_eq_getElem a hchild_len, valAt_eq_getElem a hp_len] exact hle simpa [p, hright.symm] using hleVal

After increasing a key at i, all heap edges are still valid except possibly the incoming edge to i. This is the invariant entry point for the CLRS upward bubbling loop.

theorem ArrayMaxHeap.set_increased_except_up {a : List Nat} {heapSize i key : Nat} (hheap : ArrayMaxHeap a heapSize) (hi : i < heapSize) (hraise : valAt a i ≤ key) : ArrayMaxHeapExceptUp (a.set i key) heapSize i := by have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hheap.heapSize_le_length have hlen : heapSize ≤ (a.set i key).length := by simpa [List.length_set] using hheap.heapSize_le_length have leftVal : ∀ {j : Nat}, j < heapSize → left j < heapSize → valAt a (left j) ≤ valAt a j := by intro j hj hl have hchild_len : left j < a.length := Nat.lt_of_lt_of_le hl hheap.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj hheap.heapSize_le_length have hold := hheap.left_le hj hl rw [← valAt_eq_getElem a hchild_len, ← valAt_eq_getElem a hparent_len] at hold exact hold have rightVal : ∀ {j : Nat}, j < heapSize → right j < heapSize → valAt a (right j) ≤ valAt a j := by intro j hj hr have hchild_len : right j < a.length := Nat.lt_of_lt_of_le hr hheap.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj hheap.heapSize_le_length have hold := hheap.right_le hj hr rw [← valAt_eq_getElem a hchild_len, ← valAt_eq_getElem a hparent_len] at hold exact hold refine ⟨hlen, ?_, ?_, ?_⟩ · intro j hj hl hchild_ne by_cases hparent : j = i · subst j rw [valAt_set_of_ne (a := a) (i := i) (k := left i) (x := key) (left_ne_self i), valAt_set_self hi_len] exact Nat.le_trans (leftVal hi hl) hraise · rw [valAt_set_of_ne (a := a) (i := i) (k := left j) (x := key) hchild_ne, valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent] exact leftVal hj hl · intro j hj hr hchild_ne by_cases hparent : j = i · subst j rw [valAt_set_of_ne (a := a) (i := i) (k := right i) (x := key) (right_ne_self i), valAt_set_self hi_len] exact Nat.le_trans (rightVal hi hr) hraise · rw [valAt_set_of_ne (a := a) (i := i) (k := right j) (x := key) hchild_ne, valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent] exact rightVal hj hr · intro hpos _ have hle_parent := hheap.valAt_le_parent hi hpos have hp_ne : parent i ≠ i := ne_of_lt (parent_lt_self hpos) constructor · intro hl rw [valAt_set_of_ne (a := a) (i := i) (k := left i) (x := key) (left_ne_self i), valAt_set_of_ne (a := a) (i := i) (k := parent i) (x := key) hp_ne] exact Nat.le_trans (leftVal hi hl) hle_parent · intro hr rw [valAt_set_of_ne (a := a) (i := i) (k := right i) (x := key) (right_ne_self i), valAt_set_of_ne (a := a) (i := i) (k := parent i) (x := key) hp_ne] exact Nat.le_trans (rightVal hi hr) hle_parent

One CLRS upward bubbling swap moves the only possible bad incoming edge from i to parent i.

theorem ArrayMaxHeapExceptUp.bubble_step {a : List Nat} {heapSize i : Nat} (h : ArrayMaxHeapExceptUp a heapSize i) (hi : i < heapSize) (hpos : 0 < i) (hswap : valAt a (parent i) < valAt a i) : ArrayMaxHeapExceptUp (swapAt a i (parent i)) heapSize (parent i) := by let p := parent i have hpheap : p < heapSize := Nat.lt_trans (parent_lt_self hpos) hi have hpi : p < i := parent_lt_self hpos have hi_len : i < a.length := Nat.lt_of_lt_of_le hi h.heapSize_le_length have hp_len : p < a.length := Nat.lt_of_lt_of_le hpheap h.heapSize_le_length have hlen : heapSize ≤ (swapAt a i p).length := by simpa [p, swapAt_length] using h.heapSize_le_length have hp_ne_i : p ≠ i := ne_of_lt hpi have hchildren := h.bad_children_le_parent hpos hi have hp_old_le_parent : ∀ (hp_pos : 0 < p), valAt a p ≤ valAt a (parent p) := by intro hp_pos exact h.valAt_le_parent_of_ne hpheap hp_pos hp_ne_i refine ⟨hlen, ?_, ?_, ?_⟩ · intro j hj hl hchild_ne_p by_cases hchild_i : left j = i · have hjp : j = p := by calc j = parent (left j) := (parent_left j).symm _ = parent i := by rw [hchild_i] _ = p := rfl rw [hchild_i, hjp] rw [valAt_swapAt_left hi_len hp_len, valAt_swapAt_right hi_len hp_len] exact Nat.le_of_lt hswap · by_cases hj_i : j = i · subst j have hleft_ne_p : left i ≠ p := by unfold left p parent omega rw [valAt_swapAt_of_ne hi_len hp_len (left_ne_self i) hleft_ne_p, valAt_swapAt_left hi_len hp_len] exact hchildren.1 hl · by_cases hj_p : j = p · subst j rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hchild_ne_p, valAt_swapAt_right hi_len hp_len] have hold := h.left_le hpheap hl hchild_i exact Nat.le_trans hold (Nat.le_of_lt hswap) · rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hchild_ne_p, valAt_swapAt_of_ne hi_len hp_len hj_i hj_p] exact h.left_le hj hl hchild_i · intro j hj hr hchild_ne_p by_cases hchild_i : right j = i · have hjp : j = p := by calc j = parent (right j) := (parent_right j).symm _ = parent i := by rw [hchild_i] _ = p := rfl rw [hchild_i, hjp] rw [valAt_swapAt_left hi_len hp_len, valAt_swapAt_right hi_len hp_len] exact Nat.le_of_lt hswap · by_cases hj_i : j = i · subst j have hright_ne_p : right i ≠ p := by unfold right p parent omega rw [valAt_swapAt_of_ne hi_len hp_len (right_ne_self i) hright_ne_p, valAt_swapAt_left hi_len hp_len] exact hchildren.2 hr · by_cases hj_p : j = p · subst j rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hchild_ne_p, valAt_swapAt_right hi_len hp_len] have hold := h.right_le hpheap hr hchild_i exact Nat.le_trans hold (Nat.le_of_lt hswap) · rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hchild_ne_p, valAt_swapAt_of_ne hi_len hp_len hj_i hj_p] exact h.right_le hj hr hchild_i · intro hp_pos _ have hparentp_ne_i : parent p ≠ i := by have hlt : parent p < i := Nat.lt_trans (parent_lt_self hp_pos) hpi exact ne_of_lt hlt have hparentp_ne_p : parent p ≠ p := ne_of_lt (parent_lt_self hp_pos) have hp_le_gp := hp_old_le_parent hp_pos constructor · intro hl by_cases hchild_i : left p = i · rw [hchild_i, valAt_swapAt_left hi_len hp_len] rw [valAt_swapAt_of_ne hi_len hp_len hparentp_ne_i hparentp_ne_p] exact hp_le_gp · have hleft_ne_p : left p ≠ p := left_ne_self p rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hleft_ne_p, valAt_swapAt_of_ne hi_len hp_len hparentp_ne_i hparentp_ne_p] have hold := h.left_le hpheap hl hchild_i exact Nat.le_trans hold hp_le_gp · intro hr by_cases hchild_i : right p = i · rw [hchild_i, valAt_swapAt_left hi_len hp_len] rw [valAt_swapAt_of_ne hi_len hp_len hparentp_ne_i hparentp_ne_p] exact hp_le_gp · have hright_ne_p : right p ≠ p := right_ne_self p rw [valAt_swapAt_of_ne hi_len hp_len hchild_i hright_ne_p, valAt_swapAt_of_ne hi_len hp_len hparentp_ne_i hparentp_ne_p] have hold := h.right_le hpheap hr hchild_i exact Nat.le_trans hold hp_le_gp

Fuelled upward bubbling loop for array-level HEAP-INCREASE-KEY. The fuel is bounded by the starting index, since each swap moves to the strict parent.

def arrayHeapIncreaseKeyBubbleUpFuel : Nat → List Nat → Nat → Nat → List Nat | 0, a, _heapSize, _i => a | fuel + 1, a, heapSize, i => if _ : 0 < i then if valAt a (parent i) < valAt a i then arrayHeapIncreaseKeyBubbleUpFuel fuel (swapAt a i (parent i)) heapSize (parent i) else a else a

The upward bubbling loop preserves the backing-list length.

theorem arrayHeapIncreaseKeyBubbleUpFuel_length (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (arrayHeapIncreaseKeyBubbleUpFuel fuel a heapSize i).length = a.length := by induction fuel generalizing a i with | zero => simp [arrayHeapIncreaseKeyBubbleUpFuel] | succ fuel ih => by_cases hpos : 0 < i · by_cases hswap : valAt a (parent i) < valAt a i · simp [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap, ih (a := swapAt a i (parent i)) (i := parent i), swapAt_length] · simp [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap] · simp [arrayHeapIncreaseKeyBubbleUpFuel, hpos]

The upward bubbling loop only swaps cells, so it preserves the multiset.

theorem arrayHeapIncreaseKeyBubbleUpFuel_perm (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (arrayHeapIncreaseKeyBubbleUpFuel fuel a heapSize i).Perm a := by induction fuel generalizing a i with | zero => simp [arrayHeapIncreaseKeyBubbleUpFuel] | succ fuel ih => by_cases hpos : 0 < i · by_cases hswap : valAt a (parent i) < valAt a i · have hrec := ih (a := swapAt a i (parent i)) (i := parent i) exact (by simpa [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap] using hrec.trans (swapAt_perm a i (parent i))) · simp [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap] · simp [arrayHeapIncreaseKeyBubbleUpFuel, hpos]

Enough upward-bubbling fuel discharges the upward exception and restores a global heap.

theorem ArrayMaxHeapExceptUp.bubbleUpFuel_global {fuel : Nat} {a : List Nat} {heapSize i : Nat} (h : ArrayMaxHeapExceptUp a heapSize i) (hi : i < heapSize) (hfuel : i ≤ fuel) : ArrayMaxHeap (arrayHeapIncreaseKeyBubbleUpFuel fuel a heapSize i) heapSize := by induction fuel generalizing a heapSize i with | zero => have hzero : i = 0 := by omega have hglobal : ArrayMaxHeap a heapSize := h.to_global (Or.inl hzero) simpa [arrayHeapIncreaseKeyBubbleUpFuel] using hglobal | succ fuel ih => by_cases hpos : 0 < i · by_cases hswap : valAt a (parent i) < valAt a i · have hpheap : parent i < heapSize := Nat.lt_trans (parent_lt_self hpos) hi have hp_le_fuel : parent i ≤ fuel := by have hpi : parent i < i := parent_lt_self hpos omega have hnext : ArrayMaxHeapExceptUp (swapAt a i (parent i)) heapSize (parent i) := h.bubble_step hi hpos hswap have hrec := ih (a := swapAt a i (parent i)) (heapSize := heapSize) (i := parent i) hnext hpheap hp_le_fuel simpa [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap] using hrec · have hle : valAt a i ≤ valAt a (parent i) := Nat.le_of_not_lt hswap have hglobal : ArrayMaxHeap a heapSize := h.to_global (Or.inr hle) simpa [arrayHeapIncreaseKeyBubbleUpFuel, hpos, hswap] using hglobal · have hzero : i = 0 := Nat.eq_zero_of_not_pos hpos have hglobal : ArrayMaxHeap a heapSize := h.to_global (Or.inl hzero) simpa [arrayHeapIncreaseKeyBubbleUpFuel, hpos] using hglobal

Array-level CLRS HEAP-INCREASE-KEY: write the key and bubble it upward.

def arrayHeapIncreaseKey? (a : List Nat) (heapSize i key : Nat) : Option (List Nat) := if _h : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key then some (arrayHeapIncreaseKeyBubbleUpFuel i (a.set i key) heapSize i) else none

State-correctness theorem for array-level HEAP-INCREASE-KEY.

theorem arrayHeapIncreaseKey?_state_correct {a rest : List Nat} {heapSize i key : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapIncreaseKey? a heapSize i key = some rest) : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key ∧ ArrayMaxHeap rest heapSize ∧ rest.length = a.length ∧ rest.Perm (a.set i key) := by unfold arrayHeapIncreaseKey? at hres by_cases hcond : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key · simp [hcond] at hres subst rest have hentry : ArrayMaxHeapExceptUp (a.set i key) heapSize i := hheap.set_increased_except_up hcond.1 hcond.2.2 have hrest_heap : ArrayMaxHeap (arrayHeapIncreaseKeyBubbleUpFuel i (a.set i key) heapSize i) heapSize := hentry.bubbleUpFuel_global hcond.1 (Nat.le_refl i) have hlen := arrayHeapIncreaseKeyBubbleUpFuel_length i (a.set i key) heapSize i have hperm := arrayHeapIncreaseKeyBubbleUpFuel_perm i (a.set i key) heapSize i refine ⟨hcond.1, hcond.2.1, hcond.2.2, hrest_heap, ?_, hperm⟩ simpa [List.length_set] using hlen · simp [hcond] at hres

Core no-bubble lemma for CLRS HEAP-INCREASE-KEY. If increasing a heap cell leaves it below its parent, the array is already a max-heap after the write, so the upward while-loop would stop immediately.

theorem ArrayMaxHeap.set_increased_no_bubble {a : List Nat} {heapSize i key : Nat} (hheap : ArrayMaxHeap a heapSize) (hi : i < heapSize) (hraise : valAt a i ≤ key) (hnobubble : i = 0 ∨ key ≤ valAt a (parent i)) : ArrayMaxHeap (a.set i key) heapSize := by have hi_len : i < a.length := Nat.lt_of_lt_of_le hi hheap.heapSize_le_length have hlen : heapSize ≤ (a.set i key).length := by simpa [List.length_set] using hheap.heapSize_le_length have leftVal : ∀ {j : Nat}, j < heapSize → left j < heapSize → valAt a (left j) ≤ valAt a j := by intro j hj hl have hchild_len : left j < a.length := Nat.lt_of_lt_of_le hl hheap.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj hheap.heapSize_le_length have hold := hheap.left_le hj hl rw [← valAt_eq_getElem a hchild_len, ← valAt_eq_getElem a hparent_len] at hold exact hold have rightVal : ∀ {j : Nat}, j < heapSize → right j < heapSize → valAt a (right j) ≤ valAt a j := by intro j hj hr have hchild_len : right j < a.length := Nat.lt_of_lt_of_le hr hheap.heapSize_le_length have hparent_len : j < a.length := Nat.lt_of_lt_of_le hj hheap.heapSize_le_length have hold := hheap.right_le hj hr rw [← valAt_eq_getElem a hchild_len, ← valAt_eq_getElem a hparent_len] at hold exact hold refine ⟨hlen, ?_, ?_⟩ · intro j hj hl have hchild_len : left j < (a.set i key).length := Nat.lt_of_lt_of_le hl hlen have hparent_len : j < (a.set i key).length := Nat.lt_of_lt_of_le hj hlen have hval : valAt (a.set i key) (left j) ≤ valAt (a.set i key) j := by by_cases hchild : left j = i · rw [hchild, valAt_set_self hi_len] have hparent_ne : j ≠ i := by rw [← hchild] unfold left omega rw [valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent_ne] rcases hnobubble with hroot | hle_parent · have hleft_zero : left j = 0 := by simpa [hroot] using hchild unfold left at hleft_zero omega · have hp : parent i = j := by rw [← hchild, parent_left] simpa [hp] using hle_parent · by_cases hparent : j = i · subst j rw [valAt_set_of_ne (a := a) (i := i) (k := left i) (x := key) (left_ne_self i), valAt_set_self hi_len] exact Nat.le_trans (leftVal hi hl) hraise · rw [valAt_set_of_ne (a := a) (i := i) (k := left j) (x := key) hchild, valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent] exact leftVal hj hl rw [valAt_eq_getElem (a.set i key) hchild_len, valAt_eq_getElem (a.set i key) hparent_len] at hval exact hval · intro j hj hr have hchild_len : right j < (a.set i key).length := Nat.lt_of_lt_of_le hr hlen have hparent_len : j < (a.set i key).length := Nat.lt_of_lt_of_le hj hlen have hval : valAt (a.set i key) (right j) ≤ valAt (a.set i key) j := by by_cases hchild : right j = i · rw [hchild, valAt_set_self hi_len] have hparent_ne : j ≠ i := by rw [← hchild] unfold right omega rw [valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent_ne] rcases hnobubble with hroot | hle_parent · have hright_zero : right j = 0 := by simpa [hroot] using hchild unfold right at hright_zero omega · have hp : parent i = j := by rw [← hchild, parent_right] simpa [hp] using hle_parent · by_cases hparent : j = i · subst j rw [valAt_set_of_ne (a := a) (i := i) (k := right i) (x := key) (right_ne_self i), valAt_set_self hi_len] exact Nat.le_trans (rightVal hi hr) hraise · rw [valAt_set_of_ne (a := a) (i := i) (k := right j) (x := key) hchild, valAt_set_of_ne (a := a) (i := i) (k := j) (x := key) hparent] exact rightVal hj hr rw [valAt_eq_getElem (a.set i key) hchild_len, valAt_eq_getElem (a.set i key) hparent_len] at hval exact hval

Array-level no-bubble branch of CLRS HEAP-INCREASE-KEY: write the new key at index i when the key is larger than the old key but still no larger than its parent, so the upward repair loop stops immediately.

def arrayHeapIncreaseKeyNoBubble? (a : List Nat) (heapSize i key : Nat) : Option (List Nat) := if _h : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key ∧ (i = 0 ∨ key ≤ valAt a (parent i)) then some (a.set i key) else none

State-correctness theorem for the no-bubble branch of array-level increase-key.

theorem arrayHeapIncreaseKeyNoBubble?_state_correct {a rest : List Nat} {heapSize i key : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapIncreaseKeyNoBubble? a heapSize i key = some rest) : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key ∧ (i = 0 ∨ key ≤ valAt a (parent i)) ∧ ArrayMaxHeap rest heapSize ∧ rest.length = a.length ∧ valAt rest i = key ∧ (∀ {k : Nat}, k ≠ i → valAt rest k = valAt a k) := by unfold arrayHeapIncreaseKeyNoBubble? at hres by_cases hcond : i < heapSize ∧ heapSize ≤ a.length ∧ valAt a i ≤ key ∧ (i = 0 ∨ key ≤ valAt a (parent i)) · simp [hcond] at hres subst rest have hi_len : i < a.length := Nat.lt_of_lt_of_le hcond.1 hcond.2.1 refine ⟨hcond.1, hcond.2.1, hcond.2.2.1, hcond.2.2.2, ?_, ?_, ?_, ?_⟩ · exact hheap.set_increased_no_bubble hcond.1 hcond.2.2.1 hcond.2.2.2 · simp [List.length_set] · exact valAt_set_self hi_len · intro k hk exact valAt_set_of_ne (a := a) (i := i) (k := k) (x := key) hk · simp [hcond] at hres

Array-level extract-max

Array-level HEAP-EXTRACT-MAX. The returned triple is the extracted maximum, the backing array after the CLRS root/last swap and root heapify, and the new heap prefix size.

def arrayHeapExtractMax? (a : List Nat) (heapSize : Nat) : Option (Nat × List Nat × Nat) := if h : 0 < heapSize ∧ heapSize ≤ a.length then let newHeapSize := heapSize - 1 let maximum := a[0]'(Nat.lt_of_lt_of_le h.1 h.2) let moved := swapAt a 0 newHeapSize let repaired := maxHeapifyFuel newHeapSize moved newHeapSize 0 some (maximum, repaired, newHeapSize) else none

State-correctness theorem for the array-level CLRS HEAP-EXTRACT-MAX step. The array keeps the same length and multiset, the heap prefix shrinks by one and is repaired into a max-heap, the returned key bounds the old heap prefix, and that key is stored at the first cell outside the new heap prefix.

theorem arrayHeapExtractMax?_state_correct {a : List Nat} {heapSize m : Nat} {rest : List Nat} {newHeapSize : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapExtractMax? a heapSize = some (m, rest, newHeapSize)) : 0 < heapSize ∧ newHeapSize + 1 = heapSize ∧ ArrayMaxHeap rest newHeapSize ∧ rest.length = a.length ∧ rest.Perm a ∧ (∀ {i : Nat}, i < heapSize → valAt a i ≤ m) ∧ newHeapSize < rest.length ∧ valAt rest newHeapSize = m := by unfold arrayHeapExtractMax? at hres by_cases hcond : 0 < heapSize ∧ heapSize ≤ a.length · simp [hcond] at hres rcases hres with ⟨hm, hrest_eq, hnew_eq⟩ subst m subst rest subst newHeapSize set newSize := heapSize - 1 have hsize_eq : newSize + 1 = heapSize := by dsimp [newSize] omega have hlen_swapped : newSize ≤ (swapAt a 0 newSize).length := by rw [swapAt_length] dsimp [newSize] omega have hrest_len : (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0).length = a.length := by rw [maxHeapifyFuel_length, swapAt_length] have hrest_perm : (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0).Perm a := by exact (maxHeapifyFuel_perm newSize (swapAt a 0 newSize) newSize 0).trans (swapAt_perm a 0 newSize) have h0_len : 0 < a.length := Nat.lt_of_lt_of_le hcond.1 hcond.2 have hlast_len : newSize < a.length := by dsimp [newSize] omega have hroot_val : valAt a 0 = a[0]'(Nat.lt_of_lt_of_le hcond.1 hcond.2) := by rw [valAt_eq_getElem a h0_len] have hmax_bound : ∀ {i : Nat}, i < heapSize → valAt a i ≤ a[0]'(Nat.lt_of_lt_of_le hcond.1 hcond.2) := by intro i hi rw [← hroot_val] exact hheap.valAt_le_root hi have hheap_rest : ArrayMaxHeap (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize := by by_cases hnew : 0 < newSize · have hheap' : ArrayMaxHeap a (newSize + 1) := by rwa [hsize_eq] have hexcept : ArrayMaxHeapExcept (swapAt a 0 newSize) newSize 0 := ArrayMaxHeapExcept.of_swap_root_last (a := a) (newHeapSize := newSize) hheap' exact maxHeapifyFuel_root_isMaxHeap (fuel := newSize) hexcept hnew (Nat.le_refl newSize) · have hzero : newSize = 0 := by omega rw [hzero] refine ⟨Nat.zero_le _, ?_, ?_⟩ <;> intro i hi hchild <;> omega have hstored : valAt (maxHeapifyFuel newSize (swapAt a 0 newSize) newSize 0) newSize = a[0]'(Nat.lt_of_lt_of_le hcond.1 hcond.2) := by by_cases hnew : 0 < 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) hlen_swapped hnew (Nat.le_refl newSize) have hswap_read : valAt (swapAt a 0 newSize) newSize = valAt a 0 := valAt_swapAt_right h0_len hlast_len rw [hheapify_read, hswap_read, hroot_val] · have hzero : newSize = 0 := by omega rw [hzero] have hswap_read : valAt (swapAt a 0 0) 0 = valAt a 0 := valAt_swapAt_right h0_len h0_len simpa [maxHeapifyFuel, hroot_val] using hswap_read refine ⟨hcond.1, hsize_eq, hheap_rest, hrest_len, hrest_perm, hmax_bound, ?_, hstored⟩ rw [hrest_len] exact hlast_len · simp [hcond] at hres

Array-level delete

Array-level CLRS HEAP-DELETE, expressed through the usual priority-queue recipe: raise the target cell to the current root maximum, then extract the maximum. In a finite natural-number model, the old root key is enough: it is a heap-prefix upper bound, so replacing the target by that key makes the target eligible for the subsequent extract-max step.

def arrayHeapDelete? (a : List Nat) (heapSize i : Nat) : Option (Nat × List Nat × Nat) := if _h : i < heapSize ∧ heapSize ≤ a.length then match arrayHeapIncreaseKey? a heapSize i (valAt a 0) with | some raised => match arrayHeapExtractMax? raised heapSize with | some (_removed, rest, newHeapSize) => some (valAt a i, rest, newHeapSize) | none => none | none => none else none

State-correctness theorem for array-level HEAP-DELETE. The returned heap prefix has size one less than the old prefix, is a max-heap, and the backing list is exactly the permutation produced by replacing the deleted cell with the old root maximum before the extract step.

theorem arrayHeapDelete?_state_correct {a rest : List Nat} {heapSize i deleted newHeapSize : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapDelete? a heapSize i = some (deleted, rest, newHeapSize)) : i < heapSize ∧ heapSize ≤ a.length ∧ deleted = valAt a i ∧ newHeapSize + 1 = heapSize ∧ ArrayMaxHeap rest newHeapSize ∧ rest.length = a.length ∧ rest.Perm (a.set i (valAt a 0)) ∧ (∀ {k : Nat}, k < heapSize → valAt a k ≤ valAt a 0) := by unfold arrayHeapDelete? at hres by_cases hcond : i < heapSize ∧ heapSize ≤ a.length · simp [hcond] at hres cases hinc : arrayHeapIncreaseKey? a heapSize i (valAt a 0) with | none => simp [hinc] at hres | some raised => simp [hinc] at hres cases hext : arrayHeapExtractMax? raised heapSize with | none => simp [hext] at hres | some extracted => rcases extracted with ⟨removed, extractedRest, extractedNewHeapSize⟩ simp [hext] at hres rcases hres with ⟨hdeleted, hrest, hnew⟩ subst deleted subst rest subst newHeapSize have hinc_correct := arrayHeapIncreaseKey?_state_correct (a := a) (rest := raised) (heapSize := heapSize) (i := i) (key := valAt a 0) hheap hinc have hext_correct := arrayHeapExtractMax?_state_correct (a := raised) (heapSize := heapSize) (m := removed) (rest := extractedRest) (newHeapSize := extractedNewHeapSize) hinc_correct.2.2.2.1 hext have hroot_bound : ∀ {k : Nat}, k < heapSize → valAt a k ≤ valAt a 0 := by intro k hk exact hheap.valAt_le_root hk have hperm : extractedRest.Perm (a.set i (valAt a 0)) := hext_correct.2.2.2.2.1.trans hinc_correct.2.2.2.2.2 refine ⟨hcond.1, hcond.2, rfl, hext_correct.2.1, hext_correct.2.2.1, ?_, hperm, hroot_bound⟩ exact hext_correct.2.2.2.1.trans hinc_correct.2.2.2.2.1 · simp [hcond] at hres
end Chapter06end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_06.Section_06_5_Priority_Queues.Insert.Basic

Section 6.5 — Basic array-level MAX-HEAP-INSERT

Appending a key to a full-prefix max-heap can invalidate only the new cell's incoming edge. The existing upward-exception invariant and bubble loop provide the complete repair proof.

namespace CLRSnamespace Chapter06

Reading an old array cell is unchanged after appending one new cell.

theorem valAt_append_singleton_of_lt {a : List Nat} {key i : Nat} (hi : i < a.length) : valAt (a ++ [key]) i = valAt a i := by simp [valAt, List.getD, List.getElem?_append_left hi]

Appending a key to a full-prefix heap leaves at most the new cell's incoming edge invalid. The new cell has no children inside the enlarged heap.

theorem ArrayMaxHeap.append_key_except_up {a : List Nat} (hheap : ArrayMaxHeap a a.length) (key : Nat) : ArrayMaxHeapExceptUp (a ++ [key]) (a.length + 1) a.length := by refine ⟨by simp, ?_, ?_, ?_⟩ · intro j hj hl hne have hchild : left j < a.length := by omega have hparent : j < a.length := by unfold left at hl omega rw [valAt_append_singleton_of_lt hchild, valAt_append_singleton_of_lt hparent, valAt_eq_getElem a hchild, valAt_eq_getElem a hparent] exact hheap.left_le hparent hchild · intro j hj hr hne have hchild : right j < a.length := by omega have hparent : j < a.length := by unfold right at hr omega rw [valAt_append_singleton_of_lt hchild, valAt_append_singleton_of_lt hparent, valAt_eq_getElem a hchild, valAt_eq_getElem a hparent] exact hheap.right_le hparent hchild · intro _hpos _hbad constructor · intro hleft unfold left at hleft omega · intro hright unfold right at hright omega

Array-level CLRS MAX-HEAP-INSERT: append the new key and bubble it upward. The fuel is the starting index, matching the existing increase-key repair loop.

def arrayHeapInsert (a : List Nat) (key : Nat) : List Nat := arrayHeapIncreaseKeyBubbleUpFuel a.length (a ++ [key]) (a.length + 1) a.length

Array-level insertion restores the max-heap invariant.

theorem arrayHeapInsert_isMaxHeap {a : List Nat} (key : Nat) (hheap : ArrayMaxHeap a a.length) : ArrayMaxHeap (arrayHeapInsert a key) (a.length + 1) := by exact (hheap.append_key_except_up key).bubbleUpFuel_global (by omega) (Nat.le_refl a.length)

Array-level insertion grows the backing list by exactly one cell.

theorem arrayHeapInsert_length (a : List Nat) (key : Nat) : (arrayHeapInsert a key).length = a.length + 1 := by simpa [arrayHeapInsert] using arrayHeapIncreaseKeyBubbleUpFuel_length a.length (a ++ [key]) (a.length + 1) a.length

Array-level insertion adds exactly the new key to the old multiset.

theorem arrayHeapInsert_perm (a : List Nat) (key : Nat) : (arrayHeapInsert a key).Perm (key :: a) := by have hbubble := arrayHeapIncreaseKeyBubbleUpFuel_perm a.length (a ++ [key]) (a.length + 1) a.length have happend : (a ++ [key]).Perm (key :: a) := by simpa only [List.singleton_append] using (List.perm_append_comm : (a ++ [key]).Perm ([key] ++ a)) exact hbubble.trans happend

The textbook state package for full-prefix array-level insertion.

theorem arrayHeapInsert_state_correct {a : List Nat} (key : Nat) (hheap : ArrayMaxHeap a a.length) : ArrayMaxHeap (arrayHeapInsert a key) (a.length + 1) ∧ (arrayHeapInsert a key).length = a.length + 1 ∧ (arrayHeapInsert a key).Perm (key :: a) := by exact ⟨arrayHeapInsert_isMaxHeap key hheap, arrayHeapInsert_length a key, arrayHeapInsert_perm a key⟩
end Chapter06end CLRS

CLRSLean.FourthEdition.Chapter_06.Section_06_5_Priority_Queues.Insert.Checked

Section 6.5 — Checked active-prefix MAX-HEAP-INSERT

The checked list-backed operation accepts exactly the states whose active heap prefix fits in the backing list. It inserts a new cell between that prefix and the inactive tail, preserving the tail order.

namespace CLRSnamespace Chapter06

Restricting a heap to its active prefix preserves the indexed heap.

theorem ArrayMaxHeap.take {a : List Nat} {heapSize : Nat} (hheap : ArrayMaxHeap a heapSize) : ArrayMaxHeap (a.take heapSize) heapSize := by have hlen : (a.take heapSize).length = heapSize := List.length_take_of_le hheap.heapSize_le_length refine ⟨by simp [hlen], ?_, ?_⟩ · intro i hi hl simpa only [List.getElem_take] using hheap.left_le hi hl · intro i hi hr simpa only [List.getElem_take] using hheap.right_le hi hr

Appending an inactive tail does not change heap obligations in the prefix.

theorem ArrayMaxHeap.append_tail {xs tail : List Nat} {heapSize : Nat} (hheap : ArrayMaxHeap xs heapSize) : ArrayMaxHeap (xs ++ tail) heapSize := by refine ⟨?_, ?_, ?_⟩ · calc heapSize ≤ xs.length := hheap.heapSize_le_length _ ≤ (xs ++ tail).length := by simp · intro i hi hl have hiPrefix : i < xs.length := Nat.lt_of_lt_of_le hi hheap.heapSize_le_length have hlPrefix : left i < xs.length := Nat.lt_of_lt_of_le hl hheap.heapSize_le_length simpa only [List.getElem_append_left hiPrefix, List.getElem_append_left hlPrefix] using hheap.left_le hi hl · intro i hi hr have hiPrefix : i < xs.length := Nat.lt_of_lt_of_le hi hheap.heapSize_le_length have hrPrefix : right i < xs.length := Nat.lt_of_lt_of_le hr hheap.heapSize_le_length simpa only [List.getElem_append_left hiPrefix, List.getElem_append_left hrPrefix] using hheap.right_le hi hr

Total checked insertion into an active heap prefix. The inactive tail remains after the newly enlarged prefix; an out-of-range heap size is rejected.

def arrayHeapInsert? (a : List Nat) (heapSize key : Nat) : Option (List Nat × Nat) := if _h : heapSize ≤ a.length then some (arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize, heapSize + 1) else none

Checked insertion fails exactly when the active prefix exceeds the backing list.

theorem arrayHeapInsert?_eq_none_iff (a : List Nat) (heapSize key : Nat) : arrayHeapInsert? a heapSize key = none ↔ ¬ heapSize ≤ a.length := by unfold arrayHeapInsert? by_cases h : heapSize ≤ a.length <;> simp [h]

Exact guard and output characterization for successful checked insertion.

theorem arrayHeapInsert?_eq_some_iff (a rest : List Nat) (heapSize newHeapSize key : Nat) : arrayHeapInsert? a heapSize key = some (rest, newHeapSize) ↔ heapSize ≤ a.length ∧ rest = arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize ∧ newHeapSize = heapSize + 1 := by unfold arrayHeapInsert? by_cases h : heapSize ≤ a.length · rw [dif_pos h] simp only [Option.some.injEq, Prod.mk.injEq] constructor · rintro ⟨hrest, hsize⟩ exact ⟨h, hrest.symm, hsize.symm⟩ · rintro ⟨_, hrest, hsize⟩ exact ⟨hrest.symm, hsize.symm⟩ · rw [dif_neg h] simp [h]

Successful checked insertion grows the active heap and backing list by one, preserves the inactive tail order, and adds exactly the requested key.

theorem arrayHeapInsert?_state_correct {a rest : List Nat} {heapSize newHeapSize key : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapInsert? a heapSize key = some (rest, newHeapSize)) : heapSize ≤ a.length ∧ newHeapSize = heapSize + 1 ∧ rest.length = a.length + 1 ∧ ArrayMaxHeap rest newHeapSize ∧ rest.Perm (key :: a) ∧ rest.drop newHeapSize = a.drop heapSize := by have hspec := (arrayHeapInsert?_eq_some_iff a rest heapSize newHeapSize key).1 hres rcases hspec with ⟨hguard, rfl, rfl⟩ have htakeLen : (a.take heapSize).length = heapSize := List.length_take_of_le hguard have hprefixHeap : ArrayMaxHeap (a.take heapSize) (a.take heapSize).length := by simpa [htakeLen] using hheap.take have hinsertHeap := arrayHeapInsert_isMaxHeap key hprefixHeap have hresultHeap : ArrayMaxHeap (arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize) (heapSize + 1) := by simpa [htakeLen] using hinsertHeap.append_tail (tail := a.drop heapSize) have hlength : (arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize).length = a.length + 1 := by rw [List.length_append, arrayHeapInsert_length] simp only [htakeLen, List.length_drop] have hsplit := Nat.sub_add_cancel hguard omega have hpermPrefix := (arrayHeapInsert_perm (a.take heapSize) key).append_right (a.drop heapSize) have hperm : (arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize).Perm (key :: a) := by simpa [List.take_append_drop] using hpermPrefix have hinsertLen : (arrayHeapInsert (a.take heapSize) key).length = heapSize + 1 := by simpa [htakeLen] using arrayHeapInsert_length (a.take heapSize) key have htail : (arrayHeapInsert (a.take heapSize) key ++ a.drop heapSize).drop (heapSize + 1) = a.drop heapSize := by rw [← hinsertLen] exact List.drop_left exact ⟨hguard, rfl, hlength, hresultHeap, hperm, htail⟩
end Chapter06end CLRS

CLRSLean.FourthEdition.Chapter_06.Section_06_5_Priority_Queues.Insert.Cost

Section 6.5 — Costed MAX-HEAP-INSERT

This module charges one unit for every visited nonempty-fuel frame of the upward-bubbling controller. Reads, writes, list insertion, allocation, and guards are not separately charged, matching Chapter 6's existing abstract unit-control-step metric rather than claiming RAM costs for Lean lists.

namespace CLRSnamespace Chapter06

Upward bubbling paired with its number of visited control frames.

def arrayHeapIncreaseKeyBubbleUpFuelWithCost : Nat → List Nat → Nat → Nat → List Nat × Nat | 0, a, _heapSize, _i => (a, 0) | fuel + 1, a, heapSize, i => if _ : 0 < i then if valAt a (parent i) < valAt a i then let next := arrayHeapIncreaseKeyBubbleUpFuelWithCost fuel (swapAt a i (parent i)) heapSize (parent i) (next.1, next.2 + 1) else (a, 1) else (a, 1)

Erasing the cost recovers the existing upward-bubbling implementation.

theorem arrayHeapIncreaseKeyBubbleUpFuelWithCost_result (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (arrayHeapIncreaseKeyBubbleUpFuelWithCost fuel a heapSize i).1 = arrayHeapIncreaseKeyBubbleUpFuel fuel a heapSize i := by induction fuel generalizing a i with | zero => simp [arrayHeapIncreaseKeyBubbleUpFuelWithCost, arrayHeapIncreaseKeyBubbleUpFuel] | succ fuel ih => simp only [arrayHeapIncreaseKeyBubbleUpFuelWithCost, arrayHeapIncreaseKeyBubbleUpFuel] split_ifs · exact ih _ _ · rfl · rfl

A zero-based heap parent step drops the binary index level by at least one.

theorem parent_log_add_one_le {i : Nat} (hpos : 0 < i) : Nat.log 2 (parent i + 1) + 1 ≤ Nat.log 2 (i + 1) := by have hmul : 2 * (parent i + 1) ≤ i + 1 := by rcases eq_left_or_right_parent hpos with hleft | hright · unfold left at hleft omega · unfold right at hright omega have hmono : Nat.log 2 (2 * (parent i + 1)) ≤ Nat.log 2 (i + 1) := Nat.log_mono_right hmul have hlogmul : Nat.log 2 (2 * (parent i + 1)) = Nat.log 2 (parent i + 1) + 1 := by rw [Nat.mul_comm 2 (parent i + 1)] exact Nat.log_mul_base (by norm_num) (by omega) rwa [hlogmul] at hmono

Upward bubbling visits at most one frame per binary-index level, including its terminal frame.

theorem arrayHeapIncreaseKeyBubbleUpFuelWithCost_cost_le_log (fuel : Nat) (a : List Nat) (heapSize i : Nat) : (arrayHeapIncreaseKeyBubbleUpFuelWithCost fuel a heapSize i).2 ≤ Nat.log 2 (i + 1) + 1 := by induction fuel generalizing a i with | zero => simp [arrayHeapIncreaseKeyBubbleUpFuelWithCost] | succ fuel ih => simp only [arrayHeapIncreaseKeyBubbleUpFuelWithCost] split_ifs with hpos hswap · have hrec := ih (swapAt a i (parent i)) (parent i) have hdrop := parent_log_add_one_le hpos omega · simp · simp

Full-prefix insertion paired with upward-bubbling control cost.

def arrayHeapInsertWithCost (a : List Nat) (key : Nat) : List Nat × Nat := arrayHeapIncreaseKeyBubbleUpFuelWithCost a.length (a ++ [key]) (a.length + 1) a.length

Erasing full-prefix insertion cost recovers arrayHeapInsert.

theorem arrayHeapInsertWithCost_result (a : List Nat) (key : Nat) : (arrayHeapInsertWithCost a key).1 = arrayHeapInsert a key := by exact arrayHeapIncreaseKeyBubbleUpFuelWithCost_result a.length (a ++ [key]) (a.length + 1) a.length

Full-prefix insertion has an explicit logarithmic control-frame bound.

theorem arrayHeapInsertWithCost_cost_le_log (a : List Nat) (key : Nat) : (arrayHeapInsertWithCost a key).2 ≤ Nat.log 2 (a.length + 1) + 1 := by exact arrayHeapIncreaseKeyBubbleUpFuelWithCost_cost_le_log a.length (a ++ [key]) (a.length + 1) a.length

Checked active-prefix insertion with its upward-bubbling control cost.

def arrayHeapInsertWithCost? (a : List Nat) (heapSize key : Nat) : Option ((List Nat × Nat) × Nat) := if _h : heapSize ≤ a.length then let run := arrayHeapInsertWithCost (a.take heapSize) key some ((run.1 ++ a.drop heapSize, heapSize + 1), run.2) else none

Erasing checked insertion cost recovers the checked state operation.

theorem arrayHeapInsertWithCost?_result (a : List Nat) (heapSize key : Nat) : (arrayHeapInsertWithCost? a heapSize key).map Prod.fst = arrayHeapInsert? a heapSize key := by unfold arrayHeapInsertWithCost? arrayHeapInsert? by_cases h : heapSize ≤ a.length · simp [h, arrayHeapInsertWithCost_result] · simp [h]

The checked costed wrapper inherits the complete state contract and the logarithmic bound in the enlarged heap size.

theorem arrayHeapInsertWithCost?_state_correct_and_log_cost {a rest : List Nat} {heapSize newHeapSize key cost : Nat} (hheap : ArrayMaxHeap a heapSize) (hres : arrayHeapInsertWithCost? a heapSize key = some ((rest, newHeapSize), cost)) : heapSize ≤ a.length ∧ newHeapSize = heapSize + 1 ∧ rest.length = a.length + 1 ∧ ArrayMaxHeap rest newHeapSize ∧ rest.Perm (key :: a) ∧ rest.drop newHeapSize = a.drop heapSize ∧ cost ≤ Nat.log 2 newHeapSize + 1 := by have hraw : arrayHeapInsert? a heapSize key = some (rest, newHeapSize) := by have hmap := congrArg (Option.map Prod.fst) hres rw [arrayHeapInsertWithCost?_result] at hmap simpa using hmap have hstate := arrayHeapInsert?_state_correct hheap hraw rcases hstate with ⟨hguard, hsize, hlength, hresultHeap, hperm, htail⟩ have hcostRun := arrayHeapInsertWithCost_cost_le_log (a.take heapSize) key have htakeLen : (a.take heapSize).length = heapSize := List.length_take_of_le hguard have hcost : cost = (arrayHeapInsertWithCost (a.take heapSize) key).2 := by unfold arrayHeapInsertWithCost? at hres rw [dif_pos hguard] at hres have hall : (rest = (arrayHeapInsertWithCost (a.take heapSize) key).1 ++ a.drop heapSize ∧ newHeapSize = heapSize + 1) ∧ cost = (arrayHeapInsertWithCost (a.take heapSize) key).2 := by simpa only [Option.some.injEq, Prod.mk.injEq] using hres.symm exact hall.2 refine ⟨hguard, hsize, hlength, hresultHeap, hperm, htail, ?_⟩ rw [hcost, hsize] simpa [htakeLen] using hcostRun
end Chapter06end CLRS

Scope and implementation notes

Imports
import CLRSLean.FourthEdition.Chapter_06.Section_06_1_Heaps import CLRSLean.FourthEdition.Chapter_06.Section_06_2_Maintaining_Heap_Property import CLRSLean.FourthEdition.Chapter_06.Section_06_3_Building_A_Heap import CLRSLean.FourthEdition.Chapter_06.Section_06_4_Heapsort import CLRSLean.FourthEdition.Chapter_06.Section_06_4_Heapsort.CostedExecution import CLRSLean.FourthEdition.Chapter_06.Section_06_5_Priority_Queues import CLRSLean.FourthEdition.Chapter_06.Section_06_5_Priority_Queues.Insert

Current source

Sections 6.1--6.5 are native fourth-edition sections (heaps, maintaining the heap property, building a heap, the heapsort algorithm, and priority queues), imported directly from Section 6.1, Section 6.2, Section 6.3, Section 6.4, and Section 6.5. Section 6.4 includes the nested costed-execution development. Declarations retain the CLRS.Chapter06 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_06 and CLRSLean.Chapter_06.Section_06_* forward to these sources.

Implementation details

The supporting implementation page remains available outside the main sidebar:

Coverage boundary

The represented heap and priority-queue correctness developments are reused. ArrayMaxHeapFrom a heapSize start constrains all parent indices at least start, including parents outside its descendant subtree. Heapify repair uses this stronger invariant, which is maintained by bottom-up construction. The storage model uses a persistent backing list; proved execution counters charge controller frames, excluding list traversal/copying, allocation, and imperative RAM costs.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 6 of 35