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

/-!
# HAMILTONIAN CIRCUIT

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

Hardness proof (in `HamiltonianCircuit/`): from VERTEX COVER
(`FromVertexCover.lean`, Garey–Johnson's Theorem 3.4 — a twelve-vertex
cover-testing component per edge, threaded into one chain per vertex, plus `k`
selector vertices; certified in `FromVertexCover/Code.lean` and
`FromVertexCover/Adequacy.lean`, a branching certificate).

## The predicate

Deliberately *not* mathlib's `SimpleGraph.IsHamiltonian`, which reads
`Fintype.card α ≠ 1 → ∃ a, ∃ p : G.Walk a a, p.IsHamiltonianCycle`. That guard
makes the one-vertex graph a yes-instance — a sensible convention for a graph
theory library, an edge case leaking into every gadget proof here. Under the
definition below the empty and one-vertex graphs are no-instances (no cycle is
shorter than a triangle) and the triangle is the smallest yes-instance, which
is what the reduction's degenerate branches want to emit.

The mathlib API is still what proves things about it: the reduction's forward
direction goes through `exists_isHamiltonianCycle_of_isCycles` and
`exists_isHamiltonianCycle_mono` (`Hamiltonicity.lean`), and its backward
direction through the local degree-2 forcing lemma of the same file. Note that
`Walk.IsHamiltonianCycle` carries `[DecidableEq]` in its signature; the instance
bundle supplies it.
-/

namespace Hardness

/-- HAMILTONIAN CIRCUIT: is there a cycle through every vertex exactly once? -/
def HAMILTONIAN_CIRCUIT : Problem GraphInstance :=
  fun x ↦ ∃ (a : x.V) (p : x.G.Walk a a), p.IsHamiltonianCycle

/-! ## The extreme instances

A reduction's degenerate branches need a fixed yes-instance and a fixed
no-instance to emit. Under the predicate above these are the smallest ones
available: no cycle is shorter than a triangle, so everything below three
vertices is a no-instance, and the triangle itself is a yes-instance. -/

/-- **Nothing smaller than a triangle.** A Hamiltonian circuit has length equal
to the number of vertices, and a circuit has length at least three. -/
theorem not_hamiltonianCircuit_of_card_lt_three {x : GraphInstance}
    (h : Fintype.card x.V < 3) : ¬ HAMILTONIAN_CIRCUIT x := by
  rintro ⟨a, p, hp⟩
  have h3 : 3 ≤ p.length := hp.isCycle.isCircuit.three_le_length
  rw [hp.length_eq] at h3
  omega

/-- The triangle: the smallest yes-instance. -/
def triangleInstance : GraphInstance where
  V := Fin 3
  G := ⊤

/-- The one-vertex graph: a no-instance, and the one a reduction emits when it
must say no. -/
def pointInstance : GraphInstance where
  V := Fin 1
  G := ⊥

theorem hamiltonianCircuit_triangleInstance : HAMILTONIAN_CIRCUIT triangleInstance := by
  change ∃ (a : Fin 3) (p : (⊤ : SimpleGraph (Fin 3)).Walk a a), p.IsHamiltonianCycle
  refine ⟨0, .cons (by decide : (⊤ : SimpleGraph (Fin 3)).Adj 0 1)
    (.cons (by decide : (⊤ : SimpleGraph (Fin 3)).Adj 1 2)
      (.cons (by decide : (⊤ : SimpleGraph (Fin 3)).Adj 2 0) .nil)), ?_⟩
  rw [SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq]
  exact ⟨(SimpleGraph.Walk.isCycle_def _).mpr ⟨⟨by decide⟩, by simp, by decide⟩, rfl⟩

theorem not_hamiltonianCircuit_pointInstance : ¬ HAMILTONIAN_CIRCUIT pointInstance :=
  not_hamiltonianCircuit_of_card_lt_three (by simp [pointInstance])

/-- **Renaming invariance**: having a Hamiltonian circuit transfers across a
bijection matching the two adjacency relations. The witness is transported by
`Walk.IsHamiltonianCycle.map`, which asks exactly for bijectivity. -/
theorem exists_isHamiltonianCycle_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 : V) (p : G.Walk a a), p.IsHamiltonianCycle) ↔
      ∃ (a : W) (p : H.Walk a a), p.IsHamiltonianCycle := by
  constructor
  · rintro ⟨a, p, hp⟩
    exact ⟨e a, p.map ⟨e, fun {u v} h ↦ (hadj u v).mp h⟩, hp.map e.bijective⟩
  · rintro ⟨a, p, hp⟩
    refine ⟨e.symm a, 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