import HardnessReductions.Sets.Defs

/-!
# HITTING SET

Given a set system (`Sets/Defs.lean`), are there `≤ k` ground *elements*
meeting every set of the family?

This is SET COVER's dual, and deliberately stated so that the duality is
visible on the page: the two definitions are literally each other's with the
roles of positions and elements exchanged.

```
SET COVER    ∃ s : Finset (Fin family.length),
               (∀ u : U,                 ∃ i ∈ s, u ∈ family[i]) ∧ s.card ≤ k
HITTING SET  ∃ s : Finset U,
               (∀ i : Fin family.length, ∃ u ∈ s, u ∈ family[i]) ∧ s.card ≤ k
```

(The duality is an involution on *instances* — swap elements for sets and
membership for its converse — not a reduction; each direction of the pairing
still has to be certified, and only the hardness of each is proved here.)

Hardness proof (in `HittingSet/`): from VERTEX COVER (`FromVertexCover.lean`,
the ground set is the vertices and the family is the edges; certified in
`FromVertexCover/Certified.lean`).
-/

namespace Hardness

/-- HITTING SET: is there a set of at most `k` ground elements meeting every
set of the family? -/
def HITTING_SET : Problem SetSystemInstance :=
  fun x ↦ ∃ s : Finset x.U,
    (∀ i : Fin x.family.length, ∃ u ∈ s, u ∈ x.family[i.1]'i.isLt) ∧ s.card ≤ x.k

/-- **Renaming invariance**, the dual of `exists_setCover_iff_of_equiv` and
proved dually: here it is the *selection* that transports along the ground-set
bijection and the *quantification* that transports along the length equality.
Hypotheses and conclusion are otherwise the same. -/
theorem exists_hittingSet_iff_of_equiv {U W : Type*} {F : List (Finset U)}
    {G : List (Finset W)} (e : U ≃ W) (hlen : F.length = G.length)
    (hmem : ∀ (i : ℕ) (hi : i < F.length) (u : U),
      u ∈ F[i]'hi ↔ e u ∈ G[i]'(hlen ▸ hi)) (k : ℕ) :
    (∃ s : Finset U,
        (∀ i : Fin F.length, ∃ u ∈ s, u ∈ F[i.1]'i.isLt) ∧ s.card ≤ k) ↔
      (∃ t : Finset W,
        (∀ i : Fin G.length, ∃ w ∈ t, w ∈ G[i.1]'i.isLt) ∧ t.card ≤ k) := by
  constructor
  · rintro ⟨s, hhit, hcard⟩
    refine ⟨s.map e.toEmbedding, fun i ↦ ?_, by rwa [Finset.card_map]⟩
    obtain ⟨u, hu, hmu⟩ := hhit ⟨i.1, by omega⟩
    exact ⟨e u, Finset.mem_map_of_mem _ hu, (hmem i.1 (by omega) u).mp hmu⟩
  · rintro ⟨t, hhit, hcard⟩
    refine ⟨t.map e.symm.toEmbedding, fun i ↦ ?_, by rwa [Finset.card_map]⟩
    obtain ⟨w, hw, hmw⟩ := hhit ⟨i.1, by omega⟩
    refine ⟨e.symm w, Finset.mem_map_of_mem _ hw, ?_⟩
    refine (hmem i.1 i.isLt (e.symm w)).mpr ?_
    rwa [Equiv.apply_symm_apply]

end Hardness