CubicPathwidth.Alg.Proofs2.T4LoopInit

Source file CubicPathwidth/Alg/Proofs2/T4LoopInit.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets

/-!
Task D2a1: `t4LoopInvInit_of`, the invariant `T4LoopInv` at the start of the work loop.

With `G0 := nonIsolated G`, `H := (reduceRecordF G0.copy).1`, `ops := (reduceRecordF G0.copy).2.1`
and stack `(componentGraphs H).reverse`, no final entries:

* `T4Inv`: Stage 1 `t4InitInv` gives it for `componentGraphs H`; reversing the list keeps it
  (the pairwise-disjointness relation is symmetric).
* `ThinOK []` and the thin clause are vacuous.
* `OpsRecord G0 ops (unionAll stack)`: `ReduceRecordMaximal` gives `OpsRecord G0.copy ops H`,
  `OpsRecordCongr` moves the start to `G0` (`SameGraph G0.copy G0`), and `H` is `SameGraph`
  to `unionAll (componentGraphs H).reverse` (components partition the nodes and are
  neighbour-closed). The right end moves along `SameGraph` by induction on `ops`.
* `T4Piece` of each component `H.induced c`: well formed (`InducedSpec`), nonempty, connected
  (`ComponentsConnected` in `H`, lifted to `H.induced c` since `c` is neighbour-closed), and of
  minimum degree `3` (its degrees equal the degrees in `H`, which are `≥ 3` by
  `ReduceRecordMaximal`).

Only Stage 1 contracts (`Targets`, `T2InitInv` helpers) and the hypotheses of the statement.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace T4LoopInit

/-- `SameGraph` is transitive. -/
theorem sameGraph_trans {A B C : Graph} (h1 : SameGraph A B) (h2 : SameGraph B C) :
    SameGraph A C :=
  ⟨fun v => (h1.1 v).trans (h2.1 v), fun u v => (h1.2 u v).trans (h2.2 u v)⟩

/-- Records are unchanged by replacing the final graph with one having the same nodes and
edges. -/
theorem opsRecord_right_congr (F : Graph) (ops : List Op) {R R' : Graph}
    (h : SameGraph R R') (hr : OpsRecord F ops R) : OpsRecord F ops R' := by
  induction ops generalizing F with
  | nil => exact sameGraph_trans (show SameGraph F R from hr) h
  | cons o ops ih =>
    cases o with
    | red v nb =>
      obtain ⟨h1, h2, h3, h4, h5⟩ := hr
      exact ⟨h1, h2, h3, h4, ih _ h5⟩
    | del w =>
      exact ⟨hr.1, ih _ hr.2⟩

/-- A copy has the same nodes and edges. -/
theorem sameGraph_copy (hInd : InducedSpec) {G : Graph} (hG : G.WF) :
    SameGraph G.copy G :=
  ⟨fun v => T2.mem_copy_iff hInd hG v, fun u v => T2.adj_copy_iff hInd hG u v⟩

/-- Every node of a well-formed graph lies in a component. -/
theorem nodes_iff_comp (hComp : ComponentsSpec) {H : Graph} (hH : H.WF) (x : Nat) :
    x ∈ H.nodes ↔ ∃ c ∈ H.components, x ∈ c := by
  have hperm := (hComp H hH).1
  constructor
  · intro hx
    obtain ⟨c, hc, hxc⟩ := List.mem_flatten.mp (hperm.mem_iff.symm.mp hx)
    exact ⟨c, hc, hxc⟩
  · rintro ⟨c, hc, hxc⟩
    exact hperm.mem_iff.mp (List.mem_flatten.mpr ⟨c, hc, hxc⟩)

/-- Members of `(componentGraphs H).reverse` are the induced graphs of components. -/
theorem exists_comp_of_mem {H J : Graph} (hJ : J ∈ (componentGraphs H).reverse) :
    ∃ c ∈ H.components, J = H.induced c.contains := by
  unfold componentGraphs at hJ
  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp (List.mem_reverse.mp hJ)
  exact ⟨c, hc, rfl⟩

/-- The disjoint union of the (reversed) components is `SameGraph` to `H`. -/
theorem sameGraph_unionAll_rev (hInd : InducedSpec) (hComp : ComponentsSpec)
    {H : Graph} (hH : H.WF) :
    SameGraph H (unionAll (componentGraphs H).reverse) := by
  have hgs : ∀ J ∈ (componentGraphs H).reverse, J.WF := fun J hJ =>
    T2.componentGraphs_wf hInd hH J (List.mem_reverse.mp hJ)
  obtain ⟨_, hN, hA⟩ := unionAllSpec _ hgs
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [hN]
    constructor
    · intro hx
      obtain ⟨c, hc, hxc⟩ := (nodes_iff_comp hComp hH x).mp hx
      refine ⟨H.induced c.contains, List.mem_reverse.mpr (List.mem_map.mpr ⟨c, hc, rfl⟩), ?_⟩
      exact (T2.mem_induced_comp_iff hInd hH c x).mpr ⟨hx, hxc⟩
    · rintro ⟨J, hJ, hxJ⟩
      exact T2.mem_of_componentGraphs hInd hH J (List.mem_reverse.mp hJ) x hxJ
  · rw [hA]
    constructor
    · intro hxy
      have hxH : x ∈ H.nodes := hH.nbrs_sub y x (hH.symm x y hxy)
      obtain ⟨c, hc, hxc⟩ := (nodes_iff_comp hComp hH x).mp hxH
      have hyc : y ∈ c := (hComp H hH).2.2 c hc x hxc y hxy
      exact ⟨H.induced c.contains, List.mem_reverse.mpr (List.mem_map.mpr ⟨c, hc, rfl⟩),
        (T2.adj_induced_comp_iff hInd hH c x y).mpr ⟨hxy, hxc, hyc⟩⟩
    · rintro ⟨J, hJ, hJxy⟩
      obtain ⟨c, _, rfl⟩ := exists_comp_of_mem hJ
      exact ((T2.adj_induced_comp_iff hInd hH c x y).mp hJxy).1

/-- Reachability inside a neighbour-closed set lifts to its induced graph. -/
theorem rtg_induced_aux {H J : Graph} (c : List Nat)
    (hcl : ∀ x ∈ c, ∀ y, H.Adj x y → y ∈ c)
    (hJ : ∀ a b, a ∈ c → b ∈ c → H.Adj a b → J.Adj a b)
    {x : Nat} (hx : x ∈ c) {y : Nat} (h : Relation.ReflTransGen H.Adj x y) :
    y ∈ c ∧ Relation.ReflTransGen J.Adj x y := by
  induction h with
  | refl => exact ⟨hx, Relation.ReflTransGen.refl⟩
  | @tail b d hxb hbd ih =>
    have hd : d ∈ c := hcl _ ih.1 _ hbd
    exact ⟨hd, ih.2.tail (hJ _ _ ih.1 hd hbd)⟩

/-- Degrees of an induced component agree with the degrees in `H`. -/
theorem degree_induced_eq (hInd : InducedSpec) {H : Graph} (hH : H.WF) (c : List Nat)
    (hcl : ∀ x ∈ c, ∀ y, H.Adj x y → y ∈ c) {v : Nat} (hv : v ∈ c) :
    (H.induced c.contains).degree v = H.degree v := by
  have hJ : (H.induced c.contains).WF := (hInd H c.contains hH).1
  unfold Graph.degree
  apply List.Perm.length_eq
  rw [List.perm_ext_iff_of_nodup (hJ.nbrs_nodup v) (hH.nbrs_nodup v)]
  intro u
  change (H.induced c.contains).Adj v u ↔ H.Adj v u
  rw [T2.adj_induced_comp_iff hInd hH c v u]
  constructor
  · exact fun h => h.1
  · intro h
    exact ⟨h, hv, hcl v hv u h⟩

/-- A component of a well-formed `H` with minimum degree `≥ 3` is a `T4Piece`. -/
theorem t4Piece_comp (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hConn : ComponentsConnected) {H : Graph} (hH : H.WF)
    (hMin : ∀ v ∈ H.nodes, 3 ≤ H.degree v) {c : List Nat} (hc : c ∈ H.components) :
    T4Piece (H.induced c.contains) := by
  have hJmem : ∀ x, x ∈ (H.induced c.contains).nodes ↔ x ∈ H.nodes ∧ x ∈ c :=
    fun x => T2.mem_induced_comp_iff hInd hH c x
  have hcl : ∀ x ∈ c, ∀ y, H.Adj x y → y ∈ c := (hComp H hH).2.2 c hc
  have hJadj : ∀ a b, a ∈ c → b ∈ c → H.Adj a b → (H.induced c.contains).Adj a b :=
    fun a b ha hb hab => (T2.adj_induced_comp_iff hInd hH c a b).mpr ⟨hab, ha, hb⟩
  obtain ⟨a, ha⟩ := List.exists_mem_of_ne_nil c ((hComp H hH).2.1 c hc)
  have haH : a ∈ H.nodes := (nodes_iff_comp hComp hH a).mpr ⟨c, hc, ha⟩
  refine ⟨(hInd H c.contains hH).1, List.ne_nil_of_mem ((hJmem a).mpr ⟨haH, ha⟩), ?_, ?_⟩
  · intro x hx y hy
    obtain ⟨_, hxc⟩ := (hJmem x).mp hx
    obtain ⟨_, hyc⟩ := (hJmem y).mp hy
    exact (rtg_induced_aux c hcl hJadj hxc (hConn H hH c hc x hxc y hyc)).2
  · intro v hv
    obtain ⟨hvH, hvc⟩ := (hJmem v).mp hv
    rw [degree_induced_eq hInd hH c hcl hvc]
    exact hMin v hvH

/-- Reversing a list keeps `T4Inv`. -/
theorem t4Inv_reverse {G0 : Graph} {gs : List Graph} {ops : List Op}
    (h : T4Inv G0 gs ops) : T4Inv G0 gs.reverse ops := by
  obtain ⟨hWF, hPw, hMem, hDel, hAdj⟩ := h
  refine ⟨fun J hJ => hWF J (List.mem_reverse.mp hJ), ?_,
    fun J hJ => hMem J (List.mem_reverse.mp hJ), hDel, ?_⟩
  · rw [List.pairwise_reverse]
    exact hPw.imp (fun {A B} hAB x hxB hxA => hAB x hxA hxB)
  · intro x y hxy hx hy
    obtain ⟨J, hJ, hJ'⟩ := hAdj x y hxy
      (by obtain ⟨J, hJ, h⟩ := hx; exact ⟨J, List.mem_reverse.mp hJ, h⟩)
      (by obtain ⟨J, hJ, h⟩ := hy; exact ⟨J, List.mem_reverse.mp hJ, h⟩)
    exact ⟨J, List.mem_reverse.mpr hJ, hJ'⟩

/-- Core of `t4LoopInvInit_of` for a given reduced graph `H` with a legal record. -/
theorem t4LoopInv_core (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hConn : ComponentsConnected) (hCongr : OpsRecordCongr) (G0 : Graph) (hG0 : G0.WF)
    (H : Graph) (ops : List Op) (hH : H.WF) (hRec : OpsRecord G0.copy ops H)
    (hMin : ∀ v ∈ H.nodes, 3 ≤ H.degree v) (hInv : T4Inv G0 (componentGraphs H) ops) :
    T4LoopInv G0 (componentGraphs H).reverse [] ops := by
  have hRec0 : OpsRecord G0 ops H :=
    hCongr G0.copy G0 H ops (T2.copy_wf hInd hG0) hG0 (sameGraph_copy hInd hG0) hRec
  have hRec1 : OpsRecord G0 ops (unionAll (componentGraphs H).reverse) :=
    opsRecord_right_congr G0 ops (sameGraph_unionAll_rev hInd hComp hH) hRec0
  unfold T4LoopInv
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · rw [List.map_nil, List.append_nil]
    exact t4Inv_reverse hInv
  · intro e he
    simp at he
  · rw [List.map_nil, List.append_nil]
    exact hRec1
  · intro J hJ
    rw [List.map_nil, List.append_nil] at hJ
    obtain ⟨c, hc, rfl⟩ := exists_comp_of_mem hJ
    exact t4Piece_comp hInd hComp hConn hH hMin hc
  · intro e he
    simp at he

end T4LoopInit

open T4LoopInit

/-- (D2a1) The invariant holds at the start of the loop in `algoT4Full`. -/
theorem t4LoopInvInit_of (hMax : ReduceRecordMaximal) (hConn : ComponentsConnected)
    (hCongr : OpsRecordCongr) : T4LoopInvInit := by
  intro G hG
  dsimp only
  have hG0 : (nonIsolated G).WF := (inducedSpec _ _ hG).1
  have hC : (nonIsolated G).copy.WF := T2.copy_wf inducedSpec hG0
  have hRS := (reduceRecordSpec _ hC).1
  have hM := hMax _ hC
  exact t4LoopInv_core inducedSpec componentsSpec hConn hCongr (nonIsolated G) hG0
    (reduceRecordF (nonIsolated G).copy).1 (reduceRecordF (nonIsolated G).copy).2.1 hRS
    hM.1 hM.2.1 (t4InitInv G hG)

#print axioms CubicPathwidth.Alg.t4LoopInvInit_of

end CubicPathwidth.Alg
Back to top