import HardnessReductions.Core
import HardnessReductions.Digraph.Defs
import HardnessReductions.Digraph.Acyclicity

/-!
# FEEDBACK VERTEX SET

Is there a set of at most `k` vertices whose removal leaves a digraph with no
directed cycle? Karp's FEEDBACK NODE SET; the catalog follows Garey–Johnson's
name [GT7].

Garey–Johnson asks instead for a set of vertices *meeting every directed
cycle*. The two readings agree: a cycle survives the removal of `S` exactly
when it avoids `S`, so no cycle survives exactly when every cycle meets `S`.
We state the removal form because it needs no cycles as objects — the
acyclicity of the remainder is all the predicate ever mentions, and
`Digraph/Acyclicity.lean` supplies that without a walk API. A self-loop needs
no special case: it is a one-step cycle, so its vertex belongs to every
feedback vertex set.

Hardness proof (in `FeedbackVertexSet/`): from VERTEX COVER
(`FromVertexCover.lean`, Karp's bidirection; certified in
`FromVertexCover/Certified.lean`).
-/

namespace Hardness

/-- FEEDBACK VERTEX SET: is there a set of at most `k` vertices whose removal
leaves an acyclic digraph? -/
def FEEDBACK_VERTEX_SET : Problem DigraphThresholdInstance :=
  fun x ↦ ∃ S : Finset x.V, Digraph.Acyclic (Digraph.deleteVerts x.D ↑S) ∧ S.card ≤ x.k

/-- **Renaming invariance**: existence of a feedback vertex set of size at most
`m` transfers across a bijection matching the two adjacency relations. A
minimization target, so transporting the set needs only `Finset.card_map`, no
injectivity argument. -/
theorem exists_feedbackVertexSet_iff_of_equiv {V W : Type*} {D : Digraph V} {E : Digraph W}
    (e : V ≃ W) (hadj : ∀ a b : V, D.Adj a b ↔ E.Adj (e a) (e b)) (m : ℕ) :
    (∃ S : Finset V, Digraph.Acyclic (Digraph.deleteVerts D ↑S) ∧ S.card ≤ m) ↔
      ∃ T : Finset W, Digraph.Acyclic (Digraph.deleteVerts E ↑T) ∧ T.card ≤ m := by
  have key : ∀ S : Finset V, Digraph.Acyclic (Digraph.deleteVerts D ↑S) ↔
      Digraph.Acyclic (Digraph.deleteVerts E ↑(S.map e.toEmbedding)) := by
    intro S
    refine Digraph.acyclic_iff_of_equiv e fun a b ↦ ?_
    simp only [Digraph.deleteVerts_adj, Finset.coe_map, Set.mem_image, hadj a b,
      Finset.mem_coe, Equiv.coe_toEmbedding]
    constructor
    · rintro ⟨ha, hb, hab⟩
      exact ⟨fun ⟨x, hx, hxe⟩ ↦ ha (e.injective hxe ▸ hx),
        fun ⟨x, hx, hxe⟩ ↦ hb (e.injective hxe ▸ hx), hab⟩
    · rintro ⟨ha, hb, hab⟩
      exact ⟨fun ha' ↦ ha ⟨a, ha', rfl⟩, fun hb' ↦ hb ⟨b, hb', rfl⟩, hab⟩
  constructor
  · rintro ⟨S, hS, hm⟩
    exact ⟨S.map e.toEmbedding, (key S).mp hS, by rwa [Finset.card_map]⟩
  · rintro ⟨T, hT, hm⟩
    have hmap : (T.map e.symm.toEmbedding).map e.toEmbedding = T := by ext w; simp
    exact ⟨T.map e.symm.toEmbedding, (key _).mpr (by rw [hmap]; exact hT),
      by rwa [Finset.card_map]⟩

end Hardness