Indexed min-priority queue specification

This file defines a deterministic, graph-free abstract specification (Cslib.Algorithms.Lean.IndexedMinPQ.spec) for an indexed min-priority queue over finite handles Fin n and natural-number keys bounded by K_max.

States map each handle v : Fin n to Option ℕ (none when absent, some k when present with key k). To make extractMin a deterministic state transition (Cslib.Stateful.Spec.step) that depends only on the abstract state and not on insertion history, findMin breaks equal-key ties by choosing the smallest handle index (PrioLE). Both binary heaps and Fibonacci heaps over the word RAM can realize this exact specification.

Main definitions

• Cslib.Algorithms.Lean.IndexedMinPQ.Op: priority-queue operations (isEmpty, getKey, insert, decreaseKey, extractMin).
• Cslib.Algorithms.Lean.IndexedMinPQ.State, empty, dom: abstract map state, empty queue, and present-handle set.
• Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLE, PrioLE, RawPrioLT, PrioLT, findMin: weak and strict lexicographic (key, handle) priority orders and deterministic minimum selection.
• Cslib.Algorithms.Lean.IndexedMinPQ.spec: the Cslib.Stateful.Spec with key bound K_max.

Main results

• not_rawPrioLT_iff_rawPrioLE, not_prioLT_iff_prioLE, prioLT_or_prioLT_of_ne: relationship between strict and weak lexicographic priority orders.
• dom_empty, dom_insert, dom_decreaseKey, dom_extractMin: domain evolution under each operation.
• findMin_eq_none_iff, findMin_eq_some_iff, findMin_mem_dom, findMin_le, findMin_key_le: characterization and optimality of findMin.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapters 6 and 19

inductive Cslib.Algorithms.Lean.IndexedMinPQ.Op (n : ℕ) : Type

Operations on an indexed min-priority queue over handles Fin n and natural-number keys.

• isEmpty {n : ℕ} : Op n

  Test whether the queue holds no handles.

• getKey {n : ℕ} (v : Fin n) : Op n

  Query the current key of handle v, if present.

• insert {n : ℕ} (v : Fin n) (k : ℕ) : Op n

  Insert an absent handle v with key k.

• decreaseKey {n : ℕ} (v : Fin n) (k : ℕ) : Op n

  Lower the key of a present handle v to k.

• extractMin {n : ℕ} : Op n

  Remove and return the present (handle, key) pair of minimum (key, handle).

def Cslib.Algorithms.Lean.IndexedMinPQ.instDecidableEqOp.decEq {n✝ : ℕ} (x✝ x✝¹ : Op n✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instDecidableEqOp {n✝ : ℕ} : DecidableEq (Op n✝)

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instReprOp {n✝ : ℕ} : Repr (Op n✝)

def Cslib.Algorithms.Lean.IndexedMinPQ.instReprOp.repr {n✝ : ℕ} : Op n✝ → ℕ → Std.Format

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.IndexedMinPQ.State (n : ℕ) : Type

Abstract state of an indexed min-priority queue on Fin n.

def Cslib.Algorithms.Lean.IndexedMinPQ.empty (n : ℕ) : State n

The empty priority queue on Fin n.

def Cslib.Algorithms.Lean.IndexedMinPQ.dom {n : ℕ} (s : State n) : Finset (Fin n)

The finite set of handles currently present in state s.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLE (a b : ℕ × ℕ) : Prop

Lexicographic priority comparison on raw (handle, key) : ℕ × ℕ pairs: smaller key first, breaking equal-key ties by smaller handle index.

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instDecidableRawPrioLE (a b : ℕ × ℕ) : Decidable (RawPrioLE a b)

theorem Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLE.refl (a : ℕ × ℕ) : RawPrioLE a a

Reflexivity of RawPrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLE.trans {a b c : ℕ × ℕ} (hab : RawPrioLE a b) (hbc : RawPrioLE b c) : RawPrioLE a c

Transitivity of RawPrioLE.

def Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE {n : ℕ} (a b : Fin n × ℕ) : Prop

Lexicographic priority comparison on (handle, key) pairs: smaller key first, breaking equal-key ties by smaller handle index.

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instDecidablePrioLE {n : ℕ} (a b : Fin n × ℕ) : Decidable (PrioLE a b)

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE.refl {n : ℕ} (a : Fin n × ℕ) : PrioLE a a

Reflexivity of PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE.trans {n : ℕ} {a b c : Fin n × ℕ} (hab : PrioLE a b) (hbc : PrioLE b c) : PrioLE a c

Transitivity of PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE.antisymm {n : ℕ} {a b : Fin n × ℕ} (hab : PrioLE a b) (hba : PrioLE b a) : a = b

Antisymmetry of PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE.total {n : ℕ} (a b : Fin n × ℕ) : PrioLE a b ∨ PrioLE b a

Totality of PrioLE.

def Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLT (a b : ℕ × ℕ) : Prop

Strict lexicographic priority comparison on raw (handle, key) : ℕ × ℕ pairs: smaller key first, breaking equal-key ties by strictly smaller handle index.

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instDecidableRawPrioLT (a b : ℕ × ℕ) : Decidable (RawPrioLT a b)

theorem Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLT.irrefl (a : ℕ × ℕ) : ¬RawPrioLT a a

Irreflexivity of RawPrioLT.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLT.trans {a b c : ℕ × ℕ} (hab : RawPrioLT a b) (hbc : RawPrioLT b c) : RawPrioLT a c

Transitivity of RawPrioLT.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.RawPrioLT.le {a b : ℕ × ℕ} (h : RawPrioLT a b) : RawPrioLE a b

Strict priority order RawPrioLT implies weak priority order RawPrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.not_rawPrioLT_iff_rawPrioLE {a b : ℕ × ℕ} : ¬RawPrioLT a b ↔ RawPrioLE b a

Negation of RawPrioLT is the converse weak priority order RawPrioLE.

def Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT {n : ℕ} (a b : Fin n × ℕ) : Prop

Strict lexicographic priority comparison on (handle, key) pairs: smaller key first, breaking equal-key ties by strictly smaller handle index.

@[instance_reducible]

instance Cslib.Algorithms.Lean.IndexedMinPQ.instDecidablePrioLT {n : ℕ} (a b : Fin n × ℕ) : Decidable (PrioLT a b)

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.irrefl {n : ℕ} (a : Fin n × ℕ) : ¬PrioLT a a

Irreflexivity of PrioLT.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.trans {n : ℕ} {a b c : Fin n × ℕ} (hab : PrioLT a b) (hbc : PrioLT b c) : PrioLT a c

Transitivity of PrioLT.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.asymm {n : ℕ} {a b : Fin n × ℕ} (hab : PrioLT a b) : ¬PrioLT b a

Asymmetry of PrioLT.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.le {n : ℕ} {a b : Fin n × ℕ} (h : PrioLT a b) : PrioLE a b

PrioLT implies PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.of_le_of_lt {n : ℕ} {a b c : Fin n × ℕ} (hab : PrioLE a b) (hbc : PrioLT b c) : PrioLT a c

PrioLT mixed with PrioLE on the left.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.PrioLT.of_lt_of_le {n : ℕ} {a b c : Fin n × ℕ} (hab : PrioLT a b) (hbc : PrioLE b c) : PrioLT a c

PrioLT mixed with PrioLE on the right.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.not_prioLT_iff_prioLE {n : ℕ} {a b : Fin n × ℕ} : ¬PrioLT a b ↔ PrioLE b a

Negation of PrioLT is reverse PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.prioLT_or_prioLT_of_ne {n : ℕ} {u v : Fin n} (huv : u ≠ v) (ku kv : ℕ) : PrioLT (u, ku) (v, kv) ∨ PrioLT (v, kv) (u, ku)

Any two pairs with distinct handles are strictly comparable under PrioLT.

def Cslib.Algorithms.Lean.IndexedMinPQ.chooseMin {n : ℕ} (a b : Fin n × ℕ) : Fin n × ℕ

Pick the lexicographically smaller (handle, key) pair.

def Cslib.Algorithms.Lean.IndexedMinPQ.foldMin {n : ℕ} : List (Fin n × ℕ) → Option (Fin n × ℕ)

Minimum (handle, key) pair of a list under PrioLE, or none on the empty list.

def Cslib.Algorithms.Lean.IndexedMinPQ.findMin {n : ℕ} (s : State n) : Option (Fin n × ℕ)

Unique present (u, k) minimizing (k, u.val) lexicographically, or none if empty.

def Cslib.Algorithms.Lean.IndexedMinPQ.spec (n K_max : ℕ) : Stateful.Spec

Graph-free indexed min-priority queue specification with key upper bound K_max.

Domain and findMin lemmas

theorem Cslib.Algorithms.Lean.IndexedMinPQ.mem_dom_iff {n : ℕ} {s : State n} {v : Fin n} : v ∈ dom s ↔ ∃ (k : ℕ), s v = some k

A handle belongs to dom s if and only if s v is some k for some key k.

@[simp]

theorem Cslib.Algorithms.Lean.IndexedMinPQ.notMem_dom_iff {n : ℕ} {s : State n} {v : Fin n} : v ∉ dom s ↔ s v = none

A handle is outside dom s if and only if s v = none.

@[simp]

theorem Cslib.Algorithms.Lean.IndexedMinPQ.dom_empty (n : ℕ) : dom (empty n) = ∅

The empty priority queue has empty domain.

@[simp]

theorem Cslib.Algorithms.Lean.IndexedMinPQ.dom_insert {n : ℕ} (s : State n) (v : Fin n) (k : ℕ) : dom (Function.update s v (some k)) = insert v (dom s)

Updating v to some k inserts v into dom s.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.dom_decreaseKey {n : ℕ} {s : State n} {v : Fin n} (hv : v ∈ dom s) (k : ℕ) : dom (Function.update s v (some k)) = dom s

Lowering the key of a handle already in dom s preserves dom s.

@[simp]

theorem Cslib.Algorithms.Lean.IndexedMinPQ.dom_erase_update {n : ℕ} (s : State n) (u : Fin n) : dom (Function.update s u none) = (dom s).erase u

Clearing u to none erases u from dom s.

@[simp]

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_eq_none_iff {n : ℕ} {s : State n} : findMin s = none ↔ dom s = ∅

findMin s returns none if and only if dom s is empty.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_eq_some_state {n : ℕ} {s : State n} {u : Fin n} {k : ℕ} (h : findMin s = some (u, k)) : s u = some k

If findMin s = some (u, k), then s u = some k.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_mem_dom {n : ℕ} {s : State n} {u : Fin n} {k : ℕ} (h : findMin s = some (u, k)) : u ∈ dom s

Any handle returned by findMin belongs to dom s.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_le {n : ℕ} {s : State n} {u : Fin n} {k : ℕ} (h : findMin s = some (u, k)) (v : Fin n) (k' : ℕ) : s v = some k' → k < k' ∨ k = k' ∧ ↑u ≤ ↑v

findMin minimizes (k, u.val) lexicographically among all present handles.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_key_le {n : ℕ} {s : State n} {u : Fin n} {k : ℕ} (h : findMin s = some (u, k)) {v : Fin n} {k' : ℕ} (hv : s v = some k') : k ≤ k'

The key returned by findMin is at most the key of every present handle.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.findMin_eq_some_iff {n : ℕ} {s : State n} {u : Fin n} {k : ℕ} : findMin s = some (u, k) ↔ s u = some k ∧ ∀ (v : Fin n) (k' : ℕ), s v = some k' → k < k' ∨ k = k' ∧ ↑u ≤ ↑v

Complete characterization of findMin: findMin s = some (u, k) if and only if s u = some k and (u, k) precedes every present (v, k') under PrioLE.

theorem Cslib.Algorithms.Lean.IndexedMinPQ.dom_extractMin {n K_max : ℕ} {s : State n} {u : Fin n} {k : ℕ} (h : findMin s = some (u, k)) : dom ((spec n K_max).step s Op.extractMin).1 = (dom s).erase u

Domain evolution of extractMin when findMin s = some (u, k).