Bounded-capacity dictionary specification

This file defines a deterministic abstract specification (Cslib.Algorithms.Lean.Dictionary.spec) for a bounded-capacity dictionary mapping keys from a finite universe Fin U to natural-number values bounded by V, supporting at most n_max distinct stored keys at any point in time.

States map each key u : Fin U to Option ℕ (none when absent, some v when present with value v). Following Cslib.Algorithms.Lean.IndexedMinPQ, values are represented as ℕ with the bound v < V enforced by operation admissibility (valid), so Word-RAM realizations can encode Option ℕ in a single machine register (0 for none and v + 1 for some v) without carrying dependent Fin V proof obligations inside register decoding.

An insertion insert u v is admissible whenever v < V and either the current number of stored keys (dom s).card is strictly below the capacity bound n_max, or u is already present in s (in which case updating s u to some v overwrites the existing value in place without increasing (dom s).card). This specification models lookup-and-insert dictionaries without a deletion operation.

Main definitions

• Cslib.Algorithms.Lean.Dictionary.Op: dictionary operations (get, insert).
• Cslib.Algorithms.Lean.Dictionary.State, empty, dom: abstract map state, empty dictionary, and finite set of present keys.
• Cslib.Algorithms.Lean.Dictionary.ValuesBounded: invariant that all stored values lie below V.
• Cslib.Algorithms.Lean.Dictionary.spec: the Cslib.Stateful.Spec with universe U, value bound V, and capacity bound n_max.

Main results

• dom_empty, card_dom_empty, dom_insert: domain evolution under initialization and insertion.
• card_dom_insert_le, card_dom_insert_eq_of_isSome, card_dom_insert_eq_of_eq_none: cardinality laws for dom under in-place updates and new-key insertions.
• card_dom_step_le_of_valid, card_dom_run_le_of_validHistory, card_dom_run_empty_le: any admissible operation history starting from empty U maintains (dom s).card ≤ n_max.
• valuesBounded_empty, valuesBounded_step_of_valid, valuesBounded_run_of_validHistory: any admissible operation history maintains ValuesBounded V s.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 11

inductive Cslib.Algorithms.Lean.Dictionary.Op (U : ℕ) : Type

Lookup and insertion operations on a dictionary over keys Fin U and natural-number values.

• get {U : ℕ} (u : Fin U) : Op U

  Look up the value associated with key u, if present.

• insert {U : ℕ} (u : Fin U) (v : ℕ) : Op U

  Associate key u with value v, inserting u if absent or overwriting its value if present.

@[instance_reducible]

instance Cslib.Algorithms.Lean.Dictionary.instDecidableEqOp {U✝ : ℕ} : DecidableEq (Op U✝)

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

@[instance_reducible]

instance Cslib.Algorithms.Lean.Dictionary.instReprOp {U✝ : ℕ} : Repr (Op U✝)

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

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Dictionary.State (U : ℕ) : Type

Abstract state of a dictionary over universe Fin U.

def Cslib.Algorithms.Lean.Dictionary.empty (U : ℕ) : State U

The empty dictionary on Fin U.

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

The finite set of keys currently present in state s.

def Cslib.Algorithms.Lean.Dictionary.ValuesBounded {U : ℕ} (V : ℕ) (s : State U) : Prop

Predicate asserting that every value stored in state s is strictly less than V.

def Cslib.Algorithms.Lean.Dictionary.spec (U V n_max : ℕ) : Stateful.Spec

Bounded-capacity dictionary specification over key universe Fin U, value bound V, and maximum key count n_max.

Domain, capacity, and value-bound lemmas

@[simp]

theorem Cslib.Algorithms.Lean.Dictionary.mem_dom_iff_isSome {U : ℕ} {s : State U} {u : Fin U} : u ∈ dom s ↔ (s u).isSome = true

A key belongs to dom s if and only if (s u).isSome.

theorem Cslib.Algorithms.Lean.Dictionary.mem_dom_iff {U : ℕ} {s : State U} {u : Fin U} : u ∈ dom s ↔ ∃ (v : ℕ), s u = some v

A key belongs to dom s if and only if s u = some v for some value v.

theorem Cslib.Algorithms.Lean.Dictionary.notMem_dom_iff {U : ℕ} {s : State U} {u : Fin U} : u ∉ dom s ↔ s u = none

A key is outside dom s if and only if s u = none.

@[simp]

theorem Cslib.Algorithms.Lean.Dictionary.dom_empty (U : ℕ) : dom (empty U) = ∅

The empty dictionary has empty domain.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_empty (U : ℕ) : (dom (empty U)).card = 0

The empty dictionary stores 0 keys.

@[simp]

theorem Cslib.Algorithms.Lean.Dictionary.dom_insert {U : ℕ} (s : State U) (u : Fin U) (v : ℕ) : dom (Function.update s u (some v)) = insert u (dom s)

Updating u to some v inserts u into dom s.

theorem Cslib.Algorithms.Lean.Dictionary.dom_insert_of_mem {U : ℕ} {s : State U} {u : Fin U} (hu : u ∈ dom s) (v : ℕ) : dom (Function.update s u (some v)) = dom s

Updating a key u already in dom s preserves dom s.

theorem Cslib.Algorithms.Lean.Dictionary.dom_insert_of_isSome {U : ℕ} {s : State U} {u : Fin U} (hu : (s u).isSome = true) (v : ℕ) : dom (Function.update s u (some v)) = dom s

Updating a key u with (s u).isSome preserves dom s.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_insert_le {U : ℕ} (s : State U) (u : Fin U) (v : ℕ) : (dom (Function.update s u (some v))).card ≤ (dom s).card + 1

Updating u to some v increases (dom s).card by at most 1.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_insert_eq_of_isSome {U : ℕ} {s : State U} {u : Fin U} (hu : (s u).isSome = true) (v : ℕ) : (dom (Function.update s u (some v))).card = (dom s).card

Updating a present key u ((s u).isSome) leaves (dom s).card unchanged.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_insert_eq_of_eq_none {U : ℕ} {s : State U} {u : Fin U} (hu : s u = none) (v : ℕ) : (dom (Function.update s u (some v))).card = (dom s).card + 1

Inserting an absent key u (s u = none) increases (dom s).card by 1.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_step_le_of_valid {U V n_max : ℕ} {s : State U} {o : Op U} (hs : (dom s).card ≤ n_max) (hval : (spec U V n_max).valid s o) : (dom ((spec U V n_max).step s o).1).card ≤ n_max

Any single admissible dictionary operation preserves the capacity bound (dom s).card ≤ n_max.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_run_le_of_validHistory {U V n_max : ℕ} {s : State U} {os : List (Op U)} (hs : (dom s).card ≤ n_max) (hvh : (spec U V n_max).ValidHistory s os) : (dom ((spec U V n_max).run s os).1).card ≤ n_max

Any admissible operation history preserves (dom s).card ≤ n_max.

theorem Cslib.Algorithms.Lean.Dictionary.card_dom_run_empty_le {U V n_max : ℕ} {os : List (Op U)} (hvh : (spec U V n_max).ValidHistory (empty U) os) : (dom ((spec U V n_max).run (empty U) os).1).card ≤ n_max

Any admissible operation history starting from empty U reaches a state with at most n_max keys.

theorem Cslib.Algorithms.Lean.Dictionary.valuesBounded_empty (U V : ℕ) : ValuesBounded V (empty U)

The empty dictionary satisfies ValuesBounded V.

theorem Cslib.Algorithms.Lean.Dictionary.valuesBounded_step_of_valid {U V n_max : ℕ} {s : State U} {o : Op U} (hs : ValuesBounded V s) (hval : (spec U V n_max).valid s o) : ValuesBounded V ((spec U V n_max).step s o).1

Any single admissible dictionary operation preserves ValuesBounded V.

theorem Cslib.Algorithms.Lean.Dictionary.valuesBounded_run_of_validHistory {U V n_max : ℕ} {s : State U} {os : List (Op U)} (hs : ValuesBounded V s) (hvh : (spec U V n_max).ValidHistory s os) : ValuesBounded V ((spec U V n_max).run s os).1

Any admissible operation history preserves ValuesBounded V.