CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 22. Single-Source Shortest Paths
22.5. Proofs of Shortest Paths

Imports

import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

22.5. Proofs of Shortest Paths

This section formalizes the theoretical properties of single-source shortest paths that CLRS proves in §22.5, building on the walk and relaxation model of Section 22.1. For a graph with no negative-weight cycle, the single-source distance δ(s, v) is the exact shortest-path weight; the Bellman-Ford relaxation computes it after |V| - 1 rounds (CLRS.Chapter24.WeightedGraph.relaxDist_isShortestDist, Theorem 22.4).

We introduce shortestDist as the distance function δ, and prove the CLRS §22.5 backbone:

No-path property (Lemma 22.13): δ(s, v) = ⊤ iff no walk reaches v from s.
Upper-bound property (Lemma 22.12): δ(s, v) lower-bounds the weight of every walk from s to v.
Triangle inequality (Lemma 22.11): for every edge (u, v), δ(s, v) ≤ δ(s, u) + w(u, v).

Main results

Theorem shortestDist_isShortestDist: δ(s, v) is characterized as a lower bound on all walk weights that is either ⊤ or attained
Theorem noPath_iff_top (Lemma 22.13)
Theorem shortestDist_le_walkWeight (Lemma 22.12)
Theorem IsWalkFrom.append_edge: appending a vertex along an edge extends a walk
Theorem shortestDist_triangleInequality (Lemma 22.11)
Theorem shortestDist_triangle_walk: the triangle inequality iterated along a walk
Theorem subpath_isShortest (Lemma 22.10): a prefix of a shortest walk is shortest
Theorem shortestDist_convergence (Lemma 22.14): relaxing a shortest path's final edge converges the endpoint estimate
Theorem relaxDist_eq_of_shortest_walk (Lemma 22.15): after enough rounds a shortest walk is fully relaxed
Theorem predecessor_tight: the independently selected predecessor edge is tight. Tightness alone does not prove a source-rooted tree; zero-weight cycles can admit cyclic tight selections.

The Dijkstra-correctness reformulation (Theorem 22.17) is not restated here; Dijkstra correctness is already proved in Section 22.3.

              namespace CLRSnamespace Chapter24namespace WeightedGraphvariable {V : Type*} [Fintype V] [DecidableEq V] (G : WeightedGraph V)

The single-source shortest-path distance

The single-source shortest-path distance δ(s, v), defined via the Bellman-Ford relaxation after |V| - 1 rounds. With no negative-weight cycle this is the exact minimum weight of any walk from s to v (Theorem 22.4).

def shortestDist (s v : V) : WithTop ℝ :=
  G.relaxDist s (Fintype.card V - 1) v

With no negative-weight cycle, δ(s, v) is a valid shortest distance: it lower-bounds every walk weight and is either ⊤ or attained.

theorem shortestDist_isShortestDist (hNC : G.NoNegCycle) (s v : V) :
    G.IsShortestDist s v (G.shortestDist s v) := by
  unfold shortestDist
  exact G.relaxDist_isShortestDist hNC s v

Upper-bound property (Lemma 22.12): the shortest distance δ(s, v) lower-bounds the weight of every walk from s to v.

theorem shortestDist_le_walkWeight (hNC : G.NoNegCycle) (s v : V) (p : List V)
    (hp : G.IsWalkFrom s v p) :
    G.shortestDist s v ≤ (walkWeight G.w p : WithTop ℝ) :=
  (G.shortestDist_isShortestDist hNC s v).1 p hp

No-path property (Lemma 22.13): δ(s, v) = ⊤ iff there is no walk from s to v.

Try `simp at htop_le` instead of `simpa using htop_le`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem noPath_iff_top (hNC : G.NoNegCycle) (s v : V) :
    G.shortestDist s v = (⊤ : WithTop ℝ) ↔ ¬ ∃ p : List V, G.IsWalkFrom s v p := by
  constructor
  · intro htop hp
    rcases hp with ⟨p, hp⟩
    have hle : G.shortestDist s v ≤ (walkWeight G.w p : WithTop ℝ) :=
      (G.shortestDist_isShortestDist hNC s v).1 p hp
    rw [htop] at hle
    exact absurd hle (by
      intro htop_le
      -- ⊤ ≤ a real-typed WithTop value is impossible
      Try `simp at htop_le` instead of `simpa using htop_le`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [WithTop.top_le_iff] using htop_le)
  · intro hnp
    by_cases h : G.shortestDist s v = (⊤ : WithTop ℝ)
    · exact h
    · have hattained := (G.shortestDist_isShortestDist hNC s v).2
      rcases hattained with htop | ⟨p, hp, _⟩
      · exact False.elim (h htop)
      · exact False.elim (hnp ⟨p, hp⟩)

Triangle inequality (Lemma 22.11)

Appending the vertex v to a walk that ends at u along an edge (u, v) yields a walk to v.

theorem IsWalkFrom.append_edge {s u v : V} {p : List V} (hp : G.IsWalkFrom s u p)
    (huv : (u, v) ∈ G.edges) :
    G.IsWalkFrom s v (p ++ [v]) := by
  refine ⟨?_, ?_, ?_⟩
  · refine List.IsChain.append hp.chain (by simp) ?_
    intro x hx y hy
    simp [hp.last] at hx
    simp at hy
    subst x
    subst y
    simpa [WeightedGraph.Adj] using huv
  · have hpne : p ≠ [] := hp.ne_nil
    simpa [List.head?_append_of_ne_nil p hpne] using hp.head
  · have hpne : p ≠ [] := hp.ne_nil
    simp [List.getLast?_append_of_ne_nil p]

Triangle inequality (Lemma 22.11): for every edge (u, v), δ(s, v) ≤ δ(s, u) + w(u, v).


theorem shortestDist_triangleInequality (hNC : G.NoNegCycle) (s u v : V)
    (huv : (u, v) ∈ G.edges) :
    G.shortestDist s v ≤ G.shortestDist s u + (G.w u v : WithTop ℝ) := by
  have hsu := G.shortestDist_isShortestDist hNC s u
  have hsv := G.shortestDist_isShortestDist hNC s v
  by_cases htop : G.shortestDist s u = (⊤ : WithTop ℝ)
  · -- δ(s,u) = ⊤ : RHS is ⊤
    rw [htop]
    exact le_top
  · rcases hsu.2 with htop' | ⟨p, hp, hpw⟩
    · exact False.elim (htop htop')
    · -- p is an s→u walk of weight δ(s,u); append the edge (u,v)
      have hpv : G.IsWalkFrom s v (p ++ [v]) := IsWalkFrom.append_edge G hp huv
      have hw : (walkWeight G.w (p ++ [v]) : WithTop ℝ) =
          (walkWeight G.w p : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
        have hpne : p ≠ [] := hp.ne_nil
        have hlast : p.getLast hpne = u := by
          -- p is an s→u walk, so p.getLast? = some u
          simpa [List.getLast?_eq_some_getLast hpne] using hp.last
        rw [walkWeight_append_singleton G.w p hpne v, hlast]
        simp
      have hle := hsv.1 (p ++ [v]) hpv
      rw [hw, hpw] at hle
      exact hle

Triangle inequality along a walk

Triangle inequality along a walk. If q is a walk from u to v, then the shortest distance δ(s, v) is at most δ(s, u) plus the weight of q (the CLRS triangle inequality, Lemma 22.11, iterated along the walk).


theorem shortestDist_triangle_walk (hNC : G.NoNegCycle) (s : V) {u v : V} {q : List V}
    (hq : G.IsWalkFrom u v q) :
    G.shortestDist s v ≤ G.shortestDist s u + (walkWeight G.w q : WithTop ℝ) := by
  induction q generalizing u v with
  | nil => exact False.elim (by simpa using hq.head)
  | cons a t ih =>
      have ha : a = u := by simpa using hq.head
      subst ha
      cases t with
      | nil =>
          have hv : a = v := by simpa using hq.last
          subst hv
          simp
      | cons b t' =>
          have hchain := List.isChain_cons_cons.mp hq.chain
          have hedge : (a, b) ∈ G.edges := by simpa [WeightedGraph.Adj] using hchain.1
          have htail : G.IsWalkFrom b v (b :: t') := by
            refine ⟨hchain.2, ?_, ?_⟩
            · rfl
            · simpa using hq.last
          have htri : G.shortestDist s b ≤ G.shortestDist s a + (G.w a b : WithTop ℝ) :=
            G.shortestDist_triangleInequality hNC s a b hedge
          calc
            G.shortestDist s v ≤ G.shortestDist s b + (walkWeight G.w (b :: t') : WithTop ℝ) := ih htail
            _ ≤ (G.shortestDist s a + (G.w a b : WithTop ℝ)) + (walkWeight G.w (b :: t') : WithTop ℝ) := by
                gcongr
            _ = G.shortestDist s a + ((G.w a b : WithTop ℝ) + (walkWeight G.w (b :: t') : WithTop ℝ)) := by
                rw [add_assoc]
            _ = G.shortestDist s a + (walkWeight G.w (a :: b :: t') : WithTop ℝ) := rfl

Subpath property (Lemma 22.10)

Subpath property (Lemma 22.10). If a shortest walk from s to v decomposes as l₁ ++ [u] ++ l₂ with l₁ ++ [u] a walk from s to u and u :: l₂ a walk from u to v, then the prefix l₁ ++ [u] is a shortest walk from s to u.


theorem subpath_isShortest (hNC : G.NoNegCycle) {s u v : V} {l₁ l₂ : List V}
    (hprefix : G.IsWalkFrom s u (l₁ ++ [u]))
    (hsuffix : G.IsWalkFrom u v (u :: l₂))
    (hshort : (walkWeight G.w (l₁ ++ u :: l₂) : WithTop ℝ) = G.shortestDist s v) :
    (walkWeight G.w (l₁ ++ [u]) : WithTop ℝ) = G.shortestDist s u := by
  have hsplit : walkWeight G.w (l₁ ++ u :: l₂) =
      walkWeight G.w (l₁ ++ [u]) + walkWeight G.w (u :: l₂) :=
    walkWeight_split G.w l₁ u l₂
  have hdecomp : G.shortestDist s v =
      (walkWeight G.w (l₁ ++ [u]) : WithTop ℝ) + (walkWeight G.w (u :: l₂) : WithTop ℝ) := by
    rw [← hshort, hsplit]
    push_cast
    rfl
  have hlb : G.shortestDist s u ≤ (walkWeight G.w (l₁ ++ [u]) : WithTop ℝ) :=
    G.shortestDist_le_walkWeight hNC s u (l₁ ++ [u]) hprefix
  have htri : G.shortestDist s v ≤ G.shortestDist s u + (walkWeight G.w (u :: l₂) : WithTop ℝ) :=
    G.shortestDist_triangle_walk hNC s hsuffix
  have hcombined : (walkWeight G.w (l₁ ++ [u]) : WithTop ℝ) + (walkWeight G.w (u :: l₂) : WithTop ℝ)
      ≤ G.shortestDist s u + (walkWeight G.w (u :: l₂) : WithTop ℝ) := by
    rw [← hdecomp]
    exact htri
  have hcancel := (WithTop.add_le_add_iff_right
    (WithTop.coe_ne_top : (walkWeight G.w (u :: l₂) : WithTop ℝ) ≠ ⊤)).mp hcombined
  exact le_antisymm hcancel hlb

Convergence and path relaxation (Lemmas 22.14-22.15)

Nonincreasing rounds. Bellman-Ford estimates never increase as the round count grows.

theorem relaxDist_antitone (s v : V) : Antitone (fun k : ℕ => G.relaxDist s k v) := by
  refine antitone_nat_of_succ_le ?_
  intro k
  exact G.relaxDist_succ_le s k v

Convergence property (Lemma 22.14). If the estimate at u has converged to δ(s, u) after k rounds and (u, v) is the final edge of a shortest path (δ(s, v) = δ(s, u) + w(u, v)), then one more relaxation round brings the estimate at v to δ(s, v).


theorem shortestDist_convergence {s u v : V} (huv : (u, v) ∈ G.edges)
    {k : ℕ} (hk : k + 1 ≤ Fintype.card V - 1)
    (hconv : G.relaxDist s k u = G.shortestDist s u)
    (hshort : G.shortestDist s v = G.shortestDist s u + (G.w u v : WithTop ℝ)) :
    G.relaxDist s (k + 1) v = G.shortestDist s v := by
  apply le_antisymm
  · rw [relaxDist_succ_apply]
    calc G.relaxStep (G.relaxDist s k) v
        ≤ G.relaxDist s k u + (G.w u v : WithTop ℝ) := G.relaxStep_le_pred huv
      _ = G.shortestDist s v := by rw [hconv, hshort]
  · simpa [WeightedGraph.shortestDist] using G.relaxDist_antitone s v hk

Path-relaxation property (Lemma 22.15). If p is a shortest walk from s to v with at most |V| vertices, then after p.length - 1 relaxation rounds the estimate at v equals the walk weight.


theorem relaxDist_eq_of_shortest_walk (s v : V) (p : List V)
    (hp : G.IsWalkFrom s v p)
    (hshort : (walkWeight G.w p : WithTop ℝ) = G.shortestDist s v)
    (hlen : p.length ≤ Fintype.card V) :
    G.relaxDist s (p.length - 1) v = (walkWeight G.w p : WithTop ℝ) := by
  apply le_antisymm
  · refine G.relaxDist_le_walkWeight s (p.length - 1) v p hp ?_
    have hpne : p ≠ [] := hp.ne_nil
    have hpos : 0 < p.length := List.length_pos_iff.mpr hpne
    omega
  · rw [hshort]
    have hpne : p ≠ [] := hp.ne_nil
    have hpos : 0 < p.length := List.length_pos_iff.mpr hpne
    have hk : p.length - 1 ≤ Fintype.card V - 1 := by omega
    simpa [WeightedGraph.shortestDist] using G.relaxDist_antitone s v hk

Predecessor subgraph (Lemma 22.16)

The vertex u in the predecessor set of v that minimizes δ(s, u) + w(u, v). This independent minimizer has no depth-decrease or acyclicity guarantee. If v has no incoming edge the value is v (a junk value).

noncomputable def predecessor (s v : V) : V :=
  if h : (G.preds v).Nonempty then
    Classical.choose (Finset.exists_mem_eq_inf (G.preds v) h
      (fun u => G.shortestDist s u + (G.w u v : WithTop ℝ)))
  else v

A reachable non-source vertex has an incoming edge, so its predecessor set is nonempty.


theorem preds_nonempty_of_walk (s v : V) (hv : v ≠ s) (hreach : ∃ p : List V, G.IsWalkFrom s v p) :
    (G.preds v).Nonempty := by
  rcases hreach with ⟨p, hp⟩
  have hpne : p ≠ [] := hp.ne_nil
  have hlast : p.getLast hpne = v := by
    have := hp.last
    rw [List.getLast?_eq_some_getLast hpne] at this
    exact Option.some.inj this
  have hsplit : p = p.dropLast ++ [v] := by
    conv_lhs => rw [← List.dropLast_append_getLast hpne]
    rw [hlast]
  have hdl_ne : p.dropLast ≠ [] := by
    intro hcontra
    have hlen1 : p.length = 1 := by rw [hsplit, hcontra]; simp
    rcases p with _ | ⟨x, t⟩
    · exact hpne rfl
    · have ht : t = [] := by
        have : (x :: t).length = 1 := hlen1
        simpa using this
      subst ht
      have hxs : x = s := by simpa using hp.head
      have hxv : x = v := by simpa using hp.last
      exact hv (hxv.symm.trans hxs)
  have hu : ∃ u : V, p.dropLast.getLast? = some u := by
    rw [List.getLast?_eq_some_getLast hdl_ne]
    exact ⟨_, rfl⟩
  rcases hu with ⟨u, hu⟩
  have hchain : List.IsChain G.Adj (p.dropLast ++ [v]) := by rw [← hsplit]; exact hp.chain
  have happ := List.isChain_append.1 hchain
  have hedge : G.Adj u v := happ.2.2 u (Option.mem_def.mpr hu) v (Option.mem_def.mpr (by simp))
  refine ⟨u, ?_⟩
  simpa [WeightedGraph.preds, WeightedGraph.Adj] using hedge

Bellman equation (incoming-edge form). For a reachable non-source vertex v, the shortest distance is the minimum over incoming edges (u, v) of δ(s, u) + w(u, v).


theorem shortestDist_eq_inf_preds (hNC : G.NoNegCycle) (s v : V) (hv : v ≠ s)
    (hreach : ∃ p : List V, G.IsWalkFrom s v p) :
    G.shortestDist s v = (G.preds v).inf (fun u => G.shortestDist s u + (G.w u v : WithTop ℝ)) := by
  apply le_antisymm
  · apply Finset.le_inf
    intro u hu
    have hedge : (u, v) ∈ G.edges := by simpa [WeightedGraph.preds] using hu
    exact G.shortestDist_triangleInequality hNC s u v hedge
  · rcases (G.shortestDist_isShortestDist hNC s v).2 with htop | ⟨p, hp, hpw⟩
    · exact False.elim ((G.noPath_iff_top hNC s v).mp htop hreach)
    · have hpne : p ≠ [] := hp.ne_nil
      have hlast : p.getLast hpne = v := by
        have := hp.last
        rw [List.getLast?_eq_some_getLast hpne] at this
        exact Option.some.inj this
      have hsplit : p = p.dropLast ++ [v] := by
        conv_lhs => rw [← List.dropLast_append_getLast hpne]
        rw [hlast]
      have hdl_ne : p.dropLast ≠ [] := by
        intro hcontra
        have hlen1 : p.length = 1 := by rw [hsplit, hcontra]; simp
        rcases p with _ | ⟨x, t⟩
        · exact hpne rfl
        · have ht : t = [] := by
            have : (x :: t).length = 1 := hlen1
            simpa using this
          subst ht
          have hxs : x = s := by simpa using hp.head
          have hxv : x = v := by simpa using hp.last
          exact hv (hxv.symm.trans hxs)
      have hu : ∃ u : V, p.dropLast.getLast? = some u := by
        rw [List.getLast?_eq_some_getLast hdl_ne]
        exact ⟨_, rfl⟩
      rcases hu with ⟨u, hu⟩
      have hchain : List.IsChain G.Adj (p.dropLast ++ [v]) := by rw [← hsplit]; exact hp.chain
      have happ := List.isChain_append.1 hchain
      have hedge : G.Adj u v := happ.2.2 u (Option.mem_def.mpr hu) v (Option.mem_def.mpr (by simp))
      have hu_pred : u ∈ G.preds v := by simpa [WeightedGraph.preds, WeightedGraph.Adj] using hedge
      have hprefix_head : (p.dropLast).head? = some s := by
        have hph := hp.head
        rw [hsplit, List.head?_append_of_ne_nil _ hdl_ne] at hph
        exact hph
      have hprefix_walk : G.IsWalkFrom s u (p.dropLast) := ⟨happ.1, hprefix_head, hu⟩
      have hlb_u : G.shortestDist s u ≤ (walkWeight G.w (p.dropLast) : WithTop ℝ) :=
        (G.shortestDist_isShortestDist hNC s u).1 (p.dropLast) hprefix_walk
      have hgl : p.dropLast.getLast hdl_ne = u := by
        have := List.getLast?_eq_some_getLast hdl_ne
        rw [hu] at this
        exact (Option.some.inj this).symm
      have hweight : walkWeight G.w p = walkWeight G.w (p.dropLast) + G.w u v := by
        conv_lhs => rw [hsplit]
        rw [walkWeight_append_singleton G.w (p.dropLast) hdl_ne v, hgl]
      calc
        (G.preds v).inf (fun x => G.shortestDist s x + (G.w x v : WithTop ℝ))
            ≤ G.shortestDist s u + (G.w u v : WithTop ℝ) := Finset.inf_le hu_pred
        _ ≤ (walkWeight G.w (p.dropLast) : WithTop ℝ) + (G.w u v : WithTop ℝ) := by gcongr
        _ = (walkWeight G.w p : WithTop ℝ) := by rw [hweight]; push_cast; rfl
        _ = G.shortestDist s v := hpw

The chosen predecessor is a genuine incoming neighbor of v.


theorem predecessor_isPredecessor (s v : V) (hv : v ≠ s) (hreach : ∃ p : List V, G.IsWalkFrom s v p) :
    G.predecessor s v ∈ G.preds v := by
  have hne : (G.preds v).Nonempty := G.preds_nonempty_of_walk s v hv hreach
  unfold predecessor
  rw [dif_pos hne]
  exact (Classical.choose_spec (Finset.exists_mem_eq_inf (G.preds v) hne
    (fun u => G.shortestDist s u + (G.w u v : WithTop ℝ)))).1

The chosen predecessor minimizes δ(s, ·) + w(·, v) over the incoming neighbors of v.


theorem predecessor_inf_eq (s v : V) (hv : v ≠ s) (hreach : ∃ p : List V, G.IsWalkFrom s v p) :
    (G.preds v).inf (fun u => G.shortestDist s u + (G.w u v : WithTop ℝ)) =
      G.shortestDist s (G.predecessor s v) + (G.w (G.predecessor s v) v : WithTop ℝ) := by
  have hne : (G.preds v).Nonempty := G.preds_nonempty_of_walk s v hv hreach
  unfold predecessor
  rw [dif_pos hne]
  exact (Classical.choose_spec (Finset.exists_mem_eq_inf (G.preds v) hne
    (fun u => G.shortestDist s u + (G.w u v : WithTop ℝ)))).2

Predecessor-subgraph property (Lemma 22.16). The predecessor edge is tight: for a reachable non-source vertex v, δ(s, v) = δ(s, π(v)) + w(π(v), v). This edge equation alone does not ensure source reachability or acyclicity of the selected parent relation.


theorem predecessor_tight (hNC : G.NoNegCycle) (s v : V) (hv : v ≠ s)
    (hreach : ∃ p : List V, G.IsWalkFrom s v p) :
    G.shortestDist s v = G.shortestDist s (G.predecessor s v) +
        (G.w (G.predecessor s v) v : WithTop ℝ) := by
  rw [G.shortestDist_eq_inf_preds hNC s v hv hreach]
  exact G.predecessor_inf_eq s v hv hreach

              end WeightedGraphend Chapter24end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_22.Section_22_5_Shortest_Path_Properties.PredecessorTree

Constructed shortest-path predecessor trees

The constructor computes Bellman–Ford distances, retains edges tight for those values, and runs the existing labelled BFS on that finite graph. It returns the computed distances and the actual BFS parent/depth maps. No predecessor certificate is supplied as input. First-discovery depth prevents cycles even when the tight graph contains zero-weight directed cycles.

Under the same global absence-of-negative-cycles premise as Bellman–Ford, shortest-walk prefix optimality proves that the tight graph spans exactly the original reachable vertices. Every returned parent path uses original edges and telescopes to the computed shortest distance. Source and unreachable vertices have no parent; all other reachable vertices do.

This is a finite classical graph construction over real-valued distances, using the existing noncomputable BFS representation. It adds no machine-runtime claim or negative-cycle detector, and does not alter the older tight-only predecessor selector.

namespace CLRS.Chapter24.WeightedGraphvariable {V : Type} [Fintype V] [DecidableEq V] (G : WeightedGraph V)

Keep precisely original edges tight for the computed Bellman–Ford values.

noncomputable def tightGraph (s : V) : CLRS.Chapter22.Graph V := by
  classical
  exact {
    vertices := Finset.univ
    adj := fun u => Finset.univ.filter (fun v => G.Adj u v ∧
      G.shortestDist s v = G.shortestDist s u + (G.w u v : WithTop ℝ))
    adj_sub := by intros; exact Finset.subset_univ _
    adj_outside := by intro v hv; simp at hv
  }

The auxiliary graph retains every original carrier vertex.

@[simp] theorem tightGraph_vertices (s : V) : (G.tightGraph s).vertices = Finset.univ := rfl

Auxiliary adjacency is exactly an original tight edge.

@[simp] theorem tightGraph_adj (s u v : V) : (G.tightGraph s).Adj u v ↔
    G.Adj u v ∧ G.shortestDist s v = G.shortestDist s u + (G.w u v : WithTop ℝ) := by
  classical
  simp [tightGraph, CLRS.Chapter22.Graph.Adj]

              private theorem singleton_walk (s : V) : G.IsWalkFrom s s [s] :=
  ⟨by simp, rfl, rfl⟩private theorem tight_reachable_has_walk {s v : V} (h : (G.tightGraph s).Reachable s v) :
    ∃ p, G.IsWalkFrom s v p := by
  induction h with
  | refl => exact ⟨[s], singleton_walk G s⟩
  | @tail u v h huv ih =>
    obtain ⟨p, hp⟩ := ih
    exact ⟨p ++ [v], IsWalkFrom.append_edge G hp ((G.tightGraph_adj s u v).mp huv).1⟩

private theorem shortest_walk_tight_reachable (hNC : G.NoNegCycle) (s : V) (p : List V) :
    ∀ v, G.IsWalkFrom s v p → (walkWeight G.w p : WithTop ℝ) = G.shortestDist s v →
      (G.tightGraph s).Reachable s v := by
  induction p using List.reverseRecOn with
  | nil => intro v hp; exact (IsWalkFrom.ne_nil G hp rfl).elim
  | append_singleton p x ih =>
    intro v hp hw
    have hx : x = v := by simpa using hp.last
    subst v
    by_cases hn : p = []
    · subst p
      have hs : x = s := by simpa using hp.head
      subst x
      exact .refl
    · let u := p.getLast hn
      have hlast : p.getLast? = some u := List.getLast?_eq_some_getLast hn
      have happ := List.isChain_append.mp hp.chain
      have hedge : G.Adj u x :=
        happ.2.2 u (Option.mem_def.mpr hlast) x (by simp)
      have hhead : p.head? = some s := by
        simpa only [List.head?_append_of_ne_nil _ hn] using hp.head
      have hprefix : G.IsWalkFrom s u p := ⟨happ.1, hhead, hlast⟩
      have hweight : walkWeight G.w (p ++ [x]) = walkWeight G.w p + G.w u x :=
        walkWeight_append_singleton G.w p hn x
      have hlower := G.shortestDist_le_walkWeight hNC s u p hprefix
      have htri := G.shortestDist_triangleInequality hNC s u x hedge
      have hprefix_short : (walkWeight G.w p : WithTop ℝ) = G.shortestDist s u := by
        apply le_antisymm
        · apply (WithTop.add_le_add_iff_right (WithTop.coe_ne_top : (G.w u x : WithTop ℝ) ≠ ⊤)).mp
          rw [← hw, hweight] at htri
          simpa only [WithTop.coe_add] using htri
        · exact hlower
      have htight : G.shortestDist s x = G.shortestDist s u + (G.w u x : WithTop ℝ) := by
        rw [← hw, hweight, ← hprefix_short, WithTop.coe_add]
      exact (G.tightGraph s).reachable_trans (ih u hprefix hprefix_short)
        ((G.tightGraph s).reachable_adj ((G.tightGraph_adj s u x).mpr ⟨hedge, htight⟩))

The tight graph reaches exactly the vertices reachable in the weighted graph.

theorem tightGraph_reachable_iff (hNC : G.NoNegCycle) (s v : V) :
    (G.tightGraph s).Reachable s v ↔ ∃ p, G.IsWalkFrom s v p := by
  constructor
  · exact tight_reachable_has_walk G
  · intro hr
    obtain htop | ⟨p, hp, hw⟩ := (G.shortestDist_isShortestDist hNC s v).2
    · exact ((G.noPath_iff_top hNC s v).mp htop hr).elim
    · exact shortest_walk_tight_reachable G hNC s p v hp hw

Distances and parent/depth maps returned by the constructed predecessor tree.

structure ShortestPathTreeResult (V : Type) where
  distance : V → WithTop ℝ
  parent : V → Option V
  depth : V → Option Nat

Run labelled BFS on the tight graph of actual computed shortest-path distances.

noncomputable def shortestPathTree (s : V) : ShortestPathTreeResult V :=
  let labels := (G.tightGraph s).bfsState s (by simp)
  ⟨G.shortestDist s, labels.parent, labels.distance⟩

The returned weighted distances are the computed Bellman–Ford values.

@[simp] theorem shortestPathTree_distance (s v : V) :
    (G.shortestPathTree s).distance v = G.shortestDist s v := rfl

The returned source has no predecessor.

@[simp] theorem shortestPathTree_source_parent (s : V) :
    (G.shortestPathTree s).parent s = none :=
  (G.tightGraph s).bfsState_source_parent (by simp)

The returned source has depth zero.

@[simp] theorem shortestPathTree_source_depth (s : V) :
    (G.shortestPathTree s).depth s = some 0 :=
  ((G.tightGraph s).bfsState_distanceInvariant (by simp)).source_distance

Every returned parent is an original tight edge and decreases depth by one.


theorem shortestPathTree_parent_step (s : V) {u v : V}
    (hp : (G.shortestPathTree s).parent v = some u) :
    G.Adj u v ∧ G.shortestDist s v = G.shortestDist s u + (G.w u v : WithTop ℝ) ∧
    ∃ d, (G.shortestPathTree s).depth u = some d ∧
      (G.shortestPathTree s).depth v = some (d + 1) := by
  obtain ⟨he, d, hu, hv⟩ := (G.tightGraph s).bfsState_parent_spec (by simp) hp
  obtain ⟨he, ht⟩ := (G.tightGraph_adj s u v).mp he
  exact ⟨he, ht, d, hu, hv⟩

Following a parent strictly decreases its natural-number depth.

theorem shortestPathTree_parent_depth_lt (s : V) {u v : V}
    (hp : (G.shortestPathTree s).parent v = some u) :
    ((G.shortestPathTree s).depth u).getD 0 < ((G.shortestPathTree s).depth v).getD 0 :=
  (G.tightGraph s).bfsState_parent_level_lt (by simp) hp

The actual returned predecessor relation has no directed cycle.

theorem shortestPathTree_acyclic (s v : V) :
    ¬ Relation.TransGen (fun u w => (G.shortestPathTree s).parent w = some u) v v :=
  (G.tightGraph s).bfsState_parent_acyclic (by simp) v

Exactly reachable non-source vertices receive a predecessor.

theorem shortestPathTree_parent_defined_iff (hNC : G.NoNegCycle) (s v : V) :
    (∃ u, (G.shortestPathTree s).parent v = some u) ↔
      (∃ p, G.IsWalkFrom s v p) ∧ v ≠ s := by
  simpa only [shortestPathTree, G.tightGraph_reachable_iff hNC] using
    (G.tightGraph s).bfsState_parent_defined_iff (s := s) (v := v) (by simp)

Exactly reachable vertices receive a depth.

theorem shortestPathTree_depth_defined_iff (hNC : G.NoNegCycle) (s v : V) :
    (∃ d, (G.shortestPathTree s).depth v = some d) ↔ ∃ p, G.IsWalkFrom s v p := by
  simpa only [shortestPathTree, G.tightGraph_reachable_iff hNC] using
    (G.tightGraph s).bfsState_distance_defined_iff_reachable (s := s) (v := v) (by simp)

An unreachable vertex has neither a predecessor nor a depth.

theorem shortestPathTree_unreachable (hNC : G.NoNegCycle) (s v : V)
    (hn : ¬ ∃ p, G.IsWalkFrom s v p) :
    (G.shortestPathTree s).parent v = none ∧ (G.shortestPathTree s).depth v = none := by
  constructor
  · cases hp : (G.shortestPathTree s).parent v with
    | none => rfl
    | some u => exact (hn ((G.shortestPathTree_parent_defined_iff hNC s v).mp ⟨u, hp⟩).1).elim
  · cases hd : (G.shortestPathTree s).depth v with
    | none => rfl
    | some d => exact (hn ((G.shortestPathTree_depth_defined_iff hNC s v).mp ⟨d, hd⟩)).elim



private theorem shortestDist_source (hNC : G.NoNegCycle) (s : V) : G.shortestDist s s = 0 := by
  have hle : G.shortestDist s s ≤ 0 := by
    simpa using G.shortestDist_le_walkWeight hNC s s [s] (singleton_walk G s)
  obtain ht | ⟨p, hp, hw⟩ := (G.shortestDist_isShortestDist hNC s s).2
  · rw [ht] at hle
    simp at hle
  · apply le_antisymm hle
    rw [← hw]
    exact_mod_cast hNC s p hp



private theorem parentPath_weight (hNC : G.NoNegCycle) (s : V) {v d}
    (hpath : CLRS.Chapter22.Graph.BFSParentPath (G.shortestPathTree s).parent s v d) :
    ∃ p, G.IsWalkFrom s v p ∧ p.length = d + 1 ∧
      List.IsChain (fun u w => (G.shortestPathTree s).parent w = some u) p ∧
      (walkWeight G.w p : WithTop ℝ) = G.shortestDist s v := by
  induction hpath with
  | root =>
    refine ⟨[s], singleton_walk G s, rfl, by simp, ?_⟩
    simpa using (shortestDist_source G hNC s).symm
  | @tail u v n hpath hp ih =>
    obtain ⟨p, hw, hlen, hchain, hweight⟩ := ih
    obtain ⟨hedge, htight, _⟩ := G.shortestPathTree_parent_step s hp
    refine ⟨p ++ [v], IsWalkFrom.append_edge G hw hedge, ?_, ?_, ?_⟩
    · simp [hlen]
    · apply List.isChain_append.mpr
      refine ⟨hchain, by simp, ?_⟩
      intro a ha b hb
      have hau : a = u := by
        have hh : p.getLast? = some a := Option.mem_def.mp ha
        exact Option.some.inj (hh.symm.trans hw.last)
      have hb' : b = v := by simpa using (Option.mem_def.mp hb).symm
      simpa [hau, hb'] using hp
    · have hn := IsWalkFrom.ne_nil G hw
      have hlast : p.getLast hn = u := by
        simpa only [List.getLast?_eq_some_getLast hn, Option.some.injEq] using hw.last
      rw [walkWeight_append_singleton G.w p hn v, hlast, WithTop.coe_add, hweight]
      exact htight.symm

Actual returned parent pointers recover a source walk of the computed shortest weight.

theorem shortestPathTree_path (hNC : G.NoNegCycle) (s : V) {v d}
    (hd : (G.shortestPathTree s).depth v = some d) :
    ∃ p, G.IsWalkFrom s v p ∧ p.length = d + 1 ∧
      List.IsChain (fun u w => (G.shortestPathTree s).parent w = some u) p ∧
      (walkWeight G.w p : WithTop ℝ) = (G.shortestPathTree s).distance v :=
  parentPath_weight G hNC s ((G.tightGraph s).bfsState_parentPath (by simp) hd)

Only the source has depth zero.


theorem shortestPathTree_depth_zero_iff (s v : V) :
    (G.shortestPathTree s).depth v = some 0 ↔ v = s := by
  constructor
  · intro hd
    have hr := (G.tightGraph s).bfsState_distance_reachableIn (by simp) hd
    cases hr
    rfl
  · rintro rfl
    exact G.shortestPathTree_source_depth _

A tight direct source edge receives the source as its BFS predecessor.


theorem shortestPathTree_parent_of_tight_source_edge (s v : V) (hv : v ≠ s)
    (he : G.Adj s v) (ht : G.shortestDist s v = G.shortestDist s s + (G.w s v : WithTop ℝ)) :
    (G.shortestPathTree s).parent v = some s := by
  have he' : (G.tightGraph s).Adj s v := (G.tightGraph_adj s s v).mpr ⟨he, ht⟩
  have hd : (G.shortestPathTree s).depth v = some 1 := by
    apply (G.tightGraph s).bfsState_distance_eq_some_iff (by simp) |>.mpr
    refine ⟨.tail .refl he', ?_⟩
    intro n hn
    cases n with
    | zero => cases hn; exact (hv rfl).elim
    | succ n => omega
  have hpExists := (G.tightGraph s).bfsState_parent_defined_iff (s := s) (v := v) (by simp)
  obtain ⟨u, hu⟩ := hpExists.mpr ⟨(G.tightGraph s).reachable_adj he', hv⟩
  obtain ⟨_, _, d, hdu, hdv⟩ := G.shortestPathTree_parent_step s hu
  rw [hd] at hdv
  have hd0 : d = 0 := by injection hdv with hh; omega
  rw [hd0] at hdu
  have hus := (G.shortestPathTree_depth_zero_iff s u).mp hdu
  simpa [shortestPathTree, hus] using hu

A source-rooted acyclic predecessor tree realizing shortest weighted paths.

structure IsShortestPathPredecessorTree (s : V) (result : ShortestPathTreeResult V) : Prop where
  distance_correct : ∀ v, G.IsShortestDist s v (result.distance v)
  root_parent : result.parent s = none
  root_depth : result.depth s = some 0
  parent_defined_iff : ∀ v, (∃ u, result.parent v = some u) ↔
    (∃ p, G.IsWalkFrom s v p) ∧ v ≠ s
  depth_defined_iff : ∀ v, (∃ d, result.depth v = some d) ↔ ∃ p, G.IsWalkFrom s v p
  parent_step : ∀ u v, result.parent v = some u →
    G.Adj u v ∧ result.distance v = result.distance u + (G.w u v : WithTop ℝ) ∧
    ∃ d, result.depth u = some d ∧ result.depth v = some (d + 1)
  path : ∀ v d, result.depth v = some d →
    ∃ p, G.IsWalkFrom s v p ∧ p.length = d + 1 ∧
      List.IsChain (fun u w => result.parent w = some u) p ∧
      (walkWeight G.w p : WithTop ℝ) = result.distance v
  acyclic : ∀ v, ¬ Relation.TransGen (fun u w => result.parent w = some u) v v

The constructed result satisfies the full weighted predecessor-tree contract.

theorem shortestPathTree_correct (hNC : G.NoNegCycle) (s : V) :
    G.IsShortestPathPredecessorTree s (G.shortestPathTree s) := by
  exact {
    distance_correct := G.shortestDist_isShortestDist hNC s
    root_parent := G.shortestPathTree_source_parent s
    root_depth := G.shortestPathTree_source_depth s
    parent_defined_iff := G.shortestPathTree_parent_defined_iff hNC s
    depth_defined_iff := G.shortestPathTree_depth_defined_iff hNC s
    parent_step := fun u v h => G.shortestPathTree_parent_step s h
    path := fun v d h => G.shortestPathTree_path hNC s h
    acyclic := G.shortestPathTree_acyclic s
  }

end CLRS.Chapter24.WeightedGraph