Binary heap

DefinitionParent index in a level-order binary tree#✓fully proved

In a binary tree stored in level order in an array indexed from \(0\), the parent index of a natural number \(i\) is \(\lfloor (i-1)/2 \rfloor\), where \(i - 1\) is truncated subtraction of natural numbers, so the root index \(0\) is sent to \(0\).

def heapParent (i : Nat) : Nat := (i - 1) / 2
Used by 29
Used byComparison bound for sift-up · Decrease-key in a binary min-heap · Empty binary min-heap · Heap order on a level-order array · The parent of a valid nonroot index is valid · The heap parent is one level up · Moving the last entry to the root prepares a sift-down · Appending to a heap-ordered array prepares it for sift-up · Counting does not change the result of sift-up · The root of a heap-ordered binary-heap array is minimal · Sift-down restores heap order · Sift-down precondition · Sift-up · Sift-up with comparison and swap counts · Sift-up restores heap order · Sift-up permutes the array · Arrays ready for sift-up · Swap bound for sift-up · Sift-up at an out-of-range index costs nothing · Sift-up at the root costs nothing · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Heap sort preserves multiplicities

DefinitionLeft child index in a level-order binary tree#✓fully proved

In a binary tree stored in level order in an array indexed from \(0\), the left child of the node at index \(i\) has index \(2i + 1\).

def heapLeft (i : Nat) : Nat := 2 * i + 1
Used by 12
Used byThe smaller child lies one level below its parent · Timed child selection returns the smaller child · Sift-down restores heap order · Smaller child · The smaller child has a larger index · The smaller child is a valid index · Sift-down from a leaf costs nothing · Sift-down from an invalid index costs nothing · Cost of child selection · Child selection at a node without children costs nothing · Timed smaller-child selection · Logarithmic event bound for indexed-queue extract-min

DefinitionRight child index in an array-backed binary tree#✓fully proved

In the level-order layout of a binary tree in an array indexed from \(0\), the right child of the node at index \(i\) is at index \(2i + 2\).

def heapRight (i : Nat) : Nat := 2 * i + 2
Used by 16
Used byThe smaller child lies one level below its parent · Timed child selection returns the smaller child · Sift-down makes at most two comparisons per remaining level · Sift-down restores heap order · Sift-down performs at most one swap per remaining level · Smaller child · The smaller child has a larger index · The smaller child is a valid index · Sift-down from a leaf costs nothing · Cost of child selection · Child selection at a node without children costs nothing · Timed smaller-child selection · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremThe parent of a valid nonroot index is valid#✓fully proved

For an array \(a\) of length \(|a|\) and an index \(i\) with \(0 < i < |a|\), the parent index \(\lfloor (i-1)/2 \rfloor\) of \(i\) is also less than \(|a|\).

theorem heapParent_lt_size {α : Type u} (a : Array α) (i : Nat)
    (hi : i < a.size) (hpos : 0 < i) : heapParent i < a.size
Uses 1 · Used by 27
Statement usesParent index in a level-order binary tree
Used byComparison bound for sift-up · Decrease-key in a binary min-heap · Empty binary min-heap · Heap order on a level-order array · Moving the last entry to the root prepares a sift-down · Appending to a heap-ordered array prepares it for sift-up · Counting does not change the result of sift-up · The root of a heap-ordered binary-heap array is minimal · Sift-down restores heap order · Sift-down precondition · Sift-up · Sift-up with comparison and swap counts · Sift-up restores heap order · Sift-up permutes the array · Arrays ready for sift-up · Swap bound for sift-up · Sift-up at an out-of-range index costs nothing · Sift-up at the root costs nothing · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Heap sort preserves multiplicities

DefinitionHeap order on a level-order array#✓fully proved

An array \(a\) over a type with a relation \(\le\), indexed from \(0\), is heap ordered when every entry other than the root is at least its parent entry: for every index \(i\) with \(0 < i < |a|\), where \(|a|\) is the length of \(a\), we have \(a_{\lfloor (i-1)/2 \rfloor} \le a_i\).

def HeapOrdered {α : Type u} [LE α] (a : Array α) : Prop :=
  ∀ i (hi : i < a.size), (hpos : 0 < i) →
    a[heapParent i]'(heapParent_lt_size a i hi hpos) ≤ a[i]
Uses 2 · Used by 30
Statement usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byDecrease-key in a binary min-heap · Decrease-key yields a heap-ordered array · Empty binary min-heap · Binary heap extraction splits off the minimum · Elements after binary heap extraction · The value extracted from a binary min-heap is minimal · Extraction from a binary min-heap leaves a heap-ordered array · Removing the root of a nonempty binary min-heap · Binary min-heap · The binary heap minimum lookup is a lower bound · Moving the last entry to the root prepares a sift-down · Insertion into a binary min-heap · Insertion into a binary min-heap preserves heap order · Appending to a heap-ordered array prepares it for sift-up · The root of a heap-ordered binary-heap array is minimal · Sift-down restores heap order · Sift-up restores heap order · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Heap sort preserves multiplicities

StructureArrays ready for sift-up#✓fully proved

Let \(a\) be an array of length \(|a|\) over a type with a relation \(\le\), indexed from \(0\), and for \(j > 0\) let \(p(j) = \lfloor (j - 1)/2 \rfloor\) be the parent of \(j\). The array \(a\) is ready for sift-up at an index \(i\) when \(i < |a|\), when \(a_{p(j)} \le a_j\) for every \(j \ne i\) with \(0 < j < |a|\), and when, if \(i > 0\), also \(a_{p(i)} \le a_j\) for every \(j\) with \(0 < j < |a|\) and \(p(j) = i\).

structure SiftUpReady {α : Type u} [LE α] (a : Array α) (i : Nat) : Prop where
  index_valid : i < a.size
  ordered_except : ∀ j (hj : j < a.size), (hjpos : 0 < j) → j ≠ i →
    a[heapParent j]'(heapParent_lt_size a j hj hjpos) ≤ a[j]
  parent_below_children : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    heapParent j = i → (hipos : 0 < i) →
    a[heapParent i]'(heapParent_lt_size a i index_valid hipos) ≤ a[j]
Uses 2 · Used by 7
Statement usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byDecrease-key in a binary min-heap · Appending to a heap-ordered array prepares it for sift-up · Sift-up restores heap order · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key

StructureSift-down precondition#✓fully proved

For an array \(a\) over a type ordered by \(\le\), write \(p(j) = \lfloor (j-1)/2 \rfloor\) for the parent of index \(j\). The array \(a\) is ready for sift-down at index \(i\) when \(i\) is a valid index of \(a\); \(a_{p(j)} \le a_j\) for every valid index \(j > 0\) with \(p(j) \ne i\); and, if \(i > 0\), \(a_{p(i)} \le a_j\) for every valid index \(j > 0\) with \(p(j) = i\).

Thus the only edges that may violate heap order are those leaving \(i\), and moving either child of \(i\) up to position \(i\) keeps the edge entering \(i\) ordered.

structure SiftDownReady {α : Type u} [LE α] (a : Array α) (i : Nat) : Prop where
  index_valid : i < a.size
  ordered_except : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    heapParent j ≠ i →
    a[heapParent j]'(heapParent_lt_size a j hj hjpos) ≤ a[j]
  parent_below_children : ∀ j (hj : j < a.size), (hjpos : 0 < j) →
    heapParent j = i → (hipos : 0 < i) →
    a[heapParent i]'(heapParent_lt_size a i index_valid hipos) ≤ a[j]
Uses 2 · Used by 2
Statement usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byMoving the last entry to the root prepares a sift-down · Sift-down restores heap order

DefinitionSmaller child#✓fully proved

Let \(a\) be an array of length \(|a|\) over a linearly ordered type, indexed from \(0\), and let \(i\) be an index with children \(\ell = 2i + 1\) and \(r = 2i + 2\). If \(\ell \ge |a|\), then \(i\) has no smaller child. Otherwise the smaller child of \(i\) is \(r\) when \(r < |a|\) and \(a_r < a_\ell\), and \(\ell\) in every other case, so ties go to the left child.

def smallerChild {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) : Option Nat :=
  if hl : heapLeft i < a.size then
    if hr : heapRight i < a.size then
      if a[heapRight i] < a[heapLeft i] then
        some (heapRight i)
      else
        some (heapLeft i)
    else
      some (heapLeft i)
  else
    none
Uses 2 · Used by 19
Statement usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used byThe smaller child lies one level below its parent · The smaller child's level is bounded by the array size · Timed sift-down returns the sift-down result · Timed child selection returns the smaller child · Sift-down · Sift-down with comparison and swap counts · Sift-down makes at most two comparisons per remaining level · Sift-down restores heap order · Binary-heap sift-down permutes the array · Sift-down performs at most one swap per remaining level · The smaller child has a larger index · The smaller child is a valid index · Sift-down from a leaf costs nothing · Sift-down from a node without children costs nothing · Child selection at a node without children costs nothing · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremThe smaller child has a larger index#✓fully proved

For every array \(a\) over a linearly ordered type and all indices \(i\) and \(c\), if \(c\) is the smaller child of \(i\) in \(a\), then \(i < c\).

theorem smallerChild_gt {α : Type u} [LinearOrder α]
    (a : Array α) (i c : Nat)
    (h : smallerChild a i = some c) : i < c
Uses 3 · Used by 13
Statement usesSmaller child
Proof usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used byThe smaller child lies one level below its parent · Timed sift-down returns the sift-down result · Sift-down · Sift-down with comparison and swap counts · Sift-down makes at most two comparisons per remaining level · Sift-down restores heap order · Binary-heap sift-down permutes the array · Sift-down performs at most one swap per remaining level · Sift-down from a node without children costs nothing · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremThe smaller child is a valid index#✓fully proved

For every array \(a\) over a linearly ordered type and all indices \(i\) and \(c\), if \(c\) is the smaller child of \(i\) in \(a\), then \(c\) is less than the length \(|a|\) of \(a\).

theorem smallerChild_valid {α : Type u} [LinearOrder α]
    (a : Array α) (i c : Nat)
    (h : smallerChild a i = some c) : c < a.size
Uses 3 · Used by 13
Statement usesSmaller child
Proof usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used byThe smaller child's level is bounded by the array size · Timed sift-down returns the sift-down result · Sift-down · Sift-down with comparison and swap counts · Sift-down makes at most two comparisons per remaining level · Sift-down restores heap order · Binary-heap sift-down permutes the array · Sift-down performs at most one swap per remaining level · Sift-down from a node without children costs nothing · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

DefinitionSift-up#✓fully proved

Given an array \(a\) of length \(|a|\) over a linearly ordered type, indexed from \(0\), and an index \(i\), the sift-up of \(a\) from \(i\) is defined by recursion on \(i\). If \(i = 0\) or \(i \ge |a|\), the result is \(a\). Otherwise let \(p = \lfloor (i - 1)/2 \rfloor\) be the parent of \(i\); if \(a_i < a_p\), the result is the sift-up from \(p\) of the array obtained from \(a\) by exchanging the entries at positions \(i\) and \(p\), and otherwise the result is \(a\).

Cslib.Algorithms.Lean.siftUp · 15 lines 
def siftUp {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) : Array α :=
  if hi : i < a.size then
    if hpos : 0 < i then
      let p := heapParent i
      if hlt : a[i] < a[p]'(heapParent_lt_size a i hi hpos) then
        siftUp (a.swap i p hi (heapParent_lt_size a i hi hpos)) p
      else
        a
    else
      a
  else
    a
termination_by i
decreasing_by
  exact heapParent_lt i hpos
Uses 2 · Used by 26
Statement usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byDecrease-key in a binary min-heap · Array of a binary heap after decrease-key · Multiset of a binary heap after decrease-key · Decrease-key preserves the heap size · Elements after binary heap insertion · Insertion into a binary min-heap · Counting does not change the result of sift-up · Binary-heap sift-up preserves the multiset of entries · Sift-up restores heap order · Sift-up permutes the array · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Event bound for building an indexed queue by repeated insertion · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm

DefinitionSift-down#✓fully proved

Sifting down an array \(a\) over a linearly ordered type from index \(i\) works as follows. If \(i\) has a child in \(a\), that is, if \(2i+1\) is a valid index, let \(c\) be the child of \(i\) (among \(2i+1\) and \(2i+2\), if valid) holding the smaller value, preferring the left child \(2i+1\) on ties. If \(a_c < a_i\), swap the entries at \(i\) and \(c\) and continue sifting down from \(c\); otherwise, or if \(i\) has no child, return the array unchanged.

Cslib.Algorithms.Lean.siftDown · 15 lines 
def siftDown {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) : Array α :=
  match hchild : smallerChild a i with
  | none => a
  | some c =>
    have hc : c < a.size := smallerChild_valid a i c hchild
    have hi : i < a.size := (smallerChild_gt a i c hchild).trans hc
    if hlt : a[c] < a[i] then
      siftDown (a.swap i c hi hc) c
    else
      a
termination_by a.size - i
decreasing_by
  simp only [Array.size_swap]
  have := smallerChild_gt a i c hchild
  omega
Uses 3 · Used by 11
Statement usesSmaller child · The smaller child has a larger index · The smaller child is a valid index
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Removing the root of a nonempty binary min-heap · Timed sift-down returns the sift-down result · Binary-heap sift-down preserves the multiset of entries · Sift-down restores heap order · Binary-heap sift-down permutes the array · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremSift-up permutes the array#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the array obtained by sifting up \(a\) from \(i\) is a permutation of \(a\).

theorem siftUp_perm {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftUp a i).Perm a
Uses 3 · Used by 18
Statement usesSift-up
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byDecrease-key preserves the heap size · Elements after binary heap insertion · Binary-heap sift-up preserves the multiset of entries · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Event bound for building an indexed queue by repeated insertion · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree

TheoremBinary-heap sift-down permutes the array#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the array obtained by sifting down \(a\) from \(i\) is a permutation of \(a\).

theorem siftDown_perm {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftDown a i).Perm a
Uses 4 · Used by 7
Statement usesSift-down
Proof usesSmaller child · The smaller child has a larger index · The smaller child is a valid index
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Binary-heap sift-down preserves the multiset of entries · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremBinary-heap sift-up preserves the multiset of entries#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the array obtained by sifting up \(a\) from \(i\) has the same multiset of entries as \(a\).

theorem siftUp_multiset {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (↑(siftUp a i).toList : Multiset α) = (↑a.toList : Multiset α)
Uses 2 · Used by 1
Statement usesSift-up
Proof usesSift-up permutes the array
Used byMultiset of a binary heap after decrease-key

TheoremBinary-heap sift-down preserves the multiset of entries#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the array obtained by sifting down \(a\) from \(i\) has the same multiset of entries as \(a\).

theorem siftDown_multiset {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (↑(siftDown a i).toList : Multiset α) = (↑a.toList : Multiset α)
Uses 2
Statement usesSift-down
Proof usesBinary-heap sift-down permutes the array

TheoremThe root of a heap-ordered binary-heap array is minimal#✓fully proved

If an array \(a\) over a linearly ordered type is heap-ordered, then \(a_0 \le a_i\) for every valid index \(i\) of \(a\).

theorem HeapOrdered.root_le {α : Type u} [LinearOrder α] {a : Array α}
    (h : HeapOrdered a) (i : Nat) (hi : i < a.size) :
    a[0]'(by omega) ≤ a[i]
Uses 3 · Used by 2
Statement usesHeap order on a level-order array
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byThe value extracted from a binary min-heap is minimal · The binary heap minimum lookup is a lower bound

TheoremSift-up restores heap order#✓fully proved

Let \(a\) be an array over a linearly ordered type and let \(i\) be an index such that \(a\) is ready for sift-up at \(i\). Then the array obtained by sifting up \(a\) from \(i\) is heap ordered.

theorem siftUp_ordered {α : Type u} [LinearOrder α] (a : Array α) (i : Nat)
    (h : SiftUpReady a i) : HeapOrdered (siftUp a i)
Uses 5 · Used by 6
Statement usesHeap order on a level-order array · Arrays ready for sift-up · Sift-up
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byDecrease-key in a binary min-heap · Insertion into a binary min-heap · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key

TheoremSift-down restores heap order#✓fully proved

Let \(a\) be an array over a linearly ordered type that satisfies the sift-down precondition at a valid index \(i\): the only edges that may violate heap order are those leaving \(i\), and moving either child of \(i\) up to position \(i\) keeps the edge entering \(i\) ordered. Then the array obtained by sifting down \(a\) from \(i\) is heap-ordered.

theorem siftDown_ordered {α : Type u} [LinearOrder α] (a : Array α) (i : Nat)
    (h : SiftDownReady a i) : HeapOrdered (siftDown a i)
Uses 10 · Used by 7
Statement usesHeap order on a level-order array · Sift-down precondition · Sift-down
Proof usesLeft child index in a level-order binary tree · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Right child index in an array-backed binary tree · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Removing the root of a nonempty binary min-heap · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremAppending to a heap-ordered array prepares it for sift-up#✓fully proved

If an array \(a\) of length \(n\) over a linearly ordered type is heap-ordered and \(x\) is any value, then the array obtained by appending \(x\) to \(a\) satisfies the sift-up precondition at index \(n\), the position of \(x\): the only edge that may violate heap order is the one entering index \(n\).

theorem push_siftUpReady {α : Type u} [LinearOrder α] (a : Array α)
    (h : HeapOrdered a) (x : α) : SiftUpReady (a.push x) a.size
Uses 4 · Used by 1
Statement usesHeap order on a level-order array · Arrays ready for sift-up
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byInsertion into a binary min-heap

StructureBinary min-heap#✓fully proved

A binary min-heap over a linearly ordered type \(\alpha\) is an array \(a\) of elements of \(\alpha\) (its level-order storage), of length \(|a|\) and with entries \(a_0, \dots, a_{|a|-1}\), that is heap ordered: for every index \(i\) with \(0 < i < |a|\), the entry \(a_{\lfloor (i - 1)/2 \rfloor}\) at the parent index of \(i\) is at most \(a_i\).

structure MinHeap (α : Type u) [LinearOrder α] where
  /-- The level-order storage array. -/
  data : Array α
  ordered : HeapOrdered data
Uses 1 · Used by 72
Statement usesHeap order on a level-order array
Used byBinary heap insertion leaves other multiplicities unchanged · Binary heap insertion adds one copy of the inserted value · Decrease-key in a binary min-heap · Array of a binary heap after decrease-key · Multiset of a binary heap after decrease-key · Decrease-key yields a heap-ordered array · Decrease-key preserves the heap size · Elements of a binary min-heap · Elements after binary heap insertion · Empty binary min-heap · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Binary heap extraction removes one copy of the minimum · Binary heap extraction leaves other multiplicities unchanged · Elements after binary heap extraction · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Membership after extraction from a binary min-heap · Extraction from a binary min-heap leaves a heap-ordered array · Removing the root of a nonempty binary min-heap · Minimum lookup in a binary heap · Binary heap minimum lookup fails exactly when empty · Binary heap minimum lookup succeeds exactly when nonempty · The binary heap minimum lookup is a lower bound · The binary heap minimum lookup returns a stored element · Insertion into a binary min-heap · Insertion into a binary min-heap preserves heap order · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Empty indexed minimum queue · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min · Indexed minimum queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Absent identities carry no heap entry · Recorded positions lie inside the heap · Event bound for building an indexed queue by repeated insertion · Prim's algorithm with an indexed binary heap · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · Parents returned by Prim's algorithm are adjacency-list neighbors · The root has no parent in Prim's algorithm · Heap sort · Heap sort preserves multiplicities · Heap sort output is sorted · Extracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Heap of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop invariant · Indexed reads of a successful Huffman loop · Huffman loop with lookup count · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Discarding the lookup count recovers the Huffman loop · Huffman's construction follows a two-minimum merge trace · Result of a two-minimum extraction · Huffman's construction keeps the weighted leaves

DefinitionElements of a binary min-heap#✓fully proved

The multiset of elements of a binary min-heap is the multiset of the entries of its level-order storage array, counted with multiplicity.

def MinHeap.elements {α : Type u} [LinearOrder α] (h : MinHeap α) : Multiset α :=
  h.data.toList
Uses 1 · Used by 29
Statement usesBinary min-heap
Used byBinary heap insertion leaves other multiplicities unchanged · Binary heap insertion adds one copy of the inserted value · Multiset of a binary heap after decrease-key · Elements after binary heap insertion · Binary heap extraction splits off the minimum · Binary heap extraction removes one copy of the minimum · Binary heap extraction leaves other multiplicities unchanged · Elements after binary heap extraction · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Membership after extraction from a binary min-heap · The binary heap minimum lookup is a lower bound · The binary heap minimum lookup returns a stored element · Successful extraction from an indexed min queue · Successful insertion into an indexed min queue · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Heap sort preserves multiplicities · Heap sort output is sorted · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman loop invariant · Huffman's construction follows a two-minimum merge trace

DefinitionEmpty binary min-heap#✓fully proved

The empty binary min-heap is the min-heap whose level-order storage array has no entries.

def MinHeap.empty {α : Type u} [LinearOrder α] : MinHeap α where
  data := #[]
  ordered := by simp [HeapOrdered]
Uses 4 · Used by 14
Statement usesHeap order on a level-order array · Binary min-heap · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Removing the root of a nonempty binary min-heap · Empty indexed minimum queue · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min · Heap sort · Heap sort preserves multiplicities · Heap sort output is sorted · Heap of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

DefinitionInsertion into a binary min-heap#✓fully proved

To insert a value \(x\) into a binary min-heap \(h\), append \(x\) at the end of the level-order array of \(h\) and sift it up from its index (the old length of the array), repeatedly swapping it with its parent while it is smaller. The result is again a binary min-heap.

def MinHeap.push {α : Type u} [LinearOrder α] (h : MinHeap α) (x : α) : MinHeap α where
  data := siftUp (h.data.push x) h.data.size
  ordered := siftUp_ordered _ _ (push_siftUpReady h.data h.ordered x)
Uses 5 · Used by 26
Statement usesHeap order on a level-order array · Binary min-heap · Appending to a heap-ordered array prepares it for sift-up · Sift-up · Sift-up restores heap order
Used byBinary heap insertion leaves other multiplicities unchanged · Binary heap insertion adds one copy of the inserted value · Elements after binary heap insertion · Insertion into a binary min-heap preserves heap order · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Event bound for building an indexed queue by repeated insertion · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Heap sort · Heap sort preserves multiplicities · Heap sort output is sorted · Heap of a Huffman work forest · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

DefinitionMinimum lookup in a binary heap#✓fully proved

For a binary min-heap \(h\), the minimum lookup returns the entry at index \(0\) (the root) of the storage array of \(h\) when that array is nonempty, and returns no value when it is empty.

def MinHeap.min? {α : Type u} [LinearOrder α] (h : MinHeap α) : Option α :=
  h.data[0]?
Uses 1 · Used by 4
Statement usesBinary min-heap
Used byBinary heap minimum lookup fails exactly when empty · Binary heap minimum lookup succeeds exactly when nonempty · The binary heap minimum lookup is a lower bound · The binary heap minimum lookup returns a stored element

TheoremBinary heap minimum lookup fails exactly when empty#✓fully proved

For a binary min-heap \(h\) over a linearly ordered type, looking up the minimum of \(h\) returns no value if and only if the storage array of \(h\) has size \(0\).

theorem MinHeap.min?_eq_none_iff {α : Type u} [LinearOrder α] (h : MinHeap α) :
    h.min? = none ↔ h.data.size = 0
Uses 2
Statement usesBinary min-heap · Minimum lookup in a binary heap

TheoremBinary heap minimum lookup succeeds exactly when nonempty#✓fully proved

For a binary min-heap \(h\) over a linearly ordered type, looking up the minimum of \(h\) returns a value if and only if the storage array of \(h\) has positive size.

theorem MinHeap.min?_isSome_iff {α : Type u} [LinearOrder α] (h : MinHeap α) :
    h.min?.isSome ↔ 0 < h.data.size
Uses 2
Statement usesBinary min-heap · Minimum lookup in a binary heap

TheoremThe binary heap minimum lookup returns a stored element#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If looking up the minimum of \(h\) returns \(x\), then \(x\) belongs to the multiset of elements of \(h\).

theorem MinHeap.min?_mem {α : Type u} [LinearOrder α] {h : MinHeap α} {x : α}
    (hx : h.min? = some x) : x ∈ h.elements
Uses 3
Statement usesBinary min-heap · Elements of a binary min-heap · Minimum lookup in a binary heap

TheoremThe binary heap minimum lookup is a lower bound#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If looking up the minimum of \(h\) returns \(x\), then \(x \le y\) for every element \(y\) of the multiset of elements of \(h\).

theorem MinHeap.min?_le {α : Type u} [LinearOrder α] {h : MinHeap α} {x y : α}
    (hx : h.min? = some x) (hy : y ∈ h.elements) : x ≤ y
Uses 5
Statement usesBinary min-heap · Elements of a binary min-heap · Minimum lookup in a binary heap
Proof usesHeap order on a level-order array · The root of a heap-ordered binary-heap array is minimal

TheoremElements after binary heap insertion#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type and \(x\) a value. The multiset of elements of the heap obtained by inserting \(x\) into \(h\) is the multiset of elements of \(h\) with one more copy of \(x\) added.

theorem MinHeap.elements_push {α : Type u} [LinearOrder α] (h : MinHeap α) (x : α) :
    (h.push x).elements = x ::ₘ h.elements
Uses 5 · Used by 13
Statement usesBinary min-heap · Elements of a binary min-heap · Insertion into a binary min-heap
Proof usesSift-up · Sift-up permutes the array
Used byBinary heap insertion leaves other multiplicities unchanged · Binary heap insertion adds one copy of the inserted value · Successful insertion into an indexed min queue · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Heap sort preserves multiplicities · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremBinary heap insertion adds one copy of the inserted value#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type and \(x\) a value. The multiplicity of \(x\) in the multiset of elements of the heap obtained by inserting \(x\) into \(h\) is one more than its multiplicity in the multiset of elements of \(h\).

theorem MinHeap.count_push_self {α : Type u} [LinearOrder α]
    (h : MinHeap α) (x : α) :
    Multiset.count x (h.push x).elements = Multiset.count x h.elements + 1
Uses 4
Statement usesBinary min-heap · Elements of a binary min-heap · Insertion into a binary min-heap
Proof usesElements after binary heap insertion

TheoremBinary heap insertion leaves other multiplicities unchanged#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, and let \(x \ne y\) be values. Then \(y\) occurs in the multiset of elements of the heap obtained by inserting \(x\) into \(h\) exactly as many times as it occurs in the multiset of elements of \(h\).

theorem MinHeap.count_push_of_ne {α : Type u} [LinearOrder α]
    (h : MinHeap α) {x y : α} (hyx : y ≠ x) :
    Multiset.count y (h.push x).elements = Multiset.count y h.elements
Uses 4
Statement usesBinary min-heap · Elements of a binary min-heap · Insertion into a binary min-heap
Proof usesElements after binary heap insertion

TheoremInsertion into a binary min-heap preserves heap order#✓fully proved

For every binary min-heap \(h\) over a linearly ordered type and every value \(x\), the level-order array of the heap obtained by inserting \(x\) into \(h\) is heap-ordered: the entry at every nonroot index \(i\) is at least the entry at its parent index \(\lfloor (i-1)/2 \rfloor\).

theorem MinHeap.push_ordered {α : Type u} [LinearOrder α] (h : MinHeap α) (x : α) :
    HeapOrdered (h.push x).data
Uses 3
Statement usesHeap order on a level-order array · Binary min-heap · Insertion into a binary min-heap

DefinitionMoving the last entry to the root#✓fully proved

For a nonempty array \(a\) of length \(n\), this operation swaps the entries at indices \(0\) and \(n - 1\) and then deletes the final entry. The result has length \(n - 1\); when \(n \ge 2\) its entry at index \(0\) is \(a_{n-1}\) and its entry at each index \(0 < i < n - 1\) is \(a_i\).

def moveLastToRoot {α : Type u} (a : Array α) (hne : 0 < a.size) : Array α :=
  (a.swap 0 (a.size - 1) hne (by omega)).pop
Used by 9
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Removing the root of a nonempty binary min-heap · Moving the last entry to the root removes the old root · Moving the last entry to the root prepares a sift-down · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremMoving the last entry to the root prepares a sift-down#✓fully proved

Let \(a\) be a heap-ordered array over a linearly ordered type with at least two entries, and let \(b\) be the array obtained from \(a\) by moving its last entry to the root. Then \(b\) is ready for sifting down at index \(0\): index \(0\) is valid in \(b\), and for every index \(j > 0\) of \(b\) whose parent index \(\lfloor (j - 1)/2 \rfloor\) is not \(0\), the entry of \(b\) at the parent index is at most \(b_j\).

theorem moveLastToRoot_siftDownReady {α : Type u} [LinearOrder α]
    (a : Array α) (h : HeapOrdered a) (htwo : 1 < a.size) :
    SiftDownReady (moveLastToRoot a (by omega)) 0
Uses 5 · Used by 7
Statement usesHeap order on a level-order array · Sift-down precondition · Moving the last entry to the root
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byBinary heap extraction splits off the minimum · Elements after binary heap extraction · Removing the root of a nonempty binary min-heap · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

TheoremMoving the last entry to the root removes the old root#✓fully proved

For a nonempty array \(a\) over a linearly ordered type, the multiset of entries of the array obtained from \(a\) by moving its last entry to the root equals the multiset of entries of \(a\) with one occurrence of \(a_0\) removed.

theorem moveLastToRoot_elements {α : Type u} [LinearOrder α]
    (a : Array α) (hne : 0 < a.size) :
    (↑(moveLastToRoot a hne).toList : Multiset α) =
      (↑a.toList : Multiset α).erase (a[0]'hne)
Uses 1 · Used by 1
Statement usesMoving the last entry to the root
Used byElements after binary heap extraction

DefinitionRemoving the root of a nonempty binary min-heap#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type whose level-order array is nonempty. If the array has exactly one entry, the result is the empty heap. Otherwise the last entry of the array replaces the root, the array shrinks by one, and the result is the heap obtained by sifting this entry down from the root.

def MinHeap.extractTail {α : Type u} [LinearOrder α]
    (h : MinHeap α) (hne : 0 < h.data.size) : MinHeap α :=
  if hone : h.data.size = 1 then
    MinHeap.empty
  else
    have htwo : 1 < h.data.size := by omega
    let moved := moveLastToRoot h.data hne
    ⟨siftDown moved 0,
      siftDown_ordered moved 0
        (moveLastToRoot_siftDownReady h.data h.ordered htwo)⟩
Uses 7 · Used by 10
Statement usesHeap order on a level-order array · Binary min-heap · Empty binary min-heap · Moving the last entry to the root · Moving the last entry to the root prepares a sift-down · Sift-down · Sift-down restores heap order
Used byExtracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · Elements after binary heap extraction · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min

DefinitionExtracting the minimum of a binary min-heap#✓fully proved

For a binary min-heap \(h\) over a linearly ordered type, extraction returns nothing when the level-order array of \(h\) is empty. Otherwise it returns the root entry (the first entry of the array) together with the heap obtained from \(h\) by removing its root and restoring heap order.

def MinHeap.extractMin {α : Type u} [LinearOrder α]
    (h : MinHeap α) : Option (α × MinHeap α) :=
  if hne : 0 < h.data.size then
    some (h.data[0]'hne, h.extractTail hne)
  else
    none
Uses 2 · Used by 29
Statement usesBinary min-heap · Removing the root of a nonempty binary min-heap
Used byBinary heap extraction splits off the minimum · Binary heap extraction removes one copy of the minimum · Binary heap extraction leaves other multiplicities unchanged · Elements after binary heap extraction · Extraction from a binary min-heap fails exactly when it is empty · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Membership after extraction from a binary min-heap · Extraction from a binary min-heap leaves a heap-ordered array · Successful extraction from an indexed min queue · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Heap sort · Heap sort preserves multiplicities · Heap sort output is sorted · Extracting two minima from a Huffman heap · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Huffman's construction succeeds on nonempty inputs with distinct symbols · Bounded Huffman merge loop · Huffman loop with an accumulated lookup count · Lookup count of the instrumented Huffman loop · Huffman's construction follows a two-minimum merge trace · Huffman's construction keeps the weighted leaves

TheoremExtraction from a binary min-heap fails exactly when it is empty#✓fully proved

For a binary min-heap \(h\) over a linearly ordered type, extracting the minimum of \(h\) returns no result if and only if the level-order storage array of \(h\) has size \(0\).

theorem MinHeap.extractMin_eq_none_iff {α : Type u} [LinearOrder α]
    (h : MinHeap α) : h.extractMin = none ↔ h.data.size = 0
Uses 3 · Used by 3
Statement usesBinary min-heap · Extracting the minimum of a binary min-heap
Proof usesRemoving the root of a nonempty binary min-heap
Used byHeap sort preserves multiplicities · Heap sort output is sorted · Huffman's construction succeeds on nonempty inputs with distinct symbols

TheoremThe value extracted from a binary min-heap is one of its elements#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds and returns a value \(x\) together with a heap \(r\), then \(x\) belongs to the multiset of elements of \(h\).

theorem MinHeap.extractMin_mem {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) : x ∈ h.elements
Uses 4 · Used by 8
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesRemoving the root of a nonempty binary min-heap
Used byAdjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Huffman's construction succeeds on nonempty inputs with distinct symbols

TheoremThe value extracted from a binary min-heap is minimal#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds and returns a value \(x\) together with a heap \(r\), then \(x \le y\) for every value \(y\) in the multiset of elements of \(h\).

theorem MinHeap.extractMin_le {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x y : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) (hy : y ∈ h.elements) : x ≤ y
Uses 6 · Used by 6
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesHeap order on a level-order array · The root of a heap-ordered binary-heap array is minimal · Removing the root of a nonempty binary min-heap
Used byPrim's algorithm returns a tree · Prim's algorithm returns a minimum spanning tree · The root has no parent in Prim's algorithm · Heap sort preserves multiplicities · Heap sort output is sorted · Two-minimum extraction is greedy

TheoremElements after binary heap extraction#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum of \(h\) succeeds and returns the value \(x\) and the heap \(h'\), then the multiset of elements of \(h'\) is obtained from the multiset of elements of \(h\) by erasing one occurrence of \(x\).

theorem MinHeap.extractMin_elements {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    rest.elements = h.elements.erase x
Uses 12
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesHeap order on a level-order array · Empty binary min-heap · Removing the root of a nonempty binary min-heap · Moving the last entry to the root · Moving the last entry to the root removes the old root · Moving the last entry to the root prepares a sift-down · Sift-down · Sift-down restores heap order · Binary-heap sift-down permutes the array

TheoremBinary heap extraction splits off the minimum#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum of \(h\) succeeds and returns the value \(x\) and the heap \(h'\), then the multiset of elements of \(h\) equals the multiset of elements of \(h'\) with one copy of \(x\) added.

The statement is phrased by adding \(x\) back, not by erasing it from the multiset of \(h\).

theorem MinHeap.extractMin_cons_elements {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    x ::ₘ rest.elements = h.elements
Uses 11 · Used by 15
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesHeap order on a level-order array · Empty binary min-heap · Removing the root of a nonempty binary min-heap · Moving the last entry to the root · Moving the last entry to the root prepares a sift-down · Sift-down · Sift-down restores heap order · Binary-heap sift-down permutes the array
Used byBinary heap extraction removes one copy of the minimum · Binary heap extraction leaves other multiplicities unchanged · Membership after extraction from a binary min-heap · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · Heap sort preserves multiplicities · Heap sort output is sorted · Extracting two minima preserves the heap's elements · Two-minimum extraction is greedy · Huffman's construction succeeds on nonempty inputs with distinct symbols · Huffman's construction follows a two-minimum merge trace

TheoremBinary heap extraction removes one copy of the minimum#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum of \(h\) succeeds and returns the value \(x\) and the heap \(h'\), then the multiplicity of \(x\) in the multiset of elements of \(h'\) is its multiplicity in the multiset of elements of \(h\) minus one.

theorem MinHeap.extractMin_count {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) :
    Multiset.count x rest.elements = Multiset.count x h.elements - 1
Uses 4
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesBinary heap extraction splits off the minimum

TheoremBinary heap extraction leaves other multiplicities unchanged#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum of \(h\) succeeds and returns the value \(x\) and the heap \(h'\), then every value \(y \ne x\) occurs in the multiset of elements of \(h'\) exactly as many times as in the multiset of elements of \(h\).

theorem MinHeap.extractMin_count_of_ne {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x y : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) (hyx : y ≠ x) :
    Multiset.count y rest.elements = Multiset.count y h.elements
Uses 4
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesBinary heap extraction splits off the minimum

TheoremMembership after extraction from a binary min-heap#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, and suppose extracting the minimum from \(h\) succeeds and returns a value \(x\) together with a heap \(r\). Then every value \(y \ne x\) is an element of \(r\) if and only if it is an element of \(h\).

theorem MinHeap.extractMin_mem_of_ne_iff {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x y : α} {rest : MinHeap α}
    (hx : h.extractMin = some (x, rest)) (hyx : y ≠ x) :
    y ∈ rest.elements ↔ y ∈ h.elements
Uses 4 · Used by 3
Statement usesBinary min-heap · Elements of a binary min-heap · Extracting the minimum of a binary min-heap
Proof usesBinary heap extraction splits off the minimum
Used bySuccessful extraction from an indexed min queue · Prim's algorithm returns a tree · Prim's algorithm returns a minimum spanning tree

TheoremExtraction from a binary min-heap leaves a heap-ordered array#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type. If extracting the minimum from \(h\) succeeds and returns a value \(x\) together with a heap \(r\), then the level-order array of \(r\) is heap ordered: every entry other than the root is at least its parent entry.

theorem MinHeap.extractMin_ordered {α : Type u} [LinearOrder α]
    {h : MinHeap α} {x : α} {rest : MinHeap α}
    (_hx : h.extractMin = some (x, rest)) : HeapOrdered rest.data
Uses 3
Statement usesHeap order on a level-order array · Binary min-heap · Extracting the minimum of a binary min-heap

TheoremThe heap parent is one level up#✓fully proved

For every natural number \(i > 0\), the parent index \(p = \lfloor (i-1)/2 \rfloor\) satisfies \(\lfloor \log_2(p+1) \rfloor + 1 = \lfloor \log_2(i+1) \rfloor\); that is, in the level-order binary tree the parent of a nonroot index lies one level above it.

theorem log2_heapParent_add_one (i : Nat) (hi : 0 < i) :
    Nat.log2 (heapParent i + 1) + 1 = Nat.log2 (i + 1)
Uses 1 · Used by 2
Statement usesParent index in a level-order binary tree
Used byComparison bound for sift-up · Swap bound for sift-up

DefinitionSift-up with comparison and swap counts#✓fully proved

Given an array \(a\) of length \(|a|\) over a linearly ordered type and an index \(i\), this computes the sift-up of \(a\) at \(i\) together with a cost \((c, s) \in \mathbb{N} \times \mathbb{N}\), where \(c\) counts value comparisons and \(s\) counts swaps. If \(i \ge |a|\) or \(i = 0\), the result is \(a\) with cost \((0, 0)\). Otherwise let \(p = \lfloor (i - 1)/2 \rfloor\) be the parent of \(i\). If \(a_i < a_p\), the result is this sift-up at \(p\) of the array obtained from \(a\) by exchanging the entries at positions \(i\) and \(p\), with cost \((1, 1)\) plus the cost of that recursive sift-up; otherwise the result is \(a\) with cost \((1, 0)\).

Cslib.Algorithms.Lean.TimeM.siftUp · 19 lines 
def siftUp {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    TimeM (Nat × Nat) (Array α) :=
  if hi : i < a.size then
    if hpos : 0 < i then do
      tick (1, 0)
      let p := heapParent i
      if a[i] < a[p]'(heapParent_lt_size a i hi hpos) then do
        tick (0, 1)
        siftUp (a.swap i p hi (heapParent_lt_size a i hi hpos)) p
      else
        pure a
    else
      pure a
  else
    pure a
termination_by i
decreasing_by
  unfold heapParent
  omega
Uses 2 · Used by 6
Statement usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid
Used byComparison bound for sift-up · Combined comparison and swap bound for sift-up · Counting does not change the result of sift-up · Swap bound for sift-up · Sift-up at an out-of-range index costs nothing · Sift-up at the root costs nothing

TheoremCounting does not change the result of sift-up#✓fully proved

For every array \(a\) over a linearly ordered type and every natural number \(i\), the array returned by sift-up with comparison and swap counts on \(a\) at index \(i\) equals the array returned by the plain sift-up of \(a\) at \(i\).

theorem ret_siftUp {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftUp a i).ret = Cslib.Algorithms.Lean.siftUp a i
Uses 4
Statement usesSift-up with comparison and swap counts · Sift-up
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid

TheoremComparison bound for sift-up#✓fully proved

For every array \(a\) over a linearly ordered type and every natural number \(i\), the number of value comparisons counted by sift-up with comparison and swap counts on \(a\) at index \(i\) is at most \(\lfloor \log_2(i+1) \rfloor\), the depth of index \(i\) in the level-order binary tree.

theorem comparisons_siftUp_le_log2 {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) : (siftUp a i).time.1 ≤ Nat.log2 (i + 1)
Uses 4 · Used by 1
Statement usesSift-up with comparison and swap counts
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid · The heap parent is one level up
Used byCombined comparison and swap bound for sift-up

TheoremSwap bound for sift-up#✓fully proved

For every array \(a\) over a linearly ordered type and every natural number \(i\), the number of swaps counted by sift-up with comparison and swap counts on \(a\) at index \(i\) is at most \(\lfloor \log_2(i+1) \rfloor\), the depth of index \(i\) in the level-order binary tree.

theorem swaps_siftUp_le_log2 {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) : (siftUp a i).time.2 ≤ Nat.log2 (i + 1)
Uses 4 · Used by 1
Statement usesSift-up with comparison and swap counts
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid · The heap parent is one level up
Used byCombined comparison and swap bound for sift-up

TheoremCombined comparison and swap bound for sift-up#✓fully proved

For every array \(a\) over a linearly ordered type and every natural number \(i\), if sift-up with comparison and swap counts on \(a\) at index \(i\) counts \(c\) comparisons and \(s\) swaps, then \(c + s \le 2 \lfloor \log_2(i+1) \rfloor\).

theorem events_siftUp_le_log2 {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftUp a i).time.1 + (siftUp a i).time.2 ≤ 2 * Nat.log2 (i + 1)
Uses 3
Statement usesSift-up with comparison and swap counts
Proof usesComparison bound for sift-up · Swap bound for sift-up

TheoremSift-up at the root costs nothing#✓fully proved

For every array \(a\) over a linearly ordered type, sift-up with comparison and swap counts on \(a\) at index \(0\) has cost \((0, 0)\): it counts no comparisons and no swaps.

theorem time_siftUp_zero {α : Type u} [LinearOrder α] (a : Array α) :
    (siftUp a 0).time = (0, 0)
Uses 3
Statement usesSift-up with comparison and swap counts
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid

TheoremSift-up at an out-of-range index costs nothing#✓fully proved

For every array \(a\) of length \(|a|\) over a linearly ordered type and every natural number \(i\) with \(i \ge |a|\), sift-up with comparison and swap counts on \(a\) at index \(i\) has cost \((0, 0)\): it counts no comparisons and no swaps.

theorem time_siftUp_of_size_le {α : Type u} [LinearOrder α] (a : Array α) (i : Nat)
    (hi : a.size ≤ i) : (siftUp a i).time = (0, 0)
Uses 3
Statement usesSift-up with comparison and swap counts
Proof usesParent index in a level-order binary tree · The parent of a valid nonroot index is valid

DefinitionDecrease-key in a binary min-heap#✓fully proved

Given a binary min-heap \(h\) over a linearly ordered type, with level-order array \(a\), an index \(i < |a|\) and a value \(x \le a_i\), decrease-key returns the heap whose array is obtained from \(a\) by replacing the entry at position \(i\) with \(x\) and then sifting position \(i\) up, repeatedly swapping the entry with its parent while it is strictly smaller than the parent.

Cslib.Algorithms.Lean.MinHeap.decreaseKey · 49 lines 
def MinHeap.decreaseKey {α : Type u} [LinearOrder α]
    (h : MinHeap α) (i : Fin h.data.size) (x : α)
    (hdecrease : x ≤ h.data[i.val]) : MinHeap α where
  data := siftUp (h.data.set i.val x) i.val
  ordered := siftUp_ordered _ _ (by
    refine {
      index_valid := by
        rw [Array.size_set]
        exact i.isLt
      ordered_except := ?_
      parent_below_children := ?_
    }
    · intro j hj hjpos hji
      have hj' : j < h.data.size := by
        rw [Array.size_set] at hj
        exact hj
      by_cases hp : heapParent j = i.val
      · have hold := h.ordered j hj' hjpos
        have hchain : x ≤ h.data[j] := by
          apply hdecrease.trans
          simpa only [hp] using hold
        rw [Array.getElem_set, ite_eq_left hp.symm, Array.getElem_set,
          ite_eq_right (Ne.symm hji)]
        exact hchain
      · have hold := h.ordered j hj' hjpos
        rw [Array.getElem_set, ite_eq_right (Ne.symm hp), Array.getElem_set,
          ite_eq_right (Ne.symm hji)]
        exact hold
    · intro j hj hjpos hp hipos
      have hj' : j < h.data.size := by
        rw [Array.size_set] at hj
        exact hj
      have hparent_ne : heapParent i.val ≠ i.val := by
        unfold heapParent
        omega
      have hji : j ≠ i.val := by
        intro hji
        subst j
        exact hparent_ne hp
      have hparent := h.ordered i.val i.isLt hipos
      have hchild := h.ordered j hj' hjpos
      have hchain :
          h.data[heapParent i.val]'(heapParent_lt_size h.data i.val i.isLt hipos) ≤
            h.data[j] := by
        apply hparent.trans
        simpa only [hp] using hchild
      rw [Array.getElem_set, ite_eq_right (Ne.symm hparent_ne), Array.getElem_set,
        ite_eq_right (Ne.symm hji)]
      exact hchain)
Uses 7 · Used by 4
Statement usesHeap order on a level-order array · Binary min-heap · Arrays ready for sift-up · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Sift-up · Sift-up restores heap order
Used byArray of a binary heap after decrease-key · Multiset of a binary heap after decrease-key · Decrease-key yields a heap-ordered array · Decrease-key preserves the heap size

TheoremArray of a binary heap after decrease-key#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, with level-order array \(a\), let \(i < |a|\) and let \(x \le a_i\). The array of the heap obtained by decreasing the key at position \(i\) to \(x\) equals the result of sifting up position \(i\) in the array obtained from \(a\) by replacing its entry at position \(i\) with \(x\).

theorem MinHeap.decreaseKey_data {α : Type u} [LinearOrder α]
    (h : MinHeap α) (i : Fin h.data.size) (x : α)
    (hdecrease : x ≤ h.data[i.val]) :
    (h.decreaseKey i x hdecrease).data =
      siftUp (h.data.set i.val x) i.val
Uses 3 · Used by 2
Statement usesBinary min-heap · Decrease-key in a binary min-heap · Sift-up
Used byMultiset of a binary heap after decrease-key · Decrease-key preserves the heap size

TheoremDecrease-key yields a heap-ordered array#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, with level-order array \(a\), let \(i < |a|\) and let \(x \le a_i\). The array of the heap obtained by decreasing the key at position \(i\) to \(x\) is heap-ordered: the entry at every nonroot position is at least the entry at its parent position.

theorem MinHeap.decreaseKey_ordered {α : Type u} [LinearOrder α]
    (h : MinHeap α) (i : Fin h.data.size) (x : α)
    (hdecrease : x ≤ h.data[i.val]) :
    HeapOrdered (h.decreaseKey i x hdecrease).data
Uses 3
Statement usesHeap order on a level-order array · Binary min-heap · Decrease-key in a binary min-heap

TheoremDecrease-key preserves the heap size#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, with level-order array \(a\), let \(i < |a|\) and let \(x \le a_i\). The array of the heap obtained by decreasing the key at position \(i\) to \(x\) has the same length as \(a\).

theorem MinHeap.decreaseKey_size {α : Type u} [LinearOrder α]
    (h : MinHeap α) (i : Fin h.data.size) (x : α)
    (hdecrease : x ≤ h.data[i.val]) :
    (h.decreaseKey i x hdecrease).data.size = h.data.size
Uses 5
Statement usesBinary min-heap · Decrease-key in a binary min-heap
Proof usesArray of a binary heap after decrease-key · Sift-up · Sift-up permutes the array

TheoremMultiset of a binary heap after decrease-key#✓fully proved

Let \(h\) be a binary min-heap over a linearly ordered type, with level-order array \(a\), let \(i < |a|\) and let \(x \le a_i\). The multiset of elements of the heap obtained by decreasing the key at position \(i\) to \(x\) is obtained from the multiset of elements of \(h\) by removing one occurrence of \(a_i\) and adding one occurrence of \(x\).

theorem MinHeap.decreaseKey_elements {α : Type u} [LinearOrder α]
    (h : MinHeap α) (i : Fin h.data.size) (x : α)
    (hdecrease : x ≤ h.data[i.val]) :
    (h.decreaseKey i x hdecrease).elements =
      x ::ₘ h.elements.erase (h.data[i.val])
Uses 6
Statement usesBinary min-heap · Decrease-key in a binary min-heap · Elements of a binary min-heap
Proof usesArray of a binary heap after decrease-key · Sift-up · Binary-heap sift-up preserves the multiset of entries

TheoremThe smaller child lies one level below its parent#✓fully proved

Let \(a\) be an array over a linearly ordered type and let \(i\) and \(c\) be natural numbers. If \(c\) is the smaller child of \(i\) in \(a\), then \(\lfloor \log_2 (c+1) \rfloor = \lfloor \log_2 (i+1) \rfloor + 1\); that is, in the level-order binary tree stored in \(a\), the node \(c\) lies exactly one level below \(i\).

theorem log2_smallerChild_add_one {α : Type u} [LinearOrder α]
    (a : Array α) (i c : Nat) (hchild : smallerChild a i = some c) :
    Nat.log2 (c + 1) = Nat.log2 (i + 1) + 1
Uses 4 · Used by 2
Statement usesSmaller child
Proof usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree · The smaller child has a larger index
Used bySift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level

TheoremThe smaller child's level is bounded by the array size#✓fully proved

Let \(a\) be an array over a linearly ordered type, of size \(|a|\), and let \(i\) and \(c\) be natural numbers. If \(c\) is the smaller child of \(i\) in \(a\), then \(\lfloor \log_2 (c+1) \rfloor \le \lfloor \log_2 |a| \rfloor\).

theorem log2_smallerChild_le_size {α : Type u} [LinearOrder α]
    (a : Array α) (i c : Nat) (hchild : smallerChild a i = some c) :
    Nat.log2 (c + 1) ≤ Nat.log2 a.size
Uses 2 · Used by 2
Statement usesSmaller child
Proof usesThe smaller child is a valid index
Used bySift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level

DefinitionTimed smaller-child selection#✓fully proved

Let \(a\) be an array over a linearly ordered type and \(i\) an index, with left child \(2i + 1\) and right child \(2i + 2\); cost is counted as the pair (value comparisons, array swaps). If both children are valid indices of \(a\), the selection costs \((1, 0)\) and returns the right child when its value is strictly less than the value at the left child, and the left child otherwise. If only the left child is a valid index, it returns the left child at cost \((0, 0)\). If the left child is not a valid index, it returns no child at cost \((0, 0)\).

def timedSmallerChild {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    TimeM (Nat × Nat) (Option Nat) :=
  if hl : heapLeft i < a.size then
    if hr : heapRight i < a.size then do
      tick (1, 0)
      pure (if a[heapRight i] < a[heapLeft i] then
        some (heapRight i) else some (heapLeft i))
    else pure (some (heapLeft i))
  else pure none
Uses 2 · Used by 8
Statement usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used byTimed sift-down returns the sift-down result · Timed child selection returns the smaller child · Sift-down with comparison and swap counts · Sift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level · Sift-down from a node without children costs nothing · Cost of child selection · Child selection at a node without children costs nothing

TheoremTimed child selection returns the smaller child#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the value returned by timed child selection at \(i\), with its cost discarded, is the smaller child of \(i\) in \(a\) (an optional index, absent when \(i\) has no valid child).

theorem ret_timedSmallerChild {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) :
    (timedSmallerChild a i).ret = smallerChild a i
Uses 4 · Used by 5
Statement usesTimed smaller-child selection · Smaller child
Proof usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used byTimed sift-down returns the sift-down result · Sift-down with comparison and swap counts · Sift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level · Sift-down from a node without children costs nothing

DefinitionSift-down with comparison and swap counts#✓fully proved

For an array \(a\) over a linearly ordered type and an index \(i\), timed sift-down returns an array together with a cost pair (value comparisons, array swaps), where costs add componentwise. If the left child index \(2i+1\) is not a valid index of \(a\), it returns \(a\) at cost \((0, 0)\). Otherwise let \(c\) be the smaller child of \(i\): the left child \(2i+1\), unless the right child \(2i+2\) is a valid index and \(a_{2i+2} < a_{2i+1}\), in which case \(c = 2i+2\). Selecting \(c\) costs one comparison when \(2i+2\) is a valid index and nothing otherwise. Comparing \(a_c\) with \(a_i\) costs one more comparison. If \(a_c < a_i\), the entries at \(i\) and \(c\) are swapped at the cost of one swap, and the result and remaining cost are those of timed sift-down from \(c\) in the swapped array; otherwise the result is \(a\).

Index arithmetic, bounds checks, pattern matching and recursive calls are free.

Cslib.Algorithms.Lean.TimeM.siftDown · 22 lines 
def siftDown {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    TimeM (Nat × Nat) (Array α) :=
  let selected := timedSmallerChild a i
  match hchild : selected.ret with
  | none => ⟨a, selected.time⟩
  | some c =>
    have hcanonical : smallerChild a i = some c :=
      (ret_timedSmallerChild a i).symm.trans hchild
    have hc : c < a.size := smallerChild_valid a i c hcanonical
    have hi : i < a.size := (smallerChild_gt a i c hcanonical).trans hc
    let run : TimeM (Nat × Nat) (Array α) := do
      tick (1, 0)
      if hlt : a[c] < a[i] then
        tick (0, 1)
        siftDown (a.swap i c hi hc) c
      else pure a
    ⟨run.ret, selected.time + run.time⟩
termination_by a.size - i
decreasing_by
  simp only [Array.size_swap]
  have := smallerChild_gt a i c hcanonical
  omega
Uses 5 · Used by 7
Statement usesTimed child selection returns the smaller child · Timed smaller-child selection · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byTimed sift-down returns the sift-down result · Sift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level · Total sift-down cost is at most three per remaining level · Sift-down from a leaf costs nothing · Sift-down from an invalid index costs nothing · Sift-down from a node without children costs nothing

TheoremTimed sift-down returns the sift-down result#✓fully proved

For every array \(a\) over a linearly ordered type and every index \(i\), the array returned by timed sift-down from \(i\), with its cost discarded, equals the array returned by sift-down from \(i\).

theorem ret_siftDown {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftDown a i).ret = Cslib.Algorithms.Lean.siftDown a i
Uses 7
Statement usesSift-down with comparison and swap counts · Sift-down
Proof usesTimed child selection returns the smaller child · Timed smaller-child selection · Smaller child · The smaller child has a larger index · The smaller child is a valid index

TheoremCost of child selection#✓fully proved

Let \(a\) be an array over a linearly ordered type and \(i\) an index, and count cost as the pair (value comparisons, array swaps). The timed child selection at \(i\) in \(a\) has cost \((1, 0)\) if the right child index \(2i + 2\) is less than the size of \(a\), and cost \((0, 0)\) otherwise.

theorem time_timedSmallerChild {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (timedSmallerChild a i).time =
      if heapRight i < a.size then (1, 0) else (0, 0)
Uses 3 · Used by 2
Statement usesTimed smaller-child selection · Right child index in an array-backed binary tree
Proof usesLeft child index in a level-order binary tree
Used bySift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level

TheoremChild selection at a node without children costs nothing#✓fully proved

Let \(a\) be an array over a linearly ordered type and \(i\) an index. If the smaller-child selection at \(i\) in \(a\) returns no child, then the timed child selection at \(i\), with cost counted as the pair (value comparisons, array swaps), has cost \((0, 0)\).

theorem time_timedSmallerChild_of_none {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) (hchild : smallerChild a i = none) :
    (timedSmallerChild a i).time = (0, 0)
Uses 4 · Used by 3
Statement usesTimed smaller-child selection · Smaller child
Proof usesLeft child index in a level-order binary tree · Right child index in an array-backed binary tree
Used bySift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level · Sift-down from a node without children costs nothing

TheoremSift-down performs at most one swap per remaining level#✓fully proved

Write \(|a|\) for the size of an array \(a\), and let \(\ell(n) = \lfloor \log_2 n \rfloor\) for \(n \ge 1\) and \(\ell(0) = 0\). For every array \(a\) over a linearly ordered type and every index \(i\), the number of array swaps counted by timed sift-down from \(i\) is at most \(\max(0, \ell(|a|) - \ell(i+1))\).

theorem siftDown_swaps_le {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftDown a i).time.2 ≤ Nat.log2 a.size - Nat.log2 (i + 1)
Uses 11 · Used by 1
Statement usesSift-down with comparison and swap counts
Proof usesTimed child selection returns the smaller child · Cost of child selection · Child selection at a node without children costs nothing · Timed smaller-child selection · Right child index in an array-backed binary tree · The smaller child lies one level below its parent · The smaller child's level is bounded by the array size · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byTotal sift-down cost is at most three per remaining level

TheoremSift-down makes at most two comparisons per remaining level#✓fully proved

Write \(|a|\) for the size of an array \(a\), and let \(\ell(n) = \lfloor \log_2 n \rfloor\) for \(n \ge 1\) and \(\ell(0) = 0\). For every array \(a\) over a linearly ordered type and every index \(i\), the number of value comparisons counted by timed sift-down from \(i\) is at most \(2 \max(0, \ell(|a|) - \ell(i+1))\).

theorem siftDown_comparisons_le {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftDown a i).time.1 ≤ 2 * (Nat.log2 a.size - Nat.log2 (i + 1))
Uses 11 · Used by 1
Statement usesSift-down with comparison and swap counts
Proof usesTimed child selection returns the smaller child · Cost of child selection · Child selection at a node without children costs nothing · Timed smaller-child selection · Right child index in an array-backed binary tree · The smaller child lies one level below its parent · The smaller child's level is bounded by the array size · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byTotal sift-down cost is at most three per remaining level

TheoremTotal sift-down cost is at most three per remaining level#✓fully proved

Write \(|a|\) for the size of an array \(a\), and let \(\ell(n) = \lfloor \log_2 n \rfloor\) for \(n \ge 1\) and \(\ell(0) = 0\). For every array \(a\) over a linearly ordered type and every index \(i\), the number of value comparisons plus the number of array swaps counted by timed sift-down from \(i\) is at most \(3 \max(0, \ell(|a|) - \ell(i+1))\).

theorem siftDown_time_le {α : Type u} [LinearOrder α] (a : Array α) (i : Nat) :
    (siftDown a i).time.1 + (siftDown a i).time.2 ≤
      3 * (Nat.log2 a.size - Nat.log2 (i + 1))
Uses 3
Statement usesSift-down with comparison and swap counts
Proof usesSift-down makes at most two comparisons per remaining level · Sift-down performs at most one swap per remaining level

TheoremSift-down from a node without children costs nothing#✓fully proved

Let \(a\) be an array over a linearly ordered type and \(i\) an index. If the smaller-child selection at \(i\) in \(a\) returns no child, then sift-down from \(i\), with cost counted as the pair (value comparisons, array swaps), has cost \((0, 0)\): it makes no value comparisons and no array swaps.

theorem time_siftDown_of_smallerChild_none {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) (hchild : smallerChild a i = none) :
    (siftDown a i).time = (0, 0)
Uses 7 · Used by 1
Statement usesSift-down with comparison and swap counts · Smaller child
Proof usesTimed child selection returns the smaller child · Child selection at a node without children costs nothing · Timed smaller-child selection · The smaller child has a larger index · The smaller child is a valid index
Used bySift-down from a leaf costs nothing

TheoremSift-down from a leaf costs nothing#✓fully proved

Let \(a\) be an array over a linearly ordered type, of size \(|a|\), and let \(i\) be an index with \(|a| \le 2i+1\), so that the left child of \(i\) is not a valid index (this includes invalid indices \(i\)). Then timed sift-down from \(i\) has cost pair \((0, 0)\): it counts no comparisons and no swaps.

theorem time_siftDown_of_heapLeft_ge {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) (h : a.size ≤ heapLeft i) :
    (siftDown a i).time = (0, 0)
Uses 5 · Used by 1
Statement usesSift-down with comparison and swap counts · Left child index in a level-order binary tree
Proof usesSift-down from a node without children costs nothing · Right child index in an array-backed binary tree · Smaller child
Used bySift-down from an invalid index costs nothing

TheoremSift-down from an invalid index costs nothing#✓fully proved

Let \(a\) be an array over a linearly ordered type, of size \(|a|\), and let \(i\) be a natural number with \(|a| \le i\). Then timed sift-down from \(i\) has cost pair \((0, 0)\): it counts no comparisons and no swaps.

theorem time_siftDown_of_size_le {α : Type u} [LinearOrder α]
    (a : Array α) (i : Nat) (h : a.size ≤ i) :
    (siftDown a i).time = (0, 0)
Uses 3
Statement usesSift-down with comparison and swap counts
Proof usesSift-down from a leaf costs nothing · Left child index in a level-order binary tree
74 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.