import HardnessReductions.Sets.Defs

/-!
# SET COVER

Given a set system (`Sets/Defs.lean`), do the sets at some `≤ k` positions of
the family jointly cover the whole ground set? Instances whose family does not
cover the ground set at all are simply no-instances.

Hardness proof (in `SetCover/`): from VERTEX COVER (`FromVertexCover.lean`,
covering the edges by vertex stars; certified in
`FromVertexCover/Certified.lean`, where correctness is proved directly on the
concrete encoding rather than transported). The concrete encoding of set
systems lives in `Sets/Encoding.lean`.

The dual problem — cover the *sets* by elements rather than the elements by
sets — is HITTING SET (`Sets/HittingSet.lean`), stated over the same instance
type.
-/

namespace Hardness

/-- SET COVER: is there a selection of at most `k` positions of the family
list whose sets jointly cover all of `U`? -/
def SET_COVER : Problem SetSystemInstance :=
  fun x ↦ ∃ s : Finset (Fin x.family.length),
    (∀ u : x.U, ∃ i ∈ s, u ∈ x.family[i.1]'i.isLt) ∧ s.card ≤ x.k

/-- **Renaming invariance**: a set system is only ever inspected through the
incidence between positions and ground elements, so renaming the ground set
along a bijection changes nothing. The families are related by a length
equality rather than carried by one list, because the concrete encoding
rebuilds the family and `List.length_map` is propositional; the selection
transports along `finCongr` and keeps its cardinality.

Consumed twice over: by gadget certificates, whose mathematical layer names
elements by tags while the concrete instance names them by positions, and by
the representation theorem of the domain (`Sets/Representation.lean`). -/
theorem exists_setCover_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 (Fin F.length),
        (∀ u : U, ∃ i ∈ s, u ∈ F[i.1]'i.isLt) ∧ s.card ≤ k) ↔
      (∃ t : Finset (Fin G.length),
        (∀ w : W, ∃ i ∈ t, w ∈ G[i.1]'i.isLt) ∧ t.card ≤ k) := by
  constructor
  · rintro ⟨s, hcov, hcard⟩
    refine ⟨s.map (finCongr hlen).toEmbedding, fun w ↦ ?_, by rwa [Finset.card_map]⟩
    obtain ⟨i, hi, hmi⟩ := hcov (e.symm w)
    refine ⟨finCongr hlen i, Finset.mem_map_of_mem _ hi, ?_⟩
    have h := (hmem i.1 i.isLt (e.symm w)).mp hmi
    rwa [Equiv.apply_symm_apply] at h
  · rintro ⟨t, hcov, hcard⟩
    refine ⟨t.map (finCongr hlen.symm).toEmbedding, fun u ↦ ?_,
      by rwa [Finset.card_map]⟩
    obtain ⟨i, hi, hmi⟩ := hcov (e u)
    exact ⟨finCongr hlen.symm i, Finset.mem_map_of_mem _ hi,
      (hmem i.1 (by omega) u).mpr hmi⟩

end Hardness