CubicPathwidth.Alg.Proofs.G7Concat

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

import CubicPathwidth.Alg.Spec

/-!
# G7: `ConcatValid`

Concatenating valid decompositions of pairwise vertex-disjoint graphs gives a valid
decomposition of their union. Proof by induction on the list of parts: the bags of the
head part come first, then the bags of the rest. A vertex of the head part lies in no
bag of the rest (disjointness and `BagsWithin`), and a vertex of the rest lies in no bag
of the head part (`BagsWithin`), so each interval property and each edge is inherited
from the head part or from the rest.
-/

noncomputable section

namespace CubicPathwidth.Alg

namespace G7

/-- Bag indices of an append, on the left. -/
theorem inBag_append_left {A B : List Bag} {i v : Nat} (h : i < A.length) :
    InBag (A ++ B) i v ↔ InBag A i v := by
  unfold InBag
  rw [List.getElem?_append_left h]

/-- Bag indices of an append, on the right. -/
theorem inBag_append_right {A B : List Bag} {i v : Nat} (h : A.length ≤ i) :
    InBag (A ++ B) i v ↔ InBag B (i - A.length) v := by
  unfold InBag
  rw [List.getElem?_append_right h]

/-- A bag index of a decomposition is a genuine index. -/
theorem inBag_lt {bags : List Bag} {i v : Nat} (h : InBag bags i v) : i < bags.length := by
  obtain ⟨B, hB, _⟩ := h
  obtain ⟨h1, _⟩ := List.getElem?_eq_some_iff.1 hB
  exact h1

/-- Vertices of bags lie in the graph when the bags are within it. -/
theorem inBag_mem {G : Graph} {bags : List Bag} (hbw : BagsWithin G bags) {i v : Nat}
    (h : InBag bags i v) : v ∈ G.nodes := by
  obtain ⟨B, hB, hvB⟩ := h
  exact hbw B (List.mem_of_getElem? hB) v hvB

/-- Two parts: the head `A` (with bags `BA`) and the union of the rest (with bags `bs`),
the head's vertices being disjoint from the rest. -/
theorem step (hWF : WFBasics) (hU : UnionAllSpec) (A : Graph) (BA : List Bag)
    (gs : List Graph) (bs : List Bag)
    (hA : A.WF ∧ ValidPD A BA ∧ BagsWithin A BA)
    (hgs : ∀ J ∈ gs, J.WF)
    (hdisj : ∀ J ∈ gs, ∀ x ∈ A.nodes, x ∉ J.nodes)
    (hI : ValidPD (Graph.unionAll gs) bs ∧ BagsWithin (Graph.unionAll gs) bs) :
    ValidPD (Graph.unionAll (A :: gs)) (BA ++ bs) ∧
      BagsWithin (Graph.unionAll (A :: gs)) (BA ++ bs) := by
  obtain ⟨hAwf, hAvp, hAbw⟩ := hA
  obtain ⟨hIvp, hIbw⟩ := hI
  have hwf : ∀ J ∈ A :: gs, J.WF := by
    intro J hJ
    rcases List.mem_cons.1 hJ with h | h
    · rw [h]; exact hAwf
    · exact hgs J h
  have hUn := hU (A :: gs) hwf
  have hUg := hU gs hgs
  have hnodes : ∀ x, x ∈ (Graph.unionAll (A :: gs)).nodes ↔
      x ∈ A.nodes ∨ x ∈ (Graph.unionAll gs).nodes := by
    intro x
    rw [hUn.2.1 x, hUg.2.1 x]
    simp
  have hdisj' : ∀ x, x ∈ A.nodes → x ∉ (Graph.unionAll gs).nodes := by
    intro x hxA hxU
    obtain ⟨J, hJ, hxJ⟩ := (hUg.2.1 x).1 hxU
    exact hdisj J hJ x hxA hxJ
  constructor
  · unfold ValidPD
    refine ⟨?_, ?_, ?_⟩
    · -- coverage
      intro v hv
      rcases (hnodes v).1 hv with hvA | hvU
      · obtain ⟨i, hi⟩ := hAvp.1 v hvA
        exact ⟨i, (inBag_append_left (inBag_lt hi)).2 hi⟩
      · obtain ⟨i, hi⟩ := hIvp.1 v hvU
        refine ⟨BA.length + i, ?_⟩
        rw [inBag_append_right (by omega), Nat.add_sub_cancel_left]
        exact hi
    · -- intervals
      intro v hv i j k hij hjk hi hk
      rcases (hnodes v).1 hv with hvA | hvU
      · -- v in the head: it lies in no later bag
        have hlt : ∀ m, InBag (BA ++ bs) m v → m < BA.length := by
          intro m hm
          by_contra hc
          have hc' := Nat.not_lt.mp hc
          rw [inBag_append_right hc'] at hm
          exact hdisj' v hvA (inBag_mem hIbw hm)
        have hi1 := hlt i hi
        have hk1 := hlt k hk
        have hj1 : j < BA.length := by omega
        rw [inBag_append_left hj1]
        exact hAvp.2.1 v hvA i j k hij hjk ((inBag_append_left hi1).1 hi)
          ((inBag_append_left hk1).1 hk)
      · -- v not in the head: it lies in no earlier bag
        have hvnA : v ∉ A.nodes := fun h => hdisj' v h hvU
        have hi1 : BA.length ≤ i := by
          by_contra hc
          exact hvnA (inBag_mem hAbw ((inBag_append_left (Nat.not_le.mp hc)).1 hi))
        have hk1 : BA.length ≤ k := by
          by_contra hc
          exact hvnA (inBag_mem hAbw ((inBag_append_left (Nat.not_le.mp hc)).1 hk))
        rw [inBag_append_right (by omega : BA.length ≤ j)]
        exact hIvp.2.1 v hvU (i - BA.length) (j - BA.length) (k - BA.length)
          (by omega) (by omega) ((inBag_append_right hi1).1 hi)
          ((inBag_append_right hk1).1 hk)
    · -- edges
      intro u v _ hadj
      obtain ⟨J, hJ, hJadj⟩ := (hUn.2.2 u v).1 hadj
      rcases List.mem_cons.1 hJ with hJA | hJg
      · rw [hJA] at hJadj
        obtain ⟨huA, _, _, _⟩ := hWF A hAwf u v hJadj
        obtain ⟨B, hB, hu', hv'⟩ := hAvp.2.2 u v huA hJadj
        exact ⟨B, List.mem_append.2 (Or.inl hB), hu', hv'⟩
      · obtain ⟨huJ, _, _, _⟩ := hWF J (hgs J hJg) u v hJadj
        have huU : u ∈ (Graph.unionAll gs).nodes := (hUg.2.1 u).2 ⟨J, hJg, huJ⟩
        obtain ⟨B, hB, hu', hv'⟩ := hIvp.2.2 u v huU ((hUg.2.2 u v).2 ⟨J, hJg, hJadj⟩)
        exact ⟨B, List.mem_append.2 (Or.inr hB), hu', hv'⟩
  · -- bags lie in the union
    intro B hB v hv
    rcases List.mem_append.1 hB with hB' | hB'
    · exact (hnodes v).2 (Or.inl (hAbw B hB' v hv))
    · exact (hnodes v).2 (Or.inr (hIbw B hB' v hv))

/-- Concatenation over a list of parts (induction on the list). -/
theorem concat_all (hWF : WFBasics) (hU : UnionAllSpec) :
    ∀ parts : List (Graph × List Bag),
      (∀ p ∈ parts, p.1.WF ∧ ValidPD p.1 p.2 ∧ BagsWithin p.1 p.2) →
      parts.Pairwise (fun A B => ∀ x, x ∈ A.1.nodes → x ∉ B.1.nodes) →
      ValidPD (Graph.unionAll (parts.map (·.1))) (parts.flatMap (·.2)) ∧
        BagsWithin (Graph.unionAll (parts.map (·.1))) (parts.flatMap (·.2))
  | [], _, _ => by
    have hE : ∀ x, x ∉ (Graph.unionAll []).nodes := by
      intro x hx
      obtain ⟨J, hJ, _⟩ := ((hU [] (by simp)).2.1 x).1 hx
      simp at hJ
    refine ⟨⟨fun v hv => absurd hv (hE v), fun v hv => absurd hv (hE v),
      fun u _ hu _ => absurd hu (hE u)⟩, ?_⟩
    intro B hB
    simp at hB
  | p :: rest, hp, hpw => by
    obtain ⟨hpwf, hpvp, hpbw⟩ := hp p (List.mem_cons_self)
    have hpw' := List.pairwise_cons.1 hpw
    have ih := concat_all hWF hU rest (fun q hq => hp q (List.mem_cons_of_mem _ hq)) hpw'.2
    have hdisj : ∀ J ∈ rest.map (·.1), ∀ x ∈ p.1.nodes, x ∉ J.nodes := by
      intro J hJ x hx
      obtain ⟨q, hq, rfl⟩ := List.mem_map.1 hJ
      exact hpw'.1 q hq x hx
    have hgs : ∀ J ∈ rest.map (·.1), J.WF := by
      intro J hJ
      obtain ⟨q, hq, rfl⟩ := List.mem_map.1 hJ
      exact (hp q (List.mem_cons_of_mem _ hq)).1
    simp only [List.map_cons, List.flatMap_cons]
    exact step hWF hU p.1 p.2 (rest.map (·.1)) (rest.flatMap (·.2))
      ⟨hpwf, hpvp, hpbw⟩ hgs hdisj ih

end G7

/-- Concatenating decompositions of vertex-disjoint graphs decomposes their union. -/
theorem concatValid_of (hWF : WFBasics) (hU : UnionAllSpec) : ConcatValid := by
  unfold ConcatValid
  intro parts hp hpw
  exact G7.concat_all hWF hU parts hp hpw

#print axioms CubicPathwidth.Alg.concatValid_of

end CubicPathwidth.Alg