Grace/Cumulus/GraphTheory/DijkstraStep.g17

Open in Workbench Download source

Imports

DijkstraInitial · DijkstraIndex

Declarations

Source

1-- Checked semantics of an executable Dijkstra advancement.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.DijkstraStep8import DijkstraInitial9import DijkstraIndex1011namespace Dijkstra121314theorem relax.entry_no_increase (values weights : List(Dijkstra.DistanceValues), flags : List(ℕ), sourceDistance : Option(ℕ), index : Nat)15  requires bound : Less(index, ListOps.length{A := Dijkstra.DistanceValues}(values))16  shows Dijkstra.DistanceAtMost(Dijkstra.entry(Dijkstra.relax(weights, values, flags, sourceDistance), index), Dijkstra.entry(values, index))17proof18  have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, values with Dijkstra.DistanceValues.cells19  have weightType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, weights with Dijkstra.DistanceValues.cells20  have flagNat := Dijkstra.flagAt.natural at index, flags with *21  have condition := Dijkstra.equalNat.boolean at Dijkstra.flagAt(flags, index), 1 with flagNat, assumption22  have monotone := Dijkstra.relaxValue.no_increase at Dijkstra.entry(values, index), Dijkstra.entry(weights, index), sourceDistance, equalNat(Dijkstra.flagAt(flags, index), 1) with valueType, weightType23  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, weights, flags, sourceDistance with *24  rwa pointwise2526theorem relax.entry_witnessed (V E weights source u : Set, values row : List(Dijkstra.DistanceValues), flags : List(ℕ), sourceDistance : Option(ℕ), index : Nat)27  requires bound : Less(index, ListOps.length{A := Dijkstra.DistanceValues}(values))28  requires hu : u ∈ V29  requires hv : index ∈ V30  requires oldPaths : Dijkstra.WitnessedDistance(V, E, weights, source, index, Dijkstra.entry(values, index))31  requires sourcePaths : Dijkstra.WitnessedDistance(V, E, weights, source, u, sourceDistance)32  requires edges : ∀ k ∈ ℕ, Dijkstra.entry(row, index) = Option.some(k) → WeightedEdge(E, weights, u, index, k)33  shows Dijkstra.WitnessedDistance(V, E, weights, source, index, Dijkstra.entry(Dijkstra.relax(row, values, flags, sourceDistance), index))34proof35  have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, values with Dijkstra.DistanceValues.cells36  have weightType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, row with Dijkstra.DistanceValues.cells37  have flagNat := Dijkstra.flagAt.natural at index, flags with *38  have condition := Dijkstra.equalNat.boolean at Dijkstra.flagAt(flags, index), 1 with flagNat, assumption39  have witnessed := Dijkstra.WitnessedDistance.relax with valueType, weightType, hu, hv, oldPaths, sourcePaths, edges40  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, row, flags, sourceDistance with *41  rwa pointwise4243theorem advance.selected_distance (rows : Set, values : List(Dijkstra.DistanceValues), flags : List(ℕ), index distance : Nat)44  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))45  shows Dijkstra.entry(Dijkstra.distances(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), index) = Option.some(distance)46proof47  have selected := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with *{4}, Dijkstra.DistanceValues.cells, chosen48  rcases selected with ⟨bound, entryValue, open⟩49  have marked := Dijkstra.mark.at_same at index, flags with *50  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance) with *51  have computed : Dijkstra.distances(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance))52    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.distances, chosen53  rw computed54  rw pointwise55  rw marked56  have same := Grace.Cumulus.Nat.Mod.equalNat.reflexive at 1 with assumption57  rw same58  have preserved : Dijkstra.relaxValue(Dijkstra.entry(values, index), Dijkstra.entry(Dijkstra.rowAt(rows, index), index), Bool.true, Option.some(distance)) = Dijkstra.entry(values, index)59    settle with Dijkstra.relaxValue60  rw preserved61  exact entryValue6263theorem advance.selected_settled (rows values : Set, flags : List(ℕ), index distance : Nat)64  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))65  shows Dijkstra.flagAt(Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), index) = 166proof67  have computed : Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.mark(flags, index)68    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.settled, chosen69  rw computed70  exact Dijkstra.mark.at_same at index, flags with *7172theorem advance.other_flag (rows values : Set, flags : List(ℕ), index distance target : Nat)73  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))74  requires distinct : target ≠ index75  shows Dijkstra.flagAt(Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))), target) = Dijkstra.flagAt(flags, target)76proof77  have computed : Dijkstra.settled(Dijkstra.advance(rows, Dijkstra.State.current(values, flags))) = Dijkstra.mark(flags, index)78    settle with Dijkstra.advance, Dijkstra.advanceChosen, Dijkstra.settled, chosen79  rw computed80  exact Dijkstra.mark.at_other at index, target, flags with *8182theorem advance.none (rows values flags : Set)83  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none84  shows Dijkstra.advance(rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(values, flags)85proof86  unfold Dijkstra.advance87  simp [Dijkstra.advanceChosen]8889theorem iterate.none (fuel : Nat, rows values flags : Set)90  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none91  shows Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(values, flags)92proof93  induction fuel94  | zero =>95    simp [Dijkstra.iterate]96  | succ(k) using ih =>97    have fixed := advance.none at rows, values, flags with absent98    simp [Dijkstra.iterate]99100end Dijkstra101