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

/-!
# INDEPENDENT SET

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

Hardness proofs (in `IndepSet/`): from CLIQUE (`FromClique.lean`,
complementation; certified in `Graph/Clique/FromIndepSet/Certified.lean`,
where one program serves both directions), from VERTEX COVER
(`FromVertexCover.lean`, `k ↦ n - k`; certified in
`FromVertexCover/Certified.lean`, branchlessly), and from SAT
(`FromSat.lean`, by composition; certified in `FromSat/Certified.lean`).
-/

namespace Hardness

/-- INDEPENDENT SET: does `G` contain `k` pairwise-nonadjacent vertices? -/
def INDEPENDENT_SET : Problem GraphThresholdInstance :=
  fun x ↦ ∃ s : Finset x.V, x.G.IsIndepSet ↑s ∧ x.k ≤ s.card

/-- **Renaming invariance**: existence of an independent set of size `m`
transfers across a bijection matching the two adjacency relations. Independent
sets are cliques of the complement, and complement adjacencies also
correspond, so this is `exists_clique_iff_of_equiv` on the complements. -/
theorem exists_indepSet_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.IsIndepSet ↑s ∧ m ≤ s.card) ↔
      ∃ t : Finset W, H.IsIndepSet ↑t ∧ m ≤ t.card := by
  have h := exists_clique_iff_of_equiv (G := Gᶜ) (H := Hᶜ) e
    (fun a b ↦ by
      rw [SimpleGraph.compl_adj, SimpleGraph.compl_adj]
      exact and_congr e.apply_eq_iff_eq.not.symm (hadj a b).not) m
  simpa only [SimpleGraph.isClique_compl] using h

end Hardness