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:

Array-level MAX-HEAP-INSERT contains focused basic, checked, and costed modules. They isolate the new cell's incoming-edge violation and reuse the established upward-bubbling invariant.
Basic insertion proof
Checked active-prefix proof
Logarithmic cost proof

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