CubicPathwidth.Alg.Proofs.G8SeparatorGlue

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

import CubicPathwidth.Alg.Spec

/-!
# G8: gluing at a separator (`SeparatorGlueValid`)

The parts `(c, B_c)` of `pd_tw2` have vertex lists that are pairwise disjoint and
partition `H.nodes \ X`; every bag of part `c` is extended by `X`. Vertices of `X` lie in
every bag; a vertex outside `X` lies in the bags of its unique part only, which form an
interval by validity of that part. Helpers live in `CubicPathwidth.Alg.G8`.
-/

namespace CubicPathwidth.Alg

namespace G8

/-- Convexity of the positions of `v` in a list of bags (the second clause of `ValidPD`). -/
def ConvV (bs : List Bag) (v : Nat) : Prop :=
  ∀ i j k, i ≤ j → j ≤ k → InBag bs i v → InBag bs k v → InBag bs j v

/-- The bags of `parts` after adding the separator `X` to each bag. -/
abbrev outOf (parts : List (List Nat × List Bag)) (X : Bag) : List Bag :=
  parts.flatMap fun p => p.2.map (fun B => bagUnion B X)

theorem not_contains_of_not_mem {X : List Nat} {v : Nat} (h : v ∉ X) :
    (!X.contains v) = true := by
  cases hc : X.contains v with
  | false => rfl
  | true => exact absurd (List.contains_iff_mem.mp hc) h

theorem exists_inBag_iff (bs : List Bag) (v : Nat) :
    (∃ i, InBag bs i v) ↔ ∃ B ∈ bs, v ∈ B := by
  constructor
  · rintro ⟨i, hi⟩
    unfold InBag at hi
    obtain ⟨B, hB, hv⟩ := hi
    exact ⟨B, List.mem_of_getElem? hB, hv⟩
  · rintro ⟨B, hB, hv⟩
    obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp hB
    exact ⟨i, by unfold InBag; exact ⟨B, hi, hv⟩⟩

theorem inBag_append (A B : List Bag) (i v : Nat) :
    InBag (A ++ B) i v ↔
      (i < A.length ∧ InBag A i v) ∨ (A.length ≤ i ∧ InBag B (i - A.length) v) := by
  unfold InBag
  by_cases h : i < A.length
  · rw [List.getElem?_append_left h]
    constructor
    · rintro ⟨C, hC, hv⟩
      exact Or.inl ⟨h, C, hC, hv⟩
    · rintro (⟨_, hA⟩ | ⟨h', _⟩)
      · exact hA
      · omega
  · rw [List.getElem?_append_right (by omega)]
    constructor
    · rintro ⟨C, hC, hv⟩
      exact Or.inr ⟨by omega, C, hC, hv⟩
    · rintro (⟨h', _⟩ | ⟨_, hB⟩)
      · omega
      · exact hB

theorem inBag_map_bagUnion (bs : List Bag) (X : Bag) (v : Nat) (hv : v ∉ X) (i : Nat) :
    InBag (bs.map (fun B => bagUnion B X)) i v ↔ InBag bs i v := by
  unfold InBag
  rw [List.getElem?_map]
  constructor
  · rintro ⟨C, hC, hvC⟩
    rcases Option.eq_none_or_eq_some (bs[i]?) with hn | ⟨B, hB⟩
    · rw [hn] at hC
      simp at hC
    · rw [hB] at hC
      have hCB : bagUnion B X = C := Option.some.inj hC
      refine ⟨B, hB, ?_⟩
      rw [← hCB] at hvC
      simp only [bagUnion, List.mem_append] at hvC
      exact hvC.resolve_right hv
  · rintro ⟨C, hC, hvC⟩
    refine ⟨bagUnion C X, by simp [hC], ?_⟩
    simp only [bagUnion, List.mem_append]
    exact Or.inl hvC

theorem convV_nil (v : Nat) : ConvV [] v := by
  unfold ConvV
  intro i j k _ _ hi _
  unfold InBag at hi
  obtain ⟨B, hB, _⟩ := hi
  simp at hB

theorem convV_all (bs : List Bag) (v : Nat) (h : ∀ B ∈ bs, v ∈ B) : ConvV bs v := by
  unfold ConvV
  intro i j k hij hjk _ hk
  unfold InBag at hk ⊢
  obtain ⟨B, hB, _⟩ := hk
  obtain ⟨hlt, _⟩ := List.getElem?_eq_some_iff.mp hB
  exact ⟨bs[j], List.getElem?_eq_getElem (by omega), h _ (List.getElem_mem (by omega))⟩

theorem convV_append (A B : List Bag) (v : Nat) (hA : ConvV A v) (hB : ConvV B v)
    (h : ¬ ((∃ C ∈ A, v ∈ C) ∧ (∃ C ∈ B, v ∈ C))) : ConvV (A ++ B) v := by
  unfold ConvV
  intro i j k hij hjk hi hk
  rw [inBag_append] at hi hk ⊢
  rcases hi with ⟨hiA, hiA'⟩ | ⟨hiB, hiB'⟩ <;>
    rcases hk with ⟨hkA, hkA'⟩ | ⟨hkB, hkB'⟩
  · exact Or.inl ⟨by omega, hA i j k hij hjk hiA' hkA'⟩
  · exact absurd ⟨(exists_inBag_iff A v).mp ⟨i, hiA'⟩,
      (exists_inBag_iff B v).mp ⟨k - A.length, hkB'⟩⟩ h
  · omega
  · exact Or.inr ⟨by omega, hB (i - A.length) (j - A.length) (k - A.length)
      (by omega) (by omega) hiB' hkB'⟩

theorem convV_flatMap (X : Bag) (v : Nat) :
    ∀ parts : List (List Nat × List Bag),
      (parts.map (fun x => x.1)).flatten.Nodup →
      (∀ p ∈ parts, (∃ C ∈ p.2.map (fun B => bagUnion B X), v ∈ C) → v ∈ p.1) →
      (∀ p ∈ parts, ConvV (p.2.map (fun B => bagUnion B X)) v) →
      ConvV (parts.flatMap fun p => p.2.map (fun B => bagUnion B X)) v := by
  intro parts
  induction parts with
  | nil =>
    intro _ _ _
    rw [List.flatMap_nil]
    exact convV_nil v
  | cons p rest ih =>
    intro hnd hocc hconv
    rw [List.flatMap_cons]
    have hnd' : (p.1 ++ (rest.map (fun x => x.1)).flatten).Nodup := by
      simpa only [List.map_cons, List.flatten_cons] using hnd
    obtain ⟨-, hrest, hdisj⟩ := List.nodup_append.mp hnd'
    refine convV_append _ _ v (hconv p (by simp)) ?_ ?_
    · exact ih hrest (fun q hq => hocc q (by simp [hq])) (fun q hq => hconv q (by simp [hq]))
    · rintro ⟨⟨C, hC, hvC⟩, ⟨D, hD, hvD⟩⟩
      obtain ⟨q, hq, hDq⟩ := List.mem_flatMap.mp hD
      have hvp : v ∈ p.1 := hocc p (by simp) ⟨C, hC, hvC⟩
      have hvq : v ∈ q.1 := hocc q (by simp [hq]) ⟨D, hDq, hvD⟩
      exact hdisj v hvp v (List.mem_flatten.mpr ⟨q.1, List.mem_map.mpr ⟨q, hq, rfl⟩, hvq⟩) rfl

theorem cover_part (H : Graph) (v : Nat) (hInd : InducedSpec) (hH : H.WF)
    (p : List Nat × List Bag)
    (hp : ValidPD (H.induced p.1.contains) p.2 ∧ BagsWithin (H.induced p.1.contains) p.2)
    (hvH : v ∈ H.nodes) (hvp : v ∈ p.1) : ∃ B ∈ p.2, v ∈ B := by
  obtain ⟨⟨hcov, -, -⟩, -⟩ := hp
  obtain ⟨i, hi⟩ := hcov v
    (((hInd H p.1.contains hH).2.1 v).mpr ⟨hvH, List.contains_iff_mem.mpr hvp⟩)
  exact (exists_inBag_iff p.2 v).mp ⟨i, hi⟩

theorem edge_part (H : Graph) (hInd : InducedSpec) (hH : H.WF)
    (p : List Nat × List Bag)
    (hp : ValidPD (H.induced p.1.contains) p.2 ∧ BagsWithin (H.induced p.1.contains) p.2)
    (u v : Nat) (huH : u ∈ H.nodes) (huv : H.Adj u v) (hu : u ∈ p.1) (hv : v ∈ p.1) :
    ∃ B ∈ p.2, u ∈ B ∧ v ∈ B := by
  obtain ⟨⟨-, -, hedge⟩, -⟩ := hp
  have hadj := ((hInd H p.1.contains hH).2.2 u v).mpr
    ⟨huv, List.contains_iff_mem.mpr hu, List.contains_iff_mem.mpr hv⟩
  have hnu := ((hInd H p.1.contains hH).2.1 u).mpr ⟨huH, List.contains_iff_mem.mpr hu⟩
  exact hedge u v hnu hadj

theorem occ_part (H : Graph) (X : Bag) (v : Nat) (hvX : v ∉ X) (hInd : InducedSpec)
    (hH : H.WF) (p : List Nat × List Bag)
    (hbw : BagsWithin (H.induced p.1.contains) p.2) :
    (∃ C ∈ p.2.map (fun B => bagUnion B X), v ∈ C) → v ∈ p.1 := by
  rintro ⟨C, hC, hvC⟩
  obtain ⟨B, hB, rfl⟩ := List.mem_map.mp hC
  simp only [bagUnion, List.mem_append] at hvC
  rcases hvC with h | h
  · have h2 := ((hInd H p.1.contains hH).2.1 v).mp (hbw B hB v h)
    exact List.contains_iff_mem.mp h2.2
  · exact absurd h hvX

theorem conv_part (H : Graph) (X : Bag) (v : Nat) (hvX : v ∉ X) (hvH : v ∈ H.nodes)
    (hInd : InducedSpec) (hH : H.WF) (p : List Nat × List Bag)
    (hp : ValidPD (H.induced p.1.contains) p.2 ∧ BagsWithin (H.induced p.1.contains) p.2) :
    ConvV (p.2.map (fun B => bagUnion B X)) v := by
  obtain ⟨⟨-, hconv, -⟩, hbw⟩ := hp
  unfold ConvV
  by_cases hvp : v ∈ p.1
  · intro i j k hij hjk hi hk
    have hmem : v ∈ (H.induced p.1.contains).nodes :=
      ((hInd H p.1.contains hH).2.1 v).mpr ⟨hvH, List.contains_iff_mem.mpr hvp⟩
    exact (inBag_map_bagUnion p.2 X v hvX j).mpr
      (hconv v hmem i j k hij hjk ((inBag_map_bagUnion p.2 X v hvX i).mp hi)
        ((inBag_map_bagUnion p.2 X v hvX k).mp hk))
  · intro i j k _ _ hi _
    exact absurd (occ_part H X v hvX hInd hH p hbw ((exists_inBag_iff _ v).mp ⟨i, hi⟩)) hvp

theorem glue_core (hWF : WFBasics) (hInd : InducedSpec) (H : Graph) (X : List Nat)
    (parts : List (List Nat × List Bag))
    (hH : H.WF) (hX : ∀ x ∈ X, x ∈ H.nodes)
    (hperm : (parts.map (fun x => x.1)).flatten.Perm (H.nodes.filter fun v => !X.contains v))
    (hclosed : ∀ p ∈ parts, ∀ x ∈ p.1, ∀ y, H.Adj x y → y ∈ p.1 ∨ y ∈ X)
    (hparts : ∀ p ∈ parts,
      ValidPD (H.induced p.1.contains) p.2 ∧ BagsWithin (H.induced p.1.contains) p.2) :
    ValidPD H (if (outOf parts X).isEmpty then [X] else outOf parts X) ∧
      BagsWithin H (if (outOf parts X).isEmpty then [X] else outOf parts X) := by
  have hflatNd : (parts.map (fun x => x.1)).flatten.Nodup :=
    hperm.nodup_iff.mpr (hH.nodup.filter _)
  -- every vertex of `H` outside `X` lies in some part
  have hcoverV : ∀ v ∈ H.nodes, v ∉ X → ∃ p ∈ parts, v ∈ p.1 := by
    intro v hv hvX
    have h : v ∈ (parts.map (fun x => x.1)).flatten := by
      rw [hperm.mem_iff, List.mem_filter]
      exact ⟨hv, not_contains_of_not_mem hvX⟩
    obtain ⟨l, hl, hvl⟩ := List.mem_flatten.mp h
    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hl
    exact ⟨p, hp, hvl⟩
  have hmemOut : ∀ p ∈ parts, ∀ B ∈ p.2, bagUnion B X ∈ outOf parts X := by
    intro p hp B hB
    exact List.mem_flatMap.mpr ⟨p, hp, List.mem_map.mpr ⟨B, hB, rfl⟩⟩
  have hallX : ∀ B ∈ outOf parts X, ∀ x ∈ X, x ∈ B := by
    intro B hB x hx
    obtain ⟨p, -, hB'⟩ := List.mem_flatMap.mp hB
    obtain ⟨B', -, rfl⟩ := List.mem_map.mp hB'
    simp only [bagUnion, List.mem_append]
    exact Or.inr hx
  have hBWout : ∀ B ∈ outOf parts X, ∀ v ∈ B, v ∈ H.nodes := by
    intro B hB v hv
    obtain ⟨p, hp, hB'⟩ := List.mem_flatMap.mp hB
    obtain ⟨B', hB'', rfl⟩ := List.mem_map.mp hB'
    simp only [bagUnion, List.mem_append] at hv
    rcases hv with h | h
    · have h2 := ((hInd H p.1.contains hH).2.1 v).mp ((hparts p hp).2 B' hB'' v h)
      exact h2.1
    · exact hX v h
  have hcoverOut : ∀ v ∈ H.nodes, v ∉ X → ∃ B ∈ outOf parts X, v ∈ B := by
    intro v hv hvX
    obtain ⟨p, hp, hvp⟩ := hcoverV v hv hvX
    obtain ⟨B', hB', hvB'⟩ := cover_part H v hInd hH p (hparts p hp) hv hvp
    refine ⟨bagUnion B' X, hmemOut p hp B' hB', ?_⟩
    simp only [bagUnion, List.mem_append]
    exact Or.inl hvB'
  by_cases hE : outOf parts X = []
  · -- no bag from the parts: the parts are empty, so `H.nodes ⊆ X`
    have hres : (if (outOf parts X).isEmpty then [X] else outOf parts X) = [X] := by
      simp [hE]
    rw [hres]
    have hall : ∀ v ∈ H.nodes, v ∈ X := by
      intro v hv
      by_contra hvX
      obtain ⟨B, hB, -⟩ := hcoverOut v hv hvX
      rw [hE] at hB
      simp at hB
    unfold ValidPD BagsWithin
    refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
    · intro v hv
      exact (exists_inBag_iff [X] v).mpr ⟨X, List.mem_singleton_self X, hall v hv⟩
    · intro v hv
      exact convV_all [X] v (fun B hB => by rw [List.mem_singleton.mp hB]; exact hall v hv)
    · intro u v hu huv
      exact ⟨X, List.mem_singleton_self X, hall u hu, hall v (hWF H hH u v huv).2.1⟩
    · intro B hB v hv
      rw [List.mem_singleton.mp hB] at hv
      exact hX v hv
  · -- some bag comes from a part; the result is `outOf parts X`
    have hres : (if (outOf parts X).isEmpty then [X] else outOf parts X) = outOf parts X := by
      have hne : (outOf parts X).isEmpty = false := by
        cases h : (outOf parts X).isEmpty
        · rfl
        · exact absurd (List.isEmpty_iff.mp h) hE
      simp only [hne]
      rfl
    rw [hres]
    obtain ⟨B0, hB0⟩ := List.exists_mem_of_ne_nil _ hE
    unfold ValidPD BagsWithin
    refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
    · intro v hv
      refine (exists_inBag_iff _ v).mpr ?_
      by_cases hvX : v ∈ X
      · exact ⟨B0, hB0, hallX B0 hB0 v hvX⟩
      · exact hcoverOut v hv hvX
    · intro v hv
      by_cases hvX : v ∈ X
      · exact convV_all _ v (fun B hB => hallX B hB v hvX)
      · exact convV_flatMap X v parts hflatNd
          (fun p hp => occ_part H X v hvX hInd hH p (hparts p hp).2)
          (fun p hp => conv_part H X v hvX hv hInd hH p (hparts p hp))
    · intro u v hu huv
      obtain ⟨hu', hv', -, -⟩ := hWF H hH u v huv
      by_cases huX : u ∈ X <;> by_cases hvX : v ∈ X
      · exact ⟨B0, hB0, hallX B0 hB0 u huX, hallX B0 hB0 v hvX⟩
      · obtain ⟨p, hp, hvp⟩ := hcoverV v hv' hvX
        obtain ⟨B', hB', hvB'⟩ := cover_part H v hInd hH p (hparts p hp) hv' hvp
        refine ⟨bagUnion B' X, hmemOut p hp B' hB', ?_, ?_⟩
        · simp only [bagUnion, List.mem_append]
          exact Or.inr huX
        · simp only [bagUnion, List.mem_append]
          exact Or.inl hvB'
      · obtain ⟨p, hp, hup⟩ := hcoverV u hu' huX
        obtain ⟨B', hB', huB'⟩ := cover_part H u hInd hH p (hparts p hp) hu' hup
        refine ⟨bagUnion B' X, hmemOut p hp B' hB', ?_, ?_⟩
        · simp only [bagUnion, List.mem_append]
          exact Or.inl huB'
        · simp only [bagUnion, List.mem_append]
          exact Or.inr hvX
      · obtain ⟨p, hp, hup⟩ := hcoverV u hu' huX
        have hvp : v ∈ p.1 := (hclosed p hp u hup v huv).resolve_right hvX
        obtain ⟨B', hB', huB', hvB'⟩ :=
          edge_part H hInd hH p (hparts p hp) u v hu' huv hup hvp
        refine ⟨bagUnion B' X, hmemOut p hp B' hB', ?_, ?_⟩
        · simp only [bagUnion, List.mem_append]
          exact Or.inl huB'
        · simp only [bagUnion, List.mem_append]
          exact Or.inl hvB'
    · intro B hB v hv
      exact hBWout B hB v hv

end G8

/-- Gluing at a separator `X` (the shape of `pd_tw2`). -/
theorem separatorGlueValid_of (hWF : WFBasics) (hInd : InducedSpec) : SeparatorGlueValid := by
  intro H X parts hH hX hperm hclosed hparts
  exact G8.glue_core hWF hInd H X parts hH hX hperm hclosed hparts

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.separatorGlueValid_of