CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 23. All-Pairs Shortest Paths

Chapter 23 — All-Pairs 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
import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

23.1. All-Pairs Shortest Paths Model

Definitions and basic properties of the all-pairs shortest-path model: edge-weight matrix, min-plus product, FASTER-APSP.

Main results:

CLRS.Chapter24.WeightedGraph.minPlusMul: the min-plus matrix product.
CLRS.Chapter24.WeightedGraph.fasterAPSP: CLRS FASTER-APSP (repeated squaring).
CLRS.Chapter24.WeightedGraph.lemma_25_1: Lemma 23.1 (L^(m+1) = L^m ◁ W).
CLRS.Chapter24.WeightedGraph.L_sq_eq_minPlusMul: Lemma 23.2 (L^(2m) = L^m ◁ L^m).
CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_L: FASTER-APSP equals L^(|V|-1) under NoNegCycle.
CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_shortestDist: FASTER-APSP correctness.

minPlusMulCost, fasterAPSPCost — min-plus candidate budgets. The separate MatrixExecution companion realizes them with stored tables.
numSquarings_le_log2_add_one — the iteration count is O(log |V|).
fasterAPSPCost_le_n_cubed_log — O(V³ log V) repeated-squaring work.
fasterAPSPCost_le_n_four — trivial O(V⁴) corollary.

The recursive function-valued specification does not itself establish shared table evaluation. Stored execution and counts are in the matrix companion.

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

Edge-weight matrix W.

def weightMatrix (i j : V) : WithTop ℝ :=
  if i = j then (0 : WithTop ℝ) else if G.Adj i j then (G.w i j : WithTop ℝ) else ⊤

Min-plus matrix product: (A ◁ B)ij = mink (Aik + Bkj).

def minPlusMul (A B : V → V → WithTop ℝ) (i j : V) : WithTop ℝ :=
  (Finset.univ : Finset V).inf (fun k => A i k + B k j)

EXTEND-SHORTEST-PATHS: L' = L ◁ W.

def extendShortestPaths (L : V → V → WithTop ℝ) (i j : V) : WithTop ℝ :=
  minPlusMul L G.weightMatrix i j

L m — shortest-path weights using at most m edges.

def L (G : WeightedGraph V) : ℕ → V → V → WithTop ℝ
  | 0, i, j => if i = j then (0 : WithTop ℝ) else ⊤
  | m + 1, i, j => G.extendShortestPaths (G.L m) i j

@[simp] theorem L_zero (i j : V) : G.L 0 i j = if i = j then (0 : WithTop ℝ) else ⊤ := rfl@[simp] theorem L_succ (m : ℕ) (i j : V) : G.L (m + 1) i j = G.extendShortestPaths (G.L m) i j := rfl

Number of squarings: ceil(log2(|V|-1)).

def Overlapping instance parameters in `numSquarings`:

⚠️ There are 2 `[Fintype V]` instances; one is sufficient.

Note: This linter can be disabled with `set_option linter.overlappingInstances false`numSquarings [Fintype V] : ℕ :=
  let x := Fintype.card V - 1
  if x ≤ 1 then 0 else Nat.log2 (x - 1) + 1

FASTER-APSP: repeatedly square L = L ◁ L.

def Overlapping instance parameters in `fasterAPSP`:

⚠️ There are 2 `[Fintype V]` instances; one is sufficient.

Note: This linter can be disabled with `set_option linter.overlappingInstances false`fasterAPSP [Fintype V] (G : WeightedGraph V) : V → V → WithTop ℝ :=
  (fun L => minPlusMul L L)^[numSquarings (V := V)] G.weightMatrix

Identity matrix for min-plus multiplication.

def identityMatrix (i j : V) : WithTop ℝ := if i = j then (0 : WithTop ℝ) else ⊤

              automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_diag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.identityMatrix_diag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.identityMatrix_diag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem identityMatrix_diag (i : V) : identityMatrix i i = (0 : WithTop ℝ) := by
  simp [identityMatrix]automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_offdiag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.identityMatrix_offdiag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.identityMatrix_offdiag`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem identityMatrix_offdiag {i j : V} (h : i ≠ j) : identityMatrix i j = ⊤ := by
  simp [identityMatrix, h]

theorem minPlusMul_identity_left (M : V → V → WithTop ℝ) (i j : V) :
    minPlusMul identityMatrix M i j = M i j := by
  unfold minPlusMul identityMatrix
  have h1 : (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) ≤ M i j := by
    calc
      (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) ≤
        ((fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) i) :=
        Finset.inf_le (Finset.mem_univ i)
      _ = M i j := by simp
  have h2 : M i j ≤ (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) := by
    apply Finset.le_inf
    intro k hk
    by_cases hik : i = k
    · subst k; simp
    · simp [hik]
  exact le_antisymm h1 h2

theorem minPlusMul_identity_right (M : V → V → WithTop ℝ) (i j : V) :
    minPlusMul M identityMatrix i j = M i j := by
  unfold minPlusMul identityMatrix
  have h1 : (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) ≤ M i j := by
    calc
      (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) ≤
        ((fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) j) :=
        Finset.inf_le (Finset.mem_univ j)
      _ = M i j := by simp
  have h2 : M i j ≤ (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) := by
    apply Finset.le_inf
    intro k hk
    by_cases hkj : k = j
    · subst k; simp
    · simp [hkj]
  exact le_antisymm h1 h2

Lemmas 23.1 and 23.2 (squaring identity)

Lemma 23.1. L^(m+1) = L^m ◁ W. A single EXTEND-SHORTEST-PATHS step is the min-plus product of the current shortest-path matrix with the weight matrix.

theorem lemma_25_1 (m : ℕ) (i j : V) : G.L (m + 1) i j = minPlusMul (G.L m) G.weightMatrix i j := by
  simp [L_succ, extendShortestPaths]

The function a + · distributes over ⊓ in WithTop ℝ.

lemma add_inf_distrib (a b c : WithTop ℝ) : a + (b ⊓ c) = (a + b) ⊓ (a + c) := by
  induction a using WithTop.recTopCoe with
  | top => simp
  | coe a' =>
    induction b using WithTop.recTopCoe with
    | top => simp
    | coe b' =>
      induction c using WithTop.recTopCoe with
      | top => simp
      | coe c' =>
        simpa [WithTop.coe_add] using (congrArg (WithTop.some : ℝ → WithTop ℝ)
          (min_add_add_left a' b' c')).symm

Addition distributes over Finset.inf for nonempty sets.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype 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.WeightedGraph.add_inf`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma add_inf (a : WithTop ℝ) (s : Finset V) (hs : s.Nonempty) (f : V → WithTop ℝ) :
    a + s.inf f = s.inf (fun x => a + f x) := by
  induction' s using Finset.induction_on with x s hx ih
  · exfalso; exact Finset.not_nonempty_empty hs
  · rw [Finset.inf_insert, Finset.inf_insert]
    by_cases hne : s.Nonempty
    · have h_ih := ih hne
      rw [← h_ih, add_inf_distrib]
    · have h_empty : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hne
      subst h_empty
      simp

Min-plus matrix multiplication is associative.


theorem minPlusMul_assoc (A B C : V → V → WithTop ℝ) (i j : V) :
    minPlusMul (minPlusMul A B) C i j = minPlusMul A (minPlusMul B C) i j := by
  unfold minPlusMul
  by_cases huniv : (Finset.univ : Finset V).Nonempty
  · have h_add_inf (a : WithTop ℝ) (f : V → WithTop ℝ) : a + (univ : Finset V).inf f = (univ : Finset V).inf (fun x => a + f x) :=
      add_inf a (univ : Finset V) huniv f
    have hswap_inf (f : V → V → WithTop ℝ) :
        (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => f k l)) =
        (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => f k l)) := by
      calc
        (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => f k l))
            = (univ ×ˢ univ : Finset (V × V)).inf (fun (p : V × V) => f p.1 p.2) := by
              rw [inf_product_left]
        _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => f k l)) := by
          rw [inf_product_right]
    calc
      (univ : Finset V).inf (fun k : V => ((univ : Finset V).inf (fun l : V => A i l + B l k)) + C k j)
          = (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => (A i l + B l k) + C k j)) := by
            refine Finset.inf_congr rfl (fun k hk => ?_)
            rw [add_comm, h_add_inf (C k j) (fun l : V => A i l + B l k)]
            refine Finset.inf_congr rfl (fun l hl => ?_)
            exact add_comm (C k j) (A i l + B l k)
      _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => (A i l + B l k) + C k j)) := by
        rw [hswap_inf (fun k l => (A i l + B l k) + C k j)]
      _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => A i l + (B l k + C k j))) := by
        refine Finset.inf_congr rfl (fun l hl => ?_)
        refine Finset.inf_congr rfl (fun k hk => ?_)
        simp [add_assoc]
      _ = (univ : Finset V).inf (fun l : V => A i l + (univ : Finset V).inf (fun k : V => B l k + C k j)) := by
        refine Finset.inf_congr rfl (fun l hl => ?_)
        rw [(h_add_inf (A i l) (fun k : V => B l k + C k j)).symm]
  · -- univ is empty
    have hempty : (Finset.univ : Finset V) = ∅ := Finset.not_nonempty_iff_eq_empty.mp huniv
    simp [hempty]

L (a + b) = (L a) ◁ (L b) for all a, b. General additive property of the shortest-path matrix.


theorem L_add_eq_minPlusMul (a b : ℕ) (i j : V) : G.L (a + b) i j = minPlusMul (G.L a) (G.L b) i j := by
  induction' b with b ih generalizing i j
  · -- b = 0: L (a+0) = L a = L a ◁ L 0 (since L 0 = identityMatrix)
    have hL0 : G.L (0 : ℕ) = identityMatrix := by
      ext i' j'; simp [L_zero, identityMatrix]
    rw [hL0, minPlusMul_identity_right]
    simp
  · have h_funext : G.L (a + b) = minPlusMul (G.L a) (G.L b) := by
      ext i' j'; exact ih i' j'
    calc
      G.L (a + (b + 1)) i j = G.L ((a + b) + 1) i j := by rw [add_assoc]
      _ = minPlusMul (G.L (a + b)) G.weightMatrix i j := by
        simp [extendShortestPaths]
      _ = minPlusMul (minPlusMul (G.L a) (G.L b)) G.weightMatrix i j := by rw [h_funext]
      _ = minPlusMul (G.L a) (minPlusMul (G.L b) G.weightMatrix) i j := by rw [minPlusMul_assoc]
      _ = minPlusMul (G.L a) (G.L (b + 1)) i j := by
        have hLb1 : G.L (b + 1) = minPlusMul (G.L b) G.weightMatrix := by
          ext i' j'; simpa using lemma_25_1 G b i' j'
        rw [← hLb1]

Lemma 23.2 (squaring identity). L^(2m) = L^m ◁ L^m.


theorem L_sq_eq_minPlusMul (m : ℕ) (i j : V) : G.L (2 * m) i j = minPlusMul (G.L m) (G.L m) i j := by
  calc
    G.L (2 * m) i j = G.L (m + m) i j := by rw [two_mul]
    _ = minPlusMul (G.L m) (G.L m) i j := by rw [L_add_eq_minPlusMul]

Stabilisation and FASTER-APSP correctness

L is monotone nonincreasing in m: using more edges cannot increase the shortest-path weight.

theorem L_monotone (m : ℕ) (i j : V) : G.L (m + 1) i j ≤ G.L m i j := by
  calc
    G.L (m + 1) i j = minPlusMul (G.L m) G.weightMatrix i j := lemma_25_1 G m i j
    _ ≤ (G.L m) i j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j)
    _ = (G.L m) i j := by simp [weightMatrix]

Under NoNegCycle, the univ infimum over A u + weightMatrix u j equals min(A j, (preds j).inf (A u + w u j)). This bridges the min-plus product to the Bellman-Ford relaxation step.


lemma inf_univ_weightMatrix_eq_min_preds (hNC : G.NoNegCycle) (A : V → WithTop ℝ) (j : V) :
    (Finset.univ : Finset V).inf (fun u => A u + G.weightMatrix u j) =
    min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) := by
  have h_nonneg_self_loop : G.Adj j j → (0 : WithTop ℝ) ≤ (G.w j j : WithTop ℝ) := by
    intro h_adj
    have h_nonneg_real : (0 : ℝ) ≤ G.w j j := by
      have h_walk : G.IsWalkFrom j j [j, j] :=
        ⟨(List.isChain_pair.mpr h_adj), by simp, by simp⟩
      have h_nonneg_cycle := hNC j [j, j] h_walk
      simpa [walkWeight] using h_nonneg_cycle
    exact WithTop.coe_le_coe.mpr h_nonneg_real
  apply le_antisymm
  · -- LHS <= RHS
    refine le_min ?_ (Finset.le_inf ?_)
    · -- LHS <= A j
      calc
        (Finset.univ : Finset V).inf (fun u => A u + G.weightMatrix u j) <=
            A j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j)
        _ = A j := by simp [weightMatrix]
    · -- LHS <= A u + w u j for each u in preds j
      intro u hu
      have hu_edge : (u, j) ∈ G.edges := by simpa using hu
      by_cases h_uj : u = j
      · subst u
        have h_wjj_nonneg : (0 : WithTop ℝ) <= (G.w j j : WithTop ℝ) := h_nonneg_self_loop hu_edge
        calc
          (Finset.univ : Finset V).inf (fun u' => A u' + G.weightMatrix u' j) <=
              A j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j)
          _ = A j := by simp [weightMatrix]
          _ = A j + (0 : WithTop ℝ) := by simp
          _ <= A j + (G.w j j : WithTop ℝ) := by
            simpa [add_comm] using add_le_add_left h_wjj_nonneg (A j)
      · calc
          (Finset.univ : Finset V).inf (fun u' => A u' + G.weightMatrix u' j) <=
              A u + G.weightMatrix u j := Finset.inf_le (Finset.mem_univ u)
          _ = A u + (G.w u j : WithTop ℝ) := by
            have hW : G.weightMatrix u j = (G.w u j : WithTop ℝ) := by
              dsimp [weightMatrix]
              have h_adj : G.Adj u j := hu_edge
              simp [h_uj, h_adj]
            rw [hW]
  · -- RHS <= LHS
    apply Finset.le_inf
    intro u hu
    by_cases h_uj : u = j
    · subst u
      calc
        min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) <= A j :=
          min_le_left _ _
        _ = A j + G.weightMatrix j j := by simp [weightMatrix]
    · by_cases hu_preds : u ∈ G.preds j
      · have hu_edge : (u, j) ∈ G.edges := by simpa using hu_preds
        calc
          min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ)))
              <= (G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ)) := min_le_right _ _
          _ <= A u + (G.w u j : WithTop ℝ) := by simpa using Finset.inf_le hu_preds
          _ = A u + G.weightMatrix u j := by
            have hW : G.weightMatrix u j = (G.w u j : WithTop ℝ) := by
              dsimp [weightMatrix]
              have h_adj : G.Adj u j := hu_edge
              simp [h_uj, h_adj]
            rw [hW]
      · have h_no_edge : (u, j) ∉ G.edges := by simpa using hu_preds
        calc
          min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) <= ⊤ := le_top
          _ = A u + G.weightMatrix u j := by
            have hW : G.weightMatrix u j = ⊤ := by
              have h_no_adj : ¬ G.Adj u j := by
                intro h_adj; apply h_no_edge; exact h_adj
              dsimp [weightMatrix]; simp [h_uj, h_no_adj]
            rw [hW]; simp

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.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 L_succ_eq_relaxDist_succ (hNC : G.NoNegCycle) (k : ℕ) (i j : V) :
    G.L (k + 1) i j = G.relaxDist i (k + 1) j := by
  induction' k with k ih generalizing i j
  · -- k = 0: L 1 = relaxDist i 1
    have h_inf : (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) = G.weightMatrix i j := by
      apply le_antisymm
      · calc
          (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) ≤
              (G.relaxDist i 0) i + G.weightMatrix i j := Finset.inf_le (Finset.mem_univ i)
          _ = (0 : WithTop ℝ) + G.weightMatrix i j := by simp [relaxDist_zero_apply]
          _ = G.weightMatrix i j := by simp
      · apply Finset.le_inf
        intro u hu
        by_cases h_ui : u = i
        · subst u; simp [relaxDist_zero_apply]
        · simp [relaxDist_zero_apply, h_ui]
    have hL0 : G.L 0 = identityMatrix := by
      ext i' j'; simp [L_zero, identityMatrix]
    calc
      G.L 1 i j = minPlusMul (G.L 0) G.weightMatrix i j := by
        simp [L_succ, extendShortestPaths]
      _ = minPlusMul identityMatrix G.weightMatrix i j := by rw [hL0]
      _ = G.weightMatrix i j := by simp [minPlusMul_identity_left]
      _ = (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) := by rw [h_inf]
      _ = min (G.relaxDist i 0 j) ((G.preds j).inf (fun u => G.relaxDist i 0 u + (G.w u j : WithTop ℝ))) :=
        inf_univ_weightMatrix_eq_min_preds (G := G) hNC (G.relaxDist i 0) j
      _ = G.relaxDist i 1 j := by simp [relaxDist_succ_apply, relaxStep]
  · -- k → k+1
    have h_IH_fun : ∀ u : V, G.L (k + 1) i u = G.relaxDist i (k + 1) u := by
      exact ih i
    calc
      G.L ((k + 1) + 1) i j = G.L (k + 2) i j := by 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
      _ = minPlusMul (G.L (k + 1)) G.weightMatrix i j := by simp [L_succ, extendShortestPaths]
      _ = (Finset.univ : Finset V).inf (fun u => G.L (k + 1) i u + G.weightMatrix u j) := rfl
      _ = min (G.L (k + 1) i j) ((G.preds j).inf (fun u => G.L (k + 1) i u + (G.w u j : WithTop ℝ))) :=
        inf_univ_weightMatrix_eq_min_preds (G := G) hNC (λ u => G.L (k + 1) i u) j
      _ = min (G.relaxDist i (k + 1) j) ((G.preds j).inf (fun u => G.relaxDist i (k + 1) u + (G.w u j : WithTop ℝ))) := by
        have h_preds_inf : (G.preds j).inf (fun u => G.L (k + 1) i u + (G.w u j : WithTop ℝ)) =
          (G.preds j).inf (fun u => G.relaxDist i (k + 1) u + (G.w u j : WithTop ℝ)) := by
          refine Finset.inf_congr rfl (fun u hu => ?_)
          rw [h_IH_fun u]
        rw [h_IH_fun j, h_preds_inf]
      _ = G.relaxStep (G.relaxDist i (k + 1)) j := rfl
      _ = G.relaxDist i (k + 2) j := by simp [relaxDist_succ_apply]
      _ = G.relaxDist i ((k + 1) + 1) j := by 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

Under NoNegCycle, L k i j = relaxDist i k j for all k.


theorem L_eq_relaxDist (hNC : G.NoNegCycle) (k : ℕ) (i j : V) :
    G.L k i j = G.relaxDist i k j := by
  cases' k with k
  · simp [L_zero, relaxDist_zero_apply, eq_comm]
  · rw [L_succ_eq_relaxDist_succ (G := G) hNC k i j]

Under NoNegCycle, L stabilises at |V|-1: for all m ≥ |V|-1, L m = L (|V|-1).


theorem L_stabilizes (hNC : G.NoNegCycle) (m : ℕ) (hm : Fintype.card V - 1 ≤ m) (i j : V) :
    G.L m i j = G.L (Fintype.card V - 1) i j := by
  rw [L_eq_relaxDist (G := G) hNC m i j, L_eq_relaxDist (G := G) hNC (Fintype.card V - 1) i j]
  apply le_antisymm
  · -- relaxDist i m j ≤ relaxDist i (|V|-1) j: more rounds give better (lower) estimate
    have h_mono : ∀ (k : ℕ), G.relaxDist i (k + 1) j ≤ G.relaxDist i k j :=
      fun k => G.relaxDist_succ_le i k j
    exact Nat.le_induction (le_refl _) (fun k hk hk_ih => le_trans (h_mono k) hk_ih) m hm
  · -- relaxDist i (|V|-1) j ≤ relaxDist i m j: (|V|-1) rounds already gives the shortest distance
    rcases G.relaxDist_isShortestDist hNC i j with ⟨h_lower, _⟩
    rcases G.exists_walk_of_relaxDist i m j with (htop | ⟨p, hp, hlen, hp_eq⟩)
    · rw [htop]; exact le_top
    · calc
        G.relaxDist i (Fintype.card V - 1) j ≤ (walkWeight G.w p : WithTop ℝ) := h_lower p hp
        _ = G.relaxDist i m j := by rw [hp_eq]

fasterAPSP iterates k times the function f(L) = L ◁ L applied to the weight matrix, which gives L (2^k).

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 fasterAPSP_iterate_eq_L (k : ℕ) (i j : V) :
    ((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix) i j = G.L (2 ^ k) i j := by
  induction' k with k ih generalizing i j
  · -- k=0
    have h2 : (2:ℕ)^0 = 1 := by norm_num
    calc
      ((fun M => minPlusMul M M)^[0] G.weightMatrix) i j = G.weightMatrix i j := rfl
      _ = minPlusMul identityMatrix G.weightMatrix i j := by
        rw [(minPlusMul_identity_left G.weightMatrix i j).symm]
      _ = G.L 1 i j := by
        have hL0 : G.L 0 = identityMatrix := by
          ext i' j'; simp [L_zero, identityMatrix]
        calc
          minPlusMul identityMatrix G.weightMatrix i j = minPlusMul (G.L 0) G.weightMatrix i j := by rw [hL0]
          _ = G.L 1 i j := by simp [L_succ, extendShortestPaths]
      _ = G.L ((2:ℕ)^0) i j := by rw [h2]
  · -- k → k+1
    calc
      ((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k+1] G.weightMatrix) i j
          = (minPlusMul (((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix))
              (((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix))) i j := by
            rw [Function.iterate_succ', Function.comp_apply]
      _ = minPlusMul (G.L (2 ^ k)) (G.L (2 ^ k)) i j := by
        have h_fun_eq : ((fun M => minPlusMul M M)^[k] G.weightMatrix) = G.L (2 ^ k) := by
          ext i' j'; exact ih i' j'
        rw [h_fun_eq]
      _ = G.L (2 * (2 ^ k)) i j := (L_sq_eq_minPlusMul (G := G) (2 ^ k) i j).symm
      _ = G.L (2 ^ (k + 1)) i j := by 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

2^numSquarings ≥ Fintype.card V - 1 for any Fintype V with at least 1 vertex. This holds because numSquarings is defined as ceil(log2(|V|-1)).

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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.WeightedGraph.numSquarings_pow_two_ge`:
  [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 numSquarings_pow_two_ge (hV : Nonempty V) : 2 ^ numSquarings (V := V) ≥ Fintype.card V - 1 := by
  have h_card_pos : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr hV
  unfold numSquarings
  by_cases hx1 : Fintype.card V - 1 ≤ 1
  · -- x ≤ 1, so numSquarings = 0, target: 1 ≥ x
    simp [hx1]
  · -- x > 1, so numSquarings = Nat.log2 (x - 1) + 1, target: 2^(log2(x-1)+1) ≥ x
    have hx_gt1 : 1 < Fintype.card V - 1 := by omega
    simp [hx1]
    have hnpos : Fintype.card V - 1 - 1 ≠ 0 := by omega
    set n := Fintype.card V - 1 with hn
    have h_log2_lt : n - 1 < 2 ^ (Nat.log2 (n - 1) + 1) :=
      (Nat.log2_lt (k := Nat.log2 (n - 1) + 1) (h := hnpos)).mp
        (Nat.lt_succ_self (Nat.log2 (n - 1)))
    have h_le : n ≤ 2 ^ (Nat.log2 (n - 1) + 1) := by omega
    simpa [hn] using h_le

Under NoNegCycle, fasterAPSP equals L^(|V|-1).


theorem fasterAPSP_eq_L (hNC : G.NoNegCycle) (hV : Nonempty V) (i j : V) :
    G.fasterAPSP i j = G.L (Fintype.card V - 1) i j := by
  unfold fasterAPSP
  rw [fasterAPSP_iterate_eq_L (G := G) (numSquarings (V := V)) i j]
  exact L_stabilizes (G := G) hNC (2 ^ numSquarings (V := V)) (numSquarings_pow_two_ge hV) i j

Under NoNegCycle, fasterAPSP computes the true shortest-path distances for all pairs, i.e. fasterAPSP extends to IsShortestDist for every pair.


theorem fasterAPSP_eq_shortestDist (hNC : G.NoNegCycle) (hV : Nonempty V) (i j : V) :
    G.IsShortestDist i j (G.fasterAPSP i j) := by
  have h_eq : G.fasterAPSP i j = G.relaxDist i (Fintype.card V - 1) j :=
    calc
      G.fasterAPSP i j = G.L (Fintype.card V - 1) i j := fasterAPSP_eq_L (G := G) hNC hV i j
      _ = G.relaxDist i (Fintype.card V - 1) j := L_eq_relaxDist (G := G) hNC (Fintype.card V - 1) i j
  rw [h_eq]
  exact G.relaxDist_isShortestDist hNC i j

FASTER-APSP performs numSquarings iterations of min-plus matrix squaring. Each squaring of an n × n matrix computes n² entries, each entry taking the minimum over n intermediate vertices, giving n³ scalar operations per squaring. The total is numSquarings × n³, which is O(n³ log n).

These formulas describe candidate budgets; the function-valued recursive specification does not guarantee cached intermediate tables. The separate MatrixExecution.fasterOn_visits_eq_budget theorem connects this budget to actual stored min-plus scans. Table writes are counted separately.

Candidate-visit budget of one min-plus matrix squaring on the actual |V| × |V| matrix: |V|² entries × |V| intermediate vertices = |V|³.

def minPlusMulCost (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 * Fintype.card V

Candidate-visit budget of FASTER-APSP on graph G: numSquarings iterations of minPlusMulCost G.

def fasterAPSPCost (G : WeightedGraph V) : ℕ :=
  numSquarings (V := V) * G.minPlusMulCost

The number of squarings is at most log₂ |V| + 1.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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.WeightedGraph.numSquarings_le_log2_add_one`:
  [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`lemma numSquarings_le_log2_add_one : numSquarings (V := V) ≤ Nat.log2 (Fintype.card V) + 1 := by
  unfold numSquarings
  by_cases h : Fintype.card V - 1 ≤ 1
  · simp [h]
  · simp [h]
    have hle : Nat.log2 (Fintype.card V - 1 - 1) ≤ Nat.log2 (Fintype.card V) := by
      simp only [Nat.log2_eq_log_two]
      exact Nat.log_mono_right (by omega : Fintype.card V - 1 - 1 ≤ Fintype.card V)
    exact hle

Trivial upper bound: numSquarings ≤ |V|.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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.WeightedGraph.numSquarings_le_n`:
  [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`lemma numSquarings_le_n : numSquarings (V := V) ≤ Fintype.card V := by
  unfold numSquarings
  by_cases h : Fintype.card V - 1 ≤ 1
  · simp [h]
  · simp [h]
    have hlog : Nat.log2 (Fintype.card V - 1 - 1) ≤ Fintype.card V - 1 - 1 := Nat.log2_le_self _
    omega

Work-count refinement. FASTER-APSP performs O(|V|³ log |V|) scalar operations: numSquarings ≤ log₂|V| + 1 squarings, each costing |V|³.

theorem fasterAPSPCost_le_n_cubed_log (G : WeightedGraph V) :
    G.fasterAPSPCost ≤
      Fintype.card V * Fintype.card V * Fintype.card V * (Nat.log2 (Fintype.card V) + 1) := by
  unfold fasterAPSPCost minPlusMulCost
  have hsq := numSquarings_le_log2_add_one (V := V)
  exact calc
    numSquarings (V := V) * (Fintype.card V * Fintype.card V * Fintype.card V)
        ≤ (Nat.log2 (Fintype.card V) + 1) * (Fintype.card V * Fintype.card V * Fintype.card V) :=
          Nat.mul_le_mul_right _ hsq
    _ = Fintype.card V * Fintype.card V * Fintype.card V * (Nat.log2 (Fintype.card V) + 1) := by
          ac_rfl

Trivial O(|V|⁴) upper bound. FASTER-APSP performs at most |V|⁴ scalar operations on |V| vertices (via numSquarings ≤ |V|).

theorem fasterAPSPCost_le_n_four (G : WeightedGraph V) :
    G.fasterAPSPCost ≤ Fintype.card V * Fintype.card V * Fintype.card V * Fintype.card V := by
  unfold fasterAPSPCost minPlusMulCost
  have hsq := numSquarings_le_n (V := V)
  exact calc
    numSquarings (V := V) * (Fintype.card V * Fintype.card V * Fintype.card V)
        ≤ Fintype.card V * (Fintype.card V * Fintype.card V * Fintype.card V) :=
          Nat.mul_le_mul hsq (Nat.le_refl _)
    _ = Fintype.card V * Fintype.card V * Fintype.card V * Fintype.card V := by ac_rfl

              end WeightedGraphend Chapter24end CLRS

Definitions and proofs

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]
  rfl

end CLRS.Chapter24.MatrixExecution

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) := rfl

theorem 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

              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

              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

              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]
  rfl

end CLRS.Chapter24.MatrixExecution

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford
import CLRSLean.FourthEdition.Chapter_22.Section_22_3_Dijkstra

23.3. Johnson's Algorithm for Sparse Graphs

Johnson's algorithm computes all-pairs shortest paths in a weighted directed graph with no negative-weight cycles. It works in three stages:

Potential via Bellman-Ford: add a new source vertex s with zero-weight edges to every vertex, run Bellman-Ford from s, and set h(v) = delta(s, v). This construction assumes global NoNegCycle; it does not return a negative-cycle failure or implement an abort branch.
Reweighting: define a new weight function w^(u,v) = w(u,v) + h(u) - h(v). By the triangle inequality of shortest paths, w^ >= 0 for every edge, so Dijkstra's algorithm can be used from every vertex.
|V| x Dijkstra: run Dijkstra from every vertex on the reweighted graph and recover the true distances via delta(u,v) = delta^(u,v) - h(u) + h(v).

Main results:

Theorem reweightedWeight_nonneg: reweighted edge weights are nonnegative.
Theorem reweightedWalkWeight_eq: w^(p) = w(p) + h(u) - h(v) for any walk p from u to v (telescoping property).
Theorem reweighted_isShortestDist: reweighted shortest distances equal original distances shifted by h(u) - h(v).
Lemma noNegCycle_johnsonAugmentedGraph: the augmented graph has no negative cycles iff the original graph has none.
Lemma johnsonPotential_triangle: the Bellman-Ford potential satisfies h(v) ≤ h(u) + w(u, v) for every edge (u, v).
Theorem johnsonDist_isShortestDist: CLRS Theorem 23.5 — end-to-end correctness of Johnson's algorithm: johnsonDist computes the exact all-pairs shortest-path distances.
Lemma johnsonAugmentedGraph_edges_card: the augmented graph has |V| + |E| edges.
Theorem johnsonCost_eq: an independent heap-backend budget |V|·(|V| + |E|)·(log₂|V| + 2). This formula alone does not count a concrete queue or stored distance table.
Theorem johnsonCost_le: the 2·|V|·(|V| + |E|)·(log₂|V| + 1) O-bound corollary.

The section is complete: the augmented-graph potential construction, triangle inequality, reweighting nonnegativity, end-to-end Johnson correctness, and the running-time bound are all proved.

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

Johnson's algorithm preliminary definitions

The augmented graph for Johnson's algorithm: add a fresh source vertex none with zero-weight edges to every original vertex.

All original edges are preserved, with the original weights. There are no edges entering none, so any negative cycle in the original graph remains a negative cycle (and no new negative cycles are introduced).

noncomputable def johnsonAugmentedGraph : WeightedGraph (Option V) :=
  { edges := (Finset.image (fun (v : V) => (none, some v)) Finset.univ) ∪
             (Finset.image (fun ((u, v) : V × V) => (some u, some v)) G.edges)
  , w := fun u v =>
      match u, v with
      | none, some Variable name `v` 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`v => 0
      | some u, some v => G.w u v
      | _, _ => 0
  }

@[simp] theorem mem_edges_johnsonAugmentedGraph_source (v : V) :
    (none, some v) ∈ G.johnsonAugmentedGraph.edges := by
  unfold johnsonAugmentedGraph; simp

@[simp] theorem mem_edges_johnsonAugmentedGraph_edge (u v : V) :
    (some u, some v) ∈ G.johnsonAugmentedGraph.edges ↔ (u, v) ∈ G.edges := by
  unfold johnsonAugmentedGraph; simp

There are no edges entering none in the augmented graph.

theorem no_incoming_to_none_johnsonAugmentedGraph (u : Option V) :
    (u, none) ∉ G.johnsonAugmentedGraph.edges := by
  unfold johnsonAugmentedGraph; simp

Reweighting with a potential function

The reweighted weight function w^(u,v) = w(u,v) + h(u) - h(v), where h : V -> RR is a potential function (typically delta(s, .) from Bellman-Ford).

def reweightedWeight (h : V → ℝ) (u v : V) : ℝ :=
  G.w u v + h u - h v

@[simp] theorem reweightedWeight_eq (h : V → ℝ) (u v : V) :
    G.reweightedWeight h u v = G.w u v + h u - h v := rfl

The reweighted graph G^ has the same edge set as G but with the reweighted weight function w^.

noncomputable def reweightedGraph (h : V → ℝ) : WeightedGraph V :=
  { edges := G.edges
  , w := G.reweightedWeight h
  }

@[simp] theorem edges_reweightedGraph (h : V → ℝ) :
    (G.reweightedGraph h).edges = G.edges := rfl

@[simp] theorem w_reweightedGraph (h : V → ℝ) (u v : V) :
    (G.reweightedGraph h).w u v = G.reweightedWeight h u v := rfl

Telescoping property. For any walk p from u to v, the reweighted walk weight equals the original walk weight plus h(u) - h(v).


theorem reweightedWalkWeight_eq (h : V → ℝ) (u v : V) (p : List V)
    (hp : G.IsWalkFrom u v p) : walkWeight (G.reweightedWeight h) p = walkWeight G.w p + h u - h v := by
  induction p generalizing u v with
  | nil => exact absurd rfl hp.ne_nil
  | cons a as ih =>
    have ha_u : a = u := by
      have hh := hp.head; simpa using hh
    rw [ha_u]
    rw [ha_u] at hp
    cases as with
    | nil =>
      have hv_u : v = u := by
        have hl := hp.last; simp at hl; exact hl.symm
      rw [hv_u]; simp [walkWeight, This simp argument is unused:
  reweightedWeight

Hint: Omit it from the simp argument list.
  simp [walkWeight,̵ ̵r̵e̵w̵e̵i̵g̵h̵t̵e̵d̵W̵e̵i̵g̵h̵t̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`reweightedWeight]
    | cons b bs =>
      have h_chain : List.IsChain G.Adj (u :: b :: bs) := hp.chain
      have h_chain_rest : List.IsChain G.Adj (b :: bs) := by
        cases h_chain with
        | cons_cons _ htail => exact htail
      have h_walk_rest : G.IsWalkFrom b v (b :: bs) :=
        ⟨h_chain_rest, by simp, by simpa using hp.last⟩
      simp [walkWeight, reweightedWeight]
      rw [ih b v h_walk_rest]
      ring

Nonnegativity of reweighted weights. If the potential h satisfies the triangle inequality h(v) <= h(u) + w(u, v) for every edge (u, v), then every reweighted edge weight is nonnegative.

theorem reweightedWeight_nonneg (h : V → ℝ)
    (h_triangle : ∀ u v, (u, v) ∈ G.edges → h v ≤ h u + G.w u v) :
    ∀ u v, (u, v) ∈ G.edges → 0 ≤ G.reweightedWeight h u v := by
  intro u v h_edge
  dsimp [reweightedWeight]
  have hineq : h v ≤ h u + G.w u v := h_triangle u v h_edge
  linarith

Walk equivalence: original graph ↔ reweighted graph



lemma IsWalkFrom_reweighted_iff (h : V → ℝ) (u v : V) (p : List V) :
    (G.reweightedGraph h).IsWalkFrom u v p ↔ G.IsWalkFrom u v p := by
  have h_adj_eq : (G.reweightedGraph h).Adj = G.Adj := by
    ext x y; simp [WeightedGraph.Adj, edges_reweightedGraph]
  constructor
  · intro hw; rcases hw with ⟨hc, hh, hl⟩; refine ⟨?_, hh, hl⟩; rw [← h_adj_eq]; exact hc
  · intro hw; rcases hw with ⟨hc, hh, hl⟩; refine ⟨?_, hh, hl⟩; rw [h_adj_eq]; exact hc

Lift telescoping property to WithTop ℝ

lemma reweightedWalkWeight_eq_withtop (h : V → ℝ) (u v : V) (p : List V)
    (hp : G.IsWalkFrom u v p) :
    (walkWeight (G.reweightedWeight h) p : WithTop ℝ) =
      (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by
  have h_rw := reweightedWalkWeight_eq G h u v p hp
  calc
    (walkWeight (G.reweightedWeight h) p : WithTop ℝ) =
        ((walkWeight G.w p + h u - h v : ℝ) : WithTop ℝ) := by exact_mod_cast h_rw
    _ = (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by simp

WithTop helpers

private lemma add_sub_cancel {a b c : WithTop ℝ} (hc : c ≠ ⊤) (h : a + c ≤ b + c) : a ≤ b :=
  (WithTop.add_le_add_iff_right hc).mp h



private lemma add_sub_assoc {a b c : WithTop ℝ} (hb : b ≠ ⊤) (hc : c ≠ ⊤) :
    (a + b) - c = a + (b - c) := by
  have ⟨b', hb'⟩ := Option.ne_none_iff_exists'.mp hb
  have ⟨c', hc'⟩ := Option.ne_none_iff_exists'.mp hc
  subst hb' hc'
  by_cases ha : a = ⊤
  · subst ha
    calc
      ((⊤ : WithTop ℝ) + (b' : WithTop ℝ)) - (c' : WithTop ℝ) = (⊤ : WithTop ℝ) - (c' : WithTop ℝ) := by simp
      _ = (⊤ : WithTop ℝ) := by simp
      _ = (⊤ : WithTop ℝ) + ((b' : WithTop ℝ) - (c' : WithTop ℝ)) := by rw [WithTop.top_add]
  · have ⟨a', ha'⟩ := Option.ne_none_iff_exists'.mp ha
    subst ha'
    -- ℝ equality: (a'+b'-c') = (a'+(b'-c')) in ℝ, lifted to WithTop ℝ
    calc
      ((a' : ℝ) : WithTop ℝ) + ((b' : ℝ) : WithTop ℝ) - ((c' : ℝ) : WithTop ℝ) =
          (((a' + b' - c' : ℝ) : ℝ) : WithTop ℝ) := by simp
      _ = (((a' + (b' - c') : ℝ) : ℝ) : WithTop ℝ) := by rw [show (a' + b' - c' : ℝ) = (a' + (b' - c') : ℝ) by ring]
      _ = ((a' : ℝ) : WithTop ℝ) + (((b' : ℝ) : WithTop ℝ) - ((c' : ℝ) : WithTop ℝ)) := by simp

Shortest-path preservation under reweighting

Shortest-path preservation. For any potential h, the reweighted shortest distance equals the original shortest distance shifted by h(u) - h(v). This holds without any feasibility assumption on h.


theorem reweighted_isShortestDist (h : V → ℝ) (u v : V) (d : WithTop ℝ) :
    (G.reweightedGraph h).IsShortestDist u v
      (d + (h u : WithTop ℝ) - (h v : WithTop ℝ)) ↔
    G.IsShortestDist u v d := by
  have h_fin_hu : (h u : WithTop ℝ) ≠ ⊤ := by simp
  have h_fin_hv : (h v : WithTop ℝ) ≠ ⊤ := by simp
  have h_fin_diff : ((h u : WithTop ℝ) - (h v : WithTop ℝ)) ≠ ⊤ := by simp
  have h_walk_iff := IsWalkFrom_reweighted_iff G h
  have h_rw_eq := reweightedWalkWeight_eq_withtop G h
  constructor
  · intro h_rsd; rcases h_rsd with ⟨h_lower, h_att⟩; constructor
    · intro p hp
      have hp_hat : (G.reweightedGraph h).IsWalkFrom u v p := (h_walk_iff u v p).mpr hp
      have h_bound := h_lower p hp_hat
      have h_rw' := h_rw_eq u v p hp
      have h_bound' : d + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) ≤
          (walkWeight G.w p : WithTop ℝ) + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) := by
        -- Regroup using add_sub_assoc and use h_bound + h_rw'
        simpa [add_sub_assoc h_fin_hu h_fin_hv] using
          calc
            d + (h u : WithTop ℝ) - (h v : WithTop ℝ) ≤
                (walkWeight (G.reweightedWeight h) p : WithTop ℝ) := h_bound
            _ = (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := h_rw'
      exact add_sub_cancel h_fin_diff h_bound'
    · rcases h_att with (h_dtop | ⟨p, hp_hat, hpw⟩)
      · -- h_dtop: (d + h_u - h_v) = ⊤ in reweighted graph
        -- Need: d = ⊤ in original graph.  Since h_u, h_v are finite,
        -- (d + h_u) - h_v = ⊤ implies d + h_u = ⊤, which implies d = ⊤.
        by_cases hd_top : d = ⊤
        · exact Or.inl hd_top
        · exfalso
          -- d ≠ ⊤, h_u ≠ ⊤, h_v ≠ ⊤ → d + h_u - h_v ≠ ⊤, contradicting h_dtop
          have h_sum_fin : d + (h u : WithTop ℝ) - (h v : WithTop ℝ) ≠ ⊤ := by
            -- All three are finite ℝ values, so the sum is finite
            -- Proof: case analysis to extract the ℝ values
            rcases Option.ne_none_iff_exists'.mp hd_top with ⟨d', hd'⟩
            rcases Option.ne_none_iff_exists'.mp h_fin_hu with ⟨hu', hhu'⟩
            rcases Option.ne_none_iff_exists'.mp h_fin_hv with ⟨hv', hhv'⟩
            rw [hd', hhu', hhv']
            simp
          exact h_sum_fin h_dtop
      · right
        have hp : G.IsWalkFrom u v p := (h_walk_iff u v p).mp hp_hat
        have h_rw' := h_rw_eq u v p hp
        have hpw' : (walkWeight G.w p : WithTop ℝ) = d := by
          have h_eq : (walkWeight G.w p : WithTop ℝ) + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) =
              d + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) := by
            calc
              (walkWeight G.w p : WithTop ℝ) + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) =
                  (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by
                rw [add_sub_assoc h_fin_hu h_fin_hv]
              _ = (walkWeight (G.reweightedWeight h) p : WithTop ℝ) := by symm; exact h_rw'
              _ = d + (h u : WithTop ℝ) - (h v : WithTop ℝ) := hpw
              _ = d + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) := by
                rw [add_sub_assoc h_fin_hu h_fin_hv]
          apply le_antisymm
          · apply add_sub_cancel h_fin_diff; exact h_eq.le
          · apply add_sub_cancel h_fin_diff; exact h_eq.ge
        refine ⟨p, hp, hpw'⟩
  · intro h_sd; rcases h_sd with ⟨h_lower, h_att⟩; constructor
    · intro p hp_hat
      have hp : G.IsWalkFrom u v p := (h_walk_iff u v p).mp hp_hat
      have h_rw' := h_rw_eq u v p hp
      rw [add_sub_assoc h_fin_hu h_fin_hv]
      have h_add_both : d + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) ≤
          (walkWeight G.w p : WithTop ℝ) + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) := by
        gcongr; exact h_lower p hp
      calc
        d + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) ≤
            (walkWeight G.w p : WithTop ℝ) + ((h u : WithTop ℝ) - (h v : WithTop ℝ)) := h_add_both
        _ = (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by
          rw [add_sub_assoc h_fin_hu h_fin_hv]
        _ = (walkWeight (G.reweightedWeight h) p : WithTop ℝ) := h_rw'.symm
    · rcases h_att with (h_dtop | ⟨p, hp, hpw⟩)
      · -- h_dtop: d = ⊤ in original graph
        -- Need: d + h_u - h_v = ⊤ in reweighted graph
        refine Or.inl ?_
        rw [h_dtop]; simp
      · right
        have hp_hat : (G.reweightedGraph h).IsWalkFrom u v p := (h_walk_iff u v p).mpr hp
        have h_rw' := h_rw_eq u v p hp
        refine ⟨p, hp_hat, ?_⟩
        calc
          (walkWeight (G.reweightedWeight h) p : WithTop ℝ) =
              (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := h_rw'
          _ = d + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by rw [hpw]

Negative-cycle equivalence for the augmented graph

No edge in johnsonAugmentedGraph targets none.

lemma adj_target_ne_none (u v : Option V)
    (h_adj : G.johnsonAugmentedGraph.Adj u v) : v ≠ none := by
  intro h_eq; subst h_eq
  have h_edge : (u, none) ∈ G.johnsonAugmentedGraph.edges := h_adj
  exact G.no_incoming_to_none_johnsonAugmentedGraph u h_edge

If a chain in johnsonAugmentedGraph does not start at none, then none never appears in the chain.


lemma chain_no_none (l : List (Option V))
    (h_chain : List.IsChain G.johnsonAugmentedGraph.Adj l)
    (h_head_ne_none : l.head? ≠ some none) : none ∉ l := by
  induction l with
  | nil => simp
  | cons x l' ih =>
    rw [List.isChain_cons] at h_chain
    rcases h_chain with ⟨h_adj, h_chain_tail⟩
    have hx_ne_none : x ≠ none := by
      intro h_eq; subst h_eq; apply h_head_ne_none; simp
    have h_l'_head_ne_none : l'.head? ≠ some none := by
      intro h_eq
      have h_mem : none ∈ l'.head? := by rw [h_eq]; simp
      have h_adj_x_none : G.johnsonAugmentedGraph.Adj x none := h_adj none h_mem
      exact adj_target_ne_none G x none h_adj_x_none rfl
    have h_none_notin_l' : none ∉ l' := ih h_chain_tail h_l'_head_ne_none
    intro h
    cases h with
    | head _ => exact hx_ne_none rfl
    | tail _ h_mem => exact h_none_notin_l' h_mem

The only walk from none to none in the augmented graph is [none].


lemma walk_from_none_to_none_singleton (c : List (Option V))
    (hc : G.johnsonAugmentedGraph.IsWalkFrom none none c) : c = [none] := by
  have h_last : c.getLast? = some none := hc.last
  rcases List.getLast?_eq_some_iff.mp h_last with ⟨c₁, hc_eq⟩
  subst hc_eq
  by_cases h_c₁_empty : c₁ = []
  · subst h_c₁_empty; simp
  · have h_chain : List.IsChain G.johnsonAugmentedGraph.Adj (c₁ ++ [none]) := hc.chain
    rw [List.isChain_append] at h_chain
    rcases h_chain with ⟨_, _, h_adj_cond⟩
    have h_c₁_last_some : c₁.getLast? ≠ none := by
      intro h_eq; apply h_c₁_empty
      exact (List.getLast?_eq_none_iff.mp h_eq)
    rcases Option.ne_none_iff_exists'.mp h_c₁_last_some with ⟨last_c₁, h_last_c₁⟩
    have h_adj_last_none : G.johnsonAugmentedGraph.Adj last_c₁ none :=
      h_adj_cond last_c₁ (by rw [h_last_c₁]; simp) none (by simp)
    exfalso
    exact (adj_target_ne_none G last_c₁ none h_adj_last_none) rfl

Extend a walk by a single edge u → v at the end.


lemma IsWalkFrom.append_step (hp : G.IsWalkFrom s u p) (h_edge : G.Adj u v) :
    G.IsWalkFrom s v (p ++ [v]) := by
  have h_chain : List.IsChain G.Adj (p ++ [v]) :=
    List.IsChain.append hp.chain (List.isChain_singleton v)
      (by
        intro x hx_last
        -- hx_last : p.getLast? = some x (by definition of ∈ for Option)
        rw [hp.last] at hx_last
        -- hx_last : some u = some x
        have hx_eq : x = u := (Option.some_inj.mp hx_last).symm
        subst hx_eq
        intro y hy_head
        -- hy_head : [v].head? = some y (by definition of ∈ for Option)
        -- [v].head? = some v (by simp)
        have hy_eq : y = v := by
          -- hy_head: [v].head? = some y, and [v].head? = some v
          -- So some y = some v, hence y = v
          have hh : [v].head? = some y := hy_head
          have hv : [v].head? = some v := by simp
          rw [hv] at hh
          -- hh: some v = some y
          exact (Option.some_inj.mp hh).symm
        subst hy_eq
        exact h_edge)
  have h_head : (p ++ [v]).head? = some s := by
    have hp_ne_nil : p ≠ [] := hp.ne_nil
    have hp_head_val : p.head? = some s := hp.head
    cases p with
    | nil => exact absurd rfl hp_ne_nil
    | cons a as =>
      -- p = a :: as, so (a :: as ++ [v]).head? = some a
      -- and hp.head gives some a = some s
      have h_head_a : (a :: as).head? = some a := by simp
      rw [h_head_a] at hp_head_val
      -- hp_head_val : some a = some s
      simp [hp_head_val]
  have h_last : (p ++ [v]).getLast? = some v := by simp
  exact ⟨h_chain, h_head, h_last⟩

The weight of a walk extended by a single edge.

lemma walkWeight_append_step (hp : G.IsWalkFrom s u p) (Variable name `h_edge` 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_edge : G.Adj u v) :
    (walkWeight G.w (p ++ [v]) : WithTop ℝ) =
      (walkWeight G.w p : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
  rcases List.getLast?_eq_some_iff.mp hp.last with ⟨q, hq⟩
  subst hq
  simp [walkWeight_concat G.w q u v]

An auxiliary function that strips Option.some from an element.

private def unsome (default : V) (x : Option V) : V :=
  match x with | some v => v | none => default

For a none-free list, the chain in G' lifts to a chain in G.


private lemma chain_none_free_map (default : V) (l : List (Option V))
    (h_chain : List.IsChain G.johnsonAugmentedGraph.Adj l)
    (h_no_none : none ∉ l) :
    List.IsChain G.Adj (l.map (unsome default)) := by
  induction l with
  | nil => exact List.IsChain.nil
  | cons x l' ih =>
    rw [List.isChain_cons] at h_chain
    rcases h_chain with ⟨h_adj, h_chain_tail⟩
    have hx_ne_none : x ≠ none := by
      intro h_eq; subst h_eq; exact h_no_none (by simp)
    have hl'_no_none : none ∉ l' := by
      intro h; exact h_no_none (by simp [h])
    -- Determine x (must be some a since ≠ none)
    obtain ⟨a, hx_eq⟩ := Option.ne_none_iff_exists'.mp hx_ne_none
    subst hx_eq
    -- Now x = some a
    have ih_map : List.IsChain G.Adj (l'.map (unsome default)) :=
      ih h_chain_tail hl'_no_none
    rw [show (some a :: l').map (unsome default) = a :: l'.map (unsome default) by
      simp [unsome]]
    apply List.IsChain.cons ih_map
    intro y hy
    -- hy : y ∈ (l'.map (unsome default)).head?
    -- We need G.Adj a y. Analyze l'.
    cases l' with
    | nil => simp at hy
    | cons z l'' =>
      -- z must be some b (since none ∉ l')
      have hz_ne_none : z ≠ none := by
        intro h_eq; subst h_eq; exact hl'_no_none (by simp)
      obtain ⟨b, hz_eq⟩ := Option.ne_none_iff_exists'.mp hz_ne_none
      subst hz_eq
      -- Now l' = some b :: l''
      -- The head of (some b :: l'').map (unsome default) is b
      have h_head_map : ((some b :: l'').map (unsome default)).head? = some b := by
        simp [unsome]
      rw [h_head_map] at hy
      -- Now hy : y ∈ some b, i.e. some b = some y, so b = y
      have hy_eq : b = y := Option.some_inj.mp hy
      subst hy_eq
      -- Need G.Adj a b. From h_adj: G'.Adj (some a) (some b)
      have h_adj' : G.johnsonAugmentedGraph.Adj (some a) (some b) :=
        h_adj (some b) (by simp)
      exact (G.mem_edges_johnsonAugmentedGraph_edge a b).mp h_adj'

For a none-free list, the walk weights in G' and G agree.


private lemma walkWeight_none_free_eq (default : V) (c : List (Option V))
    (h_no_none : none ∉ c) :
    walkWeight G.johnsonAugmentedGraph.w c =
      walkWeight G.w (c.map (unsome default)) := by
  induction c with
  | nil => simp [walkWeight]
  | cons x cs ih =>
    cases x with
    | none => exfalso; exact h_no_none (by simp)
    | some a =>
      cases cs with
      | nil =>
        -- c = [some a]; both sides are 0
        simp [walkWeight]
      | cons y rest =>
        have h_cs_no_none : none ∉ (y :: rest) := by
          intro h; apply h_no_none; simp [h]
        cases y with
        | none => exfalso; exact h_cs_no_none (by simp)
        | some b =>
          -- c = some a :: some b :: rest
          -- walkWeight G'.w c = G.w a b + walkWeight G'.w (some b :: rest)
          -- walkWeight G.w (c.map f) = G.w a b + walkWeight G.w (b :: rest.map f)
          have h_ih := ih h_cs_no_none
          -- h_ih: walkWeight G'.w (some b :: rest) = walkWeight G.w ((some b :: rest).map (unsome default))
          -- Compute RHS map:
          have h_map_rest : ((some b :: rest).map (unsome default)) = b :: (rest.map (unsome default)) := by
            simp [unsome]
          rw [h_map_rest] at h_ih
          -- Now h_ih: walkWeight G'.w (some b :: rest) = walkWeight G.w (b :: rest.map (unsome default))
          -- Expand both sides using walkWeight formula
          calc
            walkWeight G.johnsonAugmentedGraph.w (some a :: some b :: rest)
                = G.johnsonAugmentedGraph.w (some a) (some b) +
                  walkWeight G.johnsonAugmentedGraph.w (some b :: rest) := by simp [walkWeight]
            _ = G.w a b + walkWeight G.johnsonAugmentedGraph.w (some b :: rest) := by
              simp [johnsonAugmentedGraph]
            _ = G.w a b + walkWeight G.w (b :: rest.map (unsome default)) := by rw [h_ih]
            _ = walkWeight G.w (a :: b :: rest.map (unsome default)) := by simp [walkWeight]
            _ = walkWeight G.w ((some a :: some b :: rest).map (unsome default)) := by
              unfold unsome; simp

Project a none-free walk in G' to a walk in G with the same weight.


private lemma exists_walk_in_G_of_none_free_walk (x' : V) (c : List (Option V))
    (hc : G.johnsonAugmentedGraph.IsWalkFrom (some x') (some x') c)
    (h_no_none : none ∉ c) :
    ∃ (c' : List V),
      G.IsWalkFrom x' x' c' ∧
      walkWeight G.johnsonAugmentedGraph.w c = walkWeight G.w c' := by
  let c' := c.map (unsome x')
  have h_chain_c' : List.IsChain G.Adj c' :=
    chain_none_free_map G x' c hc.chain h_no_none
  have h_head_c' : c'.head? = some x' := by
    have h_head_c : c.head? = some (some x') := hc.head
    rcases List.head?_eq_some_iff.mp h_head_c with ⟨cs, hc_eq⟩
    subst hc_eq
    simp [c', unsome]
  have h_last_c' : c'.getLast? = some x' := by
    rcases List.getLast?_eq_some_iff.mp hc.last with ⟨q, hq⟩
    subst hq
    simp [c', unsome]
  have h_walk_c' : G.IsWalkFrom x' x' c' :=
    ⟨h_chain_c', h_head_c', h_last_c'⟩
  have h_wt_eq : walkWeight G.johnsonAugmentedGraph.w c = walkWeight G.w c' :=
    walkWeight_none_free_eq G x' c h_no_none
  exact ⟨c', h_walk_c', h_wt_eq⟩

If G has no negative cycles, then johnsonAugmentedGraph also has none.


lemma noNegCycle_johnsonAugmentedGraph (hNC : G.NoNegCycle) :
    G.johnsonAugmentedGraph.NoNegCycle := by
  intro x c hc
  cases x with
  | none =>
    have h_single : c = [none] := walk_from_none_to_none_singleton G c hc
    subst h_single; simp [walkWeight]
  | some x' =>
    have h_head_ne_none : c.head? ≠ some none := by
      rw [hc.head]; simp
    have h_no_none : none ∉ c := chain_no_none G c hc.chain h_head_ne_none
    rcases exists_walk_in_G_of_none_free_walk G x' c hc h_no_none with ⟨c', hc'_walk, hw_eq⟩
    rw [hw_eq]
    exact hNC x' c' hc'_walk

Johnson potential via Bellman-Ford on the augmented graph

A direct walk from none to some v in the augmented graph.


lemma isWalkFrom_none_some (v : V) :
    G.johnsonAugmentedGraph.IsWalkFrom none (some v) [none, some v] := by
  let G' := G.johnsonAugmentedGraph
  have h_chain : List.IsChain G'.Adj [none, some v] := by
    rw [List.isChain_cons]
    refine ⟨?_, List.isChain_singleton _⟩
    intro y hy
    have hy_eq : y = some v := by
      have h_head_val : [some v].head? = some (some v) := by simp
      rw [h_head_val] at hy
      exact (Option.some_inj.mp hy).symm
    subst hy_eq
    unfold G' johnsonAugmentedGraph WeightedGraph.Adj
    simp
  refine ⟨h_chain, ?_, ?_⟩
  · simp
  · simp

The Bellman-Ford distance from none to some v in the augmented graph is finite (not ⊤), because there is a direct zero-weight edge.

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma relaxDist_none_some_ne_top (hNC : G.NoNegCycle) (v : V) :
    G.johnsonAugmentedGraph.relaxDist none
      (Fintype.card (Option V) - 1) (some v) ≠ ⊤ := by
  let G' := G.johnsonAugmentedGraph
  have h_no_neg : G'.NoNegCycle := noNegCycle_johnsonAugmentedGraph G hNC
  have h_sd := G'.relaxDist_isShortestDist h_no_neg none (some v)
  rcases h_sd with ⟨h_lower, _⟩
  have h_walk : G'.IsWalkFrom none (some v) [none, some v] :=
    isWalkFrom_none_some G v
  have h_bound : G'.relaxDist none (Fintype.card (Option V) - 1) (some v) ≤
      (walkWeight G'.w [none, some v] : WithTop ℝ) :=
    h_lower [none, some v] h_walk
  have h_wt : (walkWeight G'.w [none, some v] : WithTop ℝ) = (0 : WithTop ℝ) := by
    simp [walkWeight, G', johnsonAugmentedGraph]
  rw [h_wt] at h_bound
  intro h_eq; rw [h_eq] at h_bound; Try `simp at h_bound` instead of `simpa using h_bound`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using h_bound

The Johnson potential h(v) is the shortest-path distance from none to some v in the augmented graph, computed by Bellman-Ford.

noncomputable def johnsonPotential (hNC : G.NoNegCycle) (v : V) : ℝ :=
  (G.johnsonAugmentedGraph.relaxDist none
    (Fintype.card (Option V) - 1) (some v)).untop
    (relaxDist_none_some_ne_top G hNC v)

The potential cast to WithTop ℝ equals the Bellman-Ford relaxation.


lemma johnsonPotential_eq (hNC : G.NoNegCycle) (v : V) :
    (G.johnsonPotential hNC v : WithTop ℝ) =
    G.johnsonAugmentedGraph.relaxDist none
      (Fintype.card (Option V) - 1) (some v) := by
  unfold johnsonPotential
  simp [This simp argument is unused:
  relaxDist_none_some_ne_top G hNC v

Hint: Omit it from the simp argument list.
  simp ̵[̵r̵e̵l̵a̵x̵D̵i̵s̵t̵_̵n̵o̵n̵e̵_̵s̵o̵m̵e̵_̵n̵e̵_̵t̵o̵p̵ ̵G̵ ̵h̵N̵C̵ ̵v̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`relaxDist_none_some_ne_top G hNC v]

The Johnson potential is the shortest-path distance from none to some v in the augmented graph.


lemma johnsonPotential_isShortestDist (hNC : G.NoNegCycle) (v : V) :
    G.johnsonAugmentedGraph.IsShortestDist none (some v)
      (G.johnsonPotential hNC v) := by
  rw [johnsonPotential_eq G hNC]
  have h_no_neg : G.johnsonAugmentedGraph.NoNegCycle :=
    noNegCycle_johnsonAugmentedGraph G hNC
  exact G.johnsonAugmentedGraph.relaxDist_isShortestDist h_no_neg none (some v)

Triangle inequality for the Johnson potential

Triangle inequality for the Johnson potential. For every edge (u, v) in G, we have h(v) ≤ h(u) + w(u, v).


lemma johnsonPotential_triangle (hNC : G.NoNegCycle) (u v : V)
    (h_edge : (u, v) ∈ G.edges) :
    G.johnsonPotential hNC v ≤ G.johnsonPotential hNC u + G.w u v := by
  let G' := G.johnsonAugmentedGraph
  let hu := G.johnsonPotential hNC u
  let hv := G.johnsonPotential hNC v
  have h_sd_u : G'.IsShortestDist none (some u) (hu : WithTop ℝ) :=
    johnsonPotential_isShortestDist G hNC u
  have h_sd_v : G'.IsShortestDist none (some v) (hv : WithTop ℝ) :=
    johnsonPotential_isShortestDist G hNC v
  rcases h_sd_u.2 with (h_top | ⟨p_u, hp_walk, hp_weight⟩)
  · have h_fin : (hu : WithTop ℝ) ≠ ⊤ := by simp
    exact absurd h_top h_fin
  · have h_edge' : G'.Adj (some u) (some v) := by
      unfold G' johnsonAugmentedGraph WeightedGraph.Adj; simp [h_edge]
    have h_walk_v : G'.IsWalkFrom none (some v) (p_u ++ [some v]) :=
      IsWalkFrom.append_step (G := G') hp_walk h_edge'
    have h_weight_v : (walkWeight G'.w (p_u ++ [some v]) : WithTop ℝ) =
        (hu : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
      rw [walkWeight_append_step G' hp_walk h_edge']
      rw [hp_weight]
      have h_w_uv : (G'.w (some u) (some v) : WithTop ℝ) = (G.w u v : WithTop ℝ) := by
        unfold G' johnsonAugmentedGraph; simp
      rw [h_w_uv]
    have h_ineq : (hv : WithTop ℝ) ≤ (walkWeight G'.w (p_u ++ [some v]) : WithTop ℝ) :=
      h_sd_v.1 (p_u ++ [some v]) h_walk_v
    rw [h_weight_v] at h_ineq
    exact_mod_cast h_ineq

Nonnegativity of the reweighted graph

With the Johnson potential, every edge weight in the reweighted graph is nonnegative, satisfying Dijkstra's precondition.


lemma reweightedGraph_nonneg (hNC : G.NoNegCycle) :
    (G.reweightedGraph (G.johnsonPotential hNC)).Nonneg := by
  rw [WeightedGraph.Nonneg]
  intro u v h_edge
  rw [w_reweightedGraph, reweightedWeight_eq]
  have h_triangle := johnsonPotential_triangle G hNC u v h_edge
  linarith

With the Johnson potential, the reweighted graph has no negative cycles.

lemma reweightedGraph_noNegCycle (hNC : G.NoNegCycle) :
    (G.reweightedGraph (G.johnsonPotential hNC)).NoNegCycle :=
  noNegCycle_of_nonneg (G := G.reweightedGraph (G.johnsonPotential hNC)) (G.reweightedGraph_nonneg hNC)

Johnson's all-pairs shortest paths

A WithTop ℝ algebra identity for finite adjustments.

private lemma add_sub_add_sub_eq (a : WithTop ℝ) (b c : ℝ) :
    a = (a + (c : WithTop ℝ) - (b : WithTop ℝ)) + (b : WithTop ℝ) - (c : WithTop ℝ) := by
  induction a using WithTop.recTopCoe with
  | top => simp
  | coe a => simp

Johnson's all-pairs shortest-path distance. Run Bellman-Ford from u in the reweighted graph, then adjust by h(v) - h(u).

noncomputable def johnsonDist (hNC : G.NoNegCycle) (u v : V) : WithTop ℝ :=
  let h := G.johnsonPotential hNC
  let d_hat := (G.reweightedGraph h).relaxDist u (Fintype.card V - 1) v
  d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ)

Theorem (Johnson correctness). johnsonDist hNC u v equals the shortest-path distance δ(u, v) in the original graph G. (CLRS Theorem 23.5)


theorem johnsonDist_isShortestDist (hNC : G.NoNegCycle) (u v : V) :
    G.IsShortestDist u v (G.johnsonDist hNC u v) := by
  let h := G.johnsonPotential hNC
  have h_no_neg : (G.reweightedGraph h).NoNegCycle := G.reweightedGraph_noNegCycle hNC
  let d_hat := (G.reweightedGraph h).relaxDist u (Fintype.card V - 1) v
  have h_sd_dhat : (G.reweightedGraph h).IsShortestDist u v d_hat :=
    (G.reweightedGraph h).relaxDist_isShortestDist h_no_neg u v
  unfold johnsonDist
  -- Let d := d_hat + h(v) - h(u). Then d + h(u) - h(v) = d_hat.
  -- So by reweighted_isShortestDist.mp, G.IsShortestDist u v d.
  have h_algebra : ((d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ)) +
      (h u : WithTop ℝ) - (h v : WithTop ℝ)) = d_hat :=
    (add_sub_add_sub_eq d_hat (h u) (h v)).symm
  have h_equiv := G.reweighted_isShortestDist h u v
    (d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ))
  rw [← h_algebra] at h_sd_dhat
  exact h_equiv.mp h_sd_dhat

General triangle inequality

The fundamental triangle inequality for shortest-path distances: for any edge (u, v), the shortest distance to v is at most the shortest distance to u plus the edge weight. No sign assumptions needed.


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

Every edge in the Johnson-augmented graph targets a some _ vertex.


lemma edge_target_some {u v : Option V}
    (h : (u, v) ∈ G.johnsonAugmentedGraph.edges) : ∃ v', v = some v' := by
  unfold johnsonAugmentedGraph at h
  rcases Finset.mem_union.mp h with (h' | h')
  · rcases Finset.mem_image.mp h' with ⟨v', _, h_eq⟩
    have hv : v = some v' := by
      have h_snd := congrArg Prod.snd h_eq
      simpa using h_snd.symm
    exact ⟨v', hv⟩
  · rcases Finset.mem_image.mp h' with ⟨⟨u', v''⟩, _, h_eq⟩
    have hv : v = some v'' := by
      have h_snd := congrArg Prod.snd h_eq
      simpa using h_snd.symm
    exact ⟨v'', hv⟩

Project a walk in the augmented graph from some a to some b to a walk in G from a to b with the same weight.


lemma walk_johnsonAugmented_some_projection (a b : V) (c : List (Option V))
    (hc : G.johnsonAugmentedGraph.IsWalkFrom (some a) (some b) c) :
    ∃ (c' : List V), G.IsWalkFrom a b c' ∧
      walkWeight G.johnsonAugmentedGraph.w c = walkWeight G.w c' := by
  let G' := G.johnsonAugmentedGraph
  induction c generalizing a b with
  | nil => exact absurd rfl hc.ne_nil
  | cons x xs ih =>
    have hx : x = some a := by
      have hh := hc.head; simp at hh
      -- hh : some x = some (some a)
      simpa using hh
    -- Use rw instead of subst to preserve the IH
    rw [hx] at hc ⊢
    -- Now c = some a :: xs
    rcases (List.isChain_cons_iff G'.Adj (some a) xs).mp hc.chain with
      (hxs_nil | ⟨y, ys, h_adj, h_chain_rest, hxs_eq⟩)
    · -- xs = []
      rw [hxs_nil] at hc ⊢
      -- c = [some a]
      have hab : a = b := by
        have hl := hc.last; simp at hl; simpa using hl
      rw [hab]
      refine ⟨[b], ⟨List.isChain_singleton b, by simp, by simp⟩, ?_⟩
      simp [walkWeight]
    · -- xs = y :: ys; rewrite everything with this
      rw [hxs_eq] at hc ih ⊢
      -- c = some a :: y :: ys
      -- h_adj : G'.Adj (some a) y
      rcases edge_target_some G h_adj with ⟨c', hy⟩
      rw [hy] at hc ih h_adj h_chain_rest ⊢
      -- y = some c'; c = some a :: some c' :: ys
      have h_edge_orig : (a, c') ∈ G.edges :=
        (G.mem_edges_johnsonAugmentedGraph_edge a c').mp h_adj
      -- h_chain_rest : IsChain G'.Adj (some c' :: ys)
      -- Build rest walk
      have h_rest_head : (some c' :: ys).head? = some (some c') := by simp
      have h_rest_last : (some c' :: ys).getLast? = some (some b) := by
        have hl := hc.last; simpa using hl
      have h_rest_walk : G'.IsWalkFrom (some c') (some b) (some c' :: ys) :=
        ⟨h_chain_rest, h_rest_head, h_rest_last⟩
      rcases ih c' b h_rest_walk with ⟨c'_walk, h_walk, h_weight_eq⟩
      -- c'_walk starts at c' and ends at b; deconstruct into c' :: rest
      have h_c'_walk_ne_nil : c'_walk ≠ [] := h_walk.ne_nil
      rcases List.exists_cons_of_ne_nil h_c'_walk_ne_nil with ⟨d, rest, h_c'_walk_eq⟩
      -- d = c' because the walk starts at c'
      have hd_eq_c' : d = c' := by
        have h_walk_head := h_walk.head
        rw [h_c'_walk_eq] at h_walk_head
        simp at h_walk_head
        simpa using h_walk_head
      rw [hd_eq_c'] at h_c'_walk_eq
      -- h_c'_walk_eq : c'_walk = c' :: rest
      have h_walk' : G.IsWalkFrom c' b (c' :: rest) := by
        rwa [h_c'_walk_eq] at h_walk
      have h_weight_eq' : walkWeight G'.w (some c' :: ys) = walkWeight G.w (c' :: rest) := by
        rwa [h_c'_walk_eq] at h_weight_eq
      -- Build full walk a :: c' :: rest
      have h_full_chain : List.IsChain G.Adj (a :: c' :: rest) := by
        rw [List.isChain_cons_iff G.Adj a (c' :: rest)]
        right; exact ⟨c', rest, h_edge_orig, h_walk'.chain, rfl⟩
      have h_full_last : (a :: c' :: rest).getLast? = some b := by
        have hlast := h_walk'.last; simpa using hlast
      have h_full_walk : G.IsWalkFrom a b (a :: c' :: rest) :=
        ⟨h_full_chain, by simp, h_full_last⟩
      have h_weight_eq_full : walkWeight G'.w (some a :: some c' :: ys) =
          walkWeight G.w (a :: c' :: rest) := by
        calc
          walkWeight G'.w (some a :: some c' :: ys) =
              G'.w (some a) (some c') + walkWeight G'.w (some c' :: ys) := rfl
          _ = G.w a c' + walkWeight G'.w (some c' :: ys) := by simp [G', johnsonAugmentedGraph]
          _ = G.w a c' + walkWeight G.w (c' :: rest) := by rw [h_weight_eq']
          _ = walkWeight G.w (a :: c' :: rest) := rfl
      exact ⟨a :: c' :: rest, h_full_walk, h_weight_eq_full⟩

Johnson potential function

The Johnson potential h(v) = δ(none, some v) from Bellman-Ford on the augmented graph. Finite because of the direct none→some v edge (weight 0).

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma johnsonPotential_finite (_hNC : G.NoNegCycle) (v : V) :
    G.johnsonAugmentedGraph.relaxDist none (Fintype.card (Option V) - 1) (some v) ≠ ⊤ := by
  let G' := G.johnsonAugmentedGraph
  have h1 : G'.relaxDist none 1 (some v) ≤ (0 : WithTop ℝ) := by
    calc
      G'.relaxDist none 1 (some v) = G'.relaxStep (G'.relaxDist none 0) (some v) := rfl
      _ ≤ G'.relaxDist none 0 none + (G'.w none (some v) : WithTop ℝ) :=
        G'.relaxStep_le_pred (by simp [G', mem_edges_johnsonAugmentedGraph_source])
      _ = (0 : WithTop ℝ) + (0 : WithTop ℝ) := by simp [G', johnsonAugmentedGraph]
      _ = (0 : WithTop ℝ) := by simp
  have hcardV : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr ⟨v⟩
  have hcard_eq : Fintype.card (Option V) - 1 = Fintype.card V := by
    simp [Fintype.card_option]
  rw [hcard_eq]
  have h_noninc : ∀ m, 1 ≤ m → G'.relaxDist none m (some v) ≤ (0 : WithTop ℝ) :=
    Nat.le_induction h1 (fun n hn hle_n =>
      calc
        G'.relaxDist none (n + 1) (some v) ≤ G'.relaxDist none n (some v) :=
          G'.relaxDist_succ_le none n (some v)
        _ ≤ (0 : WithTop ℝ) := hle_n
    )
  have h_final : G'.relaxDist none (Fintype.card V) (some v) ≤ (0 : WithTop ℝ) :=
    h_noninc (Fintype.card V) hcardV
  intro htop; rw [htop] at h_final; Try `simp at h_final` instead of `simpa using h_final`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using h_final

Nonnegative reweighted weights



theorem johnsonReweightedNonneg (hNC : G.NoNegCycle) :
    (G.reweightedGraph (G.johnsonPotential hNC)).Nonneg := by
  intro u v h_edge
  have h_edge_orig : (u, v) ∈ G.edges := by
    simpa [reweightedGraph] using h_edge
  have h_triangle := G.johnsonPotential_triangle hNC u v h_edge_orig
  dsimp [reweightedGraph, reweightedWeight]
  linarith

Johnson all-pairs distance

noncomputable def johnsonAllPairsDist (hNC : G.NoNegCycle) (u v : V) : WithTop ℝ :=
  let h := G.johnsonPotential hNC
  let G_hat := G.reweightedGraph h
  let st := G_hat.dijkstraLoop u (Fintype.card V)
  let d_hat := st.d v
  d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ)

End-to-end correctness



theorem johnsonAllPairsDist_correct (hNC : G.NoNegCycle) (u v : V) :
    G.IsShortestDist u v (G.johnsonAllPairsDist hNC u v) := by
  let h := G.johnsonPotential hNC
  let G_hat := G.reweightedGraph h
  have hnn : G_hat.Nonneg := G.johnsonReweightedNonneg hNC
  have hNC_hat : G_hat.NoNegCycle := G_hat.noNegCycle_of_nonneg hnn
  let δ_hat (v : V) : WithTop ℝ := G_hat.relaxDist u (Fintype.card V - 1) v
  have hδ_hat (v : V) : G_hat.IsShortestDist u v (δ_hat v) :=
    G_hat.relaxDist_isShortestDist hNC_hat u v
  have h_dijkstra (v : V) : (G_hat.dijkstraLoop u (Fintype.card V)).d v = δ_hat v :=
    G_hat.dijkstraLoop_correct hnn u δ_hat hδ_hat (Fintype.card V)
      (le_refl (Fintype.card V)) v
  -- Expand johnsonAllPairsDist using the locally defined h and G_hat
  -- The local h and G_hat are definitionally equal to the ones in the definition
  have h_expand : G.johnsonAllPairsDist hNC u v =
      (G_hat.dijkstraLoop u (Fintype.card V)).d v + (h v : WithTop ℝ) - (h u : WithTop ℝ) := by
    unfold johnsonAllPairsDist
    rfl
  rw [h_expand]
  rw [h_dijkstra v]
  -- Goal: G.IsShortestDist u v (δ_hat v + (h v : WithTop ℝ) - (h u : WithTop ℝ))
  -- reweighted_isShortestDist: (G_hat).IsShortestDist u v (d + h_u - h_v) ↔ G.IsShortestDist u v d
  -- Let d := δ_hat v + h_v - h_u; then d + h_u - h_v = δ_hat v
  have h_fin_hu : (h u : WithTop ℝ) ≠ ⊤ := by simp
  have h_fin_hv : (h v : WithTop ℝ) ≠ ⊤ := by simp
  set d := δ_hat v + (h v : WithTop ℝ) - (h u : WithTop ℝ) with hd
  have h_eq : d + (h u : WithTop ℝ) - (h v : WithTop ℝ) = δ_hat v := by
    dsimp [d]
    rcases Option.ne_none_iff_exists'.mp h_fin_hu with ⟨hu_val, hhu⟩
    rcases Option.ne_none_iff_exists'.mp h_fin_hv with ⟨hv_val, hhv⟩
    rw [hhu, hhv]
    by_cases hδ_top : δ_hat v = ⊤
    · rw [hδ_top]; simp
    · rcases Option.ne_none_iff_exists'.mp hδ_top with ⟨δv_val, hδv⟩
      rw [hδv]; simp
  have h_sd_d : G_hat.IsShortestDist u v (d + (h u : WithTop ℝ) - (h v : WithTop ℝ)) := by
    rw [h_eq]; exact hδ_hat v
  exact (G.reweighted_isShortestDist h u v d).mp h_sd_d

Work bound: O(V² log V + V E log V)

Johnson's algorithm runs one Bellman-Ford pass on the augmented graph (to build the potential h) and then |V| Dijkstra passes on the reweighted graph (which shares G's |E| edges). In the binary-heap cost model of Section 22.3 this is (|V| - 1)·(|V| + |E|) edge relaxations plus |V|·(|V| + |E|)·(log₂|V| + 1) heap operations, i.e. O(V² log V + V E log V).

The two image components of johnsonAugmentedGraph.edges are disjoint: edges out of none never collide with lifted original edges.


lemma johnsonAugmentedGraph_edges_disjoint (G : WeightedGraph V) :
    Disjoint (Finset.image (fun (v : V) => (none, some v)) (Finset.univ : Finset V))
      (Finset.image (fun ((u, v) : V × V) => (some u, some v)) G.edges) := by
  rw [Finset.disjoint_left]
  intro e heA heB
  rcases Finset.mem_image.mp heA with ⟨v, _, rfl⟩
  rcases Finset.mem_image.mp heB with ⟨p, _, h⟩
  have hnone : some p.1 = none := congrArg Prod.fst h
  simp at hnone

The augmented graph has |V| + |E| edges: |V| zero-weight edges out of none plus the |E| original edges.


lemma johnsonAugmentedGraph_edges_card (G : WeightedGraph V) :
    G.johnsonAugmentedGraph.edges.card = Fintype.card V + G.edges.card := by
  have hA_inj : Function.Injective (fun v : V => ((none : Option V), some v)) := by
    intro a b h; exact Option.some.inj (congrArg Prod.snd h)
  have hB_inj : Function.Injective (fun ((u, v) : V × V) => (some u, some v)) := by
    intro a b h
    exact Prod.ext (Option.some.inj (congrArg Prod.fst h)) (Option.some.inj (congrArg Prod.snd h))
  have hA : ((Finset.univ : Finset V).image (fun v : V => ((none : Option V), some v))).card = Fintype.card V :=
    (Finset.card_image_of_injective (Finset.univ : Finset V) hA_inj).trans Finset.card_univ
  have hB : (G.edges.image (fun ((u, v) : V × V) => (some u, some v))).card = G.edges.card :=
    Finset.card_image_of_injective G.edges hB_inj
  unfold johnsonAugmentedGraph
  rw [Finset.card_union_of_disjoint (johnsonAugmentedGraph_edges_disjoint G), hA, hB]

Total Johnson work: one Bellman-Ford pass on the augmented graph (potential) plus |V| Dijkstra passes on the reweighted graph. Noncomputable only because johnsonAugmentedGraph is.

noncomputable def johnsonCost (G : WeightedGraph V) : ℕ :=
  G.johnsonAugmentedGraph.bellmanFordWork +
    Fintype.card V * dijkstraWork (Fintype.card V) G.edges.card

Johnson work bound. In the binary-heap cost model, Johnson's algorithm runs in |V|·(|V| + |E|)·(log₂|V| + 2), i.e. O(V² log V + V E log V).


theorem johnsonCost_eq (G : WeightedGraph V) :
    G.johnsonCost = Fintype.card V * (Fintype.card V + G.edges.card) * (Nat.log2 (Fintype.card V) + 2) := by
  unfold johnsonCost bellmanFordWork dijkstraWork
  rw [johnsonAugmentedGraph_edges_card]
  have hcard : Fintype.card (Option V) - 1 = Fintype.card V := by
    rw [Fintype.card_option]; simp
  rw [hcard]
  ring_nf

O(V² log V + V E log V) work. Since log₂|V| + 2 ≤ 2·(log₂|V| + 1), Johnson's work is at most 2·|V|·(|V| + |E|)·(log₂|V| + 1).


theorem johnsonCost_le (G : WeightedGraph V) :
    G.johnsonCost ≤ 2 * Fintype.card V * (Fintype.card V + G.edges.card) * (Nat.log2 (Fintype.card V) + 1) := by
  rw [johnsonCost_eq]
  calc
    Fintype.card V * (Fintype.card V + G.edges.card) * (Nat.log2 (Fintype.card V) + 2)
        ≤ Fintype.card V * (Fintype.card V + G.edges.card) * (2 * (Nat.log2 (Fintype.card V) + 1)) := by
          exact Nat.mul_le_mul_left _ (by omega)
    _ = 2 * Fintype.card V * (Fintype.card V + G.edges.card) * (Nat.log2 (Fintype.card V) + 1) := by ac_rfl

              end WeightedGraphend Chapter24end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Dijkstra

Stored Dijkstra with a list scan queue. The accumulated work counts candidate visits, row-cell evaluations and writes, queue construction, and successful settlements. This indexed real-operation model treats array access and real arithmetic as primitive; it does not claim a binary-heap bound or a bit-complexity bound.

              noncomputable sectionnamespace CLRS.Chapter24.JohnsonExecutionopen MatrixExecution (Stored)structure QueueState (n : Nat) where
  row : Vector
  queue : List (Fin n)def view (st : QueueState n) : WeightedGraph.DijkstraState (Fin n) where
  S := Finset.univ \ st.queue.toFinset
  d := vecRead st.rowdef initState (weights : Stored) (s : Fin n) : QueueState n × Nat :=
  let row := vector (fun v : Fin n => (if v = s then 0 else MatrixExecution.read weights s v, 1))
  let queue := initialQueue s n le_rfl
  (⟨row, queue.1⟩, row.writes + row.visits + queue.2)

@[simp] theorem initState_work (weights : Stored) (s : Fin n) :
    (initState weights s).2 = 3 * n := by
  simp only [initState, vector_writes, initialQueue_visits]
  rw [vector_visits _ 1 (by intros; rfl)]
  omega@[simp] theorem initState_nodup (weights : Stored) (s : Fin n) :
    (initState weights s).1.queue.Nodup := initialQueue_nodup s n le_rfltheorem initState_length_le (weights : Stored) (s : Fin n) :
    (initState weights s).1.queue.length ≤ n := initialQueue_length_le s n le_rfldef MatrixCorrect (G : WeightedGraph (Fin n)) (weights : Stored) : Prop :=
  ∀ i j, MatrixExecution.read weights i j =
    if (i, j) ∈ G.edges then (G.w i j : WithTop ℝ) else ⊤theorem initState_view (G : WeightedGraph (Fin n)) (weights : Stored) (hw : MatrixCorrect G weights)
    (s : Fin n) : view (initState weights s).1 = G.dijkstraInit s := by
  apply WeightedGraph.DijkstraState.ext
  · ext v
    simp [view, initState, initialQueue_mem, v.isLt, WeightedGraph.dijkstraInit]
  · funext v
    simp [view, initState, hw s v, WeightedGraph.dijkstraInit]def relaxRow (weights : Stored) (row : Vector) (u : Fin n) : Vector :=
  vector (fun v : Fin n => (min (vecRead row v) (vecRead row u + MatrixExecution.read weights u v), 1))@[simp] theorem relaxRow_writes (weights : Stored) (row : Vector) (u : Fin n) :
    (relaxRow weights row u).writes = n := vector_writes _@[simp] theorem relaxRow_visits (weights : Stored) (row : Vector) (u : Fin n) :
    (relaxRow weights row u).visits = n := by
  simpa [relaxRow] using vector_visits (fun v : Fin n =>
    (min (vecRead row v) (vecRead row u + MatrixExecution.read weights u v), 1)) 1 (by intros; rfl)def advance (weights : Stored) (st : QueueState n) (u : Fin n) (rest : List (Fin n)) : QueueState n :=
  ⟨relaxRow weights st.row u, rest⟩

theorem advance_view (G : WeightedGraph (Fin n)) (weights : Stored) (hw : MatrixCorrect G weights)
    (st : QueueState n) (hq : st.queue.Nodup) (u : Fin n) (rest : List (Fin n))
    (hp : st.queue.Perm (u :: rest)) :
    view (advance weights st u rest) = G.dijkstraSettle (view st) u := by
  have hnew := List.nodup_cons.mp (hp.nodup_iff.mp hq)
  apply WeightedGraph.DijkstraState.ext
  · ext v
    have hm : v ∈ st.queue ↔ v = u ∨ v ∈ rest := by simpa using hp.mem_iff
    simp only [view, advance, WeightedGraph.dijkstraSettle, Finset.mem_sdiff,
      Finset.mem_univ, List.mem_toFinset, true_and, Finset.mem_insert]
    rw [hm]
    by_cases hv : v = u
    · subst v; simp [hnew.1]
    · simp [hv]
  · funext v
    simp only [view, advance, relaxRow, vector_read, WeightedGraph.dijkstraSettle]
    rw [hw u v]
    by_cases he : (u, v) ∈ G.edges <;> simp [he]def run (weights : Stored) : Nat → QueueState n → QueueState n × Nat
  | 0, st => (st, 0)
  | k + 1, st =>
      let found := extractMin (vecRead st.row) st.queue
      match found.1 with
      | none => (st, found.2)
      | some (u, rest) =>
          let next := advance weights st u rest
          let result := run weights k next
          (result.1, found.2 + next.row.writes + next.row.visits + 1 + result.2)


theorem run_invariant (G : WeightedGraph (Fin n)) (weights : Stored) (hw : MatrixCorrect G weights)
    (hnn : G.Nonneg) (s : Fin n) (δ : Fin n → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) (k : Nat)
    (st : QueueState n) (hq : st.queue.Nodup)
    (hinv : G.DijkstraInvariant hnn s δ hδ (view st)) :
    G.DijkstraInvariant hnn s δ hδ (view (run weights k st).1) := by
  induction k generalizing st with
  | zero => exact hinv
  | succ k ih =>
    simp only [run]
    split
    · exact hinv
    · rename_i u rest he
      obtain ⟨hp, hm⟩ := extractMin_spec (vecRead st.row) st.queue he
      have hn := List.nodup_cons.mp (hp.nodup_iff.mp hq)
      apply ih _ hn.2
      rw [advance_view G weights hw st hq u rest hp]
      apply G.dijkstraSettle_invariant hnn s δ hδ (view st) hinv u
      · have hu : u ∈ st.queue := hp.mem_iff.mpr (by simp)
        simpa [view] using hu
      · intro v hv
        apply hm v
        simpa [view] using hvtheorem run_queue_empty (weights : Stored) (k : Nat) (st : QueueState n)
    (hlen : st.queue.length ≤ k) : (run weights k st).1.queue = [] := by
  induction k generalizing st with
  | zero => simpa [run] using hlen
  | succ k ih =>
    simp only [run]
    split
    · rename_i he
      exact (extractMin_none (vecRead st.row) st.queue).mp he
    · rename_i u rest he
      obtain ⟨hp, _⟩ := extractMin_spec (vecRead st.row) st.queue he
      have hl := hp.length_eq
      apply ih
      change rest.length ≤ k
      simp only [List.length_cons] at hl
      omega

theorem run_work_le (weights : Stored) (k : Nat) (st : QueueState n)
    (hlen : st.queue.length ≤ n) : (run weights k st).2 ≤ k * (3 * n + 1) := by
  induction k generalizing st with
  | zero => simp [run]
  | succ k ih =>
    simp only [run]
    split
    · simp only [extractMin_visits]
      nlinarith
    · rename_i u rest he
      obtain ⟨hp, _⟩ := extractMin_spec (vecRead st.row) st.queue he
      have hl := hp.length_eq
      have hr : rest.length ≤ n := by simp only [List.length_cons] at hl; omega
      have hind := ih (advance weights st u rest) hr
      simp only [advance] at hind
      simp only [extractMin_visits, advance, relaxRow_writes, relaxRow_visits]
      nlinarithdef dijkstraStored (weights : Stored) (s : Fin n) : Vector × Nat :=
  let initial := initState weights s
  let result := run weights n initial.1
  (result.1.row, initial.2 + result.2)

theorem dijkstraStored_correct (G : WeightedGraph (Fin n)) (weights : Stored)
    (hw : MatrixCorrect G weights) (hnn : G.Nonneg) (s : Fin n) (δ : Fin n → WithTop ℝ)
    (hδ : ∀ v, G.IsShortestDist s v (δ v)) (v : Fin n) :
    vecRead (dijkstraStored weights s).1 v = δ v := by
  have hi : G.DijkstraInvariant hnn s δ hδ (view (initState weights s).1) := by
    rw [initState_view G weights hw s]
    exact G.dijkstraInit_invariant hnn s δ hδ
  have hf := run_invariant G weights hw hnn s δ hδ n (initState weights s).1
    (initState_nodup weights s) hi
  have hq := run_queue_empty weights n (initState weights s).1 (initState_length_le weights s)
  exact hf.hsettled v (by simp [view, hq])theorem dijkstraStored_work_le (weights : Stored) (s : Fin n) :
    (dijkstraStored weights s).2 ≤ 3 * n ^ 2 + 4 * n := by
  have hr := run_work_le weights n (initState weights s).1 (initState_length_le weights s)
  simp only [dijkstraStored, initState_work]
  nlinarithend CLRS.Chapter24.JohnsonExecution

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.DijkstraCore

Dijkstra settlement with an explicit minimum

This proof isolates the standard invariant update from the native classical minimum selector. A counted queue may supply any actual unsettled minimum, including its own deterministic tie choice.

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

Settle the chosen vertex and relax every outgoing edge.

noncomputable def dijkstraSettle (st : DijkstraState V) (u : V) : DijkstraState V :=
  { 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 }

Any unsettled minimum preserves the native Dijkstra invariant.


theorem dijkstraSettle_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_notin_S : u ∉ st.S) (hu_min_all : ∀ y, y ∉ st.S → st.d u ≤ st.d y) :
    DijkstraInvariant G hnn s δ hδ (G.dijkstraSettle st u) := by
  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
  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 (he | hx_S)
    · subst x
      -- 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 (he | hx_S)
    · subst x
      -- 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'⟩

end CLRS.Chapter24.WeightedGraph

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Execution

Stored Johnson execution with an indexed scan queue

Vertices are explicitly Fin n. The returned array retains one complete row per source. Execution first materializes the augmented edge matrix, computes and caches Bellman–Ford potentials, and materializes one reweighted matrix. Each source then runs stored Dijkstra once and appends its restored row. No shortest-distance oracle is called by the execution definitions.

The returned work is the sum of actual candidate visits, row evaluations/writes, queue construction/settlements, and completed-row appends. In this indexed real-operation model, the dense matrices and scan queue give a cubic upper bound. Indexed array access, graph edge/weight queries, and real arithmetic are primitives; Lean finite-set membership implementation, persistent-array copying, bit complexity, and a binary-heap runtime are outside this model. Correctness requires a graph with no negative cycle; no rejection API is implemented.

noncomputable sectionnamespace CLRS.Chapter24.JohnsonExecution

Execute one source, then materialize the restored original-weight row.

def sourceRow (prepared : Prepared n) (s : Fin n) : Vector × Nat :=
  let computed := dijkstraStored prepared.weights s
  let out := vector (fun v : Fin n =>
    (vecRead computed.1 v + vecRead prepared.potential v - vecRead prepared.potential s, 1))
  (out, computed.2 + out.writes + out.visits)

              

theorem sourceRow_work_le (prepared : Prepared n) (s : Fin n) :
    (sourceRow prepared s).2 ≤ 3 * n ^ 2 + 6 * n := by
  have hd := dijkstraStored_work_le prepared.weights s
  simp only [sourceRow, vector_writes]
  rw [vector_visits _ 1 (by intros; rfl)]
  nlinarith

theorem sourceRow_read (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (s v : Fin n) :
    vecRead (sourceRow (prepare G) s).1 v = G.johnsonAllPairsDist hNC s v := by
  let Gh := G.reweightedGraph (G.johnsonPotential hNC)
  have hnn : Gh.Nonneg := G.johnsonReweightedNonneg hNC
  let δ : Fin n → WithTop ℝ := fun v => Gh.relaxDist s (Fintype.card (Fin n) - 1) v
  have hδ : ∀ v, Gh.IsShortestDist s v (δ v) :=
    fun v => Gh.relaxDist_isShortestDist (Gh.noNegCycle_of_nonneg hnn) s v
  have hd := dijkstraStored_correct Gh (prepare G).weights (prepare_weights G hNC) hnn s δ hδ v
  have hl := Gh.dijkstraLoop_correct hnn s δ hδ n (by simp) v
  simp only [sourceRow, vector_read, prepare_potential G hNC, hd]
  simpa [WeightedGraph.johnsonAllPairsDist, Gh] using
    congrArg (fun d : WithTop ℝ => d + (G.johnsonPotential hNC v : WithTop ℝ) -
      (G.johnsonPotential hNC s : WithTop ℝ)) hl.symmstructure Result (n : Nat) where
  rows : Array Vector
  work : Nat

Append one completed source row per iteration; the inner cell loop never reruns Dijkstra.

def sourceRows (prepared : Prepared n) : (k : Nat) → k ≤ n → Result n
  | 0, _ => ⟨#[], 0⟩
  | k + 1, hk =>
    let previous := sourceRows prepared k (by omega)
    let next := sourceRow prepared ⟨k, by omega⟩
    ⟨previous.rows.push next.1, previous.work + next.2 + 1⟩

              @[simp] theorem sourceRows_size (prepared : Prepared n) (k : Nat) (hk : k ≤ n) :
    (sourceRows prepared k hk).rows.size = k := by
  induction k with
  | zero => rfl
  | succ k ih => simp [sourceRows, ih]

theorem sourceRows_get (prepared : Prepared n) (k : Nat) (hk : k ≤ n)
    (i : Nat) (hi : i < k) :
    (sourceRows prepared k hk).rows[i]? = some (sourceRow prepared ⟨i, by omega⟩).1 := by
  induction k with
  | zero => omega
  | succ k ih =>
    by_cases he : i = k
    · subst i
      simp only [sourceRows, Array.getElem?_push, sourceRows_size, ite_true]
    · have hi' : i < k := by omega
      simp only [sourceRows, Array.getElem?_push]
      rw [sourceRows_size]
      simp only [he, if_false]
      exact ih (by omega) hi'

theorem sourceRows_work_le (prepared : Prepared n) (k : Nat) (hk : k ≤ n) :
    (sourceRows prepared k hk).work ≤ k * (3 * n ^ 2 + 6 * n + 1) := by
  induction k with
  | zero => simp [sourceRows]
  | succ k ih =>
    have hs := sourceRow_work_le prepared (⟨k, by omega⟩ : Fin n)
    have hp := ih (by omega)
    simp only [sourceRows]
    nlinarithdef read (result : Result n) (i j : Fin n) : WithTop ℝ :=
  ((result.rows[i.val]?).map (fun row => vecRead row j)).getD ⊤

Stored Johnson execution for explicitly indexed vertices, with a scan priority queue.

def johnsonStored (G : WeightedGraph (Fin n)) : Result n :=
  let prepared := prepare G
  let rows := sourceRows prepared n (Nat.le_refl n)
  { rows with work := prepared.work + rows.work }

              @[simp] theorem johnsonStored_size (G : WeightedGraph (Fin n)) :
    (johnsonStored G).rows.size = n := sourceRows_size _ _ _theorem johnsonStored_read (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (i j : Fin n) :
    read (johnsonStored G) i j = G.johnsonAllPairsDist hNC i j := by
  simp only [read, johnsonStored, sourceRows_get _ n (Nat.le_refl n) i.val i.isLt,
    Option.map_some, Option.getD_some]
  exact sourceRow_read G hNC i j

theorem johnsonStored_correct (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (i j : Fin n) :
    G.IsShortestDist i j (read (johnsonStored G) i j) := by
  rw [johnsonStored_read G hNC]
  exact G.johnsonAllPairsDist_correct hNC i j

Every source has its own retained, fully materialized row.

theorem johnsonStored_row (G : WeightedGraph (Fin n)) (i : Fin n) :
    (johnsonStored G).rows[i.val]? = some (sourceRow (prepare G) i).1 :=
  sourceRows_get _ n (Nat.le_refl n) i.val i.isLt

@[simp] theorem sourceRow_width (prepared : Prepared n) (s : Fin n) :
    (sourceRow prepared s).1.cells.size = n := by
  simp [sourceRow, vector]

A specification bridge useful for finite examples, independent of Dijkstra tie choices.


theorem johnsonStored_eq_relaxDist (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle)
    (i j : Fin n) : read (johnsonStored G) i j = G.relaxDist i (n - 1) j := by
  have hs := johnsonStored_correct G hNC i j
  have hr : G.IsShortestDist i j (G.relaxDist i (n - 1) j) := by
    simpa using G.relaxDist_isShortestDist hNC i j
  have hle {a b : WithTop ℝ} (ha : G.IsShortestDist i j a)
      (hb : G.IsShortestDist i j b) : a ≤ b := by
    obtain ht | ⟨p, hp, hw⟩ := hb.2
    · rw [ht]; exact le_top
    · rw [← hw]; exact ha.1 p hp
  exact le_antisymm (hle hs hr) (hle hr hs)

              theorem johnsonStored_work_le_polynomial (G : WeightedGraph (Fin n)) :
    (johnsonStored G).work ≤ 4 * n ^ 3 + 14 * n ^ 2 + 12 * n + 4 := by
  have hs := sourceRows_work_le (prepare G) n (Nat.le_refl n)
  simp only [johnsonStored, prepare_work]
  nlinariththeorem johnsonStored_work_le (G : WeightedGraph (Fin n)) :
    (johnsonStored G).work ≤ 16 * (n + 1) ^ 3 := by
  have hs := johnsonStored_work_le_polynomial G
  nlinarith [Nat.zero_le (n ^ 3), Nat.zero_le (n ^ 2)]end CLRS.Chapter24.JohnsonExecution

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Potential

Stored Johnson preprocessing: materialize the augmented edge matrix, execute synchronous Bellman–Ford rounds, retain the potential vector, and materialize one reweighted matrix. Correctness assumes absence of negative cycles; execution does not implement a negative-cycle failure API. Counters use the indexed real-operation model of the storage primitives.

              noncomputable sectionnamespace CLRS.Chapter24.JohnsonExecutionopen MatrixExecution (Stored)def potentialPhase (G : WeightedGraph (Fin n)) : Vector × Nat :=
  let e := finSuccEquiv n
  let weights := edgeTable G.johnsonAugmentedGraph e
  let relaxed := bfLoop weights (e.symm none) n
  let potential := vector (fun v : Fin n => (vecRead relaxed.1 (e.symm (some v)), 1))
  (potential, weights.cellWrites + weights.candidateVisits + relaxed.2 + potential.writes + potential.visits)


theorem potentialPhase_read (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (v : Fin n) :
    vecRead (potentialPhase G).1 v = (G.johnsonPotential hNC v : WithTop ℝ) := by
  unfold potentialPhase
  rw [vector_read, bfLoop_read G.johnsonAugmentedGraph (finSuccEquiv n) _
    (edgeTable_read G.johnsonAugmentedGraph (finSuccEquiv n))]
  simpa using (G.johnsonPotential_eq hNC v).symm


theorem potentialPhase_work (G : WeightedGraph (Fin n)) :
    (potentialPhase G).2 = 2 * (n + 1) ^ 2 + 2 * (n + 1) +
      n * ((n + 1) * (n + 3)) + 2 * n := by
  simp only [potentialPhase, edgeTable_writes, edgeTable_visits, bfLoop_work, vector_writes]
  rw [vector_visits _ 1 (by intros; rfl)]
  ringdef reweightTable (G : WeightedGraph (Fin n)) (potential : Vector) : Stored :=
  MatrixExecution.tabulate (fun u v : Fin n =>
    (if (u, v) ∈ G.edges then (G.w u v : WithTop ℝ) + vecRead potential u - vecRead potential v else ⊤, 1))@[simp] theorem reweightTable_writes (G : WeightedGraph (Fin n)) (potential : Vector) :
    (reweightTable G potential).cellWrites = n * n := MatrixExecution.tabulate_writes _@[simp] theorem reweightTable_visits (G : WeightedGraph (Fin n)) (potential : Vector) :
    (reweightTable G potential).candidateVisits = n * n := by
  unfold reweightTable
  simpa using MatrixExecution.tabulate_visits
    (fun u v : Fin n =>
      (if (u, v) ∈ G.edges then (G.w u v : WithTop ℝ) + vecRead potential u - vecRead potential v else ⊤, 1))
    1 (by intros; rfl)structure Prepared (n : Nat) where
  potential : Vector
  weights : Stored
  work : Natdef prepare (G : WeightedGraph (Fin n)) : Prepared n :=
  let potential := potentialPhase G
  let weights := reweightTable G potential.1
  ⟨potential.1, weights, potential.2 + weights.cellWrites + weights.candidateVisits⟩@[simp] theorem prepare_potential (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (v : Fin n) :
    vecRead (prepare G).potential v = (G.johnsonPotential hNC v : WithTop ℝ) :=
  potentialPhase_read G hNC vtheorem prepare_weights (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (u v : Fin n) :
    MatrixExecution.read (prepare G).weights u v =
      if (u, v) ∈ (G.reweightedGraph (G.johnsonPotential hNC)).edges then
        ((G.reweightedGraph (G.johnsonPotential hNC)).w u v : WithTop ℝ) else ⊤ := by
  simp only [prepare, reweightTable, MatrixExecution.tabulate_read, potentialPhase_read G hNC]
  simp only [WeightedGraph.reweightedGraph, WeightedGraph.reweightedWeight]
  split <;> simp [WithTop.coe_add]theorem prepare_work (G : WeightedGraph (Fin n)) :
    (prepare G).work = n ^ 3 + 8 * n ^ 2 + 11 * n + 4 := by
  simp only [prepare, potentialPhase_work, reweightTable_writes, reweightTable_visits]
  ringend CLRS.Chapter24.JohnsonExecution

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Queue

Counted scan queue

Minimum extraction traverses an explicit queue and returns the remaining queue without its selected minimum. Its counter counts actual candidate visits. This is a linear scan queue, with no binary-heap logarithmic bound claimed.

noncomputable sectionnamespace CLRS.Chapter24.JohnsonExecution

Scan a list queue, returning its minimum and the remaining queue. Each nonempty recursive frame records one actual candidate visit.

def extractMin (d : α → WithTop ℝ) : List α → Option (α × List α) × Nat
  | [] => (none, 0)
  | x :: xs =>
      let tail := extractMin d xs
      match tail.1 with
      | none => (some (x, []), tail.2 + 1)
      | some (y, ys) =>
          if d x ≤ d y then (some (x, xs), tail.2 + 1)
          else (some (y, x :: ys), tail.2 + 1)

              @[simp] theorem extractMin_visits (d : α → WithTop ℝ) (xs : List α) :
    (extractMin d xs).2 = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    simp only [extractMin]
    split
    · simp [ih]
    · split <;> simp [ih]@[simp] theorem extractMin_none (d : α → WithTop ℝ) (xs : List α) :
    (extractMin d xs).1 = none ↔ xs = [] := by
  cases xs with
  | nil => simp [extractMin]
  | cons x xs =>
    simp only [extractMin]
    split
    · simp
    · split <;> simptheorem extractMin_spec (d : α → WithTop ℝ) (xs : List α) {u rest}
    (h : (extractMin d xs).1 = some (u, rest)) :
    xs.Perm (u :: rest) ∧ ∀ v ∈ xs, d u ≤ d v := by
  induction xs generalizing u rest with
  | nil => simp [extractMin] at h
  | cons x xs ih =>
    simp only [extractMin] at h
    split at h
    · rename_i ht
      have he := (extractMin_none d xs).mp ht
      subst xs
      have he : (x, []) = (u, rest) := Option.some.inj h
      cases he
      exact ⟨.refl _, by simp⟩
    · rename_i y ys ht
      obtain ⟨hp, hm⟩ := ih ht
      split at h
      · rename_i hxy
        have he : (x, xs) = (u, rest) := Option.some.inj h
        cases he
        refine ⟨.refl _, ?_⟩
        intro v hv
        rcases List.mem_cons.mp hv with rfl | hv
        · exact le_rfl
        · exact le_trans hxy (hm v hv)
      · rename_i hxy
        have he : (y, x :: ys) = (u, rest) := Option.some.inj h
        cases he
        refine ⟨(List.Perm.cons x hp).trans (.swap u x ys), ?_⟩
        intro v hv
        rcases List.mem_cons.mp hv with rfl | hv
        · exact le_of_lt (lt_of_not_ge hxy)
        · exact hm v hv

Build the explicit unsettled queue, counting each enumerated vertex.

def initialQueue (s : Fin n) : (k : Nat) → k ≤ n → List (Fin n) × Nat
  | 0, _ => ([], 0)
  | k + 1, hk =>
      let rest := initialQueue s k (by omega)
      let v : Fin n := ⟨k, by omega⟩
      (if v = s then rest.1 else v :: rest.1, rest.2 + 1)

              @[simp] theorem initialQueue_visits (s : Fin n) (k : Nat) (hk : k ≤ n) :
    (initialQueue s k hk).2 = k := by
  induction k with
  | zero => rfl
  | succ k ih => simp [initialQueue, ih]

theorem initialQueue_mem (s : Fin n) (k : Nat) (hk : k ≤ n) (v : Fin n) :
    v ∈ (initialQueue s k hk).1 ↔ v.val < k ∧ v ≠ s := by
  induction k with
  | zero => simp [initialQueue]
  | succ k ih =>
    simp only [initialQueue]
    split
    · rename_i he
      rw [ih]
      constructor
      · intro h; exact ⟨by omega, h.2⟩
      · rintro ⟨hv, hvs⟩
        refine ⟨?_, hvs⟩
        have hne : v.val ≠ k := by
          intro heq
          apply hvs
          exact (Fin.ext heq).trans he
        omega
    · rename_i he
      rw [List.mem_cons, ih]
      constructor
      · rintro (rfl | ⟨hv, hvs⟩)
        · exact ⟨by simp, he⟩
        · exact ⟨by omega, hvs⟩
      · rintro ⟨hv, hvs⟩
        by_cases heq : v.val = k
        · left; exact Fin.ext heq
        · right; exact ⟨by omega, hvs⟩

theorem initialQueue_nodup (s : Fin n) (k : Nat) (hk : k ≤ n) :
    (initialQueue s k hk).1.Nodup := by
  induction k with
  | zero => simp [initialQueue]
  | succ k ih =>
    simp only [initialQueue]
    split
    · exact ih _
    · rw [List.nodup_cons]
      exact ⟨by simp [initialQueue_mem], ih _⟩

theorem initialQueue_length_le (s : Fin n) (k : Nat) (hk : k ≤ n) :
    (initialQueue s k hk).1.length ≤ k := by
  induction k with
  | zero => simp [initialQueue]
  | succ k ih =>
    have hh := ih (by omega)
    simp only [initialQueue]
    split
    · exact Nat.le_trans hh (Nat.le_succ _)
    · simpa only [List.length_cons] using Nat.succ_le_succ hhend CLRS.Chapter24.JohnsonExecution

CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Storage

Stored rows and synchronous Bellman–Ford execution

Rows and edge tables are materialized before use. Every cell append and scanned candidate contributes to a counter returned by the actual loops. Bellman–Ford reads the previous stored row and a cached dense edge table; no recursive relaxation oracle is called during a round. Exact real arithmetic, graph edge/weight queries, and indexed array access are abstract primitives. The model excludes Lean finite-set membership implementation, bit costs, and persistent-array copying.

              noncomputable sectionnamespace CLRS.Chapter24.JohnsonExecutionopen CLRS.Chapter15.DPExecutionopen MatrixExecution (Stored)abbrev Vector := Row (WithTop ℝ)def vecRead (row : Vector) (i : Fin n) : WithTop ℝ := row.cells[i.val]?.getD ⊤def vector (f : Fin n → WithTop ℝ × Nat) : Vector :=
  buildRow (fun i => if hi : i < n then f ⟨i, hi⟩ else (⊤, 0)) n@[simp] theorem vector_read (f : Fin n → WithTop ℝ × Nat) (i : Fin n) :
    vecRead (vector f) i = (f i).1 := by
  simp [vecRead, vector, i.isLt]@[simp] theorem vector_writes (f : Fin n → WithTop ℝ × Nat) : (vector f).writes = n := by
  simp [vector]

theorem vector_visits (f : Fin n → WithTop ℝ × Nat) (c : Nat) (hc : ∀ i, (f i).2 = c) :
    (vector f).visits = n * c := by
  rw [vector, buildRow_visits]
  calc
    _ = ∑ _i ∈ Finset.range n, c := by
      apply Finset.sum_congr rfl
      intro i hi
      simp [Finset.mem_range.mp hi, hc]
    _ = _ := by simpvariable {V : Type} [Fintype V] [DecidableEq V]def edgeTable (G : WeightedGraph V) (e : Fin n ≃ V) : Stored :=
  MatrixExecution.tabulate (fun i j => (if (e i, e j) ∈ G.edges then (G.w (e i) (e j) : WithTop ℝ) else ⊤, 1))@[simp] theorem edgeTable_read (G : WeightedGraph V) (e : Fin n ≃ V) (i j : Fin n) :
    MatrixExecution.read (edgeTable G e) i j =
      if (e i, e j) ∈ G.edges then (G.w (e i) (e j) : WithTop ℝ) else ⊤ := by
  simp [edgeTable]@[simp] theorem edgeTable_writes (G : WeightedGraph V) (e : Fin n ≃ V) :
    (edgeTable G e).cellWrites = n * n := MatrixExecution.tabulate_writes _@[simp] theorem edgeTable_visits (G : WeightedGraph V) (e : Fin n ≃ V) :
    (edgeTable G e).candidateVisits = n * n := by
  simpa [edgeTable] using MatrixExecution.tabulate_visits
    (fun i j : Fin n => (if (e i, e j) ∈ G.edges then (G.w (e i) (e j) : WithTop ℝ) else ⊤, 1)) 1
    (by intros; rfl)def bfRound (weights : Stored) (prev : Vector) (n : Nat) : Vector :=
  vector (fun v : Fin n =>
    let candidates := MatrixExecution.scanFin (fun u : Fin n =>
      vecRead prev u + MatrixExecution.read weights u v)
    (min (vecRead prev v) candidates.1, candidates.2 + 1))@[simp] theorem bfRound_writes (weights : Stored) (prev : Vector) (n : Nat) :
    (bfRound weights prev n).writes = n := vector_writes _@[simp] theorem bfRound_visits (weights : Stored) (prev : Vector) (n : Nat) :
    (bfRound weights prev n).visits = n * (n + 1) := by
  apply vector_visits
  intro i
  simpomit [DecidableEq V] in
private theorem inf_fin_equiv (e : Fin n ≃ V) (f : V → WithTop ℝ) :
    Finset.univ.inf (fun i : Fin n => f (e i)) = Finset.univ.inf f := by
  apply le_antisymm
  · apply Finset.le_inf
    intro v _
    simpa using (Finset.inf_le (s := Finset.univ) (f := fun i : Fin n => f (e i))
      (Finset.mem_univ (e.symm v)))
  · apply Finset.le_inf
    intro i _
    exact Finset.inf_le (Finset.mem_univ (e i))

theorem bfRound_read (G : WeightedGraph V) (e : Fin n ≃ V) (weights : Stored)
    (hw : ∀ i j, MatrixExecution.read weights i j =
      if (e i, e j) ∈ G.edges then (G.w (e i) (e j) : WithTop ℝ) else ⊤)
    (prev : Vector) (d : V → WithTop ℝ) (hd : ∀ i, vecRead prev i = d (e i)) (v : Fin n) :
    vecRead (bfRound weights prev n) v = G.relaxStep d (e v) := by
  simp only [bfRound, vector_read, MatrixExecution.scanFin_value, hd, hw]
  simp_rw [add_ite, add_top]
  rw [inf_fin_equiv e (fun u => if (u, e v) ∈ G.edges then d u + (G.w u (e v) : WithTop ℝ) else ⊤)]
  simp [WeightedGraph.relaxStep, WeightedGraph.preds, Finset.inf_ite]def bfLoop (weights : Stored) (s : Fin n) : Nat → Vector × Nat
  | 0 =>
      let initial := vector (fun i : Fin n => (if i = s then 0 else ⊤, 1))
      (initial, initial.writes + initial.visits)
  | k + 1 =>
      let prev := bfLoop weights s k
      let next := bfRound weights prev.1 n
      (next, prev.2 + next.writes + next.visits)

theorem bfLoop_read (G : WeightedGraph V) (e : Fin n ≃ V) (weights : Stored)
    (hw : ∀ i j, MatrixExecution.read weights i j =
      if (e i, e j) ∈ G.edges then (G.w (e i) (e j) : WithTop ℝ) else ⊤)
    (s : Fin n) (k : Nat) (v : Fin n) :
    vecRead (bfLoop weights s k).1 v = G.relaxDist (e s) k (e v) := by
  induction k generalizing v with
  | zero => simp [bfLoop, WeightedGraph.relaxDist, e.injective.eq_iff]
  | succ k ih =>
    change vecRead (bfRound weights (bfLoop weights s k).1 n) v = _
    rw [bfRound_read G e weights hw _ (G.relaxDist (e s) k) (fun i => ?_)]
    · rfl
    · exact ih i

@[simp] theorem bfLoop_work (weights : Stored) (s : Fin n) (k : Nat) :
    (bfLoop weights s k).2 = 2 * n + k * (n * (n + 2)) := by
  induction k with
  | zero =>
    simp only [bfLoop, vector_writes]
    rw [vector_visits _ 1 (by intros; rfl)]
    omega
  | succ k ih =>
    simp only [bfLoop, bfRound_writes, bfRound_visits, ih]
    ringend CLRS.Chapter24.JohnsonExecution

Scope and implementation notes

Imports

import CLRSLean.Chapter_25
import CLRSLean.FourthEdition.Chapter_23.Section_23_1_All_Pairs_Model
import CLRSLean.FourthEdition.Chapter_23.Section_23_2_Floyd_Warshall
import CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm
import CLRSLean.FourthEdition.Chapter_23.Section_23_2_Floyd_Warshall.NegativeCycle
import CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Reindex
import CLRSLean.FourthEdition.Chapter_23.Section_23_3_Johnsons_Algorithm.Execution

Current source

Sections 23.1--23.3 are native fourth-edition sections (shortest paths and matrix multiplication, the Floyd–Warshall algorithm, and Johnson's algorithm for sparse graphs), imported directly from Section 23.1, Section 23.2, and Section 23.3. The sections extend the fourth-edition weighted-graph model (Section 22.1). Declarations retain the legacy CLRS.Chapter24.WeightedGraph namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_25 and CLRSLean.Chapter_25.Section_25_* forward to these sources.

Coverage boundary

The native sections prove valid-input shortest-path correctness. The legacy matrix initializer sets the diagonal to zero and cannot detect a negative self-edge. The cycle-safe initializer preserves those edges, and cycleFloydWarshall_negative_iff proves that a negative final diagonal is equivalent to a negative cycle, with no absence-of-negative-cycles premise. Under NoNegCycle, the corrected and legacy distance results agree.

MatrixExecution stores each completed table, shares each previous phase once, and counts actual min-plus scans and table writes. Its Floyd updates are exactly n³; repeated squaring has exactly numSquarings * n³ candidate visits. Separate counters include initial and intermediate table writes and the final n diagonal scan. An explicit vertex/index equivalence supports arbitrary finite carriers. These are exact real-arithmetic cell models, excluding enumeration construction, allocation and bit costs; the real comparisons remain noncomputable primitives in Lean.

Johnson's existing construction assumes NoNegCycle and has no negative-cycle failure result. Its heap expression is a conditional backend budget. The separate JohnsonExecution.johnsonStored over indexed graphs Fin n prepares a stored Bellman–Ford potential, caches reweighted edges, runs a stored scan queue from each source and retains every result row. Its actual counter is at most 4n³ + 14n² + 12n + 4, hence 16(n+1)³. It refines the original valid-input Johnson distances. Graph queries, indexed access and real arithmetic are primitives; finite-set lookup internals, persistent-array copying and bit costs are not included.

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 23 of 35

23.1. All-Pairs Shortest Paths Model

Lemmas 23.1 and 23.2 (squaring identity)

Stabilisation and FASTER-APSP correctness

Work-count refinement

Definitions and proofs

Finite-carrier interfaces for stored matrix execution

Stored matrices and counted min-plus products

Counted stored Floyd–Warshall and repeated squaring

23.2. The Floyd-Warshall Algorithm

Proven

Floyd-Warshall algorithm definition

Predecessor matrix Π

Path reconstruction

Walk-through-set predicate

Lemma 23.7: D bounds simple walks through ks

General lower bound via cycle removal

Attainability — every finite DP value is realized by a walk

Negative-cycle detection (CLRS Theorem 23.3)

Pi-D optimal substructure

Edge inequality for shortest-path distances

Path-reconstruction correctness

Transitive closure

Work bound: O(V³)

Definitions and proofs

Complete Floyd–Warshall negative-cycle detection

Finite-carrier interfaces for stored matrix execution

Stored matrices and counted min-plus products

Counted stored Floyd–Warshall and repeated squaring

23.3. Johnson's Algorithm for Sparse Graphs

Johnson's algorithm preliminary definitions

Reweighting with a potential function

Walk equivalence: original graph ↔ reweighted graph

Lift telescoping property to WithTop ℝ

WithTop helpers

Shortest-path preservation under reweighting

Negative-cycle equivalence for the augmented graph

Johnson potential via Bellman-Ford on the augmented graph

Triangle inequality for the Johnson potential

Nonnegativity of the reweighted graph

Johnson's all-pairs shortest paths

General triangle inequality

Johnson potential function

Nonnegative reweighted weights

Johnson all-pairs distance

End-to-end correctness

Work bound: O(V² log V + V E log V)

Definitions and proofs

Dijkstra settlement with an explicit minimum

Stored Johnson execution with an indexed scan queue

Counted scan queue

Stored rows and synchronous Bellman–Ford execution

Scope and implementation notes

Current source

Coverage boundary

Lemma 23.7: `D` bounds simple walks through `ks`