import HardnessReductions.Core
import HardnessReductions.Graph.Defs
import HardnessReductions.Hamiltonicity

/-!
# HAMILTONIAN PATH

Does the graph have a path visiting every vertex exactly once?

Hardness proof (in `HamiltonianPath/`): from HAMILTONIAN CIRCUIT
(`FromHamiltonianCircuit.lean`, Garey–Johnson [GT39] — split the distinguished
vertex in two and hang a pendant vertex off each half; certified in
`FromHamiltonianCircuit/Certified.lean`).

## The predicate

Mathlib's `Walk.IsHamiltonian` is a predicate on a walk with *given* ends, so
the problem quantifies over both: Garey–Johnson's GT39 asks for a Hamiltonian
path anywhere, not between prescribed endpoints. (The prescribed-endpoint
variant is a different catalog entry, and not one this reduction produces.)

Under this definition the one-vertex graph is a yes-instance — the `nil` walk
visits its vertex once — and the *empty* graph is a no-instance, there being no
vertex to start at. That asymmetry is the mirror image of HAMILTONIAN CIRCUIT's,
where everything below three vertices says no, and it is again what fixes the
degenerate branch of a reduction: the graph a reduction emits to say "no" is the
empty one.
-/

namespace Hardness

/-- HAMILTONIAN PATH: is there a path through every vertex exactly once? -/
def HAMILTONIAN_PATH : Problem GraphInstance :=
  fun x ↦ ∃ (a b : x.V) (p : x.G.Walk a b), p.IsHamiltonian

/-- The empty graph: the smallest no-instance, and the one a reduction emits
when it must say no. There is no vertex for a path to start at. -/
def emptyInstance : GraphInstance where
  V := Fin 0
  G := ⊥

theorem not_hamiltonianPath_emptyInstance : ¬ HAMILTONIAN_PATH emptyInstance := by
  rintro ⟨a, -, -, -⟩
  exact a.elim0

/-- **Renaming invariance**: having a Hamiltonian path transfers across a
bijection matching the two adjacency relations, by `Walk.IsHamiltonian.map`. -/
theorem exists_isHamiltonian_iff_of_equiv {V W : Type*} [DecidableEq V] [DecidableEq W]
    {G : SimpleGraph V} {H : SimpleGraph W} (e : V ≃ W)
    (hadj : ∀ a b : V, G.Adj a b ↔ H.Adj (e a) (e b)) :
    (∃ (a b : V) (p : G.Walk a b), p.IsHamiltonian) ↔
      ∃ (a b : W) (p : H.Walk a b), p.IsHamiltonian := by
  constructor
  · rintro ⟨a, b, p, hp⟩
    exact ⟨e a, e b, p.map ⟨e, fun {u v} h ↦ (hadj u v).mp h⟩, hp.map _ e.bijective⟩
  · rintro ⟨a, b, p, hp⟩
    refine ⟨e.symm a, e.symm b, p.map ⟨e.symm, fun {u v} h ↦ ?_⟩, hp.map _ e.symm.bijective⟩
    exact (hadj _ _).mpr (by rwa [e.apply_symm_apply, e.apply_symm_apply])

end Hardness