import CubicPathwidth.T4.ProcessDefs

/-!
# Locality of the process (helper for `DeletionX`)

Facts about the evolving torso graph `tgraph`, derived from `TorsoDynamics`:

* `reach_adj_comp`: along a `Reach`, torso edges stay inside one torso component of the
  starting state;
* `reach_preserve`: a closed set of high-degree core vertices that is not deleted is
  untouched (same core membership, same torso neighbourhoods);
* `tcomp_preserve`: such a torso component stays a torso component, with the same `cmin`;
* `psi_delete`: the exact change of `ψ` under the deletion of one core vertex.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 SectionDecomposition

namespace DelX

variable {n : ℕ}

/-! ## Degrees as cardinalities of neighbourhoods -/

open Classical in
/-- The torso neighbourhood of `v`. -/
def nbrs (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (v : Fin n) : Finset (Fin n) :=
  Finset.univ.filter (fun u => (tgraph G F B).Adj v u)

theorem mem_nbrs {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} {v u : Fin n} :
    u ∈ nbrs G F B v ↔ (tgraph G F B).Adj v u := by
  classical
  simp [nbrs]

theorem tdeg_eq_card_nbrs (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (v : Fin n) :
    tdeg G F B v = (nbrs G F B v).card := by
  classical
  unfold tdeg
  rw [← SimpleGraph.card_neighborFinset_eq_degree]
  congr 1
  ext u
  simp [mem_nbrs]

theorem tdeg_congr {G : SimpleGraph (Fin n)} {F B F' B' : Finset (Fin n)} {x : Fin n}
    (h : ∀ y, (tgraph G F B).Adj x y ↔ (tgraph G F' B').Adj x y) :
    tdeg G F B x = tdeg G F' B' x := by
  rw [tdeg_eq_card_nbrs, tdeg_eq_card_nbrs]
  congr 1
  ext u
  simp only [mem_nbrs]
  exact h u

theorem tgraph_adj_mem {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} {x y : Fin n}
    (h : (tgraph G F B).Adj x y) : x ∈ B ∧ y ∈ B := ⟨h.2.1, h.2.2.1⟩

theorem mem_tcomps {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)}
    (hC : C ∈ tcomps G F B) : ∃ v ∈ B, C = component (tgraph G F B) B v := by
  classical
  unfold tcomps components at hC
  obtain ⟨v, hv, h⟩ := Finset.mem_image.mp hC
  exact ⟨v, hv, h.symm⟩

theorem component_mem_tcomps {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} {u : Fin n}
    (hu : u ∈ B) : component (tgraph G F B) B u ∈ tcomps G F B :=
  mem_components_of_mem (tgraph G F B) hu

/-! ## Accessors for `TorsoDynamics` -/

theorem td_del (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B : Finset (Fin n)} (hg : Good G F B) {w : Fin n} (hw : w ∈ B) (x y : Fin n) :
    (tgraph G (F.erase w) (B.erase w)).Adj x y ↔
      (tgraph G F B).Adj x y ∧ x ≠ w ∧ y ≠ w :=
  (hdyn n G F B hg).1 w hw x y

theorem td_red (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B : Finset (Fin n)} (hg : Good G F B) {v : Fin n} (hv : v ∈ B)
    (hd : tdeg G F B v ≤ 2) (x y : Fin n) :
    (tgraph G F (B.erase v)).Adj x y ↔
      x ≠ v ∧ y ≠ v ∧ ((tgraph G F B).Adj x y ∨
        (x ≠ y ∧ (tgraph G F B).Adj x v ∧ (tgraph G F B).Adj y v)) :=
  (hdyn n G F B hg).2.1 v hv hd x y

theorem td_maxred (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B : Finset (Fin n)} (hg : Good G F B) :
    ∃ B' ⊆ B, Reach G (F, B) (F, B') ∧ (∀ v ∈ B', 3 ≤ tdeg G F B' v) ∧
      ∀ v ∈ B', tdeg G F B' v ≤ tdeg G F B v :=
  (hdyn n G F B hg).2.2

/-! ## Torso edges stay inside one torso component -/

theorem component_eq_of_mem' {G : SimpleGraph (Fin n)} {U : Finset (Fin n)} {x y : Fin n}
    (hy : y ∈ component G U x) : component G U y = component G U x :=
  component_eq_of_mem G hy

theorem reach_adj_comp (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)}
    (hg : Good G F B) :
    ∀ t : Finset (Fin n) × Finset (Fin n), Reach G (F, B) t →
      ∀ x y, (tgraph G t.1 t.2).Adj x y → y ∈ component (tgraph G F B) B x := by
  intro t ht
  induction ht with
  | refl =>
    intro x y h
    exact component_closed (tgraph G F B) B x x (mem_component_self _ h.2.1) y h.2.2.1 h
  | tail hab hbc ih =>
    rename_i s' t'
    obtain ⟨F1, B1⟩ := s'
    have hg1 : Good G F1 B1 := hg.reach hab
    have hsub : B1 ⊆ B := (Reach.subset hab).2
    cases hbc with
    | @reduce _ _ v hv hd =>
      intro x y hxy
      obtain ⟨hxv, hyv, h | ⟨hne, hxv', hyv'⟩⟩ := (td_red hdyn hg1 hv hd x y).1 hxy
      · exact ih x y h
      · have h1 : v ∈ component (tgraph G F B) B x := ih x _ hxv'
        have h2 : v ∈ component (tgraph G F B) B y := ih y _ hyv'
        have e1 := component_eq_of_mem (tgraph G F B) h1
        have e2 := component_eq_of_mem (tgraph G F B) h2
        have hyB : y ∈ B := hsub (tgraph_adj_mem hyv').1
        have : y ∈ component (tgraph G F B) B y := mem_component_self _ hyB
        rw [← e2, e1] at this
        exact this
    | delete hw =>
      intro x y hxy
      exact ih x y ((td_del hdyn hg1 hw x y).1 hxy).1

/-! ## Untouched closed sets -/

theorem reach_preserve (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B : Finset (Fin n)} (hg : Good G F B) (S : Finset (Fin n))
    (hcl : ∀ x ∈ S, ∀ y, (tgraph G F B).Adj x y → y ∈ S)
    (hSB : S ⊆ B) (hdeg : ∀ x ∈ S, 3 ≤ tdeg G F B x) :
    ∀ t : Finset (Fin n) × Finset (Fin n), Reach G (F, B) t → S ⊆ t.1 →
      S ⊆ t.2 ∧ ∀ x ∈ S, ∀ y, (tgraph G t.1 t.2).Adj x y ↔ (tgraph G F B).Adj x y := by
  intro t ht
  induction ht with
  | refl => intro _; exact ⟨hSB, fun _ _ _ => Iff.rfl⟩
  | tail hab hbc ih =>
    rename_i s' t'
    obtain ⟨F1, B1⟩ := s'
    have hg1 : Good G F1 B1 := hg.reach hab
    cases hbc with
    | @reduce _ _ v hv hd =>
      intro hSF
      have hSF1 : S ⊆ F1 := hSF
      obtain ⟨hSB1, hadj1⟩ := ih hSF1
      have hvS : v ∉ S := by
        intro hvS
        have h3 := hdeg v hvS
        have h4 : tdeg G F1 B1 v = tdeg G F B v :=
          tdeg_congr (fun y => hadj1 v hvS y)
        omega
      refine ⟨fun x hx => Finset.mem_erase.mpr ⟨fun h => hvS (h ▸ hx), hSB1 hx⟩, ?_⟩
      intro x hx y
      rw [td_red hdyn hg1 hv hd x y]
      constructor
      · rintro ⟨hxv, hyv, h | ⟨hne, hxv', hyv'⟩⟩
        · exact (hadj1 x hx y).1 h
        · exact absurd (hcl x hx v ((hadj1 x hx v).1 hxv')) hvS
      · intro h
        exact ⟨fun h' => hvS (h' ▸ hx), fun h' => hvS (h' ▸ hcl x hx y h),
          Or.inl ((hadj1 x hx y).2 h)⟩
    | @delete _ _ w hw =>
      intro hSF
      have hSF' : S ⊆ F1.erase w := hSF
      have hSF1 : S ⊆ F1 := hSF'.trans (Finset.erase_subset _ _)
      obtain ⟨hSB1, hadj1⟩ := ih hSF1
      have hwS : ∀ x ∈ S, x ≠ w := fun x hx h => by
        have := hSF' hx
        rw [h] at this
        simp at this
      refine ⟨fun x hx => Finset.mem_erase.mpr ⟨hwS x hx, hSB1 hx⟩, ?_⟩
      intro x hx y
      rw [td_del hdyn hg1 hw x y]
      constructor
      · rintro ⟨h, _, _⟩
        exact (hadj1 x hx y).1 h
      · intro h
        exact ⟨(hadj1 x hx y).2 h, hwS x hx, hwS y (hcl x hx y h)⟩

/-- A torso component whose vertices are not deleted stays a torso component, with the
same minimum torso degree. -/
theorem tcomp_preserve (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B F' B' : Finset (Fin n)} (hg : Good G F B) (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v)
    (h : Reach G (F, B) (F', B')) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    (hCF : C ⊆ F') : C ∈ tcomps G F' B' ∧ cmin G F' B' C = cmin G F B C := by
  obtain ⟨hCB, hcl, hconn⟩ := mem_components (tgraph G F B) hC
  have hcl' : ∀ x ∈ C, ∀ y, (tgraph G F B).Adj x y → y ∈ C :=
    fun x hx y hxy => hcl x hx y (tgraph_adj_mem hxy).2 hxy
  obtain ⟨hCB', hadj⟩ := reach_preserve hdyn hg C hcl' hCB
    (fun x hx => hmin x (hCB hx)) (F', B') h hCF
  have hcl2 : ClosedIn (tgraph G F' B') B' C :=
    fun x hx y _ hxy => hcl' x hx y ((hadj x hx y).1 hxy)
  have hconn2 : SectionConnected (tgraph G F' B') C :=
    ⟨hconn.1, fun S hS hSc hSne => hconn.2 S hS
      (fun a ha b hb hab => hSc a ha b hb ((hadj a (hS ha) b).2 hab)) hSne⟩
  obtain ⟨v, hv⟩ := hconn.1
  have heq : component (tgraph G F' B') B' v = C :=
    component_eq_of_connected (tgraph G F' B') hCB' hcl2 hconn2 hv
  refine ⟨?_, ?_⟩
  · rw [← heq]
    exact component_mem_tcomps (hCB' hv)
  · unfold cmin
    simp only [hconn.1, dite_true]
    apply Finset.inf'_congr hconn.1 rfl
    intro x hx
    exact tdeg_congr (fun y => hadj x hx y)

/-- The new torso component of a surviving vertex `u` of `C` lies inside `C`. -/
theorem reach_component_subset (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)}
    {F B F' B' : Finset (Fin n)} (hg : Good G F B) (h : Reach G (F, B) (F', B'))
    {C : Finset (Fin n)} (hC : C ∈ tcomps G F B) {u : Fin n} (hu : u ∈ C) (hu' : u ∈ B') :
    component (tgraph G F' B') B' u ⊆ C := by
  obtain ⟨v, hvB, rfl⟩ := mem_tcomps hC
  have hcl : ClosedIn (tgraph G F' B') B' (component (tgraph G F B) B v ∩ B') := by
    intro x hx y hy hxy
    refine Finset.mem_inter.mpr ⟨?_, hy⟩
    have h1 := reach_adj_comp hdyn hg (F', B') h x y hxy
    rw [component_eq_of_mem (tgraph G F B) (Finset.mem_inter.mp hx).1] at h1
    exact h1
  have := component_min (tgraph G F' B') Finset.inter_subset_right hcl
    (Finset.mem_inter.mpr ⟨hu, hu'⟩)
  exact this.trans Finset.inter_subset_left

/-! ## Deleting one vertex -/

theorem nbrs_subset_erase {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} {w : Fin n} :
    nbrs G F B w ⊆ B.erase w := by
  intro u hu
  have h := mem_nbrs.mp hu
  exact Finset.mem_erase.mpr ⟨h.1.symm, h.2.2.1⟩

theorem tdeg_delete (hdyn : TorsoDynamics) {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)}
    (hg : Good G F B) {w : Fin n} (hw : w ∈ B) {v : Fin n} (hv : v ≠ w) :
    tdeg G (F.erase w) (B.erase w) v + (if v ∈ nbrs G F B w then 1 else 0) =
      tdeg G F B v := by
  classical
  have hset : nbrs G (F.erase w) (B.erase w) v = (nbrs G F B v).erase w := by
    ext u
    simp only [mem_nbrs, Finset.mem_erase, td_del hdyn hg hw]
    constructor
    · rintro ⟨h, _, hu⟩; exact ⟨hu, h⟩
    · rintro ⟨hu, h⟩; exact ⟨h, hv, hu⟩
  rw [tdeg_eq_card_nbrs, tdeg_eq_card_nbrs, hset]
  by_cases hvn : v ∈ nbrs G F B w
  · have hwn : w ∈ nbrs G F B v := by
      rw [mem_nbrs]; exact ((mem_nbrs.mp hvn)).symm
    simp only [hvn, ite_true]
    rw [Finset.card_erase_of_mem hwn]
    have := Finset.card_pos.mpr ⟨w, hwn⟩
    omega
  · have hwn : w ∉ nbrs G F B v := by
      intro h; exact hvn (by rw [mem_nbrs]; exact (mem_nbrs.mp h).symm)
    simp only [hvn, ite_false]
    rw [Finset.erase_eq_of_notMem hwn]
    simp

theorem psi_delete (hdyn : TorsoDynamics) (b : ℕ → ℝ) {G : SimpleGraph (Fin n)}
    {F B : Finset (Fin n)} (hg : Good G F B) {w : Fin n} (hw : w ∈ B) :
    psi b G (F.erase w) (B.erase w) = psi b G F B - b (tdeg G F B w) -
      ∑ v ∈ nbrs G F B w, (b (tdeg G F B v) - b (tdeg G F B v - 1)) := by
  classical
  unfold psi
  rw [← Finset.add_sum_erase B _ hw]
  have h1 : ∑ v ∈ nbrs G F B w, (b (tdeg G F B v) - b (tdeg G (F.erase w) (B.erase w) v)) =
      ∑ v ∈ B.erase w, (b (tdeg G F B v) - b (tdeg G (F.erase w) (B.erase w) v)) := by
    apply Finset.sum_subset nbrs_subset_erase
    intro v hv hvn
    have hvw := (Finset.mem_erase.mp hv).1
    have := tdeg_delete hdyn hg hw hvw
    simp only [hvn, ite_false, add_zero] at this
    rw [this]; ring
  have h2 : ∑ v ∈ nbrs G F B w, (b (tdeg G F B v) - b (tdeg G (F.erase w) (B.erase w) v)) =
      ∑ v ∈ nbrs G F B w, (b (tdeg G F B v) - b (tdeg G F B v - 1)) := by
    apply Finset.sum_congr rfl
    intro v hv
    have hvw : v ≠ w := (Finset.mem_erase.mp (nbrs_subset_erase hv)).1
    have := tdeg_delete hdyn hg hw hvw
    simp only [hv, ite_true] at this
    have h3 : tdeg G (F.erase w) (B.erase w) v = tdeg G F B v - 1 := by omega
    rw [h3]
  rw [← h2, h1, Finset.sum_sub_distrib]
  ring

end DelX

end T4
end CubicPathwidth