import Mathlib.Combinatorics.SimpleGraph.Finite
import HardnessReductions.Core
import HardnessReductions.Graph.Defs
import HardnessReductions.Graph.EdgeList

/-!
# SIMPLE MAX CUT

Split the vertices in two; how many edges can be made to cross?

A counting problem (like MAX 2SAT) in graph form. Where a subset problem
asks for a *set* with a property — a
clique, a cover, an independent set — this one asks for a bipartition and
counts what it separates, so the witness is unconstrained and all the content
sits in the number.

## The bipartition is a `Bool`-colouring

Garey–Johnson–Stockmeyer write the witness as a partition `N = S₁ ∪ S₂`. Here it
is a function `χ : V → Bool`, which is the same data without the side conditions
that `S₁ ∩ S₂ = ∅` and `S₁ ∪ S₂ = N` would have to carry. It is also the shape
the reduction produces: the partition GJS build from a truth assignment *is* a
truth assignment, read through the literal nodes.

An edge crosses when its endpoints get different colours. `crosses` is that
test, defined by `Sym2.lift` so that it is a function of the *edge* rather than
of an oriented pair — the symmetry obligation is discharged once, here, and no
client ever picks an orientation.

## Weights, and why this problem stands alone

Garey–Johnson's [ND16] is MAX CUT, whose edges carry weights; SIMPLE MAX CUT is
its unit-weight restriction, and the one GJS prove hard. Weighted instances live
in the network domain (`Networks/Defs.lean`), not here: `GraphThresholdInstance`
has no room for a weight, so the unit-weight problem is a catalog entry in its
own right rather than a `Problem.restrict` of a weighted parent. When the
weighted problem lands, this entry becomes its restriction and its hardness
transfers upward unchanged.

Hardness proof (in `MaxCut/`): from MAX 2SAT (`FromMaxSat2.lean`, the
Garey–Johnson–Stockmeyer rail-and-ladder framework of `Framework.lean`;
certified in `FromMaxSat2/Code.lean` and `FromMaxSat2/Adequacy.lean`).
-/

namespace Hardness

variable {V W : Type*}

/-! ## Crossing edges -/

/-- Does the edge `e` cross the bipartition `χ` — do its two endpoints get
different colours?

Defined through `Sym2.lift`, so that the symmetry of the test is discharged once
and the predicate applies to an edge rather than to an oriented pair. -/
def crosses (χ : V → Bool) (e : Sym2 V) : Bool :=
  Sym2.lift ⟨fun u v ↦ χ u != χ v, by intro a b; dsimp only; cases χ a <;> cases χ b <;> rfl⟩ e

@[simp] theorem crosses_mk (χ : V → Bool) (u v : V) :
    crosses χ s(u, v) = (χ u != χ v) := rfl

theorem crosses_iff (χ : V → Bool) (u v : V) :
    crosses χ s(u, v) = true ↔ χ u ≠ χ v := by
  rw [crosses_mk, bne_iff_ne]

/-! ## The cut -/

variable [Fintype V]

/-- The size of the cut `χ`: how many edges of `G` have their endpoints coloured
differently. -/
def cutSize (G : SimpleGraph V) [DecidableRel G.Adj] (χ : V → Bool) : ℕ :=
  (G.edgeFinset.filter fun e ↦ crosses χ e).card

/-- The cut never exceeds the number of edges — the unconditional upper bound a
threshold guard raises itself above, in the maximization idiom of MAX 2SAT's
`numSat_le_seven_mul`. -/
theorem cutSize_le (G : SimpleGraph V) [DecidableRel G.Adj] (χ : V → Bool) :
    cutSize G χ ≤ G.edgeFinset.card :=
  Finset.card_filter_le _ _

/-! ## The cut of a list-presented graph

The bridge from the graph objective to the `countP` the counting toolkit
(`Counting.lean`) reasons about. Both halves of faithfulness are spent here, and
visibly: loop-freeness identifies the edge set, and `Nodup` is what lets the
resulting `Finset`'s cardinality be read back as a list length. Drop the latter
and the equation becomes a `≤` in the wrong direction for a yes-instance — which
is exactly the parallel-edge collapse that makes the construction need distinct
clauses in the first place. -/

/-- **The cut of a faithful list is a `countP` over it**: one entry per edge, so
counting crossing edges of the graph is counting crossing entries of the list. -/
theorem cutSize_ofEdgeList [DecidableEq V] {l : List (V × V)}
    (hne : ∀ p ∈ l, p.1 ≠ p.2) (hnd : (edgeSyms l).Nodup) (χ : V → Bool) :
    cutSize (ofEdgeList l) χ = l.countP fun p ↦ χ p.1 != χ p.2 := by
  rw [cutSize, edgeFinset_ofEdgeList hne, ← List.toFinset_filter,
    List.toFinset_card_of_nodup (hnd.filter _), List.countP_eq_length_filter,
    edgeSyms, List.filter_map, List.length_map]
  rfl

/-- **The list length bounds the cut, with no faithfulness at all** — the
unconditional upper bound the maximization guard raises its threshold above.
Loop entries are not even excluded: a sloppier list only pads the bound. -/
theorem cutSize_le_length [DecidableEq V] (l : List (V × V)) (χ : V → Bool) :
    cutSize (ofEdgeList l) χ ≤ l.length := by
  refine le_trans (cutSize_le _ _) ?_
  calc (ofEdgeList l).edgeFinset.card
      ≤ (edgeSyms l).toFinset.card := by
        refine Finset.card_le_card fun e he ↦ ?_
        rw [SimpleGraph.mem_edgeFinset] at he
        induction e using Sym2.ind with
        | _ u w =>
          rw [SimpleGraph.mem_edgeSet, ofEdgeList_adj] at he
          rw [List.mem_toFinset, mem_edgeSyms]
          exact he.2
    _ ≤ (edgeSyms l).length := List.toFinset_card_le _
    _ = l.length := by rw [edgeSyms, List.length_map]
example : cutSize (ofEdgeList [((0 : Fin 3), 1), (1, 2), (0, 2)]) (fun v ↦ v == 0) = 2 := by
  decide

/-- **Why `Nodup` is a hypothesis and not a convenience.** The same edge written
twice is one edge of the graph, so the cut is `1` where the `countP` of
`cutSize_ofEdgeList` would be `2`. A construction that counts must therefore
prove its list names each edge once; it cannot be arranged after the fact. -/
example : cutSize (ofEdgeList [((0 : Fin 2), 1), (0, 1)]) (fun v ↦ v == 0) = 1 := by
  decide

example : ([((0 : Fin 2), 1), (0, 1)].countP fun p ↦ (p.1 == 0) != (p.2 == 0)) = 2 := by
  decide

/-! ## Renaming invariance

The counting twin of the entries' clique/cover invariance lemmas: a *count* is
invariant only under maps that carry edges one for one, so the transfer runs
through the edge bijection `Sym2.map e` rather than through any witness set.
Consumed by the representation pair and by the certificate's adequacy. -/

/-- The cut objective transfers across a bijection matching the two adjacency
relations: cutting `H` with `χ` is cutting `G` with `χ` read through the
bijection. -/
theorem cutSize_eq_of_equiv {W : Type*} [Fintype W]
    {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (e : V ≃ W) (hadj : ∀ a b : V, G.Adj a b ↔ H.Adj (e a) (e b)) (χ : W → Bool) :
    cutSize H χ = cutSize G fun v ↦ χ (e v) := by
  rw [cutSize, cutSize]
  refine Finset.card_nbij' (Sym2.map e.symm) (Sym2.map e) ?_ ?_ ?_ ?_
  · intro s hs
    induction s using Sym2.ind with
    | _ u w =>
      rw [Finset.mem_coe, Finset.mem_filter, SimpleGraph.mem_edgeFinset,
        SimpleGraph.mem_edgeSet] at hs
      rw [Sym2.map_mk, Finset.mem_coe, Finset.mem_filter, SimpleGraph.mem_edgeFinset,
        SimpleGraph.mem_edgeSet]
      refine ⟨?_, ?_⟩
      · refine (hadj _ _).mpr ?_
        rw [e.apply_symm_apply, e.apply_symm_apply]
        exact hs.1
      · rw [crosses_mk] at hs ⊢
        simpa [e.apply_symm_apply] using hs.2
  · intro s hs
    induction s using Sym2.ind with
    | _ u w =>
      rw [Finset.mem_coe, Finset.mem_filter, SimpleGraph.mem_edgeFinset,
        SimpleGraph.mem_edgeSet] at hs
      rw [Sym2.map_mk, Finset.mem_coe, Finset.mem_filter, SimpleGraph.mem_edgeFinset,
        SimpleGraph.mem_edgeSet]
      exact ⟨(hadj u w).mp hs.1, hs.2⟩
  · intro s _
    simp [Sym2.map_map]
  · intro s _
    simp [Sym2.map_map]

/-- Existence of a `k`-cut transfers across a bijection matching the two
adjacency relations — the shape the representation pair consumes. -/
theorem exists_cut_iff_of_equiv {W : Type*} [Fintype W]
    {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (e : V ≃ W) (hadj : ∀ a b : V, G.Adj a b ↔ H.Adj (e a) (e b)) (k : ℕ) :
    (∃ χ : V → Bool, k ≤ cutSize G χ) ↔ ∃ χ : W → Bool, k ≤ cutSize H χ := by
  constructor
  · rintro ⟨χ, hχ⟩
    refine ⟨fun w ↦ χ (e.symm w), ?_⟩
    rw [cutSize_eq_of_equiv e hadj]
    have hfun : (fun v ↦ χ (e.symm (e v))) = χ := by
      funext v
      rw [e.symm_apply_apply]
    rwa [hfun]
  · rintro ⟨χ, hχ⟩
    exact ⟨fun v ↦ χ (e v), by rwa [← cutSize_eq_of_equiv e hadj]⟩

/-! ## The problem -/

/-- **SIMPLE MAX CUT** [ND16, unit weights]: is there a bipartition of the
vertices crossed by at least `k` edges?

Hardness proof: from MAX 2SAT (`MaxCut/FromMaxSat2.lean`, certified). -/
def SIMPLE_MAX_CUT : Problem GraphThresholdInstance :=
  fun x ↦ ∃ χ : x.V → Bool, x.k ≤ cutSize x.G χ

end Hardness