import MaxLeafFormal.SteinerDir
import MaxLeafFormal.CDS
import MaxLeafFormal.MLS
import MaxLeafFormal.Budget

/-!
# States, the directed encoding, `lem:cds-dir-steiner` and `cor:cds-steiner`, correctness
-/

namespace MaxLeafFormal.SteinerCDS

open Finset MaxLeafFormal.CDS

/-- A triple `(𝒟, B, R)` (def:cds-state). Declared before the section variables. -/
structure State (V : Type*) where
  D : Finset (Finset V)
  B : Finset V
  R : Finset V

/-! Auxiliary facts about `ℕ∞` infima and induced subgraphs. -/

theorem sInf_le_sInf_of_exists {s t : Set ℕ∞} (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) :
    sInf t ≤ sInf s :=
  le_sInf fun x hx => by
    obtain ⟨y, hy, hyx⟩ := h x hx
    exact (sInf_le hy).trans hyx

theorem induce_reach_mono {V : Type*} (G : SimpleGraph V) {s t : Set V} (hst : s ⊆ t) {x y : V}
    (hx : x ∈ s) (hy : y ∈ s) (h : (G.induce s).Reachable ⟨x, hx⟩ ⟨y, hy⟩) :
    (G.induce t).Reachable ⟨x, hst hx⟩ ⟨y, hst hy⟩ := by
  rw [SimpleGraph.reachable_iff_reflTransGen] at h ⊢
  have key : ∀ z : s, Relation.ReflTransGen (G.induce s).Adj ⟨x, hx⟩ z →
      Relation.ReflTransGen (G.induce t).Adj ⟨x, hst hx⟩ ⟨z.1, hst z.2⟩ := by
    intro z hz
    induction hz with
    | refl => exact .refl
    | tail _ hab ih => exact ih.tail hab
  exact key _ h

theorem induce_reach_step {V : Type*} (G : SimpleGraph V) {s : Set V} {c x y : V} (hc : c ∈ s)
    (hx : x ∈ s) (hy : y ∈ s) (h : (G.induce s).Reachable ⟨c, hc⟩ ⟨x, hx⟩) (hxy : G.Adj x y) :
    (G.induce s).Reachable ⟨c, hc⟩ ⟨y, hy⟩ :=
  h.trans (SimpleGraph.Adj.reachable (G := G.induce s) (u := ⟨x, hx⟩) (v := ⟨y, hy⟩) hxy)

variable {V : Type*} [Fintype V] [DecidableEq V]

/-- `V(𝒟)`. -/
def State.VD (J : State V) : Finset V := J.D.biUnion id

variable (G : SimpleGraph V) [DecidableRel G.Adj]

/-- def:cds-state. -/
def IsState (J : State V) : Prop :=
  (∀ C ∈ J.D, (G.induce (C : Set V)).Connected) ∧
  (∀ C ∈ J.D, ∀ C' ∈ J.D, C ≠ C' → Disjoint C C' ∧ ∀ a ∈ C, ∀ b ∈ C', ¬ G.Adj a b) ∧
  Disjoint J.B J.VD ∧ Disjoint J.R (closedNbhd G J.VD)

/-- Solutions (def:cds-state); `Connected` includes `V(𝒟) ∪ Y ≠ ∅`. -/
def IsSol (J : State V) (Y : Finset V) : Prop :=
  Y ⊆ J.B ∧ J.R ⊆ closedNbhd G Y ∧ (G.induce ((J.VD ∪ Y : Finset V) : Set V)).Connected

/-- `OPT_φ(J)`, `⊤` if there is no solution. -/
noncomputable def optSt (J : State V) (φ : V → ℕ) : ℕ∞ :=
  sInf ((fun Y : Finset V => ((∑ b ∈ Y, φ b : ℕ) : ℕ∞)) '' {Y | IsSol G J Y})

/-- Vertices of `G⃗_J`: `Ĉ`, `b̂`, `ř` (def:cds-dir-encoding). -/
abbrev EncV (J : State V) : Type _ := ({C // C ∈ J.D} ⊕ {b // b ∈ J.B}) ⊕ {r // r ∈ J.R}

/-- Arcs of `G⃗_J` (def:cds-dir-encoding). The cases do not overlap: the last three list all pairs
that are not arcs. -/
def encAdj (J : State V) : EncV J → EncV J → Prop
  | .inl (.inr b), .inl (.inr b') => G.Adj b.1 b'.1
  | .inl (.inl C), .inl (.inr b) => ∃ c ∈ C.1, G.Adj c b.1
  | .inl (.inr b), .inl (.inl C) => ∃ c ∈ C.1, G.Adj c b.1
  | .inl (.inr b), .inr r => b.1 = r.1 ∨ G.Adj b.1 r.1
  | .inl (.inl _), .inl (.inl _) => False
  | .inl (.inl _), .inr _ => False
  | .inr _, _ => False

/-- Arcs of `G⃗_J` are decidable, by cases on the constructors (computable). The body is not
fixed (any instance will do, since `Decidable` is a subsingleton). -/
instance encAdj.instDecidableRel (J : State V) : DecidableRel (encAdj G J) := by
  intro x y
  rcases x with (C | b) | r <;> rcases y with (C' | b') | r' <;> simp only [encAdj] <;>
    infer_instance

/-- Weights: `φ(b)` on `b̂`, `0` on `Ĉ` and `ř`. -/
def encWt (J : State V) (φ : V → ℕ) : EncV J → ℕ
  | .inl (.inr b) => φ b.1
  | _ => 0

def encRoot (J : State V) (C₁ : Finset V) (h : C₁ ∈ J.D) : EncV J := .inl (.inl ⟨C₁, h⟩)

open Classical in
/-- `K₁ = {Ĉ : C ∈ 𝒟 \ {C₁}} ∪ Ř` (lem:cds-dir-steiner). -/
noncomputable def encTerm (J : State V) (C₁ : Finset V) : Finset (EncV J) :=
  univ.filter fun w => match w with
    | .inl (.inl C) => C.1 ≠ C₁
    | .inl (.inr _) => False
    | .inr _ => True

/-- `steinerAlg` on the encoding, with root `Ĉ₁`; arcs decided by `encAdj.instDecidableRel`. -/
noncomputable def encAlg (J : State V) (φ : V → ℕ) (C₁ : Finset V) (h : C₁ ∈ J.D) : ℕ∞ :=
  SteinerDir.steinerAlg (encAdj G J) (encWt J φ) (encRoot J C₁ h) (encTerm J C₁)

/-- `J^{(b)}` (proof of lem:cds-dir-steiner). -/
def Jb (J : State V) (b : V) : State V := ⟨{{b}}, J.B.erase b, J.R \ closedNbhd G {b}⟩

/-- The computation of lem:cds-dir-steiner. -/
noncomputable def stateAlg (J : State V) (φ : V → ℕ) : ℕ∞ :=
  if h : J.D.Nonempty then encAlg G J φ h.choose h.choose_spec
  else J.B.inf fun b => (φ b : ℕ∞) + encAlg G (Jb G J b) φ {b} (mem_singleton_self {b})

/-! ### Auxiliary lemmas for `eq:cds-dir-match` -/

section Aux

theorem mem_encTerm_C (J : State V) (C₁ : Finset V) (C : {C // C ∈ J.D}) :
    (.inl (.inl C) : EncV J) ∈ encTerm J C₁ ↔ C.1 ≠ C₁ := by
  simp [encTerm]

theorem not_mem_encTerm_B (J : State V) (C₁ : Finset V) (b : {b // b ∈ J.B}) :
    (.inl (.inr b) : EncV J) ∉ encTerm J C₁ := by
  simp [encTerm]

theorem mem_encTerm_R (J : State V) (C₁ : Finset V) (r : {r // r ∈ J.R}) :
    (.inr r : EncV J) ∈ encTerm J C₁ := by
  simp [encTerm]

/-- The vertices `b̂` for `b ∈ Y ∩ B`. -/
def liftB (J : State V) (Y : Finset V) : Finset (EncV J) :=
  (Y.subtype (· ∈ J.B)).image fun b => .inl (.inr b)

theorem mem_liftB_B (J : State V) (Y : Finset V) (b : {b // b ∈ J.B}) :
    (.inl (.inr b) : EncV J) ∈ liftB J Y ↔ b.1 ∈ Y := by
  rw [liftB, mem_image]
  constructor
  · rintro ⟨a, ha, he⟩
    simp only [Sum.inl.injEq, Sum.inr.injEq] at he
    subst he
    exact mem_subtype.mp ha
  · intro hb
    exact ⟨b, mem_subtype.mpr hb, rfl⟩

theorem mem_liftB (J : State V) (Y : Finset V) (x : EncV J) (hx : x ∈ liftB J Y) :
    ∃ b : {b // b ∈ J.B}, b.1 ∈ Y ∧ x = .inl (.inr b) := by
  rw [liftB, mem_image] at hx
  obtain ⟨b, hb, rfl⟩ := hx
  exact ⟨b, mem_subtype.mp hb, rfl⟩

theorem sum_liftB (J : State V) (φ : V → ℕ) (Y : Finset V) (hY : Y ⊆ J.B) :
    ∑ x ∈ liftB J Y, encWt J φ x = ∑ b ∈ Y, φ b := by
  rw [liftB, sum_image (fun a _ b _ h => by simpa using h)]
  simp only [encWt]
  rw [sum_subtype_eq_sum_filter φ, filter_true_of_mem (fun x hx => hY hx)]

/-- Reachability from the root through arcs whose heads lie in `{r} ∪ K₁ ∪ D'`. -/
abbrev EReach (J : State V) (C₁ : Finset V) (h : C₁ ∈ J.D) (D' : Finset (EncV J)) (x : EncV J) :
    Prop :=
  Relation.ReflTransGen
    (fun u v => encAdj G J u v ∧ v ∈ insert (encRoot J C₁ h) (encTerm J C₁ ∪ D'))
    (encRoot J C₁ h) x

theorem mem_VD {J : State V} {x : V} : x ∈ J.VD ↔ ∃ C ∈ J.D, x ∈ C := by
  simp [State.VD]

/-- Solutions give feasible sets (proof of lem:cds-dir-steiner). -/
theorem feasible_liftB (J : State V) (hJ : IsState G J) (C₁ : Finset V) (h : C₁ ∈ J.D)
    (Y : Finset V) (hY : IsSol G J Y) :
    SteinerDir.Feasible (encAdj G J) (encRoot J C₁ h) (encTerm J C₁) (liftB J Y) := by
  obtain ⟨hYB, hRY, hconn⟩ := hY
  obtain ⟨hDconn, hDdisj, hBD, -⟩ := hJ
  set S : Set V := ((J.VD ∪ Y : Finset V) : Set V) with hS
  have hCH : ∀ C (hC : C ∈ J.D), (.inl (.inl ⟨C, hC⟩) : EncV J) ∈
      insert (encRoot J C₁ h) (encTerm J C₁ ∪ liftB J Y) := by
    intro C hC
    by_cases hC1 : C = C₁
    · subst hC1; exact mem_insert_self _ _
    · exact mem_insert_of_mem (mem_union_left _ ((mem_encTerm_C J C₁ ⟨C, hC⟩).mpr hC1))
  have hbH : ∀ b (hb : b ∈ J.B), b ∈ Y → (.inl (.inr ⟨b, hb⟩) : EncV J) ∈
      insert (encRoot J C₁ h) (encTerm J C₁ ∪ liftB J Y) := by
    intro b hb hbY
    exact mem_insert_of_mem (mem_union_right _ ((mem_liftB_B J Y ⟨b, hb⟩).mpr hbY))
  obtain ⟨⟨c₁, hc₁⟩⟩ := (hDconn C₁ h).nonempty
  have hc₁' : c₁ ∈ C₁ := hc₁
  have hVS : ∀ C ∈ J.D, ∀ z ∈ C, z ∈ S := by
    intro C hC z hz
    rw [hS, mem_coe]
    exact mem_union_left _ (mem_VD.mpr ⟨C, hC, hz⟩)
  have hc₁S : c₁ ∈ S := hVS C₁ h c₁ hc₁'
  have key : ∀ z : S, Relation.ReflTransGen (G.induce S).Adj ⟨c₁, hc₁S⟩ z →
      (∀ hzB : z.1 ∈ J.B, z.1 ∈ Y → EReach G J C₁ h (liftB J Y) (.inl (.inr ⟨z.1, hzB⟩))) ∧
      (∀ C (hC : C ∈ J.D), z.1 ∈ C → EReach G J C₁ h (liftB J Y) (.inl (.inl ⟨C, hC⟩))) := by
    intro z hz
    induction hz with
    | refl =>
      refine ⟨fun hzB _ => ?_, fun C hC hzC => ?_⟩
      · exact absurd (mem_VD.mpr ⟨C₁, h, hc₁'⟩) (disjoint_left.mp hBD hzB)
      · have hCC : C = C₁ := by
          by_contra hne
          exact disjoint_left.mp (hDdisj C hC C₁ h hne).1 hzC hc₁'
        subst hCC
        exact Relation.ReflTransGen.refl
    | @tail x z _ hxz ih =>
      have hxz' : G.Adj x.1 z.1 := hxz
      obtain ⟨ihB, ihC⟩ := ih
      have hx : x.1 ∈ J.VD ∪ Y := x.2
      rw [mem_union, mem_VD] at hx
      refine ⟨fun hzB hzY => ?_, fun C hC hzC => ?_⟩
      · rcases hx with ⟨C', hC', hxC'⟩ | hxY
        · exact Relation.ReflTransGen.tail (ihC C' hC' hxC') ⟨⟨x.1, hxC', hxz'⟩, hbH _ hzB hzY⟩
        · exact Relation.ReflTransGen.tail (ihB (hYB hxY) hxY) ⟨hxz', hbH _ hzB hzY⟩
      · rcases hx with ⟨C', hC', hxC'⟩ | hxY
        · by_cases hCC : C' = C
          · subst hCC; exact ihC C' hC' hxC'
          · exact absurd hxz' ((hDdisj C' hC' C hC hCC).2 x.1 hxC' z.1 hzC)
        · exact Relation.ReflTransGen.tail (ihB (hYB hxY) hxY) ⟨⟨z.1, hzC, hxz'.symm⟩, hCH C hC⟩
  have reach : ∀ z (hz : z ∈ S), Relation.ReflTransGen (G.induce S).Adj ⟨c₁, hc₁S⟩ ⟨z, hz⟩ :=
    fun z hz => (SimpleGraph.reachable_iff_reflTransGen _ _).mp (hconn.preconnected _ _)
  refine ⟨?_, ?_, ?_⟩
  · intro hr
    obtain ⟨b, -, hb⟩ := mem_liftB J Y _ hr
    simp [encRoot] at hb
  · rw [disjoint_left]
    intro x hx1 hx2
    obtain ⟨b, -, rfl⟩ := mem_liftB J Y _ hx2
    exact not_mem_encTerm_B J C₁ b hx1
  · intro k hk
    rcases k with (⟨C, hC⟩ | ⟨b, hb⟩) | ⟨r, hr⟩
    · obtain ⟨⟨z, hz⟩⟩ := (hDconn C hC).nonempty
      have hz' : z ∈ C := hz
      exact (key ⟨z, hVS C hC z hz'⟩ (reach _ _)).2 C hC hz'
    · exact absurd hk (not_mem_encTerm_B J C₁ ⟨b, hb⟩)
    · have hrN := hRY hr
      have hrK : (.inr ⟨r, hr⟩ : EncV J) ∈ insert (encRoot J C₁ h) (encTerm J C₁ ∪ liftB J Y) :=
        mem_insert_of_mem (mem_union_left _ (mem_encTerm_R J C₁ ⟨r, hr⟩))
      rw [mem_closedNbhd] at hrN
      rcases hrN with hrY | ⟨y, hyY, hyr⟩
      · have hrS : r ∈ S := by rw [hS, mem_coe]; exact mem_union_right _ hrY
        exact Relation.ReflTransGen.tail ((key ⟨r, hrS⟩ (reach _ _)).1 (hYB hrY) hrY) ⟨Or.inl rfl, hrK⟩
      · have hyS : y ∈ S := by rw [hS, mem_coe]; exact mem_union_right _ hyY
        exact Relation.ReflTransGen.tail ((key ⟨y, hyS⟩ (reach _ _)).1 (hYB hyY) hyY) ⟨Or.inr hyr, hrK⟩

/-- Feasible sets give solutions of no larger weight (proof of lem:cds-dir-steiner). -/
theorem sol_of_feasible (J : State V) (hJ : IsState G J) (φ : V → ℕ) (C₁ : Finset V)
    (h : C₁ ∈ J.D) (D' : Finset (EncV J))
    (hD : SteinerDir.Feasible (encAdj G J) (encRoot J C₁ h) (encTerm J C₁) D') :
    ∃ Y, IsSol G J Y ∧ ∑ b ∈ Y, φ b ≤ ∑ x ∈ D', encWt J φ x := by
  classical
  obtain ⟨-, -, hreach⟩ := hD
  obtain ⟨hDconn, -, -, -⟩ := hJ
  set Y : Finset V := J.B.filter
    (fun b => ∃ hb : b ∈ J.B, EReach G J C₁ h D' (.inl (.inr ⟨b, hb⟩))) with hYdef
  have hYB : Y ⊆ J.B := filter_subset _ _
  have hmemY : ∀ b (hb : b ∈ J.B), EReach G J C₁ h D' (.inl (.inr ⟨b, hb⟩)) → b ∈ Y :=
    fun b hb hr => mem_filter.mpr ⟨hb, hb, hr⟩
  have hYmem : ∀ b ∈ Y, ∃ hb : b ∈ J.B, EReach G J C₁ h D' (.inl (.inr ⟨b, hb⟩)) :=
    fun b hbY => (mem_filter.mp hbY).2
  have hinD : ∀ b (hb : b ∈ J.B), EReach G J C₁ h D' (.inl (.inr ⟨b, hb⟩)) →
      (.inl (.inr ⟨b, hb⟩) : EncV J) ∈ D' := by
    intro b hb hr
    rcases Relation.ReflTransGen.cases_tail hr with he | ⟨c, _, _, hcH⟩
    · simp [encRoot] at he
    · rcases mem_insert.mp hcH with he | hcH
      · simp [encRoot] at he
      rcases mem_union.mp hcH with hK | hD
      · exact absurd hK (not_mem_encTerm_B J C₁ ⟨b, hb⟩)
      · exact hD
  have hroot : ∀ C (hC : C ∈ J.D), EReach G J C₁ h D' (.inl (.inl ⟨C, hC⟩)) := by
    intro C hC
    by_cases hC1 : C = C₁
    · subst hC1; exact Relation.ReflTransGen.refl
    · exact hreach _ ((mem_encTerm_C J C₁ ⟨C, hC⟩).mpr hC1)
  refine ⟨Y, ⟨hYB, ?_, ?_⟩, ?_⟩
  · -- `R ⊆ N[Y]`
    intro r hr
    have := hreach _ (mem_encTerm_R J C₁ ⟨r, hr⟩)
    rcases Relation.ReflTransGen.cases_tail this with he | ⟨c, hc, hcr, _⟩
    · simp [encRoot] at he
    · rcases c with (⟨C, hC⟩ | ⟨b, hb⟩) | ⟨r', hr'⟩
      · simp [encAdj] at hcr
      · have hbY : b ∈ Y := hmemY b hb hc
        rw [mem_closedNbhd]
        simp only [encAdj] at hcr
        rcases hcr with hbr | hadj
        · exact Or.inl (hbr ▸ hbY)
        · exact Or.inr ⟨b, hbY, hadj⟩
      · simp [encAdj] at hcr
  · -- connectivity of `G[V(𝒟) ∪ Y]`
    set S : Set V := ((J.VD ∪ Y : Finset V) : Set V) with hS
    obtain ⟨⟨c₁, hc₁⟩⟩ := (hDconn C₁ h).nonempty
    have hc₁' : c₁ ∈ C₁ := hc₁
    have hVS : ∀ C ∈ J.D, ∀ z ∈ C, z ∈ S := by
      intro C hC z hz
      rw [hS, mem_coe]
      exact mem_union_left _ (mem_VD.mpr ⟨C, hC, hz⟩)
    have hYS : ∀ b ∈ Y, b ∈ S := by
      intro b hb
      rw [hS, mem_coe]
      exact mem_union_right _ hb
    have hc₁S : c₁ ∈ S := hVS C₁ h c₁ hc₁'
    -- `IR z`: `z` is reachable from `c₁` inside `S`
    have hCall : ∀ C (hC : C ∈ J.D) (c z : V) (hc : c ∈ C) (hz : z ∈ C),
        (G.induce S).Reachable ⟨c₁, hc₁S⟩ ⟨c, hVS C hC c hc⟩ →
        (G.induce S).Reachable ⟨c₁, hc₁S⟩ ⟨z, hVS C hC z hz⟩ := by
      intro C hC c z hc hz hr
      have h1 := (hDconn C hC).preconnected ⟨c, hc⟩ ⟨z, hz⟩
      exact hr.trans (induce_reach_mono G (s := (C : Set V)) (t := S) (fun v hv => hVS C hC v hv)
        hc hz h1)
    have Q : ∀ x, EReach G J C₁ h D' x →
        (∀ C (hC : C ∈ J.D), x = .inl (.inl ⟨C, hC⟩) → ∀ z (hz : z ∈ C),
          (G.induce S).Reachable ⟨c₁, hc₁S⟩ ⟨z, hVS C hC z hz⟩) ∧
        (∀ b (hb : b ∈ J.B), x = .inl (.inr ⟨b, hb⟩) → ∀ hbS : b ∈ S,
          (G.induce S).Reachable ⟨c₁, hc₁S⟩ ⟨b, hbS⟩) := by
      intro x hx
      unfold EReach at hx
      induction hx with
      | refl =>
        refine ⟨fun C hC he z hz => ?_, fun b hb he => ?_⟩
        · simp only [encRoot, Sum.inl.injEq, Subtype.mk.injEq] at he
          have hc₁C : c₁ ∈ C := he ▸ hc₁'
          exact hCall C hC c₁ z hc₁C hz (SimpleGraph.Reachable.refl _)
        · simp [encRoot] at he
      | @tail a x hra hax ih =>
        obtain ⟨harc, -⟩ := hax
        obtain ⟨ihC, ihB⟩ := ih
        rcases a with (⟨C, hC⟩ | ⟨b, hb⟩) | ⟨r, hr⟩ <;>
          rcases x with (⟨C', hC'⟩ | ⟨b', hb'⟩) | ⟨r', hr'⟩ <;>
          simp only [encAdj] at harc
        · -- `Ĉ → b̂'`
          refine ⟨fun _ _ he => by simp at he, fun b₀ hb₀ he hbS => ?_⟩
          simp only [Sum.inl.injEq, Sum.inr.injEq, Subtype.mk.injEq] at he
          subst he
          obtain ⟨c, hc, hcb⟩ := harc
          exact induce_reach_step G hc₁S (hVS C hC c hc) hbS
            (ihC C hC rfl c hc) hcb
        · -- `b̂ → Ĉ'`
          refine ⟨fun C₀ hC₀ he z hz => ?_, fun _ _ he => by simp at he⟩
          simp only [Sum.inl.injEq, Subtype.mk.injEq] at he
          subst he
          obtain ⟨c, hc, hcb⟩ := harc
          have hbY : b ∈ Y := hmemY b hb hra
          have h1 := ihB b hb rfl (hYS b hbY)
          exact hCall _ hC₀ c z hc hz
            (induce_reach_step G hc₁S (hYS b hbY) _ h1 hcb.symm)
        · -- `b̂ → b̂'`
          refine ⟨fun _ _ he => by simp at he, fun b₀ hb₀ he hbS => ?_⟩
          simp only [Sum.inl.injEq, Sum.inr.injEq, Subtype.mk.injEq] at he
          subst he
          have hbY : b ∈ Y := hmemY b hb hra
          exact induce_reach_step G hc₁S (hYS b hbY) hbS (ihB b hb rfl (hYS b hbY)) harc
        · -- `b̂ → ř'`
          exact ⟨fun _ _ he => by simp at he, fun _ _ he => by simp at he⟩
    have hIR : ∀ z (hz : z ∈ S), (G.induce S).Reachable ⟨c₁, hc₁S⟩ ⟨z, hz⟩ := by
      intro z hz
      have hz' : z ∈ J.VD ∪ Y := hz
      rw [mem_union, mem_VD] at hz'
      rcases hz' with ⟨C, hC, hzC⟩ | hzY
      · exact (Q _ (hroot C hC)).1 C hC rfl z hzC
      · obtain ⟨hb, hr⟩ := hYmem z hzY
        exact (Q _ hr).2 z hb rfl hz
    rw [SimpleGraph.connected_iff]
    exact ⟨fun u v => (hIR u.1 u.2).symm.trans (hIR v.1 v.2), ⟨⟨c₁, hc₁S⟩⟩⟩
  · -- weights
    rw [← sum_liftB J φ Y hYB]
    refine sum_le_sum_of_subset_of_nonneg (fun x hx => ?_) (fun _ _ _ => Nat.zero_le _)
    obtain ⟨⟨b, hb⟩, hbY, rfl⟩ := mem_liftB J Y x hx
    obtain ⟨hb', hr⟩ := hYmem b hbY
    exact hinD b hb' hr

theorem optSt_attained (J : State V) (φ : V → ℕ) (h : optSt G J φ ≠ ⊤) :
    ∃ Y, IsSol G J Y ∧ optSt G J φ = ((∑ b ∈ Y, φ b : ℕ) : ℕ∞) := by
  unfold optSt at h ⊢
  have hne : ((fun Y : Finset V => ((∑ b ∈ Y, φ b : ℕ) : ℕ∞)) '' {Y | IsSol G J Y}).Nonempty := by
    by_contra hemp
    rw [Set.not_nonempty_iff_eq_empty] at hemp
    rw [hemp, sInf_empty] at h
    exact h rfl
  obtain ⟨Y, hY, hYeq⟩ := csInf_mem hne
  exact ⟨Y, hY, hYeq.symm⟩

end Aux

-- eq:cds-dir-match; no decidability instance on the arcs is involved
theorem optSt_eq_optDir (J : State V) (hJ : IsState G J) (φ : V → ℕ)
    (C₁ : Finset V) (h : C₁ ∈ J.D) :
    optSt G J φ =
      SteinerDir.optDir (encAdj G J) (encWt J φ) (encRoot J C₁ h) (encTerm J C₁) := by
  unfold optSt SteinerDir.optDir
  apply le_antisymm
  · apply sInf_le_sInf_of_exists
    rintro _ ⟨D', hD', rfl⟩
    obtain ⟨Y, hY, hle⟩ := sol_of_feasible G J hJ φ C₁ h D' hD'
    exact ⟨_, ⟨Y, hY, rfl⟩, Nat.cast_le.mpr hle⟩
  · apply sInf_le_sInf_of_exists
    rintro _ ⟨Y, hY, rfl⟩
    refine ⟨_, ⟨liftB J Y, feasible_liftB G J hJ C₁ h Y hY, rfl⟩, ?_⟩
    exact le_of_eq (by simp only [sum_liftB J φ Y hY.1])

-- The case 𝒟 = ∅
theorem isState_Jb (J : State V) (b : V) :
    IsState G (Jb G J b) := by
  have hVD : (Jb G J b).VD = {b} := by simp [Jb, State.VD]
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro C hC
    simp only [Jb, mem_singleton] at hC
    subst hC
    rw [SimpleGraph.connected_iff]
    refine ⟨fun u v => ?_, ?_⟩
    swap
    · exact ⟨⟨b, by simp⟩⟩
    have hu : u.1 = b := by have := u.2; simpa using this
    have hv : v.1 = b := by have := v.2; simpa using this
    have : u = v := Subtype.ext (hu.trans hv.symm)
    subst this
    exact SimpleGraph.Reachable.refl _
  · intro C hC C' hC' hne
    simp only [Jb, mem_singleton] at hC hC'
    exact absurd (hC.trans hC'.symm) hne
  · rw [hVD]
    simp [Jb]
  · rw [hVD]
    exact sdiff_disjoint

theorem optSt_eq_inf_Jb (J : State V) (hD : J.D = ∅) (φ : V → ℕ) :
    optSt G J φ = J.B.inf fun b => (φ b : ℕ∞) + optSt G (Jb G J b) φ := by
  have hVD : J.VD = ∅ := by simp [State.VD, hD]
  have hVDb : ∀ b, (Jb G J b).VD = {b} := by intro b; simp [Jb, State.VD]
  apply le_antisymm
  · refine Finset.le_inf fun b hb => ?_
    by_cases htop : optSt G (Jb G J b) φ = ⊤
    · rw [htop, add_top]; exact le_top
    obtain ⟨Y', hY', heq⟩ := optSt_attained G _ φ htop
    rw [heq]
    obtain ⟨hY'B, hY'R, hY'c⟩ := hY'
    have hbY' : b ∉ Y' := fun hm => by
      have := hY'B hm
      simp [Jb] at this
    have hsol : IsSol G J (insert b Y') := by
      refine ⟨?_, ?_, ?_⟩
      · rw [insert_subset_iff]
        exact ⟨hb, fun x hx => (mem_erase.mp (hY'B hx)).2⟩
      · intro x hx
        rw [mem_closedNbhd]
        by_cases hxb : x ∈ closedNbhd G {b}
        · rw [mem_closedNbhd] at hxb
          rcases hxb with hxb | ⟨y, hy, hyx⟩
          · exact Or.inl (mem_insert.mpr (Or.inl (mem_singleton.mp hxb)))
          · exact Or.inr ⟨y, mem_insert.mpr (Or.inl (mem_singleton.mp hy)), hyx⟩
        · have hx' : x ∈ (Jb G J b).R := by simp [Jb, hx, hxb]
          have := hY'R hx'
          rw [mem_closedNbhd] at this
          rcases this with hxY | ⟨y, hy, hyx⟩
          · exact Or.inl (mem_insert_of_mem hxY)
          · exact Or.inr ⟨y, mem_insert_of_mem hy, hyx⟩
      · have hset : J.VD ∪ insert b Y' = (Jb G J b).VD ∪ Y' := by
          rw [hVD, hVDb, empty_union, insert_eq]
        rw [hset]
        exact hY'c
    have h2 : sInf ((fun Y : Finset V => ((∑ b ∈ Y, φ b : ℕ) : ℕ∞)) '' {Y | IsSol G J Y}) ≤
        ((∑ x ∈ insert b Y', φ x : ℕ) : ℕ∞) := sInf_le ⟨insert b Y', hsol, rfl⟩
    refine h2.trans (le_of_eq ?_)
    rw [sum_insert hbY', Nat.cast_add]
  · refine le_sInf ?_
    rintro _ ⟨Y, hY, rfl⟩
    obtain ⟨hYB, hYR, hYc⟩ := hY
    obtain ⟨⟨b, hbS⟩⟩ := hYc.nonempty
    have hbY : b ∈ Y := by
      have : b ∈ J.VD ∪ Y := hbS
      rwa [hVD, empty_union] at this
    have hsol : IsSol G (Jb G J b) (Y.erase b) := by
      refine ⟨?_, ?_, ?_⟩
      · exact erase_subset_erase b hYB
      · intro x hx
        simp only [Jb, mem_sdiff] at hx
        obtain ⟨hxR, hxb⟩ := hx
        rw [mem_closedNbhd] at hxb
        have := hYR hxR
        rw [mem_closedNbhd] at this ⊢
        rcases this with hxY | ⟨y, hy, hyx⟩
        · refine Or.inl (mem_erase.mpr ⟨fun he => hxb (Or.inl (mem_singleton.mpr he)), hxY⟩)
        · refine Or.inr ⟨y, mem_erase.mpr ⟨fun he => hxb (Or.inr ⟨y, mem_singleton.mpr he, hyx⟩),
            hy⟩, hyx⟩
      · have hset : (Jb G J b).VD ∪ Y.erase b = J.VD ∪ Y := by
          rw [hVD, hVDb, empty_union, ← insert_eq, insert_erase hbY]
        rw [hset]
        exact hYc
    refine (Finset.inf_le (hYB hbY)).trans ?_
    have h1 : optSt G (Jb G J b) φ ≤ ((∑ x ∈ Y.erase b, φ x : ℕ) : ℕ∞) :=
      sInf_le ⟨Y.erase b, hsol, rfl⟩
    calc (φ b : ℕ∞) + optSt G (Jb G J b) φ ≤ (φ b : ℕ∞) + ((∑ x ∈ Y.erase b, φ x : ℕ) : ℕ∞) :=
          add_le_add le_rfl h1
      _ = ((∑ x ∈ Y, φ x : ℕ) : ℕ∞) := by
          rw [← add_sum_erase Y φ hbY, Nat.cast_add]

-- lem:cds-dir-steiner, correctness of the computation for every state
theorem stateAlg_eq (J : State V) (hJ : IsState G J) (φ : V → ℕ) :
    stateAlg G J φ = optSt G J φ := by
  unfold stateAlg
  split_ifs with h
  · unfold encAlg
    rw [SteinerDir.steinerAlg_eq, ← optSt_eq_optDir G J hJ φ]
  · have hD : J.D = ∅ := not_nonempty_iff_eq_empty.mp h
    rw [optSt_eq_inf_Jb G J hD φ]
    refine Finset.inf_congr rfl fun b _ => ?_
    unfold encAlg
    rw [SteinerDir.steinerAlg_eq]
    exact congrArg (fun x => (φ b : ℕ∞) + x)
      (optSt_eq_optDir G (Jb G J b) (isState_Jb G J b) φ {b} _).symm

open Classical in
/-- `𝒟_X`: the vertex sets of the components of `G[X]`, one for each component. -/
noncomputable def compSets (X : Finset V) : Finset (Finset V) :=
  univ.image fun c : (G.induce (X : Set V)).ConnectedComponent =>
    X.filter fun y => ∃ hy : y ∈ X, (G.induce (X : Set V)).connectedComponentMk ⟨y, hy⟩ = c

/-- `J_X` (eq:cds-JX); for `X = ∅` this is `J₀ = (∅, V, V)`. -/
noncomputable def JX (X : Finset V) : State V :=
  ⟨compSets G X, univ \ X, univ \ closedNbhd G X⟩

theorem mem_compSets_iff (X C : Finset V) : C ∈ compSets G X ↔
    ∃ c : (G.induce (X : Set V)).ConnectedComponent,
      ∀ y, y ∈ C ↔ ∃ hy : y ∈ X, (G.induce (X : Set V)).connectedComponentMk ⟨y, hy⟩ = c := by
  simp only [compSets, mem_image, mem_univ, true_and]
  constructor
  · rintro ⟨c, rfl⟩
    exact ⟨c, fun y => by simp only [mem_filter]; exact ⟨fun h => h.2, fun h => ⟨h.1, h⟩⟩⟩
  · rintro ⟨c, hc⟩
    refine ⟨c, ?_⟩
    ext y
    simp only [mem_filter, hc]
    exact ⟨fun h => h.2, fun h => ⟨h.1, h⟩⟩

-- J_X is a state, and its solutions
theorem JX_empty : JX G ∅ = ⟨∅, univ, univ⟩ := by
  have h1 : compSets G ∅ = ∅ := by
    ext C
    simp only [notMem_empty, iff_false]
    intro hC
    obtain ⟨c, -⟩ := (mem_compSets_iff G ∅ C).mp hC
    exact SimpleGraph.ConnectedComponent.ind (β := fun _ => False)
      (fun v => absurd v.2 (by simp)) c
  have h2 : closedNbhd G ∅ = ∅ := by simp [closedNbhd]
  simp only [JX, h1, h2, sdiff_empty]

theorem VD_JX (X : Finset V) : (JX G X).VD = X := by
  classical
  ext y
  simp only [State.VD, JX, mem_biUnion, id]
  constructor
  · rintro ⟨C, hC, hy⟩
    obtain ⟨c, hc⟩ := (mem_compSets_iff G X C).mp hC
    exact ((hc y).mp hy).1
  · intro hy
    let c := (G.induce (X : Set V)).connectedComponentMk ⟨y, hy⟩
    refine ⟨X.filter (fun z => ∃ hz : z ∈ X,
      (G.induce (X : Set V)).connectedComponentMk ⟨z, hz⟩ = c),
      (mem_compSets_iff G X _).mpr ⟨c, fun z => ?_⟩, ?_⟩
    · rw [mem_filter]; exact ⟨fun h => h.2, fun h => ⟨h.1, h⟩⟩
    · rw [mem_filter]; exact ⟨hy, hy, rfl⟩

theorem isState_JX (X : Finset V) : IsState G (JX G X) := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro C hC
    obtain ⟨c, hc⟩ := (mem_compSets_iff G X C).mp hC
    revert hc
    refine SimpleGraph.ConnectedComponent.ind (fun v => ?_) c
    intro hc
    have hvC : v.1 ∈ C := (hc v.1).mpr ⟨v.2, rfl⟩
    -- every vertex reachable from `v` in `G[X]` lies in `C` and is reachable from `v` in `G[C]`
    have key : ∀ z : (X : Set V), Relation.ReflTransGen (G.induce (X : Set V)).Adj v z →
        ∃ hz : z.1 ∈ C, (G.induce (C : Set V)).Reachable ⟨v.1, hvC⟩ ⟨z.1, hz⟩ := by
      intro z hz
      induction hz with
      | refl => exact ⟨hvC, SimpleGraph.Reachable.refl _⟩
      | @tail a b hva hab ih =>
        obtain ⟨haC, hr⟩ := ih
        have hvb : (G.induce (X : Set V)).Reachable v b :=
          (SimpleGraph.reachable_iff_reflTransGen _ _).mpr (hva.tail hab)
        have hbC : b.1 ∈ C := (hc b.1).mpr ⟨b.2,
          (SimpleGraph.ConnectedComponent.eq.mpr hvb).symm⟩
        exact ⟨hbC, induce_reach_step G (s := (C : Set V)) hvC haC hbC hr hab⟩
    have hall : ∀ z (hz : z ∈ (C : Set V)), (G.induce (C : Set V)).Reachable ⟨v.1, hvC⟩ ⟨z, hz⟩ := by
      intro z hz
      obtain ⟨hzX, hzc⟩ := (hc z).mp hz
      have hvz : (G.induce (X : Set V)).Reachable v ⟨z, hzX⟩ :=
        SimpleGraph.ConnectedComponent.eq.mp hzc.symm
      obtain ⟨_, hr⟩ := key ⟨z, hzX⟩ ((SimpleGraph.reachable_iff_reflTransGen _ _).mp hvz)
      exact hr
    rw [SimpleGraph.connected_iff]
    exact ⟨fun u w => (hall u.1 u.2).symm.trans (hall w.1 w.2), ⟨⟨v.1, hvC⟩⟩⟩
  · intro C hC C' hC' hne
    obtain ⟨c, hc⟩ := (mem_compSets_iff G X C).mp hC
    obtain ⟨c', hc'⟩ := (mem_compSets_iff G X C').mp hC'
    have hcc : c ≠ c' := by
      rintro rfl
      exact hne (by ext y; rw [hc, hc'])
    refine ⟨?_, ?_⟩
    · rw [disjoint_left]
      intro y hy hy'
      obtain ⟨hyX, h1⟩ := (hc y).mp hy
      obtain ⟨_, h2⟩ := (hc' y).mp hy'
      exact hcc (h1.symm.trans h2)
    · intro a ha b hb hab
      obtain ⟨haX, h1⟩ := (hc a).mp ha
      obtain ⟨hbX, h2⟩ := (hc' b).mp hb
      have : (G.induce (X : Set V)).Reachable ⟨a, haX⟩ ⟨b, hbX⟩ :=
        SimpleGraph.Adj.reachable (G := G.induce (X : Set V)) (u := ⟨a, haX⟩) (v := ⟨b, hbX⟩) hab
      exact hcc (h1.symm.trans ((SimpleGraph.ConnectedComponent.eq.mpr this).trans h2))
  · show Disjoint (univ \ X) (JX G X).VD
    rw [VD_JX]
    exact sdiff_disjoint
  · show Disjoint (univ \ closedNbhd G X) (closedNbhd G (JX G X).VD)
    rw [VD_JX]
    exact sdiff_disjoint

theorem isSol_JX_iff (X Y : Finset V) :
    IsSol G (JX G X) Y ↔ Disjoint X Y ∧ IsCDS G (X ∪ Y) := by
  unfold IsSol IsCDS
  rw [VD_JX]
  show (Y ⊆ univ \ X ∧ univ \ closedNbhd G X ⊆ closedNbhd G Y ∧
      (G.induce ((X ∪ Y : Finset V) : Set V)).Connected) ↔ _
  have h1 : Y ⊆ univ \ X ↔ Disjoint X Y := by
    rw [subset_sdiff]
    simp [disjoint_comm]
  have h2 : univ \ closedNbhd G X ⊆ closedNbhd G Y ↔
      ∀ v, v ∈ X ∪ Y ∨ ∃ u ∈ X ∪ Y, G.Adj v u := by
    constructor
    · intro h v
      by_cases hv : v ∈ closedNbhd G X
      · rw [mem_closedNbhd] at hv
        rcases hv with hv | ⟨x, hx, hxv⟩
        · exact Or.inl (mem_union_left _ hv)
        · exact Or.inr ⟨x, mem_union_left _ hx, hxv.symm⟩
      · have := h (mem_sdiff.mpr ⟨mem_univ v, hv⟩)
        rw [mem_closedNbhd] at this
        rcases this with hv | ⟨y, hy, hyv⟩
        · exact Or.inl (mem_union_right _ hv)
        · exact Or.inr ⟨y, mem_union_right _ hy, hyv.symm⟩
    · intro h v hv
      rw [mem_sdiff, mem_closedNbhd] at hv
      rw [mem_closedNbhd]
      rcases h v with hv' | ⟨u, hu, huv⟩
      · rcases mem_union.mp hv' with h' | h'
        · exact absurd (Or.inl h') hv.2
        · exact Or.inl h'
      · rcases mem_union.mp hu with h' | h'
        · exact absurd (Or.inr ⟨u, h', huv.symm⟩) hv.2
        · exact Or.inr ⟨u, h', huv.symm⟩
  rw [h1, h2]
  exact ⟨fun ⟨a, b, c⟩ => ⟨a, c, b⟩, fun ⟨a, c, b⟩ => ⟨a, b, c⟩⟩

/-- `𝒜_St` (def:cds-ast): accept iff `OPT(J_X) ≤ k − |X|`, where `k − |X|` is an integer
(def:fw-iss). Written as `OPT(J_X) + |X| ≤ k` in `ℕ∞`, so inputs with `k < |X|` are rejected. -/
def aSt (X : Finset V) (k : ℕ) : Prop :=
  stateAlg G (JX G X) (fun _ => 1) + (X.card : ℕ∞) ≤ (k : ℕ∞)

-- cor:cds-steiner, correctness: 𝒜_St solves Φ_CDS-Extension (def:fw-iss)
theorem aSt_iff_ext (X : Finset V) (k : ℕ) :
    aSt G X k ↔ ∃ Y : Finset V, Disjoint X Y ∧ X.card + Y.card ≤ k ∧ IsCDS G (X ∪ Y) := by
  unfold aSt
  rw [stateAlg_eq G (JX G X) (isState_JX G X)]
  constructor
  · intro h
    have hne : optSt G (JX G X) (fun _ => 1) ≠ ⊤ := by
      intro htop
      rw [htop, top_add, top_le_iff] at h
      exact ENat.natCast_ne_top _ h
    obtain ⟨Y, hY, heq⟩ := optSt_attained G _ _ hne
    rw [heq] at h
    rw [isSol_JX_iff] at hY
    refine ⟨Y, hY.1, ?_, hY.2⟩
    have h2 : (Y.card : ℕ∞) + X.card ≤ k := by simpa using h
    have h3 : Y.card + X.card ≤ k := by exact_mod_cast h2
    omega
  · rintro ⟨Y, hXY, hle, hcds⟩
    have h1 : optSt G (JX G X) (fun _ => 1) ≤ (Y.card : ℕ∞) := by
      unfold optSt
      exact sInf_le ⟨Y, (isSol_JX_iff G X Y).mpr ⟨hXY, hcds⟩, by simp⟩
    calc optSt G (JX G X) (fun _ => 1) + (X.card : ℕ∞) ≤ (Y.card : ℕ∞) + X.card :=
          add_le_add h1 le_rfl
      _ ≤ (k : ℕ∞) := by exact_mod_cast (by omega : Y.card + X.card ≤ k)

-- The same for |X| ≤ k, in the form of the third conjunct of `RSCTrials.rscAccept`
theorem aSt_iff_extYes (X : Finset V) (k : ℕ) (hk : X.card ≤ k) :
    aSt G X k ↔ MLS.ExtYes (IsCDS G) X (k - X.card) := by
  rw [aSt_iff_ext]
  unfold MLS.ExtYes
  constructor
  · rintro ⟨Y, h1, h2, h3⟩; exact ⟨Y, h1, by omega, h3⟩
  · rintro ⟨Y, h1, h2, h3⟩; exact ⟨Y, h1, by omega, h3⟩

-- Inputs with k < |X| are rejected (def:fw-iss)
theorem not_aSt_of_lt (X : Finset V) (k : ℕ) (hk : k < X.card) : ¬ aSt G X k := by
  rw [aSt_iff_ext]
  rintro ⟨Y, -, h, -⟩
  omega

-- OPT(J₀) = γc(G); uses `Budget.isCDS_univ`
theorem optSt_J0 (hG : G.Connected) : optSt G (JX G ∅) (fun _ => 1) = (γc G : ℕ∞) := by
  have hsol : ∀ Y, IsSol G (JX G ∅) Y ↔ IsCDS G Y := by
    intro Y
    rw [isSol_JX_iff]
    simp
  have hne : {s | ∃ S, IsCDS G S ∧ S.card = s}.Nonempty :=
    ⟨_, univ, Budget.isCDS_univ G hG, rfl⟩
  obtain ⟨S, hS, hSc⟩ := Nat.sInf_mem hne
  have hleS : optSt G (JX G ∅) (fun _ => 1) ≤ (S.card : ℕ∞) := by
    unfold optSt
    exact sInf_le ⟨S, (hsol S).mpr hS, by simp⟩
  apply le_antisymm
  · rw [show γc G = S.card from hSc.symm]
    exact hleS
  · have hnt : optSt G (JX G ∅) (fun _ => 1) ≠ ⊤ :=
      ne_top_of_le_ne_top (ENat.natCast_ne_top S.card) hleS
    obtain ⟨Y, hY, heq⟩ := optSt_attained G _ _ hnt
    rw [heq]
    have : γc G ≤ Y.card := Nat.sInf_le ⟨Y, (hsol Y).mp hY, rfl⟩
    simpa using this

-- eq:cds-TX, |Tm(J_X)| = |R| + |𝒟| = termCount
theorem terminals_JX (X : Finset V) :
    (JX G X).R.card + (JX G X).D.card = termCount G X := by
  show (univ \ closedNbhd G X).card + (compSets G X).card = _
  unfold termCount comp
  rw [card_univ_sdiff]
  congr 1
  rw [compSets, card_image_of_injective, card_univ, Fintype.card_eq_nat_card]
  intro c c' hcc'
  revert hcc'
  refine SimpleGraph.ConnectedComponent.ind (fun v => ?_) c
  intro hcc'
  have := Finset.ext_iff.mp hcc' v.1
  simp only [mem_filter] at this
  obtain ⟨_, hy, hyc⟩ := this.mp (by simp [v.2])
  exact hyc

end MaxLeafFormal.SteinerCDS