Bellman–Ford algorithm
StructureWeighted directed edge#✓fully proved
A weighted directed edge on the vertices \(0, \dots, n-1\) consists of a source vertex, a target vertex and an integer weight.
Bellman-Ford takes a list of such edges, so each entry is one edge occurrence.
public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqUsed by 60
DefinitionWeight-forgetting directed graph#✓fully proved
For a list of weighted edges on the vertices \(\{0, \dots, n-1\}\), the associated ordered directed graph enumerates its vertices as \(0, 1, \dots, n-1\), and the outgoing neighbor list of a vertex \(u\) is the list of targets of the edges of the list with source \(u\), in the order in which they occur and with repetitions.
@[expose] public def toDirectedAdjacency {n : Nat}
(edges : List (Edge n)) : DirectedAdjacency (Fin n) where
vertices := List.finRange n
vertices_nodup := List.nodup_finRange n
vertices_complete := List.mem_finRange
adjacency source :=
(edges.filter fun edge => decide (edge.source = source)).map Edge.targetpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
structure DirectedAdjacency (V : Type u) where
/-- The complete deterministic enumeration of vertices. -/
vertices : List V
/-- The vertex enumeration contains no duplicates. -/
vertices_nodup : vertices.Nodup
/-- Every vertex occurs in the enumeration. -/
vertices_complete : ∀ vertex, vertex ∈ vertices
/-- The ordered outgoing neighbors of each vertex. Entries may repeat. -/
adjacency : V → List VCSLibExt/Algorithms/Lean/Graph/DirectedAdjacency.lean:32
adjacency : V → List VCSLibExt/Algorithms/Lean/Graph/DirectedAdjacency.lean:40
target : Fin nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:63
Uses 2 · Used by 27
DefinitionVertices of a path#✓fully proved
For a vertex \(s\) of \(\{0, \dots, n-1\}\) and a list of weighted edges \(e_1, \dots, e_k\) on these vertices, the vertices of the path from \(s\) along this list are the list \(s, t_1, \dots, t_k\), where \(t_i\) is the target of \(e_i\).
The edges are not required to be consecutive.
@[expose] public def pathVertices {n : Nat}
(source : Fin n) (path : List (Edge n)) : List (Fin n) :=
source :: path.map Edge.targetpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
target : Fin nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:63
Uses 1 · Used by 17
DefinitionBellman–Ford path weight#✓fully proved
The weight of a list of integer-weighted edges is the sum of the weights of its entries, an edge occurring several times being counted each time.
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:65
Uses 1 · Used by 33
DefinitionWeighted path in an edge list#✓fully proved
Let \(E\) be a list of weighted directed edges on the vertices \(0, \dots, n-1\). A list \(P = (e_1, \dots, e_k)\) of weighted directed edges is a weighted path in \(E\) from \(s\) to \(t\) when every \(e_i\) belongs to \(E\), the target of \(e_i\) is the source of \(e_{i+1}\) for every \(i < k\), and either \(k = 0\) and \(s = t\), or \(k \ge 1\), the source of \(e_1\) is \(s\) and the target of \(e_k\) is \(t\).
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
target : Fin nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:63
Uses 1 · Used by 36
TheoremEdges of the weight-forgetting graph#✓fully proved
For a list \(E\) of weighted directed edges on the vertices \(0, \dots, n-1\) and vertices \(u\), \(v\), the graph obtained from \(E\) by forgetting weights has an edge from \(u\) to \(v\) if and only if some edge in \(E\) has source \(u\) and target \(v\).
public theorem edge_toDirectedAdjacency_iff {n : Nat} {edges : List (Edge n)} {u v : Fin n} :
(toDirectedAdjacency edges).Edge u v ↔
∃ edge, edge ∈ edges ∧ edge.source = u ∧ edge.target = vpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def toDirectedAdjacency {n : Nat}
(edges : List (Edge n)) : DirectedAdjacency (Fin n) where
vertices := List.finRange n
vertices_nodup := List.nodup_finRange n
vertices_complete := List.mem_finRange
adjacency source :=
(edges.filter fun edge => decide (edge.source = source)).map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:69
Uses 3 · Used by 11
TheoremTail of a weighted path#✓fully proved
Let \(E\) be a list of weighted directed edges on the vertices \(0, \dots, n-1\) and let \(s\) and \(t\) be vertices. If the list consisting of an edge \(e\) followed by a list \(R\) of edges is a weighted path in \(E\) from \(s\) to \(t\), then \(R\) is a weighted path in \(E\) from the target of \(e\) to \(t\).
public theorem isWeightedPath_tail {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {first : Edge n} {rest : List (Edge n)}
(path : IsWeightedPath edges source target (first :: rest)) :
IsWeightedPath edges first.target target restpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
Uses 2 · Used by 4
TheoremAppending an edge to a weighted path#✓fully proved
Let \(E\) be a list of weighted directed edges on the vertices \(0, \dots, n-1\) and let \(s\), \(m\) and \(t\) be vertices. If \(P\) is a weighted path in \(E\) from \(s\) to \(m\) and \(e\) is an edge belonging to \(E\) with source \(m\) and target \(t\), then the list \(P\) followed by \(e\) is a weighted path in \(E\) from \(s\) to \(t\).
public theorem isWeightedPath_append_edge {n : Nat} {edges : List (Edge n)}
{source middle target : Fin n} {path : List (Edge n)} {edge : Edge n}
(path_valid : IsWeightedPath edges source middle path)
(edge_mem : edge ∈ edges) (edge_source : edge.source = middle)
(edge_target : edge.target = target) :
IsWeightedPath edges source target (path ++ [edge])public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
Uses 2 · Used by 10
TheoremWeight of a path with an edge appended#✓fully proved
For every list \(P\) of weighted directed edges on the vertices \(0, \dots, n-1\) and every weighted directed edge \(e\) on these vertices, the weight of the list \(P\) followed by \(e\) is the weight of \(P\) plus the weight of \(e\).
public theorem pathWeight_append_edge {n : Nat} (path : List (Edge n)) (edge : Edge n) :
pathWeight (path ++ [edge]) = pathWeight path + edge.weightpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
Uses 2 · Used by 10
TheoremWeighted paths give walks of the same length#✓fully proved
Let \(E\) be a list of weighted directed edges on the vertices \(0, \dots, n-1\) and let \(s\) and \(t\) be vertices. If a list \(P\) of \(k\) edges is a weighted path in \(E\) from \(s\) to \(t\), then there is a walk of length \(k\) from \(s\) to \(t\) in the directed graph obtained from \(E\) by forgetting the weights.
public theorem isWeightedPath_walk {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {path : List (Edge n)}
(path_valid : IsWeightedPath edges source target path) :
(toDirectedAdjacency edges).Walk path.length source targetpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
@[expose] public def toDirectedAdjacency {n : Nat}
(edges : List (Edge n)) : DirectedAdjacency (Fin n) where
vertices := List.finRange n
vertices_nodup := List.nodup_finRange n
vertices_complete := List.mem_finRange
adjacency source :=
(edges.filter fun edge => decide (edge.source = source)).map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:69
Uses 6 · Used by 9
TheoremReachability by weighted paths#✓fully proved
For a list of weighted edges on the vertices \(\{0, \dots, n-1\}\) and vertices \(s\) and \(t\), the vertex \(t\) is reachable from \(s\) in the directed graph obtained from the list by forgetting the weights if and only if there is a weighted path from \(s\) to \(t\) using edges of the list.
public theorem reachable_iff_exists_isWeightedPath {n : Nat} {edges : List (Edge n)}
{source target : Fin n} :
(toDirectedAdjacency edges).Reachable source target ↔
∃ path, IsWeightedPath edges source target pathpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def toDirectedAdjacency {n : Nat}
(edges : List (Edge n)) : DirectedAdjacency (Fin n) where
vertices := List.finRange n
vertices_nodup := List.nodup_finRange n
vertices_complete := List.mem_finRange
adjacency source :=
(edges.filter fun edge => decide (edge.source = source)).map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:69
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
Uses 9 · Used by 3
StructureReachable negative cycle witness#✓fully proved
For a list of weighted edges on the vertices \(\{0, \dots, n-1\}\) and a source vertex \(s\), a reachable negative cycle consists of a base vertex \(b\), a weighted path \(p\) from \(s\) to \(b\) using edges of the list whose vertices along \(p\) from \(s\) are pairwise distinct, and a nonempty weighted path \(c\) from \(b\) to \(b\) using edges of the list whose edges have pairwise distinct sources and whose weight is negative.
Cslib.Algorithms.Lean.BellmanFord.ReachableNegativeCycle · 19 lines
public structure ReachableNegativeCycle {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- The distinguished cycle vertex reached by the prefix. -/
base : Fin n
/-- A source-to-base path. -/
«prefix» : List (Edge n)
/-- A nonempty closed path based at `base`. -/
cycle : List (Edge n)
/-- The prefix uses input edges and has the declared endpoints. -/
prefix_valid : IsWeightedPath edges source base «prefix»
/-- The prefix visits no vertex twice. -/
prefix_simple : (pathVertices source «prefix»).Nodup
/-- The cycle uses input edges and closes at `base`. -/
cycle_valid : IsWeightedPath edges base base cycle
/-- The cycle has at least one edge. -/
cycle_nonempty : cycle ≠ []
/-- The edge sources around the cycle are pairwise distinct. -/
cycle_simple : (cycle.map Edge.source).Nodup
/-- The cycle has negative total weight. -/
cycle_negative : pathWeight cycle < 0public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
base : Fin nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:244
@[expose] public def pathVertices {n : Nat}
(source : Fin n) (path : List (Edge n)) : List (Fin n) :=
source :: path.map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:78
cycle : List (Edge n)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:248
source : Fin nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:61
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
Uses 4 · Used by 22
DefinitionExistence of a reachable negative cycle#✓fully proved
Let \(E\) be a list of weighted directed edges on the vertices \(0, \dots, n-1\) and \(s\) a vertex. Then \(E\) has a negative cycle reachable from \(s\) when there is a reachable negative cycle witness for \(E\) and \(s\): a base vertex \(b\), a weighted path in \(E\) from \(s\) to \(b\) that visits no vertex twice, and a nonempty weighted path in \(E\) from \(b\) to \(b\) whose edge sources are pairwise distinct and whose total weight is negative.
@[expose] public def HasReachableNegativeCycle {n : Nat}
(edges : List (Edge n)) (source : Fin n) : Prop :=
Nonempty (ReachableNegativeCycle edges source)public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure ReachableNegativeCycle {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- The distinguished cycle vertex reached by the prefix. -/
base : Fin n
/-- A source-to-base path. -/
«prefix» : List (Edge n)
/-- A nonempty closed path based at `base`. -/
cycle : List (Edge n)
/-- The prefix uses input edges and has the declared endpoints. -/
prefix_valid : IsWeightedPath edges source base «prefix»
/-- The prefix visits no vertex twice. -/
prefix_simple : (pathVertices source «prefix»).Nodup
/-- The cycle uses input edges and closes at `base`. -/
⋯CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:242
StructureBellman-Ford distance table#✓fully proved
For a graph on the vertices \(0, \dots, n-1\), the output of a successful Bellman-Ford run consists of a source vertex \(s\), for every vertex a distance that is either an integer or \(\infty\), and for every vertex an optional predecessor edge (a weighted directed edge, or none).
The structure only records these values; that they are shortest-path data is proved separately.
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) npublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
Uses 1 · Used by 46
DefinitionBellman-Ford path reconstruction#✓fully proved
Let the output of a Bellman-Ford run on \(n\) vertices have source \(s\). The path to a vertex \(t\) is built backwards from \(t\): at a vertex \(v \ne s\), take the recorded predecessor edge \(e\) of \(v\), put it in front of the edges collected so far, and continue from the source of \(e\). When \(s\) is reached within at most \(n\) such steps, the result is the collected list of edges (empty if \(t = s\)). If some vertex on the way has no predecessor edge, or \(s\) is not reached within \(n\) steps, there is no result.
public def Distances.pathTo? {n : Nat} (result : Distances n) (target : Fin n) :
Option (List (Edge n)) := by
let rec follow (current : Fin n) : Nat → List (Edge n) → Option (List (Edge n))
| 0, suffix => if current = result.source then some suffix else none
| fuel + 1, suffix =>
if current = result.source then
some suffix
else
match result.predecessor.get current with
| none => none
| some edge => follow edge.source fuel (edge :: suffix)
exact follow target n []public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
Uses 2 · Used by 6
StructureBellman-Ford cost counters#✓fully proved
The cost of a Bellman-Ford run is a pair of natural numbers: the number of edge occurrences checked by relaxation passes, and the number of predecessor edges read or emitted while reconstructing a negative-cycle witness.
public structure Cost where
/-- Edge occurrences checked by relaxation passes. -/
relaxationChecks : Nat
/-- Predecessor edges read or emitted while reconstructing a failure witness. -/
cycleWitnessSteps : Nat
deriving DecidableEqUsed by 22
DefinitionTotal Bellman–Ford cost#✓fully proved
The total of a Bellman–Ford cost record is its number of edge relaxation checks plus its number of negative-cycle witness reconstruction steps.
@[expose] public def Cost.total (cost : Cost) : Nat :=
cost.relaxationChecks + cost.cycleWitnessStepspublic structure Cost where
/-- Edge occurrences checked by relaxation passes. -/
relaxationChecks : Nat
/-- Predecessor edges read or emitted while reconstructing a failure witness. -/
cycleWitnessSteps : Nat
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:291
Uses 1 · Used by 6
InductiveBellman–Ford result#✓fully proved
For a list of weighted edges on the vertices \(\{0, \dots, n-1\}\) and a source vertex \(s\), a Bellman–Ford result is either a distance record (a source vertex, an optional integer distance for each vertex and an optional predecessor edge for each vertex) or a reachable negative cycle witness for the list and \(s\).
The type itself does not require the distances to be correct.
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public structure ReachableNegativeCycle {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- The distinguished cycle vertex reached by the prefix. -/
base : Fin n
/-- A source-to-base path. -/
«prefix» : List (Edge n)
/-- A nonempty closed path based at `base`. -/
cycle : List (Edge n)
/-- The prefix uses input edges and has the declared endpoints. -/
prefix_valid : IsWeightedPath edges source base «prefix»
/-- The prefix visits no vertex twice. -/
prefix_simple : (pathVertices source «prefix»).Nodup
/-- The cycle uses input edges and closes at `base`. -/
⋯CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:242
Uses 3 · Used by 21
DefinitionBellman–Ford algorithm#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. Bellman–Ford run on \(E\) from \(s\) starts with distance \(d(s) = 0\) and \(d(v) = \infty\) for every other vertex \(v\), and makes \(n - 1\) passes over \(E\) followed by one final pass. A pass goes through the edges of \(E\) in list order, charging one relaxation check per edge occurrence; an edge from \(u\) to \(v\) of weight \(w\) with \(d(u)\) finite sets \(d(v)\) to \(d(u) + w\) and records the edge as the predecessor edge of \(v\) when \(d(v) = \infty\) or \(d(u) + w < d(v)\). If the final pass changes no distance, the result is the distances and predecessor edges. Otherwise, starting from the vertex whose distance the final pass changed last, the algorithm follows \(n\) predecessor edges back to a vertex \(b\); it then collects the cycle of predecessor edges through \(b\), following at most \(n\) predecessor edges back from \(b\) until it reaches an edge with source \(b\), and collects a path from \(s\) to \(b\) of at most \(n - 1\) edges by following back from \(b\) the edges by which vertices first received a finite distance. Each lookup of a recorded edge in these three steps is charged as one witness step, also when no edge is recorded. If all three steps succeed and give a reachable negative cycle witness for \(E\) and \(s\), that witness is the result; otherwise the result is the distances and predecessor edges.
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourcepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Cost where
/-- Edge occurrences checked by relaxation passes. -/
relaxationChecks : Nat
/-- Predecessor edges read or emitted while reconstructing a failure witness. -/
cycleWitnessSteps : Nat
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:291
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) := do
let state ← runPasses edges (n - 1) (initialState source)
let state ← relaxEdges edges { state with lastUpdated := none }
finish edges source stateCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Extraction.lean:954
Uses 8 · Used by 20
TheoremBellman-Ford succeeds exactly when no negative cycle is reachable#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. Bellman-Ford run on \(E\) from \(s\) returns distances if and only if there is no negative cycle reachable from \(s\), that is, no simple path from \(s\) to a vertex \(b\) together with a nonempty cycle through \(b\) along edges of \(E\) whose edge sources are pairwise distinct and whose total weight is negative.
public theorem bellmanFord_returns_distances_iff {n : Nat} (edges : List (Edge n))
(source : Fin n) :
(∃ result, (bellmanFord edges source).ret = Result.distances result) ↔
¬HasReachableNegativeCycle edges sourcepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def HasReachableNegativeCycle {n : Nat}
(edges : List (Edge n)) (source : Fin n) : Prop :=
Nonempty (ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:263
Uses 10 · Used by 1
TheoremBellman-Ford reports a negative cycle exactly when one is reachable#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. Bellman-Ford run on \(E\) from \(s\) returns a reachable negative cycle witness if and only if a negative cycle is reachable from \(s\), that is, there are a simple path from \(s\) to a vertex \(b\) and a nonempty cycle through \(b\) along edges of \(E\) whose edge sources are pairwise distinct and whose total weight is negative.
public theorem bellmanFord_returns_negativeCycle_iff {n : Nat} (edges : List (Edge n))
(source : Fin n) :
(∃ witness, (bellmanFord edges source).ret = Result.negativeCycle witness) ↔
HasReachableNegativeCycle edges sourcepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def HasReachableNegativeCycle {n : Nat}
(edges : List (Edge n)) (source : Fin n) : Prop :=
Nonempty (ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:263
TheoremBellman-Ford distances are realized by walks#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. If Bellman-Ford run on \(E\) from \(s\) returns distances \(d\) and the distance \(d(t)\) of a vertex \(t\) is a finite integer \(\delta\), then there is a walk from \(s\) to \(t\) along edges of \(E\) whose total weight is \(\delta\).
public theorem bellmanFord_distance_realized {n : Nat} {edges : List (Edge n)}
{source target : Fin n}
{result : Distances n} {distance : Int}
(hRun : (bellmanFord edges source).ret = Result.distances result)
(hDistance : result.distance.get target = some distance) :
∃ path, IsWeightedPath edges source target path ∧ pathWeight path = distancepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
Uses 9 · Used by 1
TheoremBellman-Ford distances are lower bounds on walk weights#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. If Bellman-Ford run on \(E\) from \(s\) returns distances \(d\), the distance \(d(t)\) of a vertex \(t\) is a finite integer \(\delta\), and \(P\) is a walk from \(s\) to \(t\) along edges of \(E\) (vertices may repeat), then \(\delta\) is at most the total weight of \(P\).
public theorem bellmanFord_distance_minimal {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {result : Distances n} {distance : Int}
{path : List (Edge n)}
(hRun : (bellmanFord edges source).ret = Result.distances result)
(hDistance : result.distance.get target = some distance)
(hPath : IsWeightedPath edges source target path) :
distance ≤ pathWeight pathpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
Uses 9 · Used by 1
TheoremBellman-Ford leaves exactly the unreachable vertices at infinite distance#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. If Bellman-Ford run on \(E\) from \(s\) returns distances \(d\), with \(\infty\) marking a vertex that has no finite distance, then for every vertex \(t\), \(d(t) = \infty\) if and only if \(t\) is not reachable from \(s\) in the directed graph obtained from \(E\) by forgetting the weights.
public theorem bellmanFord_distance_eq_none_iff {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {result : Distances n}
(hRun : (bellmanFord edges source).ret = Result.distances result) :
result.distance.get target = none ↔
¬(toDirectedAdjacency edges).Reachable source targetpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def toDirectedAdjacency {n : Nat}
(edges : List (Edge n)) : DirectedAdjacency (Fin n) where
vertices := List.finRange n
vertices_nodup := List.nodup_finRange n
vertices_complete := List.mem_finRange
adjacency source :=
(edges.filter fun edge => decide (edge.source = source)).map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:69
Uses 12 · Used by 1
TheoremBellman-Ford predecessor edges are tight#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. Suppose Bellman-Ford run on \(E\) from \(s\) returns distances \(d\) together with predecessor edges, and the predecessor edge of a vertex \(t\) is an edge \(e\) from \(u\) to \(v\) of weight \(w\). Then \(e\) belongs to \(E\), \(v = t\), and \(d(u)\) and \(d(t)\) are both finite with \(d(t) = d(u) + w\).
public theorem bellmanFord_predecessor_spec {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {result : Distances n} {edge : Edge n}
(hRun : (bellmanFord edges source).ret = Result.distances result)
(hPredecessor : result.predecessor.get target = some edge) :
edge ∈ edges ∧ edge.target = target ∧
∃ sourceDistance targetDistance,
result.distance.get edge.source = some sourceDistance ∧
result.distance.get target = some targetDistance ∧
targetDistance = sourceDistance + edge.weightpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
TheoremBellman-Ford gives the source no predecessor#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. If Bellman-Ford run on \(E\) from \(s\) returns distances together with predecessor edges, then \(s\) has no predecessor edge.
public theorem bellmanFord_source_predecessor_eq_none {n : Nat} {edges : List (Edge n)}
{source : Fin n} {result : Distances n}
(hRun : (bellmanFord edges source).ret = Result.distances result) :
result.predecessor.get source = nonepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
TheoremBellman-Ford path reconstruction fails exactly at infinite distances#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. If Bellman-Ford run on \(E\) from \(s\) returns distances \(d\), with \(\infty\) marking a vertex that has no finite distance, together with predecessor edges, then for every vertex \(t\), reconstructing a path to \(t\) (following predecessor edges back from \(t\) for at most \(n\) steps until \(s\) is reached) fails if and only if \(d(t) = \infty\).
public theorem bellmanFord_pathTo?_eq_none_iff {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {result : Distances n}
(hRun : (bellmanFord edges source).ret = Result.distances result) :
result.pathTo? target = none ↔ result.distance.get target = nonepublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
Uses 10
TheoremBellman-Ford reconstructed paths are simple and realize the distances#✓fully proved
Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and let \(s\) be a vertex. Suppose Bellman-Ford run on \(E\) from \(s\) returns distances \(d\) together with predecessor edges, and that reconstructing a path to a vertex \(t\) (following predecessor edges back from \(t\) for at most \(n\) steps until \(s\) is reached) yields the edge sequence \(P\). Then \(P\) is a walk from \(s\) to \(t\) along edges of \(E\), \(d(t)\) is finite and equals the total weight of \(P\), the vertex \(s\) and the targets of the edges of \(P\) are pairwise distinct, and \(P\) has fewer than \(n\) edges.
public theorem bellmanFord_pathTo?_spec {n : Nat} {edges : List (Edge n)}
{source target : Fin n} {result : Distances n} {path : List (Edge n)}
(hRun : (bellmanFord edges source).ret = Result.distances result)
(hPath : result.pathTo? target = some path) :
IsWeightedPath edges source target path ∧
result.distance.get target = some (pathWeight path) ∧
(pathVertices source path).Nodup ∧ path.length < npublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
@[expose] public def pathVertices {n : Nat}
(source : Fin n) (path : List (Edge n)) : List (Fin n) :=
source :: path.map Edge.targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:78
Uses 10
TheoremPredecessor paths realize the distances under a decreasing rank#✓fully proved
Let \(R\) be a distances record on \(n\) vertices with source \(s\), distance table \(d\) (each \(d(v)\) is an integer or infinite) and predecessor table \(p\); let \(E\) be a list of weighted edges; and let \(r\) assign to each vertex \(v\) a natural number \(r(v) < n\). Suppose that \(d(s) = 0\), that every vertex \(v\) with \(d(v)\) infinite has no predecessor, that every vertex \(v \ne s\) with \(d(v)\) finite has a predecessor, and that whenever \(p(v) = e\), the edge \(e\) occurs in \(E\), ends at \(v\), and its start \(u\) has \(d(u)\) finite, \(d(v) = d(u) + w(e)\) where \(w(e)\) is the weight of \(e\), and \(r(u) < r(v)\). Then for every vertex \(t\), following predecessors from \(t\) back to \(s\) for at most \(n\) edges fails exactly when \(d(t)\) is infinite; and whenever it returns a path \(P\) and \(d(t)\) is finite, \(P\) is a path from \(s\) to \(t\) made of edges of \(E\), its total weight is \(d(t)\), and it has fewer than \(n\) edges.
Cslib.Algorithms.Lean.BellmanFord.Distances.pathTo?_spec_of_rank · 18 lines
public theorem Distances.pathTo?_spec_of_rank {n : Nat} (result : Distances n)
(edges : List (Edge n)) (rank : Fin n → Nat)
(rank_bound : ∀ vertex, rank vertex < n)
(source_zero : result.distance.get result.source = some 0)
(infinite_predecessor : ∀ vertex, result.distance.get vertex = none →
result.predecessor.get vertex = none)
(finite_predecessor : ∀ vertex distance, result.distance.get vertex = some distance →
vertex ≠ result.source → ∃ edge, result.predecessor.get vertex = some edge)
(predecessor_step : ∀ vertex edge, result.predecessor.get vertex = some edge →
edge ∈ edges ∧ edge.target = vertex ∧ ∃ sourceDistance,
result.distance.get edge.source = some sourceDistance ∧
result.distance.get vertex = some (sourceDistance + edge.weight) ∧
rank edge.source < rank vertex) :
∀ target, (result.pathTo? target = none ↔ result.distance.get target = none) ∧
∀ path distance, result.pathTo? target = some path →
result.distance.get target = some distance →
IsWeightedPath edges result.source target path ∧
pathWeight path = distance ∧ path.length < npublic structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
@[expose] public def IsWeightedPath {n : Nat} (edges : List (Edge n)) (source target : Fin n)
(path : List (Edge n)) : Prop :=
(∀ edge ∈ path, edge ∈ edges) ∧
path.IsChain (fun left right => left.target = right.source) ∧
match path with
| [] => source = target
| first :: rest =>
first.source = source ∧ (first :: rest).getLast?.map Edge.target = some targetCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:87
@[expose] public def pathWeight {n : Nat} (path : List (Edge n)) : Int :=
(path.map Edge.weight).sumCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:83
Uses 5 · Used by 2
TheoremRelaxation checks of Bellman-Ford pass by pass#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), Bellman-Ford run on \(E\) from \(s\) charges exactly \((n - 1) \cdot |E| + |E|\) relaxation checks, where \(|E|\) is the length of \(E\).
The two terms count one check per edge occurrence in each of the \(n - 1\) ordinary passes and in the final pass.
public theorem bellmanFord_relaxationChecks {n : Nat} (edges : List (Edge n)) (source : Fin n) :
(bellmanFord edges source).time.relaxationChecks =
(n - 1) * edges.length + edges.lengthpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
Uses 9 · Used by 1
TheoremBellman-Ford makes exactly \(n \cdot |E|\) relaxation checks#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), Bellman-Ford run on \(E\) from \(s\) charges exactly \(n \cdot |E|\) relaxation checks, where \(|E|\) is the length of \(E\) counting repeated edges.
public theorem bellmanFord_relaxationChecks_eq_mul {n : Nat} (edges : List (Edge n))
(source : Fin n) :
(bellmanFord edges source).time.relaxationChecks = n * edges.lengthpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
Uses 5 · Used by 3
TheoremBellman-Ford spends at most \(3n\) witness steps#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), Bellman-Ford run on \(E\) from \(s\) charges at most \(3n\) negative-cycle witness reconstruction steps.
public theorem bellmanFord_cycleWitnessSteps_le {n : Nat} (edges : List (Edge n))
(source : Fin n) :
(bellmanFord edges source).time.cycleWitnessSteps ≤ 3 * npublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
Uses 9 · Used by 2
TheoremBellman-Ford spends no witness steps when it returns distances#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), if Bellman-Ford run on \(E\) from \(s\) returns distances rather than a negative cycle, then the run charges zero negative-cycle witness reconstruction steps.
public theorem bellmanFord_cycleWitnessSteps_eq_zero {n : Nat} (edges : List (Edge n))
(source : Fin n) (result : Distances n)
(hRun : (bellmanFord edges source).ret = Result.distances result) :
(bellmanFord edges source).time.cycleWitnessSteps = 0public structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure Distances (n : Nat) where
/-- The source used for the run. -/
source : Fin n
/-- Finite shortest weights, with `none` denoting infinity. -/
distance : Vector (Option Int) n
/-- The final predecessor edge for every vertex. -/
predecessor : Vector (Option (Edge n)) nCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:268
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
Uses 9 · Used by 2
TheoremWitness cost of a returned negative cycle#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), if Bellman-Ford run on \(E\) from \(s\) returns a reachable negative cycle whose cycle has \(c\) edges and whose path from \(s\) to the cycle has \(q\) edges, then the run charges exactly \(n + c + q\) negative-cycle witness reconstruction steps.
public theorem bellmanFord_cycleWitnessSteps_eq {n : Nat} (edges : List (Edge n))
(source : Fin n) (witness : ReachableNegativeCycle edges source)
(hRun : (bellmanFord edges source).ret = Result.negativeCycle witness) :
(bellmanFord edges source).time.cycleWitnessSteps =
n + witness.cycle.length + witness.prefix.lengthpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public structure ReachableNegativeCycle {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- The distinguished cycle vertex reached by the prefix. -/
base : Fin n
/-- A source-to-base path. -/
«prefix» : List (Edge n)
/-- A nonempty closed path based at `base`. -/
cycle : List (Edge n)
/-- The prefix uses input edges and has the declared endpoints. -/
prefix_valid : IsWeightedPath edges source base «prefix»
/-- The prefix visits no vertex twice. -/
prefix_simple : (pathVertices source «prefix»).Nodup
/-- The cycle uses input edges and closes at `base`. -/
⋯CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:242
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
public inductive Result {n : Nat} (edges : List (Edge n)) (source : Fin n) where
/-- Exact shortest distances and predecessor edges. -/
| distances (result : Distances n)
/-- A concrete reachable negative cycle. -/
| negativeCycle (witness : ReachableNegativeCycle edges source)CSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:329
TheoremBellman-Ford makes at most \(4 n |E|\) counted steps#✓fully proved
For every list \(E\) of weighted edges on \(n\) vertices and every source \(s\), the total cost of Bellman-Ford run on \(E\) from \(s\) (its relaxation checks plus its negative-cycle witness reconstruction steps) is at most \(4 \cdot n \cdot |E|\), where \(|E|\) is the length of \(E\).
public theorem bellmanFord_total_le {n : Nat} (edges : List (Edge n)) (source : Fin n) :
(bellmanFord edges source).time.total ≤ 4 * n * edges.lengthpublic structure Edge (n : Nat) where
/-- The source vertex. -/
source : Fin n
/-- The target vertex. -/
target : Fin n
/-- The integer edge weight. -/
weight : Int
deriving DecidableEqCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Basic.lean:59
public def bellmanFord {n : Nat} (edges : List (Edge n)) (source : Fin n) :
TimeM Cost (Result edges source) :=
Internal.bellmanFord edges sourceCSLibExt/Algorithms/Lean/Graph/ShortestPath/BellmanFord/Correctness.lean:964
Uses 12
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.