import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
import HardnessReductions.Core
import HardnessReductions.Graph.Defs

/-!
# Graph colorability

Garey–Johnson's GRAPH K-COLORABILITY [GT4]: can the vertices be painted with
`K` colors so that no edge is monochromatic? The instance is a graph together
with a number, so `GraphThresholdInstance` serves unchanged — here the
threshold `k` *is* the number of colors. This is the `SetSystemInstance`
situation: several catalog entries asking different questions of one
Garey–Johnson instance, sharing one instance type and one encoding.

3-COLORABILITY is the restriction `k = 3`. It has its own identity in the
literature, so it is a catalog entry rather than a footnote, exactly as 3SAT
is (`Logic/Sat3.lean`), and for the same reason: it is what later reductions
start from.

Hardness proof (in `Colorability3/`): from SAT (`FromSat.lean`, the palette /
variable / chained-OR gadget; certified in `FromSat/Code.lean` and
`FromSat/Adequacy.lean`). K-COLORABILITY is then hard by weakening, along
`threeColorToColorability` below.

## What this file supplies that mathlib does not

mathlib defines `SimpleGraph.Colorable n` as `Nonempty (G.Coloring (Fin n))`,
a bundled hom into a complete graph. It has no lemma putting that in the form
a gadget reduction argues with — a bare function `V → Fin n` separating
adjacent vertices — so `colorable_iff_exists_fun` states it here. Both
directions are one-liners; the value is having one name for the passage, since
every proof about a constructed graph crosses it twice.

`colorable_iff_of_equiv` is the renaming-invariance lemma every catalog entry
owes its future gadgets: it is what lets a certificate transport a
tagged construction onto positions (compare `matching3D_iff_of_equiv`,
`exactCover3_iff_of_equiv`). mathlib's `colorable_congr` wants a
`SimpleGraph.Iso`; callers here have an `Equiv` on vertices plus an adjacency
correspondence, and building the iso by hand at each use site is noise.
-/

namespace Hardness

open SimpleGraph

/-! ### Colorings as plain functions -/

/-- Colorability in the form gadget reductions argue with: a bare function to
`Fin n` that separates adjacent vertices. mathlib's `Colorable` bundles a
graph hom instead; this is the same statement with the bundling removed. -/
theorem colorable_iff_exists_fun {V : Type*} (G : SimpleGraph V) (n : ℕ) :
    G.Colorable n ↔ ∃ f : V → Fin n, ∀ u v, G.Adj u v → f u ≠ f v := by
  constructor
  · rintro ⟨C⟩
    exact ⟨⇑C, fun _ _ h ↦ C.valid h⟩
  · rintro ⟨f, hf⟩
    exact ⟨Coloring.mk f fun {u v} h ↦ hf u v h⟩

/-- **Renaming invariance**: colorability sees only the adjacency structure, so
it transports along any vertex bijection matching the two adjacency relations.

Stated with the correspondence as a hypothesis rather than as a
`SimpleGraph.Iso`, because that is the form gadget certificates produce: a
positional numbering of tagged vertex names, shown bijective, plus a lemma
saying which pairs of positions the decoded graph joins. -/
theorem colorable_iff_of_equiv {V W : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (e : V ≃ W) (he : ∀ u v : V, G.Adj u v ↔ H.Adj (e u) (e v)) (n : ℕ) :
    G.Colorable n ↔ H.Colorable n := by
  rw [colorable_iff_exists_fun, colorable_iff_exists_fun]
  constructor
  · rintro ⟨f, hf⟩
    refine ⟨fun w ↦ f (e.symm w), fun a b hab ↦ hf _ _ ?_⟩
    rw [he]
    rwa [e.apply_symm_apply, e.apply_symm_apply]
  · rintro ⟨g, hg⟩
    exact ⟨fun v ↦ g (e v), fun u v huv ↦ hg _ _ ((he u v).mp huv)⟩

/-! ### The problems -/

/-- GRAPH K-COLORABILITY [GT4]: can `G` be properly coloured with `k` colours?
The threshold field of the instance carries the number of colours. -/
def GRAPH_COLORABILITY : Problem GraphThresholdInstance :=
  fun x ↦ x.G.Colorable x.k

/-- GRAPH 3-COLORABILITY: K-COLORABILITY restricted to three colours, in the
promise-free formulation of `Problem.restrict` — an instance carrying any other
`k` is simply a no-instance, so `GRAPH_3_COLORABILITY` is a problem over
arbitrary `GraphThresholdInstance`s. -/
def GRAPH_3_COLORABILITY : Problem GraphThresholdInstance :=
  GRAPH_COLORABILITY.restrict fun x ↦ x.k = 3

/-- A fixed no-instance of K-COLORABILITY: one vertex, no colours. -/
def noColorInstance : GraphThresholdInstance where
  V := Unit
  G := ⊥
  k := 0

/-- Nothing with a vertex is colourable with zero colours. -/
theorem not_colorability_noColorInstance : ¬ GRAPH_COLORABILITY noColorInstance := by
  intro h
  exact (colorable_zero_iff.mp h).elim ()

/-- 3-COLORABILITY is a special case of K-COLORABILITY: hardness-even-if
implies plain hardness. As with `sat3ToSat`, the map is not the identity —
instances carrying a `k` other than three go to a fixed no-instance. -/
def threeColorToColorability : GRAPH_3_COLORABILITY ⟶ᵣ GRAPH_COLORABILITY :=
  Reduction.ofRestrict _ noColorInstance not_colorability_noColorInstance

end Hardness