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

/-!
# VERTEX COVER

Is there a set of at most `k` vertices meeting every edge?

Hardness proofs (in `VertexCover/`): from INDEPENDENT SET
(`FromIndepSet.lean`, `k ↦ n - k`; certified in
`FromIndepSet/Certified.lean`) and from SAT (`FromSat.lean`, by composition;
certified in `FromSat/Certified.lean`).

Restriction: hard even on graphs of maximum degree at most three
(`VertexCover/BoundedDegree.lean`).
-/

namespace Hardness

/-- VERTEX COVER: is there a set of at most `k` vertices meeting every edge? -/
def VERTEX_COVER : Problem GraphThresholdInstance :=
  fun x ↦ ∃ s : Finset x.V, x.G.IsVertexCover ↑s ∧ s.card ≤ x.k

/-- Vertex covers, quantified over *edges* rather than over adjacent pairs.
Mathlib states `IsVertexCover` as a condition on `G.Adj v w`; every reduction
that turns edges into set-system items (`Sets/SetCover/FromVertexCover.lean`,
`Sets/HittingSet/FromVertexCover.lean`) wants the edge-indexed form instead. -/
theorem isVertexCover_iff_forall_edge {V : Type*} {G : SimpleGraph V} {c : Set V} :
    G.IsVertexCover c ↔ ∀ e ∈ G.edgeSet, ∃ v ∈ c, v ∈ e := by
  constructor
  · intro hc e
    induction e with
    | _ a b =>
      intro he
      rcases hc (G.mem_edgeSet.mp he) with h | h
      · exact ⟨a, h, Sym2.mem_mk_left a b⟩
      · exact ⟨b, h, Sym2.mem_mk_right a b⟩
  · intro h a b hadj
    obtain ⟨v, hv, hve⟩ := h s(a, b) (G.mem_edgeSet.mpr hadj)
    rcases Sym2.mem_iff.mp hve with rfl | rfl
    · exact Or.inl hv
    · exact Or.inr hv

/-- **Renaming invariance**: existence of a vertex cover of size at most `m`
transfers across a bijection matching the two adjacency relations. A
minimization target, so transporting the cover needs only `Finset.card_map`,
no injectivity argument. -/
theorem exists_vertexCover_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.IsVertexCover ↑s ∧ s.card ≤ m) ↔
      ∃ t : Finset W, H.IsVertexCover ↑t ∧ t.card ≤ m := by
  constructor
  · rintro ⟨s, hs, hm⟩
    refine ⟨s.map e.toEmbedding, fun a b hab ↦ ?_, by rwa [Finset.card_map]⟩
    have h := hs ((hadj (e.symm a) (e.symm b)).mpr
      (by rwa [e.apply_symm_apply, e.apply_symm_apply]))
    rcases h with h | h
    · exact Or.inl (by simpa using Finset.mem_map_of_mem e.toEmbedding h)
    · exact Or.inr (by simpa using Finset.mem_map_of_mem e.toEmbedding h)
  · rintro ⟨t, ht, hm⟩
    refine ⟨t.map e.symm.toEmbedding, fun a b hab ↦ ?_, by rwa [Finset.card_map]⟩
    have h := ht ((hadj a b).mp hab)
    rcases h with h | h
    · exact Or.inl (by simpa using Finset.mem_map_of_mem e.symm.toEmbedding h)
    · exact Or.inr (by simpa using Finset.mem_map_of_mem e.symm.toEmbedding h)

end Hardness