Reference · Graph algorithms

rainbow.algorithms.proofs.graph.walk-cycle-cut

Graph algorithmssrc/rainbow/algorithms/proofs/graph/walk_cycle_cut.clj0 definitions, 5 theorems

CUTTING A CYCLE OUT OF A WALK, the step of the Bellman-Ford cycle-removal lemma. A walk x of k = c + (d + a) arcs that revisits a node, x (d + a) = x a, loses the closed segment x a .. x (d + a): cut x a d = fun t. if t <= a then x t else x (t + d) (c + a arcs) If no closed walk is negative (signed/no-negative-cycles: every walk z of d arcs over nodes < n with z d = z 0 has length >= 0), the cut walk has the same ends and is no longer: signed/walk-cut-cycle : no-negative-cycles n W -> (forall t <= c + (d + a), x t < n) -> x (d + a) = x a -> (forall t <= c + a, cut t < n) /\ cut 0 = x 0 /\ cut (c + a) = x (c + (d + a)) /\ walk-length (cut, c + a) <= walk-length (x, c + (d + a)) The lengths are split with signed/expr-sum-value-append into prefix (a arcs), cycle (d arcs) and suffix (c arcs). The prefixes agree because cut = x up to a. The suffixes agree term by term because cut t = x (t + d) from a on (nat/walk-cut-shifted) and (i + a) + d = i + (d + a). The cycle is the closed walk fun t. x (t + a), so it is >= 0.

Depends onalgorithms.proofs.graph.bellman-ford-convergence-attainedmath.sums.value-append

nat/walk-shift-arith :
  (i a d : ℕ)
  → algebra/nat-add (algebra/nat-add i a) d = algebra/nat-add i (algebra/nat-add d a)

nat/walk-cut-below :
  (x : ℕ → ℕ) (a d t : ℕ)
  (ht : t ≤ a)
  → data/Bool.rec (fun x₄ => ℕ) (x (algebra/nat-add t d)) (x t) (nat/decide-at-most t a) = x t

nat/walk-cut-shifted :
  (x : ℕ → ℕ) (a d : ℕ)
  (hrep : x (algebra/nat-add d a) = x a)
  (t : ℕ)
  (ht : a ≤ t)
  → data/Bool.rec (fun x₄ => ℕ) (x (algebra/nat-add t d)) (x t) (nat/decide-at-most t a) = x (algebra/nat-add t d)

signed/walk-cut-length :
  (n : ℕ) (W : ℕ → ℕ → ℚ)
  (hneg : ∀ (z : ℕ → ℕ), ∀ (d : ℕ), ∀ (hz : ∀ (t : ℕ), ∀ (ht : t ≤ d), nat/strict-below (z t) n), ∀ (hc : z d = z 0), 0 ≤ signed/expr-sum-value (fun t => W (z t) (z (data/succ t))) d)
  (x : ℕ → ℕ) (a d c : ℕ)
  (hin : ∀ (t : ℕ), ∀ (ht : t ≤ algebra/nat-add c (algebra/nat-add d a)), nat/strict-below (x t) n)
  (hrep : x (algebra/nat-add d a) = x a)
  → signed/expr-sum-value (fun t => W ((fun t₁ => data/Bool.rec (fun x₃ => ℕ) (x (algebra/nat-add t₁ d)) (x t₁) (nat/decide-at-most t₁ a)) t) ((fun t₁ => data/Bool.rec (fun x₄ => ℕ) (x (algebra/nat-add t₁ d)) (x t₁) (nat/decide-at-most t₁ a)) (data/succ t))) (algebra/nat-add c a) ≤ signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) (algebra/nat-add c (algebra/nat-add d a))

nat/walk-cut-range :
  (n : ℕ) (x : ℕ → ℕ) (a d c : ℕ)
  (hin : ∀ (t : ℕ), ∀ (ht : t ≤ algebra/nat-add c (algebra/nat-add d a)), nat/strict-below (x t) n)
  (hrep : x (algebra/nat-add d a) = x a)
  (t : ℕ)
  (ht : t ≤ algebra/nat-add c a)
  → nat/strict-below ((fun t₁ => data/Bool.rec (fun x₂ => ℕ) (x (algebra/nat-add t₁ d)) (x t₁) (nat/decide-at-most t₁ a)) t) n