import CubicPathwidth.Alg.Spec2
import CubicPathwidth.Alg.Proofs.C5ReduceRecord
import CubicPathwidth.Alg.Proofs.G1WFBasics
import CubicPathwidth.Alg.Proofs.G2AddEdge
import CubicPathwidth.Alg.Proofs.G3RemoveNode

/-!
# R2: `ReduceRecordMaximal` from `ReduceRecordNoFallback` (Stage 2, task R2)

Statement: `reduceRecordMaximal_of (hR1 : ReduceRecordNoFallback) : ReduceRecordMaximal`.

Strategy. The loop `reduceLoop` is run on `G` with the initial stack of nodes of degree
at most two. The loop invariant `Inv2 G0 G stack L` says: the Stage 1 invariant `C5.Inv`
holds; `OpsRecord G0 L.reverse G` (the recorded operations replay to the current graph);
every node of `G` of degree at most two is on the stack; and degrees in `G` never exceed
those in `G0`. One non-skipped step is `redStep` (`C5.stepG_props` for well-formedness),
and the record is extended at its end (`opsRecord_snoc`). When the flag is `false` the
loop ended with an empty stack, so every node has degree at least `3`.

Stage 1 facts used: `removeNodeSpec_of wfBasics` (G3), `addEdgeSpec` (G2), `C5.step_inv`,
`C5.stepG_props`, `C5.Inv` (C5). No other Stage 2 file is imported.
-/

namespace CubicPathwidth.Alg

open Graph

namespace R2

theorem remSpec : RemoveNodeSpec := removeNodeSpec_of wfBasics

theorem addSpec : AddEdgeSpec := addEdgeSpec

/-- The graph part of one loop step is `redStep`. -/
theorem stepG_eq (G : Graph) (v : Nat) :
    C5.stepG (G.removeNode v) (G.nbrs v) = redStep G v := by
  unfold C5.stepG redStep
  rfl

/-- Nodes and adjacency of `redStep G v` (for every `v`). -/
theorem redStep_facts (G : Graph) (hG : G.WF) (v : Nat) :
    (∀ 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) ∨
      (G.degree v = 2 ∧ G.Adj v x ∧ G.Adj v y ∧ x ≠ y)) := by
  obtain ⟨hR1, hR2, hR3⟩ := remSpec G v hG
  have hnd := hG.nbrs_nodup v
  unfold redStep
  rcases hn : G.nbrs v with _ | ⟨a, _ | ⟨b, _ | ⟨c, l⟩⟩⟩
  · dsimp only
    have h2 : ¬ G.degree v = 2 := by simp [Graph.degree, hn]
    refine ⟨hR2, fun x y => ?_⟩
    rw [hR3 x y]
    constructor
    · exact Or.inl
    · rintro (h | ⟨h2', _⟩)
      · exact h
      · exact absurd h2' h2
  · dsimp only
    have h2 : ¬ G.degree v = 2 := by simp [Graph.degree, hn]
    refine ⟨hR2, fun x y => ?_⟩
    rw [hR3 x y]
    constructor
    · exact Or.inl
    · rintro (h | ⟨h2', _⟩)
      · exact h
      · exact absurd h2' h2
  · dsimp only
    have hne : a ≠ b := by
      intro h
      rw [hn, h] at hnd
      simp at hnd
    have ha : a ∈ G.nbrs v := by rw [hn]; simp
    have hb : b ∈ G.nbrs v := by rw [hn]; simp
    have haN : a ∈ G.nodes := hG.nbrs_sub v a ha
    have hbN : b ∈ G.nodes := hG.nbrs_sub v b hb
    have hav : a ≠ v := by
      intro h
      rw [h] at ha
      exact hG.loopless v ha
    have hbv : b ≠ v := by
      intro h
      rw [h] at hb
      exact hG.loopless v hb
    have hdeg : G.degree v = 2 := by simp [Graph.degree, hn]
    have hx : ∀ x, G.Adj v x ↔ x = a ∨ x = b := by
      intro x
      unfold Graph.Adj
      rw [hn]
      simp
    obtain ⟨hA1, hA2, hA3⟩ := addSpec (G.removeNode v) a b (remSpec G v hG).1 hne
    refine ⟨fun x => ?_, fun x y => ?_⟩
    · rw [hA2 x, hR2 x]
      constructor
      · rintro (h | h | h)
        · exact h
        · rw [h]; exact ⟨haN, hav⟩
        · rw [h]; exact ⟨hbN, hbv⟩
      · exact fun h => Or.inl h
    · rw [hA3 x y, hR3 x y, hdeg, hx x, hx y]
      constructor
      · rintro (h | h | h)
        · exact Or.inl h
        · exact Or.inr ⟨rfl, Or.inl h.1, Or.inr h.2, by rw [h.1, h.2]; exact hne⟩
        · exact Or.inr ⟨rfl, Or.inr h.1, Or.inl h.2, by rw [h.1, h.2]; exact hne.symm⟩
      · rintro (h | ⟨_, hx', hy', hxy⟩)
        · exact Or.inl h
        · rcases hx' with h1 | h1 <;> rcases hy' with h2 | h2
          · exact absurd (h1.trans h2.symm) hxy
          · exact Or.inr (Or.inl ⟨h1, h2⟩)
          · exact Or.inr (Or.inr ⟨h1, h2⟩)
          · exact absurd (h1.trans h2.symm) hxy
  · dsimp only
    have h2 : ¬ G.degree v = 2 := by simp [Graph.degree, hn]
    refine ⟨hR2, fun x y => ?_⟩
    rw [hR3 x y]
    constructor
    · exact Or.inl
    · rintro (h | ⟨h2', _⟩)
      · exact h
      · exact absurd h2' h2

/-- The degree of a node is determined by its adjacency (both lists duplicate-free). -/
theorem deg_eq_of_adj_iff {G H : Graph} (hG : G.WF) (hH : H.WF) (x : Nat)
    (h : ∀ y, G.Adj x y ↔ H.Adj x y) : G.degree x = H.degree x := by
  unfold Graph.degree
  exact ((List.perm_ext_iff_of_nodup (hG.nbrs_nodup x) (hH.nbrs_nodup x)).2
    (fun y => h y)).length_eq

/-- A degree is bounded by the length of any list containing the neighbours. -/
theorem deg_le_of_adj_subset {G : Graph} (hG : G.WF) (x : Nat) (l : List Nat)
    (h : ∀ y, G.Adj x y → y ∈ l) : G.degree x ≤ l.length :=
  (hG.nbrs_nodup x).length_le_of_subset (fun y hy => h y hy)

/-- `redStep` keeps well-formedness. -/
theorem wf_redStep {G : Graph} (hG : G.WF) (v : Nat) : (redStep G v).WF := by
  have hnbN : ∀ x ∈ G.nbrs v, x ∈ (G.removeNode v).nodes := by
    intro x hx
    rw [(remSpec G v hG).2.1 x]
    refine ⟨hG.nbrs_sub v x hx, ?_⟩
    intro h
    rw [h] at hx
    exact hG.loopless v hx
  have h := (C5.stepG_props addSpec (G.removeNode v) (G.nbrs v) (remSpec G v hG).1
    (hG.nbrs_nodup v) hnbN).1
  rwa [stepG_eq] at h

/-- Degrees of `redStep G v` never exceed those of `G` (degree at most two at `v`). -/
theorem redStep_degree_le {G : Graph} (hG : G.WF) (v : Nat) (x : Nat) :
    (redStep G v).degree x ≤ G.degree x := by
  have hW := wf_redStep hG v
  have hF := redStep_facts G hG v
  by_cases h2 : G.degree v = 2
  · obtain ⟨a, b, hab⟩ := List.length_eq_two.1 h2
    have ha : a ∈ G.nbrs v := by rw [hab]; simp
    have hb : b ∈ G.nbrs v := by rw [hab]; simp
    have hne : a ≠ b := by
      intro h
      have := hG.nbrs_nodup v
      rw [hab, h] at this
      simp at this
    have hx : ∀ x, G.Adj v x ↔ x = a ∨ x = b := by
      intro x
      unfold Graph.Adj
      rw [hab]
      simp
    have hva : v ∈ G.nbrs a := hG.symm v a ha
    have hvb : v ∈ G.nbrs b := hG.symm v b hb
    by_cases hxa : x = a
    · rw [hxa]
      refine le_trans (deg_le_of_adj_subset hW a (b :: (G.nbrs a).erase v) ?_) ?_
      · intro y hy
        rcases (hF.2 a y).1 hy with ⟨h1, _, h3⟩ | ⟨_, _, h4, h5⟩
        · exact List.mem_cons_of_mem _ ((List.mem_erase_of_ne h3).2 h1)
        · rcases (hx y).1 h4 with h | h
          · exact absurd h.symm h5
          · rw [h]; simp
      · rw [List.length_cons, List.length_erase_of_mem hva]
        have := List.length_pos_of_mem hva
        unfold Graph.degree
        omega
    by_cases hxb : x = b
    · rw [hxb]
      refine le_trans (deg_le_of_adj_subset hW b (a :: (G.nbrs b).erase v) ?_) ?_
      · intro y hy
        rcases (hF.2 b y).1 hy with ⟨h1, _, h3⟩ | ⟨_, _, h4, h5⟩
        · exact List.mem_cons_of_mem _ ((List.mem_erase_of_ne h3).2 h1)
        · rcases (hx y).1 h4 with h | h
          · rw [h]; simp
          · exact absurd h.symm h5
      · rw [List.length_cons, List.length_erase_of_mem hvb]
        have := List.length_pos_of_mem hvb
        unfold Graph.degree
        omega
    · refine le_trans (deg_le_of_adj_subset hW x (G.nbrs x) ?_) le_rfl
      intro y hy
      rcases (hF.2 x y).1 hy with ⟨h1, _, _⟩ | ⟨_, h4, _, _⟩
      · exact h1
      · rcases (hx x).1 h4 with h | h
        · exact absurd h hxa
        · exact absurd h hxb
  · refine le_trans (deg_le_of_adj_subset hW x (G.nbrs x) ?_) le_rfl
    intro y hy
    rcases (hF.2 x y).1 hy with ⟨h1, _, _⟩ | ⟨h2', _⟩
    · exact h1
    · exact absurd h2' h2

/-- Degrees of non-neighbours of `v` are unchanged by `redStep G v`. -/
theorem redStep_degree_eq {G : Graph} (hG : G.WF) (v x : Nat) (hx : ¬ G.Adj v x)
    (hxv : x ≠ v) : (redStep G v).degree x = G.degree x := by
  refine (deg_eq_of_adj_iff (wf_redStep hG v) hG x ?_)
  intro y
  rw [(redStep_facts G hG v).2 x y]
  constructor
  · rintro (⟨h1, _, _⟩ | ⟨_, h3, _, _⟩)
    · exact h1
    · exact absurd h3 hx
  · intro h
    refine Or.inl ⟨h, hxv, ?_⟩
    intro hyv
    rw [hyv] at h
    exact hx (hG.symm x v h)

/-- `redStep` respects `SameGraph` on well-formed graphs. -/
theorem sameGraph_redStep {G H : Graph} (hG : G.WF) (hH : H.WF) (hGH : SameGraph G H)
    (v : Nat) : SameGraph (redStep G v) (redStep H v) := by
  have hdeg : G.degree v = H.degree v := deg_eq_of_adj_iff hG hH v (fun y => hGH.2 v y)
  have hF := redStep_facts G hG v
  have hF' := redStep_facts H hH v
  unfold SameGraph at hGH ⊢
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [hF.1 x, hF'.1 x, hGH.1 x]
  · rw [hF.2 x y, hF'.2 x y, hdeg, hGH.2 x y, hGH.2 v x, hGH.2 v y]

/-- Appending one reduction at the end of a record (the record ends at `R`). -/
theorem opsRecord_snoc (ops : List Op) : ∀ (F R : Graph) (v : Nat),
    F.WF → R.WF → OpsRecord F ops R → v ∈ R.nodes → R.degree v ≤ 2 →
    OpsRecord F (ops ++ [Op.red v (R.nbrs v)]) (redStep R v) := by
  induction ops with
  | nil =>
    intro F R v hF hR hO hv hd
    have hFR : SameGraph F R := hO
    unfold SameGraph at hFR
    simp only [List.nil_append, OpsRecord]
    refine ⟨(hFR.1 v).2 hv, hR.nbrs_nodup v, hd, fun x => (hFR.2 v x).symm, ?_⟩
    exact sameGraph_redStep hF hR (by unfold SameGraph; exact hFR) v
  | cons o ops ih =>
    intro F R v hF hR hO hv hd
    cases o with
    | red v' nb' =>
      simp only [OpsRecord] at hO
      obtain ⟨h1, h2, h3, h4, h5⟩ := hO
      simp only [List.cons_append, OpsRecord]
      exact ⟨h1, h2, h3, h4, ih (redStep F v') R v (wf_redStep hF v') hR h5 hv hd⟩
    | del w =>
      simp only [OpsRecord] at hO
      obtain ⟨h1, h2⟩ := hO
      simp only [List.cons_append, OpsRecord]
      exact ⟨h1, ih (F.removeNode w) R v ((remSpec F w hF).1) hR h2 hv hd⟩

/-- Invariant of the reduction loop, relative to its start `G0`. -/
def Inv2 (G0 G : Graph) (stack : List Nat) (L : List Op) : Prop :=
  C5.Inv G0 G L ∧ OpsRecord G0 L.reverse G ∧
    (∀ x ∈ G.nodes, G.degree x ≤ 2 → x ∈ stack) ∧
    (∀ x ∈ G.nodes, G.degree x ≤ G0.degree x)

/-- The conclusion of `ReduceRecordMaximal` for the output of the loop. -/
def Final2 (G0 R : Graph) (ops : List Op) : Prop :=
  OpsRecord G0 ops R ∧ (∀ v ∈ R.nodes, 3 ≤ R.degree v) ∧
    (∀ v ∈ R.nodes, R.degree v ≤ G0.degree v)

/-- An empty stack gives the conclusion. -/
theorem final_of_nil (G0 G : Graph) (L : List Op) (hI : Inv2 G0 G [] L) :
    Final2 G0 G L.reverse := by
  obtain ⟨_, hO, hs, hd⟩ := hI
  refine ⟨hO, fun x hx => ?_, fun x hx => hd x hx⟩
  by_contra hc
  have := hs x hx (by omega)
  simp at this

/-- The loop, when its flag is `false`, produces a `Final2` output. -/
theorem loop_props (G0 : Graph) (hG0 : G0.WF) (fuel : Nat) :
    ∀ (G : Graph) (stack : List Nat) (L : List Op),
    Inv2 G0 G stack L → (reduceLoop fuel G stack L).2.2 = false →
    Final2 G0 (reduceLoop fuel G stack L).1 (reduceLoop fuel G stack L).2.1 := by
  induction fuel with
  | zero =>
    intro G stack L hI hf
    cases stack with
    | nil => exact final_of_nil G0 G L hI
    | cons v rest => simp [reduceLoop] at hf
  | succ n ih =>
    intro G stack L hI hf
    obtain ⟨hC, hO, hs, hd⟩ := hI
    have hGW : G.WF := hC.1
    cases stack with
    | nil => exact final_of_nil G0 G L ⟨hC, hO, hs, hd⟩
    | cons v rest =>
      by_cases hc : (!G.mem v || decide (G.degree v > 2)) = true
      · have hred : reduceLoop (n+1) G (v :: rest) L = reduceLoop n G rest L := by
          simp only [reduceLoop, hc, ite_true]
        rw [hred] at hf ⊢
        refine ih G rest L ⟨hC, hO, fun x hx hdx => ?_, hd⟩ hf
        rcases List.mem_cons.1 (hs x hx hdx) with h | h
        · exfalso
          have hm : G.mem v = true := (hGW.mem_iff v).2 (h ▸ hx)
          have hgt : 2 < G.degree v := by
            have := hc
            simp [hm] at this
            omega
          rw [h] at hdx
          omega
        · exact h
      · have hm : G.mem v = true := by
          by_contra h
          have h0 : G.mem v = false := by simpa using h
          apply hc
          simp [h0]
        have hd2 : G.degree v ≤ 2 := by
          by_contra h
          apply hc
          have h' : 2 < G.degree v := by omega
          simp [hm, h']
        have hv : v ∈ G.nodes := (hGW.mem_iff v).1 hm
        have hred : reduceLoop (n+1) G (v :: rest) L =
            reduceLoop n (redStep G v) ((G.nbrs v).reverse ++ rest)
              (Op.red v (G.nbrs v) :: L) := by
          simp only [reduceLoop, hc]
          rfl
        rw [hred] at hf ⊢
        have hI' : Inv2 G0 (redStep G v) ((G.nbrs v).reverse ++ rest)
            (Op.red v (G.nbrs v) :: L) := by
          refine ⟨?_, ?_, ?_, ?_⟩
          · have h := C5.step_inv remSpec addSpec G0 G L v hC hm
            rw [stepG_eq] at h
            exact h
          · rw [List.reverse_cons]
            exact opsRecord_snoc L.reverse G0 G v hG0 hGW hO hv hd2
          · intro x hx hdx
            have hxG := ((redStep_facts G hGW v).1 x).1 hx
            by_cases hxa : G.Adj v x
            · exact List.mem_append_left _ (List.mem_reverse.2 (show x ∈ G.nbrs v from hxa))
            · rw [redStep_degree_eq hGW v x hxa hxG.2] at hdx
              rcases List.mem_cons.1 (hs x hxG.1 hdx) with h | h
              · exact absurd h hxG.2
              · exact List.mem_append_right _ h
          · intro x hx
            have hxG := ((redStep_facts G hGW v).1 x).1 hx
            exact le_trans (redStep_degree_le hGW v x) (hd x hxG.1)
        exact ih (redStep G v) ((G.nbrs v).reverse ++ rest) (Op.red v (G.nbrs v) :: L) hI' hf

end R2

/-- `ReduceRecordMaximal` from the absence of fallbacks of `reduce_record`. -/
theorem reduceRecordMaximal_of (hR1 : ReduceRecordNoFallback) : ReduceRecordMaximal := by
  intro G hG
  have hf : (reduceRecordF G).2.2 = false := hR1 G hG
  have hC : C5.Inv G G [] :=
    ⟨hG, fun _ hx => hx, fun _ _ _ _ h => h,
      fun o ho => absurd ho (List.not_mem_nil), fun _ hx => Or.inl hx⟩
  have hI : R2.Inv2 G G ((G.nodes.filter fun v => G.degree v ≤ 2).reverse) [] := by
    refine ⟨hC, ?_, ?_, fun x _ => le_refl _⟩
    · show SameGraph G G
      unfold SameGraph
      exact ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩
    · intro x hx hd
      simp [List.mem_filter, hx, hd]
  have key := R2.loop_props G hG (3 * G.numNodes + 1) G _ [] hI hf
  exact key

#print axioms CubicPathwidth.Alg.reduceRecordMaximal_of

end CubicPathwidth.Alg