Grace/Cumulus/GraphTheory/DijkstraInvariant.g17

Open in Workbench Download source

Imports

DijkstraProgress · DijkstraCut

Declarations

Source

1-- The executable-state invariant driving Dijkstra verification.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.DijkstraInvariant8import DijkstraProgress9import DijkstraCut1011namespace Dijkstra1213def Vertices (count : Set) : Set := { v ∈ ℕ | Less(v, count) }1415-- Only entries inside the vertex domain represent graph edges. Extra matrix16-- padding is irrelevant; missing entries are handled by the executable lookup.17predicate MatrixRepresents (count rows E weights : Set) :=18  Dijkstra.TypedRows(rows) ∧ WeightedGraph(Vertices(count), E, weights) ∧19  (∀ u ∈ Vertices(count), ∀ v ∈ Vertices(count), ∀ k ∈ ℕ,20    Dijkstra.entry(Dijkstra.rowAt(rows, u), v) = Option.some(k) ↔ WeightedEdge(E, weights, u, v, k))2122predicate VectorWitnesses (count E weights source values : Set) :=23  ∀ v ∈ Vertices(count), Dijkstra.WitnessedDistance(Vertices(count), E, weights, source, v, Dijkstra.entry(values, v))2425predicate SettledCorrect (count E weights source values flags : Set) :=26  ∀ v ∈ Vertices(count), Dijkstra.flagAt(flags, v) = 1 →27    ∃ d ∈ ℕ, Dijkstra.entry(values, v) = Option.some(d) ∧28      ShortestPathCost(Vertices(count), E, weights, source, v, d)2930-- DistanceAtMost treats none as infinity. The finite settled source of an31-- edge therefore forces a finite tentative label at its open endpoint.32predicate RelaxedFrontier (count E weights values flags : Set) :=33  ∀ u ∈ Vertices(count), ∀ v ∈ Vertices(count), ∀ k ∈ ℕ,34    Dijkstra.flagAt(flags, u) = 1 → Dijkstra.flagAt(flags, v) ≠ 1 →35    WeightedEdge(E, weights, u, v, k) →36      Dijkstra.DistanceAtMost(Dijkstra.entry(values, v), Dijkstra.extension(Dijkstra.entry(values, u), Option.some(k)))3738-- The invariant speaks directly about executable accessors. Matrix agreement39-- is a separate, unchanged input premise. Only 1 means settled; no extra40-- binary-flag condition is needed for the correctness argument.41predicate StateInvariant (count E weights source values flags : Set) :=42  Nat(count) ∧ source ∈ Vertices(count) ∧43  List(Dijkstra.DistanceValues, values) ∧ List(ℕ, flags) ∧44  Dijkstra.vectorLength(values) = count ∧ ListOps.length{A := ℕ}(flags) = count ∧45  Dijkstra.entry(values, source) = Option.some(0) ∧46  VectorWitnesses(count, E, weights, source, values) ∧47  SettledCorrect(count, E, weights, source, values, flags) ∧48  RelaxedFrontier(count, E, weights, values, flags)4950-- The flag split needed when transporting the invariant across a mark.51-- Contextual simplification supplies target ≠ index while rewriting the52-- second disjunct; no exploratory split is needed in the tactic search.53theorem mark.flag_cases (index target : Nat, flags : List(ℕ))54  shows target = index ∨ Dijkstra.flagAt(Dijkstra.mark(flags, index), target) = Dijkstra.flagAt(flags, target)55proof56  simp [Dijkstra.mark.at_other]5758-- An open vertex after marking was already open before marking. This is59-- the flag premise needed to reuse the previous relaxed-frontier invariant.60theorem mark.open_was_open (index target : Nat, flags : List(ℕ))61  requires stillOpen : Dijkstra.flagAt(Dijkstra.mark(flags, index), target) ≠ 162  shows Dijkstra.flagAt(flags, target) ≠ 163proof64  have alternatives := mark.flag_cases at index, target, flags with *65  cases alternatives with selected | unchanged66  . exfalso67    apply stillOpen68    rw selected69    exact Dijkstra.mark.at_same at index, flags with *70  . intro settled71    apply stillOpen72    rwa unchanged7374theorem StateInvariant.initial (count : Nat, E weights source : Set)75  requires sourceIn : source ∈ Vertices(count)76  shows StateInvariant(count, E, weights, source,77    Dijkstra.initialDistances(count, 0, source), Dijkstra.initialFlags(count))78proof79  have sourceZero : Dijkstra.entry(Dijkstra.initialDistances(count, 0, source), source) = Option.some(0)80    simp (backchain := 2, work := 512) [Dijkstra.initialDistances.lookup, Dijkstra.initialCell.at_source, nat.omega, Vertices.membership]81  have witnesses : VectorWitnesses(count, E, weights, source, Dijkstra.initialDistances(count, 0, source))82    unfold VectorWitnesses83    simp [Vertices.membership, Dijkstra.initialDistances.lookup, Dijkstra.initialCell.witnessed]84  have allOpen : ∀ target ∈ Vertices(count), Dijkstra.flagAt(Dijkstra.initialFlags(count), target) ≠ 185    intros target targetIn86    simp (backchain := 2, work := 512) [Dijkstra.initialFlags.entry, nat.omega, Vertices.membership]87  have settled : SettledCorrect(count, E, weights, source, Dijkstra.initialDistances(count, 0, source), Dijkstra.initialFlags(count))88    intros target targetIn marked89    exfalso90    exact allOpen with target, targetIn, marked91  have frontier : RelaxedFrontier(count, E, weights, Dijkstra.initialDistances(count, 0, source), Dijkstra.initialFlags(count))92    intros u uIn v vIn k kIn marked open edge93    exfalso94    exact allOpen with u, uIn, marked95  unfold StateInvariant96  simp (backchain := 2, work := 512) [Dijkstra.initialDistances.closed, Dijkstra.initialFlags.closed, Dijkstra.initialDistances.length, Dijkstra.initialFlags.length, nat.omega, Vertices.membership]9798end Dijkstra99