import Mathlib.Combinatorics.SimpleGraph.Partition
import Mathlib.Combinatorics.SimpleGraph.Clique
import HardnessReductions.Core
import HardnessReductions.Graph.Defs
import HardnessReductions.Graph.Colorability

/-!
# Graph clique cover

Garey–Johnson's PARTITION INTO CLIQUES [GT15], usually called GRAPH CLIQUE
COVER: can the vertices be split into at most `k` groups, each of which is a
clique? The instance is a graph together with a number, so
`GraphThresholdInstance` serves unchanged — the third catalog entry asking a
question of that one Garey–Johnson instance, after K-COLORABILITY and CLIQUE.

Hardness proof (in `CliqueCover/`): from K-COLORABILITY
(`FromColorability.lean`, complementation; certified in
`FromColorability/Certified.lean`), and hence from 3-COLORABILITY and from SAT
by composition.

## Why complementation is the whole reduction

A clique of `G` is an independent set of `Gᶜ` and conversely, so a partition
of the vertices into cliques of `G` *is* a partition into independent sets of
`Gᶜ` — and a partition into at most `k` independent sets is exactly a
`k`-colouring. Both halves of that sentence are already in mathlib
(`isIndepSet_compl`, `partitionable_iff_colorable`), so the mathematical
content of this file is one lemma with no combinatorial argument in it.

The definition below spells the partition out rather than being *defined* as
`Gᶜ.Colorable k`. That would make the reduction true by definition and prove
nothing: a catalog entry has to say what the literature says the problem is,
and the passage to colouring is then a theorem worth stating.
-/

namespace Hardness

open SimpleGraph

/-! ### The predicate -/

/-- `G` has a clique cover of size at most `n`: its vertices can be partitioned
into at most `n` cliques. The partition is a set of parts, as in mathlib's
`SimpleGraph.Partition`, and `Setoid.IsPartition` is what makes the parts
nonempty, pairwise disjoint and exhaustive. -/
def CliqueCoverable {V : Type*} (G : SimpleGraph V) (n : ℕ) : Prop :=
  ∃ P : Set (Set V), Setoid.IsPartition P ∧ (∀ s ∈ P, G.IsClique s) ∧
    ∃ h : P.Finite, h.toFinset.card ≤ n

/-- **A clique cover of `G` is a colouring of `Gᶜ`.** Cliques of `G` are
exactly independent sets of `Gᶜ` (`isIndepSet_compl`), and a partition into at
most `n` independent sets is exactly an `n`-colouring
(`partitionable_iff_colorable`). -/
theorem cliqueCoverable_iff_colorable_compl {V : Type*} (G : SimpleGraph V) (n : ℕ) :
    CliqueCoverable G n ↔ Gᶜ.Colorable n := by
  rw [← SimpleGraph.partitionable_iff_colorable]
  constructor
  · rintro ⟨P, hP, hcl, hfin, hcard⟩
    exact ⟨⟨P, hP, fun s hs ↦ (isIndepSet_compl G).mpr (hcl s hs)⟩, hfin, hcard⟩
  · rintro ⟨⟨P, hP, hind⟩, hfin, hcard⟩
    exact ⟨P, hP, fun s hs ↦ (isIndepSet_compl G).mp (hind s hs), hfin, hcard⟩

/-- Clique cover is invariant under renaming the vertices: the lemma every
gadget certificate into this problem transports along. -/
theorem cliqueCoverable_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 : ℕ) :
    CliqueCoverable G n ↔ CliqueCoverable H n := by
  rw [cliqueCoverable_iff_colorable_compl, cliqueCoverable_iff_colorable_compl]
  refine colorable_iff_of_equiv e (fun u v ↦ ?_) n
  rw [compl_adj, compl_adj, he]
  exact and_congr_left' (Iff.symm e.apply_eq_iff_eq.not)

/-! ### The problem -/

/-- GRAPH CLIQUE COVER [GT15]: can `G`'s vertices be partitioned into at most
`k` cliques? The threshold field of the instance carries the number of
cliques. -/
def GRAPH_CLIQUE_COVER : Problem GraphThresholdInstance :=
  fun x ↦ CliqueCoverable x.G x.k

end Hardness