import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.G1WFBasics
import CubicPathwidth.Alg.Proofs.G2AddEdge
import CubicPathwidth.Alg.Proofs.G3RemoveNode

/-!
# D2d: the frame rule for records (`OpsRecordFrame`)

Task D2d of Stage 2 (`Plan2Deletion.lean`). Proves `opsRecordFrame`: a record
on `K` is a record on any disjoint union `M` of `K` and `L`, ending in the disjoint union
of the final graph `K'` and `L`.

Route: induction on `ops`, generalizing `K` and `M`. A `red` step on `K` and on `M` have
the same neighbour set at `v` (since `L` does not see `v`), hence the same length, so the
two `redStep`s have the same nodes and adjacency up to `L`. The Stage 1 specs
`removeNodeSpec`, `addEdgeSpec` (through `removeNodeSpec_of wfBasics`) give the
node/adjacency behaviour of the operations and well-formedness.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace D2d

/-- Stage 1 `RemoveNodeSpec`. -/
theorem rmSpec : RemoveNodeSpec := removeNodeSpec_of wfBasics

/-- Adjacency in a well-formed graph has both endpoints among the nodes. -/
theorem adj_mem {G : Graph} (hG : G.WF) {x y : Nat} (h : G.Adj x y) :
    x ∈ G.nodes ∧ y ∈ G.nodes := by
  obtain ⟨h1, h2, _, _⟩ := wfBasics G hG x y h
  exact ⟨h1, h2⟩

/-- Characterization of one `redStep` (WF input). The neighbour set of `v` enters only
through membership and length, so it is the same for two graphs with the same
neighbour set at `v`. -/
theorem redStep_facts (G : Graph) (v : Nat) (hG : G.WF) :
    (redStep G v).WF ∧
    (∀ x, x ∈ (redStep G v).nodes ↔ x ∈ G.nodes ∧ x ≠ v) ∧
    (∀ x y, (redStep G v).Adj x y ↔
      (G.Adj x y ∧ x ≠ v ∧ y ≠ v) ∨
        (x ∈ G.nbrs v ∧ y ∈ G.nbrs v ∧ x ≠ y ∧ (G.nbrs v).length = 2)) := by
  have hR := rmSpec G v hG
  have hnd := hG.nbrs_nodup v
  unfold redStep
  split
  · rename_i a b heq
    have hab : a ≠ b := by
      have := hnd
      rw [heq] at this
      exact fun e => (List.nodup_cons.1 this).1 (by simp [e])
    have ha : a ∈ G.nbrs v := by rw [heq]; simp
    have hb : b ∈ G.nbrs v := by rw [heq]; simp
    have hav : a ≠ v := fun h => hG.loopless v (h ▸ ha)
    have hbv : b ≠ v := fun h => hG.loopless v (h ▸ hb)
    have ha' : a ∈ (G.removeNode v).nodes := (hR.2.1 a).2 ⟨hG.nbrs_sub v a ha, hav⟩
    have hb' : b ∈ (G.removeNode v).nodes := (hR.2.1 b).2 ⟨hG.nbrs_sub v b hb, hbv⟩
    have hae := addEdgeSpec (G.removeNode v) a b hR.1 hab
    refine ⟨hae.1, ?_, ?_⟩
    · intro x
      rw [hae.2.1 x, hR.2.1 x]
      constructor
      · rintro (h | h | h)
        · exact h
        · exact ⟨h ▸ ha' |> fun h' => ((hR.2.1 x).1 h').1, h ▸ hav⟩
        · exact ⟨h ▸ hb' |> fun h' => ((hR.2.1 x).1 h').1, h ▸ hbv⟩
      · exact fun h => Or.inl h
    · intro x y
      rw [hae.2.2 x y, hR.2.2 x y, heq]
      by_cases hxa : x = a <;> by_cases hxb : x = b <;>
        by_cases hya : y = a <;> by_cases hyb : y = b <;>
        simp_all
  · rename_i hne
    refine ⟨hR.1, hR.2.1, ?_⟩
    intro x y
    rw [hR.2.2 x y]
    constructor
    · intro h
      exact Or.inl h
    · rintro (h | ⟨_, _, _, hl⟩)
      · exact h
      · exfalso
        obtain ⟨a, b, hab⟩ := List.length_eq_two.mp hl
        exact hne a b hab

/-- The `L`-part of an adjacency is away from `v` when `v` is a node of `K`. -/
theorem L_adj_ne {K L : Graph} (hL : L.WF) (hdis : ∀ x, x ∈ K.nodes → x ∉ L.nodes)
    {v x y : Nat} (hv : v ∈ K.nodes) (h : L.Adj x y) : x ≠ v ∧ y ≠ v := by
  obtain ⟨hx, hy⟩ := adj_mem hL h
  exact ⟨fun e => hdis v hv (e ▸ hx), fun e => hdis v hv (e ▸ hy)⟩

/-- Main induction. -/
theorem frame_main : OpsRecordFrame := by
  intro K K' L M M' ops
  induction ops generalizing K M with
  | nil =>
    intro hK hL hM hdis hMn hMa hK'n hK'a hrec
    have hr : SameGraph K K' := hrec
    refine ⟨fun v => ?_, fun u v => ?_⟩
    · rw [hMn v, hK'n v, hr.1 v]
    · exact (Iff.trans (hMa u v) (or_congr (hr.2 u v) Iff.rfl)).trans (Iff.symm (hK'a u v))
  | cons o ops ih =>
    intro hK hL hM hdis hMn hMa hK'n hK'a hrec
    cases o with
    | red v nb =>
      obtain ⟨hvK, hnb, hlen, hnbA, hrec1⟩ := hrec
      have hvM : v ∈ M.nodes := (hMn v).2 (Or.inl hvK)
      have hvL : v ∉ L.nodes := hdis v hvK
      -- `L` does not see `v`, so `M` and `K` have the same neighbours at `v`
      have hMAdj : ∀ x, M.Adj v x ↔ K.Adj v x := by
        intro x
        constructor
        · intro h
          rcases (hMa v x).1 h with h1 | h1
          · exact h1
          · exact absurd (adj_mem hL h1).1 hvL
        · intro h
          exact (hMa v x).2 (Or.inl h)
      have hMvA : ∀ x, x ∈ M.nbrs v ↔ x ∈ K.nbrs v := fun x => hMAdj x
      have hlenEq : (M.nbrs v).length = (K.nbrs v).length := by
        have hp : (M.nbrs v).Perm (K.nbrs v) :=
          (List.perm_ext_iff_of_nodup (hM.nbrs_nodup v) (hK.nbrs_nodup v)).2 hMvA
        exact hp.length_eq
      have hLx : ∀ x y, L.Adj x y → x ≠ v ∧ y ≠ v := fun x y h => L_adj_ne hL hdis hvK h
      have hMv1 : ∀ x, x ∈ nb ↔ M.Adj v x := fun x => (hnbA x).trans (hMAdj x).symm
      refine ⟨hvM, hnb, hlen, hMv1, ?_⟩
      have hK1 := redStep_facts K v hK
      have hM1 := redStep_facts M v hM
      refine ih (redStep K v) (redStep M v) hK1.1 hL hM1.1 ?_ ?_ ?_ hK'n hK'a hrec1
      · intro x hx
        exact hdis x ((hK1.2.1 x).1 hx).1
      · intro x
        rw [hM1.2.1 x, hK1.2.1 x, hMn x]
        constructor
        · rintro ⟨h | h, hxv⟩
          · exact Or.inl ⟨h, hxv⟩
          · exact Or.inr h
        · rintro (⟨h, hxv⟩ | h)
          · exact ⟨Or.inl h, hxv⟩
          · exact ⟨Or.inr h, fun e => hvL (e ▸ h)⟩
      · intro x y
        rw [hM1.2.2 x y, hK1.2.2 x y, hMa x y, hlenEq]
        have hMK1 : x ∈ M.nbrs v ↔ x ∈ K.nbrs v := hMvA x
        have hMK2 : y ∈ M.nbrs v ↔ y ∈ K.nbrs v := hMvA y
        rw [hMK1, hMK2]
        have hl := hLx x y
        constructor
        · rintro (⟨h | h, hx, hy⟩ | hP)
          · exact Or.inl (Or.inl ⟨h, hx, hy⟩)
          · exact Or.inr h
          · exact Or.inl (Or.inr hP)
        · rintro ((⟨h, hx, hy⟩ | hP) | h)
          · exact Or.inl ⟨Or.inl h, hx, hy⟩
          · exact Or.inr hP
          · exact Or.inl ⟨Or.inr h, (hl h).1, (hl h).2⟩
    | del w =>
      obtain ⟨hwK, hrec1⟩ := hrec
      refine ⟨(hMn w).2 (Or.inl hwK), ?_⟩
      have rK := rmSpec K w hK
      have rM := rmSpec M w hM
      have hwL : w ∉ L.nodes := hdis w hwK
      refine ih (K.removeNode w) (M.removeNode w) rK.1 hL rM.1 ?_ ?_ ?_ hK'n hK'a hrec1
      · intro x hx
        exact hdis x (((rK.2.1 x).1 hx).1)
      · intro x
        rw [rM.2.1 x, rK.2.1 x, hMn x]
        constructor
        · rintro ⟨h | h, hxw⟩
          · exact Or.inl ⟨h, hxw⟩
          · exact Or.inr h
        · rintro (⟨h, hxw⟩ | h)
          · exact ⟨Or.inl h, hxw⟩
          · exact ⟨Or.inr h, fun e => hwL (e ▸ h)⟩
      · intro x y
        rw [rM.2.2 x y, rK.2.2 x y, hMa x y]
        have hl : ∀ x y, L.Adj x y → x ≠ w ∧ y ≠ w :=
          fun x y h => L_adj_ne hL hdis hwK h
        constructor
        · rintro ⟨h | h, hx, hy⟩
          · exact Or.inl ⟨h, hx, hy⟩
          · exact Or.inr h
        · rintro (⟨h, hx, hy⟩ | h)
          · exact ⟨Or.inl h, hx, hy⟩
          · exact ⟨Or.inr h, (hl x y h).1, (hl x y h).2⟩

end D2d

/-- Frame rule for records (`OpsRecordFrame`, task D2d). -/
theorem opsRecordFrame : OpsRecordFrame := D2d.frame_main

#print axioms CubicPathwidth.Alg.opsRecordFrame

end CubicPathwidth.Alg