1. CLRS-Lean
  2. Chapter 6. Heapsort
  3. 6.1. Heaps
Imports
import Mathlib

CLRS Section 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.

Current gap:

  • This section proves the mathematical heap predicate and root-maximum fact. The executable MAX-HEAPIFY, BUILD-MAX-HEAP, and HEAPSORT refinements appear in Sections 6.2--6.4.

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) := induction xs with exact hxs w ( ) exact hxs w ( ) exact ih (fun z hz => hxs z ( )) w hwin

Inserting into a descending list preserves descending order.

Descending insertion preserves the elements up to permutation.

theorem insertDesc_perm (x : Nat) (xs : List Nat) : (insertDesc x xs).Perm (x :: xs) := induction xs with

Repeated insertion builds a descending heap.

theorem buildMaxHeap_orderedDesc (xs : List Nat) : OrderedDesc (buildMaxHeap xs) := induction xs with

Building the heap preserves the input elements up to permutation.

theorem buildMaxHeap_perm (xs : List Nat) : (buildMaxHeap xs).Perm xs := induction xs with

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 := cases h with

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

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 := cases h with

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) := cases h with

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 := cases h with

Heapsort returns an ascending list.

theorem heapSort_orderedAsc (xs : List Nat) : OrderedAsc (heapSort xs) :=

Heapsort preserves the input elements up to permutation.

theorem heapSort_perm (xs : List Nat) : (heapSort xs).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 :=

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) :=

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

theorem parent_left (i : Nat) : parent (left i) = i :=

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

theorem parent_right (i : Nat) : parent (right i) = i :=

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 also use a localized heap predicate. It checks only parent nodes whose indices are at least start. This matches the CLRS subtree view: when repairing the subtree rooted at start, edges entering the subtree root from smaller indices are outside the local obligation.

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

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

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

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

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

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

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

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

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

exact Nat.le_trans hedge ( )

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.

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 := exact orderedDesc_getElem_le h ( ; ) (Nat.lt_of_lt_of_le hl hlen) exact orderedDesc_getElem_le h ( ; ) (Nat.lt_of_lt_of_le hr hlen)
end Chapter06end CLRS