import HardnessReductions.Sets.Defs

/-!
# SET SPLITTING

Given a set system (`Sets/Defs.lean`), is there a partition of the ground set
into two parts such that no set of the family lies wholly inside one part?
Garey–Johnson's [SP4], also known as HYPERGRAPH 2-COLORABILITY — the family is
a hypergraph and the two parts are the colours, the demand being that no
hyperedge is monochromatic.

A partition into two parts is a `Bool`-valued labelling of the ground set, and
"the set `A` is not wholly inside one part" is "`A` has an element on each
side". Written that way the question is *literally* the not-all-equal
condition of `Clause.Nae`, one set at a time, which is what makes the
reduction from NAE3SAT a translation rather than a construction. Two readings
come with the phrasing: the empty set can never be split, so a family
containing it is a no-instance (`∅` is contained in either part), and neither
can a singleton.

Garey–Johnson give SET SPLITTING no bound `K`, so its instance is the covering
problems' minus that number: `SetFamilyInstance`, not `SetSystemInstance` with
a field left unread. The sharing happens at the encoding instead — one
`SetSystemTy`, one decoder, whose threshold coordinate this question ignores —
so a reduction into SET SPLITTING may emit any threshold at all without the
abstract statement ever mentioning one.

Hardness proof (in `SetSplitting/`): from NAE3SAT (`FromNae3Sat.lean`, Lovász's
system whose ground set is the literals — the complementary pairs and the
clauses are the family; certified in `FromNae3Sat/Code.lean` and
`FromNae3Sat/Adequacy.lean`).
-/

namespace Hardness

/-- SET SPLITTING: is there a two-part partition of the ground set — a
`Bool`-valued labelling — under which every set of the family has an element on
each side? -/
def SET_SPLITTING : Problem SetFamilyInstance :=
  fun x ↦ ∃ f : x.U → Bool, ∀ i : Fin x.family.length,
    (∃ u ∈ x.family[i.1]'i.isLt, f u = true) ∧
      (∃ u ∈ x.family[i.1]'i.isLt, f u = false)

/-- **Renaming invariance**, in the shape the certificates produce and the
representation pair consumes: a ground-set bijection matching membership set by
set carries splittings both ways, the labelling transporting along the
bijection and the quantification along the length equality. -/
theorem exists_splitting_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)) :
    (∃ f : U → Bool, ∀ i : Fin F.length,
        (∃ u ∈ F[i.1]'i.isLt, f u = true) ∧ (∃ u ∈ F[i.1]'i.isLt, f u = false)) ↔
      (∃ g : W → Bool, ∀ i : Fin G.length,
        (∃ w ∈ G[i.1]'i.isLt, g w = true) ∧
          (∃ w ∈ G[i.1]'i.isLt, g w = false)) := by
  constructor
  · rintro ⟨f, hf⟩
    refine ⟨fun w ↦ f (e.symm w), fun i ↦ ?_⟩
    obtain ⟨⟨u, hu, hut⟩, ⟨v, hv, hvf⟩⟩ := hf ⟨i.1, by omega⟩
    refine ⟨⟨e u, (hmem i.1 (by omega) u).mp hu, by simpa using hut⟩,
      ⟨e v, (hmem i.1 (by omega) v).mp hv, by simpa using hvf⟩⟩
  · rintro ⟨g, hg⟩
    refine ⟨fun u ↦ g (e u), fun i ↦ ?_⟩
    obtain ⟨⟨w, hw, hwt⟩, ⟨z, hz, hzf⟩⟩ := hg ⟨i.1, by omega⟩
    refine ⟨⟨e.symm w, (hmem i.1 i.isLt _).mpr (by rwa [Equiv.apply_symm_apply]),
        by simpa using hwt⟩,
      ⟨e.symm z, (hmem i.1 i.isLt _).mpr (by rwa [Equiv.apply_symm_apply]),
        by simpa using hzf⟩⟩

end Hardness