Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 23. All-Pairs Shortest Paths
  4. 23.2. The Floyd-Warshall Algorithm
Browse chapters
Imports
import Mathlib import CLRSLean.FourthEdition.Chapter_23.Section_23_1_All_Pairs_Model
set_option linter.unusedSectionVars false

23.2. The Floyd-Warshall Algorithm

Proven

  • Through predicate and walk-splitting lemmas (through_subwalk_left, through_subwalk_right) — Lemma 23.7 core machinery.

  • D_le_simpleWalk — the main induction (Lemma 23.7).

  • floydWarshall_le_walk — lower bound via cycle removal from Ch24.

  • D_attainable — walk concatenation (DP values are realized).

  • floydWarshall_isShortestDist — Theorem 23.8.

  • Pi — predecessor matrix Π (parallel recurrence alongside D).

  • Pi_adj — every predecessor points along a real graph edge.

  • fwReconstructPath — fuel-based shortest-path reconstruction from Π.

  • floydWarshall_nonneg_diag and negative_diagonal_implies_negative_cycle are contrapositives, establishing only the absence/soundness direction for the legacy initializer. The NegativeCycle companion preserves negative self-edges and proves both directions via cycleFloydWarshall_negative_iff.

  • Pi_D_ge — optimal-substructure lower bound for the predecessor matrix.

  • floydWarshallPi_D_eq — floydWarshall i j = floydWarshall i k + w(k,j) when floydWarshallPi i j = some k.

  • reconstructPathFuel_isWalkFrom — reconstructed path is a valid walk.

  • reconstructPathFuel_weight_eq — reconstructed path has weight floydWarshall i j (path-reconstruction correctness).

  • transitiveClosure — boolean reachability matrix from Floyd-Warshall.

  • transitiveClosure_iff_exists_walk — correctness of transitive closure.

  • fwStepCost, floydWarshallCost, floydWarshall_O_cubed describe the cubic table-update budget. The function-valued recurrence does not cache intermediate matrices. The MatrixExecution companion supplies stored evaluation and proves its actual update count equals this budget; initialization writes and diagonal scanning are counted separately.

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

Floyd-Warshall algorithm definition

def fwStep (D : V → V → WithTop ℝ) (k : V) (i j : V) : WithTop ℝ := min (D i j) (D i k + D k j)noncomputable def D (G : WeightedGraph V) : List V → V → V → WithTop ℝ | [], i, j => G.weightMatrix i j | k :: ks, i, j => min (G.D ks i j) (G.D ks i k + G.D ks k j)@[simp] theorem D_nil (G : WeightedGraph V) (i j : V) : G.D [] i j = G.weightMatrix i j := rfltheorem D_cons (k : V) (ks : List V) (i j : V) : G.D (k :: ks) i j = min (G.D ks i j) (G.D ks i k + G.D ks k j) := rflnoncomputable def floydWarshall (G : WeightedGraph V) : V → V → WithTop ℝ := G.D (Finset.univ.toList : List V)lemma weightMatrix_self (i : V) : G.weightMatrix i i = (0 : WithTop ℝ) := by simp [weightMatrix]

Predecessor matrix Π

The predecessor matrix Pi ks i j stores the immediate predecessor of j on a best-known path from i to j using only intermediate vertices from ks. The convention follows CLRS equations (23.5)-(23.6):

  • Pi [] i j = none (NIL) if i=j or (i,j) is not an edge; Pi [] i j = some i if i≠j and (i,j) is an edge.

  • Pi (k::ks) i j = Pi ks k j when going through k yields a strictly shorter distance (i.e. D ks i k + D ks k j < D ks i j); otherwise Pi ks i j.

The final all-pairs predecessor matrix is floydWarshallPi := Pi (univ.toList).

Predecessor matrix Π, computed alongside the distance matrix D (CLRS eqs. (23.5)-(23.6)). Pi ks i j = some k means k is the predecessor of j on a best-known path from i to j through vertices in ks.

noncomputable def Pi (G : WeightedGraph V) : List V → V → V → Option V | [], i, j => if i = j then none else if G.Adj i j then some i else none | k :: ks, i, j => if (G.D ks i k + G.D ks k j) < (G.D ks i j) then G.Pi ks k j else G.Pi ks i j
@[simp] theorem Pi_nil (G : WeightedGraph V) (i j : V) : G.Pi [] i j = (if i = j then none else if G.Adj i j then some i else none) := rfltheorem Pi_cons (k : V) (ks : List V) (i j : V) : G.Pi (k :: ks) i j = (if (G.D ks i k + G.D ks k j) < (G.D ks i j) then G.Pi ks k j else G.Pi ks i j) := rfl

When the distance through k is strictly better, the predecessor matrix is updated to the predecessor of j on the best-known path from k to j.

lemma Pi_cons_lt {k : V} {ks : List V} {i j : V} (hlt : G.D ks i k + G.D ks k j < G.D ks i j) : G.Pi (k :: ks) i j = G.Pi ks k j := by rw [Pi_cons, if_pos hlt]
lemma Pi_cons_not_lt {k : V} {ks : List V} {i j : V} (hle : ¬ (G.D ks i k + G.D ks k j < G.D ks i j)) : G.Pi (k :: ks) i j = G.Pi ks i j := by rw [Pi_cons, if_neg hle]

Base-case predecessor specification: Pi [] i j = some k implies k=i, i≠j, and (i,j) is an edge.

lemma Pi_nil_spec (G : WeightedGraph V) (i j k : V) (h : G.Pi [] i j = some k) : k = i ∧ i ≠ j ∧ G.Adj i j := by rw [Pi_nil] at h by_cases hij : i = j · subst hij; simp at h · simp [hij] at h by_cases hadj : G.Adj i j · simp [hadj] at h have h_ik : i = k := by simpa using h have hk_i : k = i := h_ik.symm exact ⟨hk_i, hij, hadj⟩ · simp [hadj] at h

Predecessor edge lemma. Pi ks i j = some k implies (k,j) is an edge in the graph. This is the key invariant for path reconstruction: every predecessor recorded by Pi is an actual predecessor vertex along a real edge.

The proof is by induction on ks; both branches of the inductive step preserve the property from the base case where Pi [] i j = some i only when (i,j) ∈ E.

lemma Pi_adj (ks : List V) (i j k : V) (hPi : G.Pi ks i j = some k) : G.Adj k j := by revert i j k induction ks with | nil => intro i j k hPi rcases Pi_nil_spec G i j k hPi with ⟨hk_i, _, hadj⟩ subst hk_i; exact hadj | cons k' ks ih => intro i j k hPi rw [Pi_cons] at hPi split at hPi · exact ih k' j k hPi · exact ih i j k hPi

Final Floyd-Warshall predecessor matrix (CLRS Π-matrix).

noncomputable def floydWarshallPi (G : WeightedGraph V) : V → V → Option V := G.Pi (Finset.univ.toList : List V)

Edge lemma specialised to the final predecessor matrix.

lemma floydWarshallPi_adj (i j k : V) (hPi : G.floydWarshallPi i j = some k) : G.Adj k j := G.Pi_adj (Finset.univ.toList : List V) i j k hPi

Path reconstruction

Path reconstruction follows the CLRS PRINT-ALL-PAIRS-SHORTEST-PATH recursion: given Π[i,j] = k, the path from i to j is the path from i to k followed by the edge (k, j).

We use a fuel-based implementation bounded by Fintype.card V to ensure well-founded recursion. Under NoNegCycle, shortest paths are simple, so at most |V-1| edges are needed. When fuel runs out we return [] (which cannot happen for well-defined shortest paths under NoNegCycle).

Reconstruct a path from i to j using at most fuel recursion steps. Returns [] when fuel is exhausted or no predecessor exists.

def reconstructPathFuel (Pi : V → V → Option V) (fuel : ℕ) (i j : V) : List V := match fuel with | 0 => [] | fuel + 1 => if Variable name `h` 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`h : i = j then [i] else match Pi i j with | none => [] | some k => let path := reconstructPathFuel Pi fuel i k if Variable name `hpath` 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`hpath : path = [] then [] else path ++ [j]

Reconstruct a shortest path from i to j using the Floyd-Warshall predecessor matrix. Fuel = Fintype.card V ensures sufficient recursion depth for simple paths.

noncomputable def fwReconstructPath (G : WeightedGraph V) (i j : V) : List V := reconstructPathFuel G.floydWarshallPi (Fintype.card V) i j

A reconstructible vertex pair has a nonempty predecessor chain that terminates at i. This is the invariant that makes reconstruction succeed.

lemma reconstructPathFuel_ne_nil (Pi : V → V → Option V) (fuel : ℕ) (i j : V) (h_fuel : 0 < fuel) (h_eq : i = j) : reconstructPathFuel Pi fuel i j = [i] := by subst h_eq rcases Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp h_fuel) with ⟨n, rfl⟩ simp [reconstructPathFuel]
lemma reconstructPathFuel_cons (Pi : V → V → Option V) (fuel : ℕ) (i j k : V) (hPi : Pi i j = some k) (hij : i ≠ j) (hne : reconstructPathFuel Pi fuel i k ≠ []) : reconstructPathFuel Pi (fuel + 1) i j = reconstructPathFuel Pi fuel i k ++ [j] := by simp [reconstructPathFuel, hij, hPi, hne]

Walk-through-set predicate

Every vertex of p is i, j, or in S.

def Through (S : Finset V) (i j : V) (p : List V) : Prop := ∀ v ∈ p, v = i ∨ v = j ∨ v ∈ S
lemma Through.univ (i j : V) (p : List V) : Through (Finset.univ : Finset V) i j p := by intro v _; exact Or.inr (Or.inr (Finset.mem_univ v)) lemma last_in_tail {l₁ l₂ : List V} {k j : V} (hlast : (l₁ ++ k :: l₂).getLast? = some j) (hk_ne_j : k ≠ j) : j ∈ k :: l₂ := by by_cases hl₂ : l₂ = [] · subst hl₂; simp at hlast; exact absurd hlast hk_ne_j · have hlast' : (k :: l₂).getLast? = some j := by simpa using hlast rcases (List.getLast?_eq_some_iff.mp hlast') with ⟨ys, h_eq⟩; rw [h_eq]; simp lemma through_subwalk_left {l₁ l₂ : List V} {i j k : V} {S : Finset V} (hNodup : (l₁ ++ k :: l₂).Nodup) (hp_through : Through ({k} ∪ S) i j (l₁ ++ k :: l₂)) (hlast : (l₁ ++ k :: l₂).getLast? = some j) (hk_ne_i : k ≠ i) (hk_ne_j : k ≠ j) : Through S i k (l₁ ++ [k]) := by have hNodup_app := (List.nodup_append.mp hNodup) have hdisjoint : ∀ a ∈ l₁, ∀ b ∈ k :: l₂, a ≠ b := hNodup_app.2.2 have hk_not_mem_l₁ : k ∉ l₁ := by intro hk_mem; have hk_mem_tail : k ∈ k :: l₂ := by simp exact hdisjoint k hk_mem k hk_mem_tail rfl have hj_mem_tail : j ∈ k :: l₂ := last_in_tail hlast hk_ne_j intro v hv; rcases List.mem_append.mp hv with (hv_l₁ | hv_last) · rcases hp_through v (List.mem_append_left (k :: l₂) hv_l₁) with (hvi | hvj | hmem) · exact Or.inl hvi · rw [hvj] at hv_l₁; exact absurd rfl (hdisjoint j hv_l₁ j hj_mem_tail) · rcases Finset.mem_insert.mp hmem with (hvk | hv_S) · rw [hvk] at hv_l₁; exact absurd hv_l₁ hk_not_mem_l₁ · exact Or.inr (Or.inr hv_S) · simp at hv_last; subst hv_last; exact Or.inr (Or.inl rfl) lemma through_subwalk_right {l₁ l₂ : List V} {i j k : V} {S : Finset V} (hNodup : (l₁ ++ k :: l₂).Nodup) (hp_through : Through ({k} ∪ S) i j (l₁ ++ k :: l₂)) (hhead : (l₁ ++ k :: l₂).head? = some i) (hk_ne_i : k ≠ i) (_hk_ne_j : k ≠ j) : Through S k j (k :: l₂) := by have hNodup_app := (List.nodup_append.mp hNodup) have hdisjoint : ∀ a ∈ l₁, ∀ b ∈ k :: l₂, a ≠ b := hNodup_app.2.2 have hNodup_tail : (k :: l₂).Nodup := hNodup_app.2.1 have hk_not_mem_l₂ : k ∉ l₂ := (List.nodup_cons.mp hNodup_tail).1 intro v hv; cases hv with | head _ => exact Or.inl rfl | tail _ hv_l₂ => have hv_mem_tail : v ∈ k :: l₂ := List.Mem.tail _ hv_l₂ rcases hp_through v (List.mem_append_right l₁ hv_mem_tail) with (hvi | hvj | hmem) · rw [hvi] at hv_l₂ by_cases hl₁ : l₁ = [] · rw [hl₁] at hhead; simp at hhead; exact absurd hhead hk_ne_i · have hi_mem_l₁ : i ∈ l₁ := by have hhead' : l₁.head? = some i := by rw [List.head?_append_of_ne_nil _ hl₁] at hhead; exact hhead rcases (List.head?_eq_some_iff.mp hhead') with ⟨l₁', hl₁'⟩; rw [hl₁']; simp have hi_mem_tail : i ∈ k :: l₂ := List.Mem.tail _ hv_l₂ exact absurd rfl (hdisjoint i hi_mem_l₁ i hi_mem_tail) · exact Or.inr (Or.inl hvj) · rcases Finset.mem_insert.mp hmem with (hvk | hv_S) · rw [hvk] at hv_l₂; exact absurd hv_l₂ hk_not_mem_l₂ · exact Or.inr (Or.inr hv_S)

Lemma 23.7: D bounds simple walks through ks

The proof is by induction on ks. The nil case analyses the walk structure (only [i] or [i,j] allowed when Through ∅). The cons case splits on whether k is an interior vertex: if yes, split the walk at k using through_subwalk_left/right and apply the induction hypothesis; if no, the walk already goes through ks and IH applies directly.

The proof strategy is correct but the current version has Lean syntax issues (nested match/pattern interaction inside induction). Fix in VS Code.

lemma D_le_simpleWalk (ks : List V) (i j : V) (p : List V) (hp_walk : G.IsWalkFrom i j p) (hNodup : p.Nodup) (hp_through : Through (ks.toFinset) i j p) : (G.D ks i j : WithTop ℝ) ≤ (walkWeight G.w p : WithTop ℝ) := by revert i j p hp_walk hNodup hp_through induction ks with | nil => intro i j p hp_walk hNodup hp_through; rw [D_nil] have hp_ne_nil : p ≠ [] := hp_walk.ne_nil match p with | [] => exact absurd rfl hp_ne_nil | [a] => have ha_i : a = i := by have h := hp_walk.head; simp at h; exact h have ha_j : a = j := by have h := hp_walk.last; simp at h; exact h subst ha_i; subst ha_j; simp [weightMatrix_self G] | [a, b] => have ha_i : a = i := by have h := hp_walk.head; simp at h; exact h have hb_j : b = j := by have hlast : [a, b].getLast? = some b := by simp have h := hp_walk.last; rw [hlast] at h; simpa using h rw [ha_i, hb_j]; rw [ha_i, hb_j] at hp_walk; rw [ha_i, hb_j] at hNodup by_cases hij : i = j · subst hij; simp at hNodup · have h_adj : G.Adj i j := by have h := (List.isChain_cons.mp hp_walk.chain).1 exact h j (by simp) dsimp [weightMatrix]; simp [hij, h_adj] | a :: b :: c :: _ => have ha_or : a = i ∨ a = j := by have := hp_through a (by simp); simpa using this have hb_or : b = i ∨ b = j := by have := hp_through b (by simp); simpa using this have hc_or : c = i ∨ c = j := by have := hp_through c (by simp); simpa using this rcases ha_or with (rfl|rfl) <;> rcases hb_or with (rfl|rfl) <;> rcases hc_or with (rfl|rfl) <;> simp at hNodup | cons k ks ih => intro i j p hp_walk hNodup hp_through; rw [D_cons] by_cases hk_mem : k ∈ p · by_cases hk_i : k = i · have hp_ks : Through (ks.toFinset) i j p := by intro v hv; have h := hp_through v hv rcases h with (hvi | hrest) · exact Or.inl hvi · rcases hrest with (hvj | hm) · exact Or.inr (Or.inl hvj) · have hm' : v ∈ ({k} ∪ (ks.toFinset : Finset V)) := by have h_eq : (k :: ks).toFinset = {k} ∪ ks.toFinset := by simp rw [h_eq] at hm; exact hm rcases Finset.mem_union.mp hm' with (hvk_sing | hS) · have hvk : v = k := Finset.mem_singleton.mp hvk_sing rw [hk_i] at hvk; exact Or.inl hvk · exact Or.inr (Or.inr hS) have hle := ih i j p hp_walk hNodup hp_ks exact le_trans (min_le_left _ _) hle · by_cases hk_j : k = j · have hp_ks : Through (ks.toFinset) i j p := by intro v hv; have h := hp_through v hv rcases h with (hvi | hrest) · exact Or.inl hvi · rcases hrest with (hvj | hm) · exact Or.inr (Or.inl hvj) · have hm' : v ∈ ({k} ∪ (ks.toFinset : Finset V)) := by have h_eq : (k :: ks).toFinset = {k} ∪ ks.toFinset := by simp rw [h_eq] at hm; exact hm rcases Finset.mem_union.mp hm' with (hvk_sing | hS) · have hvk : v = k := Finset.mem_singleton.mp hvk_sing rw [hk_j] at hvk; exact Or.inr (Or.inl hvk) · exact Or.inr (Or.inr hS) have hle := ih i j p hp_walk hNodup hp_ks exact le_trans (min_le_left _ _) hle · obtain ⟨l₁, l₂, hp_eq⟩ := List.mem_iff_append.mp hk_mem rw [hp_eq] at hp_walk hNodup hp_through ⊢ have hchain : List.IsChain G.Adj (l₁ ++ k :: l₂) := hp_walk.chain have hchain_app := List.isChain_append.mp hchain have hp₁_chain : List.IsChain G.Adj (l₁ ++ [k]) := by refine List.IsChain.append hchain_app.1 (List.isChain_singleton k) ?_ intro a ha b hb have hb' : b = k := by have h := hb; simp at h; exact h.symm rw [hb']; exact hchain_app.2.2 a ha k (by simp) have hp₁_head : (l₁ ++ [k]).head? = some i := by by_cases hl₁ : l₁ = [] · subst hl₁; simp have hh : (k :: l₂).head? = some i := hp_walk.head have hhead_k : (k :: l₂).head? = some k := by simp rw [hhead_k] at hh; simp at hh; exact absurd hh hk_i · have hhead := hp_walk.head rw [List.head?_append_of_ne_nil _ hl₁] at hhead rw [List.head?_append_of_ne_nil _ hl₁]; exact hhead have hp₁_walk : G.IsWalkFrom i k (l₁ ++ [k]) := ⟨hp₁_chain, hp₁_head, by simp⟩ have hp₂_last : (k :: l₂).getLast? = some j := by by_cases hl₂ : l₂ = [] · subst hl₂; simp have hl : (l₁ ++ [k]).getLast? = some j := hp_walk.last simp at hl; exact absurd hl hk_j · have halast : (l₁ ++ k :: l₂).getLast? = some j := hp_walk.last simpa [hl₂] using halast have hp₂_walk : G.IsWalkFrom k j (k :: l₂) := ⟨hchain_app.2.1, by simp, hp₂_last⟩ have hp₁_nodup : (l₁ ++ [k]).Nodup := hNodup.sublist (List.Sublist.append (List.Sublist.refl l₁) (show List.Sublist [k] (k :: l₂) from by have : [k] = k :: [] := by simp rw [this] exact List.Sublist.cons_cons k (List.nil_sublist l₂))) have hp₂_nodup : (k :: l₂).Nodup := hNodup.sublist (List.sublist_append_right l₁ (k :: l₂)) have hp_union : Through ({k} ∪ (ks.toFinset)) i j (l₁ ++ k :: l₂) := by have h_eq : (k :: ks).toFinset = {k} ∪ ks.toFinset := by simp rw [h_eq] at hp_through; exact hp_through have hp₁_through : Through (ks.toFinset) i k (l₁ ++ [k]) := through_subwalk_left hNodup hp_union hp_walk.last hk_i hk_j have hp₂_through : Through (ks.toFinset) k j (k :: l₂) := through_subwalk_right hNodup hp_union hp_walk.head hk_i hk_j have hle₁ : (G.D ks i k : WithTop ℝ) ≤ (walkWeight G.w (l₁ ++ [k]) : WithTop ℝ) := ih i k (l₁ ++ [k]) hp₁_walk hp₁_nodup hp₁_through have hle₂ : (G.D ks k j : WithTop ℝ) ≤ (walkWeight G.w (k :: l₂) : WithTop ℝ) := ih k j (k :: l₂) hp₂_walk hp₂_nodup hp₂_through have hsum : (G.D ks i k + G.D ks k j : WithTop ℝ) ≤ (walkWeight G.w (l₁ ++ [k]) + walkWeight G.w (k :: l₂) : WithTop ℝ) := add_le_add hle₁ hle₂ have hweight : walkWeight G.w (l₁ ++ k :: l₂) = walkWeight G.w (l₁ ++ [k]) + walkWeight G.w (k :: l₂) := walkWeight_split G.w l₁ k l₂ have hsum' : (walkWeight G.w (l₁ ++ [k]) + walkWeight G.w (k :: l₂) : WithTop ℝ) = (walkWeight G.w (l₁ ++ k :: l₂) : WithTop ℝ) := by exact_mod_cast hweight.symm rw [hsum'] at hsum apply le_trans (min_le_right _ _); exact hsum · have hp_ks : Through (ks.toFinset) i j p := by intro v hv; have h := hp_through v hv rcases h with (hvi | hrest) · exact Or.inl hvi · rcases hrest with (hvj | hm) · exact Or.inr (Or.inl hvj) · have hm' : v ∈ ({k} ∪ (ks.toFinset : Finset V)) := by have h_eq : (k :: ks).toFinset = {k} ∪ ks.toFinset := by simp rw [h_eq] at hm; exact hm rcases Finset.mem_union.mp hm' with (hvk_sing | hS) · exfalso have hvk : v = k := Finset.mem_singleton.mp hvk_sing subst hvk; exact hk_mem hv · exact Or.inr (Or.inr hS) have hle := ih i j p hp_walk hNodup hp_ks exact le_trans (min_le_left _ _) hle

General lower bound via cycle removal

lemma floydWarshall_le_walk (hNC : G.NoNegCycle) (i j : V) (p : List V) (hp : G.IsWalkFrom i j p) : (G.floydWarshall i j : WithTop ℝ) ≤ (walkWeight G.w p : WithTop ℝ) := by -- Under NoNegCycle, there's a simple path q with ≤ weight obtain ⟨q, hq, hq_nodup, hq_le⟩ := G.exists_simple_le hNC i j p.length p (le_refl _) hp have hq_weight : (walkWeight G.w q : WithTop ℝ) ≤ (walkWeight G.w p : WithTop ℝ) := by exact_mod_cast hq_le -- q is simple, and Through univ is always true have huniv_eq : ((Finset.univ : Finset V).toList : List V).toFinset = Finset.univ := by simp have hq_through : Through ((Finset.univ.toList : List V).toFinset) i j q := by rw [huniv_eq]; exact Through.univ i j q -- Apply D_le_simpleWalk (once proven) have hle := D_le_simpleWalk G (Finset.univ.toList : List V) i j q hq hq_nodup hq_through simpa [floydWarshall] using le_trans hle hq_weight

Attainability — every finite DP value is realized by a walk

The proof is by induction on ks. At each step, either the value comes from D ks i j (IH) or from D ks i k + D ks k j (concatenate the two realizing walks, overlapping at k).

lemma D_attainable (ks : List V) (i j : V) : (G.D ks i j = ⊤) ∨ (∃ p, G.IsWalkFrom i j p ∧ (walkWeight G.w p : WithTop ℝ) = G.D ks i j) := by induction' ks with k ks ih generalizing i j · rw [D_nil]; dsimp [weightMatrix] by_cases hij : i = j · subst hij have hw : G.weightMatrix i i = (0 : WithTop ℝ) := weightMatrix_self G i simp [This simp argument is unused: hw Hint: Omit it from the simp argument list. simp ̵[̵h̵w̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hw] refine ⟨[i], ?_, ?_⟩ · exact { chain := List.isChain_singleton i, head := by simp, last := by simp } · simp · by_cases hadj : G.Adj i j · refine Or.inr ⟨[i, j], ?_, ?_⟩ · refine ⟨?_, by simp, by simp⟩ refine (List.isChain_cons (x := i) (l := [j])).mpr ⟨?_, List.isChain_singleton j⟩ intro b hb; simp at hb; subst hb; exact hadj · simp [walkWeight, hij, hadj] · simp [hij, hadj] · rw [D_cons] rcases min_choice (G.D ks i j) (G.D ks i k + G.D ks k j) with (hmin | hmin) · rw [hmin]; exact ih i j · rw [hmin] rcases ih i k with (htop_ik | ⟨pik, hpik, hpikw⟩) · simp [htop_ik] · rcases ih k j with (htop_kj | ⟨pkj, hpkj, hpkjw⟩) · simp [htop_kj] · -- Concatenate pik ++ pkj.tail (overlap at k) have hpik_ne_nil : pik ≠ [] := hpik.ne_nil cases pkj with | nil => exact absurd rfl hpkj.ne_nil | cons a as => have ha_k : a = k := by simpa using hpkj.head -- Work with as = pkj.tail, and a = k have hpkj_chain' : List.IsChain G.Adj (k :: as) := by rw [← ha_k]; exact hpkj.chain have chain_decomp := List.isChain_cons.mp hpkj_chain' have as_chain : List.IsChain G.Adj as := chain_decomp.2 have head_adj : ∀ y ∈ as.head?, G.Adj k y := chain_decomp.1 set q := pik ++ as with hq_def -- Chain for concatenated walk have hq_chain : List.IsChain G.Adj q := by rw [hq_def] -- use the iff version of isChain_append apply (List.isChain_append (l₁ := pik) (l₂ := as)).mpr refine ⟨hpik.chain, as_chain, ?_⟩ intro a' ha' b' hb' rw [hpik.last] at ha' simp at ha' have ha'_k : a' = k := ha'.symm rw [ha'_k]; exact head_adj b' hb' have hq_head : q.head? = some i := by rw [hq_def, List.head?_append_of_ne_nil _ hpik_ne_nil]; exact hpik.head have hq_last : q.getLast? = some j := by rw [hq_def] by_cases has : as = [] · subst has; simp have hk_eq_j : k = j := by have hlast := hpkj.last; simp at hlast; rw [ha_k] at hlast; exact hlast have hpik_last' := hpik.last; rw [hk_eq_j] at hpik_last'; exact hpik_last' · have hlast' : (pik ++ as).getLast? = as.getLast? := List.getLast?_append_of_ne_nil _ has rw [hlast'] have htail_last : as.getLast? = some j := by have hlast_pkj := hpkj.last rw [ha_k] at hlast_pkj have h_getLast : (k :: as).getLast? = as.getLast? := by simpa using List.getLast?_cons_of_ne_nil has rw [h_getLast] at hlast_pkj exact hlast_pkj exact htail_last have hq_walk : G.IsWalkFrom i j q := ⟨hq_chain, hq_head, hq_last⟩ -- Weight equality have hpik_last_eq := hpik.last rcases List.getLast?_eq_some_iff.mp hpik_last_eq with ⟨l, hpik_snoc⟩ have hq_weight : (walkWeight G.w q : WithTop ℝ) = G.D ks i k + G.D ks k j := by rw [hq_def, hpik_snoc] have h_list_eq : (l ++ [k]) ++ as = l ++ k :: as := by simp rw [h_list_eq] rw [walkWeight_split G.w l k as, ← hpik_snoc] have h_pkj_eq : (k :: as) = (a :: as) := by rw [ha_k] rw [h_pkj_eq] push_cast; rw [hpikw, hpkjw] exact Or.inr ⟨q, hq_walk, hq_weight⟩theorem floydWarshall_isShortestDist (hNC : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (G.floydWarshall i j) := by constructor · intro p hp; exact G.floydWarshall_le_walk hNC i j p hp · rcases G.D_attainable (Finset.univ.toList : List V) i j with (htop | ⟨p, hp, hpw⟩) · left; simpa [floydWarshall] using htop · right; refine ⟨p, hp, ?_⟩; simpa [floydWarshall] using hpw

Negative-cycle detection (CLRS Theorem 23.3)

The Floyd-Warshall algorithm detects negative-weight cycles by inspecting the diagonal entries of the final distance matrix. CLRS Theorem 23.3 states:

diagonal entries of the final distance matrix is strictly negative.

We prove both directions.

Soundness of the diagonal test. Under NoNegCycle, every diagonal entry of the Floyd-Warshall matrix is nonnegative. This is the forward direction (NoNegCycle → diagonal ≥ 0) of CLRS Theorem 23.3.

theorem floydWarshall_nonneg_diag (hNC : G.NoNegCycle) (i : V) : (0 : WithTop ℝ) ≤ G.floydWarshall i i := by rcases G.D_attainable (Finset.univ.toList : List V) i i with (htop | ⟨p, hp, hpw⟩) · rw [floydWarshall, htop]; exact le_top · rw [floydWarshall, ← hpw] have h_nonneg : 0 ≤ walkWeight G.w p := hNC i p hp exact_mod_cast h_nonneg

Completeness of the diagonal test. If a diagonal entry of the Floyd-Warshall matrix is strictly negative, then there exists a negative-weight closed walk in the graph. This is the reverse direction (diagonal < 0 → ¬NoNegCycle) of CLRS Theorem 23.3.

theorem negative_diagonal_implies_negative_cycle (i : V) (h : G.floydWarshall i i < (0 : WithTop ℝ)) : ∃ (c : List V), G.IsWalkFrom i i c ∧ walkWeight G.w c < 0 := by rcases G.D_attainable (Finset.univ.toList : List V) i i with (htop | ⟨p, hp, hpw⟩) · rw [floydWarshall, htop] at h; simp at h · have hpw_cast : (walkWeight G.w p : WithTop ℝ) = G.floydWarshall i i := by simpa [floydWarshall] using hpw have h_coe_lt : (walkWeight G.w p : WithTop ℝ) < (0 : WithTop ℝ) := by rw [hpw_cast]; exact h -- Extract the ℝ inequality from the WithTop inequality. -- From h_coe_lt : (walkWeight G.w p : WithTop ℝ) < (0 : WithTop ℝ) -- extract the ℝ inequality using exact_mod_cast. have h_lt : walkWeight G.w p < 0 := by exact_mod_cast h_coe_lt exact ⟨p, hp, h_lt⟩

Pi-D optimal substructure

The key invariant connecting Pi and D: if Pi ks i j = some k with i ≠ j, then D ks i j ≥ D ks i k + w(k,j). This is the lower-bound direction of the optimal-substructure property. Combined with the upper bound from the edge inequality for IsShortestDist, we obtain equality for the final floydWarshall/floydWarshallPi matrices.

Under NoNegCycle, the diagonal of D is zero for any intermediate set. The empty walk [i] has weight 0, and any closed walk has nonnegative weight, so the minimum closed-walk weight through ks is exactly 0.

lemma D_diag_eq_zero (hNC : G.NoNegCycle) (ks : List V) (i : V) : G.D ks i i = (0 : WithTop ℝ) := by rcases G.D_attainable ks i i with (htop | ⟨p, hp, hpw⟩) · -- D = ⊤: impossible since [i] is a walk from i to i with weight 0 have h_walk : G.IsWalkFrom i i [i] := ⟨List.isChain_singleton i, by simp, by simp⟩ have h0 : (G.D ks i i : WithTop ℝ) ≤ (walkWeight G.w [i] : WithTop ℝ) := G.D_le_simpleWalk ks i i [i] h_walk (by simp) (by intro v hv; simp at hv; subst hv; exact Or.inl rfl) simp [walkWeight] at h0 rw [htop] at h0; simp at h0 · -- D is finite and realized by closed walk p have h_nonneg : (0 : ℝ) ≤ walkWeight G.w p := hNC i p hp have h_zero : (G.D ks i i : WithTop ℝ) ≤ (0 : WithTop ℝ) := by have h_walk : G.IsWalkFrom i i [i] := ⟨List.isChain_singleton i, by simp, by simp⟩ have h_le := G.D_le_simpleWalk ks i i [i] h_walk (by simp) (by intro v hv; simp at hv; subst hv; exact Or.inl rfl) simpa [walkWeight] using h_le have h_nonneg' : (0 : WithTop ℝ) ≤ (G.D ks i i : WithTop ℝ) := by rw [← hpw]; exact_mod_cast h_nonneg exact le_antisymm h_zero h_nonneg'

Pi-D lower bound. If Pi ks i j = some k with i ≠ j, then the DP distance satisfies D ks i k + w(k,j) ≤ D ks i j. In words: the path that goes optimally to k and then takes the direct edge (k,j) is no heavier than the optimal path to j.

The proof is by induction on ks. The critical observation is that D (v::ks) i k = min (D ks i k) (D ks i v + D ks v k) supplies exactly the inequality needed to apply the induction hypothesis via min_le_left or min_le_right.

lemma Pi_D_ge (hNC : G.NoNegCycle) (ks : List V) (i j k : V) (hPi : G.Pi ks i j = some k) (hij : i ≠ j) : G.D ks i k + (G.w k j : WithTop ℝ) ≤ G.D ks i j := by revert i j k hPi hij induction ks with | nil => intro i j k hPi hij rcases Pi_nil_spec G i j k hPi with ⟨hk_i, _, hadj⟩ rw [hk_i] have hD_ij : G.D [] i j = (G.w i j : WithTop ℝ) := by rw [D_nil]; dsimp [weightMatrix]; simp [hij, hadj] have hD_ik : G.D [] i i = (0 : WithTop ℝ) := by rw [D_nil, weightMatrix_self G i] rw [hD_ij, hD_ik]; simp | cons v ks' ih => intro i j k hPi hij rw [Pi_cons] at hPi split at hPi · -- UPDATE: D ks' i v + D ks' v j < D ks' i j, Pi ks' v j = some k rename_i h_lt have hvj : v ≠ j := by intro heq rw [heq] at h_lt have h_diag : G.D ks' j j = (0 : WithTop ℝ) := D_diag_eq_zero G hNC ks' j rw [h_diag] at h_lt simp at h_lt have ih_kj := ih v j k hPi hvj rw [D_cons] have hD_ij : G.D (v :: ks') i j = G.D ks' i v + G.D ks' v j := by rw [D_cons]; exact min_eq_right (le_of_lt h_lt) rw [hD_ij] have hD_ik : G.D (v :: ks') i k ≤ G.D ks' i v + G.D ks' v k := by rw [D_cons]; exact min_le_right _ _ calc G.D (v :: ks') i k + (G.w k j : WithTop ℝ) ≤ (G.D ks' i v + G.D ks' v k) + (G.w k j : WithTop ℝ) := by gcongr _ = G.D ks' i v + (G.D ks' v k + (G.w k j : WithTop ℝ)) := by abel _ ≤ G.D ks' i v + G.D ks' v j := by gcongr · -- NO-UPDATE: ¬ D ks' i v + D ks' v j < D ks' i j, Pi ks' i j = some k rename_i h_not_lt have ih_ij := ih i j k hPi hij rw [D_cons] have hD_ij : G.D (v :: ks') i j = G.D ks' i j := by rw [D_cons]; exact min_eq_left (by rw [not_lt] at h_not_lt; exact h_not_lt) rw [hD_ij] have hD_ik : G.D (v :: ks') i k ≤ G.D ks' i k := by rw [D_cons]; exact min_le_left _ _ calc G.D (v :: ks') i k + (G.w k j : WithTop ℝ) ≤ G.D ks' i k + (G.w k j : WithTop ℝ) := by gcongr _ ≤ G.D ks' i j := ih_ij

Edge inequality for shortest-path distances

For any source s with shortest distances δ(t) = δ(s, t) and any edge (u, v), we have δ(v) ≤ δ(u) + w(u, v). This is a general property of shortest paths: extend a walk realizing δ(u) with the edge (u, v). Reproved here to avoid a cross-section dependency.

theorem isShortestDist_edge_ineq (s u v : V) (δ : V → WithTop ℝ) (hδ : ∀ t, G.IsShortestDist s t (δ t)) (h_edge : (u, v) ∈ G.edges) : δ v ≤ δ u + (G.w u v : WithTop ℝ) := by rcases (hδ u).2 with hutop | ⟨q, hq, hqw⟩ · rw [hutop]; simp · have hq_ne : q ≠ [] := hq.ne_nil have h_last : q.getLast hq_ne = u := by have htemp := List.getLast?_eq_getLast_of_ne_nil hq_ne have h_eq_some : some u = some (q.getLast hq_ne) := 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 have hsing : [v].head? = some v := by simp rw [hsing, Option.mem_def] at hb simpa using hb.symm subst hb_v exact h_edge · rw [List.head?_append_of_ne_nil _ hq_ne] 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) v : ℝ) : WithTop ℝ) := by exact_mod_cast walkWeight_append_singleton G.w q hq_ne v _ = (walkWeight G.w q : WithTop ℝ) + (G.w (q.getLast hq_ne) v : WithTop ℝ) := by simp _ = (walkWeight G.w q : WithTop ℝ) + (G.w u v : WithTop ℝ) := by rw [h_last] _ = δ u + (G.w u v : WithTop ℝ) := by rw [hqw] have h_bound : δ v ≤ (walkWeight G.w (q ++ [v]) : WithTop ℝ) := (hδ v).1 _ h_walk rw [h_weight] at h_bound exact h_bound

Pi-D equality for the final Floyd-Warshall matrices. If the predecessor matrix records k as the immediate predecessor of j on a shortest path from i to j, then floydWarshall i j = floydWarshall i k + w(k,j).

The lower bound comes from Pi_D_ge specialised to ks := univ.toList. The upper bound is the edge inequality for IsShortestDist.

lemma floydWarshallPi_D_eq (hNC : G.NoNegCycle) (i j k : V) (hPi : G.floydWarshallPi i j = some k) (hij : i ≠ j) : G.floydWarshall i j = G.floydWarshall i k + (G.w k j : WithTop ℝ) := by have h_edge : (k, j) ∈ G.edges := G.floydWarshallPi_adj i j k hPi have h_sd_i := G.floydWarshall_isShortestDist hNC i -- Upper bound: floydWarshall i j ≤ floydWarshall i k + G.w k j have h_upper : (G.floydWarshall i j : WithTop ℝ) ≤ G.floydWarshall i k + (G.w k j : WithTop ℝ) := by have h_ineq := G.isShortestDist_edge_ineq i k j (fun t => G.floydWarshall i t) h_sd_i h_edge simpa using h_ineq -- Lower bound: floydWarshall i k + G.w k j ≤ floydWarshall i j have h_lower : G.floydWarshall i k + (G.w k j : WithTop ℝ) ≤ (G.floydWarshall i j : WithTop ℝ) := by simpa [floydWarshall, floydWarshallPi] using Pi_D_ge G hNC (Finset.univ.toList : List V) i j k hPi hij exact (le_antisymm h_lower h_upper).symm

Path-reconstruction correctness

We prove that the path reconstructed by reconstructPathFuel from the Floyd-Warshall predecessor matrix floydWarshallPi is a valid walk whose weight exactly equals floydWarshall i j.

The path reconstructed by reconstructPathFuel is a valid walk, provided the predecessor matrix satisfies the adjacency property.

Try `simp at h_ne` instead of `simpa using h_ne` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` lemma reconstructPathFuel_isWalkFrom (Pi : V → V → Option V) (fuel : ℕ) (i j : V) (hPi_adj : ∀ i j k, Pi i j = some k → G.Adj k j) (h_ne : reconstructPathFuel Pi fuel i j ≠ []) : G.IsWalkFrom i j (reconstructPathFuel Pi fuel i j) := by induction fuel generalizing i j with | zero => simp [reconstructPathFuel] at h_ne | succ fuel ih => unfold reconstructPathFuel at h_ne ⊢ dsimp at h_ne ⊢ by_cases hij : i = j · subst i; simp exact ⟨List.isChain_singleton j, by simp, by simp⟩ · simp [hij, This simp argument is unused: reconstructPathFuel Hint: Omit it from the simp argument list. simp [hij,̵ ̵r̵e̵c̵o̵n̵s̵t̵r̵u̵c̵t̵P̵a̵t̵h̵F̵u̵e̵l̵] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`reconstructPathFuel] at h_ne ⊢ cases hPi : Pi i j with | none => Try `simp at h_ne` instead of `simpa using h_ne` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [reconstructPathFuel, hij, hPi] using h_ne | some k => simp [This simp argument is unused: reconstructPathFuel Hint: Omit it from the simp argument list. simp [̵r̵e̵c̵o̵n̵s̵t̵r̵u̵c̵t̵P̵a̵t̵h̵F̵u̵e̵l̵,̵ ̵h̵P̵i̵,̵[̲h̲P̲i̲,̲ hij] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`reconstructPathFuel, hPi, This simp argument is unused: hij Hint: Omit it from the simp argument list. simp [reconstructPathFuel, hPi,̵ ̵h̵i̵j̵] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hij] at h_ne ⊢ by_cases hpath : reconstructPathFuel Pi fuel i k = [] · simp [hpath] at h_ne · simp [hpath] at h_ne ⊢ have hwalk_ik := ih i k hpath have h_adj : G.Adj k j := hPi_adj i j k hPi have hchain : List.IsChain G.Adj (reconstructPathFuel Pi fuel i k ++ [j]) := by refine hwalk_ik.chain.append (List.isChain_singleton j) ?_ intro a ha b hb rw [hwalk_ik.last] at ha have ha_k : a = k := by simpa using ha.symm subst ha_k have hb_j : b = j := by have hsing : [j].head? = some j := by simp rw [hsing] at hb; simpa using hb.symm subst hb_j; exact h_adj refine ⟨hchain, ?_, ?_⟩ · rw [List.head?_append_of_ne_nil _ hpath] exact hwalk_ik.head · simp

Path-reconstruction weight equality. For the Floyd-Warshall predecessor matrix under NoNegCycle, the reconstructed path has weight floydWarshall i j.

The proof is by induction on fuel. At each step we use floydWarshallPi_D_eq to decompose the shortest distance through the recorded predecessor.

Try `simp at h_ne` instead of `simpa using h_ne` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` lemma reconstructPathFuel_weight_eq (hNC : G.NoNegCycle) (fuel : ℕ) (i j : V) (h_ne : reconstructPathFuel G.floydWarshallPi fuel i j ≠ []) : (walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i j) : WithTop ℝ) = G.floydWarshall i j := by have h_adj : ∀ i j k, G.floydWarshallPi i j = some k → G.Adj k j := G.floydWarshallPi_adj induction fuel generalizing i j with | zero => simp [reconstructPathFuel] at h_ne | succ fuel ih => unfold reconstructPathFuel at h_ne ⊢ dsimp at h_ne ⊢ by_cases hij : i = j · subst i; simp [This simp argument is unused: walkWeight Hint: Omit it from the simp argument list. simp ̵[̵w̵a̵l̵k̵W̵e̵i̵g̵h̵t̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`walkWeight] have h_diag : G.floydWarshall j j = (0 : WithTop ℝ) := D_diag_eq_zero G hNC (Finset.univ.toList) j simp [h_diag] · simp [hij, This simp argument is unused: reconstructPathFuel Hint: Omit it from the simp argument list. simp [hij,̵ ̵r̵e̵c̵o̵n̵s̵t̵r̵u̵c̵t̵P̵a̵t̵h̵F̵u̵e̵l̵] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`reconstructPathFuel] at h_ne ⊢ cases hPi : G.floydWarshallPi i j with | none => Try `simp at h_ne` instead of `simpa using h_ne` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [reconstructPathFuel, hij, hPi] using h_ne | some k => simp [This simp argument is unused: reconstructPathFuel Hint: Omit it from the simp argument list. simp [̵r̵e̵c̵o̵n̵s̵t̵r̵u̵c̵t̵P̵a̵t̵h̵F̵u̵e̵l̵,̵ ̵h̵P̵i̵,̵[̲h̲P̲i̲,̲ hij] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`reconstructPathFuel, hPi, This simp argument is unused: hij Hint: Omit it from the simp argument list. simp [reconstructPathFuel, hPi,̵ ̵h̵i̵j̵] at h_ne ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hij] at h_ne ⊢ by_cases hpath : reconstructPathFuel G.floydWarshallPi fuel i k = [] · simp [hpath] at h_ne · simp [hpath] at h_ne ⊢ have hwalk_ik : G.IsWalkFrom i k (reconstructPathFuel G.floydWarshallPi fuel i k) := reconstructPathFuel_isWalkFrom G G.floydWarshallPi fuel i k h_adj hpath have hweight_ik : (walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k) : WithTop ℝ) = G.floydWarshall i k := ih i k hpath have h_getlast : (reconstructPathFuel G.floydWarshallPi fuel i k).getLast hpath = k := by have hlast := hwalk_ik.last have htemp := List.getLast?_eq_getLast_of_ne_nil hpath have h_eq : some ((reconstructPathFuel G.floydWarshallPi fuel i k).getLast hpath) = some k := by rw [htemp] at hlast; exact hlast exact Option.some_inj.mp h_eq -- Weight of ik_path ++ [j] = floydWarshall i k + G.w k j have hweight_full : (walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k ++ [j]) : WithTop ℝ) = G.floydWarshall i k + (G.w k j : WithTop ℝ) := by calc (walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k ++ [j]) : WithTop ℝ) = ((walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k) + G.w ((reconstructPathFuel G.floydWarshallPi fuel i k).getLast hpath) j : ℝ) : WithTop ℝ) := by exact_mod_cast walkWeight_append_singleton G.w (reconstructPathFuel G.floydWarshallPi fuel i k) hpath j _ = ((walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k) + G.w k j : ℝ) : WithTop ℝ) := by rw [h_getlast] _ = (walkWeight G.w (reconstructPathFuel G.floydWarshallPi fuel i k) : WithTop ℝ) + (G.w k j : WithTop ℝ) := by simp _ = G.floydWarshall i k + (G.w k j : WithTop ℝ) := by rw [hweight_ik] rw [hweight_full] exact (floydWarshallPi_D_eq G hNC i j k hPi hij).symm

Transitive closure

The transitive closure of a weighted graph (interpreted as a directed graph: edge exists iff weight is finite) is the boolean matrix T[i,j] where T[i,j] = true iff there exists a walk from i to j.

Under NoNegCycle, Floyd-Warshall computes this exactly: floydWarshall i j ≠ ⊤ iff there is a walk from i to j. This follows directly from floydWarshall_le_walk (every walk has weight at least the shortest distance, so finite distance implies existence) and D_attainable (every finite DP value is realized by a walk).

Transitive closure as a boolean matrix: T[i,j] = true iff j is reachable from i (there exists a finite-weight walk). This is the CLRS §23.2 transitive closure variant of Floyd-Warshall.

noncomputable def transitiveClosure (G : WeightedGraph V) : V → V → Bool := fun i j => G.floydWarshall i j ≠ ⊤

Transitive closure correctness (soundness). If there is a walk from i to j, then the transitive closure reports true.

theorem transitiveClosure_of_walk (hNC : G.NoNegCycle) (i j : V) {p : List V} (hwalk : G.IsWalkFrom i j p) : G.transitiveClosure i j := by have hle := G.floydWarshall_le_walk hNC i j p hwalk have hpos : G.floydWarshall i j ≠ ⊤ := by intro htop have : (walkWeight G.w p : WithTop ℝ) = ⊤ := top_unique (htop ▸ hle) have hfinite : (walkWeight G.w p : WithTop ℝ) ≠ ⊤ := by simp [This simp argument is unused: walkWeight Hint: Omit it from the simp argument list. simp ̵[̵w̵a̵l̵k̵W̵e̵i̵g̵h̵t̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`walkWeight] exact hfinite this simpa [transitiveClosure] using hpos

Transitive closure correctness (completeness). If the transitive closure reports true, then there exists a walk from i to j.

theorem transitiveClosure_exists_walk (Variable name `hNC` 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`hNC : G.NoNegCycle) (i j : V) (hT : G.transitiveClosure i j) : ∃ p, G.IsWalkFrom i j p := by have hT' : G.floydWarshall i j ≠ ⊤ := by simpa [transitiveClosure] using hT have h_fw : G.floydWarshall i j = G.D (Finset.univ.toList : List V) i j := rfl rw [h_fw] at hT' rcases G.D_attainable (Finset.univ.toList : List V) i j with (htop | hwalk) · exact (hT' htop).elim · rcases hwalk with ⟨p, hp, _⟩ exact ⟨p, hp⟩

Transitive closure correctness. Under NoNegCycle, the Floyd-Warshall transitive closure correctly decides walk existence between every pair of vertices (CLRS §23.2 transitive-closure variant).

theorem transitiveClosure_iff_exists_walk (hNC : G.NoNegCycle) (i j : V) : G.transitiveClosure i j ↔ ∃ p, G.IsWalkFrom i j p := by constructor · exact G.transitiveClosure_exists_walk hNC i j · rintro ⟨p, hp⟩; exact G.transitiveClosure_of_walk hNC i j hp

Work bound: O(V³)

The Floyd-Warshall recurrence D performs one min-update (and at most one addition) for each ordered pair (i, j) and each intermediate vertex in Finset.univ.toList, i.e. |V|³ scalar operations in total.

Cost of one Floyd-Warshall intermediate vertex: |V|² entry updates.

def fwStepCost (Variable name `G` 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`G : WeightedGraph V) : ℕ := Fintype.card V * Fintype.card V

Floyd-Warshall table-update budget: the length of the intermediate-vertex list Finset.univ.toList (exactly the list floydWarshall recurses over) times fwStepCost G. Noncomputable only because Finset.univ.toList is.

noncomputable def floydWarshallCost (G : WeightedGraph V) : ℕ := (Finset.univ.toList : List V).length * G.fwStepCost

O(V³) work. Finset.univ.toList has length |V|, so floydWarshallCost G = |V|³.

theorem floydWarshall_O_cubed (G : WeightedGraph V) : G.floydWarshallCost = Fintype.card V * Fintype.card V * Fintype.card V := by unfold floydWarshallCost fwStepCost rw [Finset.length_toList, Finset.card_univ] ac_rfl
end WeightedGraphend Chapter24end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_23.Section_23_2_Floyd_Warshall.NegativeCycle

Complete Floyd–Warshall negative-cycle detection

The cycle-safe initializer takes the minimum of the empty-walk cost zero and an existing self-loop's weight. The original initializer and all original public theorem signatures remain intact. Under no negative cycles, the new initializer and recurrence equal the original ones.

Completeness is proved independently of shortest-path cycle removal: nonnegative final diagonals force triangle inequalities for every processed pivot. Edge bounds and walk induction then show every closed walk is nonnegative. Thus the corrected final diagonal test is equivalent to existence of a negative closed walk, including negative self-loops and cycles in disconnected components.

The definitions use exact real comparisons, as does the existing recurrence. The Boolean interface describes the finite diagonal scan; machine cost and stored-array refinement are supplied separately.

namespace CLRS.Chapter24.WeightedGraphopen Finsetvariable {V : Type*} [Fintype V] [DecidableEq V]noncomputable def floydFrom (initial : V → V → WithTop ℝ) : List V → V → V → WithTop ℝ | [], i, j => initial i j | k :: ks, i, j => min (floydFrom initial ks i j) (floydFrom initial ks i k + floydFrom initial ks k j)omit [Fintype V] [DecidableEq V] in theorem floydFrom_le_initial (initial : V → V → WithTop ℝ) (ks : List V) (i j : V) : floydFrom initial ks i j ≤ initial i j := by induction ks with | nil => exact le_rfl | cons k ks ih => exact (min_le_left _ _).trans ih /- If a Floyd stage has nonnegative diagonals, its processed pivots satisfy triangle inequalities. This implication needs no no-negative-cycle premise. -/ omit [Fintype V] [DecidableEq V] in theorem floydFrom_triangle (initial : V → V → WithTop ℝ) (ks : List V) (hd : ∀ x, 0 ≤ floydFrom initial ks x x) : ∀ k ∈ ks, ∀ i j, floydFrom initial ks i j ≤ floydFrom initial ks i k + floydFrom initial ks k j := by induction ks with | nil => simp | cons v vs ih => let X := floydFrom initial vs have hold : ∀ x, 0 ≤ X x x := fun x => (hd x).trans (min_le_left _ _) have ht := ih hold intro k hk i j simp only [List.mem_cons] at hk change min (X i j) (X i v + X v j) ≤ min (X i k) (X i v + X v k) + min (X k j) (X k v + X v j) rcases hk with rfl | hk · rw [min_eq_left (le_add_of_nonneg_right (hold k)), min_eq_left (le_add_of_nonneg_left (hold k))] exact min_le_right _ _ · have hic : X i v ≤ X i k + X k v := ht k hk i v have hcj : X v j ≤ X v k + X k j := ht k hk v j have hij : X i j ≤ X i k + X k j := ht k hk i j have hcycle : 0 ≤ X k v + X v k := (hd k).trans (min_le_right _ _) rcases min_choice (X i k) (X i v + X v k) with ha | ha <;> rcases min_choice (X k j) (X k v + X v j) with hb | hb <;> rw [ha, hb] · exact (min_le_left _ _).trans hij · calc min (X i j) (X i v + X v j) ≤ X i v + X v j := min_le_right _ _ _ ≤ (X i k + X k v) + X v j := add_le_add hic le_rfl _ = _ := by ac_rfl · calc min (X i j) (X i v + X v j) ≤ X i v + X v j := min_le_right _ _ _ ≤ X i v + (X v k + X k j) := add_le_add le_rfl hcj _ = _ := by ac_rfl · calc min (X i j) (X i v + X v j) ≤ X i v + X v j := min_le_right _ _ _ ≤ (X i v + X v j) + (X k v + X v k) := le_add_of_nonneg_right hcycle _ = _ := by ac_rfl

Initialization retains a negative self-loop while allowing the empty walk.

noncomputable def cycleWeightMatrix (G : WeightedGraph V) (i j : V) : WithTop ℝ := if i = j then if G.Adj i j then min 0 (G.w i j : WithTop ℝ) else 0 else if G.Adj i j then (G.w i j : WithTop ℝ) else ⊤
noncomputable def cycleD (G : WeightedGraph V) : List V → V → V → WithTop ℝ := floydFrom G.cycleWeightMatrixnoncomputable def cycleFloydWarshall (G : WeightedGraph V) : V → V → WithTop ℝ := G.cycleD (Finset.univ.toList : List V)theorem cycleWeightMatrix_le_self (G : WeightedGraph V) (i : V) : G.cycleWeightMatrix i i ≤ 0 := by by_cases h : G.Adj i i <;> simp [cycleWeightMatrix, h]theorem cycleWeightMatrix_le_edge (G : WeightedGraph V) (i j : V) (h : G.Adj i j) : G.cycleWeightMatrix i j ≤ (G.w i j : WithTop ℝ) := by by_cases he : i = j · simp only [cycleWeightMatrix, if_pos he, if_pos h]; exact min_le_right _ _ · simp [cycleWeightMatrix, he, h]theorem cycleFloydWarshall_triangle (G : WeightedGraph V) (hd : ∀ i, 0 ≤ G.cycleFloydWarshall i i) (i k j : V) : G.cycleFloydWarshall i j ≤ G.cycleFloydWarshall i k + G.cycleFloydWarshall k j := floydFrom_triangle G.cycleWeightMatrix (Finset.univ.toList : List V) hd k (by simp) i jtheorem cycleFloydWarshall_le_edge (G : WeightedGraph V) (i j : V) (h : G.Adj i j) : G.cycleFloydWarshall i j ≤ (G.w i j : WithTop ℝ) := (floydFrom_le_initial _ _ _ _).trans (cycleWeightMatrix_le_edge G i j h)theorem cycleFloydWarshall_le_self (G : WeightedGraph V) (i : V) : G.cycleFloydWarshall i i ≤ 0 := (floydFrom_le_initial _ _ _ _).trans (cycleWeightMatrix_le_self G i) theorem cycleFloydWarshall_le_walk_of_nonneg_diag (G : WeightedGraph V) (hd : ∀ i, 0 ≤ G.cycleFloydWarshall i i) (i j : V) (p : List V) (hp : G.IsWalkFrom i j p) : G.cycleFloydWarshall i j ≤ (walkWeight G.w p : WithTop ℝ) := by induction p generalizing i j with | nil => have h := hp.head; simp at h | cons a as ih => have hai : a = i := by simpa using hp.head subst a cases as with | nil => have hij : i = j := by simpa using hp.last subst j simpa using cycleFloydWarshall_le_self G i | cons b bs => have hchain := List.isChain_cons.mp hp.chain have hab : G.Adj i b := hchain.1 b (by simp) have htail : G.IsWalkFrom b j (b :: bs) := ⟨hchain.2, by simp, by simpa using hp.last⟩ calc G.cycleFloydWarshall i j ≤ G.cycleFloydWarshall i b + G.cycleFloydWarshall b j := cycleFloydWarshall_triangle G hd i b j _ ≤ (G.w i b : WithTop ℝ) + (walkWeight G.w (b :: bs) : WithTop ℝ) := add_le_add (cycleFloydWarshall_le_edge G i b hab) (ih b j htail) _ = _ := by simp

Nonnegative final diagonals rule out every negative closed walk.

theorem noNegCycle_of_cycleFloydWarshall_nonneg_diag (G : WeightedGraph V) (hd : ∀ i, 0 ≤ G.cycleFloydWarshall i i) : G.NoNegCycle := by intro i p hp have h := (hd i).trans (cycleFloydWarshall_le_walk_of_nonneg_diag G hd i i p hp) exact_mod_cast h
theorem self_weight_nonneg_of_noNegCycle (G : WeightedGraph V) (hn : G.NoNegCycle) (i : V) (ha : G.Adj i i) : 0 ≤ G.w i i := by have hp : G.IsWalkFrom i i [i, i] := ⟨by simpa using ha, by simp, by simp⟩ simpa [walkWeight] using hn i [i, i] hp

Existing initialization is preserved on every no-negative-cycle input.

theorem cycleWeightMatrix_eq_weightMatrix (G : WeightedGraph V) (hn : G.NoNegCycle) : G.cycleWeightMatrix = G.weightMatrix := by funext i j by_cases hij : i = j · subst j by_cases ha : G.Adj i i · have hw : (0 : WithTop ℝ) ≤ (G.w i i : WithTop ℝ) := by exact_mod_cast self_weight_nonneg_of_noNegCycle G hn i ha simp [cycleWeightMatrix, weightMatrix, ha, min_eq_left hw] · simp [cycleWeightMatrix, weightMatrix, ha] · simp [cycleWeightMatrix, weightMatrix, hij]
theorem cycleD_eq_D (G : WeightedGraph V) (hn : G.NoNegCycle) (ks : List V) : G.cycleD ks = G.D ks := by induction ks with | nil => exact cycleWeightMatrix_eq_weightMatrix G hn | cons k ks ih => funext i j change min (G.cycleD ks i j) (G.cycleD ks i k + G.cycleD ks k j) = _ rw [ih] rfltheorem cycleFloydWarshall_eq_floydWarshall (G : WeightedGraph V) (hn : G.NoNegCycle) : G.cycleFloydWarshall = G.floydWarshall := cycleD_eq_D G hn _ theorem cycleFloydWarshall_nonneg_diag (G : WeightedGraph V) (hn : G.NoNegCycle) (i : V) : 0 ≤ G.cycleFloydWarshall i i := by rw [cycleFloydWarshall_eq_floydWarshall G hn] exact G.floydWarshall_nonneg_diag hn i

Complete global negative-cycle test, including negative self-loops.

theorem cycleFloydWarshall_negative_iff (G : WeightedGraph V) : (∃ i, G.cycleFloydWarshall i i < 0) ↔ ¬ G.NoNegCycle := by constructor · rintro ⟨i, hi⟩ hn exact (not_lt_of_ge (cycleFloydWarshall_nonneg_diag G hn i)) hi · intro hn by_contra h apply hn apply noNegCycle_of_cycleFloydWarshall_nonneg_diag G simpa only [not_exists, not_lt] using h

Equivalent explicit-witness formulation of the detector.

theorem cycleFloydWarshall_negative_iff_closed_walk (G : WeightedGraph V) : (∃ i, G.cycleFloydWarshall i i < 0) ↔ ∃ i p, G.IsWalkFrom i i p ∧ walkWeight G.w p < 0 := by rw [cycleFloydWarshall_negative_iff] unfold NoNegCycle push Not rfl
noncomputable def hasNegativeDiagonal (matrix : V → V → WithTop ℝ) : Bool := (Finset.univ : Finset V).toList.any (fun i => decide (matrix i i < 0))omit [DecidableEq V] in theorem hasNegativeDiagonal_eq_true_iff (matrix : V → V → WithTop ℝ) : hasNegativeDiagonal matrix = true ↔ ∃ i, matrix i i < 0 := by simp [hasNegativeDiagonal]

Boolean interface to the corrected global negative-cycle detector.

noncomputable def detectsNegativeCycle (G : WeightedGraph V) : Bool := hasNegativeDiagonal G.cycleFloydWarshall
theorem detectsNegativeCycle_iff (G : WeightedGraph V) : G.detectsNegativeCycle = true ↔ ¬ G.NoNegCycle := by rw [detectsNegativeCycle, hasNegativeDiagonal_eq_true_iff, cycleFloydWarshall_negative_iff] theorem negative_closed_walk_detected (G : WeightedGraph V) (i : V) (p : List V) (hp : G.IsWalkFrom i i p) (hw : walkWeight G.w p < 0) : G.detectsNegativeCycle = true := by rw [detectsNegativeCycle, hasNegativeDiagonal_eq_true_iff, cycleFloydWarshall_negative_iff_closed_walk] exact ⟨i, p, hp, hw⟩ theorem cycleFloydWarshall_isShortestDist (G : WeightedGraph V) (hn : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (G.cycleFloydWarshall i j) := by rw [cycleFloydWarshall_eq_floydWarshall G hn] exact G.floydWarshall_isShortestDist hn i j

The original recurrence is the generic stored-matrix target with its original initializer.

theorem floydFrom_weightMatrix (G : WeightedGraph V) (ks : List V) : floydFrom G.weightMatrix ks = G.D ks := by induction ks with | nil => rfl | cons k ks ih => funext i j simp only [floydFrom, ih, D_cons]
end CLRS.Chapter24.WeightedGraph

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Reindex

Finite-carrier interfaces for stored matrix execution

An explicit vertex/index equivalence supplies array indices. Its construction is not included in the scalar-operation counters. The equivalence itself is arbitrary; the refinement theorems relate results to the original graph.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionvariable {V : Type*} [Fintype V] [DecidableEq V]

Encode a mathematical matrix with the caller's vertex enumeration.

def encode (e : V ≃ Fin n) (a : V → V → WithTop ℝ) : Fin n → Fin n → WithTop ℝ := fun i j => a (e.symm i) (e.symm j)
omit [DecidableEq V] in theorem encode_minPlus (e : V ≃ Fin n) (a b : V → V → WithTop ℝ) : WeightedGraph.minPlusMul (encode e a) (encode e b) = encode e (WeightedGraph.minPlusMul a b) := by funext i j apply le_antisymm · apply Finset.le_inf intro v _ exact (Finset.inf_le (f := fun k => encode e a i k + encode e b k j) (Finset.mem_univ (e v))).trans_eq (by simp [encode]) · apply Finset.le_inf intro k _ exact Finset.inf_le (Finset.mem_univ (e.symm k))omit [Fintype V] [DecidableEq V] in theorem encode_floyd (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) : WeightedGraph.floydFrom (encode e a) (ks.map e) = encode e (WeightedGraph.floydFrom a ks) := by induction ks with | nil => rfl | cons k ks ih => funext i j simp [List.map_cons, WeightedGraph.floydFrom, ih, encode]def floydOn (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) : Run := floyd (encode e a) (ks.map e)automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem floydOn_read (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) (i j : V) : read (floydOn e a ks).table (e i) (e j) = WeightedGraph.floydFrom a ks i j := by simp [floydOn, floyd_read, encode_floyd, encode]def squareOn (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) : Run := square (encode e a) qomit [DecidableEq V] in theorem encode_square (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) : (fun b => WeightedGraph.minPlusMul b b)^[q] (encode e a) = encode e ((fun b => WeightedGraph.minPlusMul b b)^[q] a) := by induction q with | zero => rfl | succ q ih => simp only [Function.iterate_succ_apply', ih, encode_minPlus]automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem squareOn_read (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) (i j : V) : read (squareOn e a q).table (e i) (e j) = ((fun b => WeightedGraph.minPlusMul b b)^[q] a) i j := by simp [squareOn, square_read, encode_square, encode]

Actual stored cycle-safe Floyd result over the original vertex type.

def cycleFloydOn (e : V ≃ Fin n) (G : WeightedGraph V) : Run := floydOn e G.cycleWeightMatrix Finset.univ.toList
@[simp] theorem cycleFloydOn_read (e : V ≃ Fin n) (G : WeightedGraph V) (i j : V) : read (cycleFloydOn e G).table (e i) (e j) = G.cycleFloydWarshall i j := floydOn_read _ _ _ _ _ theorem cycleFloydOn_shortest (e : V ≃ Fin n) (G : WeightedGraph V) (hNC : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (read (cycleFloydOn e G).table (e i) (e j)) := by rw [cycleFloydOn_read, WeightedGraph.cycleFloydWarshall_eq_floydWarshall G hNC] exact G.floydWarshall_isShortestDist hNC i j

Scan the actual stored diagonal, returning the minimum and visit count.

def diagonalScan (n : Nat) (t : Stored) : WithTop ℝ × Nat := scanFin (fun i : Fin n => read t i i)
@[simp] theorem diagonalScan_visits (n : Nat) (t : Stored) : (diagonalScan n t).2 = n := scanFin_visits _

The counted diagonal scan detects exactly the negative-cycle inputs.

theorem diagonalScan_negative_iff (e : V ≃ Fin n) (G : WeightedGraph V) : (diagonalScan n (cycleFloydOn e G).table).1 < 0 ↔ ¬ G.NoNegCycle := by rw [diagonalScan, scanFin_value, Finset.inf_lt_iff] have hex : (∃ i : Fin n, i ∈ Finset.univ ∧ read (cycleFloydOn e G).table i i < 0) ↔ ∃ v, G.cycleFloydWarshall v v < 0 := by constructor · rintro ⟨i, _, hi⟩ refine ⟨e.symm i, ?_⟩ have heq := cycleFloydOn_read e G (e.symm i) (e.symm i) simp only [Equiv.apply_symm_apply] at heq exact heq ▸ hi · rintro ⟨v, hv⟩ exact ⟨e v, Finset.mem_univ _, by simpa using hv⟩ exact hex.trans G.cycleFloydWarshall_negative_iff

Counted Floyd updates, excluding the separately counted final diagonal scan.

@[simp] theorem cycleFloydOn_visits (e : V ≃ Fin n) (G : WeightedGraph V) : (cycleFloydOn e G).visits = n ^ 3 := by have hcard : Fintype.card V = n := by simpa using Fintype.card_congr e simp [cycleFloydOn, floydOn, hcard, pow_succ, Nat.mul_assoc]

Stored repeated squaring over the original graph carrier.

def fasterOn (e : V ≃ Fin n) (G : WeightedGraph V) : Run := squareOn e G.weightMatrix (WeightedGraph.numSquarings (V := V))
@[simp] theorem fasterOn_read (e : V ≃ Fin n) (G : WeightedGraph V) (i j : V) : read (fasterOn e G).table (e i) (e j) = G.fasterAPSP i j := squareOn_read _ _ _ _ _ theorem fasterOn_shortest (e : V ≃ Fin n) (G : WeightedGraph V) (hNC : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (read (fasterOn e G).table (e i) (e j)) := by rw [fasterOn_read] exact G.fasterAPSP_eq_shortestDist hNC ⟨i⟩ i j@[simp] theorem fasterOn_visits (e : V ≃ Fin n) (G : WeightedGraph V) : (fasterOn e G).visits = WeightedGraph.numSquarings (V := V) * n ^ 3 := square_visits _ _

The old Floyd budget is exactly the updates of this stored execution.

theorem cycleFloydOn_visits_eq_budget (e : V ≃ Fin n) (G : WeightedGraph V) : (cycleFloydOn e G).visits = G.floydWarshallCost := by have hc : Fintype.card V = n := by simpa using Fintype.card_congr e rw [cycleFloydOn_visits, G.floydWarshall_O_cubed, hc] ring

The old squaring budget is exactly the executed min-plus candidate visits.

theorem fasterOn_visits_eq_budget (e : V ≃ Fin n) (G : WeightedGraph V) : (fasterOn e G).visits = G.fasterAPSPCost := by have hc : Fintype.card V = n := by simpa using Fintype.card_congr e rw [fasterOn_visits] simp [WeightedGraph.fasterAPSPCost, WeightedGraph.minPlusMulCost, hc, pow_succ, Nat.mul_assoc]
end CLRS.Chapter24.MatrixExecution

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Basic

Stored matrices and counted min-plus products

Every row and cell is appended once. Inner scans return both their minimum and their actual number of visits. Exact real arithmetic, comparison, and array access are abstract primitives; allocation and bit costs are excluded.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionopen CLRS.Chapter15.DPExecutionabbrev Stored := Table (WithTop ℝ)def read (t : Stored) (i j : Fin n) : WithTop ℝ := get t.rows i.val j.valdef cell (f : Fin n → Fin n → WithTop ℝ × Nat) (i j : Nat) : WithTop ℝ × Nat := if hi : i < n then if hj : j < n then f ⟨i, hi⟩ ⟨j, hj⟩ else (⊤, 0) else (⊤, 0)def tabulate (f : Fin n → Fin n → WithTop ℝ × Nat) : Stored := buildLayers (fun _ => n) (fun i _ j => cell f i j) n @[simp] theorem tabulate_read (f : Fin n → Fin n → WithTop ℝ × Nat) (i j : Fin n) : read (tabulate f) i j = (f i j).1 := by have h := buildLayers_correct (fun _ => n) (fun i _ j => cell f i j) (fun i j => (cell f i j).1) (by intros; rfl) n i.val i.isLt j.val j.isLt simpa [read, tabulate, cell, i.isLt, j.isLt] using h@[simp] theorem tabulate_writes (f : Fin n → Fin n → WithTop ℝ × Nat) : (tabulate f).cellWrites = n * n := by simp [tabulate, buildLayers_cellWrites] theorem tabulate_visits (f : Fin n → Fin n → WithTop ℝ × Nat) (c : Nat) (hc : ∀ i j, (f i j).2 = c) : (tabulate f).candidateVisits = n * n * c := by have rowVisits (i : Nat) (hi : i < n) : ∑ j ∈ Finset.range n, (cell f i j).2 = n * c := by calc _ = ∑ _j ∈ Finset.range n, c := Finset.sum_congr rfl (fun j hj => by simp [cell, hi, Finset.mem_range.mp hj, hc]) _ = n * c := by simp have layers : ∀ k, k ≤ n → (buildLayers (fun _ => n) (fun i _ j => cell f i j) k).candidateVisits = k * (n * c) := by intro k hk induction k with | zero => simp [buildLayers] | succ k ih => simp only [buildLayers] rw [ih (by omega), buildRow_visits, rowVisits k (by omega)] ring simpa [tabulate, Nat.mul_assoc] using layers n (by omega)def scanMin (f : Nat → WithTop ℝ) : Nat → WithTop ℝ × Nat | 0 => (⊤, 0) | k + 1 => let prev := scanMin f k; (min prev.1 (f k), prev.2 + 1)@[simp] theorem scanMin_visits (f : Nat → WithTop ℝ) (k : Nat) : (scanMin f k).2 = k := by induction k with | zero => rfl | succ k ih => simp [scanMin, ih]theorem scanMin_value (f : Nat → WithTop ℝ) (k : Nat) : (scanMin f k).1 = (Finset.range k).inf f := by induction k with | zero => simp [scanMin] | succ k ih => simp [scanMin, ih, Finset.range_add_one, min_comm]def scanFin (f : Fin n → WithTop ℝ) : WithTop ℝ × Nat := scanMin (fun k => if hk : k < n then f ⟨k, hk⟩ else ⊤) n@[simp] theorem scanFin_visits (f : Fin n → WithTop ℝ) : (scanFin f).2 = n := scanMin_visits _ _ theorem scanFin_value (f : Fin n → WithTop ℝ) : (scanFin f).1 = Finset.univ.inf f := by rw [scanFin, scanMin_value] apply le_antisymm · apply Finset.le_inf intro i _ exact (Finset.inf_le (Finset.mem_range.mpr i.isLt)).trans_eq (by simp [i.isLt]) · apply Finset.le_inf intro k hk have hkn := Finset.mem_range.mp hk simpa [hkn] using (Finset.inf_le (s := Finset.univ) (f := f) (Finset.mem_univ (⟨k, hkn⟩ : Fin n)))def multiply (n : Nat) (a b : Stored) : Stored := tabulate (fun i j : Fin n => scanFin (fun k => read a i k + read b k j))@[simp] theorem multiply_read (a b : Stored) (i j : Fin n) : read (multiply n a b) i j = WeightedGraph.minPlusMul (read a) (read b) i j := by simp [multiply, scanFin_value, WeightedGraph.minPlusMul]@[simp] theorem multiply_writes (n : Nat) (a b : Stored) : (multiply n a b).cellWrites = n * n := tabulate_writes _ @[simp] theorem multiply_visits (n : Nat) (a b : Stored) : (multiply n a b).candidateVisits = n ^ 3 := by rw [multiply, tabulate_visits _ n (by intros; exact scanFin_visits _)] ringend CLRS.Chapter24.MatrixExecution

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Algorithms

Counted stored Floyd–Warshall and repeated squaring

Each recursive call is bound once. A Floyd phase reads the completed previous matrix and writes the next matrix; a squaring phase calls the counted min-plus product. Cumulative counters include initialization. No recursive specification is invoked by a cell evaluator.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionstructure Run where table : Stored writes : Nat visits : Natdef initialRun (f : Fin n → Fin n → WithTop ℝ) : Run := let t := tabulate (fun i j => (f i j, 0)) ⟨t, t.cellWrites, t.candidateVisits⟩@[simp] theorem initialRun_read (f : Fin n → Fin n → WithTop ℝ) (i j : Fin n) : read (initialRun f).table i j = f i j := tabulate_read _ _ _@[simp] theorem initialRun_writes (f : Fin n → Fin n → WithTop ℝ) : (initialRun f).writes = n * n := tabulate_writes _ @[simp] theorem initialRun_visits (f : Fin n → Fin n → WithTop ℝ) : (initialRun f).visits = 0 := by change (tabulate (fun i j => (f i j, 0))).candidateVisits = 0 rw [tabulate_visits _ 0 (by intros; rfl)] simpdef floyd (initial : Fin n → Fin n → WithTop ℝ) : List (Fin n) → Run | [] => initialRun initial | k :: ks => let prev := floyd initial ks let next := tabulate (fun i j => (min (read prev.table i j) (read prev.table i k + read prev.table k j), 1)) ⟨next, prev.writes + next.cellWrites, prev.visits + next.candidateVisits⟩theorem floyd_read (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) (i j : Fin n) : read (floyd initial ks).table i j = WeightedGraph.floydFrom initial ks i j := by induction ks generalizing i j with | nil => exact initialRun_read _ _ _ | cons k ks ih => simp only [floyd, tabulate_read, WeightedGraph.floydFrom, ih]@[simp] theorem floyd_writes (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) : (floyd initial ks).writes = (ks.length + 1) * (n * n) := by induction ks with | nil => simp [floyd] | cons k ks ih => simp [floyd, ih, Nat.add_mul] @[simp] theorem floyd_visits (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) : (floyd initial ks).visits = ks.length * (n * n) := by induction ks with | nil => simp [floyd] | cons k ks ih => simp only [floyd, List.length_cons] rw [ih, tabulate_visits _ 1 (by intros; rfl)] ringdef square (initial : Fin n → Fin n → WithTop ℝ) : Nat → Run | 0 => initialRun initial | q + 1 => let prev := square initial q let next := multiply n prev.table prev.table ⟨next, prev.writes + next.cellWrites, prev.visits + next.candidateVisits⟩theorem square_read (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (read (square initial q).table : Fin n → Fin n → WithTop ℝ) = (fun a => WeightedGraph.minPlusMul a a)^[q] initial := by induction q with | zero => funext i j; exact initialRun_read _ _ _ | succ q ih => funext i j simp only [square, multiply_read, Function.iterate_succ_apply', ih]@[simp] theorem square_writes (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (square initial q).writes = (q + 1) * (n * n) := by induction q with | zero => simp [square] | succ q ih => simp [square, ih, Nat.add_mul]@[simp] theorem square_visits (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (square initial q).visits = q * n ^ 3 := by induction q with | zero => simp [square] | succ q ih => simp [square, ih, Nat.add_mul]

Cycle-safe stored Floyd execution, including negative self-edges.

def cycleFloyd (G : WeightedGraph (Fin n)) : Run := floyd G.cycleWeightMatrix Finset.univ.toList
@[simp] theorem cycleFloyd_read (G : WeightedGraph (Fin n)) (i j : Fin n) : read (cycleFloyd G).table i j = G.cycleFloydWarshall i j := floyd_read _ _ _ _

Exactly the counted Floyd cell update on every vertex pair and pivot.

@[simp] theorem cycleFloyd_visits (G : WeightedGraph (Fin n)) : (cycleFloyd G).visits = n ^ 3 := by simp [cycleFloyd, pow_succ, Nat.mul_assoc]

Correctness of the actual stored output under the valid-input premise.

theorem cycleFloyd_shortest (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (i j : Fin n) : G.IsShortestDist i j (read (cycleFloyd G).table i j) := by rw [cycleFloyd_read, WeightedGraph.cycleFloydWarshall_eq_floydWarshall G hNC] exact G.floydWarshall_isShortestDist hNC i j

The stored result detects a negative cycle in either direction.

theorem cycleFloyd_negative_iff (G : WeightedGraph (Fin n)) : (∃ i : Fin n, read (cycleFloyd G).table i i < 0) ↔ ¬ G.NoNegCycle := by simp only [cycleFloyd_read] exact G.cycleFloydWarshall_negative_iff

Counted repeated squaring of the graph matrix.

def faster (G : WeightedGraph (Fin n)) : Run := square G.weightMatrix (WeightedGraph.numSquarings (V := Fin n))
@[simp] theorem faster_read (G : WeightedGraph (Fin n)) (i j : Fin n) : read (faster G).table i j = G.fasterAPSP i j := by change read (square G.weightMatrix (WeightedGraph.numSquarings (V := Fin n))).table i j = _ rw [square_read] rflend CLRS.Chapter24.MatrixExecution