Indexed minimum priority queue

StructureIndexed minimum queue#✓fully proved

Let \(W\) be a linearly ordered type, let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined, and let \(n\) be a natural number. An indexed minimum queue over the identities \(0, \dots, n-1\) consists of a binary min-heap whose entries are pairs \((k, v)\) of a key \(k \in W \cup \{\top\}\) and an identity \(v < n\), ordered lexicographically (first by key, then by identity), together with a position vector assigning to each identity \(v < n\) either nothing or an index \(i < n\). It is required that the heap has at most \(n\) entries and that, for all identities \(v < n\) and indices \(i < n\), the position of \(v\) is \(i\) exactly when \(i\) is a slot of the heap whose entry has identity \(v\).

structure IndexedMinQueue (W : Type u) [LinearOrder W] (n : Nat) where
  heap : Cslib.Algorithms.Lean.MinHeap (WithTop W ×ₗ Fin n)
  position : Vector (Option (Fin n)) n
  capacity : heap.data.size ≤ n
  inverse : ∀ (v i : Fin n), position[v] = some i ↔
    ∃ hi : i.val < heap.data.size, (ofLex (heap.data[i.val]'hi)).2 = v
Uses 1 · Used by 29
Statement usesBinary min-heap
Used byDecrease-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 · The empty indexed min queue has no present identity · 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 · Membership test in an indexed minimum queue · Membership reads the position vector · Membership costs one position read · 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

DefinitionEmpty indexed minimum queue#✓fully proved

For every linearly ordered type \(W\) and every natural number \(n\), the empty indexed minimum queue over the identities \(0, \dots, n-1\), with keys in \(W\) with a new greatest element adjoined, has the empty min-heap and a position vector that assigns nothing to each of the \(n\) identities, so no identity is present.

def empty {W : Type u} [LinearOrder W] (n : Nat) : IndexedMinQueue W n where
  heap := MinHeap.empty
  position := Vector.replicate n none
  capacity := by simp [MinHeap.empty]
  inverse := by simp [MinHeap.empty]
Uses 3 · Used by 11
Statement usesIndexed minimum queue · Binary min-heap · Empty binary min-heap
Used byThe empty indexed min queue has no present identity · 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

DefinitionMembership test in an indexed minimum queue#✓fully proved

Costs are counted as five event counts: comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements. For an indexed minimum queue \(q\) over the identities \(0, \dots, n-1\) and an identity \(v < n\), the membership test returns true exactly when the position vector of \(q\) assigns an index to \(v\), and its cost is one position read and no other event.

@[no_expose] def member {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) : TimeM (Fin 5 → Nat) Bool :=
  ⟨q.position[v].isSome, event 2⟩
Uses 1 · Used by 11
Statement usesIndexed minimum queue
Used byMembership reads the position vector · Membership costs one position read · 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

DefinitionInsertion into an indexed minimum queue#✓fully proved

Let \(W\) be a linearly ordered type and let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined. Costs are counted as five event counts: comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements. Given an indexed minimum queue \(q\) over the identities \(0, \dots, n-1\) with keys in \(W \cup \{\top\}\), whose heap entries (pairs of a key and an identity) are ordered lexicographically, first by key and then by identity, an identity \(v < n\) and a key \(k \in W \cup \{\top\}\), insertion fails (returns nothing) when the position vector of \(q\) assigns an index to \(v\), at the cost of one position read. Otherwise it appends the entry \((k, v)\) at the end of the heap, sets the position of \(v\) to that slot, and sifts the entry up: while it is not at the root and is smaller than its parent, it is swapped with its parent and the positions of both swapped identities are updated. It returns the resulting queue, at the cost of one position read, one position write and one entry append, plus one comparison for each comparison with a parent and one swap and two position writes for each swap.

Cslib.Algorithms.Lean.IndexedMinQueue.insert · 28 lines 
@[no_expose] def insert {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : WithTop W) :
    TimeM (Fin 5 → Nat) (Option (IndexedMinQueue W n)) :=
  if hpresent : q.position[v].isSome = true then
    ⟨none, event 2⟩
  else
    have habsent : q.position[v] = none := by
      simpa [Option.isSome_iff_ne_none] using hpresent
    have hspare : q.heap.data.size < n := absent_spare q v habsent
    let entry := toLex (key, v)
    let a := q.heap.data.push entry
    let position := q.position.set v (some ⟨q.heap.data.size, hspare⟩)
    let hcap : a.size ≤ n := by simp [a]; omega
    let r := siftUpTracked a position hcap q.heap.data.size
    have hrdata : r.data = (q.heap.push entry).data := by
      exact siftUpTracked_data a position hcap q.heap.data.size
    have hrinv : Inverse r.data r.position := by
      apply siftUpTracked_inverse a position hcap
      exact inverse_push q.heap.data q.position hspare q.inverse v key habsent
    let heap' : MinHeap (WithTop W ×ₗ Fin n) :=
      ⟨r.data, by rw [hrdata]; exact (q.heap.push entry).ordered⟩
    have hcap' : heap'.data.size ≤ n := by
      rw [show heap'.data = r.data from rfl, hrdata]
      change (siftUp a q.heap.data.size).size ≤ n
      rw [(siftUp_perm a q.heap.data.size).size_eq]
      exact hcap
    ⟨some ⟨heap', r.position, hcap', hrinv⟩,
      event 2 + event 3 + event 4 + r.time⟩
Uses 8 · Used by 13
Statement usesHeap order on a level-order array · Indexed minimum queue · Binary min-heap · Insertion into a binary min-heap · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Sift-up · Sift-up permutes the array
Used byInsertion 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 · 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

DefinitionDecrease-key in an indexed minimum queue#✓fully proved

Let \(W\) be a linearly ordered type and let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined. Costs are counted as five event counts: comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements. Given an indexed minimum queue \(q\) over the identities \(0, \dots, n-1\) with keys in \(W \cup \{\top\}\), whose heap entries (pairs of a key and an identity) are ordered lexicographically, first by key and then by identity, an identity \(v < n\) and a finite key \(k \in W\), decrease-key fails (returns nothing) when the position vector of \(q\) assigns no index to \(v\), at the cost of one position read, and when \(k\) is not strictly smaller than the current key of \(v\), at the cost of one position read and one comparison. Otherwise it replaces the entry of \(v\) by \((k, v)\) in the same slot and sifts it up: while it is not at the root and is smaller than its parent, it is swapped with its parent and the positions of both swapped identities are updated. It returns the resulting queue, at the cost of one position read, one comparison and one entry replacement, plus one comparison for each comparison with a parent and one swap and two position writes for each swap.

Cslib.Algorithms.Lean.IndexedMinQueue.decreaseKey · 27 lines 
@[no_expose] def decreaseKey {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : W) :
    TimeM (Fin 5 → Nat) (Option (IndexedMinQueue W n)) :=
  match hp : q.position[v] with
  | none => ⟨none, event 2⟩
  | some i =>
    have hi : i.val < q.heap.data.size := (q.inverse v i).1 hp |>.choose
    let old := q.heap.data[i.val]'hi
    if hlt : (↑key : WithTop W) < (ofLex old).1 then
      have hid : (ofLex old).2 = v := (q.inverse v i).1 hp |>.choose_spec
      let a := q.heap.data.set i.val (toLex ((↑key : WithTop W), v)) hi
      have hinv : Inverse a q.position :=
        inverse_set_key q.heap.data q.position q.inverse i.val hi v hid key
      let r := siftUpTracked a q.position (by simpa [a] using q.capacity) i.val
      have hrinv := siftUpTracked_inverse a q.position (by simpa [a] using q.capacity) hinv i.val
      let heap' : MinHeap (WithTop W ×ₗ Fin n) :=
        ⟨r.data, by
          rw [siftUpTracked_data]
          exact siftUp_ordered a i.val (set_decrease_ready q v key i hi hid hlt)⟩
      let q' : IndexedMinQueue W n :=
        ⟨heap', r.position, by
          rw [show heap'.data = r.data from rfl, siftUpTracked_data]
          rw [(siftUp_perm a i.val).size_eq]
          simpa [a] using q.capacity, hrinv⟩
      ⟨some q', event 2 + event 0 + event 4 + r.time⟩
    else
      ⟨none, event 2 + event 0⟩
Uses 9 · Used by 12
Statement usesHeap order on a level-order array · Indexed minimum queue · 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 · Sift-up permutes the array
Used byDecrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · 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

DefinitionExtract-min in an indexed minimum queue#✓fully proved

Costs are counted as five event counts: comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements. Given an indexed minimum queue \(q\), extract-min fails (returns nothing) exactly when the heap of \(q\) is empty, at zero cost. Otherwise let \((k, v)\) be the root entry of the heap. If the heap has one entry, extract-min returns \((k, v)\) together with the queue whose heap is empty and in which \(v\) has no position, at the cost of one position write and one entry pop. If the heap has at least two entries, the root is swapped with the last entry and the positions of both are updated, the last slot is removed, the position of \(v\) is cleared, and the new root is sifted down: while it has a child, let \(c\) be its smaller child (the left one on ties); if \(c\) is smaller than it, the two are swapped and the positions of both are updated, otherwise the sift stops. It returns \((k, v)\) together with the resulting queue, at the cost of one swap, three position writes and one entry pop, plus, at each sift-down step, one comparison between the two children when both exist, one comparison with \(c\), and one swap and two position writes when a swap is made.

Cslib.Algorithms.Lean.IndexedMinQueue.extractMin · 60 lines 
@[no_expose] def extractMin {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) :
    TimeM (Fin 5 → Nat)
      (Option ((WithTop W ×ₗ Fin n) × IndexedMinQueue W n)) :=
  if hempty : q.heap.data.size = 0 then
    ⟨none, 0⟩
  else
    have hne : 0 < q.heap.data.size := Nat.pos_of_ne_zero hempty
    let entry := q.heap.data[0]'hne
    let v := (ofLex entry).2
    if hone : q.heap.data.size = 1 then
      let position := q.position.set v none
      have hinv : Inverse (#[] : Array (WithTop W ×ₗ Fin n)) position := by
        have hlast : (ofLex (q.heap.data[q.heap.data.size - 1]'(by omega))).2 = v := by
          simp [v, entry, hone]
        have hpop : q.heap.data.pop = #[] :=
          Array.eq_empty_of_size_eq_zero (by simp [hone])
        simpa only [hpop] using
          inverse_pop_clear q.heap.data q.position q.capacity q.inverse hne v hlast
      let q' : IndexedMinQueue W n :=
        ⟨MinHeap.empty, position, by simp [MinHeap.empty], hinv⟩
      ⟨some (entry, q'), event 3 + event 4⟩
    else
      have htwo : 1 < q.heap.data.size := by omega
      let last := q.heap.data.size - 1
      let aSwap := q.heap.data.swap 0 last hne (by dsimp [last]; omega)
      let positionSwap := swapPosition q.heap.data q.position q.capacity 0 last hne
        (by dsimp [last]; omega)
      have hinvSwap : Inverse aSwap positionSwap := by
        apply inverse_swap q.heap.data q.position q.capacity q.inverse 0 last hne
          (by dsimp [last]; omega)
        omega
      let a := aSwap.pop
      let position := positionSwap.set v none
      have hlast : (ofLex (aSwap[aSwap.size - 1]'(by
          dsimp only [aSwap]
          rw [Array.size_swap]
          omega))).2 = v := by
        simp [aSwap, last, v, entry]
      have hinv : Inverse a position := by
        exact inverse_pop_clear aSwap positionSwap (by simpa [aSwap] using q.capacity)
          hinvSwap (by simp [aSwap]; omega) v hlast
      have hcap : a.size ≤ n := by
        have hc := q.capacity
        simp only [a, aSwap, Array.size_pop, Array.size_swap]
        omega
      let r := siftDownTracked a position hcap 0
      have hrdata : r.data = (q.heap.extractTail hne).data := by
        rw [MinHeap.extractTail, dite_eq_right hone]
        exact siftDownTracked_data a position hcap 0
      have hrinv := siftDownTracked_inverse a position hcap hinv 0
      let heap' : MinHeap (WithTop W ×ₗ Fin n) :=
        ⟨r.data, by rw [hrdata]; exact (q.heap.extractTail hne).ordered⟩
      let q' : IndexedMinQueue W n :=
        ⟨heap', r.position, by
          change r.data.size ≤ n
          rw [siftDownTracked_data, (siftDown_perm a 0).size_eq]
          exact hcap, hrinv⟩
      ⟨some (entry, q'),
        event 1 + event 3 + event 3 + event 3 + event 4 + r.time⟩
Uses 14 · Used by 12
Statement usesHeap order on a level-order array · Indexed minimum queue · Binary min-heap · Empty binary min-heap · Removing the root of a nonempty binary min-heap · Right child index in an array-backed binary tree · 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 · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byExtraction 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 · 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

TheoremRecorded positions lie inside the heap#✓fully proved

Let \(W\) be a linearly ordered type and let \(q\) be an indexed min-queue over \(W\) with identities in \(\{0, \dots, n-1\}\). If the position table of \(q\) records slot \(i\) for an identity \(v\), then \(i\) is less than the number of entries currently stored in the heap array of \(q\).

theorem position_valid {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v i : Fin n)
    (h : q.position[v] = some i) : i.val < q.heap.data.size
Uses 2 · Used by 12
Statement usesIndexed minimum queue · Binary min-heap
Used byDecrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · 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

TheoremAbsent identities carry no heap entry#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\) and let \(v\) be an identity. The position vector of \(q\) records no slot for \(v\) if and only if no entry of the heap array of \(q\) has identity \(v\).

theorem position_eq_none_iff {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) :
    q.position[v] = none ↔
      ¬ ∃ entry ∈ q.heap.data.toList, (ofLex entry).2 = v
Uses 2 · Used by 8
Statement usesIndexed minimum queue · Binary min-heap
Used bySuccessful 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

TheoremThe empty indexed min queue has no present identity#✓fully proved

For every linear order \(W\), every \(n\) and every identity \(v \in \{0, \dots, n-1\}\), the position vector of the empty indexed min queue over \(W\) with identities in \(\{0, \dots, n-1\}\) records no slot for \(v\).

theorem empty_position {W : Type u} [LinearOrder W] {n : Nat}
    (v : Fin n) : (empty (W := W) n).position[v] = none
Uses 2 · Used by 7
Statement usesIndexed minimum queue · Empty indexed minimum queue
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

TheoremInsertion fails exactly on present identities#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\), let \(v\) be an identity and let \(k \in W \cup \{\top\}\). Inserting \(v\) with key \(k\) into \(q\) returns no queue if and only if the position vector of \(q\) records a slot for \(v\).

theorem insert_eq_none_iff {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : WithTop W) :
    (insert q v key).ret = none ↔ q.position[v].isSome = true
Uses 9 · Used by 7
Statement usesIndexed minimum queue · Insertion into an indexed minimum queue
Proof usesHeap order on a level-order array · Binary min-heap · Insertion into a binary min-heap · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Sift-up · Sift-up permutes the array
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

TheoremExtraction from an indexed min queue fails exactly when it is empty#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\). Extracting the minimum of \(q\) returns no result if and only if the heap array of \(q\) has size \(0\).

theorem extractMin_eq_none_iff {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) :
    (extractMin q).ret = none ↔ q.heap.data.size = 0
Uses 15 · Used by 7
Statement usesIndexed minimum queue · Extract-min in an indexed minimum queue · Binary min-heap
Proof usesHeap order on a level-order array · Empty binary min-heap · Removing the root of a nonempty binary min-heap · Right child index in an array-backed binary tree · 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 · Smaller child · The smaller child has a larger index · The smaller child is a valid index
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

TheoremMembership reads the position vector#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\) and let \(v\) be an identity. The membership test for \(v\) in \(q\) returns true if and only if the position vector of \(q\) records a slot for \(v\).

theorem member_ret {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) :
    (member q v).ret = q.position[v].isSome
Uses 2 · Used by 8
Statement usesIndexed minimum queue · Membership test in an indexed minimum queue
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 · Parents returned by Prim's algorithm are adjacency-list neighbors · The root has no parent in Prim's algorithm

TheoremMembership costs one position read#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\) and let \(v\) be an identity. The cost of the membership test for \(v\) in \(q\), counted in five event classes (comparisons, swaps, position-vector reads, position-vector writes, and entry appends, pops or replacements), is exactly one position-vector read and no event of any other class.

theorem member_time {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) :
    (member q v).time = fun c : Fin 5 => if c = 2 then 1 else 0
Uses 2 · Used by 1
Statement usesIndexed minimum queue · Membership test in an indexed minimum queue
Used byLogarithmic heap cost of Prim's algorithm

TheoremSuccessful insertion into an indexed min queue#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\), let \(v\) be an identity and let \(k \in W \cup \{\top\}\), and suppose that inserting \(v\) with key \(k\) into \(q\) returns the queue \(q'\). Then the heap of \(q'\) is the binary min-heap push of the entry \((k, v)\) onto the heap of \(q\); the position vector of \(q'\) records a slot \(i\) for \(v\), with \(i\) less than the size of the heap array of \(q'\), and that array holds \((k, v)\) at index \(i\); and every identity \(w \neq v\) has a recorded slot in \(q'\) if and only if it has one in \(q\).

theorem insert_ret {W : Type u} [LinearOrder W] {n : Nat}
    (q q' : IndexedMinQueue W n) (v : Fin n) (key : WithTop W)
    (h : (insert q v key).ret = some q') :
    q'.heap = q.heap.push (toLex (key, v)) ∧
      (∃ (i : Fin n) (hi : i.val < q'.heap.data.size),
        q'.position[v] = some i ∧ q'.heap.data[i.val]'hi = toLex (key, v)) ∧
      ∀ w : Fin n, w ≠ v → q'.position[w].isSome = q.position[w].isSome
Uses 12 · Used by 8
Statement usesIndexed minimum queue · Insertion into an indexed minimum queue · Binary min-heap · Insertion into a binary min-heap
Proof usesHeap order on a level-order array · Absent identities carry no heap entry · Elements of a binary min-heap · Elements after binary heap insertion · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Sift-up · Sift-up permutes the array
Used byEvent 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

TheoremDecrease-key fails exactly on absent identities and non-decreases#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\), let \(v\) be an identity and let \(k \in W\). Decreasing the key of \(v\) to \(k\) in \(q\) returns no queue if and only if either the position vector of \(q\) records no slot for \(v\), or it records a slot \(i\) for \(v\) with \(i\) less than the size of the heap array of \(q\) and \(k\) is not strictly less, in \(W \cup \{\top\}\), than the key of the heap entry at index \(i\).

theorem decreaseKey_eq_none_iff {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : W) :
    (decreaseKey q v key).ret = none ↔
      q.position[v] = none ∨
        ∃ (i : Fin n) (hi : i.val < q.heap.data.size),
          q.position[v] = some i ∧
            ¬ (↑key : WithTop W) < (ofLex (q.heap.data[i.val]'hi)).1
Uses 11 · Used by 8
Statement usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Binary min-heap
Proof usesHeap order on a level-order array · Recorded positions lie inside the 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 · Sift-up permutes the array
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 · Parents returned by Prim's algorithm are adjacency-list neighbors · The root has no parent in Prim's algorithm

TheoremSuccessful decrease-key#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\), let \(v\) be an identity and let \(k \in W\), and suppose that decreasing the key of \(v\) to \(k\) in \(q\) returns the queue \(q'\). Let \(a\) be the heap array of \(q\). Then the position vector of \(q\) records a slot \(i\) for \(v\) with \(i\) less than the size of \(a\), \(k\) is strictly less, in \(W \cup \{\top\}\), than the key of the entry \(a_i\), and the heap array of \(q'\) is obtained by sifting up from index \(i\) the array that agrees with \(a\) except that \(a_i\) is replaced by \((k, v)\). Moreover, every identity has a recorded slot in \(q'\) if and only if it has one in \(q\).

theorem decreaseKey_ret {W : Type u} [LinearOrder W] {n : Nat}
    (q q' : IndexedMinQueue W n) (v : Fin n) (key : W)
    (h : (decreaseKey q v key).ret = some q') :
    (∃ (i : Fin n) (hi : i.val < q.heap.data.size),
      q.position[v] = some i ∧
        (↑key : WithTop W) < (ofLex (q.heap.data[i.val]'hi)).1 ∧
        q'.heap.data = siftUp
          (q.heap.data.set i.val (toLex ((↑key : WithTop W), v)) hi) i.val) ∧
      ∀ w : Fin n, q'.position[w].isSome = q.position[w].isSome
Uses 11 · Used by 7
Statement usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Binary min-heap · Sift-up
Proof usesHeap order on a level-order array · Recorded positions lie inside the 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 restores heap order · Sift-up permutes the array
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

TheoremSuccessful extraction from an indexed min queue#✓fully proved

Let \(q\) be an indexed min queue over a linear order \(W\) with identities in \(\{0, \dots, n-1\}\), and suppose that extracting the minimum of \(q\) returns the heap entry \(e = (k, u)\), with key \(k \in W \cup \{\top\}\) and identity \(u\), together with the queue \(q'\). Then binary min-heap extraction on the heap of \(q\) returns \(e\) together with the heap of \(q'\); the position vector of \(q'\) records no slot for \(u\); and every identity \(w \neq u\) has a recorded slot in \(q'\) if and only if it has one in \(q\).

theorem extractMin_ret {W : Type u} [LinearOrder W] {n : Nat}
    (q q' : IndexedMinQueue W n) (entry : WithTop W ×ₗ Fin n)
    (h : (extractMin q).ret = some (entry, q')) :
    q.heap.extractMin = some (entry, q'.heap) ∧
      q'.position[(ofLex entry).2] = none ∧
      ∀ w : Fin n, w ≠ (ofLex entry).2 →
        q'.position[w].isSome = q.position[w].isSome
Uses 19 · Used by 7
Statement usesIndexed minimum queue · Extract-min in an indexed minimum queue · Binary min-heap · Extracting the minimum of a binary min-heap
Proof usesHeap order on a level-order array · Absent identities carry no heap entry · Elements of a binary min-heap · Empty binary min-heap · Membership after extraction from a binary min-heap · Removing the root of a nonempty binary min-heap · Right child index in an array-backed binary tree · 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 · Smaller child · The smaller child has a larger index · The smaller child is a valid index
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

TheoremLogarithmic event bound for indexed-queue insertion#✓fully proved

Let \(W\) be a linearly ordered type and let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined. Let \(q\) be an indexed minimum queue over the identities \(0, \dots, n-1\) with keys in \(W \cup \{\top\}\) whose heap has \(s\) entries, let \(v < n\) be an identity and let \(k \in W \cup \{\top\}\) be a key. For each of the five counted events (comparisons, swaps, position reads, position writes, and entry appends, pops or replacements), the number of times that event occurs when inserting \(v\) with key \(k\) into \(q\) is at most \(20 (\lfloor \log_2 (s + 1) \rfloor + 1)\).

theorem insert_time {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : WithTop W) (c : Fin 5) :
    (insert q v key).time c ≤ 20 * (Nat.log2 (q.heap.data.size + 1) + 1)
Uses 9 · Used by 2
Statement usesIndexed minimum queue · Insertion into an indexed minimum queue · Binary min-heap
Proof usesHeap order on a level-order array · Insertion into a binary min-heap · Parent index in a level-order binary tree · The parent of a valid nonroot index is valid · Sift-up · Sift-up permutes the array
Used byEvent bound for building an indexed queue by repeated insertion · Logarithmic heap cost of Prim's algorithm

TheoremLogarithmic event bound for indexed-queue decrease-key#✓fully proved

Let \(W\) be a linearly ordered type and let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined. Let \(q\) be an indexed minimum queue over the identities \(0, \dots, n-1\) with keys in \(W \cup \{\top\}\) whose heap has \(s\) entries, let \(v < n\) be an identity and let \(k \in W\) be a key. For each of the five counted events (comparisons, swaps, position reads, position writes, and entry appends, pops or replacements), the number of times that event occurs when decreasing the key of \(v\) to \(k\) in \(q\) is at most \(20 (\lfloor \log_2 (s + 1) \rfloor + 1)\).

theorem decreaseKey_time {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (v : Fin n) (key : W) (c : Fin 5) :
    (decreaseKey q v key).time c ≤ 20 * (Nat.log2 (q.heap.data.size + 1) + 1)
Uses 11 · Used by 1
Statement usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Binary min-heap
Proof usesHeap order on a level-order array · Recorded positions lie inside the 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 · Sift-up permutes the array
Used byLogarithmic heap cost of Prim's algorithm

TheoremLogarithmic event bound for indexed-queue extract-min#✓fully proved

Let \(q\) be an indexed minimum queue whose heap has \(s\) entries. For each of the five counted events (comparisons, swaps, position reads, position writes, and entry appends, pops or replacements), the number of times that event occurs when extracting the minimum of \(q\) is at most \(20 (\lfloor \log_2 (s + 1) \rfloor + 1)\).

theorem extractMin_time {W : Type u} [LinearOrder W] {n : Nat}
    (q : IndexedMinQueue W n) (c : Fin 5) :
    (extractMin q).time c ≤ 20 * (Nat.log2 (q.heap.data.size + 1) + 1)
Uses 16 · Used by 1
Statement usesIndexed minimum queue · Extract-min in an indexed minimum queue · Binary min-heap
Proof usesHeap order on a level-order array · Empty binary min-heap · Removing the root of a nonempty binary min-heap · Left child index in a level-order binary tree · Right child index in an array-backed binary tree · 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 · Smaller child · The smaller child has a larger index · The smaller child is a valid index
Used byLogarithmic heap cost of Prim's algorithm

TheoremEvent bound for building an indexed queue by repeated insertion#✓fully proved

Let \(W\) be a linearly ordered type and let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined. Let \(q_0, \dots, q_n\) be indexed minimum queues over the identities \(0, \dots, n-1\) with keys in \(W \cup \{\top\}\), and let \(k_0, \dots, k_{n-1}\) be keys in \(W \cup \{\top\}\). Suppose \(q_0\) is the empty queue and, for each \(i < n\), inserting identity \(i\) with key \(k_i\) into \(q_i\) succeeds and returns \(q_{i+1}\). Then for each of the five counted events (comparisons, swaps, position reads, position writes, and entry appends, pops or replacements), the total number of times that event occurs over these \(n\) insertions is at most \(20 n (\lfloor \log_2 (n + 1) \rfloor + 1)\).

theorem repeated_insert_time {W : Type u} [LinearOrder W] {n : Nat}
    (qs : Fin (n + 1) → IndexedMinQueue W n) (keys : Fin n → WithTop W)
    (hstart : qs 0 = empty (W := W) n)
    (hsteps : ∀ i : Fin n,
      (insert (qs i.castSucc) i (keys i)).ret = some (qs i.succ))
    (c : Fin 5) :
    (∑ i : Fin n, (insert (qs i.castSucc) i (keys i)).time c) ≤
      20 * n * (Nat.log2 (n + 1) + 1)
Uses 9
Statement usesIndexed minimum queue · Empty indexed minimum queue · Insertion into an indexed minimum queue
Proof usesSuccessful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Binary min-heap · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array
21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.