Grace/Cumulus/GraphTheory/DijkstraCorrectness.g17

Open in Workbench Download source

Imports

DijkstraInvariant

Declarations

Source

1-- End-to-end correctness of the executable Dijkstra solver.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.DijkstraCorrectness8import DijkstraInvariant910namespace Dijkstra1112predicate OpenLowerBound (count values flags bound : Set) :=13  ∀ v ∈ Dijkstra.Vertices(count), ∀ d ∈ ℕ, Dijkstra.entry(values, v) = Option.some(d) →14    Dijkstra.flagAt(flags, v) ≠ 1 → bound ≤ d1516theorem minimum.open_lower_bound (count index distance : Nat, values : List(Dijkstra.DistanceValues), flags : List(ℕ))17  requires length : Dijkstra.vectorLength(values) = count18  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))19  shows OpenLowerBound(count, values, flags, distance)20proof21  intros v vIn d dIn value open22  have vInfo := Dijkstra.Vertices.membership.forward with vIn23  have bound : Less(v, ListOps.length{A := Dijkstra.DistanceValues}(values))24    unfold Dijkstra.vectorLength at length25    rw length26    simp27  exact Dijkstra.minimum.le_open_entry at Dijkstra.DistanceValues, values, flags, index, distance, v, d with Dijkstra.DistanceValues.cells, chosen, bound, value, open2829-- The cut argument in the representation used by the executable algorithm.30theorem StateInvariant.path_lower_bound (count E weights source values flags : Set, bound n : Nat)31  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)32  requires minimal : OpenLowerBound(count, values, flags, bound)33  shows ∀ v ∈ Dijkstra.Vertices(count), ∀ c ∈ ℕ, Dijkstra.flagAt(flags, v) ≠ 1 →34    (v, c) ∈ pathsOfLength(Dijkstra.Vertices(count), E, weights, source, n) → bound ≤ c35proof36  induction n37  | zero =>38    rcases invariant with ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩39    intros v vIn c cIn open path40    rw pathsOfLength.zero at path41    have pair := singleton.membership.forward with path42    obtain ⟨vs, c0⟩ := orderedPair.injective with pair43    rw vs at open44    have zeroIn := nat.omega.forward with Naturals.constructor.zero45    have least := minimal with source, sourceIn, 0, zeroIn, sourceZero, open46    rwa c047  | succ(m) using ih =>48    rcases invariant with ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩49    intros v vIn c cIn open path50    rw pathsOfLength.successor at path51    obtain ⟨bounded, u, uIn, y, yIn, prior, priorIn, k, kIn, earlier, edge, pair⟩ := costStep.membership.forward with path52    obtain ⟨vy, cSum⟩ := orderedPair.injective with pair53    rw vy at open54    have priorNat : Nat(prior) by typecheck55    have kNat : Nat(k) by typecheck56    have alternatives : Dijkstra.flagAt(flags, u) = 1 ∨ Dijkstra.flagAt(flags, u) ≠ 1 by tauto57    cases alternatives with closed | uOpen58    . have certified := settled with u, uIn, closed59      rcases certified with ⟨d, dIn, value, shortest⟩60      rcases shortest with ⟨dNat, witnessed, least⟩61      have mIn := nat.omega.forward at m with assumption62      have prefix : HasPathCost(Dijkstra.Vertices(count), E, weights, source, u, prior)63        unfold HasPathCost64        refine ⟨m, mIn, earlier⟩65      have priorBound := least with prior, priorIn, prefix66      have crossing := frontier with u, uIn, y, yIn, k, kIn, closed, open, edge67      rw value at crossing68      simp [Dijkstra.extension, Dijkstra.extendSome] at crossing69      have sumIn := nat.omega.forward at add(d, k) with assumption70      have reflexive : Option.some(add(d, k)) = Option.some(add(d, k)) by rfl71      obtain ⟨e, eIn, entryValue, upper⟩ := crossing with add(d, k), sumIn, reflexive72      have chosenBound := minimal with y, yIn, e, eIn, entryValue, open73      have first := LessEqual.transitive with chosenBound, upper74      have reflexiveK := LessEqual.reflexive with kNat75      have extension := LessEqual.add with dNat, priorBound, reflexiveK76      rw cSum77      exact LessEqual.transitive with first, extension78    . have prefixBound := ih with u, uIn, prior, priorIn, uOpen, earlier79      have extension := LessEqual.add_right with priorNat, kNat80      rw cSum81      exact LessEqual.transitive with prefixBound, extension8283theorem StateInvariant.open_path_bound (count E weights source values flags target : Set, bound cost : Nat)84  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)85  requires minimal : OpenLowerBound(count, values, flags, bound)86  requires targetIn : target ∈ Dijkstra.Vertices(count)87  requires open : Dijkstra.flagAt(flags, target) ≠ 188  requires path : HasPathCost(Dijkstra.Vertices(count), E, weights, source, target, cost)89  shows bound ≤ cost90proof91  rcases path with ⟨n, nIn, reached⟩92  have costIn := nat.omega.forward at cost with assumption93  have lower := Dijkstra.StateInvariant.path_lower_bound at count, E, weights, source, values, flags, bound, n with invariant, minimal94  exact lower with target, targetIn, cost, costIn, open, reached9596theorem StateInvariant.certifies_minimum (count index distance : Nat, E weights source values flags : Set)97  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)98  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))99  shows ShortestPathCost(Dijkstra.Vertices(count), E, weights, source, index, distance)100proof101  obtain ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩ := invariant102  obtain ⟨bound, value, open⟩ := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with valuesType, flagsType, Dijkstra.DistanceValues.cells, chosen103  have indexIn : index ∈ Dijkstra.Vertices(count)104    apply Dijkstra.Vertices.membership.backward105    constructor106    . exact nat.omega.forward at index with assumption107    . unfold Dijkstra.vectorLength at valuesLength108      rwa ← valuesLength109  have minimal := minimum.open_lower_bound at count, index, distance, values, flags with *110  have distanceIn := nat.omega.forward at distance with assumption111  have witness := witnesses with index, indexIn112  have path := witness with distance, distanceIn, value113  unfold ShortestPathCost114  refine ⟨assumption, path, _⟩115  intros c cIn candidate116  exact Dijkstra.StateInvariant.open_path_bound with invariant, minimal, indexIn, open, candidate117118119theorem DistanceAtMost.transitive (a b c : Set)120  requires first : Dijkstra.DistanceAtMost(a, b)121  requires second : Dijkstra.DistanceAtMost(b, c)122  shows Dijkstra.DistanceAtMost(a, c)123proof124  intros e eIn value125  obtain ⟨d, dIn, bValue, de⟩ := second with e, eIn, value126  obtain ⟨f, fIn, aValue, fd⟩ := first with d, dIn, bValue127  refine ⟨f, fIn, aValue, _⟩128  arith129130theorem DistanceAtMost.zero (value : Set)131  requires bound : Dijkstra.DistanceAtMost(value, Option.some(0))132  shows value = Option.some(0)133proof134  have zeroIn := nat.omega.forward at 0 with assumption135  have reflexive : Option.some(0) = Option.some(0) by rfl136  obtain ⟨d, dIn, equality, leZero⟩ := bound with 0, zeroIn, reflexive137  have dNat : Nat(d) by typecheck138  have nonnegative := Grace.Core.Nat.Order.LessEqual.zero with dNat139  have zero := LessEqual.antisymmetric with dNat, Naturals.constructor.zero, leZero, nonnegative140  rwa zero at equality141142theorem minOption.le_finite (old : Option(ℕ), cost : Nat)143  shows Dijkstra.DistanceAtMost(Dijkstra.minOption(old, Option.some(cost)), Option.some(cost))144proof145  have cases := Dijkstra.option_cases at old with assumption146  cases cases with absent | finite147  . rw absent148    simp [Dijkstra.minOption]149    exact Dijkstra.DistanceAtMost.reflexive150  . rcases finite with ⟨d, dIn, value⟩151    obtain ⟨e, eIn, computed, choices, oldBound, newBound⟩ := Dijkstra.minOption.finite at d, cost with assumption152    intros c cIn same153    have equal := Option.inductive.injective.some with same154    refine ⟨e, eIn, _, _⟩155    . rw value156      exact computed157    . rw ← equal158      exact newBound159160theorem relax.entry_settled (values : List(Dijkstra.DistanceValues), row flags distance : Set, index : Nat)161  requires bound : Less(index, Dijkstra.vectorLength(values))162  requires closed : Dijkstra.flagAt(flags, index) = 1163  shows Dijkstra.entry(Dijkstra.relax(row, values, flags, distance), index) = Dijkstra.entry(values, index)164proof165  unfold Dijkstra.vectorLength at bound166  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, row, flags, distance with *167  rw [pointwise, closed]168  simp [Grace.Cumulus.Nat.Mod.equalNat.reflexive, Dijkstra.relaxValue]169170theorem relax.entry_edge_bound (values row : List(Dijkstra.DistanceValues), flags : List(ℕ), index distance weight : Nat)171  requires bound : Less(index, Dijkstra.vectorLength(values))172  requires open : Dijkstra.flagAt(flags, index) ≠ 1173  requires edge : Dijkstra.entry(row, index) = Option.some(weight)174  shows Dijkstra.DistanceAtMost(Dijkstra.entry(Dijkstra.relax(row, values, flags, Option.some(distance)), index), Option.some(add(distance, weight)))175proof176  have oldType := Dijkstra.entry.valid at Dijkstra.DistanceValues, index, values with Dijkstra.DistanceValues.cells177  have no := Dijkstra.equalNat.false_iff.backward with open178  have sumNat : Nat(add(distance, weight)) by typecheck179  have least := minOption.le_finite with oldType, sumNat180  unfold Dijkstra.vectorLength at bound181  have pointwise := Dijkstra.relax.entry at Dijkstra.DistanceValues, index, values, row, flags, Option.some(distance) with *182  have computed : Dijkstra.entry(Dijkstra.relax(row, values, flags, Option.some(distance)), index) = Dijkstra.minOption(Dijkstra.entry(values, index), Option.some(add(distance, weight)))183    settle with pointwise, no, edge, Dijkstra.relaxValue, Dijkstra.extension, Dijkstra.extendSome184  rwa computed185186187theorem StateInvariant.relax_selected (count index distance : Nat, E weights source rows values flags : Set)188  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)189  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)190  requires chosen : Dijkstra.minimum(values, flags, 0) = Option.some(Dijkstra.Candidate.value(index, distance))191  shows Dijkstra.StateInvariant(count, E, weights, source,192    Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index))193proof194  have certified := Dijkstra.StateInvariant.certifies_minimum at count, index, distance, E, weights, source, values, flags with *195  rcases invariant with ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩196  rcases matrix with ⟨rowsTyped, graph, edges⟩197  have indexInNat := nat.omega.forward at index with assumption198  have distanceIn := nat.omega.forward at distance with assumption199  have rowType := rowsTyped with index, indexInNat200  have distanceType := Option.inductive.constructor.some with distanceIn201  obtain ⟨indexBound, selectedValue, selectedOpen⟩ := Dijkstra.minimum.selected_entry at Dijkstra.DistanceValues, values, flags, index, distance with valuesType, flagsType, Dijkstra.DistanceValues.cells, chosen202  have indexIn : index ∈ Dijkstra.Vertices(count)203    apply Dijkstra.Vertices.membership.backward204    refine ⟨indexInNat, _⟩205    unfold Dijkstra.vectorLength at valuesLength206    rwa ← valuesLength207  have markedType := Dijkstra.mark.closed at index, flags with flagsType208  have markedLength := Dijkstra.mark.length at index, flags with flagsType209  rw flagsLength at markedLength210  have relaxedType := Dijkstra.relax.closed with valuesType, rowType, markedType, distanceType211  have relaxedLength := Dijkstra.relax.length at Dijkstra.DistanceValues, values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance) with valuesType212  rw valuesLength at relaxedLength213  have indexVectorBound : Less(index, Dijkstra.vectorLength(values))214    unfold Dijkstra.vectorLength215    exact indexBound216  have indexClosed := Dijkstra.mark.at_same at index, flags with flagsType217  have newSelected : Dijkstra.entry(Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), index) = Option.some(distance)218    have same := relax.entry_settled at values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance), index with valuesType, indexVectorBound, indexClosed219    rwa same220  have newSource : Dijkstra.entry(Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), source) = Option.some(0)221    have sourceInfo := Dijkstra.Vertices.membership.forward with sourceIn222    have bound : Less(source, ListOps.length{A := Dijkstra.DistanceValues}(values))223      unfold Dijkstra.vectorLength at valuesLength224      rw valuesLength225      simp226    have decreasing := Dijkstra.relax.entry_no_increase with valuesType, rowType, markedType, distanceType, bound227    rw sourceZero at decreasing228    exact Dijkstra.DistanceAtMost.zero with decreasing229  have newWitnesses : Dijkstra.VectorWitnesses(count, E, weights, source, Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)))230    intros v vIn231    have vInfo := Dijkstra.Vertices.membership.forward with vIn232    have bound : Less(v, ListOps.length{A := Dijkstra.DistanceValues}(values))233      unfold Dijkstra.vectorLength at valuesLength234      rw valuesLength235      simp236    have oldPaths := witnesses with v, vIn237    have sourcePaths := witnesses with index, indexIn238    rw selectedValue at sourcePaths239    have represented : ∀ k ∈ ℕ, Dijkstra.entry(Dijkstra.rowAt(rows, index), v) = Option.some(k) → WeightedEdge(E, weights, index, v, k)240      intros k kIn value241      have agreement := edges with index, indexIn, v, vIn, k, kIn242      exact agreement.forward with value243    exact Dijkstra.relax.entry_witnessed with valuesType, rowType, distanceType, bound, indexIn, vIn, oldPaths, sourcePaths, represented244  have newSettled : Dijkstra.SettledCorrect(count, E, weights, source, Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index))245    intros v vIn closed246    have vInfo := Dijkstra.Vertices.membership.forward with vIn247    have bound : Less(v, Dijkstra.vectorLength(values))248      rw valuesLength249      simp250    have alternatives := Dijkstra.mark.flag_cases at index, v, flags with flagsType251    cases alternatives with same | unchanged252    . rw under same253      refine ⟨distance, distanceIn, newSelected, certified⟩254    . have wasClosed := closed255      rw unchanged at wasClosed256      obtain ⟨d, dIn, value, shortest⟩ := settled with v, vIn, wasClosed257      have preserved := relax.entry_settled at values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance), v with valuesType, bound, closed258      refine ⟨d, dIn, _, shortest⟩259      rwa preserved260  have newFrontier : Dijkstra.RelaxedFrontier(count, E, weights, Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index))261    intros u uIn v vIn k kIn closed open edge262    have uInfo := Dijkstra.Vertices.membership.forward with uIn263    have vInfo := Dijkstra.Vertices.membership.forward with vIn264    have uBound : Less(u, Dijkstra.vectorLength(values))265      rw valuesLength266      simp267    have vBound : Less(v, Dijkstra.vectorLength(values))268      rw valuesLength269      simp270    have sameU := relax.entry_settled at values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), Option.some(distance), u with valuesType, uBound, closed271    rw sameU272    have alternatives := Dijkstra.mark.flag_cases at index, u, flags with flagsType273    cases alternatives with same | unchanged274    . rw [same, selectedValue]275      have shifted := edge276      rw same at shifted277      have agreement := edges with index, indexIn, v, vIn, k, kIn278      have weightValue := agreement.backward with shifted279      have relaxed := relax.entry_edge_bound at values, Dijkstra.rowAt(rows, index), Dijkstra.mark(flags, index), v, distance, k with valuesType, rowType, vBound, open, weightValue280      simp [Dijkstra.extension, Dijkstra.extendSome]281    . have wasClosed := closed282      rw unchanged at wasClosed283      have wasOpen := Dijkstra.mark.open_was_open with flagsType, open284      have old := frontier with u, uIn, v, vIn, k, kIn, wasClosed, wasOpen, edge285      unfold Dijkstra.vectorLength at vBound286      have decreasing := Dijkstra.relax.entry_no_increase with valuesType, rowType, markedType, distanceType, vBound287      exact Dijkstra.DistanceAtMost.transitive with decreasing, old288  unfold Dijkstra.StateInvariant289  refine ⟨countNat, sourceIn, relaxedType, markedType, relaxedLength, markedLength, newSource, newWitnesses, newSettled, newFrontier⟩290291292theorem StateInvariant.advance (count : Nat, E weights source rows values flags : Set)293  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)294  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)295  shows ∃ nextValues, ∃ nextFlags,296    Dijkstra.advance(rows, Dijkstra.State.current(values, flags)) = Dijkstra.State.current(nextValues, nextFlags) ∧297    Dijkstra.StateInvariant(count, E, weights, source, nextValues, nextFlags)298proof299  obtain ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩ := invariant300  obtain ⟨valid, member, least⟩ := Dijkstra.minimum.correct at Dijkstra.DistanceValues, values, flags, 0 with valuesType, flagsType, Naturals.constructor.zero, Dijkstra.DistanceValues.cells301  cases valid with absent | finite302  . have fixed := Dijkstra.advance.none at rows, values, flags with absent303    refine ⟨values, flags, fixed, invariant⟩304  . rcases finite with ⟨index, indexIn, distance, distanceIn, chosen⟩305    have preserved := Dijkstra.StateInvariant.relax_selected with invariant, matrix, chosen306    refine ⟨Dijkstra.relax(Dijkstra.rowAt(rows, index), values, Dijkstra.mark(flags, index), Option.some(distance)), Dijkstra.mark(flags, index), _, preserved⟩307    simp [Dijkstra.advance, Dijkstra.advanceChosen]308309theorem StateInvariant.iterate (count fuel : Nat, E weights source rows values flags : Set)310  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)311  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)312  shows Dijkstra.StateInvariant(count, E, weights, source,313    Dijkstra.distances(Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags))),314    Dijkstra.settled(Dijkstra.iterate(fuel, rows, Dijkstra.State.current(values, flags))))315proof316  induction fuel generalizing values flags317  | zero =>318    intros values flags invariant319    rwa [Dijkstra.iterate, Dijkstra.distances, Dijkstra.settled]320  | succ(k) using ih =>321    intros values flags invariant322    obtain ⟨nextValues, nextFlags, advanced, preserved⟩ := Dijkstra.StateInvariant.advance with invariant, matrix323    have previous := ih with nextValues, nextFlags, preserved324    rwa [Dijkstra.iterate, advanced]325326theorem solve.invariant (count source : Nat, E weights rows : Set)327  requires sourceIn : source ∈ Dijkstra.Vertices(count)328  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)329  shows Dijkstra.StateInvariant(count, E, weights, source,330    Dijkstra.distances(Dijkstra.solve(count, source, rows)), Dijkstra.settled(Dijkstra.solve(count, source, rows)))331proof332  have initial := Dijkstra.StateInvariant.initial at count, E, weights, source with sourceIn333  have preserved := Dijkstra.StateInvariant.iterate at count, count, E, weights, source, rows, Dijkstra.initialDistances(count, 0, source), Dijkstra.initialFlags(count) with *334  rwa Dijkstra.solve335336theorem StateInvariant.finished_finite (count target distance : Nat, E weights source values flags : Set)337  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)338  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none339  requires targetIn : target ∈ Dijkstra.Vertices(count)340  requires value : Dijkstra.entry(values, target) = Option.some(distance)341  shows ShortestPathCost(Dijkstra.Vertices(count), E, weights, source, target, distance)342proof343  rcases invariant with ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩344  have targetInfo := Dijkstra.Vertices.membership.forward with targetIn345  have bound : Less(target, ListOps.length{A := Dijkstra.DistanceValues}(values))346    unfold Dijkstra.vectorLength at valuesLength347    rw valuesLength348    simp349  have closed := Dijkstra.minimum.none_no_open_finite at Dijkstra.DistanceValues, values, flags, target, distance with valuesType, flagsType, Dijkstra.DistanceValues.cells, absent, bound, value350  obtain ⟨d, dIn, entryValue, shortest⟩ := settled with target, targetIn, closed351  rw value at entryValue352  have same := Option.inductive.injective.some with entryValue353  rwa same354355theorem StateInvariant.finished_open_unreachable (count target cost : Nat, E weights source values flags : Set)356  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)357  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none358  requires targetIn : target ∈ Dijkstra.Vertices(count)359  requires open : Dijkstra.flagAt(flags, target) ≠ 1360  shows ¬HasPathCost(Dijkstra.Vertices(count), E, weights, source, target, cost)361proof362  intro path363  obtain ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩ := invariant364  have arbitraryBound : OpenLowerBound(count, values, flags, succ(cost))365    intros v vIn d dIn value vOpen366    have vInfo := Dijkstra.Vertices.membership.forward with vIn367    have bound : Less(v, ListOps.length{A := Dijkstra.DistanceValues}(values))368      unfold Dijkstra.vectorLength at valuesLength369      rw valuesLength370      simp371    have closed := Dijkstra.minimum.none_no_open_finite at Dijkstra.DistanceValues, values, flags, v, d with valuesType, flagsType, Dijkstra.DistanceValues.cells, absent, bound, value372    exfalso373    exact vOpen with closed374  have impossible := Dijkstra.StateInvariant.open_path_bound with invariant, arbitraryBound, targetIn, open, path375  have strict : cost < cost by exact impossible376  exact Less.irreflexive with strict377378theorem StateInvariant.finished_none (count target : Nat, E weights source values flags : Set)379  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)380  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none381  requires targetIn : target ∈ Dijkstra.Vertices(count)382  shows Dijkstra.entry(values, target) = Option.none ↔383    (∀ cost ∈ ℕ, ¬HasPathCost(Dijkstra.Vertices(count), E, weights, source, target, cost))384proof385  obtain ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩ := invariant386  constructor387  . intro value388    have open : Dijkstra.flagAt(flags, target) ≠ 1389      intro closed390      obtain ⟨settledDistance, settledIn, entryValue, shortest⟩ := settled with target, targetIn, closed391      rw value at entryValue392      exact Option.inductive.disjoint.none.some with entryValue393    intros cost costIn394    exact Dijkstra.StateInvariant.finished_open_unreachable at count, target, cost, E, weights, source, values, flags with *395  . intro unreachable396    have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, target, values with valuesType, Dijkstra.DistanceValues.cells397    have shape := Dijkstra.option_cases with valueType398    cases shape with none | some399    . exact none400    . rcases some with ⟨d, dIn, value⟩401      have witness := witnesses with target, targetIn402      have path := witness with d, dIn, value403      have impossible := unreachable with d, dIn404      exfalso405      exact impossible with path406407theorem StateInvariant.finished_value (count target distance : Nat, E weights source values flags : Set)408  requires invariant : Dijkstra.StateInvariant(count, E, weights, source, values, flags)409  requires absent : Dijkstra.minimum(values, flags, 0) = Option.none410  requires targetIn : target ∈ Dijkstra.Vertices(count)411  shows Dijkstra.entry(values, target) = Option.some(distance) ↔412    ShortestPathCost(Dijkstra.Vertices(count), E, weights, source, target, distance)413proof414  constructor415  . intro value416    exact Dijkstra.StateInvariant.finished_finite at count, target, distance, E, weights, source, values, flags with *417  . intro shortest418    obtain ⟨countNat, sourceIn, valuesType, flagsType, valuesLength, flagsLength, sourceZero, witnesses, settled, frontier⟩ := invariant419    have valueType := Dijkstra.entry.valid at Dijkstra.DistanceValues, target, values with valuesType, Dijkstra.DistanceValues.cells420    have shape := Dijkstra.option_cases with valueType421    cases shape with none | some422    . have characterization := Dijkstra.StateInvariant.finished_none at count, target, E, weights, source, values, flags with invariant, absent, targetIn423      have unreachable := characterization.forward with none424      have distanceIn := nat.omega.forward at distance with assumption425      have impossible := unreachable with distance, distanceIn426      rcases shortest with ⟨distanceNat, path, least⟩427      exfalso428      exact impossible with path429    . rcases some with ⟨d, dIn, value⟩430      have certified := Dijkstra.StateInvariant.finished_finite at count, target, d, E, weights, source, values, flags with *431      have same := ShortestPathCost.unique with certified, shortest432      rwa same at value433434-- For every natural size, represented nonnegative weighted graph, and source435-- in range: finite results are shortest, and none is exactly unreachability.436theorem solve.correct (count source target : Nat, E weights rows : Set)437  requires sourceIn : source ∈ Dijkstra.Vertices(count)438  requires targetIn : target ∈ Dijkstra.Vertices(count)439  requires matrix : Dijkstra.MatrixRepresents(count, rows, E, weights)440  shows (∀ distance ∈ ℕ,441    Dijkstra.entry(Dijkstra.distances(Dijkstra.solve(count, source, rows)), target) = Option.some(distance) ↔442      ShortestPathCost(Dijkstra.Vertices(count), E, weights, source, target, distance)) ∧443    (Dijkstra.entry(Dijkstra.distances(Dijkstra.solve(count, source, rows)), target) = Option.none ↔444      (∀ cost ∈ ℕ, ¬HasPathCost(Dijkstra.Vertices(count), E, weights, source, target, cost)))445proof446  have invariant := solve.invariant at count, source, E, weights, rows with *447  have rowsTyped : Dijkstra.TypedRows(rows) by simp [Dijkstra.MatrixRepresents]448  have absent := Dijkstra.solve.exhausts_finite_frontier at count, source, rows with *449  constructor450  . intros distance distanceIn451    exact Dijkstra.StateInvariant.finished_value at count, target, distance, E, weights, source, Dijkstra.distances(Dijkstra.solve(count, source, rows)), Dijkstra.settled(Dijkstra.solve(count, source, rows)) with *452  . exact Dijkstra.StateInvariant.finished_none at count, target, E, weights, source, Dijkstra.distances(Dijkstra.solve(count, source, rows)), Dijkstra.settled(Dijkstra.solve(count, source, rows)) with invariant, absent, targetIn453454end Dijkstra455