Grace/Cumulus/GraphTheory/WeightedPaths.g17

Open in Workbench Download source

Imports

Reachability · Nat.Order

Declarations

Source

1-- Set-theoretic weighted paths: the specification for shortest paths.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.WeightedPaths8import Reachability9import Nat.Order1011predicate WeightedGraph (V E weights : Set) :=12  RelationOn(E, V) ∧ FunctionBetween(weights, E, ℕ)1314predicate WeightedEdge (E weights u v cost : Set) :=15  Adjacent(E, u, v) ∧ Nat(cost) ∧ weights((u, v)) = cost1617-- A path result is the set-theoretic pair (ending vertex, total cost).18-- Each level is bounded by V × ℕ, and the union over finite levels19-- specifies all finite walks, including those in infinite graphs.20def costStep (V E weights previous : Set) : Set :=21  { p ∈ V × ℕ | ∃ u ∈ V, ∃ v ∈ V, ∃ c ∈ ℕ, ∃ k ∈ ℕ,22    (u, c) ∈ previous ∧ WeightedEdge(E, weights, u, v, k) ∧23    p = (v, add(c, k)) }2425def pathsOfLength (V E weights source : Set, n : Nat) → Set26  | V, E, weights, source, zero => {(source, 0)}27  | V, E, weights, source, succ(n) =>28    costStep(V, E, weights, pathsOfLength(V, E, weights, source, n))2930predicate HasPathCost (V E weights source target cost : Set) :=31  ∃ n ∈ ℕ, (target, cost) ∈ pathsOfLength(V, E, weights, source, n)3233predicate ShortestPathCost (V E weights source target cost : Set) :=34  Nat(cost) ∧ HasPathCost(V, E, weights, source, target, cost) ∧35  (∀ other ∈ ℕ, HasPathCost(V, E, weights, source, target, other) →36    LessEqual(cost, other))3738theorem ShortestPathCost.unique (V E weights source target a b : Set)39  requires first : ShortestPathCost(V, E, weights, source, target, a)40  requires second : ShortestPathCost(V, E, weights, source, target, b)41  shows a = b42proof43  rcases first with ⟨aNat, aPath, aMinimal⟩44  rcases second with ⟨bNat, bPath, bMinimal⟩45  have aIn := nat.omega.forward with aNat46  have bIn := nat.omega.forward with bNat47  have ab := aMinimal with b, bIn, bPath48  have ba := bMinimal with a, aIn, aPath49  exact LessEqual.antisymmetric with aNat, bNat, ab, ba5051theorem pathsOfLength.zero (V E weights source : Set)52  shows pathsOfLength(V, E, weights, source, 0) = {(source, 0)}53proof54  unfold pathsOfLength55  rfl5657theorem pathsOfLength.successor (V E weights source : Set, n : Nat)58  shows pathsOfLength(V, E, weights, source, succ(n)) =59    costStep(V, E, weights, pathsOfLength(V, E, weights, source, n))60proof61  unfold pathsOfLength62  rfl6364theorem HasPathCost.source (V E weights source : Set)65  shows HasPathCost(V, E, weights, source, source, 0)66proof67  unfold HasPathCost68  have zeroNat := nat.omega.forward with Naturals.constructor.zero69  have initial : (source, 0) ∈ pathsOfLength(V, E, weights, source, 0)70    rw pathsOfLength.zero71    exact singleton.self72  refine ⟨0, zeroNat, initial⟩7374theorem HasPathCost.extend (V E weights source u v c k : Set)75  requires hu : u ∈ V76  requires hv : v ∈ V77  requires hc : Nat(c)78  requires hk : Nat(k)79  requires reached : HasPathCost(V, E, weights, source, u, c)80  requires edge : WeightedEdge(E, weights, u, v, k)81  shows HasPathCost(V, E, weights, source, v, add(c, k))82proof83  rcases reached with ⟨n, hn, previous⟩84  have cIn := nat.omega.forward with hc85  have kIn := nat.omega.forward with hk86  have sumNat := add.closed at k, c with hk87  have sumIn := nat.omega.forward with sumNat88  have pair := product.pair with hv, sumIn89  have stepped : (v, add(c, k)) ∈ costStep(V, E, weights,90      pathsOfLength(V, E, weights, source, n))91    exact costStep.membership.backward with ⟨pair, u, hu, v, hv, c, cIn, k, kIn, previous, edge, rfl⟩92  have nNat := nat.omega.backward with hn93  have nextNat := Naturals.constructor.succ with nNat94  have nextIn := nat.omega.forward with nextNat95  witness succ(n)96  constructor97  . exact nextIn98  . rw pathsOfLength.successor99    exact stepped100101-- A feasible potential is a lower bound on the cost of *every* walk.102predicate PathPotential (V E weights source labels : Set) :=103  FunctionBetween(labels, V, ℕ) ∧ labels(source) = 0 ∧104  (∀ u ∈ V, ∀ v ∈ V, ∀ k ∈ ℕ,105    WeightedEdge(E, weights, u, v, k) →106    LessEqual(labels(v), add(labels(u), k)))107108theorem PathPotential.lower_bound (V E weights source labels : Set, n : Nat)109  requires potential : PathPotential(V, E, weights, source, labels)110  shows ∀ v ∈ V, ∀ c ∈ ℕ,111    (v, c) ∈ pathsOfLength(V, E, weights, source, n) →112    LessEqual(labels(v), c)113proof114  induction n115  | zero =>116    intros v hv c hc path117    rw pathsOfLength.zero at path118    have equal := singleton.membership.forward with path119    obtain ⟨vs, c0⟩ := orderedPair.injective with equal120    rcases potential with ⟨function, initial, edges⟩121    rw [vs, c0, initial]122    exact LessEqual.reflexive with Naturals.constructor.zero123  | succ(m) using ih =>124    intros v hv c hc path125    rw pathsOfLength.successor at path126    have parts := costStep.membership.forward with path127    rcases parts with ⟨bounded, u, hu, y, hy, prior, hprior,128      k, hk, earlier, edge, pairShape⟩129    obtain ⟨vy, cSum⟩ := orderedPair.injective with pairShape130    rcases potential with ⟨function, initial, edges⟩131    have priorBound := ih with u, hu, prior, hprior, earlier132    have edgeBound := edges with u, hu, y, hy, k, hk, edge133    have uNat := FunctionBetween.apply_closed with function, hu134    have yNat := FunctionBetween.apply_closed with function, hy135    have uNumber := nat.omega.backward with uNat136    have yNumber := nat.omega.backward with yNat137    have priorNat := nat.omega.backward with hprior138    have kNat := nat.omega.backward with hk139    have rightRefl := LessEqual.reflexive with kNat140    have sumBound := LessEqual.add with uNumber, priorNat, kNat, kNat, priorBound, rightRefl141    have result := LessEqual.transitive with yNumber, *{2}, edgeBound, sumBound142    rw [vy, cSum]143    exact result144145-- A feasible labeling plus a witnessed path of the same weight is a146-- complete shortest-path certificate, for paths of arbitrary finite length.147theorem PathPotential.certifies_shortest (V E weights source labels target cost : Set)148  requires potential : PathPotential(V, E, weights, source, labels)149  requires targetIn : target ∈ V150  requires costNat : Nat(cost)151  requires witness : HasPathCost(V, E, weights, source, target, cost)152  requires value : labels(target) = cost153  shows ShortestPathCost(V, E, weights, source, target, cost)154proof155  constructor156  . exact costNat157  . constructor158    . exact witness159    . intros other otherIn otherPath160      rcases otherPath with ⟨n, nIn, path⟩161      have nNat := nat.omega.backward with nIn162      have lower := PathPotential.lower_bound with nNat, potential163      have bound := lower with target, targetIn, other, otherIn, path164      rwa value at bound165