import HardnessReductions.Core
import HardnessReductions.Graph.Defs

/-!
# DOMINATING SET

Is there a set of at most `k` vertices such that every vertex either belongs
to the set or is adjacent to a member?

Mathlib has no dominating-set theory, so the predicate is defined here.

Hardness proof (in `DominatingSet/`): from VERTEX COVER
(`FromVertexCover.lean`, the edge-vertex gadget with the isolated-vertex
correction `k ↦ k + #isolated`; certified in
`FromVertexCover/Certified.lean`, where the argument is redone directly on
concrete graphs because duplicate edges rule out transporting it).
-/

namespace Hardness

/-- A set of vertices dominating the graph: every vertex is in the set or
adjacent to a member. -/
def IsDominatingSet {V : Type*} (G : SimpleGraph V) (s : Finset V) : Prop :=
  ∀ v, ∃ u ∈ s, u = v ∨ G.Adj u v

/-- DOMINATING SET: is there a set of at most `k` vertices dominating the
graph? -/
def DOMINATING_SET : Problem GraphThresholdInstance :=
  fun x ↦ ∃ s : Finset x.V, IsDominatingSet x.G s ∧ s.card ≤ x.k

/-- **Renaming invariance**: existence of a dominating set of size at most `m`
transfers across a bijection matching the two adjacency relations. -/
theorem exists_dominatingSet_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, IsDominatingSet G s ∧ s.card ≤ m) ↔
      ∃ t : Finset W, IsDominatingSet H t ∧ t.card ≤ m := by
  constructor
  · rintro ⟨s, hs, hm⟩
    refine ⟨s.map e.toEmbedding, fun w ↦ ?_, by rwa [Finset.card_map]⟩
    obtain ⟨u, hu, hor⟩ := hs (e.symm w)
    refine ⟨e u, by simpa using Finset.mem_map_of_mem e.toEmbedding hu, ?_⟩
    rcases hor with rfl | h
    · exact Or.inl (e.apply_symm_apply w)
    · have h' := (hadj u (e.symm w)).mp h
      rw [e.apply_symm_apply] at h'
      exact Or.inr h'
  · rintro ⟨t, ht, hm⟩
    refine ⟨t.map e.symm.toEmbedding, fun v ↦ ?_, by rwa [Finset.card_map]⟩
    obtain ⟨u, hu, hor⟩ := ht (e v)
    refine ⟨e.symm u, by simpa using Finset.mem_map_of_mem e.symm.toEmbedding hu, ?_⟩
    rcases hor with rfl | h
    · exact Or.inl (e.symm_apply_apply v)
    · refine Or.inr ?_
      rw [hadj (e.symm u) v, e.apply_symm_apply]
      exact h

end Hardness