CubicPathwidth.Alg.Proofs.A3T4

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

import CubicPathwidth.Alg.Spec

/-!
# Task A3: validity of `algo_T4` from its hypotheses (task A3)

`algoT4Valid_of` takes the statements T1, T2, G6, G7, C2, C7 and T3 as hypotheses (each is
proved in another file) and proves `AlgoT4Valid`.

Route: `G0 := nonIsolated G`; the work loop of `algo_T4` keeps the invariant `T4Inv`
(`T4InitInv` and `T4LoopPreserves`). Every final entry decomposes validly inside its own
graph (`PlainLayoutValid` for `.sweep`; `UndoValid` with `R = Graph.empty` for `.thin`).
`ConcatValid` decomposes `R = unionAll` of the final graphs; `UndoValid` on `G0` inserts
the deletions; `AppendIsolatedValid` appends the isolated vertices.
-/

namespace CubicPathwidth.Alg

open Graph

namespace A3

/-- `T4Inv` depends only on the membership of the graphs in the work list, and the
disjointness clause is symmetric, so a permutation of the list preserves it. -/
theorem t4Inv_perm {G0 : Graph} {gs gs' : List Graph} {ops : List Op}
    (hp : gs.Perm gs') (h : T4Inv G0 gs ops) : T4Inv G0 gs' ops := by
  obtain ⟨h1, h2, h3, h4, h5⟩ := h
  refine ⟨fun J hJ => h1 J (hp.mem_iff.2 hJ), ?_, fun J hJ => h3 J (hp.mem_iff.2 hJ), h4, ?_⟩
  · exact (List.Perm.pairwise_iff (R := fun A B : Graph => ∀ x, x ∈ A.nodes → x ∉ B.nodes)
      (fun {A B} h x hB hA => h x hA hB) hp).1 h2
  · intro x y hxy hx hy
    have hx' : ∃ J ∈ gs, x ∈ J.nodes := by
      obtain ⟨J, hJ, hxJ⟩ := hx
      exact ⟨J, hp.mem_iff.2 hJ, hxJ⟩
    have hy' : ∃ J ∈ gs, y ∈ J.nodes := by
      obtain ⟨J, hJ, hyJ⟩ := hy
      exact ⟨J, hp.mem_iff.2 hJ, hyJ⟩
    obtain ⟨J, hJ, hadj⟩ := h5 x y hxy hx' hy'
    exact ⟨J, hp.mem_iff.1 hJ, hadj⟩

/-- The empty graph is well formed. -/
theorem empty_wf : Graph.empty.WF where
  nodup := List.nodup_nil
  mem_iff := by intro v; simp [Graph.mem, Graph.empty]
  nbrs_nodup := by intro v; simp [Graph.nbrs, Graph.empty]
  nbrs_sub := by intro u v h; simp [Graph.nbrs, Graph.empty] at h
  symm := by intro u v h; simp [Graph.nbrs, Graph.empty] at h
  loopless := by intro v h; simp [Graph.nbrs, Graph.empty] at h

/-- The empty decomposition is valid for the empty graph. -/
theorem validPD_empty : ValidPD Graph.empty [] := by
  unfold ValidPD
  refine ⟨?_, ?_, ?_⟩
  · intro v hv; simp [Graph.empty] at hv
  · intro v hv; simp [Graph.empty] at hv
  · intro u v hu; simp [Graph.empty] at hu

/-- No bags, so no bag leaves the graph. -/
theorem bagsWithin_nil (G : Graph) : BagsWithin G [] := by
  unfold BagsWithin
  intro B hB
  simp at hB

/-- Flattening the parts of the concatenation gives the bags of the thin/sweep entries. -/
theorem flatMap_parts (lab : Labeler) (l : List FinalEntry) :
    (l.map (fun e => (e.graph, (t4Decompose lab e).1))).flatMap (·.2) =
      (l.map (t4Decompose lab)).flatMap (·.1) := by
  simp only [List.flatMap_map]

/-- Each final entry decomposes validly inside its own graph. -/
theorem finalPart (hPL : PlainLayoutValid) (hUndo : UndoValid) (lab : Labeler)
    (final : List FinalEntry) (hWF : ∀ J ∈ final.map (·.graph), J.WF)
    (hTh : ThinOK final) :
    ∀ e ∈ final, ValidPD e.graph (t4Decompose lab e).1 ∧
      BagsWithin e.graph (t4Decompose lab e).1 := by
  intro e he
  rcases e with ⟨g, k, tops⟩
  have hw : g.WF := hWF g (List.mem_map_of_mem (f := fun e : FinalEntry => e.graph) he)
  cases k with
  | sweep => exact hPL g hw (lab g)
  | thin =>
    have h := hUndo g Graph.empty tops [] hw empty_wf
      (by intro x hx; simp [Graph.empty] at hx)
      (by intro x y hx; simp [Graph.empty] at hx)
      validPD_empty (bagsWithin_nil _)
    exact ⟨h.1, h.2 (hTh ⟨g, FinalKind.thin, tops⟩ he)⟩

/-- The decomposition of the final graphs and the deletions, from the invariant. -/
theorem finalStep (hU : UnionAllSpec) (hCat : ConcatValid)
    (hPL : PlainLayoutValid) (hUndo : UndoValid) (hIso : AppendIsolatedValid)
    (G : Graph) (lab : Labeler) (hG : G.WF) (final : List FinalEntry) (ops : List Op)
    (hG0 : (nonIsolated G).WF)
    (hT : T4Inv (nonIsolated G) (final.map (·.graph)) ops) (hTh : ThinOK final) :
    ValidPD G ((undoF (nonIsolated G) ops (unionAll (final.map (·.graph)))
      ((final.map (t4Decompose lab)).flatMap (·.1))).1 ++ isolatedBags G) := by
  obtain ⟨hWF, hPw, hNd, hDel, hEdge⟩ := hT
  have hPart := finalPart hPL hUndo lab final hWF hTh
  -- the parts of `ConcatValid`
  have hparts : ∀ p ∈ final.map (fun e => (e.graph, (t4Decompose lab e).1)),
      p.1.WF ∧ ValidPD p.1 p.2 ∧ BagsWithin p.1 p.2 := by
    intro p hp
    obtain ⟨e, he, rfl⟩ := List.mem_map.1 hp
    exact ⟨hWF _ (List.mem_map_of_mem (f := fun e : FinalEntry => e.graph) he),
      (hPart e he).1, (hPart e he).2⟩
  have hdis : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).Pairwise
      (fun A B => ∀ x, x ∈ A.1.nodes → x ∉ B.1.nodes) :=
    List.pairwise_map.2 (List.pairwise_map.1 hPw)
  obtain ⟨hV, hB⟩ := hCat (final.map (fun e => (e.graph, (t4Decompose lab e).1))) hparts hdis
  have e1 : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).map (·.1) =
      final.map (·.graph) := by
    simp only [List.map_map]
    rfl
  have e2 : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).flatMap (·.2) =
      (final.map (t4Decompose lab)).flatMap (·.1) := flatMap_parts lab final
  rw [e1, e2] at hV hB
  -- the union of the final graphs
  have hRU := hU (final.map (·.graph)) (fun J hJ => hWF J hJ)
  have hRsub : ∀ x ∈ (unionAll (final.map (·.graph))).nodes,
      x ∈ (nonIsolated G).nodes ∧ x ∉ deletedSet ops := by
    intro x hx
    obtain ⟨J, hJ, hxJ⟩ := (hRU.2.1 x).1 hx
    exact hNd J hJ x hxJ
  have hRadj : ∀ x y, x ∈ (unionAll (final.map (·.graph))).nodes →
      y ∈ (unionAll (final.map (·.graph))).nodes →
      (nonIsolated G).Adj x y → (unionAll (final.map (·.graph))).Adj x y := by
    intro x y hx hy hxy
    obtain ⟨J1, hJ1, hx1⟩ := (hRU.2.1 x).1 hx
    obtain ⟨J2, hJ2, hy2⟩ := (hRU.2.1 y).1 hy
    obtain ⟨J, hJ, hadj⟩ := hEdge x y hxy ⟨J1, hJ1, hx1⟩ ⟨J2, hJ2, hy2⟩
    exact (hRU.2.2 x y).2 ⟨J, hJ, hadj⟩
  -- undo the reductions and deletions, then the isolated vertices
  obtain ⟨hV0, hB0⟩ := hUndo (nonIsolated G) (unionAll (final.map (·.graph))) ops
    ((final.map (t4Decompose lab)).flatMap (·.1)) hG0 hRU.1 hRsub hRadj hV hB
  exact hIso G hG _ hV0 (hB0 hDel)

end A3

/-- Validity of `algo_T4` (task A3), from the hypotheses proved in other files. -/
theorem algoT4Valid_of (hWF : WFBasics) (hInd : InducedSpec) (hU : UnionAllSpec)
    (hCat : ConcatValid) (hPL : PlainLayoutValid) (hUndo : UndoValid) (hInit : T4InitInv)
    (hLoop : T4LoopPreserves) (hIso : AppendIsolatedValid) : AlgoT4Valid := by
  intro G hG lab
  have hG0 : (nonIsolated G).WF := (hInd G (fun v => G.degree v != 0) hG).1
  have hT0 : T4Inv (nonIsolated G) (componentGraphs (reduceRecordF (nonIsolated G).copy).1)
      (reduceRecordF (nonIsolated G).copy).2.1 := hInit G hG
  have hStart : T4Inv (nonIsolated G)
      ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse ++
        ([] : List FinalEntry).map (·.graph))
      (reduceRecordF (nonIsolated G).copy).2.1 := by
    rw [List.map_nil, List.append_nil]
    exact A3.t4Inv_perm (List.reverse_perm _).symm hT0
  have hL := hLoop (nonIsolated G) (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
    _ [] _ hG0 hStart (by unfold ThinOK; intro e he; simp at he)
  obtain ⟨hT, hTh⟩ := hL
  have key := A3.finalStep hU hCat hPL hUndo hIso G lab hG _ _ hG0 hT hTh
  exact key

#print axioms CubicPathwidth.Alg.algoT4Valid_of

end CubicPathwidth.Alg