Costs of walks and closed walks

The traveling salesman modules measure a route through a cost function δ : α → α → W in two ways: walkCost δ a L b is the cost of the walk from a through the entries of L in order to b, and cycleCost δ t is the cost of the closed walk visiting the entries of t in order and returning to the first. A closed walk is a walk from its first vertex back to itself (cycleCost_cons), and its cost does not depend on the starting point (cycleCost_rotate).

Main definitions

• Cslib.Algorithms.Lean.TSP.walkCost: the cost of a walk through a list of vertices.
• Cslib.Algorithms.Lean.TSP.cycleCost: the cost of a closed walk.

Main results

• walkCost_append_singleton, walkCost_map: extending a walk at its end, relabeling vertices.
• cycleCost_cons: a closed walk from a is the walk from a through the rest back to a.
• cycleCost_rotate, cycleCost_append_comm: a closed walk costs the same from any starting point.

def Cslib.Algorithms.Lean.TSP.walkCost {α : Type u_1} {W : Type u_2} [Add W] (δ : α → α → W) : α → List α → α → W

The cost δ a x₀ + δ x₀ x₁ + ⋯ + δ xₖ b of the walk from a through the entries x₀, …, xₖ of L in order to b.

theorem Cslib.Algorithms.Lean.TSP.walkCost_append_singleton {α : Type u_1} {W : Type u_2} [AddSemigroup W] (δ : α → α → W) (a : α) (L : List α) (x b : α) : walkCost δ a (L ++ [x]) b = walkCost δ a L x + δ x b

Extending a walk by one vertex at its end adds one step.

theorem Cslib.Algorithms.Lean.TSP.walkCost_map {α : Type u_1} {W : Type u_2} {β : Type u_3} [Add W] (f : α → β) (δ : β → β → W) (a : α) (L : List α) (b : α) : walkCost δ (f a) (List.map f L) (f b) = walkCost (fun (x y : α) => δ (f x) (f y)) a L b

Relabeling the vertices of a walk relabels its costs.

def Cslib.Algorithms.Lean.TSP.cycleCost {α : Type u_1} (δ : α → α → ℕ) (t : List α) : ℕ

The cost of the closed walk visiting the entries of t in order and returning to the first: δ t₀ t₁ + δ t₁ t₂ + ⋯ + δ tₖ t₀. A single vertex a costs δ a a; the empty walk costs 0.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_rotate {α : Type u_1} (δ : α → α → ℕ) (t : List α) (k : ℕ) : cycleCost δ (t.rotate k) = cycleCost δ t

A closed walk costs the same from any starting point.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_append_comm {α : Type u_1} (δ : α → α → ℕ) (A X : List α) : cycleCost δ (A ++ X) = cycleCost δ (X ++ A)

A closed walk through A and then X costs the same as one through X and then A.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_pair {α : Type u_1} (δ : α → α → ℕ) (u v : α) : cycleCost δ [u, v] = δ u v + δ v u

A closed walk on two vertices goes there and back.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_cons {α : Type u_1} (δ : α → α → ℕ) (a : α) (L : List α) : cycleCost δ (a :: L) = walkCost δ a L a

A closed walk from a is the walk from a through the remaining vertices back to a.