import HardnessReductions.Core
import HardnessReductions.Networks.Defs
import Mathlib.Combinatorics.SimpleGraph.Acyclic

/-!
# STEINER TREE IN GRAPHS

Is there a subtree of `G` including every required vertex, of total weight at
most `B`?

Hardness proof (in `SteinerTree/`): from EXACT COVER BY 3-SETS
(`FromExactCover3.lean`, Garey–Johnson [ND12] — a root joined to a vertex per
available 3-set, each 3-set joined to its three elements, all weights `1`, the
root and the ground elements required; certified in
`FromExactCover3/Code.lean` and `FromExactCover3/Adequacy.lean`).

## The predicate

A subtree is presented as *the set of vertices it spans together with a graph
on that set*: `W : Finset V` and `T : SimpleGraph ↥W`, with `T` a tree
(mathlib's `IsTree`: connected and acyclic), every `T`-adjacency an adjacency
of `G`, and `R ⊆ W`. Its weight is the sum of `w` over its edges, read in the
ambient graph along the inclusion `↥W → V`.

Presenting the subtree on a carrier of its own — rather than as a subgraph of
`G` on all of `V` — is what keeps `IsTree` the right predicate: a graph on all
of `V` is connected only if it spans, and a Steiner tree spans `R`, not `V`.
The price is that renaming the vertices renames the subtree's *carrier* too;
`steinerTree_iff_of_equiv` pays it once, transporting `W` by image and `T`
along `SimpleGraph.Iso.map`, in the same way TRAVELING SALESMAN's invariance
lemma transports the index type of a tour.

## Weight and size

`subtreeWeight_of_weight_one` is the entry's arithmetic lemma: a subtree all of
whose edges weigh `1` costs exactly one less than the number of vertices it
spans. Both directions of a unit-weight reduction cross it — the construction
direction to price an explicit subtree, the reflection direction to bound the
number of vertices a subtree within budget can touch — and it is `IsTree`'s
edge count (`isTree_iff_connected_and_card`) with the sum evaluated.
-/

namespace Hardness

open SimpleGraph

/-- The weight of a subtree `T` spanning `W`: the sum of the instance's weight
over `T`'s edges, each read as a pair of ambient vertices. -/
noncomputable def subtreeWeight (x : SteinerInstance) {W : Finset x.V}
    (T : SimpleGraph {v // v ∈ W}) : ℕ :=
  ∑ e ∈ (Set.toFinite T.edgeSet).toFinset, x.w (Sym2.map Subtype.val e)

/-- STEINER TREE IN GRAPHS: is there a subtree of `G` spanning a vertex set
that includes every required vertex, of weight at most `B`? -/
def STEINER_TREE : Problem SteinerInstance := fun x ↦
  ∃ (W : Finset x.V) (T : SimpleGraph {v // v ∈ W}),
    x.R ⊆ W ∧ (∀ u v, T.Adj u v → x.G.Adj ↑u ↑v) ∧ T.IsTree ∧ subtreeWeight x T ≤ x.B

/-! ## Weight and size -/

/-- **A unit-weight subtree costs one less than it spans.** With every edge of
`T` weighing `1`, the weight sum counts `T`'s edges, and a tree on `W` has
`W.card - 1` of them. -/
theorem subtreeWeight_of_weight_one {x : SteinerInstance} {W : Finset x.V}
    {T : SimpleGraph {v // v ∈ W}} (hT : T.IsTree)
    (hw : ∀ e ∈ T.edgeSet, x.w (Sym2.map Subtype.val e) = 1) :
    subtreeWeight x T + 1 = W.card := by
  have hsum : subtreeWeight x T = (Set.toFinite T.edgeSet).toFinset.card := by
    rw [subtreeWeight,
      Finset.sum_congr rfl fun e he ↦ hw e ((Set.Finite.mem_toFinset _).mp he)]
    simp
  have hcard : (Set.toFinite T.edgeSet).toFinset.card = Nat.card T.edgeSet :=
    (Set.ncard_eq_toFinset_card _ _).symm
  rw [hsum, hcard, (isTree_iff_connected_and_card.mp hT).2, Nat.card_eq_fintype_card,
    Fintype.card_coe]

/-- An edge of a subtree is an edge of the ambient graph. -/
theorem mem_edgeSet_of_subtree {x : SteinerInstance} {W : Finset x.V}
    {T : SimpleGraph {v // v ∈ W}} (hTG : ∀ u v, T.Adj u v → x.G.Adj ↑u ↑v)
    {s : Sym2 {v // v ∈ W}} (hs : s ∈ T.edgeSet) :
    Sym2.map Subtype.val s ∈ x.G.edgeSet := by
  induction s using Sym2.ind with
  | _ a b => exact hTG a b hs

/-! ## Renaming invariance

An instance is inspected only through its adjacencies, its weights, its
required set and its bound, so a bijection of the vertices matching all four
preserves the answer. Unlike a colouring or a cover, the witness here has a
*carrier* of its own: the transported subtree lives on `W.image e`, and the
tree itself travels along `SimpleGraph.Iso.map`, which is what keeps `IsTree`
and the edge sum from having to be reproved. -/

/-- **Renaming invariance**, one direction. -/
theorem steinerTree_of_equiv {x y : SteinerInstance} (e : x.V ≃ y.V)
    (hG : ∀ a b, x.G.Adj a b ↔ y.G.Adj (e a) (e b))
    (hw : ∀ s ∈ x.G.edgeSet, x.w s = y.w (Sym2.map e s))
    (hR : ∀ v, v ∈ x.R ↔ e v ∈ y.R) (hB : x.B = y.B) :
    STEINER_TREE x → STEINER_TREE y := by
  rintro ⟨W, T, hRW, hTG, hTtree, hwt⟩
  have hmem : ∀ v : x.V, v ∈ W ↔ e v ∈ W.image e := fun v ↦ by
    simp [Finset.mem_image, e.injective.eq_iff]
  set eW : {v // v ∈ W} ≃ {v // v ∈ W.image e} := e.subtypeEquiv hmem with heW
  have hval : ∀ v : {v // v ∈ W}, (eW.toEmbedding v).val = e v.val := fun _ ↦ rfl
  have hcomp : ∀ v : {v // v ∈ W.image e}, e ((eW.symm v : {v // v ∈ W}) : x.V) = (v : y.V) := by
    intro v
    have h := hval (eW.symm v)
    rw [show eW.toEmbedding (eW.symm v) = v from eW.apply_symm_apply v] at h
    exact h.symm
  -- the transported subtree, and the two facts about its edges
  have hedge : ∀ s : Sym2 {v // v ∈ W},
      s ∈ T.edgeSet ↔ Sym2.map eW s ∈ (T.map eW.toEmbedding).edgeSet := by
    intro s
    rw [edgeSet_map, Set.mem_image]
    refine ⟨fun hs ↦ ⟨s, hs, rfl⟩, ?_⟩
    rintro ⟨t, ht, hts⟩
    rw [Function.Embedding.sym2Map_apply] at hts
    rwa [Sym2.map.injective eW.injective hts] at ht
  have hweight : subtreeWeight y (T.map eW.toEmbedding) = subtreeWeight x T := by
    refine Finset.sum_nbij' (i := fun s ↦ Sym2.map eW.symm s) (j := fun s ↦ Sym2.map eW s)
      ?_ ?_ ?_ ?_ ?_
    · intro s hs
      rw [Set.Finite.mem_toFinset] at hs ⊢
      refine (hedge (Sym2.map eW.symm s)).mpr ?_
      rwa [Sym2.map_map, Equiv.self_comp_symm, Sym2.map_id, id_eq]
    · intro s hs
      rw [Set.Finite.mem_toFinset] at hs ⊢
      exact (hedge s).mp hs
    · intro s _
      rw [Sym2.map_map, Equiv.self_comp_symm, Sym2.map_id, id_eq]
    · intro s _
      rw [Sym2.map_map, Equiv.symm_comp_self, Sym2.map_id, id_eq]
    · intro s hs
      rw [Set.Finite.mem_toFinset] at hs
      have hTs : Sym2.map eW.symm s ∈ T.edgeSet := by
        refine (hedge (Sym2.map eW.symm s)).mpr ?_
        rwa [Sym2.map_map, Equiv.self_comp_symm, Sym2.map_id, id_eq]
      have hmap : Sym2.map Subtype.val s
          = Sym2.map e (Sym2.map Subtype.val (Sym2.map eW.symm s)) := by
        rw [Sym2.map_map, Sym2.map_map]
        refine congrFun (congrArg Sym2.map (funext fun v ↦ ?_)) s
        exact (hcomp v).symm
      rw [hmap, ← hw _ (mem_edgeSet_of_subtree hTG hTs)]
  refine ⟨W.image e, T.map eW.toEmbedding, ?_, ?_, ?_, ?_⟩
  · intro v' hv'
    have : e (e.symm v') ∈ W.image e := (hmem _).mp (hRW ((hR _).mpr (by rwa [e.apply_symm_apply])))
    rwa [e.apply_symm_apply] at this
  · intro u v huv
    obtain ⟨a, b, hab, rfl, rfl⟩ := (map_adj _ _ _ _).mp huv
    rw [hval, hval]
    exact (hG _ _).mp (hTG a b hab)
  · exact (SimpleGraph.Iso.map eW T).isTree_iff.mp hTtree
  · rw [hweight, ← hB]
    exact hwt

/-- **Renaming invariance**: STEINER TREE sees the vertices only through the
adjacencies, weights, required set and bound. -/
theorem steinerTree_iff_of_equiv {x y : SteinerInstance} (e : x.V ≃ y.V)
    (hG : ∀ a b, x.G.Adj a b ↔ y.G.Adj (e a) (e b))
    (hw : ∀ s ∈ x.G.edgeSet, x.w s = y.w (Sym2.map e s))
    (hR : ∀ v, v ∈ x.R ↔ e v ∈ y.R) (hB : x.B = y.B) :
    STEINER_TREE x ↔ STEINER_TREE y :=
  ⟨steinerTree_of_equiv e hG hw hR hB,
    steinerTree_of_equiv e.symm
      (fun a b ↦ by rw [hG, e.apply_symm_apply, e.apply_symm_apply])
      (fun s hs ↦ by
        have hs' : Sym2.map e.symm s ∈ x.G.edgeSet := by
          induction s using Sym2.ind with
          | _ a b =>
            rw [Sym2.map_mk]
            exact (hG _ _).mpr (by rwa [e.apply_symm_apply, e.apply_symm_apply])
        rw [hw _ hs', Sym2.map_map, Equiv.self_comp_symm, Sym2.map_id, id_eq])
      (fun v ↦ by rw [hR, e.apply_symm_apply]) hB.symm⟩

end Hardness