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

/-!
# CLIQUE

Does the graph contain `k` pairwise-adjacent vertices?

Hardness proofs (in `Clique/`): from SAT (`FromSat.lean`, the occurrence
graph; certified in `FromSat/Code.lean` and `FromSat/Adequacy.lean`), from
INDEPENDENT SET (`FromIndepSet.lean`, complementation; certified in
`FromIndepSet/Certified.lean`), and from VERTEX COVER
(`FromVertexCover.lean`, by composition; certified in
`FromVertexCover/Certified.lean`).
-/

namespace Hardness

/-- CLIQUE: does `G` contain `k` pairwise-adjacent vertices? -/
def CLIQUE : Problem GraphThresholdInstance :=
  fun x ↦ ∃ s : Finset x.V, x.G.IsClique ↑s ∧ x.k ≤ s.card

/-- Existence of an `m`-clique transfers across a bijection that matches the
two adjacency relations. -/
theorem exists_clique_iff_of_equiv {V W : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (e : V ≃ W) (hadj : ∀ a b : V, G.Adj a b ↔ H.Adj (e a) (e b)) (m : ℕ) :
    (∃ s : Finset V, G.IsClique ↑s ∧ m ≤ s.card) ↔
      ∃ t : Finset W, H.IsClique ↑t ∧ m ≤ t.card := by
  constructor
  · rintro ⟨s, hs, hm⟩
    refine ⟨s.map e.toEmbedding, ?_, by rwa [Finset.card_map]⟩
    rw [Finset.coe_map]
    rintro a ⟨a', ha', rfl⟩ b ⟨b', hb', rfl⟩ hab
    exact (hadj a' b').mp (hs ha' hb' fun h ↦ hab (congrArg _ h))
  · rintro ⟨t, ht, hm⟩
    refine ⟨t.map e.symm.toEmbedding, ?_, by rwa [Finset.card_map]⟩
    rw [Finset.coe_map]
    rintro a ⟨a', ha', rfl⟩ b ⟨b', hb', rfl⟩ hab
    rw [hadj]
    have h := ht ha' hb' fun h ↦ hab (congrArg _ h)
    simpa using h

end Hardness