Reference · Graph algorithms

rainbow.algorithms.proofs.graph.dijkstra-invariant

Graph algorithmssrc/rainbow/algorithms/proofs/graph/dijkstra_invariant.clj0 definitions, 7 theorems

DIJKSTRA'S INVARIANT (the Dijkstra step family's Level-3 half). Labels L(t, v), settled flags s(t, v) that are 0 or 1 (settled when s ~ 1), chosen nodes p t, and NONNEGATIVE weights W on n nodes. Each iteration satisfies (from signed/dijkstra-step-reading): R1 p < n R2 s(t, p) ~ 0 R3 s(t, j) ~ 0 -> L(t, p) <= L(t, j) (argmin of the unsettled) R4 s(t+1, j) ~ 1 -> s(t, j) ~ 1 \/ j = p R5 s(t+1, j) ~ 0 -> s(t, j) ~ 0 /\ j /= p R6 L(t+1, j) <= L(t, j) R7 L(t+1, j) <= L(t, p) + W(p, j) R8 L(t+1, j) ~ L(t, j) \/ L(t+1, j) ~ L(t, p) + W(p, j) The invariant, for every t reached through such rounds from a start with nothing settled and L(0, 0) <= 0: A settled u: L(t, u) <= the length of every walk 0 -> u (settled labels are final) C settled u: L(t, v) <= L(t, u) + W(u, v) for every v (their arcs are relaxed) D settled u, unsettled v: L(t, u) <= L(t, v) (settled below unsettled) S L(t, 0) <= 0 signed/dijkstra-walk-bound, derived from C by induction on the walk: every walk from 0 whose nodes before the last are settled bounds the label at its end. The new node's label is FINAL: a walk to p first leaves the settled set at some x f (nat/least-witness), and L(t, p) <= L(t, x f) <= prefix <= whole walk, by argmin, the walk bound and nonnegative weights. Settled labels never change (R8 with W >= 0 and D), which keeps C.

Depends onalgorithms.proofs.graph.walk-cycle-cutmath.nat.extremal-indexmath.sums.value-append

signed/dijkstra-walk-bound :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (t : ℕ)
  (hc : ∀ (u : ℕ), ∀ (hu : nat/strict-below u n), ∀ (hsu : s t u = 1), ∀ (v : ℕ), ∀ (hv : nat/strict-below v n), L t v ≤ L t u + W u v)
  (hsrc : L t 0 ≤ 0)
  (x : ℕ → ℕ)
  (hx0 : x 0 = 0)
  (k : ℕ) (hin : ∀ (tr : ℕ), ∀ (htr : tr ≤ k), nat/strict-below (x tr) n)
  (hset : ∀ (ps : ℕ), ∀ (hps : nat/strict-below ps k), s t (x ps) = 1)
  → L t (x k) ≤ signed/expr-sum-value (fun ta => W (x ta) (x (data/succ ta))) k

signed/dijkstra-stable :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ) (t : ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hR1 : nat/strict-below (P t) n)
  (hR2 : s t (P t) = 0)
  (hR3 : ∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3)
  (hR4 : ∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t))
  (hR5 : ∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity))
  (hR6 : ∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6)
  (hR7 : ∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (P t) + W (P t) j7)
  (hR8 : ∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (data/succ t) j8 = L t j8) (L (data/succ t) j8 = L t (P t) + W (P t) j8))
  (hD : ∀ (ou : ℕ), ∀ (hou : nat/strict-below ou n), ∀ (hso : s t ou = 1), ∀ (ov : ℕ), ∀ (hov : nat/strict-below ov n), ∀ (huo : s t ov = 0), L t ou ≤ L t ov)
  (u : ℕ) (hu : nat/strict-below u n)
  (hsu : proposition/disjunction (s t u = 1) (u = P t))
  → L t u ≤ L (data/succ t) u

signed/dijkstra-relaxed-step :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ) (t : ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hR1 : nat/strict-below (P t) n)
  (hR2 : s t (P t) = 0)
  (hR3 : ∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3)
  (hR4 : ∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t))
  (hR5 : ∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity))
  (hR6 : ∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6)
  (hR7 : ∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (P t) + W (P t) j7)
  (hR8 : ∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (data/succ t) j8 = L t j8) (L (data/succ t) j8 = L t (P t) + W (P t) j8))
  (hC : ∀ (u : ℕ), ∀ (hu : nat/strict-below u n), ∀ (hsu : s t u = 1), ∀ (v : ℕ), ∀ (hv : nat/strict-below v n), L t v ≤ L t u + W u v)
  (hD : ∀ (ou : ℕ), ∀ (hou : nat/strict-below ou n), ∀ (hso : s t ou = 1), ∀ (ov : ℕ), ∀ (hov : nat/strict-below ov n), ∀ (huo : s t ov = 0), L t ou ≤ L t ov)
  (u : ℕ) (hu : nat/strict-below u n)
  (hsu : s (data/succ t) u = 1)
  (v : ℕ) (hv : nat/strict-below v n)
  → L (data/succ t) v ≤ L (data/succ t) u + W u v

signed/dijkstra-order-step :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ) (t : ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hR1 : nat/strict-below (P t) n)
  (hR2 : s t (P t) = 0)
  (hR3 : ∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3)
  (hR4 : ∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t))
  (hR5 : ∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity))
  (hR6 : ∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6)
  (hR7 : ∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (P t) + W (P t) j7)
  (hR8 : ∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (data/succ t) j8 = L t j8) (L (data/succ t) j8 = L t (P t) + W (P t) j8))
  (hD : ∀ (ou : ℕ), ∀ (hou : nat/strict-below ou n), ∀ (hso : s t ou = 1), ∀ (ov : ℕ), ∀ (hov : nat/strict-below ov n), ∀ (huo : s t ov = 0), L t ou ≤ L t ov)
  (ou : ℕ) (hou : nat/strict-below ou n)
  (hso : s (data/succ t) ou = 1)
  (ov : ℕ) (hov : nat/strict-below ov n)
  (huo : s (data/succ t) ov = 0)
  → L (data/succ t) ou ≤ L (data/succ t) ov

signed/dijkstra-source-step :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ) (t : ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hR1 : nat/strict-below (P t) n)
  (hR2 : s t (P t) = 0)
  (hR3 : ∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3)
  (hR4 : ∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t))
  (hR5 : ∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity))
  (hR6 : ∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6)
  (hR7 : ∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (P t) + W (P t) j7)
  (hR8 : ∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (data/succ t) j8 = L t j8) (L (data/succ t) j8 = L t (P t) + W (P t) j8))
  (hS : L t 0 ≤ 0)
  → L (data/succ t) 0 ≤ 0

signed/dijkstra-final-step :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ) (t : ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hR1 : nat/strict-below (P t) n)
  (hR2 : s t (P t) = 0)
  (hR3 : ∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3)
  (hR4 : ∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t))
  (hR5 : ∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity))
  (hR6 : ∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6)
  (hR7 : ∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (P t) + W (P t) j7)
  (hR8 : ∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (data/succ t) j8 = L t j8) (L (data/succ t) j8 = L t (P t) + W (P t) j8))
  (hA : ∀ (fu : ℕ), ∀ (hfu : nat/strict-below fu n), ∀ (hsf : s t fu = 1), ∀ (fk : ℕ), ∀ (fx : ℕ → ℕ), ∀ (hf0 : fx 0 = 0), ∀ (hfin : ∀ (tr : ℕ), ∀ (htr : tr ≤ fk), nat/strict-below (fx tr) n), ∀ (hfk : fx fk = fu), L t fu ≤ signed/expr-sum-value (fun ta => W (fx ta) (fx (data/succ ta))) fk)
  (hC : ∀ (u : ℕ), ∀ (hu : nat/strict-below u n), ∀ (hsu : s t u = 1), ∀ (v : ℕ), ∀ (hv : nat/strict-below v n), L t v ≤ L t u + W u v)
  (hS : L t 0 ≤ 0)
  (h01 : ∀ (zv : ℕ), ∀ (hzv : nat/strict-below zv n), proposition/disjunction (s t zv = 0) (s t zv = 1))
  (fu : ℕ) (hfu : nat/strict-below fu n)
  (hsf : s (data/succ t) fu = 1)
  (fk : ℕ) (fx : ℕ → ℕ)
  (hf0 : fx 0 = 0)
  (hfin : ∀ (tr : ℕ), ∀ (htr : tr ≤ fk), nat/strict-below (fx tr) n)
  (hfk : fx fk = fu)
  → L (data/succ t) fu ≤ signed/expr-sum-value (fun ta => W (fx ta) (fx (data/succ ta))) fk

signed/dijkstra-invariant :
  (n : ℕ) (W L s : ℕ → ℕ → ℚ) (P : ℕ → ℕ)
  (hW : ∀ (wu : ℕ), ∀ (hwu : nat/strict-below wu n), ∀ (wv : ℕ), ∀ (hwv : nat/strict-below wv n), 0 ≤ W wu wv)
  (hbase : ∀ (bv : ℕ), ∀ (hbv : nat/strict-below bv n), s 0 bv = 0)
  (hsrc : L 0 0 ≤ 0)
  (r : ℕ)
  (hr : ∀ (t : ℕ), ∀ (ht : nat/strict-below t r), proposition/conjunction (nat/strict-below (P t) n) (proposition/conjunction (s t (P t) = 0) (proposition/conjunction (∀ (j3 : ℕ), ∀ (hj3 : nat/strict-below j3 n), ∀ (hu3 : s t j3 = 0), L t (P t) ≤ L t j3) (proposition/conjunction (∀ (j4 : ℕ), ∀ (hj4 : nat/strict-below j4 n), ∀ (hs4 : s (data/succ t) j4 = 1), proposition/disjunction (s t j4 = 1) (j4 = P t)) (proposition/conjunction (∀ (j5 : ℕ), ∀ (hj5 : nat/strict-below j5 n), ∀ (hu5 : s (data/succ t) j5 = 0), proposition/conjunction (s t j5 = 0) (j5 = P t → proposition/falsity)) (proposition/conjunction (∀ (j6 : ℕ), ∀ (hj6 : nat/strict-below j6 n), L (data/succ t) j6 ≤ L t j6) (proposition/conjunction (∀ (j7 : ℕ), ∀ (hj7 : nat/strict-below j7 n), L (data/succ t) j7 ≤ L t (…⟨1⟩ …⟨1⟩) + W (…⟨1⟩ …⟨1⟩) j7) (∀ (j8 : ℕ), ∀ (hj8 : nat/strict-below j8 n), proposition/disjunction (L (…⟨1⟩ …⟨1⟩) j8 = L t j8) (L (…⟨1⟩ …⟨1⟩) j8 = …⟨1⟩ …⟨1⟩ …⟨3⟩ + …⟨1⟩ …⟨3⟩ …⟨1⟩)))))))))
  (h01 : ∀ (t : ℕ), ∀ (ht : nat/strict-below t r), ∀ (zv : ℕ), ∀ (hzv : nat/strict-below zv n), proposition/disjunction (s t zv = 0) (s t zv = 1))
  → proposition/conjunction (∀ (fu : ℕ), ∀ (hfu : nat/strict-below fu n), ∀ (hsf : s r fu = 1), ∀ (fk : ℕ), ∀ (fx : ℕ → ℕ), ∀ (hf0 : fx 0 = 0), ∀ (hfin : ∀ (tr : ℕ), ∀ (htr : tr ≤ fk), nat/strict-below (fx tr) n), ∀ (hfk : fx fk = fu), L r fu ≤ signed/expr-sum-value (fun ta => W (fx ta) (fx (…⟨1⟩ …⟨1⟩))) fk) (conjunction)
  where conjunction := proposition/conjunction (∀ (u : ℕ), ∀ (hu : nat/strict-below u n), ∀ (hsu : s r u = 1), ∀ (v : ℕ), ∀ (hv : nat/strict-below v n), L r v ≤ L r u + W u v) (proposition/conjunction (∀ (ou : ℕ), ∀ (hou : nat/strict-below ou n), ∀ (hso : s r ou = 1), ∀ (ov : ℕ), ∀ (hov : nat/strict-below ov n), ∀ (huo : s r ov = 0), L r ou ≤ L r ov) (L r 0 ≤ 0))