Grace/Cumulus/GraphTheory/DijkstraCut.g17

Open in Workbench Download source

Imports

WeightedPaths · Connectivity

Declarations

Source

1-- The first-unsettled-vertex argument for Dijkstra's greedy step.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.DijkstraCut8import WeightedPaths9import Connectivity1011-- S is the settled region. Its labels bound every source path.12predicate SettledLowerBounds (V E weights source S labels : Set) :=13  FunctionBetween(labels, S, ℕ) ∧14  (∀ u ∈ S, ∀ c ∈ ℕ, HasPathCost(V, E, weights, source, u, c) → labels(u) ≤ c)1516-- Before the source is settled, the next finite minimum must be zero.17-- Afterwards every route to an unsettled vertex must cross this boundary.18predicate FrontierCutBound (V E weights source S labels bound : Set) :=19  Nat(bound) ∧ (source ∈ S ∨ bound = 0) ∧20  (∀ u ∈ S, ∀ v ∈ V, ∀ k ∈ ℕ,21    ¬(v ∈ S) → WeightedEdge(E, weights, u, v, k) → bound ≤ add(labels(u), k))2223theorem FrontierCutBound.lower_bound (V E weights source S labels bound : Set, n : Nat)24  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)25  requires frontier : FrontierCutBound(V, E, weights, source, S, labels, bound)26  shows ∀ v ∈ V, ∀ c ∈ ℕ, ¬(v ∈ S) →27    (v, c) ∈ pathsOfLength(V, E, weights, source, n) → bound ≤ c28proof29  induction n30  | zero =>31    intros v hv c hc outside path32    rw pathsOfLength.zero at path33    have pair := singleton.membership.forward with path34    have coordinates := orderedPair.injective with pair35    rcases coordinates with ⟨vs, c0⟩36    rcases frontier with ⟨boundNat, initial, edges⟩37    cases initial with sourceInside | boundZero38    . exfalso39      apply outside40      rw vs41      exact sourceInside42    . rw boundZero43      rw c044      exact LessEqual.reflexive with Naturals.constructor.zero45  | succ(m) using ih =>46    intros v hv c hc outside path47    rw pathsOfLength.successor at path48    have parts := costStep.membership.forward at V, E, weights,49      pathsOfLength(V, E, weights, source, m), (v, c) with path50    rcases parts with ⟨bounded, u, hu, y, hy, prior, hprior, k, hk, earlier, edge, pair⟩51    have coordinates := orderedPair.injective with pair52    rcases coordinates with ⟨vy, cSum⟩53    have yOutside : ¬(y ∈ S)54      intro inside55      apply outside56      rw vy57      exact inside58    have priorNat := nat.omega.backward with hprior59    have kNat := nat.omega.backward with hk60    have sumNat := add.closed at k, prior with kNat61    rcases frontier with ⟨boundNat, initial, edges⟩62    have alternatives : u ∈ S ∨ ¬(u ∈ S) by tauto63    cases alternatives with uInside | uOutside64    . rcases settled with ⟨function, shortest⟩65      have mNat : Nat(m) by typecheck66      have mIn := nat.omega.forward with mNat67      have prefix : HasPathCost(V, E, weights, source, u, prior)68        unfold HasPathCost69        refine ⟨m, mIn, earlier⟩70      have priorBound := shortest with u, uInside, prior, hprior, prefix71      have crossing := edges with u, uInside, y, hy, k, hk, yOutside, edge72      have labelIn := FunctionBetween.apply_closed with function, uInside73      have labelNat := nat.omega.backward with labelIn74      have same := LessEqual.reflexive with kNat75      have sumBound := LessEqual.add with labelNat, priorNat, kNat, kNat, priorBound, same76      have labelSumNat := add.closed at k, labels(u) with kNat77      have result := LessEqual.transitive with boundNat, labelSumNat, sumNat, crossing, sumBound78      rw cSum79      exact result80    . have prefixBound := ih with u, hu, prior, hprior, uOutside, earlier81      have extensionBound := LessEqual.add_right with priorNat, kNat82      have result := LessEqual.transitive with boundNat, priorNat, sumNat, prefixBound, extensionBound83      rw cSum84      exact result8586theorem FrontierCutBound.all_paths (V E weights source S labels bound target cost : Set)87  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)88  requires frontier : FrontierCutBound(V, E, weights, source, S, labels, bound)89  requires targetIn : target ∈ V90  requires outside : ¬(target ∈ S)91  requires costNat : Nat(cost)92  requires path : HasPathCost(V, E, weights, source, target, cost)93  shows bound ≤ cost94proof95  rcases path with ⟨n, hn, reached⟩96  have nNat := nat.omega.backward with hn97  have cIn := nat.omega.forward with costNat98  have boundAll := FrontierCutBound.lower_bound with nNat, settled, frontier99  exact boundAll with target, targetIn, cost, cIn, outside, reached100101-- This is the greedy step: a witnessed minimum at the cut is globally shortest.102theorem FrontierCutBound.certifies_next (V E weights source S labels bound target : Set)103  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)104  requires frontier : FrontierCutBound(V, E, weights, source, S, labels, bound)105  requires targetIn : target ∈ V106  requires outside : ¬(target ∈ S)107  requires path : HasPathCost(V, E, weights, source, target, bound)108  shows ShortestPathCost(V, E, weights, source, target, bound)109proof110  have boundNat : Nat(bound) by simp [FrontierCutBound]111  unfold ShortestPathCost112  refine ⟨boundNat, path, _⟩113  intros other otherIn otherPath114  have otherNat := nat.omega.backward with otherIn115  exact FrontierCutBound.all_paths with settled, frontier, targetIn, outside, otherNat, otherPath116117-- F contains the discovered, unsettled vertices with finite tentative labels.118-- Every edge leaving S has already supplied a candidate in F.119predicate FrontierTable (V E weights S labels F tentative : Set) :=120  FunctionBetween(tentative, F, ℕ) ∧121  (∀ u ∈ S, ∀ v ∈ V, ∀ k ∈ ℕ,122    ¬(v ∈ S) → WeightedEdge(E, weights, u, v, k) →123    (v ∈ F ∧ tentative(v) ≤ add(labels(u), k)))124125theorem FrontierTable.cut_bound (V E weights source S labels F tentative bound : Set)126  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)127  requires table : FrontierTable(V, E, weights, S, labels, F, tentative)128  requires boundNat : Nat(bound)129  requires initial : source ∈ S ∨ bound = 0130  requires minimal : ∀ v ∈ F, bound ≤ tentative(v)131  shows FrontierCutBound(V, E, weights, source, S, labels, bound)132proof133  rcases settled with ⟨settledFunction, lower⟩134  rcases table with ⟨tentativeFunction, relaxed⟩135  unfold FrontierCutBound136  refine ⟨boundNat, initial, _⟩137  intros u hu v hv k hk outside edge138  obtain ⟨discovered, upper⟩ := relaxed with u, hu, v, hv, k, hk, outside, edge139  have chosenBound := minimal with v, discovered140  have tentativeIn := FunctionBetween.apply_closed with tentativeFunction, discovered141  have tentativeNat := nat.omega.backward with tentativeIn142  have kNat := nat.omega.backward with hk143  have labelIn := FunctionBetween.apply_closed with settledFunction, hu144  have labelNat := nat.omega.backward with labelIn145  exact LessEqual.transitive with boundNat, tentativeNat, chosenBound, upper146147theorem FrontierTable.certifies_minimum (V E weights source S labels F tentative target bound : Set)148  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)149  requires table : FrontierTable(V, E, weights, S, labels, F, tentative)150  requires boundNat : Nat(bound)151  requires initial : source ∈ S ∨ bound = 0152  requires minimal : ∀ v ∈ F, bound ≤ tentative(v)153  requires targetIn : target ∈ V154  requires outside : ¬(target ∈ S)155  requires path : HasPathCost(V, E, weights, source, target, bound)156  shows ShortestPathCost(V, E, weights, source, target, bound)157proof158  have cut := FrontierTable.cut_bound with settled, table, boundNat, initial, minimal159  exact FrontierCutBound.certifies_next with settled, cut, targetIn, outside, path160161-- Settling the certified vertex preserves the lower-bound invariant.162theorem SettledLowerBounds.enlarge (V E weights source S labels target cost updated : Set)163  requires settled : SettledLowerBounds(V, E, weights, source, S, labels)164  requires shortest : ShortestPathCost(V, E, weights, source, target, cost)165  requires function : updated : S ∪ {target} → ℕ166  requires oldValues : ∀ u ∈ S, updated(u) = labels(u)167  requires newValue : updated(target) = cost168  shows SettledLowerBounds(V, E, weights, source, S ∪ {target}, updated)169proof170  rcases settled with ⟨oldFunction, oldLower⟩171  rcases shortest with ⟨costNat, path, least⟩172  unfold SettledLowerBounds173  refine ⟨function, _⟩174  intros u hu c hc candidate175  have alternatives := union2.membership.forward with hu176  cases alternatives with old | new177  . have equality := oldValues with u, old178    rw equality179    exact oldLower with u, old, c, hc, candidate180  . have equality := singleton.membership.forward with new181    rw [equality, newValue]182    rw equality at candidate183    exact least with c, hc, candidate184185-- Weighted paths have the same finite reachability meaning as graph routes.186theorem pathsOfLength.reachable (V E weights source : Set, n : Nat)187  shows ∀ v ∈ V, ∀ c ∈ ℕ,188    (v, c) ∈ pathsOfLength(V, E, weights, source, n) → Reachable(V, E, source, v)189proof190  induction n191  | zero =>192    intros v hv c hc path193    rw pathsOfLength.zero at path194    have pair := singleton.membership.forward with path195    have coordinates := orderedPair.injective with pair196    rcases coordinates with ⟨vs, c0⟩197    rw vs198    exact Reachable.reflexive199  | succ(m) using ih =>200    intros v hv c hc path201    rw pathsOfLength.successor at path202    have parts := costStep.membership.forward at V, E, weights,203      pathsOfLength(V, E, weights, source, m), (v, c) with path204    rcases parts with ⟨bounded, u, hu, y, hy, prior, hprior, k, hk, earlier, edge, pair⟩205    have coordinates := orderedPair.injective with pair206    rcases coordinates with ⟨vy, cSum⟩207    have prefix := ih with u, hu, prior, hprior, earlier208    rcases edge with ⟨adjacent, kNat, value⟩209    rw vy210    exact Reachable.extend with prefix, hy, adjacent211212theorem HasPathCost.reachable (V E weights source target cost : Set)213  requires targetIn : target ∈ V214  requires costNat : Nat(cost)215  requires path : HasPathCost(V, E, weights, source, target, cost)216  shows Reachable(V, E, source, target)217proof218  rcases path with ⟨n, hn, reached⟩219  have nNat := nat.omega.backward with hn220  have costIn := nat.omega.forward with costNat221  have all := pathsOfLength.reachable at V, E, weights, source, n with nNat222  exact all with target, targetIn, cost, costIn, reached223224theorem EdgeClosed.excludes_path (V E weights source target cost S : Set)225  requires start : source ∈ S226  requires closed : EdgeClosed(V, E, S)227  requires targetIn : target ∈ V228  requires outside : ¬(target ∈ S)229  requires costNat : Nat(cost)230  shows ¬HasPathCost(V, E, weights, source, target, cost)231proof232  intro path233  have route := HasPathCost.reachable with targetIn, costNat, path234  have contained := Reachable.in_closed_set with start, closed, route235  exact outside with contained236237-- If relaxation has no finite candidates left, no weighted path can leave S.238theorem FrontierTable.empty_unreachable (V E weights source S labels tentative target cost : Set)239  requires table : FrontierTable(V, E, weights, S, labels, empty, tentative)240  requires graph : WeightedGraph(V, E, weights)241  requires start : source ∈ S242  requires included : S ⊆ V243  requires targetIn : target ∈ V244  requires outside : ¬(target ∈ S)245  requires costNat : Nat(cost)246  shows ¬HasPathCost(V, E, weights, source, target, cost)247proof248  rcases table with ⟨tentativeFunction, relaxed⟩249  rcases graph with ⟨relation, weightFunction⟩250  have closed : EdgeClosed(V, E, S)251    intros u hu v hv edge252    have alternatives : v ∈ S ∨ ¬(v ∈ S) by tauto253    cases alternatives with inside | out254    . exact inside255    . exfalso256      have pairIn : (u, v) ∈ E257        unfold Adjacent at edge258        exact edge259      have weightIn := FunctionBetween.apply_closed with weightFunction, pairIn260      have weightNat := nat.omega.backward with weightIn261      have weighted : WeightedEdge(E, weights, u, v, weights((u, v)))262        unfold WeightedEdge263        refine ⟨edge, weightNat, rfl⟩264      obtain ⟨inEmpty, inequality⟩ := relaxed with u, hu, v, hv, weights((u, v)), weightIn, out, weighted265      exact set.empty with inEmpty266  exact EdgeClosed.excludes_path with start, closed, targetIn, outside, costNat267