Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 6. Heapsort
  4. 6.1. Heaps
Browse chapters
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