import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Card
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
import Mathlib.Data.Finset.BooleanAlgebra
import HardnessReductions.Core

/-!
# Exact cover by 3-sets

An instance of EXACT COVER BY 3-SETS is a finite ground set together with a
collection of subsets of it. A yes-instance is one where some subcollection of
*3-element* sets covers the ground set exactly: every element lies in exactly
one chosen set.

Two deliberate choices, both the same choice made for 3-DIMENSIONAL MATCHING
(`Sets/Matching3D.lean`) — push the well-formedness promises of
Garey–Johnson's statement into the *question*, where they cost nothing:

* Garey–Johnson require every member of the collection to have exactly three
  elements. Asking instead that the *chosen* subcollection consist of 3-sets
  says the same thing on well-formed instances — a set of any other size is
  simply never usable — and is total on all instances, so no predicate infects
  the instance type.
* Garey–Johnson also require `|Z| = 3q`. That is implied: an exact cover by
  3-sets has `|Z| = 3 · |C|`, so an instance violating it is a no-instance
  already.

The collection is a `Finset (Finset Z)` rather than a list, for the reason
3-DIMENSIONAL MATCHING's triples are: duplicates are meaningless here (two
equal sets cover the same elements, so no exact cover contains both), unlike
in SET COVER where the threshold *counts* the chosen sets.

Hardness proof (in `ExactCover3/`): from 3-DIMENSIONAL MATCHING
(`FromMatching3D.lean`, the disjoint union of the three coordinate sets;
certified in `FromMatching3D/Certified.lean`).
-/

namespace Hardness

/-- `C` covers the ambient type exactly: every element lies in exactly one
member of `C`. The `∃!` packages both halves of "is an exact cover" —
*covering* (some member contains `z`) and *disjointness* (no two do) — exactly
as `IsExactCover` does for a family indexed by a coordinate map. -/
def IsExactSetCover {Z : Type*} (C : Finset (Finset Z)) : Prop :=
  ∀ z : Z, ∃! S, S ∈ C ∧ z ∈ S

namespace IsExactSetCover

variable {Z : Type*} {C : Finset (Finset Z)}

/-- Every element is covered. -/
theorem exists_mem (h : IsExactSetCover C) (z : Z) : ∃ S ∈ C, z ∈ S := by
  obtain ⟨S, ⟨hS, hz⟩, -⟩ := h z
  exact ⟨S, hS, hz⟩

/-- No two chosen sets overlap. -/
theorem eq_of_mem (h : IsExactSetCover C) {S₁ S₂ : Finset Z} (h₁ : S₁ ∈ C)
    (h₂ : S₂ ∈ C) {z : Z} (hz₁ : z ∈ S₁) (hz₂ : z ∈ S₂) : S₁ = S₂ := by
  obtain ⟨S, -, huniq⟩ := h z
  rw [huniq S₁ ⟨h₁, hz₁⟩, huniq S₂ ⟨h₂, hz₂⟩]

end IsExactSetCover

/-- Covering and disjointness, assembled — the companion of `isExactCover_iff`
for set families. -/
theorem isExactSetCover_iff {Z : Type*} {C : Finset (Finset Z)} :
    IsExactSetCover C ↔
      (∀ z : Z, ∃ S ∈ C, z ∈ S) ∧
        ∀ S₁ ∈ C, ∀ S₂ ∈ C, ∀ z : Z, z ∈ S₁ → z ∈ S₂ → S₁ = S₂ := by
  constructor
  · exact fun h ↦ ⟨h.exists_mem, fun _ h₁ _ h₂ _ hz₁ hz₂ ↦ h.eq_of_mem h₁ h₂ hz₁ hz₂⟩
  · rintro ⟨hcov, hdisj⟩ z
    obtain ⟨S, hS, hz⟩ := hcov z
    exact ⟨S, ⟨hS, hz⟩, fun T hT ↦ hdisj T hT.1 S hS z hT.2 hz⟩

/-! ## Counting an exact cover

A family that covers the ground type has total size at least the ground type's,
with equality exactly when the cover is exact. Both halves are the same double
count — summing the sizes of the members counts, element by element, how many
members contain it — and a reduction *from* X3C wants both: the construction
direction to price a cover, the reflection direction to recognize one out of an
arithmetic bound. -/

/-- **The double count**: the total size of a family is, element by element,
the number of members containing it. -/
theorem sum_card_eq_sum_card_filter {Z : Type*} [Fintype Z] [DecidableEq Z]
    (C : Finset (Finset Z)) :
    ∑ S ∈ C, S.card = ∑ z : Z, (C.filter fun S ↦ z ∈ S).card := by
  have h : ∀ S : Finset Z, S.card = ∑ z : Z, if z ∈ S then 1 else 0 := fun S ↦ by
    rw [← Finset.card_filter, Finset.filter_univ_mem]
  simp only [h, Finset.card_filter]
  exact Finset.sum_comm

/-- The ground type is no larger than the total size of a family covering
it. -/
theorem card_le_sum_card_of_cover {Z : Type*} [Fintype Z]
    {C : Finset (Finset Z)} (hcov : ∀ z : Z, ∃ S ∈ C, z ∈ S) :
    Fintype.card Z ≤ ∑ S ∈ C, S.card := by
  classical
  rw [sum_card_eq_sum_card_filter, show Fintype.card Z = ∑ _z : Z, 1 by simp]
  refine Finset.sum_le_sum fun z _ ↦ ?_
  obtain ⟨S, hS, hz⟩ := hcov z
  exact Finset.card_pos.mpr ⟨S, Finset.mem_filter.mpr ⟨hS, hz⟩⟩

/-- An exact cover has total size exactly that of the ground type. -/
theorem IsExactSetCover.sum_card {Z : Type*} [Fintype Z]
    {C : Finset (Finset Z)} (h : IsExactSetCover C) :
    ∑ S ∈ C, S.card = Fintype.card Z := by
  classical
  have hone : ∀ z : Z, (C.filter fun S ↦ z ∈ S).card = 1 := by
    intro z
    obtain ⟨S, ⟨hS, hz⟩, huniq⟩ := h z
    refine Finset.card_eq_one.mpr ⟨S, Finset.eq_singleton_iff_unique_mem.mpr
      ⟨Finset.mem_filter.mpr ⟨hS, hz⟩, fun T hT ↦ huniq T (Finset.mem_filter.mp hT)⟩⟩
  rw [sum_card_eq_sum_card_filter, Finset.sum_congr rfl fun z _ ↦ hone z]
  simp

/-- **An exact cover, recognized by its size**: a family that covers the ground
type and is no larger than it in total covers it exactly. This is the shape a
reduction from X3C reflects — the budget bounds the number of sets used, the
sets have three elements each, and the two bounds meet. -/
theorem isExactSetCover_of_sum_card_le {Z : Type*} [Fintype Z]
    {C : Finset (Finset Z)} (hcov : ∀ z : Z, ∃ S ∈ C, z ∈ S)
    (hle : ∑ S ∈ C, S.card ≤ Fintype.card Z) : IsExactSetCover C := by
  classical
  have hge : ∀ z : Z, 1 ≤ (C.filter fun S ↦ z ∈ S).card := by
    intro z
    obtain ⟨S, hS, hz⟩ := hcov z
    exact Finset.card_pos.mpr ⟨S, Finset.mem_filter.mpr ⟨hS, hz⟩⟩
  have hsum : ∑ z : Z, (C.filter fun S ↦ z ∈ S).card ≤ ∑ _z : Z, 1 := by
    rw [← sum_card_eq_sum_card_filter, show ∑ _z : Z, 1 = Fintype.card Z by simp]
    exact hle
  have heq : ∀ z : Z, (C.filter fun S ↦ z ∈ S).card = 1 := by
    intro z
    exact ((Finset.sum_eq_sum_iff_of_le fun i _ ↦ hge i).mp
      (le_antisymm (Finset.sum_le_sum fun i _ ↦ hge i) hsum) z (Finset.mem_univ z)).symm
  intro z
  obtain ⟨S, hS⟩ := Finset.card_eq_one.mp (heq z)
  refine ⟨S, Finset.mem_filter.mp (hS ▸ Finset.mem_singleton_self S), fun T hT ↦ ?_⟩
  exact Finset.mem_singleton.mp (hS ▸ Finset.mem_filter.mpr hT)

/-- An instance of EXACT COVER BY 3-SETS: a finite ground set with decidable
equality, and a collection of subsets of it. -/
structure ExactCover3Instance : Type 1 where
  /-- The ground set. -/
  Z : Type
  [fintypeZ : Fintype Z]
  [decEqZ : DecidableEq Z]
  /-- The available sets. -/
  sets : Finset (Finset Z)

attribute [instance] ExactCover3Instance.fintypeZ ExactCover3Instance.decEqZ

/-- EXACT COVER BY 3-SETS: is there a subcollection of available 3-element
sets covering every ground element exactly once? -/
def EXACT_COVER_3 : Problem ExactCover3Instance := fun I ↦
  ∃ C ⊆ I.sets, (∀ S ∈ C, S.card = 3) ∧ IsExactSetCover C

/-! ## Invariance under renaming

As with 3-DIMENSIONAL MATCHING, an instance is only ever inspected through the
incidence between sets and elements, so renaming the ground set along a
bijection changes nothing. This is the transport a *certificate* needs: the
mathematical layer names ground elements by tags (here, by which of the three
coordinate sets of a 3DM instance they came from), while a concrete instance
can only name them by *positions* of an element list. -/

/-- An exact set cover transports along a bijection of the ground set. -/
theorem IsExactSetCover.image {Z Z' : Type*} [DecidableEq Z']
    {C : Finset (Finset Z)} (e : Z ≃ Z') (h : IsExactSetCover C) :
    IsExactSetCover (C.image (Finset.image e)) := by
  intro z'
  obtain ⟨S, ⟨hSC, hzS⟩, huniq⟩ := h (e.symm z')
  refine ⟨S.image e, ⟨Finset.mem_image_of_mem _ hSC, ?_⟩, ?_⟩
  · exact Finset.mem_image.mpr ⟨e.symm z', hzS, e.apply_symm_apply z'⟩
  · rintro T ⟨hT, hzT⟩
    obtain ⟨S₀, hS₀C, rfl⟩ := Finset.mem_image.mp hT
    obtain ⟨w, hwS₀, hwz⟩ := Finset.mem_image.mp hzT
    have hw : w = e.symm z' := by rw [← hwz, Equiv.symm_apply_apply]
    exact congrArg (Finset.image e) (huniq S₀ ⟨hS₀C, hw ▸ hwS₀⟩)

/-- Renaming the ground set along a bijection preserves yes-instances. The
available sets need only correspond at *cardinality three*: a set of any other
size is never usable, since the question asks for a cover by 3-sets. -/
theorem exactCover3_of_equiv {I J : ExactCover3Instance} (e : I.Z ≃ J.Z)
    (h : ∀ S : Finset I.Z, S.card = 3 → S ∈ I.sets → S.image e ∈ J.sets) :
    EXACT_COVER_3 I → EXACT_COVER_3 J := by
  rintro ⟨C, hC, hcard, hex⟩
  refine ⟨C.image (Finset.image e), ?_, ?_, hex.image e⟩
  · intro S hS
    obtain ⟨S₀, hS₀, rfl⟩ := Finset.mem_image.mp hS
    exact h S₀ (hcard S₀ hS₀) (hC hS₀)
  · intro S hS
    obtain ⟨S₀, hS₀, rfl⟩ := Finset.mem_image.mp hS
    rw [Finset.card_image_of_injective _ e.injective]
    exact hcard S₀ hS₀

/-- **Renaming invariance, in the form the concrete encoding needs**: instances
whose *3-element* available sets correspond under a bijection of the ground set
have the same answer, whatever either does with sets of other sizes.

The strengthening over `exactCover3_iff_of_equiv` is what makes X3C
representable at all. A concrete instance names each available set by three
element indices, so it can express nothing else; the encoding may therefore
drop every set of size other than three, and this lemma is the proof that
dropping them is free. That is precisely the design choice recorded at the top
of this file — the `card = 3` condition sits in the *question* rather than on
the instance type — collecting its interest. -/
theorem exactCover3_iff_of_equiv_card3 {I J : ExactCover3Instance} (e : I.Z ≃ J.Z)
    (h : ∀ S : Finset I.Z, S.card = 3 → (S ∈ I.sets ↔ S.image e ∈ J.sets)) :
    EXACT_COVER_3 I ↔ EXACT_COVER_3 J := by
  refine ⟨exactCover3_of_equiv e fun S hc hS ↦ (h S hc).mp hS,
    exactCover3_of_equiv e.symm fun S' hc' hS' ↦ ?_⟩
  have hc : (S'.image e.symm).card = 3 := by
    rwa [Finset.card_image_of_injective _ e.symm.injective]
  refine (h (S'.image e.symm) hc).mpr ?_
  rwa [Finset.image_image, Equiv.self_comp_symm, Finset.image_id]

/-- **Renaming invariance**: instances that agree up to a bijection of the
ground set have the same answer. -/
theorem exactCover3_iff_of_equiv {I J : ExactCover3Instance} (e : I.Z ≃ J.Z)
    (h : ∀ S : Finset I.Z, S ∈ I.sets ↔ S.image e ∈ J.sets) :
    EXACT_COVER_3 I ↔ EXACT_COVER_3 J :=
  exactCover3_iff_of_equiv_card3 e fun S _ ↦ h S

end Hardness