import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
import Mathlib.Combinatorics.SimpleGraph.Matching
import HardnessReductions.Cycle

/-!
# Hamiltonicity: the upstreamable toolkit

The graph-theoretic lemmas the Hamiltonicity entries need and mathlib does not
have. What admits a lemma here is not a theme but a *status*: it mentions no
reduction, no problem and no encoding, it is stated at mathlib's own
hypotheses, and it would be at home upstream. (The file began as the
local-structure lemmas of VERTEX COVER → HAMILTONIAN CIRCUIT, Garey–Johnson
Thm 3.4; it has since taken in the path-side lemma HAMILTONIAN PATH runs on and
the enumeration bridge TSP asks for. The status is the constant, not the
subject.)

## Local structure against global cycles

Mathlib carries undirected Hamiltonicity in full
(`Walk.IsHamiltonianCycle`) and the 2-factor theory under the name
`SimpleGraph.IsCycles` (developed for Tutte's theorem, in mathlib's
`Combinatorics/SimpleGraph/Matching.lean`).
What is missing is the *bridge* in each direction between that global theory
and the two things a gadget argument needs:

* **`adj_toSubgraph_iff_of_ncard_neighborSet_eq_two`** — *local degree-2
  forcing*. If a vertex `v` has exactly two neighbours, every Hamiltonian cycle
  uses both edges at `v`. Mathlib's `Walk.IsCycle.adj_toSubgraph_iff_of_isCycles`
  proves this but hypothesizes `G.IsCycles` *globally*; the gadget analysis
  needs it from degree 2 *at the single vertex `v`*. The proof is the mathlib
  one with the global hypothesis replaced by the local cardinality.

* **`exists_isHamiltonianCycle_of_isCycles`** — *the 2-factor packaging*. A
  finite connected graph with no isolated vertex in which every non-isolated
  vertex has exactly two neighbours (`IsCycles`) has a Hamiltonian cycle. This
  turns mathlib's
  `IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp` (connected
  + `IsCycles` → a single cycle spanning the component) into the packaged
  `IsHamiltonianCycle` the reduction's forward direction produces.

* **`forall_of_closed_toSubgraph`** — *the cycle cannot be split*. A property
  closed under the cycle's own adjacency and holding somewhere holds
  everywhere. This is what refutes a gadget's *subcycle trap*: a set of
  vertices carrying all of its own cycle edges, locally consistent but
  disconnected from the rest.

* **`eq_end_of_ncard_neighborSet_le_one`** — *endpoint forcing*, the path-side
  counterpart of degree-2 forcing. A vertex with a single neighbour that lies
  on a path is one of the path's two ends, because an interior vertex of a path
  has two distinct neighbours in the path's own subgraph. This is what a
  pendant vertex is *for*: attaching one pins down where a Hamiltonian path can
  start or stop.

## Changing representation

* **`exists_isHamiltonianCycle_iff_exists_equiv`** — *cycles as cyclic
  enumerations*. A graph on three vertices or more has a Hamiltonian cycle
  exactly when its vertices can be enumerated cyclically along adjacencies.
  Mathlib has the path-level half already (`IsHamiltonian.getVertEquiv`); what
  is missing is the cyclic statement and, more to the point, its converse —
  which is where the 2-factor packaging earns its keep. This is the shape a
  problem about *orderings* of a set, as against walks in a graph, wants to be
  handed.
-/

namespace Hardness

open SimpleGraph SimpleGraph.Walk

variable {V : Type*} {G : SimpleGraph V} {v : V}

/-- **Local degree-2 forcing.** If `v` has exactly two neighbours in `G`, then a
Hamiltonian (indeed any) cycle through `v` is adjacent to `w` in its own
subgraph exactly when `G` is — i.e. it uses *both* edges at `v`. This is
`Walk.IsCycle.adj_toSubgraph_iff_of_isCycles` with the global `G.IsCycles`
hypothesis weakened to `(G.neighborSet v).ncard = 2` at the single vertex. -/
theorem adj_toSubgraph_iff_of_ncard_neighborSet_eq_two [LocallyFinite G]
    {u : V} {p : G.Walk u u}
    (hp : p.IsCycle) (hv : v ∈ p.toSubgraph.verts)
    (hv2 : (G.neighborSet v).ncard = 2) :
    ∀ w, p.toSubgraph.Adj v w ↔ G.Adj v w := by
  refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)
  have h2 := hp.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)
  rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
    ← Set.cast_ncard (SimpleGraph.Walk.finite_neighborSet_toSubgraph p), hv2, h2]

/-- **Local degree-2 forcing, in degree form.** A Hamiltonian cycle uses both
edges at any degree-2 vertex: at such a `v` the cycle's own adjacencies coincide
with `G`'s. The Hamiltonian cycle spans every vertex, so the membership
hypothesis of `adj_toSubgraph_iff_of_ncard_neighborSet_eq_two` is automatic. -/
theorem adj_toSubgraph_iff_of_degree_eq_two [DecidableEq V] [Fintype V] [DecidableRel G.Adj]
    {u : V} {p : G.Walk u u} (hp : p.IsHamiltonianCycle) (hv2 : G.degree v = 2) (w : V) :
    p.toSubgraph.Adj v w ↔ G.Adj v w := by
  have hncard : (G.neighborSet v).ncard = 2 := by
    rw [← Nat.card_coe_set_eq, Nat.card_eq_fintype_card, card_neighborSet_eq_degree, hv2]
  exact adj_toSubgraph_iff_of_ncard_neighborSet_eq_two hp.isCycle
    (p.mem_verts_toSubgraph.mpr (hp.mem_support v)) hncard w

/-- **The 2-factor packaging.** A finite connected graph with more than one
vertex in which every non-isolated vertex has exactly two neighbours
(`G.IsCycles`) has a Hamiltonian cycle. This packages mathlib's
`IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp` — connectivity
collapses the spanning cycle's component to all of `V`, and a spanning cycle is
Hamiltonian. The reduction's forward direction builds a graph of this shape and
reads off the cycle. -/
theorem exists_isHamiltonianCycle_of_isCycles [DecidableEq V] [Finite V] [Nontrivial V]
    (hcyc : G.IsCycles) (hconn : G.Connected) :
    ∃ (v : V) (p : G.Walk v v), p.IsHamiltonianCycle := by
  obtain ⟨v⟩ : Nonempty V := inferInstance
  have hne : (G.neighborSet v).Nonempty := by
    have hv : v ∈ G.support := by rw [hconn.preconnected.support_eq_univ]; trivial
    obtain ⟨w, hw⟩ := G.mem_support.mp hv
    exact ⟨w, hw⟩
  obtain ⟨p, hpc, hverts⟩ :=
    hcyc.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp
      (c := G.connectedComponentMk v) rfl hne
  have hsupp : (G.connectedComponentMk v).supp = Set.univ := by
    ext w
    simp only [ConnectedComponent.mem_supp_iff, Set.mem_univ, iff_true]
    exact ConnectedComponent.sound (hconn.preconnected w v)
  have hmem : ∀ w, w ∈ p.support := by
    intro w
    rw [← p.mem_verts_toSubgraph, hverts, hsupp]; trivial
  have htail : p.tail.IsHamiltonian := by
    refine hpc.isPath_tail.isHamiltonian_of_mem (fun w => ?_)
    rcases eq_or_ne w v with hw | hw
    · subst hw; exact p.tail.end_mem_support
    · rw [support_tail_of_not_nil p hpc.not_nil]
      have hw' := hmem w
      rw [← cons_tail_support p, List.mem_cons] at hw'
      exact hw'.resolve_left hw
  exact ⟨v, p, hpc, htail⟩

/-- **Transfer along a subgraph inclusion.** A Hamiltonian cycle of a subgraph is
a Hamiltonian cycle of the ambient graph. Mathlib proves this only for its own
`SimpleGraph.IsHamiltonian` (`IsHamiltonian.mono`), whose `Fintype.card ≠ 1`
guard we deliberately avoid; the underlying step is the same one-liner, since
`Hom.ofLE` is the identity on vertices. The reduction's forward direction builds
a cycle in the graph of the *chosen* edges and reads it in the gadget graph. -/
theorem exists_isHamiltonianCycle_mono [DecidableEq V] {H : SimpleGraph V} (hGH : G ≤ H)
    (h : ∃ (v : V) (p : G.Walk v v), p.IsHamiltonianCycle) :
    ∃ (v : V) (p : H.Walk v v), p.IsHamiltonianCycle := by
  obtain ⟨v, p, hp⟩ := h
  exact ⟨v, p.map (.ofLE hGH), hp.map Function.bijective_id⟩

/-! ## The cycle cannot be split

The other half of the local toolkit: degree-2 forcing says which edges a cycle
*must* use, and this says a set of vertices it could confine itself to does not
exist. A gadget's subcycle trap — a handful of vertices carrying all of their
own cycle edges — is refuted by exhibiting one vertex outside it. -/

/-- Propagation along a walk: a property closed under the walk's own steps and
holding at its start holds everywhere the walk goes. Stated against `edges`
rather than `toSubgraph`, which is what makes the induction a two-liner. -/
theorem forall_mem_support_of_closed_edges {P : V → Prop} :
    ∀ {u w : V} (q : G.Walk u w),
      (∀ x y, s(x, y) ∈ q.edges → P x → P y) → P u → ∀ x ∈ q.support, P x := by
  intro u w q
  induction q with
  | nil => intro _ hu x hx; rwa [List.mem_singleton.mp hx]
  | @cons u v w hadj q' ih =>
    intro hstep hu x hx
    have hv : P v := hstep u v List.mem_cons_self hu
    rcases List.mem_cons.mp hx with rfl | hx
    · exact hu
    · exact ih (fun x y he ↦ hstep x y (List.mem_cons_of_mem _ he)) hv x hx

/-- A walk's own adjacency is membership of its edge list. -/
theorem adj_toSubgraph_iff_mem_edges {u w x y : V} (q : G.Walk u w) :
    q.toSubgraph.Adj x y ↔ s(x, y) ∈ q.edges :=
  Subgraph.mem_edgeSet.symm.trans q.mem_edges_toSubgraph

/-- **A Hamiltonian cycle cannot be split.** A property closed under the cycle's
own adjacency and holding at one vertex holds at every vertex: the cycle's
adjacency is symmetric, so the complement is closed too, and the cycle's support
is everything. A gadget uses this contrapositively — a set of vertices whose
cycle edges all stay inside it must miss no vertex, which one vertex outside
refutes. -/
theorem forall_of_closed_toSubgraph [DecidableEq V] {a : V} {p : G.Walk a a}
    (hp : p.IsHamiltonianCycle) {P : V → Prop}
    (hstep : ∀ x y, p.toSubgraph.Adj x y → P x → P y) {u : V} (hu : P u) (w : V) : P w := by
  have hedge : ∀ x y, s(x, y) ∈ p.edges → P x → P y := fun x y he ↦
    hstep x y ((adj_toSubgraph_iff_mem_edges p).mpr he)
  by_cases ha : P a
  · exact forall_mem_support_of_closed_edges p hedge ha w (hp.mem_support w)
  · have hsym : ∀ x y, s(x, y) ∈ p.edges → ¬ P x → ¬ P y := by
      intro x y he hx hy
      exact hx (hedge y x (by rwa [Sym2.eq_swap]) hy)
    exact absurd hu (forall_mem_support_of_closed_edges p hsym ha u (hp.mem_support u))

/-! ## Paths: endpoint forcing, and reversal

The path-side toolkit, needed as soon as a gadget asks for a Hamiltonian *path*
rather than a circuit. Degree-2 forcing says which edges a cycle must use;
endpoint forcing says where a path must stop. -/

/-- **Endpoint forcing.** A vertex of a path with at most one neighbour in the
ambient graph is one of the path's two ends: an interior vertex is
`p.getVert i` for `0 < i < p.length`, and mathlib's
`IsPath.ncard_neighborSet_toSubgraph_internal_eq_two` gives it two distinct
neighbours already inside the path's own subgraph. -/
theorem eq_end_of_ncard_neighborSet_le_one [Finite V] {a b x : V} {p : G.Walk a b}
    (hp : p.IsPath) (hx : x ∈ p.support) (h1 : (G.neighborSet x).ncard ≤ 1) :
    x = a ∨ x = b := by
  by_contra hcon
  push Not at hcon
  obtain ⟨i, hgv, hi⟩ := SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hx
  have hi0 : i ≠ 0 := by rintro rfl; exact hcon.1 (by rw [← hgv, p.getVert_zero])
  have hil : i < p.length :=
    lt_of_le_of_ne hi (by rintro rfl; exact hcon.2 (by rw [← hgv, p.getVert_length]))
  have h2 : (p.toSubgraph.neighborSet x).ncard = 2 := by
    rw [← hgv]; exact hp.ncard_neighborSet_toSubgraph_internal_eq_two hi0 hil
  have hsub : p.toSubgraph.neighborSet x ⊆ G.neighborSet x := fun _ hy ↦ p.toSubgraph.adj_sub hy
  have := Set.ncard_le_ncard hsub (Set.toFinite _)
  omega

/-- Reversal preserves Hamiltonicity of a path: the support is reversed, and
list counts do not see the order. -/
@[simp] theorem isHamiltonian_reverse_iff [DecidableEq V] {a b : V} {p : G.Walk a b} :
    p.reverse.IsHamiltonian ↔ p.IsHamiltonian := by
  simp [SimpleGraph.Walk.IsHamiltonian, SimpleGraph.Walk.support_reverse]

/-! ## Cycles as cyclic enumerations -/

/-- **A Hamiltonian cycle is a cyclic enumeration of the vertices**, and
conversely. Forward: `p.getVert` is injective on `[0, length - 1]` for a cycle
and there are `Fintype.card V` of those, so it *is* a bijection, and consecutive
values are adjacent — the wrap-around edge being the one from `getVert (n - 1)`
to the basepoint. Backward: read the enumeration as a graph, every vertex joined
to its two neighbours in the cyclic order; it is connected and `IsCycles` by
construction, so the 2-factor packaging above returns a Hamiltonian cycle of it,
and it is a subgraph of `G`.

The successor is `finRotate`, which is total in `n` — `· + 1` would need a
`NeZero` hypothesis to write down, and the problem this lemma serves (TSP's
tours) cannot supply one. Three vertices are needed in both directions: with
two, a single edge enumerates cyclically, crossed once each way, without being
a cycle. -/
theorem exists_isHamiltonianCycle_iff_exists_equiv [Fintype V] [DecidableEq V]
    (h3 : 3 ≤ Fintype.card V) :
    (∃ (a : V) (p : G.Walk a a), p.IsHamiltonianCycle) ↔
      ∃ σ : Fin (Fintype.card V) ≃ V, ∀ i, G.Adj (σ i) (σ (finRotate _ i)) := by
  constructor
  · rintro ⟨a, p, hp⟩
    have hlen : p.length = Fintype.card V := hp.length_eq
    have hinj : Function.Injective (fun i : Fin (Fintype.card V) ↦ p.getVert i.val) := by
      intro i j hij
      exact Fin.val_injective (hp.isCycle.getVert_injOn'
        (by simp only [Set.mem_setOf_eq]; omega) (by simp only [Set.mem_setOf_eq]; omega) hij)
    have hbij : Function.Bijective (fun i : Fin (Fintype.card V) ↦ p.getVert i.val) :=
      (Fintype.bijective_iff_injective_and_card _).mpr ⟨hinj, by simp⟩
    refine ⟨Equiv.ofBijective _ hbij, fun i ↦ ?_⟩
    change G.Adj (p.getVert i.val) (p.getVert (finRotate _ i).val)
    rw [val_finRotate]
    split_ifs with hlast
    · have h1 := p.adj_getVert_succ (i := i.val) (by omega)
      rw [show i.val + 1 = p.length from by omega, p.getVert_length] at h1
      rw [p.getVert_zero]
      exact h1
    · exact p.adj_getVert_succ (by omega)
  · rintro ⟨σ, hσ⟩
    classical
    have hrot : ∀ i : Fin (Fintype.card V), finRotate _ i ≠ i := by
      intro i hc
      have h1 := congrArg Fin.val hc
      rw [val_finRotate] at h1
      have hi := i.isLt
      split_ifs at h1 <;> omega
    have hrot2 : ∀ i : Fin (Fintype.card V), (finRotate _).symm i ≠ finRotate _ i := by
      intro i hc
      have h1 := congrArg (finRotate (Fintype.card V)) hc
      rw [Equiv.apply_symm_apply] at h1
      have h2 := congrArg Fin.val h1
      rw [val_finRotate, val_finRotate] at h2
      have hi := i.isLt
      split_ifs at h2 <;> omega
    set H : SimpleGraph V :=
      SimpleGraph.fromRel
        (fun u v ↦ ∃ i : Fin (Fintype.card V), u = σ i ∧ v = σ (finRotate _ i)) with hH
    have hHG : H ≤ G := by
      intro u v huv
      rw [hH, fromRel_adj] at huv
      rcases huv.2 with ⟨i, rfl, rfl⟩ | ⟨i, rfl, rfl⟩
      · exact hσ i
      · exact (hσ i).symm
    have hadjH : ∀ i : Fin (Fintype.card V), H.Adj (σ i) (σ (finRotate _ i)) := by
      intro i
      rw [hH, fromRel_adj]
      exact ⟨fun hc ↦ hrot i (σ.injective hc.symm), Or.inl ⟨i, rfl, rfl⟩⟩
    have hnb : ∀ i : Fin (Fintype.card V),
        H.neighborSet (σ i) = {σ ((finRotate _).symm i), σ (finRotate _ i)} := by
      intro i
      ext v
      simp only [SimpleGraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
      constructor
      · intro hadj
        rw [hH, fromRel_adj] at hadj
        rcases hadj.2 with ⟨j, hj, rfl⟩ | ⟨j, rfl, hj⟩
        · rw [σ.injective hj]
          exact Or.inr rfl
        · refine Or.inl ?_
          rw [σ.injective hj, Equiv.symm_apply_apply]
      · rintro (rfl | rfl)
        · have := (hadjH ((finRotate _).symm i)).symm
          rwa [Equiv.apply_symm_apply] at this
        · exact hadjH i
    have hcyc : H.IsCycles := by
      intro v _
      obtain ⟨i, rfl⟩ : ∃ i, σ i = v := ⟨σ.symm v, σ.apply_symm_apply v⟩
      rw [hnb i]
      exact Set.ncard_pair fun hc ↦ hrot2 i (σ.injective hc)
    have h0 : 0 < Fintype.card V := by omega
    have hreach : ∀ (k : ℕ) (hk : k < Fintype.card V),
        H.Reachable (σ ⟨0, h0⟩) (σ ⟨k, hk⟩) := by
      intro k
      induction k with
      | zero => intro _; exact Reachable.refl _
      | succ k ih =>
        intro hk
        have hk' : k < Fintype.card V := by omega
        have hstep : finRotate _ (⟨k, hk'⟩ : Fin (Fintype.card V)) = ⟨k + 1, hk⟩ := by
          apply Fin.val_injective
          rw [val_finRotate]
          change (if k + 1 = Fintype.card V then 0 else k + 1) = k + 1
          exact if_neg (by omega)
        have hstepr := (hadjH ⟨k, hk'⟩).reachable
        rw [hstep] at hstepr
        exact (ih hk').trans hstepr
    haveI : Nonempty V := ⟨σ ⟨0, h0⟩⟩
    have hconn : H.Connected := by
      refine ⟨fun u v ↦ ?_⟩
      have key : ∀ w : V, H.Reachable (σ ⟨0, h0⟩) w := by
        intro w
        obtain ⟨i, rfl⟩ : ∃ i, σ i = w := ⟨σ.symm w, σ.apply_symm_apply w⟩
        simpa using hreach i.val i.isLt
      exact (key u).symm.trans (key v)
    have : Nontrivial V := Fintype.one_lt_card_iff_nontrivial.mp (by omega)
    exact exists_isHamiltonianCycle_mono hHG (exists_isHamiltonianCycle_of_isCycles hcyc hconn)

end Hardness