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

Chapter 22 — Single-Source Shortest Paths

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib

22.1. The Bellman-Ford Algorithm

This section opens Chapter 22 (single-source shortest paths). It defines a finite weighted directed graph, walks and their weights, the single-source shortest-path distance δ(s, ·), and the Bellman-Ford relaxation dynamic program. It then proves that the relaxation values are exact shortest-path distances after |V| - 1 rounds when the graph has no negative-weight cycle anywhere in the graph. This is a valid-input distance interface, not a source-relative negative-cycle detector with failure return. A negative cycle unreachable from the chosen source still violates the stated NoNegCycle premise. The separate O(V·E) formula is an abstract round/edge budget, not a cached-table execution counter.

Main results:

CLRS.Chapter24.WeightedGraph: a finite weighted directed graph as an edge Finset plus a real weight function.
CLRS.Chapter24.WeightedGraph.relaxDist: the Bellman-Ford relaxation after k synchronous rounds, valued in WithTop ℝ (⊤ = unreachable).
CLRS.Chapter24.WeightedGraph.relaxDist_le_walkWeight: relaxation is a lower bound for the weight of every walk with at most k edges (the upper-bound property).
CLRS.Chapter24.WeightedGraph.exists_walk_of_relaxDist: every finite relaxation value is attained by an actual walk (realizability).
CLRS.Chapter24.WeightedGraph.exists_simple_le: with no negative-weight cycle, any walk shortens to a simple path of no larger weight (cycle removal).
CLRS.Chapter24.WeightedGraph.relaxDist_isShortestDist: CLRS Theorem 22.4 — with no negative-weight cycle, relaxDist (|V|-1) is the single-source shortest-path distance, characterized by IsShortestDist.
CLRS.Chapter24.WeightedGraph.bellmanFordWork_le: the (|V|-1)·|E| work bound (O(V·E)).

Notation conventions used in this section:

G : a WeightedGraph
s : the source vertex
w u v : the weight of edge (u, v)
relaxDist k v : shortest-path estimate at v after k rounds
⊤ : +∞, i.e. no walk found yet

The recurrence is synchronous: every next-round estimate reads the preceding round's values. It is a mathematical evaluation of that recurrence, not an instrumented in-place edge loop or a proof of cache reuse. The valid-input shortest-distance theorem is independent of those operational refinements.

              namespace CLRSnamespace Chapter24open Finset

A finite weighted directed graph: a finite set of directed edges together with a real-valued weight function. Only the weights of actual edges are used; w is total for convenience (junk values off the edge set are never read).

The directed edges of the graph.

The weight of a directed edge (u, v).

              structure WeightedGraph (V : Type*) [Fintype V] [DecidableEq V] where  edges : Finset (V × V)  w : V → V → ℝ

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

Directed adjacency: there is an edge from u to v.

def Adj (u v : V) : Prop := (u, v) ∈ G.edges

instance : DecidableRel G.Adj := fun u v => by
  unfold WeightedGraph.Adj; infer_instance

The predecessors of v: all u with an edge u → v.

def preds (v : V) : Finset V := Finset.univ.filter (fun u => (u, v) ∈ G.edges)

@[simp] theorem mem_preds {u v : V} : u ∈ G.preds v ↔ (u, v) ∈ G.edges := by
  simp [preds]

Walks and their weights

sectionomit [Fintype V] [DecidableEq V]

The weight of a vertex list, i.e. the sum of the edge weights of consecutive pairs. A single vertex or the empty list has weight 0.

def walkWeight (w : V → V → ℝ) : List V → ℝ
  | [] => 0
  | [_] => 0
  | a :: b :: t => w a b + walkWeight w (b :: t)

@[simp] theorem walkWeight_singleton (w : V → V → ℝ) (a : V) :
    walkWeight w [a] = 0 := rfl

@[simp] theorem walkWeight_cons_cons (w : V → V → ℝ) (a b : V) (t : List V) :
    walkWeight w (a :: b :: t) = w a b + walkWeight w (b :: t) := rfl

Weight of a walk that ends with the edge (u, v): peel off the last edge.


theorem walkWeight_concat (w : V → V → ℝ) (q : List V) (u v : V) :
    walkWeight w (q ++ [u, v]) = walkWeight w (q ++ [u]) + w u v := by
  induction q with
  | nil => simp
  | cons x xs ih =>
    cases xs with
    | nil => simp
    | cons y ys =>
      simp only [List.cons_append] at ih ⊢
      rw [walkWeight_cons_cons, walkWeight_cons_cons, ih]
      ring

end

p is a walk from s to v in G: a chain of edges whose head is s and whose last vertex is v.

Consecutive vertices are joined by edges.

The walk starts at the source s.

The walk ends at v.

              structure IsWalkFrom (s v : V) (p : List V) : Prop where  chain : List.IsChain G.Adj p  head : p.head? = some s  last : p.getLast? = some v

theorem IsWalkFrom.ne_nil {s v : V} {p : List V} (h : G.IsWalkFrom s v p) : p ≠ [] := by
  rintro rfl
  simpa using h.head

The Bellman-Ford relaxation dynamic program

One synchronous relaxation round: relax every incoming edge of every vertex. relaxStep d v = min (d v) (min over predecessors u of (d u + w u v)).

def relaxStep (d : V → WithTop ℝ) : V → WithTop ℝ :=
  fun v => min (d v) ((G.preds v).inf (fun u => d u + (G.w u v : WithTop ℝ)))

Bellman-Ford after k rounds from source s. Round 0 places 0 at the source and ⊤ elsewhere; each further round applies relaxStep.

def relaxDist (G : WeightedGraph V) (s : V) : ℕ → V → WithTop ℝ
  | 0 => fun v => if v = s then (0 : WithTop ℝ) else ⊤
  | (k + 1) => G.relaxStep (G.relaxDist s k)

              @[simp] theorem relaxDist_zero_eq (s : V) :
    G.relaxDist s 0 = fun v => if v = s then (0 : WithTop ℝ) else ⊤ := rfl@[simp] theorem relaxDist_succ_eq (s : V) (k : ℕ) :
    G.relaxDist s (k + 1) = G.relaxStep (G.relaxDist s k) := rfl

theorem relaxDist_zero_apply (s v : V) :
    G.relaxDist s 0 v = if v = s then (0 : WithTop ℝ) else ⊤ := by
  rw [relaxDist_zero_eq]

theorem relaxDist_succ_apply (s : V) (k : ℕ) (v : V) :
    G.relaxDist s (k + 1) v = G.relaxStep (G.relaxDist s k) v := by
  rw [relaxDist_succ_eq]

theorem relaxDist_zero_self (s : V) : G.relaxDist s 0 s = 0 := by
  rw [relaxDist_zero_apply]; simp

One relaxation round never increases an estimate (the upper-bound property is monotone).

theorem relaxStep_le_self (d : V → WithTop ℝ) (v : V) : G.relaxStep d v ≤ d v := by
  simp only [relaxStep]; exact min_le_left _ _

One relaxation round respects every edge: relaxStep d v ≤ d u + w u v.

theorem relaxStep_le_pred {d : V → WithTop ℝ} {u v : V} (h : (u, v) ∈ G.edges) :
    G.relaxStep d v ≤ d u + (G.w u v : WithTop ℝ) := by
  simp only [relaxStep]
  exact le_trans (min_le_right _ _) (Finset.inf_le (by simpa [mem_preds] using h))

Bellman-Ford estimates are monotone nonincreasing in the round count.


theorem relaxDist_succ_le (s : V) (k : ℕ) (v : V) :
    G.relaxDist s (k + 1) v ≤ G.relaxDist s k v := by
  rw [relaxDist_succ_apply]; exact G.relaxStep_le_self (G.relaxDist s k) v

Upper-bound property. After k rounds the estimate at v is at most the weight of any walk from s to v using at most k edges.

Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
theorem relaxDist_le_walkWeight (s : V) :
    ∀ (k : ℕ) (v : V) (p : List V), G.IsWalkFrom s v p → p.length ≤ k + 1 →
      G.relaxDist s k v ≤ (walkWeight G.w p : WithTop ℝ) := by
  intro k
  induction k with
  | zero =>
    intro v p hp hlen
    have hne := hp.ne_nil
    obtain ⟨x, rfl⟩ : ∃ x, p = [x] := by
      rcases p with _ | ⟨a, _ | ⟨b, tl⟩⟩
      · exact absurd rfl hne
      · exact ⟨a, rfl⟩
      · simp only [List.length_cons] at hlen; omega
    have hxs : x = s := by simpa using hp.head
    have hxv : x = v := by simpa using hp.last
    subst hxs; subst hxv
    simp [relaxDist_zero_apply]
  | succ k ih =>
    intro v p hp hlen
    by_cases hshort : p.length ≤ k + 1
    · exact le_trans (G.relaxDist_succ_le s k v) (ih v p hp hshort)
    · have hlong : k + 1 < p.length := not_le.mp hshort
      have hne : p ≠ [] := hp.ne_nil
      have hlast : p.getLast hne = v := by
        have := hp.last
        rw [List.getLast?_eq_some_getLast hne] at this
        exact Option.some.inj this
      have hsplit : p = p.dropLast ++ [v] := by
        conv_lhs => rw [← List.dropLast_append_getLast hne]
        rw [hlast]
      have hdl_ne : p.dropLast ≠ [] := by
        intro hcontra
        have : p.length ≤ 1 := by rw [hsplit, hcontra]; simp
        omega
      set q := p.dropLast with hq
      obtain ⟨u, hu⟩ : ∃ u, q.getLast? = some u := by
        rw [List.getLast?_eq_some_getLast hdl_ne]; exact ⟨_, rfl⟩
      have hchain : List.IsChain G.Adj (q ++ [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 hqhead : q.head? = some s := by
        have hph := hp.head
        rw [hsplit, List.head?_append_of_ne_nil _ hdl_ne] at hph
        exact hph
      have hqchain : List.IsChain G.Adj q := happ.1
      have hqwalk : G.IsWalkFrom s u q := ⟨hqchain, hqhead, hu⟩
      have hqlen : q.length ≤ k + 1 := by
        have hpq : p.length = q.length + 1 := by rw [hsplit]; simp
        omega
      -- reconstruct p = q.dropLast ++ [u, v]
      have hgl : q.getLast hdl_ne = u := by
        have := List.getLast?_eq_some_getLast hdl_ne
        rw [hu] at this
        exact (Option.some.inj this).symm
      have hq_split : q = q.dropLast ++ [u] := by
        conv_lhs => rw [← List.dropLast_append_getLast hdl_ne]
        rw [hgl]
      have hp_uv : p = q.dropLast ++ [u, v] := by
        rw [hsplit]
        conv_lhs => rw [hq_split]
        simp
      have hweight : walkWeight G.w p = walkWeight G.w q + G.w u v := by
        rw [hp_uv, walkWeight_concat, ← hq_split]
      have hIH : G.relaxDist s k u ≤ (walkWeight G.w q : WithTop ℝ) := ih u q hqwalk hqlen
      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 hedge
        _ ≤ (walkWeight G.w q : WithTop ℝ) + (G.w u v : WithTop ℝ) := by gcongr
        _ = (walkWeight G.w p : WithTop ℝ) := by rw [hweight]; push_cast; Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring

Weight of a nonempty walk extended by one vertex v.

omit [Fintype V] [DecidableEq V] in


theorem walkWeight_append_singleton (w : V → V → ℝ) (q : List V) (hq : q ≠ []) (v : V) :
    walkWeight w (q ++ [v]) = walkWeight w q + w (q.getLast hq) v := by
  have h1 : q ++ [v] = q.dropLast ++ [q.getLast hq, v] := by
    rw [show ([q.getLast hq, v] : List V) = [q.getLast hq] ++ [v] from rfl, ← List.append_assoc,
      List.dropLast_append_getLast hq]
  rw [h1, walkWeight_concat, List.dropLast_append_getLast hq]

Realizability. Every finite relaxation value after k rounds is the weight of an actual walk from s using at most k edges.


theorem exists_walk_of_relaxDist (s : V) :
    ∀ (k : ℕ) (v : V), G.relaxDist s k v = ⊤ ∨
      ∃ p, G.IsWalkFrom s v p ∧ p.length ≤ k + 1 ∧
        (walkWeight G.w p : WithTop ℝ) = G.relaxDist s k v := by
  intro k
  induction k with
  | zero =>
    intro v
    by_cases hv : v = s
    · subst hv
      right
      exact ⟨[v], ⟨List.isChain_singleton v, by simp, by simp⟩, by simp,
        by simp [relaxDist_zero_apply]⟩
    · left
      rw [relaxDist_zero_apply]; simp [hv]
  | succ k ih =>
    intro v
    have hstep : G.relaxDist s (k + 1) v =
        min (G.relaxDist s k v)
          ((G.preds v).inf (fun u => G.relaxDist s k u + (G.w u v : WithTop ℝ))) := by
      rw [relaxDist_succ_apply]; rfl
    rcases min_choice (G.relaxDist s k v)
        ((G.preds v).inf (fun u => G.relaxDist s k u + (G.w u v : WithTop ℝ))) with hmin | hmin
    · rw [hstep, hmin]
      rcases ih v with htop | ⟨p, hp, hplen, hpw⟩
      · left; exact htop
      · right; exact ⟨p, hp, by omega, hpw⟩
    · rw [hstep, hmin]
      by_cases hBtop :
          (G.preds v).inf (fun u => G.relaxDist s k u + (G.w u v : WithTop ℝ)) = ⊤
      · left; exact hBtop
      · right
        have hne : (G.preds v).Nonempty := by
          rcases (G.preds v).eq_empty_or_nonempty with he | hne
          · rw [he] at hBtop; simp at hBtop
          · exact hne
        obtain ⟨u, hu_mem, hu_eq⟩ := Finset.exists_mem_eq_inf (G.preds v) hne
          (fun u => G.relaxDist s k u + (G.w u v : WithTop ℝ))
        have hedge : (u, v) ∈ G.edges := by simpa [mem_preds] using hu_mem
        have hutop : G.relaxDist s k u ≠ ⊤ := by
          intro h
          apply hBtop
          rw [hu_eq, h, WithTop.top_add]
        rcases ih u with htop | ⟨q, hq, hqlen, hqw⟩
        · exact absurd htop hutop
        · have hqne : q ≠ [] := hq.ne_nil
          have hgl : q.getLast hqne = u := by
            have := List.getLast?_eq_some_getLast hqne
            rw [hq.last] at this
            exact (Option.some.inj this).symm
          refine ⟨q ++ [v], ?_, ?_, ?_⟩
          · refine ⟨?_, ?_, ?_⟩
            · refine List.IsChain.append hq.chain (List.isChain_singleton v) ?_
              intro x hx y hy
              have hxu : x = u := by
                rw [Option.mem_def, hq.last] at hx
                exact (Option.some.inj hx).symm
              have hyv : y = v := Eq.symm (by simpa using hy)
              subst hxu; subst hyv
              exact hedge
            · rw [List.head?_append_of_ne_nil _ hqne]; exact hq.head
            · simp
          · simp only [List.length_append, List.length_cons, List.length_nil]
            omega
          · rw [hu_eq, walkWeight_append_singleton G.w q hqne v, hgl]
            push_cast
            rw [hqw]

No negative cycles and cycle removal

G has no negative-weight cycle: every closed walk has nonnegative weight. This is CLRS's hypothesis under which shortest paths (and Bellman-Ford) are well defined; a negative closed walk would contain a negative cycle.

def NoNegCycle : Prop := ∀ (x : V) (c : List V), G.IsWalkFrom x x c → 0 ≤ walkWeight G.w c

Weight of a walk splits at any interior vertex x.

omit [Fintype V] [DecidableEq V] in


theorem walkWeight_split (w : V → V → ℝ) (l₁ : List V) (x : V) (l₂ : List V) :
    walkWeight w (l₁ ++ x :: l₂) = walkWeight w (l₁ ++ [x]) + walkWeight w (x :: l₂) := by
  induction l₁ with
  | nil => simp
  | cons a rest ih =>
    cases rest with
    | nil => simp
    | cons b rest' =>
      simp only [List.cons_append] at ih ⊢
      rw [walkWeight_cons_cons, walkWeight_cons_cons, ih]
      ring

A list that is not Nodup has a vertex appearing twice, exposing the enclosed cycle.

omit [Fintype V] in


theorem exists_dup_decomp : ∀ {l : List V}, ¬ l.Nodup →
    ∃ (a : V) (l₁ l₂ l₃ : List V), l = l₁ ++ a :: l₂ ++ a :: l₃ := by
  intro l
  induction l with
  | nil => intro h; simp at h
  | cons b t ih =>
    intro h
    by_cases hb : b ∈ t
    · obtain ⟨l₂, l₃, ht⟩ := List.mem_iff_append.mp hb
      exact ⟨b, [], l₂, l₃, by rw [ht]; simp⟩
    · have hnt : ¬ t.Nodup := fun htn => h (List.nodup_cons.mpr ⟨hb, htn⟩)
      obtain ⟨a, l₁, l₂, l₃, ht⟩ := ih hnt
      exact ⟨a, b :: l₁, l₂, l₃, by rw [ht]; simp⟩

Cycle removal. With no negative cycle, every walk from s to v can be shortened to a simple (repetition-free) path of no larger weight.


theorem exists_simple_le (hNC : G.NoNegCycle) (s v : V) :
    ∀ (n : ℕ) (p : List V), p.length ≤ n → G.IsWalkFrom s v p →
      ∃ q, G.IsWalkFrom s v q ∧ q.Nodup ∧ walkWeight G.w q ≤ walkWeight G.w p := by
  intro n
  induction n with
  | zero =>
    intro p hlen hp
    exact absurd (List.length_eq_zero_iff.mp (Nat.le_zero.mp hlen)) hp.ne_nil
  | succ n ih =>
    intro p hlen hp
    by_cases hnd : p.Nodup
    · exact ⟨p, hp, hnd, le_refl _⟩
    · obtain ⟨x, l₁, l₂, l₃, ht⟩ := exists_dup_decomp hnd
      -- chains of the pieces
      have hc_l1x2 : List.IsChain G.Adj (l₁ ++ (x :: l₂)) :=
        hp.chain.prefix ⟨x :: l₃, ht.symm⟩
      have hc1 : List.IsChain G.Adj l₁ := hc_l1x2.left_of_append
      have hc2 : List.IsChain G.Adj (x :: l₃) :=
        hp.chain.suffix ⟨l₁ ++ (x :: l₂), ht.symm⟩
      have hchain' : List.IsChain G.Adj (l₁ ++ x :: l₃) := by
        refine hc1.append hc2 ?_
        intro a ha b hb
        have hbx : b = x := (show x = b by simpa using hb).symm
        rw [hbx]
        exact (List.isChain_append.1 hc_l1x2).2.2 a ha x (by simp)
      -- head and last of the shortened walk
      have hhead' : (l₁ ++ x :: l₃).head? = some s := by
        have hh : (l₁ ++ x :: l₃).head? = p.head? := by
          rw [ht]; cases l₁ <;> simp
        rw [hh]; exact hp.head
      have hlast' : (l₁ ++ x :: l₃).getLast? = some v := by
        have hxl3 : (x :: l₃).getLast? = some v := by
          have hpe : p = (l₁ ++ x :: l₂) ++ (x :: l₃) := ht
          have hl := hp.last
          rw [hpe, List.getLast?_append_of_ne_nil _ (by simp : (x :: l₃) ≠ [])] at hl
          exact hl
        rw [List.getLast?_append_of_ne_nil _ (by simp : (x :: l₃) ≠ [])]
        exact hxl3
      have hp' : G.IsWalkFrom s v (l₁ ++ x :: l₃) := ⟨hchain', hhead', hlast'⟩
      -- the enclosed cycle from {lit}`x` to {lit}`x`
      have hcyc_walk : G.IsWalkFrom x x ((x :: l₂) ++ [x]) := by
        refine ⟨?_, ?_, ?_⟩
        · refine hp.chain.infix ⟨l₁, l₃, ?_⟩
          rw [ht]; simp [List.append_assoc]
        · rw [List.cons_append]; rfl
        · exact List.getLast?_concat
      have hcyc : (0 : ℝ) ≤ walkWeight G.w ((x :: l₂) ++ [x]) := hNC x _ hcyc_walk
      -- weight decomposition
      have hwp : walkWeight G.w p
          = walkWeight G.w (l₁ ++ [x]) + walkWeight G.w ((x :: l₂) ++ [x])
            + walkWeight G.w (x :: l₃) := by
        have e2 : (l₁ ++ (x :: l₂)) ++ [x] = l₁ ++ x :: (l₂ ++ [x]) := by simp
        have e3 : x :: (l₂ ++ [x]) = (x :: l₂) ++ [x] := by simp
        rw [ht, walkWeight_split G.w (l₁ ++ (x :: l₂)) x l₃, e2,
            walkWeight_split G.w l₁ x (l₂ ++ [x]), e3]
      have hwp' : walkWeight G.w (l₁ ++ x :: l₃)
          = walkWeight G.w (l₁ ++ [x]) + walkWeight G.w (x :: l₃) :=
        walkWeight_split G.w l₁ x l₃
      have hle : walkWeight G.w (l₁ ++ x :: l₃) ≤ walkWeight G.w p := by
        rw [hwp, hwp']; linarith
      -- the shortened walk is strictly shorter, so induction applies
      have hlp : p.length = l₁.length + l₂.length + l₃.length + 2 := by
        rw [ht]; simp only [List.length_append, List.length_cons]; omega
      have hlp' : (l₁ ++ x :: l₃).length = l₁.length + l₃.length + 1 := by
        simp only [List.length_append, List.length_cons]; omega
      have hlen' : (l₁ ++ x :: l₃).length ≤ n := by omega
      obtain ⟨q, hq, hqnd, hqle⟩ := ih (l₁ ++ x :: l₃) hlen' hp'
      exact ⟨q, hq, hqnd, le_trans hqle hle⟩

Correctness of Bellman-Ford (CLRS Theorem 22.4)

d is the single-source shortest-path distance δ(s, v): it lower-bounds every walk weight, and is either ⊤ (no walk exists) or attained by a walk. These are exactly CLRS's defining properties of δ.

def IsShortestDist (s v : V) (d : WithTop ℝ) : Prop :=
  (∀ p, G.IsWalkFrom s v p → d ≤ (walkWeight G.w p : WithTop ℝ)) ∧
    (d = ⊤ ∨ ∃ p, G.IsWalkFrom s v p ∧ (walkWeight G.w p : WithTop ℝ) = d)

CLRS Theorem 22.4 (correctness of Bellman-Ford). With no negative-weight cycle, the relaxation values after |V| - 1 rounds are exactly the single-source shortest-path distances δ(s, ·).


theorem relaxDist_isShortestDist (hNC : G.NoNegCycle) (s v : V) :
    G.IsShortestDist s v (G.relaxDist s (Fintype.card V - 1) v) := by
  have hcard : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr ⟨s⟩
  refine ⟨?_, ?_⟩
  · intro p hp
    obtain ⟨q, hq, hqnd, hqle⟩ := G.exists_simple_le hNC s v p.length p le_rfl hp
    have hqlen : q.length ≤ Fintype.card V := hqnd.length_le_card
    have hle := G.relaxDist_le_walkWeight s (Fintype.card V - 1) v q hq (by omega)
    calc G.relaxDist s (Fintype.card V - 1) v
        ≤ (walkWeight G.w q : WithTop ℝ) := hle
      _ ≤ (walkWeight G.w p : WithTop ℝ) := by exact_mod_cast hqle
  · rcases G.exists_walk_of_relaxDist s (Fintype.card V - 1) v with htop | ⟨p, hp, _, hpw⟩
    · left; exact htop
    · right; exact ⟨p, hp, hpw⟩

Convergence. With no negative cycle, one more relaxation round after |V| - 1 changes nothing: the estimates have stabilized at δ.


theorem relaxDist_stabilizes (hNC : G.NoNegCycle) (s v : V) :
    G.relaxDist s (Fintype.card V) v = G.relaxDist s (Fintype.card V - 1) v := by
  have hcard : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr ⟨s⟩
  refine le_antisymm ?_ ?_
  · have h : Fintype.card V = (Fintype.card V - 1) + 1 := by omega
    rw [h]; exact G.relaxDist_succ_le s (Fintype.card V - 1) v
  · rcases G.exists_walk_of_relaxDist s (Fintype.card V) v with htop | ⟨p, hp, _, hpw⟩
    · rw [htop]; exact le_top
    · rw [← hpw]
      exact (G.relaxDist_isShortestDist hNC s v).1 p hp

Work bound: `O(V·E)`

Total Bellman-Ford work: |V| - 1 relaxation rounds, each relaxing all |E| edges once, i.e. (|V| - 1) · |E| edge relaxations.

def bellmanFordWork (G : WeightedGraph V) : ℕ := (Fintype.card V - 1) * G.edges.card

O(V·E) work. The (|V| - 1) · |E| edge relaxations are bounded by |V| · |E|.

theorem bellmanFordWork_le : G.bellmanFordWork ≤ Fintype.card V * G.edges.card := by
  unfold bellmanFordWork
  exact Nat.mul_le_mul_right _ (Nat.sub_le _ _)

              end WeightedGraphend Chapter24end CLRS

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

22.2. Single-Source Shortest Paths in DAGs

This section proves a single relaxation pass correct given a supplied, complete, duplicate-free topological vertex order. It does not construct that weighted order from Chapter 20's unweighted topological sorter. Under the ordering hypothesis, every edge runs forward and one pass gives exact distances.

The section reuses the Chapter 22.1 weighted-graph model wholesale: the WeightedGraph structure, walkWeight, IsWalkFrom, and the shortest-distance specification IsShortestDist. Chapter 20.4's topological order is stated over the unweighted Chapter22.Graph; since Chapter 22 uses a different structure (Chapter24.WeightedGraph), we restate the topological-order predicate directly over WeightedGraph.Adj.

Main results:

CLRS.Chapter24.WeightedGraph.IsTopoOrder: a topological order of the weighted graph — a duplicate-free list of every vertex in which every directed edge runs forward (restatement of Chapter22.Graph.IsTopologicalOrder over WeightedGraph.Adj).
CLRS.Chapter24.WeightedGraph.isAcyclic_of_isTopoOrder: a weighted graph admitting a topological order is acyclic (the DAG hypothesis, obtained for free from the ordering).
CLRS.Chapter24.WeightedGraph.relaxFrom: relax all out-edges of a single vertex once.
CLRS.Chapter24.WeightedGraph.dagRelax: fold relaxFrom along a topological order, threading the tentative-distance map (DAG-SHORTEST-PATHS).
CLRS.Chapter24.WeightedGraph.dagRelax_respects_edge: after one pass in topological order the distances obey every edge constraint d v ≤ d u + w u v.
CLRS.Chapter24.WeightedGraph.dagRelax_isShortestDist: the CLRS §22.2 correctness statement — the folded distances are exactly the single-source shortest-path distances δ(s, ·), characterized by IsShortestDist.
CLRS.Chapter24.WeightedGraph.sum_outdegree and CLRS.Chapter24.WeightedGraph.dagSSSPWork_eq: the |V| + |E| = Θ(V + E) work bound — one pass touches each vertex once and each edge once.

Notation conventions used in this section:

G : a WeightedGraph
s : the source vertex
order : a topological order of G's vertices
d v : the tentative shortest-path estimate at v, valued in WithTop ℝ
⊤ : +∞, i.e. no walk found yet

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

Topological order and acyclicity over the weighted graph

A topological order of the weighted graph G: a duplicate-free list that contains every vertex, in which every directed edge u → v runs forward (the source occurs strictly before the target). This restates Chapter22.Graph.IsTopologicalOrder over CLRS.Chapter24.WeightedGraph.Adj, whose vertex set is all of the finite type V.

def IsTopoOrder (G : WeightedGraph V) (order : List V) : Prop :=
  order.Nodup ∧ (∀ v : V, v ∈ order) ∧
    (∀ u v : V, G.Adj u v → order.idxOf u < order.idxOf v)

A weighted graph is acyclic when no vertex reaches itself by a nontrivial directed path. This mirrors Chapter22.Graph.IsDAG.

def IsAcyclic (G : WeightedGraph V) : Prop := ∀ v, ¬ Relation.TransGen G.Adj v v

The finish-index of an edge strictly increases along a topological order, hence so does the index along any directed path (transitive closure).

theorem idxOf_lt_of_transGen {order : List V} (hlt : ∀ u v : V, G.Adj u v →
    order.idxOf u < order.idxOf v) {a b : V} (h : Relation.TransGen G.Adj a b) :
    order.idxOf a < order.idxOf b := by
  induction h with
  | single hab => exact hlt _ _ hab
  | tail _ hbc ih => exact lt_trans ih (hlt _ _ hbc)

The DAG hypothesis, for free. Any weighted graph that admits a topological order is acyclic: a directed cycle would force a vertex index to be strictly less than itself.

theorem isAcyclic_of_isTopoOrder {order : List V} (hTopo : G.IsTopoOrder order) :
    G.IsAcyclic := by
  intro v hv
  exact absurd (G.idxOf_lt_of_transGen hTopo.2.2 hv) (lt_irrefl _)

A purely combinatorial fact used to prove correctness: in a duplicate-free list split as pre ++ u :: suf, every vertex of suf occurs strictly after u.

omit [Fintype V] in


theorem idxOf_lt_of_split {order pre suf : List V} {u x : V}
    (hnd : order.Nodup) (hsplit : order = pre ++ u :: suf) (hx : x ∈ suf) :
    order.idxOf u < order.idxOf x := by
  subst hsplit
  have hdisj : pre.Disjoint (u :: suf) := List.disjoint_of_nodup_append hnd
  have hu_pre : u ∉ pre := fun h => hdisj h (List.mem_cons.2 (Or.inl rfl))
  have hx_pre : x ∉ pre := fun h => hdisj h (List.mem_cons.2 (Or.inr hx))
  have hu_suf : u ∉ suf := (List.nodup_cons.mp (List.Nodup.of_append_right hnd)).1
  have hxu : x ≠ u := fun h => hu_suf (h ▸ hx)
  rw [List.idxOf_append_of_notMem hu_pre, List.idxOf_append_of_notMem hx_pre,
    List.idxOf_cons_self, List.idxOf_cons_ne suf hxu.symm]
  omega

Single-vertex out-edge relaxation

Relax every out-edge of u once: for each edge u → v, lower the estimate d v to d u + w u v. Vertices with no edge from u are left unchanged (the ⊤ branch is absorbed by min).

def relaxFrom (d : V → WithTop ℝ) (u : V) : V → WithTop ℝ :=
  fun v => min (d v) (if G.Adj u v then d u + (G.w u v : WithTop ℝ) else ⊤)

@[simp] theorem relaxFrom_apply (d : V → WithTop ℝ) (u v : V) :
    G.relaxFrom d u v = min (d v) (if G.Adj u v then d u + (G.w u v : WithTop ℝ) else ⊤) :=
  rfl

One out-edge relaxation never increases an estimate.


theorem relaxFrom_le (d : V → WithTop ℝ) (u v : V) : G.relaxFrom d u v ≤ d v := by
  rw [relaxFrom_apply]; exact min_le_left _ _

The topological-order relaxation pass

DAG-SHORTEST-PATHS: initialize the source to 0 and every other vertex to ⊤, then fold relaxFrom along the topological order, relaxing the out-edges of each vertex exactly once.

def dagRelax (G : WeightedGraph V) (s : V) (order : List V) : V → WithTop ℝ :=
  order.foldl (fun d u => G.relaxFrom d u) (fun v => if v = s then (0 : WithTop ℝ) else ⊤)

theorem dagRelax_def (s : V) (order : List V) :
    G.dagRelax s order =
      order.foldl (fun d u => G.relaxFrom d u)
        (fun v => if v = s then (0 : WithTop ℝ) else ⊤) := rfl

Folding relaxFrom along any list only lowers estimates.

theorem foldl_relaxFrom_le :
    ∀ (l : List V) (d : V → WithTop ℝ) (v : V),
      l.foldl (fun d u => G.relaxFrom d u) d v ≤ d v := by
  intro l
  induction l with
  | nil => intro d v; simp
  | cons u l ih =>
    intro d v
    simp only [List.foldl_cons]
    exact le_trans (ih (G.relaxFrom d u) v) (G.relaxFrom_le d u v)

If no vertex of l has an edge into t, folding relaxFrom along l leaves the estimate at t unchanged.


theorem foldl_relaxFrom_eq_of_no_pred (t : V) :
    ∀ (l : List V) (d : V → WithTop ℝ), (∀ x ∈ l, ¬ G.Adj x t) →
      l.foldl (fun d u => G.relaxFrom d u) d t = d t := by
  intro l
  induction l with
  | nil => intro d _; simp
  | cons u l ih =>
    intro d h
    simp only [List.foldl_cons]
    have hut : ¬ G.Adj u t := h u (List.mem_cons.2 (Or.inl rfl))
    have hstep : G.relaxFrom d u t = d t := by
      rw [relaxFrom_apply, if_neg hut]; exact min_eq_left le_top
    rw [ih (G.relaxFrom d u) (fun x hx => h x (List.mem_cons.2 (Or.inr hx))), hstep]

Each edge is respected after one pass. For a topological order and any edge u → v, the folded distances satisfy d v ≤ d u + w u v.

The key structural facts: splitting order = pre ++ u :: suf, the estimate at u is already final when u is processed (no later vertex has an edge into u), while processing u lowers d v to at most d u + w u v, and later steps only lower it further.


theorem dagRelax_respects_edge (s : V) {order : List V}
    (hTopo : G.IsTopoOrder order) {u v : V} (hedge : G.Adj u v) :
    G.dagRelax s order v ≤ G.dagRelax s order u + (G.w u v : WithTop ℝ) := by
  obtain ⟨hnd, hmem, hlt⟩ := hTopo
  obtain ⟨pre, suf, hsplit⟩ := List.mem_iff_append.mp (hmem u)
  -- no later vertex points back into u, and u has no self-loop
  have hnusuf : ∀ x ∈ suf, ¬ G.Adj x u := by
    intro x hx hadjxu
    have h2 := idxOf_lt_of_split hnd hsplit hx
    have h1 := hlt x u hadjxu
    omega
  have hnuu : ¬ G.Adj u u := fun h => absurd (hlt u u h) (lt_irrefl _)
  -- decompose the fold at u
  have hdecomp : G.dagRelax s order =
      suf.foldl (fun d u => G.relaxFrom d u)
        (G.relaxFrom (pre.foldl (fun d u => G.relaxFrom d u)
          (fun v => if v = s then (0 : WithTop ℝ) else ⊤)) u) := by
    rw [dagRelax_def, hsplit, List.foldl_append, List.foldl_cons]
  set d1 := pre.foldl (fun d u => G.relaxFrom d u)
    (fun v => if v = s then (0 : WithTop ℝ) else ⊤) with hd1def
  -- u's estimate is final: processing suf never touches it
  have hDu : G.dagRelax s order u = d1 u := by
    rw [hdecomp, G.foldl_relaxFrom_eq_of_no_pred u suf (G.relaxFrom d1 u) hnusuf,
      relaxFrom_apply, if_neg hnuu, min_eq_left le_top]
  -- v's estimate was lowered past d1 u + w u v when u was processed
  have hDv : G.dagRelax s order v ≤ d1 u + (G.w u v : WithTop ℝ) := by
    rw [hdecomp]
    refine le_trans (G.foldl_relaxFrom_le suf (G.relaxFrom d1 u) v) ?_
    rw [relaxFrom_apply, if_pos hedge]
    exact min_le_right _ _
  rw [hDu]; exact hDv

Correctness: the folded distances are the shortest-path distances

Path-relaxation, telescoped. If a distance map respects every edge (d v ≤ d u + w u v), then along any walk d telescopes: d b ≤ d a + walkWeight p. This is the abstract core of shortest-path lower bounds.


theorem le_add_walkWeight_of_respects {d : V → WithTop ℝ}
    (hresp : ∀ a b, G.Adj a b → d b ≤ d a + (G.w a b : WithTop ℝ)) :
    ∀ (p : List V) (a b : V), G.IsWalkFrom a b p →
      d b ≤ d a + (walkWeight G.w p : WithTop ℝ) := by
  intro p
  induction p with
  | nil => intro a b hw; exact absurd rfl hw.ne_nil
  | cons x rest ih =>
    intro a b hw
    have hxa : x = a := by simpa using hw.head
    cases rest with
    | nil =>
      have hxb : x = b := by simpa using hw.last
      subst hxa; subst hxb; simp
    | cons y t =>
      subst hxa
      have hedge : G.Adj x y := hw.chain.rel_head
      have hchain' : List.IsChain G.Adj (y :: t) := hw.chain.tail
      have hlast' : (y :: t).getLast? = some b := by
        have h := hw.last; rwa [List.getLast?_cons_cons] at h
      have hw' : G.IsWalkFrom y b (y :: t) := ⟨hchain', rfl, hlast'⟩
      have h1 := ih y b hw'
      have h2 := hresp x y hedge
      have hcast : (walkWeight G.w (x :: y :: t) : WithTop ℝ)
          = (G.w x y : WithTop ℝ) + (walkWeight G.w (y :: t) : WithTop ℝ) := by
        rw [walkWeight_cons_cons, WithTop.coe_add]
      calc d b ≤ d y + (walkWeight G.w (y :: t) : WithTop ℝ) := h1
        _ ≤ (d x + (G.w x y : WithTop ℝ)) + (walkWeight G.w (y :: t) : WithTop ℝ) := by
              gcongr
        _ = d x + ((G.w x y : WithTop ℝ) + (walkWeight G.w (y :: t) : WithTop ℝ)) := by
              rw [add_assoc]
        _ = d x + (walkWeight G.w (x :: y :: t) : WithTop ℝ) := by rw [hcast]

d is realizable from s: every finite estimate is the weight of an actual walk from s. This is preserved by relaxation and holds initially.

def IsRealizable (G : WeightedGraph V) (s : V) (d : V → WithTop ℝ) : Prop :=
  ∀ v, d v = ⊤ ∨ ∃ p, G.IsWalkFrom s v p ∧ (walkWeight G.w p : WithTop ℝ) = d v

The initial estimate map is realizable: the source is reached by the trivial walk [s], everything else is ⊤.

theorem isRealizable_init (s : V) :
    G.IsRealizable s (fun v => if v = s then (0 : WithTop ℝ) else ⊤) := by
  intro v
  by_cases hv : v = s
  · right
    exact ⟨[v], ⟨List.isChain_singleton v, by simp [hv], by simp⟩, by simp [hv]⟩
  · left; simp [hv]

One out-edge relaxation preserves realizability: a newly lowered estimate at v comes from a realized estimate at u extended by the edge u → v.


theorem relaxFrom_isRealizable (s : V) (d : V → WithTop ℝ) (u : V)
    (hd : G.IsRealizable s d) : G.IsRealizable s (G.relaxFrom d u) := by
  intro v
  rw [relaxFrom_apply]
  rcases min_choice (d v) (if G.Adj u v then d u + (G.w u v : WithTop ℝ) else ⊤) with hm | hm
  · rw [hm]; exact hd v
  · rw [hm]
    by_cases hadj : G.Adj u v
    · rw [if_pos hadj]
      by_cases hdu : d u = ⊤
      · left; rw [hdu, WithTop.top_add]
      · rcases hd u with htop | ⟨q, hq, hqw⟩
        · exact absurd htop hdu
        · right
          have hqne : q ≠ [] := hq.ne_nil
          have hgl : q.getLast hqne = u := by
            have hh := List.getLast?_eq_some_getLast hqne
            rw [hq.last] at hh
            exact (Option.some.inj hh).symm
          refine ⟨q ++ [v], ⟨?_, ?_, ?_⟩, ?_⟩
          · refine List.IsChain.append hq.chain (List.isChain_singleton v) ?_
            intro a ha b hb
            have hau : a = u := by
              rw [Option.mem_def, hq.last] at ha
              exact (Option.some.inj ha).symm
            have hbv : b = v := Eq.symm (by simpa using hb)
            subst hau; subst hbv
            exact hadj
          · rw [List.head?_append_of_ne_nil _ hqne]; exact hq.head
          · simp
          · rw [walkWeight_append_singleton G.w q hqne v, hgl]
            push_cast
            rw [hqw]
    · rw [if_neg hadj]; left; rfl

Realizability is preserved by the whole relaxFrom fold.

theorem foldl_relaxFrom_isRealizable (s : V) :
    ∀ (l : List V) (d : V → WithTop ℝ), G.IsRealizable s d →
      G.IsRealizable s (l.foldl (fun d u => G.relaxFrom d u) d) := by
  intro l
  induction l with
  | nil => intro d hd; simpa using hd
  | cons u l ih =>
    intro d hd
    simp only [List.foldl_cons]
    exact ih (G.relaxFrom d u) (G.relaxFrom_isRealizable s d u hd)

The output of dagRelax is realizable from s.


theorem dagRelax_isRealizable (s : V) (order : List V) :
    G.IsRealizable s (G.dagRelax s order) := by
  rw [dagRelax_def]
  exact G.foldl_relaxFrom_isRealizable s order _ (G.isRealizable_init s)

The source estimate never exceeds 0.

theorem dagRelax_source_le (s : V) (order : List V) : G.dagRelax s order s ≤ 0 := by
  have h := G.foldl_relaxFrom_le order (fun v => if v = s then (0 : WithTop ℝ) else ⊤) s
  simpa [dagRelax_def] using h

CLRS §22.2 correctness (DAG-SHORTEST-PATHS). For a topological order of the (necessarily acyclic) weighted graph, the single relaxation pass computes the exact single-source shortest-path distances: for every vertex v, the folded estimate dagRelax s order v satisfies IsShortestDist s v, i.e. it equals δ(s, v).

The two halves are the lower bound (the estimate is ≤ every walk weight, via the per-edge upper-bound property telescoped along the walk) and realizability (the estimate is attained by an actual walk).


theorem dagRelax_isShortestDist (s : V) {order : List V}
    (hTopo : G.IsTopoOrder order) (v : V) :
    G.IsShortestDist s v (G.dagRelax s order v) := by
  refine ⟨?_, ?_⟩
  · intro p hp
    have hresp : ∀ a b, G.Adj a b →
        G.dagRelax s order b ≤ G.dagRelax s order a + (G.w a b : WithTop ℝ) :=
      fun a b hab => G.dagRelax_respects_edge s hTopo hab
    calc G.dagRelax s order v
        ≤ G.dagRelax s order s + (walkWeight G.w p : WithTop ℝ) :=
          G.le_add_walkWeight_of_respects hresp p s v hp
      _ ≤ 0 + (walkWeight G.w p : WithTop ℝ) := by
          have hsrc := G.dagRelax_source_le s order
          gcongr
      _ = (walkWeight G.w p : WithTop ℝ) := by rw [zero_add]
  · rcases G.dagRelax_isRealizable s order v with htop | ⟨p, hp, hpw⟩
    · left; exact htop
    · right; exact ⟨p, hp, hpw⟩

Work bound: `Θ(V + E)`

The out-degree of u: the number of edges leaving u.

def outdegree (G : WeightedGraph V) (u : V) : ℕ := (G.edges.filter (fun e => e.1 = u)).card

The out-degrees sum to the number of edges: one relaxation pass touches each edge exactly once.

theorem sum_outdegree (G : WeightedGraph V) :
    (∑ u : V, G.outdegree u) = G.edges.card := by
  simp only [outdegree]
  exact (Finset.card_eq_sum_card_fiberwise (fun e _ => Finset.mem_univ e.1)).symm

Independent vertex/edge budget for an ideal single pass; not an attached counter for the represented distance-map evaluation or order construction.

def dagSSSPWork (G : WeightedGraph V) : ℕ := Fintype.card V + G.edges.card

Arithmetic decomposition of the independent budget via out-degrees.


theorem dagSSSPWork_eq (G : WeightedGraph V) :
    G.dagSSSPWork = Fintype.card V + ∑ u : V, G.outdegree u := by
  rw [dagSSSPWork, sum_outdegree]

The independent budget is bounded by its defining formula.

theorem dagSSSPWork_le (G : WeightedGraph V) :
    G.dagSSSPWork ≤ Fintype.card V + G.edges.card := le_refl _

              end WeightedGraphend Chapter24end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

Directed adjacency: there is an edge from u to v.

def Adj (u v : V) : Prop := (u, v) ∈ G.edges

Imports

import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

22.3. Dijkstra's Algorithm

Building on the weighted directed-graph model and the shortest-path distance δ of Section 22.1, this section formalizes the correctness core of Dijkstra's algorithm under nonnegative edge weights: the greedy invariant (CLRS Theorem 22.6), stating that the unsettled vertex with minimum tentative distance already has the correct shortest-path distance. It also records the conditional binary-heap operation budget. The mathematical queue's minimum selector is not a concrete binary heap, and the budget is not a counter attached to its execution.

Main results:

CLRS.Chapter24.WeightedGraph.Nonneg: nonnegative edge weights.
CLRS.Chapter24.WeightedGraph.noNegCycle_of_nonneg: nonnegative weights have no negative cycle, so Section 22.1's δ machinery applies.
CLRS.Chapter24.WeightedGraph.walkWeight_nonneg: walks have nonnegative weight.
CLRS.Chapter24.WeightedGraph.exists_crossing: a walk from a settled to an unsettled vertex crosses the settled frontier.
CLRS.Chapter24.WeightedGraph.dijkstra_extractMin_correct: CLRS Theorem 22.6 (greedy invariant) — under the Dijkstra relaxation invariants, the extracted minimum-tentative-distance vertex has d u = δ u.
CLRS.Chapter24.WeightedGraph.dijkstraWork_le_edge_log: the (|V| + |E|)·log|V| binary-heap work is O(E log V) for connected graphs.

The greedy invariant is the mathematical heart of Dijkstra: a standard induction using it settles every reachable vertex with its exact distance. The executable priority-queue loop and its state threading are a separate refinement layer, consistent with the Chapter 22/23 graph track.

Notation conventions:

S : the set of settled vertices
d : tentative distances
δ : true shortest-path distances (from Section 22.1)
u : the vertex extracted with minimum tentative distance

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

Nonnegative weights

All edge weights are nonnegative (Dijkstra's hypothesis).

def Nonneg : Prop := ∀ u v, (u, v) ∈ G.edges → 0 ≤ G.w u v

With nonnegative weights every walk has nonnegative weight.


theorem walkWeight_nonneg (hnn : G.Nonneg) :
    ∀ {p : List V}, List.IsChain G.Adj p → 0 ≤ walkWeight G.w p := by
  intro p
  induction p with
  | nil => intro _; simp [walkWeight]
  | cons a t ih =>
    intro hp
    cases t with
    | nil => simp [walkWeight]
    | cons b t' =>
      rw [walkWeight_cons_cons]
      have hedge : (a, b) ∈ G.edges := hp.rel_head
      have h1 : 0 ≤ G.w a b := hnn a b hedge
      have h2 : 0 ≤ walkWeight G.w (b :: t') := ih hp.tail
      linarith

Nonnegative weights have no negative cycle, so the Section 22.1 shortest-path distance δ is well defined.

theorem noNegCycle_of_nonneg (hnn : G.Nonneg) : G.NoNegCycle := by
  intro x c hc
  exact G.walkWeight_nonneg hnn hc.chain

Crossing the settled frontier

A walk from a settled vertex a ∈ S to an unsettled vertex u ∉ S contains a frontier edge (x, y) with x ∈ S, y ∉ S, and a settled prefix reaching x.


theorem exists_crossing (S : Finset V) :
    ∀ (p : List V) (a u : V), G.IsWalkFrom a u p → a ∈ S → u ∉ S →
      ∃ (P R : List V) (x y : V), p = P ++ x :: y :: R ∧ x ∈ S ∧ y ∉ S ∧
        G.IsWalkFrom a x (P ++ [x]) := by
  intro p
  induction p with
  | nil => intro a u hp _ _; exact absurd rfl hp.ne_nil
  | cons a' rest ih =>
    intro a u hp haS huS
    have ha' : a' = a := by simpa using hp.head
    subst a'
    cases rest with
    | nil =>
      have hau : a = u := by simpa using hp.last
      exact absurd (hau ▸ haS) huS
    | cons c rest' =>
      have hac : G.Adj a c := hp.chain.rel_head
      by_cases hcS : c ∈ S
      · have hcwalk : G.IsWalkFrom c u (c :: rest') := by
          refine ⟨hp.chain.tail, by simp, ?_⟩
          rw [← List.getLast?_cons_cons (a := a)]; exact hp.last
        obtain ⟨P', R', x, y, heq, hx, hy, hwx⟩ := ih c u hcwalk hcS huS
        refine ⟨a :: P', R', x, y, by rw [heq]; simp, hx, hy, ?_⟩
        refine ⟨?_, by simp, List.getLast?_concat⟩
        refine hwx.chain.cons ?_
        intro z hz
        have hzc : z = c := by
          rw [Option.mem_def, hwx.head] at hz
          exact (Option.some.inj hz).symm
        rw [hzc]; exact hac
      · exact ⟨[], rest', a, c, by simp, haS, hcS,
          ⟨List.isChain_singleton a, by simp, by simp⟩⟩

The greedy invariant (CLRS Theorem 22.6)

CLRS Theorem 22.6 (Dijkstra greedy invariant). Suppose the source s is settled (s ∈ S), tentative distances never underestimate δ on the frontier (hvalid), and every frontier edge out of a settled vertex has been relaxed (htent). Then the unsettled vertex u of minimum tentative distance already has the correct shortest-path distance d u = δ u.

This is the invariant that makes Dijkstra correct under nonnegative weights: it justifies moving u into the settled set with a final, correct distance.


theorem dijkstra_extractMin_correct
    (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v))
    (S : Finset V) (hsS : s ∈ S) (d : V → WithTop ℝ)
    (htent : ∀ y, y ∉ S → ∀ x, x ∈ S → (x, y) ∈ G.edges →
      d y ≤ δ x + (G.w x y : WithTop ℝ))
    (hvalid : ∀ y, y ∉ S → δ y ≤ d y)
    (u : V) (hu : u ∉ S) (hmin : ∀ y, y ∉ S → d u ≤ d y) :
    d u = δ u := by
  refine le_antisymm ?_ (hvalid u hu)
  rcases (hδ u).2 with hutop | ⟨p, hp, hpw⟩
  · rw [hutop]; exact le_top
  · obtain ⟨P, R, x, y, heq, hxS, hyS, hwx⟩ := G.exists_crossing S p s u hp hsS hu
    obtain ⟨hPx_chain, hxy, hyR_chain⟩ :=
      List.isChain_append_cons_cons.1 (show List.IsChain G.Adj (P ++ x :: y :: R) by
        rw [← heq]; exact hp.chain)
    have hxy_edge : (x, y) ∈ G.edges := hxy
    -- weight of the prefix through the frontier edge is at most the whole walk
    have hp_eq2 : p = (P ++ [x]) ++ (y :: R) := by rw [heq]; simp
    have hsplit : walkWeight G.w p
        = walkWeight G.w ((P ++ [x]) ++ [y]) + walkWeight G.w (y :: R) := by
      rw [hp_eq2, walkWeight_split G.w (P ++ [x]) y R]
    have hconcat : walkWeight G.w ((P ++ [x]) ++ [y])
        = walkWeight G.w (P ++ [x]) + G.w x y := by
      rw [List.append_assoc]; exact walkWeight_concat G.w P x y
    have htail_nonneg : 0 ≤ walkWeight G.w (y :: R) := G.walkWeight_nonneg hnn hyR_chain
    have hprefix_le : walkWeight G.w (P ++ [x]) + G.w x y ≤ walkWeight G.w p := by
      rw [hsplit, hconcat]; linarith
    have hδx : δ x ≤ (walkWeight G.w (P ++ [x]) : WithTop ℝ) := (hδ x).1 (P ++ [x]) hwx
    have hdy : d y ≤ δ x + (G.w x y : WithTop ℝ) := htent y hyS x hxS hxy_edge
    calc d u ≤ d y := hmin y hyS
      _ ≤ δ x + (G.w x y : WithTop ℝ) := hdy
      _ ≤ (walkWeight G.w (P ++ [x]) : WithTop ℝ) + (G.w x y : WithTop ℝ) := by gcongr
      _ ≤ (walkWeight G.w p : WithTop ℝ) := by
          rw [← WithTop.coe_add]; exact_mod_cast hprefix_le
      _ = δ u := hpw

Work bound: `O(E log V)`

Abstract backend budget assuming the displayed numbers of extract-min and decrease-key operations at logarithmic unit charges. No concrete heap execution or operation-count refinement is asserted by this definition.

def dijkstraWork (vertices edges : Nat) : Nat :=
  (vertices + edges) * (Nat.log2 vertices + 1)

Arithmetic bound on the independent backend budget under the supplied vertex/edge-size inequality. This does not prove the queue execution cost.

theorem dijkstraWork_le_edge_log {vertices edges : Nat} (hconn : vertices ≤ 2 * edges) :
    dijkstraWork vertices edges ≤ 3 * edges * (Nat.log2 vertices + 1) := by
  unfold dijkstraWork
  apply Nat.mul_le_mul_right
  omega

Executable priority-queue loop

The state of the Dijkstra algorithm: the set of settled vertices and the current tentative distance map.

Settled vertices (those whose exact distance is known).

Tentative distances.

              @[ext]
structure DijkstraState (V : Type*) where  S : Finset V  d : V → WithTop ℝ

The initial state: source pre-settled with distance 0, and every outgoing edge (s, v) pre-relaxed to w s v. All other vertices have tentative distance ⊤.

This pre-settles the source and pre-relaxes its outgoing edges so that DijkstraInvariant holds from the start, matching CLRS's implicit first iteration that extracts s and relaxes its edges before entering the loop.

def dijkstraInit (s : V) : DijkstraState V :=
  { S := {s}
    d := fun v =>
      if v = s then (0 : WithTop ℝ)
      else if (s, v) ∈ G.edges then (G.w s v : WithTop ℝ)
      else ⊤ }

One iteration: extract an unsettled vertex of minimum tentative distance, settle it, and relax its outgoing edges. When no unsettled vertex remains, the state is unchanged. Noncomputable because V is not assumed to be linearly ordered.

noncomputable def dijkstraStep (G : WeightedGraph V) (st : DijkstraState V) : DijkstraState V :=
  let U := Finset.univ \ st.S
  if hU : U.Nonempty then
    have h_min : ∃ u ∈ U, ∀ v ∈ U, st.d u ≤ st.d v := U.exists_min_image st.d hU
    let u := Classical.choose h_min
    { S := insert u st.S
      d := fun v => if (u, v) ∈ G.edges then min (st.d v) (st.d u + (G.w u v : WithTop ℝ)) else st.d v }
  else st

The Dijkstra loop invariant. For a state st satisfying this invariant, settled vertices have their exact shortest-path distance, and the unsettled vertices satisfy the two properties required by CLRS Theorem 22.6.

The source is settled.

Every settled vertex has its exact distance.

For every frontier edge, the tentative distance at the unsettled endpoint is at most the optimal distance to the settled endpoint plus the edge weight.

Tentative distances never underestimate the true shortest-path distance.

              structure DijkstraInvariant (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) (st : DijkstraState V) : Prop where  hsS : s ∈ st.S  hsettled : ∀ x ∈ st.S, st.d x = δ x  htent : ∀ y ∉ st.S, ∀ x ∈ st.S, (x, y) ∈ G.edges →
    st.d y ≤ δ x + (G.w x y : WithTop ℝ)  hvalid : ∀ y ∉ st.S, δ y ≤ st.d y

The shortest-path distance from a vertex to itself is zero.


theorem isShortestDist_self_zero (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) : δ s = (0 : WithTop ℝ) := by
  have h_walk : G.IsWalkFrom s s [s] :=
    ⟨List.isChain_singleton s, by simp, by simp⟩
  have h_le : δ s ≤ (0 : WithTop ℝ) := (hδ s).1 [s] h_walk
  rcases (hδ s).2 with htop | ⟨p, hp, hpw⟩
  · rw [htop] at h_le; simp at h_le
  · have h_nonneg : (0 : ℝ) ≤ walkWeight G.w p := G.walkWeight_nonneg hnn hp.chain
    have hδ_nonneg : (0 : WithTop ℝ) ≤ δ s := by
      rw [← hpw]; exact_mod_cast h_nonneg
    exact le_antisymm h_le hδ_nonneg

If (u, v) is an edge, then the shortest-path distance to v is bounded above by the shortest-path distance to u plus the edge weight (triangle inequality).


theorem delta_le_delta_add_edge (Variable name `hnn` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ t, G.IsShortestDist s t (δ t)) (u v : V) (h_edge : (u, v) ∈ G.edges) :
    δ v ≤ δ u + (G.w u v : WithTop ℝ) := by
  rcases (hδ u).2 with hutop | ⟨q, hq, hqw⟩
  · -- δ u = ⊤, then RHS = ⊤, and the inequality holds trivially
    rw [hutop]; simp
  · -- δ u is finite, realized by walk q from s to u
    rcases (hδ v).2 with htop | ⟨p, hp, hpw⟩
    · -- δ v = ⊤: impossible because q ++ [v] is a walk from s to v (via u)
      exfalso
      have h_walk : G.IsWalkFrom s v (q ++ [v]) := by
        refine ⟨?_, ?_, ?_⟩
        · refine hq.chain.append (List.isChain_singleton v) ?_
          intro a ha b hb
          have ha_u : a = u := by
            rw [Option.mem_def, hq.last] at ha
            exact (Option.some.inj ha).symm
          subst ha_u
          have hb_v : b = v := by
            simpa using hb.symm
          subst hb_v
          exact h_edge
        · rw [List.head?_append_of_ne_nil _ hq.ne_nil]
          exact hq.head
        · simp
      have h_contra : δ v ≤ (walkWeight G.w (q ++ [v]) : WithTop ℝ) := (hδ v).1 _ h_walk
      rw [htop] at h_contra
      simp at h_contra
    · -- both δ u and δ v are finite
      have h_getlast_u : q.getLast hq.ne_nil = u := by
        have htemp := List.getLast?_eq_getLast_of_ne_nil hq.ne_nil
        have h_eq_some : some u = some (q.getLast hq.ne_nil) := by
          rw [← hq.last, htemp]
        exact (Option.some_inj.mp h_eq_some).symm
      have h_walk : G.IsWalkFrom s v (q ++ [v]) := by
        refine ⟨?_, ?_, ?_⟩
        · refine hq.chain.append (List.isChain_singleton v) ?_
          intro a ha b hb
          have ha_u : a = u := by
            rw [Option.mem_def, hq.last] at ha
            exact (Option.some.inj ha).symm
          subst ha_u
          have hb_v : b = v := by
            simpa using hb.symm
          subst hb_v
          exact h_edge
        · rw [List.head?_append_of_ne_nil _ hq.ne_nil]
          exact hq.head
        · simp
      have h_weight : (walkWeight G.w (q ++ [v]) : WithTop ℝ) = δ u + (G.w u v : WithTop ℝ) := by
        calc
          (walkWeight G.w (q ++ [v]) : WithTop ℝ) = ((walkWeight G.w q + G.w (q.getLast hq.ne_nil) v : ℝ) : WithTop ℝ) := by
            exact_mod_cast walkWeight_append_singleton G.w q hq.ne_nil v
          _ = (walkWeight G.w q : WithTop ℝ) + (G.w (q.getLast hq.ne_nil) v : WithTop ℝ) := by simp
          _ = (walkWeight G.w q : WithTop ℝ) + (G.w u v : WithTop ℝ) := by simp [h_getlast_u]
          _ = δ u + (G.w u v : WithTop ℝ) := by rw [hqw]
      have h_walk_weight : δ v ≤ (walkWeight G.w (q ++ [v]) : WithTop ℝ) :=
        (hδ v).1 (q ++ [v]) h_walk
      rw [h_weight] at h_walk_weight
      exact h_walk_weight

If the Dijkstra invariant holds, then any unsettled vertex u that minimizes st.d among unsettled vertices satisfies st.d u = δ u.

theorem extractMin_correct_of_invariant (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v))
    (st : DijkstraState V) (h_inv : DijkstraInvariant G hnn s δ hδ st)
    (u : V) (hu : u ∉ st.S) (hmin : ∀ y, y ∉ st.S → st.d u ≤ st.d y) :
    st.d u = δ u :=
  G.dijkstra_extractMin_correct hnn s δ hδ st.S h_inv.hsS st.d h_inv.htent h_inv.hvalid u hu hmin

If the Dijkstra invariant holds for st, then it also holds after one more dijkstraStep.


theorem dijkstraStep_invariant (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v))
    (st : DijkstraState V) (h_inv : DijkstraInvariant G hnn s δ hδ st) :
    DijkstraInvariant G hnn s δ hδ (dijkstraStep G st) := by
  unfold dijkstraStep
  let U := Finset.univ \ st.S
  by_cases hU : U.Nonempty
  · have h_min : ∃ u ∈ U, ∀ v ∈ U, st.d u ≤ st.d v := U.exists_min_image st.d hU
    let u := Classical.choose h_min
    have hu_mem : u ∈ U := (Classical.choose_spec h_min).1
    have hu_min : ∀ v ∈ U, st.d u ≤ st.d v := (Classical.choose_spec h_min).2
    have hu_notin_S : u ∉ st.S := (Finset.mem_sdiff.1 hu_mem).2
    have hu_min_all : ∀ y, y ∉ st.S → st.d u ≤ st.d y := by
      intro y hy
      apply hu_min y
      exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ y, hy⟩
    have h_du_eq_δu : st.d u = δ u :=
      G.extractMin_correct_of_invariant hnn s δ hδ st h_inv u hu_notin_S hu_min_all
    rw [dif_pos hU]
    let S' := insert u st.S
    let d' := fun v => if (u, v) ∈ G.edges then min (st.d v) (st.d u + (G.w u v : WithTop ℝ)) else st.d v
    have h_s_S' : s ∈ S' := Finset.mem_insert_of_mem h_inv.hsS
    have h_settled' : ∀ x ∈ S', d' x = δ x := by
      intro x hx
      rcases Finset.mem_insert.1 hx with (rfl | hx_S)
      · -- x = u
        dsimp [d']
        by_cases h_edge_uu : (u, u) ∈ G.edges
        · have h_nonneg_w : 0 ≤ G.w u u := hnn u u h_edge_uu
          have h_add : st.d u ≤ st.d u + (G.w u u : WithTop ℝ) := by
            have h_nonneg_w' : (0 : WithTop ℝ) ≤ (G.w u u : WithTop ℝ) := by exact_mod_cast h_nonneg_w
            exact le_add_of_nonneg_right h_nonneg_w'
          simp [h_edge_uu]
          have h_min_eq : min (st.d u) (st.d u + (G.w u u : WithTop ℝ)) = st.d u :=
            min_eq_left h_add
          rw [h_min_eq, h_du_eq_δu]
        · simp [h_edge_uu, h_du_eq_δu]
      · -- x ∈ st.S
        have h_dx_eq_δx : st.d x = δ x := h_inv.hsettled x hx_S
        dsimp [d']
        by_cases h_edge_ux : (u, x) ∈ G.edges
        · have h_ineq : δ x ≤ δ u + (G.w u x : WithTop ℝ) :=
            G.delta_le_delta_add_edge hnn s δ hδ u x h_edge_ux
          have h_add : st.d x ≤ st.d u + (G.w u x : WithTop ℝ) := by
            rw [h_dx_eq_δx, h_du_eq_δu]
            exact h_ineq
          simp [h_edge_ux]
          have h_min_eq : min (st.d x) (st.d u + (G.w u x : WithTop ℝ)) = st.d x :=
            min_eq_left h_add
          rw [h_min_eq, h_dx_eq_δx]
        · simp [h_edge_ux, h_dx_eq_δx]
    have h_htent' : ∀ y ∉ S', ∀ x ∈ S', (x, y) ∈ G.edges → d' y ≤ δ x + (G.w x y : WithTop ℝ) := by
      intro y hy_S' x hx_S' h_edge
      have hy_notin_S : y ∉ st.S := by
        intro hy_S; apply hy_S'; simp [S', hy_S]
      rcases Finset.mem_insert.1 hx_S' with (rfl | hx_S)
      · -- x = u
        dsimp [d']
        have h_edge_uy : (u, y) ∈ G.edges := h_edge
        calc
          (if (u, y) ∈ G.edges then min (st.d y) (st.d u + (G.w u y : WithTop ℝ)) else st.d y)
              = min (st.d y) (st.d u + (G.w u y : WithTop ℝ)) := by simp [h_edge_uy]
          _ ≤ st.d u + (G.w u y : WithTop ℝ) := min_le_right _ _
          _ = δ u + (G.w u y : WithTop ℝ) := by rw [h_du_eq_δu]
      · -- x ∈ st.S
        have h_old_htent : st.d y ≤ δ x + (G.w x y : WithTop ℝ) :=
          h_inv.htent y hy_notin_S x hx_S h_edge
        dsimp [d']
        by_cases h_edge_uy : (u, y) ∈ G.edges
        · calc
            (if (u, y) ∈ G.edges then min (st.d y) (st.d u + (G.w u y : WithTop ℝ)) else st.d y)
                = min (st.d y) (st.d u + (G.w u y : WithTop ℝ)) := by simp [h_edge_uy]
            _ ≤ st.d y := min_le_left _ _
            _ ≤ δ x + (G.w x y : WithTop ℝ) := h_old_htent
        · simp [h_edge_uy, h_old_htent]
    have h_valid' : ∀ y ∉ S', δ y ≤ d' y := by
      intro y hy_S'
      have hy_notin_S : y ∉ st.S := by
        intro hy_S; apply hy_S'; simp [S', hy_S]
      have h_old_valid : δ y ≤ st.d y := h_inv.hvalid y hy_notin_S
      by_cases h_edge_uy : (u, y) ∈ G.edges
      · have h_ineq : δ y ≤ δ u + (G.w u y : WithTop ℝ) :=
          G.delta_le_delta_add_edge hnn s δ hδ u y h_edge_uy
        have h_hvalid_via_add : δ y ≤ st.d u + (G.w u y : WithTop ℝ) := by
          rw [h_du_eq_δu]
          exact h_ineq
        simpa [d', h_edge_uy] using le_min_iff.mpr ⟨h_old_valid, h_hvalid_via_add⟩
      · simpa [d', h_edge_uy] using h_old_valid
    exact ⟨h_s_S', h_settled', h_htent', h_valid'⟩
  · rw [dif_neg hU]
    exact h_inv

Fuelled Dijkstra loop. dijkstraLoop G s n runs n iterations from the initial state.

noncomputable def dijkstraLoop (G : WeightedGraph V) (s : V) (n : ℕ) : DijkstraState V :=
  Nat.recOn n (dijkstraInit G s) (fun _ st => dijkstraStep G st)

Each step adds exactly one vertex (if unsettled vertices remain) or zero (if all are settled). Returns (card unchanged ∧ already all settled) or (+1 advancement).


lemma dijkstraStep_card_S (st : DijkstraState V) :
    ((dijkstraStep G st).S.card = st.S.card ∧ st.S = Finset.univ) ∨
    (dijkstraStep G st).S.card = st.S.card + 1 := by
  by_cases h_all : st.S = Finset.univ
  · -- all settled, step adds nothing
    have hcard : (dijkstraStep G st).S.card = st.S.card := by
      unfold dijkstraStep
      simp [h_all]
    left
    exact ⟨hcard, h_all⟩
  · -- unsettled vertices remain, step adds one
    have hU : (Finset.univ \ st.S).Nonempty := by
      have h_exists : ∃ v, v ∉ st.S := by
        by_contra! h_all_in
        apply h_all
        exact Finset.eq_univ_iff_forall.mpr h_all_in
      rcases h_exists with ⟨v, hv⟩
      refine ⟨v, Finset.mem_sdiff.mpr ⟨Finset.mem_univ v, hv⟩⟩
    have hcard' : (dijkstraStep G st).S.card = st.S.card + 1 := by
      unfold dijkstraStep
      rw [dif_pos hU]
      have h_min : ∃ u ∈ (Finset.univ \ st.S), ∀ v ∈ (Finset.univ \ st.S), st.d u ≤ st.d v :=
        (Finset.univ \ st.S).exists_min_image st.d hU
      let u := Classical.choose h_min
      have hu_mem : u ∈ (Finset.univ \ st.S) :=
        (Classical.choose_spec h_min).1
      have hu_notin_S : u ∉ st.S := (Finset.mem_sdiff.1 hu_mem).2
      dsimp
      rw [Finset.card_insert_of_notMem hu_notin_S]
    right
    exact hcard'

After k steps from the initial state, the settled set has size at least min k (Fintype.card V).


lemma dijkstraLoop_card_ge (G : WeightedGraph V) (s : V) (k : ℕ) :
    (dijkstraLoop G s k).S.card ≥ min k (Fintype.card V) := by
  induction k with
  | zero => simp [dijkstraLoop]
  | succ k ih =>
    have h_eq : dijkstraLoop G s (k+1) = dijkstraStep G (dijkstraLoop G s k) := by
      simp [dijkstraLoop]
    rw [h_eq]
    have hcases := G.dijkstraStep_card_S (dijkstraLoop G s k)
    rcases hcases with (⟨hcard, h_univ⟩ | hcard)
    · -- No addition, all vertices are already settled
      rw [hcard]
      have hcard' : (dijkstraLoop G s k).S.card = Fintype.card V := by
        simp [h_univ]
      rw [hcard']
      exact Nat.min_le_right (k+1) (Fintype.card V)
    · -- Added one unsettled vertex
      rw [hcard]
      omega

After at least Fintype.card V iterations, all vertices are settled.


theorem dijkstraLoop_finish (G : WeightedGraph V) (s : V) (n : ℕ) (hn : Fintype.card V ≤ n) :
    (dijkstraLoop G s n).S = Finset.univ := by
  have hcard_ge : (dijkstraLoop G s n).S.card ≥ Fintype.card V := by
    have hmin : min n (Fintype.card V) = Fintype.card V := Nat.min_eq_right hn
    have h := G.dijkstraLoop_card_ge s n
    rw [hmin] at h
    exact h
  have hcard_le : (dijkstraLoop G s n).S.card ≤ Fintype.card V := by
    calc
      (dijkstraLoop G s n).S.card ≤ (Finset.univ : Finset V).card :=
        Finset.card_le_card (Finset.subset_univ _)
      _ = Fintype.card V := card_univ
  have hcard_eq : (dijkstraLoop G s n).S.card = Fintype.card V := by omega
  have h_sub : (dijkstraLoop G s n).S ⊆ Finset.univ := Finset.subset_univ _
  exact Finset.eq_of_subset_of_card_le h_sub (by
    rw [hcard_eq, card_univ])

Initial invariant and final correctness

The initial Dijkstra state satisfies the invariant: the source is pre-settled with distance 0 (which equals δ s by isShortestDist_self_zero), every outgoing edge (s, y) is pre-relaxed to w s y, the frontier-edge condition holds because d y = w s y = δ s + w s y, and δ y ≤ w s y holds because [s, y] is a walk from s to y.


theorem dijkstraInit_invariant (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) :
    DijkstraInvariant G hnn s δ hδ (dijkstraInit G s) := by
  refine {
    hsS := by simp [dijkstraInit]
    hsettled := by
      intro x hx
      have hxS : x = s := by simpa [dijkstraInit] using hx
      subst x
      have hδs : δ s = (0 : WithTop ℝ) := G.isShortestDist_self_zero hnn s δ hδ
      simp [dijkstraInit, hδs]
    htent := by
      intro y hyS x hxS hedge
      have hx : x = s := by simpa [dijkstraInit] using hxS
      subst x
      have hy : y ≠ s := by
        intro h; subst y; exact hyS (by simp [dijkstraInit])
      have hδs : δ s = (0 : WithTop ℝ) := G.isShortestDist_self_zero hnn s δ hδ
      simp [dijkstraInit, hy, hedge, hδs]
    hvalid := by
      intro y hyS
      have hy : y ≠ s := by
        intro h; subst y; exact hyS (by simp [dijkstraInit])
      by_cases hedge : (s, y) ∈ G.edges
      · -- δ y ≤ w s y because [s, y] is a walk
        have h_walk : G.IsWalkFrom s y [s, y] := by
          refine ⟨?_, by simp, by simp⟩
          simp [WeightedGraph.Adj, hedge, This simp argument is unused:
  List.isChain_singleton

Hint: Omit it from the simp argument list.
  simp [WeightedGraph.Adj, hedge,̵ ̵L̵i̵s̵t̵.̵i̵s̵C̵h̵a̵i̵n̵_̵s̵i̵n̵g̵l̵e̵t̵o̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`List.isChain_singleton]
        have hδy_le : δ y ≤ (G.w s y : WithTop ℝ) := by
          simpa [walkWeight_singleton, walkWeight_cons_cons] using (hδ y).1 [s, y] h_walk
        simp [dijkstraInit, hy, hedge, hδy_le]
      · simp [dijkstraInit, hy, hedge]
  }

The Dijkstra invariant is preserved by the fuelled loop: if it holds for the initial state, it holds after any number of iterations.


theorem dijkstraLoop_invariant (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) (k : ℕ) :
    DijkstraInvariant G hnn s δ hδ (dijkstraLoop G s k) := by
  induction k with
  | zero =>
      simpa [dijkstraLoop] using dijkstraInit_invariant G hnn s δ hδ
  | succ k ih =>
      rw [dijkstraLoop]
      exact dijkstraStep_invariant G hnn s δ hδ (dijkstraLoop G s k) ih

Dijkstra correctness. After Fintype.card V iterations, every vertex has its exact shortest-path distance: (dijkstraLoop G s n).d v = δ v for all v, provided n ≥ Fintype.card V. In particular, n = Fintype.card V suffices.


theorem dijkstraLoop_correct (hnn : G.Nonneg) (s : V) (δ : V → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) (n : ℕ) (hn : Fintype.card V ≤ n) (v : V) :
    (dijkstraLoop G s n).d v = δ v := by
  have hfin := G.dijkstraLoop_finish s n hn
  have hinv := dijkstraLoop_invariant G hnn s δ hδ n
  have h_mem : v ∈ (dijkstraLoop G s n).S := by rw [hfin]; exact Finset.mem_univ v
  exact hinv.hsettled v h_mem

              end WeightedGraphend Chapter24end CLRS

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

22.4. Difference Constraints and Shortest Paths

This section formalizes the connection between systems of difference constraints and shortest paths (CLRS §22.4). A difference constraint is an inequality of the form x_j ≤ x_i + b. The system is feasible if there exists a real assignment x satisfying every constraint.

The key insight is to build the constraint graph: one vertex per variable, plus a fresh source s with a zero-weight edge to every variable vertex, and an edge (i, j) of weight b for each constraint x_j ≤ x_i + b. Then

Theorem 22.9: the system is feasible ↔ the constraint graph has no negative-weight cycle (NoNegCycle). The forward direction uses a potential function; the reverse direction builds an explicit feasible assignment from the Bellman-Ford shortest-path distances δ(s, ·).

The section reuses the Chapter 22.1 weighted-graph model wholesale: the WeightedGraph structure, NoNegCycle, IsShortestDist, relaxDist, and the correctness theorem relaxDist_isShortestDist (CLRS Theorem 22.4).

Main results:

CLRS.Chapter24.WeightedGraph.DiffConstraintSystem: a finite set of difference constraints x_j ≤ x_i + b.
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.IsFeasible: an assignment satisfies every constraint.
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.constraintGraph: the constraint graph built from the system.
CLRS.Chapter24.WeightedGraph.le_add_walkWeight_of_potential: a general potential-function lemma used in the forward direction.
CLRS.Chapter24.WeightedGraph.relaxDist_respects_edge: after |V| - 1 rounds, Bellman-Ford estimates satisfy the triangle inequality δ(s, v) ≤ δ(s, u) + w(u, v).
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.le_add_walkWeight_some: potential lemma for constraint edges.
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.noNegCycle_of_feasible: feasible assignment ⇒ no negative-weight cycle (Theorem 22.9, forward).
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.feasible_of_noNegCycle: no negative-weight cycle ⇒ feasible assignment via Bellman-Ford (Theorem 22.9, reverse).
CLRS.Chapter24.WeightedGraph.DiffConstraintSystem.diffConstraint_feasible_iff_noNegCycle: CLRS Theorem 22.9 — the full equivalence, with explicit Bellman-Ford solution.

Notation conventions used in this section:

I : the variable index type
sys : a DiffConstraintSystem I
x : an assignment I → ℝ
s (or none) : the source vertex of the constraint graph
δ : the single-source shortest-path distance

              namespace CLRSnamespace Chapter24open Finsetnamespace WeightedGraph

Difference constraint systems

A system of difference constraints over variables indexed by I. Each recorded constraint (i, j) ∈ constraints demands x_j ≤ x_i + b i j.

The variable pairs that have a constraint.

The bound for each pair: x_j ≤ x_i + b i j.

              structure DiffConstraintSystem (I : Type*) [Fintype I] [DecidableEq I] where  constraints : Finset (I × I)  b : I → I → ℝ

namespace DiffConstraintSystemvariable {I : Type*} [Fintype I] [DecidableEq I] (sys : DiffConstraintSystem I)

An assignment x : I → ℝ satisfies every constraint in the system.

def IsFeasible (x : I → ℝ) : Prop :=
  ∀ i j, (i, j) ∈ sys.constraints → x j ≤ x i + sys.b i j

The constraint graph of sys. Vertices are Option I; the source none has a zero-weight edge to each variable vertex, and each constraint (i, j) contributes a directed edge (some i) → (some j) of weight sys.b i j.

def constraintGraph : WeightedGraph (Option I) :=
  { edges := (Finset.univ.image fun (i : I) => (none, some i)) ∪
             (sys.constraints.image fun (ij : I × I) => (some ij.1, some ij.2))
  , w := fun u v =>
      match u, v with
      | none, some Variable name `i` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`i => 0
      | some i, some j => if (i, j) ∈ sys.constraints then sys.b i j else 0
      | _, _ => 0
  }

              @[simp] theorem mem_edges_source (i : I) : (none, some i) ∈ sys.constraintGraph.edges := by
  dsimp [constraintGraph]
  simp@[simp] theorem mem_edges_constraint {i j : I} :
    (some i, some j) ∈ sys.constraintGraph.edges ↔ (i, j) ∈ sys.constraints := by
  dsimp [constraintGraph]
  simptheorem constraintGraph_w_source (i : I) : sys.constraintGraph.w none (some i) = 0 := rfltheorem constraintGraph_w_constraint (i j : I) :
    sys.constraintGraph.w (some i) (some j) = if (i, j) ∈ sys.constraints then sys.b i j else 0 := rfl

The source vertex none has no incoming edges in the constraint graph.

lemma no_incoming_to_none (u : Option I) : (u, none) ∉ sys.constraintGraph.edges := by
  dsimp [constraintGraph]
  simp

For a feasible assignment, every constraint edge respects the potential.

lemma constraint_edge_potential (hx : sys.IsFeasible x) (i j : I) (hmem : (i, j) ∈ sys.constraints) :
    x j ≤ x i + sys.constraintGraph.w (some i) (some j) := by
  have hx_ij := hx i j hmem
  simp [constraintGraph_w_constraint, hmem]
  exact hx_ij

end DiffConstraintSystem

Potential-function lemma

Potential-function lemma. Let f : V → ℝ be a potential such that f v ≤ f u + w u v for every edge (u, v). Then for any walk from a to b, we have f b ≤ f a + walkWeight G.w p.


theorem le_add_walkWeight_of_potential {V : Type*} [Fintype V] [DecidableEq V] (G : WeightedGraph V)
    (f : V → ℝ) (h_edge : ∀ u v, (u, v) ∈ G.edges → f v ≤ f u + G.w u v) (a b : V) (p : List V)
    (hp : G.IsWalkFrom a b p) : f b ≤ f a + walkWeight G.w p := by
  induction p generalizing a b with
  | nil => exfalso; apply hp.ne_nil; rfl
  | cons x xs ih =>
    have ha_x : a = x := by
      have hhead := hp.head
      simp at hhead
      exact hhead.symm
    subst ha_x
    match xs with
    | [] =>
      have hb_a : b = a := by
        have hlast := hp.last
        simp at hlast
        exact hlast.symm
      subst hb_a
      simp
    | y :: ys =>
      have htail_walk : G.IsWalkFrom y b (y :: ys) := by
        have hchain : List.IsChain G.Adj (a :: y :: ys) := hp.chain
        have hchain_tail : List.IsChain G.Adj (y :: ys) := by
          cases hchain with
          | cons_cons _ htail => exact htail
        refine ⟨hchain_tail, by simp, hp.last⟩
      have h_adj : G.Adj a y := by
        have hchain : List.IsChain G.Adj (a :: y :: ys) := hp.chain
        cases hchain with
        | cons_cons h _ => exact h
      have hedge : (a, y) ∈ G.edges := h_adj
      have h_edge_ay := h_edge a y hedge
      have ih_ty := ih y b htail_walk
      calc
        f b ≤ f y + walkWeight G.w (y :: ys) := ih_ty
        _ ≤ (f a + G.w a y) + walkWeight G.w (y :: ys) := by gcongr
        _ = f a + (G.w a y + walkWeight G.w (y :: ys)) := by ring
        _ = f a + walkWeight G.w (a :: y :: ys) := by simp

Triangle inequality for Bellman-Ford

After |V| - 1 rounds, the Bellman-Ford shortest-path estimates respect every edge: δ(s, v) ≤ δ(s, u) + w(u, v) (the triangle inequality).


theorem relaxDist_respects_edge {V : Type*} [Fintype V] [DecidableEq V] (G : WeightedGraph V)
    (hNC : G.NoNegCycle) (s u v : V) (h_edge : (u, v) ∈ G.edges) :
    G.relaxDist s (Fintype.card V - 1) v ≤
    G.relaxDist s (Fintype.card V - 1) u + (G.w u v : WithTop ℝ) := by
  have hdist_u : G.IsShortestDist s u (G.relaxDist s (Fintype.card V - 1) u) :=
    G.relaxDist_isShortestDist hNC s u
  have hdist_v : G.IsShortestDist s v (G.relaxDist s (Fintype.card V - 1) v) :=
    G.relaxDist_isShortestDist hNC s v
  rcases hdist_u.2 with (hu_top | ⟨p, hp, hpw⟩)
  · -- δ(s, u) = ⊤, so RHS = ⊤, trivial
    simp [hu_top]
  · have hp_ne : p ≠ [] := hp.ne_nil
    have hpv_walk : G.IsWalkFrom s v (p ++ [v]) := by
      refine ⟨?_, ?_, by simp⟩
      · refine List.IsChain.append hp.chain (List.isChain_singleton v) ?_
        intro x hx y hy
        have hx_u : x = u := by
          rw [Option.mem_def, hp.last] at hx
          exact (Option.some.inj hx).symm
        have hy_v : y = v := Eq.symm (by simpa using hy)
        subst hx_u; subst hy_v
        exact h_edge
      · rw [List.head?_append_of_ne_nil _ hp_ne]
        exact hp.head
    have h_walk_weight' : (walkWeight G.w (p ++ [v]) : WithTop ℝ) =
        G.relaxDist s (Fintype.card V - 1) u + (G.w u v : WithTop ℝ) := by
      have h_last : p.getLast hp_ne = u := by
        have hlast := hp.last
        rw [List.getLast?_eq_some_getLast hp_ne] at hlast
        exact Option.some.inj hlast
      have h_ℝ : walkWeight G.w (p ++ [v]) = walkWeight G.w p + G.w u v := by
        rw [walkWeight_append_singleton G.w p hp_ne v, h_last]
      calc
        (walkWeight G.w (p ++ [v]) : WithTop ℝ) = (walkWeight G.w p : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
          simp [h_ℝ]
        _ = G.relaxDist s (Fintype.card V - 1) u + (G.w u v : WithTop ℝ) := by rw [hpw]
    have hle : G.relaxDist s (Fintype.card V - 1) v ≤
        (walkWeight G.w (p ++ [v]) : WithTop ℝ) := hdist_v.1 _ hpv_walk
    calc
      G.relaxDist s (Fintype.card V - 1) v ≤ (walkWeight G.w (p ++ [v]) : WithTop ℝ) := hle
      _ = G.relaxDist s (Fintype.card V - 1) u + (G.w u v : WithTop ℝ) := h_walk_weight'

namespace DiffConstraintSystemvariable {I : Type*} [Fintype I] [DecidableEq I] (sys : DiffConstraintSystem I)

Potential lemma for constraint edges. For any walk from some a to some b in the constraint graph, we have x b ≤ x a + walkWeight CG.w c.


lemma le_add_walkWeight_some (hx : sys.IsFeasible x) (a b : I) (c : List (Option I))
    (hp : (sys.constraintGraph).IsWalkFrom (some a) (some b) c) :
    x b ≤ x a + walkWeight (sys.constraintGraph).w c := by
  induction c generalizing a b with
  | nil => exfalso; apply hp.ne_nil; rfl
  | cons z zs ih =>
    have hz_some : z = some a := by simpa using hp.head
    subst hz_some
    match zs with
    | [] =>
      have hb_a : b = a := by
        have hl := hp.last
        simp at hl
        have h_some_inj : some a = some b := by simpa using hl
        injection h_some_inj with h_eq
        exact h_eq.symm
      subst hb_a; simp
    | y :: ys =>
      -- Show y = some j for some j
      have hy_some : ∃ j : I, y = some j := by
        have h_adj : (sys.constraintGraph).Adj (some a) y := by
          have hchain : List.IsChain (sys.constraintGraph).Adj ((some a) :: y :: ys) := hp.chain
          cases hchain with
          | cons_cons hadj _ => exact hadj
        rcases y with (y | y)
        · exfalso
          -- y = none, but there's no edge from some a to none by constraint graph construction
          dsimp [Adj] at h_adj
          apply sys.no_incoming_to_none (some a)
          exact h_adj
        · exact ⟨y, rfl⟩
      rcases hy_some with ⟨j, hyj⟩
      subst hyj
      have hedge : ((some a, some j) : Option I × Option I) ∈ (sys.constraintGraph).edges := by
        have h_adj : (sys.constraintGraph).Adj (some a) (some j) := by
          have hchain : List.IsChain (sys.constraintGraph).Adj ((some a) :: (some j) :: ys) := hp.chain
          cases hchain with
          | cons_cons hadj _ => exact hadj
        exact h_adj
      have hm : (a, j) ∈ sys.constraints := by
        dsimp [constraintGraph] at hedge; simpa using hedge
      have hx_ineq : x j ≤ x a + sys.b a j := hx a j hm
      have htail_walk : (sys.constraintGraph).IsWalkFrom (some j) (some b) ((some j) :: ys) := by
        have htail_chain : List.IsChain (sys.constraintGraph).Adj ((some j) :: ys) := by
          have hchain : List.IsChain (sys.constraintGraph).Adj ((some a) :: (some j) :: ys) := hp.chain
          cases hchain with
          | cons_cons _ htail => exact htail
        refine ⟨htail_chain, by simp, ?_⟩
        simpa using hp.last
      have ih_tail : x b ≤ x j + walkWeight (sys.constraintGraph).w ((some j) :: ys) :=
        ih j b htail_walk
      have hw_constraint : (sys.constraintGraph).w (some a) (some j) = sys.b a j := by
        simp [constraintGraph_w_constraint, hm]
      calc
        x b ≤ x j + walkWeight (sys.constraintGraph).w ((some j) :: ys) := ih_tail
        _ ≤ (x a + sys.b a j) + walkWeight (sys.constraintGraph).w ((some j) :: ys) := by gcongr
        _ = x a + (sys.b a j + walkWeight (sys.constraintGraph).w ((some j) :: ys)) := by ring
        _ = x a + walkWeight (sys.constraintGraph).w ((some a) :: (some j) :: ys) := by
          simp [hw_constraint]

Feasible → no negative cycle. If the system has a feasible assignment, then the constraint graph has no negative-weight cycle (Theorem 22.9, forward).


theorem noNegCycle_of_feasible (hx : sys.IsFeasible x) :
    sys.constraintGraph.NoNegCycle := by
  set CG := sys.constraintGraph with hCG
  intro v c hwalk
  rcases v with (v | v)
  · -- v = none: the only closed walk from none is [none] (weight 0)
    -- because there are no edges entering none
    have hc_singleton : c = [none] := by
      by_contra! h
      -- h : c ≠ [none]
      have hne : c ≠ [] := hwalk.ne_nil
      -- Determine length: if length = 1 then c = [none]; if length ≥ 2 then impossible
      by_cases hlen1 : c.length = 1
      · -- c.length = 1, so c = [c.head ...] = [none]
        have hhead_val : c.head hne = none := by
          have hh := hwalk.head
          -- hh : c.head? = some none  →  ∃ ys, c = none :: ys
          rcases List.head?_eq_some_iff.mp hh with ⟨ys, hc_eq⟩
          simp [hc_eq]
        rcases c with (_ | ⟨x, xs⟩)
        · exact hne rfl
        · have hxs_empty : xs = [] := by
            cases xs with
            | nil => rfl
            | cons y ys =>
              have : (x :: y :: ys).length ≥ 2 := by simp
              have hlen1' : (x :: y :: ys).length = 1 := hlen1
              omega
          subst hxs_empty
          have hx : x = none := hhead_val
          subst hx; exfalso; exact h rfl
      · -- c.length ≠ 1, so c.length ≥ 2 (since c ≠ [])
        have hlen_gt_1 : c.length ≥ 2 := by
          have hpos : c.length ≥ 1 := by
            have hpos' : c.length > 0 := by
              apply Nat.pos_of_ne_zero
              intro hzero
              apply hne
              simpa using hzero
            omega
          have hneq1 : c.length ≠ 1 := hlen1
          omega
        -- Since c has at least 2 elements, destruct it
        rcases c with (_ | ⟨a, r⟩)
        · exact hne rfl
        · rcases r with (_ | ⟨b, tl⟩)
          · -- c = [a]; with length ≥ 2, impossible
            have : (a :: []).length ≥ 2 := hlen_gt_1
            simp at this
          · -- c = a :: b :: tl
            have ha_none : a = none := by
              have hh := hwalk.head
              simpa using hh
            subst ha_none
            -- c = none :: b :: tl, ends with none
            have hne_nbtl : (none :: b :: tl) ≠ [] := by simp
            have hlast_val : List.getLast (none :: b :: tl) hne_nbtl = none := by
              have hlast' := hwalk.last
              rw [List.getLast?_eq_some_getLast hne_nbtl] at hlast'
              exact Option.some.inj hlast'
            have hsplit : (none :: b :: tl) = ((none :: b :: tl).dropLast) ++ [none] := by
              conv_lhs => rw [← List.dropLast_append_getLast hne_nbtl, hlast_val]
            have hchain' : List.IsChain CG.Adj (((none :: b :: tl).dropLast) ++ [none]) := by
              rw [← hsplit]; exact hwalk.chain
            have happ := List.isChain_append.1 hchain'
            have hlen_gt_1' : (none :: b :: tl).length ≥ 2 := by
              simp
            have hdrop_ne : (none :: b :: tl).dropLast ≠ [] := by
              intro hdrop
              have hlen1 : (none :: b :: tl).length = 1 := by
                have hlen_eq : (none :: b :: tl).length = ((none :: b :: tl).dropLast).length + 1 := by
                  rw [hsplit]; simp
                rw [hlen_eq, hdrop]; simp
              omega
            have hu_mem : List.getLast ((none :: b :: tl).dropLast) hdrop_ne ∈ ((none :: b :: tl).dropLast).getLast? := by
              rw [List.getLast?_eq_some_getLast hdrop_ne]
              simp
            have h_penultimate_edge : CG.Adj (List.getLast ((none :: b :: tl).dropLast) hdrop_ne) none :=
              happ.2.2 (List.getLast ((none :: b :: tl).dropLast) hdrop_ne) hu_mem none (by simp)
            have h_edge : (List.getLast ((none :: b :: tl).dropLast) hdrop_ne, none) ∈ CG.edges := h_penultimate_edge
            exact sys.no_incoming_to_none (List.getLast ((none :: b :: tl).dropLast) hdrop_ne) h_edge
    subst hc_singleton; simp
  · -- v = some i: apply the potential lemma for constraint edges
    have := sys.le_add_walkWeight_some hx v v c hwalk
    linarith

No negative cycle → feasible. If the constraint graph has no negative cycle, then the Bellman-Ford shortest-path distances δ(none, some i) give an explicit feasible assignment (Theorem 22.9, reverse).


theorem feasible_of_noNegCycle (hNC : sys.constraintGraph.NoNegCycle) :
    ∃ x : I → ℝ, sys.IsFeasible x := by
  set CG := sys.constraintGraph with hCG
  have hcard : 1 ≤ Fintype.card (Option I) :=
    Fintype.card_pos_iff.mpr ⟨none⟩
  -- Bellman-Ford shortest distances from the source
  let d : Option I → WithTop ℝ := CG.relaxDist none (Fintype.card (Option I) - 1)
  have hdist : ∀ (v : Option I), CG.IsShortestDist none v (d v) :=
    fun v => CG.relaxDist_isShortestDist hNC none v

  -- Each d (some i) is finite because there is a zero-weight walk from none to some i
  have hfinite (i : I) : d (some i) ≠ ⊤ := by
    have hzero_walk : CG.IsWalkFrom none (some i) [none, some i] := by
      have hadj : CG.Adj none (some i) := by
        dsimp [CG, constraintGraph, Adj]; simp
      have hchain : List.IsChain CG.Adj [none, some i] :=
        List.IsChain.cons (List.isChain_singleton (some i)) (by
          intro y hy
          have hy_eq : some i = y := by simpa using hy
          rw [← hy_eq]
          exact hadj)
      refine ⟨hchain, by simp, by simp⟩
    have hle : d (some i) ≤ (0 : WithTop ℝ) := by
      have := (hdist (some i)).1 _ hzero_walk
      have hweight : walkWeight CG.w [none, some i] = 0 := by
        calc
          walkWeight CG.w [none, some i] = CG.w none (some i) := by simp
          _ = 0 := sys.constraintGraph_w_source i
      simpa [hweight] using this
    intro htop
    have : (⊤ : WithTop ℝ) ≤ (0 : WithTop ℝ) := by rw [← htop]; exact hle
    simp at this

  have hfinite' (i : I) : ∃ r : ℝ, d (some i) = (r : WithTop ℝ) := by
    have hi : d (some i) ≠ (none : Option ℝ) := hfinite i
    rcases (Option.ne_none_iff_exists.mp hi) with ⟨r, hr⟩
    exact ⟨r, hr.symm⟩
  choose x hx using hfinite'

  refine ⟨x, ?_⟩
  intro i j hij
  have hedge : (some i, some j) ∈ CG.edges := by
    dsimp [CG, constraintGraph]
    simp [hij]
  have htri : d (some j) ≤ d (some i) + (CG.w (some i) (some j) : WithTop ℝ) :=
    CG.relaxDist_respects_edge hNC none (some i) (some j) hedge
  have hw : CG.w (some i) (some j) = sys.b i j := by
    dsimp [CG, constraintGraph]
    simp [hij]
  rw [hw] at htri
  rw [hx i, hx j] at htri
  -- htri: (x j : WithTop ℝ) ≤ (x i : WithTop ℝ) + (sys.b i j : WithTop ℝ)
  have htri' : (x j : WithTop ℝ) ≤ (x i + sys.b i j : WithTop ℝ) := by
    simpa [WithTop.coe_add] using htri
  exact WithTop.coe_le_coe.mp htri'

CLRS Theorem 22.9 (difference constraints and shortest paths). A system of difference constraints is feasible iff its constraint graph has no negative-weight cycle. When feasible, the Bellman-Ford shortest-path distances from the source give an explicit solution x i = δ(s, i).

theorem diffConstraint_feasible_iff_noNegCycle :
    (∃ x : I → ℝ, sys.IsFeasible x) ↔ sys.constraintGraph.NoNegCycle := by
  constructor
  · rintro ⟨x, hx⟩
    exact sys.noNegCycle_of_feasible hx
  · intro hNC
    rcases sys.feasible_of_noNegCycle hNC with ⟨x, hx⟩
    exact ⟨x, hx⟩

              end DiffConstraintSystemend WeightedGraphend Chapter24end CLRS

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

Scope and implementation notes

Imports

import CLRSLean.Chapter_24
import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford
import CLRSLean.FourthEdition.Chapter_22.Section_22_2_SSSP_In_DAGs
import CLRSLean.FourthEdition.Chapter_22.Section_22_3_Dijkstra
import CLRSLean.FourthEdition.Chapter_22.Section_22_4_Difference_Constraints
import CLRSLean.FourthEdition.Chapter_22.Section_22_5_Shortest_Path_Properties
import CLRSLean.FourthEdition.Chapter_22.Section_22_5_Shortest_Path_Properties.PredecessorTree

Current source

Sections 22.1--22.5 are native fourth-edition sections (Bellman–Ford, SSSP in DAGs, Dijkstra, difference constraints, and the shortest-path property proofs), imported directly from Section 22.1, Section 22.2, Section 22.3, Section 22.4, and Section 22.5. Declarations retain the legacy CLRS.Chapter24 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_24 and CLRSLean.Chapter_24.Section_24_* forward to these sources.

Coverage boundary

Bellman–Ford proves synchronous distance correctness under global NoNegCycle; it does not return failure for source-reachable negative cycles or weaken the premise to source-relative absence. DAG shortest paths require a supplied complete topological order. Dijkstra proves its mathematical loop under nonnegative edge weights; its binary-heap budget is an independent backend formula, not a measured concrete priority-queue execution. The vertex/edge and round/edge formulas likewise do not imply stored-table reuse.

Difference constraints use a fresh source reaching every variable, so global negative-cycle absence is appropriate for their feasibility equivalence. The old independently minimizing predecessor selector proves tight edges only; zero-weight cycles show why a separate decreasing-depth parent construction is required for a source-rooted shortest-path tree. The new shortestPathTree computes distances, constructs the tight-edge graph, and returns its actual BFS parents and depths. shortestPathTree_correct proves source-rooted weighted shortest paths and coverage; strictly decreasing depths prove acyclicity even with zero-weight cycles. This classical construction adds no runtime claim.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 22 of 35

22.1. The Bellman-Ford Algorithm

Walks and their weights

The Bellman-Ford relaxation dynamic program

No negative cycles and cycle removal

Correctness of Bellman-Ford (CLRS Theorem 22.4)

Work bound: O(V·E)

22.2. Single-Source Shortest Paths in DAGs

Topological order and acyclicity over the weighted graph

Single-vertex out-edge relaxation

The topological-order relaxation pass

Correctness: the folded distances are the shortest-path distances

Work bound: Θ(V + E)

Definitions and proofs

CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

22.3. Dijkstra's Algorithm

Nonnegative weights

Crossing the settled frontier

The greedy invariant (CLRS Theorem 22.6)

Work bound: O(E log V)

Executable priority-queue loop

Initial invariant and final correctness

22.4. Difference Constraints and Shortest Paths

Difference constraint systems

Potential-function lemma

Triangle inequality for Bellman-Ford

22.5. Proofs of Shortest Paths

Main results

The single-source shortest-path distance

Triangle inequality (Lemma 22.11)

Triangle inequality along a walk

Subpath property (Lemma 22.10)

Convergence and path relaxation (Lemmas 22.14-22.15)

Predecessor subgraph (Lemma 22.16)

Definitions and proofs

CLRSLean.FourthEdition.Chapter_22.Section_22_5_Shortest_Path_Properties.PredecessorTree

Constructed shortest-path predecessor trees

Scope and implementation notes

Current source

Coverage boundary

Work bound: `O(V·E)`

Work bound: `Θ(V + E)`

Work bound: `O(E log V)`