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

/-!
# FEEDBACK ARC SET

Is there a set of at most `k` arcs whose removal leaves a digraph with no
directed cycle? Garey–Johnson's [GT8]; Karp's FEEDBACK ARC SET.

As with FEEDBACK VERTEX SET, the removal form replaces Garey–Johnson's "a set
of arcs meeting every directed cycle", and for the same reason: the two agree,
and only the removal form avoids cycles as objects. The condition that the
chosen arcs *are* arcs is Garey–Johnson's `A' ⊆ A` and is kept — dropping it
would change nothing about hardness, but the entry should state the instance
the literature states.

Hardness proof (in `FeedbackArcSet/`): from VERTEX COVER
(`FromVertexCover.lean`, Karp's vertex-splitting construction; certified in
`FromVertexCover/Code.lean` and `FromVertexCover/Adequacy.lean`).
-/

namespace Hardness

/-- FEEDBACK ARC SET: is there a set of at most `k` arcs whose removal leaves
an acyclic digraph? -/
def FEEDBACK_ARC_SET : Problem DigraphThresholdInstance :=
  fun x ↦ ∃ F : Finset (x.V × x.V), (∀ p ∈ F, x.D.Adj p.1 p.2) ∧
    Digraph.Acyclic (Digraph.deleteArcs x.D ↑F) ∧ F.card ≤ x.k

/-- One direction of renaming invariance; the statement is symmetric in the two
digraphs, so `exists_feedbackArcSet_iff_of_equiv` gets the other by applying
this to `e.symm`. -/
theorem exists_feedbackArcSet_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 : ℕ}
    (h : ∃ F : Finset (V × V), (∀ p ∈ F, D.Adj p.1 p.2) ∧
      Digraph.Acyclic (Digraph.deleteArcs D ↑F) ∧ F.card ≤ m) :
    ∃ F : Finset (W × W), (∀ p ∈ F, E.Adj p.1 p.2) ∧
      Digraph.Acyclic (Digraph.deleteArcs E ↑F) ∧ F.card ≤ m := by
  obtain ⟨F, harc, hacyc, hcard⟩ := h
  refine ⟨F.map (e.prodCongr e).toEmbedding, ?_, ?_, by rwa [Finset.card_map]⟩
  · intro p hp
    rw [Finset.mem_map_equiv] at hp
    have := harc _ hp
    simpa [hadj] using this
  · refine (Digraph.acyclic_iff_of_equiv e fun a b ↦ ?_).mp hacyc
    simp only [Digraph.deleteArcs_adj, hadj a b, Finset.mem_coe, Finset.mem_map_equiv,
      Equiv.prodCongr_symm, Equiv.prodCongr_apply, Prod.map_apply, Equiv.symm_apply_apply]

/-- **Renaming invariance**: existence of a feedback arc set of size at most
`m` transfers across a bijection matching the two adjacency relations. The
witness is a set of *pairs*, so it transports along `e.prodCongr e`; as for
every minimization target, only `Finset.card_map` is needed. -/
theorem exists_feedbackArcSet_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 : ℕ) :
    (∃ F : Finset (V × V), (∀ p ∈ F, D.Adj p.1 p.2) ∧
        Digraph.Acyclic (Digraph.deleteArcs D ↑F) ∧ F.card ≤ m) ↔
      ∃ F : Finset (W × W), (∀ p ∈ F, E.Adj p.1 p.2) ∧
        Digraph.Acyclic (Digraph.deleteArcs E ↑F) ∧ F.card ≤ m :=
  ⟨exists_feedbackArcSet_of_equiv e hadj,
    exists_feedbackArcSet_of_equiv e.symm fun a b ↦ by simp [hadj (e.symm a) (e.symm b)]⟩

end Hardness