CubicPathwidth.Alg.Proofs.T2InitInv

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

import CubicPathwidth.Alg.Spec

/-!
Task T2: `T4InitInv`, the invariant of `algo_T4` before the work loop starts.

With `G0 := nonIsolated G`, `H := (reduceRecordF G0.copy).1` and `ops := (reduceRecordF G0.copy).2.1`,
the initial work list is `componentGraphs H`. Its members are the induced graphs of the
components of `H`; they are well formed (`InducedSpec`), pairwise vertex-disjoint (the
components are a partition of `H.nodes`, which is duplicate-free), contained in `G0`
(`ReduceRecordSpec`), and every edge of `G0` between two vertices of `H` is an edge of
`H` (edge preservation of `ReduceRecordSpec` on `G0.copy`) and lies in the component of its
first end (closure in `ComponentsSpec`). The recorded ops are all reductions, so they
delete nothing (`deletedSet ops = []`).

Only `InducedSpec`, `ComponentsSpec` and `ReduceRecordSpec` are used; `WFBasics` is not needed.
-/

namespace CubicPathwidth.Alg

open Graph

namespace T2

/-- Membership in `copy`. -/
theorem mem_copy_iff (hInd : InducedSpec) {G : Graph} (hG : G.WF) (x : Nat) :
    x ∈ G.copy.nodes ↔ x ∈ G.nodes := by
  have h := (hInd G (fun _ => true) hG).2.1 x
  constructor
  · intro hx
    exact (h.mp hx).1
  · intro hx
    exact h.mpr ⟨hx, rfl⟩

/-- Adjacency in `copy`. -/
theorem adj_copy_iff (hInd : InducedSpec) {G : Graph} (hG : G.WF) (x y : Nat) :
    G.copy.Adj x y ↔ G.Adj x y := by
  have h := (hInd G (fun _ => true) hG).2.2 x y
  constructor
  · intro hxy
    exact (h.mp hxy).1
  · intro hxy
    exact h.mpr ⟨hxy, rfl, rfl⟩

/-- `copy` is well formed. -/
theorem copy_wf (hInd : InducedSpec) {G : Graph} (hG : G.WF) : G.copy.WF :=
  (hInd G (fun _ => true) hG).1

/-- Nodes of an induced graph of a component. -/
theorem mem_induced_comp_iff (hInd : InducedSpec) {H : Graph} (hH : H.WF) (c : List Nat)
    (x : Nat) :
    x ∈ (H.induced c.contains).nodes ↔ x ∈ H.nodes ∧ x ∈ c := by
  rw [(hInd H c.contains hH).2.1 x, List.contains_iff_mem]

/-- Edges of an induced graph of a component. -/
theorem adj_induced_comp_iff (hInd : InducedSpec) {H : Graph} (hH : H.WF) (c : List Nat)
    (x y : Nat) :
    (H.induced c.contains).Adj x y ↔ H.Adj x y ∧ x ∈ c ∧ y ∈ c := by
  rw [(hInd H c.contains hH).2.2 x y, List.contains_iff_mem, List.contains_iff_mem]

/-- The components of `H` are pairwise disjoint. -/
theorem components_pairwise_disjoint (hComp : ComponentsSpec) {H : Graph} (hH : H.WF) :
    H.components.Pairwise List.Disjoint := by
  have hperm : H.components.flatten.Perm H.nodes := (hComp H hH).1
  have hnd : H.components.flatten.Nodup := hperm.nodup_iff.mpr hH.nodup
  exact (List.nodup_flatten.mp hnd).2

/-- The induced graphs of the components are pairwise vertex-disjoint. -/
theorem componentGraphs_pairwise (hInd : InducedSpec) (hComp : ComponentsSpec) {H : Graph}
    (hH : H.WF) :
    (componentGraphs H).Pairwise (fun A B => ∀ x, x ∈ A.nodes → x ∉ B.nodes) := by
  unfold componentGraphs
  rw [List.pairwise_map]
  refine (components_pairwise_disjoint hComp hH).imp ?_
  intro c d hcd x hxc hxd
  rw [mem_induced_comp_iff hInd hH] at hxc hxd
  exact hcd hxc.2 hxd.2

/-- Every member of `componentGraphs H` is well formed. -/
theorem componentGraphs_wf (hInd : InducedSpec) {H : Graph} (hH : H.WF) :
    ∀ J ∈ componentGraphs H, J.WF := by
  intro J hJ
  unfold componentGraphs at hJ
  obtain ⟨c, _, rfl⟩ := List.mem_map.mp hJ
  exact (hInd H c.contains hH).1

/-- Vertices of a member of `componentGraphs H` are nodes of `H`. -/
theorem mem_of_componentGraphs (hInd : InducedSpec) {H : Graph} (hH : H.WF) :
    ∀ J ∈ componentGraphs H, ∀ x ∈ J.nodes, x ∈ H.nodes := by
  intro J hJ x hx
  unfold componentGraphs at hJ
  obtain ⟨c, _, rfl⟩ := List.mem_map.mp hJ
  exact ((mem_induced_comp_iff hInd hH c x).mp hx).1

/-- Deleted set of an op list made only of reductions is empty. -/
theorem deletedSet_nil_of_red (ops : List Op) (h : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    deletedSet ops = [] := by
  unfold deletedSet
  rw [List.filterMap_eq_nil_iff]
  intro a ha
  obtain ⟨v, nb, rfl⟩ := h a ha
  rfl

/-- Core of `T4InitInv`: the invariant for any `G0` well formed and any `H` that is the
result of `reduceRecord` on a copy of `G0` (as given by `ReduceRecordSpec`), with
`H.nodes ⊆ G0.nodes` and edge preservation. -/
theorem t4Inv_of_reduce (hInd : InducedSpec) (hComp : ComponentsSpec) (G0 : Graph)
    (_hG0 : G0.WF) (H : Graph) (ops : List Op) (hH : H.WF)
    (hHsub : ∀ x ∈ H.nodes, x ∈ G0.nodes)
    (hHadj : ∀ x y, x ∈ H.nodes → y ∈ H.nodes → G0.Adj x y → H.Adj x y)
    (hOps : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    T4Inv G0 (componentGraphs H) ops := by
  have hDel : deletedSet ops = [] := deletedSet_nil_of_red ops hOps
  refine ⟨componentGraphs_wf hInd hH, componentGraphs_pairwise hInd hComp hH, ?_, ?_, ?_⟩
  · intro J hJ x hx
    rw [hDel]
    refine ⟨hHsub x (mem_of_componentGraphs hInd hH J hJ x hx), ?_⟩
    simp
  · intro x hx
    rw [hDel] at hx
    simp at hx
  · intro x y hxy hxJ hyJ
    obtain ⟨J, hJ, hxJ⟩ := hxJ
    obtain ⟨J', hJ', hyJ'⟩ := hyJ
    have hxH : x ∈ H.nodes := mem_of_componentGraphs hInd hH J hJ x hxJ
    have hyH : y ∈ H.nodes := mem_of_componentGraphs hInd hH J' hJ' y hyJ'
    have hAdj : H.Adj x y := hHadj x y hxH hyH hxy
    unfold componentGraphs at hJ
    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hJ
    have hxc : x ∈ c := ((mem_induced_comp_iff hInd hH c x).mp hxJ).2
    have hyc : y ∈ c := (hComp H hH).2.2 c hc x hxc y hAdj
    refine ⟨H.induced c.contains, ?_, ?_⟩
    · unfold componentGraphs
      exact List.mem_map.mpr ⟨c, hc, rfl⟩
    · exact (adj_induced_comp_iff hInd hH c x y).mpr ⟨hAdj, hxc, hyc⟩

end T2

open T2

/-- Task T2 (Stage 1): the invariant holds initially, for every well-formed graph. -/
theorem t4InitInv_of (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hRed : ReduceRecordSpec) : T4InitInv := by
  intro G hG
  have hG0 : (nonIsolated G).WF := (hInd G _ hG).1
  have hC : (nonIsolated G).copy.WF := copy_wf hInd hG0
  obtain ⟨hHWF, hHsub, hHadj, hOps, _⟩ := hRed _ hC
  have hOps' : ∀ o ∈ (reduceRecordF (nonIsolated G).copy).2.1, ∃ v nb, o = Op.red v nb := by
    intro o ho
    obtain ⟨v, nb, he, _⟩ := hOps o ho
    exact ⟨v, nb, he⟩
  refine t4Inv_of_reduce hInd hComp (nonIsolated G) hG0 (reduceRecordF (nonIsolated G).copy).1
    (reduceRecordF (nonIsolated G).copy).2.1 hHWF ?_ ?_ hOps'
  · intro x hx
    have hx' : x ∈ (nonIsolated G).copy.nodes := hHsub x hx
    exact (mem_copy_iff hInd hG0 x).mp hx'
  · intro x y hx hy hxy
    have hxy' : (nonIsolated G).copy.Adj x y := (adj_copy_iff hInd hG0 x y).mpr hxy
    exact hHadj x y hx hy hxy'

#print axioms CubicPathwidth.Alg.t4InitInv_of

end CubicPathwidth.Alg
Back to top