CubicPathwidth.SectionInsertion

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

import CubicPathwidth.SectionAssembly

/-! Insert a disjoint attached section at an existing bag, retaining that bag. -/

noncomputable section
namespace CubicPathwidth
namespace BagPath
variable {V : Type*}

def takeUntil (P : BagPath V) (i : ℕ) (hi : i ≤ P.lastIndex) : BagPath V where
  lastIndex := i
  bag := P.bag
  interval := by
    intro a b c hab hbc hc v hv
    exact P.interval a b c hab hbc (hc.trans hi) v hv

def suffix (P : BagPath V) (i : ℕ) (_hi : i ≤ P.lastIndex) : BagPath V where
  lastIndex := P.lastIndex - i
  bag := fun j => P.bag (j + i)
  interval := by
    intro a b c hab hbc hc v hv
    exact P.interval (a + i) (b + i) (c + i) (by omega) (by omega) (by omega) v hv

theorem takeUntil_width (P : BagPath V) (i) (hi) {w : ℝ} (hP : P.WidthAtMost w) :
    (P.takeUntil i hi).WidthAtMost w := fun j hj => hP j (hj.trans hi)

theorem suffix_width (P : BagPath V) (i) (hi) {w : ℝ} (hP : P.WidthAtMost w) :
    (P.suffix i hi).WidthAtMost w := by
  intro j hj
  exact hP (j + i) (by change j ≤ P.lastIndex - i at hj; omega)

theorem concat_subset (P Q : BagPath V) (hc : Compatible P Q) (W : Finset V)
    (hP : ∀ i, i ≤ P.lastIndex → P.bag i ⊆ W)
    (hQ : ∀ i, i ≤ Q.lastIndex → Q.bag i ⊆ W) :
    ∀ i, i ≤ (P.concat Q hc).lastIndex → (P.concat Q hc).bag i ⊆ W := by
  intro i hi
  change i ≤ P.lastIndex + Q.lastIndex + 1 at hi
  by_cases h : i ≤ P.lastIndex
  · rw [concat_bag_left _ _ _ _ h]
    exact hP i h
  · change (if i ≤ P.lastIndex then P.bag i else Q.bag (i - (P.lastIndex + 1))) ⊆ W
    rw [ite_eq_right h]
    exact hQ _ (by omega)

end BagPath
namespace SectionDecomposition
variable {n : ℕ} {G : SimpleGraph (Fin n)} {U V : Finset (Fin n)}

/-- The inserted section meets the old graph only through the chosen bag.
Every old bag survives unchanged. Repeated insertions at those surviving
bags therefore take a maximum of costs, rather than accumulating overhead. -/
theorem insert_at_bag (P : SectionDecomposition G U) (Q : SectionDecomposition G V)
    (hdis : Disjoint U V) (i : ℕ) (hi : i ≤ P.lastIndex)
    (hsep : ∀ v ∈ V, ∀ u ∈ U, G.Adj v u → u ∈ P.bag i)
    {a b : ℝ} (hP : P.toBagPath.WidthAtMost a) (hQ : Q.toBagPath.WidthAtMost b) :
    ∃ R : SectionDecomposition G (U ∪ V),
      R.toBagPath.WidthAtMost (max a (b + ((P.bag i).card : ℝ))) ∧
      ∀ k, k ≤ P.lastIndex → ∃ j, j ≤ R.lastIndex ∧ R.bag j = P.bag k := by
  let A := P.toBagPath.takeUntil i hi
  let M := Q.hold (P.bag i)
  let B := P.toBagPath.suffix i hi
  have hAM : BagPath.Compatible A M.toBagPath := by
    intro v j k hj hk hvj hvk
    have hvU : v ∈ U := P.bag_subset j (hj.trans hi) hvj
    have hvI : v ∈ P.bag i := by
      rcases Finset.mem_union.mp hvk with hvQ | hvI
      · exact False.elim (Finset.disjoint_left.mp hdis hvU (Q.bag_subset k hk hvQ))
      · exact hvI
    exact ⟨hvI, Finset.mem_union_right _ hvI⟩
  let T := A.concat M.toBagPath hAM
  have hTB : BagPath.Compatible T B := by
    intro v j k hj hk hvj hvk
    have hk' : k + i ≤ P.lastIndex := by change k ≤ P.lastIndex - i at hk; omega
    have hvU : v ∈ U := P.bag_subset (k + i) hk' hvk
    have hvI : v ∈ P.bag i := by
      by_cases hjA : j ≤ i
      · have hvold : v ∈ P.bag j := by
          rw [BagPath.concat_bag_left _ _ _ _ hjA] at hvj
          exact hvj
        exact P.interval j i (k + i) hjA (by omega) hk' v ⟨hvold, hvk⟩
      · have hjM : j - (i + 1) ≤ Q.lastIndex := by
          change j ≤ i + Q.lastIndex + 1 at hj
          omega
        have hvM : v ∈ Q.bag (j - (i + 1)) ∪ P.bag i := by
          change v ∈ (if j ≤ i then P.bag j else Q.bag (j - (i + 1)) ∪ P.bag i) at hvj
          rwa [ite_eq_right hjA] at hvj
        rcases Finset.mem_union.mp hvM with hvQ | hvI
        · exact False.elim (Finset.disjoint_left.mp hdis hvU (Q.bag_subset _ hjM hvQ))
        · exact hvI
    constructor
    · rw [BagPath.concat_last]
      exact Finset.mem_union_right _ hvI
    · change v ∈ P.bag (0 + i)
      simpa only [Nat.zero_add] using hvI
  let R := T.concat B hTB
  have hRlen : R.lastIndex = T.lastIndex + B.lastIndex + 1 := rfl
  have hTlen : T.lastIndex = i + Q.lastIndex + 1 := rfl
  have hBlen : B.lastIndex = P.lastIndex - i := rfl
  have hOld : ∀ k, k ≤ P.lastIndex → ∃ j, j ≤ R.lastIndex ∧ R.bag j = P.bag k := by
    intro k hk
    by_cases hki : k ≤ i
    · refine ⟨k, ?_, ?_⟩
      · rw [hRlen, hTlen, hBlen]; omega
      · rw [BagPath.concat_bag_left _ _ _ _ (by rw [hTlen]; omega),
          BagPath.concat_bag_left _ _ _ _ hki]
        rfl
    · refine ⟨T.lastIndex + 1 + (k - i), ?_, ?_⟩
      · rw [hRlen, hBlen]; omega
      · rw [BagPath.concat_bag_right]
        change P.bag (k - i + i) = P.bag k
        rw [Nat.sub_add_cancel (by omega)]
  have hMid : ∀ k, k ≤ Q.lastIndex →
      i + 1 + k ≤ R.lastIndex ∧ R.bag (i + 1 + k) = Q.bag k ∪ P.bag i := by
    intro k hk
    constructor
    · rw [hRlen, hTlen, hBlen]; omega
    · rw [BagPath.concat_bag_left _ _ _ _ (by rw [hTlen]; omega)]
      exact BagPath.concat_bag_right A M.toBagPath hAM k
  have hsubset : ∀ j, j ≤ R.lastIndex → R.bag j ⊆ U ∪ V := by
    apply BagPath.concat_subset
    · apply BagPath.concat_subset
      · intro j hj
        exact (P.bag_subset j (hj.trans hi)).trans Finset.subset_union_left
      · intro j hj v hv
        rcases Finset.mem_union.mp hv with hv | hv
        · exact Finset.mem_union_right _ (Q.bag_subset j hj hv)
        · exact Finset.mem_union_left _ (P.bag_subset i hi hv)
    · intro j hj
      exact (P.bag_subset (j + i) (by change j ≤ P.lastIndex - i at hj; omega)).trans
        Finset.subset_union_left
  let D : SectionDecomposition G (U ∪ V) := {
    toBagPath := R
    bag_subset := hsubset
    vertex_covered := by
      intro v hv
      rcases Finset.mem_union.mp hv with hvU | hvV
      · obtain ⟨k, hk, hvk⟩ := P.vertex_covered v hvU
        obtain ⟨j, hj, he⟩ := hOld k hk
        exact ⟨j, hj, he.symm ▸ hvk⟩
      · obtain ⟨k, hk, hvk⟩ := Q.vertex_covered v hvV
        exact ⟨i + 1 + k, (hMid k hk).1, (hMid k hk).2.symm ▸ Finset.mem_union_left _ hvk⟩
    edge_covered := by
      intro u hu v hv huv
      by_cases huU : u ∈ U
      · by_cases hvU : v ∈ U
        · obtain ⟨k, hk, huk, hvk⟩ := P.edge_covered u huU v hvU huv
          obtain ⟨j, hj, he⟩ := hOld k hk
          exact ⟨j, hj, he.symm ▸ huk, he.symm ▸ hvk⟩
        · have hvV := (Finset.mem_union.mp hv).resolve_left hvU
          obtain ⟨k, hk, hvk⟩ := Q.vertex_covered v hvV
          exact ⟨i + 1 + k, (hMid k hk).1,
            (hMid k hk).2.symm ▸ Finset.mem_union_right _ (hsep v hvV u huU huv.symm),
            (hMid k hk).2.symm ▸ Finset.mem_union_left _ hvk⟩
      · have huV := (Finset.mem_union.mp hu).resolve_left huU
        by_cases hvU : v ∈ U
        · obtain ⟨k, hk, huk⟩ := Q.vertex_covered u huV
          exact ⟨i + 1 + k, (hMid k hk).1,
            (hMid k hk).2.symm ▸ Finset.mem_union_left _ huk,
            (hMid k hk).2.symm ▸ Finset.mem_union_right _ (hsep u huV v hvU huv)⟩
        · have hvV := (Finset.mem_union.mp hv).resolve_left hvU
          obtain ⟨k, hk, huk, hvk⟩ := Q.edge_covered u huV v hvV huv
          exact ⟨i + 1 + k, (hMid k hk).1,
            (hMid k hk).2.symm ▸ Finset.mem_union_left _ huk,
            (hMid k hk).2.symm ▸ Finset.mem_union_left _ hvk⟩ }
  refine ⟨D, ?_, hOld⟩
  have hw := BagPath.concat_width hTB
    (BagPath.concat_width hAM (BagPath.takeUntil_width _ _ _ hP) (hold_width Q _ hQ))
    (BagPath.suffix_width _ _ _ hP)
  exact hw.mono (max_le le_rfl (le_max_left _ _))

end SectionDecomposition
end CubicPathwidth