1. CLRS-Lean
  2. Chapter 6. Heapsort
  3. 6.5. Priority Queues
Imports
import CLRSLean.Chapter_06.Section_06_4_Heapsort

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

Current gaps:

  • Runtime bounds and RAM semantics are deferred.

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

Priority-queue insertion adds exactly the inserted key.

theorem heapInsert_perm (x : Nat) (h : List Nat) : (heapInsert x h).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 :=

Increasing a key and rebuilding returns a heap.

theorem heapIncreaseKey_orderedDesc (old new : Nat) (h : List Nat) : OrderedDesc (heapIncreaseKey old new h) :=

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

Deleting one key occurrence and rebuilding returns a heap.

theorem heapDelete_orderedDesc (key : Nat) (h : List Nat) : OrderedDesc (heapDelete key h) :=

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

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.

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

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

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.

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

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

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.

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

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 := induction fuel generalizing a i with

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 := induction fuel generalizing a i with exact ( )

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

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

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.

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

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.

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.

end Chapter06end CLRS