CubicPathwidth.Alg.Proofs.A12Top

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

import CubicPathwidth.Alg.Spec

/-!
Tasks A1, A2 and the top-level part of A3 of Stage 1.

* `algoT2aValid_of`: `algoT2a` is `plainLayout`, so `PlainLayoutValid` gives validity.
* `algoT1Valid_of`: `algoT1` is `switchedLayout`, so `SwitchedLayoutValid` gives validity.
* `algoMixedValid_of`: `algoMixed G lab = undo G ops H bagsH` with `r := reduceRecordF G.copy`,
  `H := r.1`, `ops := r.2.1`, `bagsH := if H.numNodes = 0 then [] else plainLayout H (lab H)`.
  The hypotheses of `UndoValid` are checked from `ReduceRecordSpec` (on `G.copy`, whose
  nodes, adjacency and well-formedness come from `InducedSpec`); all ops are reductions,
  so `deletedSet ops = []`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace A12

/-- The deleted set of a list of operations made only of reductions is empty. -/
theorem deletedSet_eq_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 o ho
  obtain ⟨v, nb, rfl⟩ := h o ho
  rfl

/-- Validity of the bags used for the reduced graph `H` in `algo_mixed`. -/
theorem bagsH_valid (hPL : PlainLayoutValid) (H : Graph) (lab : Labeler) (hH : H.WF) :
    ValidPD H (if H.numNodes = 0 then [] else plainLayout H (lab H)) ∧
      BagsWithin H (if H.numNodes = 0 then [] else plainLayout H (lab H)) := by
  by_cases h0 : H.numNodes = 0
  · have hnil : H.nodes = [] := List.eq_nil_of_length_eq_zero h0
    simp only [h0, ↓reduceIte]
    refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
    · intro v hv
      simp [hnil] at hv
    · intro v hv
      simp [hnil] at hv
    · intro u v hu _
      simp [hnil] at hu
    · intro B hB
      simp at hB
  · simp only [h0, ↓reduceIte]
    exact hPL H hH (lab H)

/-- The core of `algo_mixed`: for any reduction record `(H, ops)` of `G.copy` (with the
facts that `ReduceRecordSpec` gives), `algoMixedF` is `undo G ops H bagsH`, which is valid. -/
theorem mixed_core (hPL : PlainLayoutValid) (hUndo : UndoValid) (G : Graph) (lab : Labeler)
    (H : Graph) (ops : List Op) (hG : G.WF) (hH : H.WF)
    (hHsub : ∀ x ∈ H.nodes, x ∈ G.nodes)
    (hHadj : ∀ x y, x ∈ H.nodes → y ∈ H.nodes → G.Adj x y → H.Adj x y)
    (hOps : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    ValidPD G (undo G ops H (if H.numNodes = 0 then [] else plainLayout H (lab H))) := by
  have hBags := bagsH_valid hPL H lab hH
  have hDel : deletedSet ops = [] := deletedSet_eq_nil_of_red ops hOps
  exact (hUndo G H ops _ hG hH
    (fun x hx => ⟨hHsub x hx, by rw [hDel]; simp⟩)
    (fun x y hx hy hxy => hHadj x y hx hy hxy)
    hBags.1 hBags.2).1

end A12

/-- Task A1 (`algo_T2a` is `plain_layout`): validity of the plain sweep gives validity of
`algo_T2a`. -/
theorem algoT2aValid_of (hPL : PlainLayoutValid) : AlgoT2aValid := by
  intro G hG Y
  exact (hPL G hG Y).1

/-- Task A2 (`algo_T1` is `switched_layout`): validity of the switched layout gives
validity of `algo_T1` (the degree hypothesis is not needed). -/
theorem algoT1Valid_of (hSL : SwitchedLayoutValid) : AlgoT1Valid := by
  intro G hG _ Y
  exact (hSL G hG Y).1

/-- Task A3 (`algo_mixed`, top level): from the reduction spec, the induced-subgraph spec,
the plain sweep and the undo lemma, `algo_mixed` is valid for every graph and labeler. -/
theorem algoMixedValid_of (hWF : WFBasics) (hInd : InducedSpec) (hRed : ReduceRecordSpec)
    (hPL : PlainLayoutValid) (hUndo : UndoValid) : AlgoMixedValid := by
  intro G hG lab
  have hC : G.copy.WF := (hInd G (fun _ => true) hG).1
  have hCn : ∀ x, x ∈ G.copy.nodes ↔ x ∈ G.nodes := fun x => by
    have := (hInd G (fun _ => true) hG).2.1 x
    simpa [Graph.copy] using this
  have hCa : ∀ x y, G.copy.Adj x y ↔ G.Adj x y := fun x y => by
    have := (hInd G (fun _ => true) hG).2.2 x y
    simpa [Graph.copy] using this
  obtain ⟨hHwf, hHsub, hHadj, hOps, -⟩ := hRed G.copy hC
  have hOps' : ∀ o ∈ (reduceRecordF G.copy).2.1, ∃ v nb, o = Op.red v nb := fun o ho => by
    obtain ⟨v, nb, h1, -⟩ := hOps o ho
    exact ⟨v, nb, h1⟩
  exact A12.mixed_core hPL hUndo G lab (reduceRecordF G.copy).1 (reduceRecordF G.copy).2.1
    hG hHwf
    (fun x hx => (hCn x).1 (hHsub x hx))
    (fun x y hx hy hxy => hHadj x y hx hy ((hCa x y).2 hxy))
    hOps'

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT2aValid_of
#print axioms CubicPathwidth.Alg.algoT1Valid_of
#print axioms CubicPathwidth.Alg.algoMixedValid_of
Back to top