import HardnessReductions.Sets.Defs

/-!
# SET PACKING

Given a set system (`Sets/Defs.lean`), are there `≥ k` positions of the family
whose sets are pairwise disjoint?

Note the threshold's direction: SET PACKING is a maximization question
(`k ≤ s.card`), like CLIQUE and INDEPENDENT SET, whereas SET COVER and HITTING
SET are minimization questions (`s.card ≤ k`). That is not a stylistic choice —
it is why the hardness proof comes from INDEPENDENT SET rather than from either
of the other two set-system problems.

Disjointness is required of *distinct positions*, not of distinct sets: the
family is a list, so a set occurring twice occupies two positions, and those
two positions form a packing exactly when the set is empty. This is the
size-model discipline of explicit representations, and it is the honest reading
of Garey–Johnson's "`C` contains at least `K` mutually disjoint sets".

Hardness proofs (in `SetPacking/`): from INDEPENDENT SET
(`FromIndepSet.lean`, the vertex-star system; certified in
`FromIndepSet/Certified.lean`) and from CLIQUE (`FromClique.lean`, by
composition with complementation — this composite is Karp's original
reduction, whose sets are the stars of the *complement* graph; certified in
`FromIndepSet/Certified.lean`, where one program serves both sources).
-/

namespace Hardness

/-- SET PACKING: are there at least `k` positions of the family list whose sets
are pairwise disjoint? -/
def SET_PACKING : Problem SetSystemInstance :=
  fun x ↦ ∃ s : Finset (Fin x.family.length),
    (∀ i ∈ s, ∀ j ∈ s, i ≠ j →
      Disjoint (x.family[i.1]'i.isLt) (x.family[j.1]'j.isLt)) ∧ x.k ≤ s.card

/-- Corresponding sets are disjoint together: a bijection of the ground set
matching membership matches disjointness, since it has an inverse to carry a
common element back. -/
theorem disjoint_iff_of_mem_iff {U W : Type*}
    {A B : Finset U} {A' B' : Finset W} (e : U ≃ W)
    (hA : ∀ u : U, u ∈ A ↔ e u ∈ A') (hB : ∀ u : U, u ∈ B ↔ e u ∈ B') :
    Disjoint A B ↔ Disjoint A' B' := by
  simp only [Finset.disjoint_left]
  constructor
  · intro h w hw' hw''
    exact h ((hA (e.symm w)).mpr (by rwa [Equiv.apply_symm_apply]))
      ((hB (e.symm w)).mpr (by rwa [Equiv.apply_symm_apply]))
  · exact fun h u hu hu' ↦ h ((hA u).mp hu) ((hB u).mp hu')

/-- **Renaming invariance**, the packing analogue of
`exists_setCover_iff_of_equiv`: the selected positions transport along the
length equality as there, and the pairwise disjointness of the selected sets
along the ground-set bijection (`disjoint_iff_of_mem_iff`). The threshold runs
the other way, which changes nothing — `Finset.card_map` serves either
direction. -/
theorem exists_setPacking_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),
        (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (F[i.1]'i.isLt) (F[j.1]'j.isLt))
          ∧ k ≤ s.card) ↔
      (∃ t : Finset (Fin G.length),
        (∀ i ∈ t, ∀ j ∈ t, i ≠ j → Disjoint (G[i.1]'i.isLt) (G[j.1]'j.isLt))
          ∧ k ≤ t.card) := by
  have hdisj : ∀ (i j : ℕ) (hi : i < F.length) (hj : j < F.length),
      Disjoint (F[i]'hi) (F[j]'hj)
        ↔ Disjoint (G[i]'(hlen ▸ hi)) (G[j]'(hlen ▸ hj)) :=
    fun i j hi hj ↦ disjoint_iff_of_mem_iff e (hmem i hi) (hmem j hj)
  constructor
  · rintro ⟨s, hpack, hcard⟩
    refine ⟨s.map (finCongr hlen).toEmbedding, ?_, by rwa [Finset.card_map]⟩
    intro i hi j hj hne
    obtain ⟨i₀, hi₀, rfl⟩ := Finset.mem_map.mp hi
    obtain ⟨j₀, hj₀, rfl⟩ := Finset.mem_map.mp hj
    exact (hdisj i₀.1 j₀.1 i₀.isLt j₀.isLt).mp
      (hpack i₀ hi₀ j₀ hj₀ fun h ↦ hne (congrArg _ h))
  · rintro ⟨t, hpack, hcard⟩
    refine ⟨t.map (finCongr hlen.symm).toEmbedding, ?_, by rwa [Finset.card_map]⟩
    intro i hi j hj hne
    obtain ⟨i₀, hi₀, rfl⟩ := Finset.mem_map.mp hi
    obtain ⟨j₀, hj₀, rfl⟩ := Finset.mem_map.mp hj
    exact (hdisj i₀.1 j₀.1 (by omega) (by omega)).mpr
      (hpack i₀ hi₀ j₀ hj₀ fun h ↦ hne (congrArg _ h))

end Hardness