import HardnessReductions.Core
import HardnessReductions.Networks.Defs
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Logic.Equiv.Fin.Rotate

/-!
# TRAVELING SALESMAN

Is there a tour through all the cities of length at most `B`?

Hardness proof (in `TravelingSalesman/`): from HAMILTONIAN CIRCUIT
(`FromHamiltonianCircuit.lean`, Garey–Johnson [ND22] — distance `1` along the
edges of the graph and `2` everywhere else, budget the number of cities;
certified in `FromHamiltonianCircuit/Certified.lean`).

## The predicate

Garey–Johnson asks for an *ordering* `⟨c_π(1), …, c_π(m)⟩` of the cities, and
that is what the predicate says: an enumeration `σ : Fin (card V) ≃ V`, its
length the sum of the distances between consecutive cities, the tour closing
from the last back to the first. The cyclic successor is `finRotate`, not
`· + 1`: the literal `1` of `Fin n` needs a `NeZero n` instance, which an
instance whose city type might be empty cannot supply, whereas `finRotate` is
total in `n`.

That the question is about orderings rather than about walks in a graph is the
gap this entry's reduction has to cross, and it crosses it once and for all
with `exists_isHamiltonianCycle_iff_exists_equiv` (`Hamiltonicity.lean`): a
graph on three vertices or more has a Hamiltonian cycle exactly when its
vertices enumerate cyclically along adjacencies.

Under this definition the *empty* instance is a yes-instance — the empty sum is
`0` — so the instance a reduction emits to say "no" cannot be the empty one; it
is `oneCityInstance`, one city at positive distance from itself with no budget.
-/

namespace Hardness

/-- TRAVELING SALESMAN: is there an ordering of the cities whose round trip has
length at most `B`? -/
def TRAVELING_SALESMAN : Problem TSPInstance :=
  fun x ↦ ∃ σ : Fin (Fintype.card x.V) ≃ x.V,
    ∑ i, x.d (σ i) (σ (finRotate _ i)) ≤ x.B

/-- A fixed no-instance: a single city, a positive distance from itself, and no
budget at all. (The *empty* instance is a yes-instance here, its tour being the
empty sum, so this is the small no-instance a branching reduction wants.) -/
def oneCityInstance : TSPInstance where
  V := Fin 1
  d := fun _ _ ↦ 1
  dsymm := fun _ _ ↦ rfl
  B := 0

theorem not_travelingSalesman_oneCityInstance : ¬ TRAVELING_SALESMAN oneCityInstance := by
  rintro ⟨σ, hσ⟩
  simp [oneCityInstance] at hσ

/-! ## Renaming invariance

Every other entry's renaming-invariance lemma transports a *witness* — a walk,
a colouring, a set — along a bijection. This one transports the *index type* of
the witness as well: a tour is an enumeration `Fin (card V) ≃ V`, so renaming
the cities also renames the tour's positions, along `finCongr` of
`Fintype.card_congr`. `cast_finRotate` is what makes that second transport
harmless — the cyclic successor commutes with a cast of the index type — and it
is the only place in the entry where a dependent rewrite could have bitten. -/

/-- The cyclic successor commutes with a cast of the index type. -/
theorem cast_finRotate {m n : ℕ} (h : m = n) (i : Fin m) :
    Fin.cast h (finRotate m i) = finRotate n (Fin.cast h i) := by
  subst h
  rfl

/-- **Renaming invariance**, one direction: a bijection of cities matching the
distances carries a tour to a tour, its enumeration reindexed along the
induced equality of city counts. -/
theorem travelingSalesman_of_equiv {x y : TSPInstance} (e : x.V ≃ y.V)
    (hd : ∀ a b, x.d a b = y.d (e a) (e b)) (hB : x.B = y.B)
    (h : TRAVELING_SALESMAN x) : TRAVELING_SALESMAN y := by
  obtain ⟨σ, hσ⟩ := h
  have hcard : Fintype.card x.V = Fintype.card y.V := Fintype.card_congr e
  refine ⟨(finCongr hcard).symm.trans (σ.trans e), ?_⟩
  have hsum := Fintype.sum_equiv (finCongr hcard)
    (fun i ↦ x.d (σ i) (σ (finRotate _ i)))
    (fun i ↦ y.d (((finCongr hcard).symm.trans (σ.trans e)) i)
      (((finCongr hcard).symm.trans (σ.trans e)) (finRotate _ i))) (fun i ↦ ?_)
  · rw [← hsum, ← hB]
    exact hσ
  · simp only [Equiv.trans_apply, finCongr_symm, finCongr_apply, ← cast_finRotate,
      Fin.cast_cast, Fin.cast_eq_self]
    rw [hd]

/-- **Renaming invariance**: TRAVELING SALESMAN sees a city type only through
its distances. -/
theorem travelingSalesman_iff_of_equiv {x y : TSPInstance} (e : x.V ≃ y.V)
    (hd : ∀ a b, x.d a b = y.d (e a) (e b)) (hB : x.B = y.B) :
    TRAVELING_SALESMAN x ↔ TRAVELING_SALESMAN y :=
  ⟨travelingSalesman_of_equiv e hd hB,
    travelingSalesman_of_equiv e.symm
      (fun a b ↦ by rw [hd, Equiv.apply_symm_apply, Equiv.apply_symm_apply]) hB.symm⟩

end Hardness