CubicPathwidth.Alg.Proofs.T1AppendIsolated

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

import CubicPathwidth.Alg.Spec

/-!
# T1: appending one bag per isolated vertex

Proves `AppendIsolatedValid` from `WFBasics` and `InducedSpec`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace T1

/-- The isolated vertices of `G` in node order: the list behind `isolatedBags G`. -/
def isoList (G : Graph) : List Nat := G.nodes.filter fun v => G.degree v == 0

theorem isolatedBags_eq (G : Graph) :
    isolatedBags G = (isoList G).map fun v => [v] := rfl

theorem mem_isoList {G : Graph} {v : Nat} (h : v ∈ isoList G) :
    v ∈ G.nodes ∧ G.degree v = 0 := by
  unfold isoList at h
  rw [List.mem_filter] at h
  exact ⟨h.1, by simpa using h.2⟩

theorem mem_isoList_of {G : Graph} {v : Nat} (hv : v ∈ G.nodes) (hd : G.degree v = 0) :
    v ∈ isoList G := by
  unfold isoList
  rw [List.mem_filter]
  exact ⟨hv, by simpa using hd⟩

theorem isoList_nodup {G : Graph} (hG : G.WF) : (isoList G).Nodup :=
  List.Nodup.filter _ hG.nodup

/-- Index uniqueness in a duplicate-free list. -/
theorem getElem?_inj_of_nodup {l : List Nat} (h : l.Nodup) {i j v : Nat}
    (hi : l[i]? = some v) (hj : l[j]? = some v) : i = j := by
  rcases List.getElem?_eq_some_iff.mp hi with ⟨hi1, hi2⟩
  rcases List.getElem?_eq_some_iff.mp hj with ⟨hj1, hj2⟩
  exact (List.Nodup.getElem_inj_iff h).mp (hi2.trans hj2.symm)

/-- A bag at an index of `bags` stays a bag at that index of `bags ++ B`. -/
theorem inBag_append_left {bags B : List Bag} {i v : Nat} (h : InBag bags i v) :
    InBag (bags ++ B) i v := by
  obtain ⟨C, hC, hv⟩ := h
  rcases List.getElem?_eq_some_iff.mp hC with ⟨hlt, _⟩
  refine ⟨C, ?_, hv⟩
  rw [List.getElem?_append_left hlt]
  exact hC

/-- Index decomposition of membership in `bags ++ isolatedBags G`. -/
theorem inBag_append_iso_cases {G : Graph} {bags : List Bag} {i v : Nat}
    (h : InBag (bags ++ isolatedBags G) i v) :
    (i < bags.length ∧ InBag bags i v) ∨
      (∃ q, i = bags.length + q ∧ (isoList G)[q]? = some v) := by
  obtain ⟨B, hB, hv⟩ := h
  by_cases hlt : i < bags.length
  · left
    refine ⟨hlt, ?_⟩
    refine ⟨B, ?_, hv⟩
    rw [List.getElem?_append_left hlt] at hB
    exact hB
  · right
    have hlt' : bags.length ≤ i := Nat.le_of_not_lt hlt
    refine ⟨i - bags.length, by omega, ?_⟩
    rw [List.getElem?_append_right hlt', isolatedBags_eq, List.getElem?_map] at hB
    cases hq : (isoList G)[i - bags.length]? with
    | none => rw [hq] at hB; simp at hB
    | some w =>
      rw [hq] at hB
      simp only [Option.map_some, Option.some.injEq] at hB
      subst hB
      simp at hv
      exact congrArg some hv.symm

/-- The isolated vertex `v` lies in the bag `[v]` at index `bags.length + q`. -/
theorem inBag_iso_of {G : Graph} {bags : List Bag} {q v : Nat}
    (h : (isoList G)[q]? = some v) : InBag (bags ++ isolatedBags G) (bags.length + q) v := by
  refine ⟨[v], ?_, by simp⟩
  rw [List.getElem?_append_right (by omega), Nat.add_sub_cancel_left, isolatedBags_eq,
    List.getElem?_map, h]
  rfl

end T1

open T1

/-- Appending one bag per isolated vertex extends a decomposition of `nonIsolated G`
to one of `G`. -/
theorem appendIsolatedValid_of (hWF : WFBasics) (hInd : InducedSpec) : AppendIsolatedValid := by
  intro G hG bags hV hBW
  have hI := hInd G (fun v => G.degree v != 0) hG
  have hNodes : ∀ x, x ∈ (nonIsolated G).nodes ↔ x ∈ G.nodes ∧ G.degree x ≠ 0 := by
    intro x
    unfold nonIsolated
    rw [hI.2.1 x]
    simp
  have hAdj : ∀ x y, (nonIsolated G).Adj x y ↔ G.Adj x y ∧ G.degree x ≠ 0 ∧ G.degree y ≠ 0 := by
    intro x y
    unfold nonIsolated
    rw [hI.2.2 x y]
    simp
  have hnoBag : ∀ B ∈ bags, ∀ v ∈ B, G.degree v ≠ 0 := fun B hB' v hvB =>
    ((hNodes v).mp (hBW B hB' v hvB)).2
  -- an index of `bags ++ isolatedBags G` holding an isolated vertex is an isolated index
  have hisoIdx : ∀ {m v : Nat}, G.degree v = 0 → InBag (bags ++ isolatedBags G) m v →
      ∃ q, m = bags.length + q ∧ (isoList G)[q]? = some v := by
    intro m v hd h
    rcases inBag_append_iso_cases h with ⟨_, h'⟩ | h'
    · obtain ⟨B, hB', hvB⟩ := h'
      exact absurd hd (hnoBag B (List.mem_of_getElem? hB') v hvB)
    · exact h'
  refine ⟨?_, ?_, ?_⟩
  · intro v hv
    by_cases hd : G.degree v = 0
    · obtain ⟨q, hq⟩ := List.mem_iff_getElem?.mp (mem_isoList_of hv hd)
      exact ⟨_, inBag_iso_of hq⟩
    · obtain ⟨i, hi⟩ := hV.1 v ((hNodes v).mpr ⟨hv, hd⟩)
      exact ⟨i, inBag_append_left hi⟩
  · intro v hv i j k hij hjk hi hk
    by_cases hd : G.degree v = 0
    · obtain ⟨q1, rfl, h1⟩ := hisoIdx hd hi
      obtain ⟨q2, rfl, h2⟩ := hisoIdx hd hk
      have hq : q1 = q2 := getElem?_inj_of_nodup (isoList_nodup hG) h1 h2
      subst hq
      have hj : j = bags.length + q1 := by omega
      subst hj
      exact hi
    · have hvN : v ∈ (nonIsolated G).nodes := (hNodes v).mpr ⟨hv, hd⟩
      have hbag : ∀ m, InBag (bags ++ isolatedBags G) m v → InBag bags m v := by
        intro m h
        rcases inBag_append_iso_cases h with ⟨_, h'⟩ | ⟨q, _, hq⟩
        · exact h'
        · exact absurd (mem_isoList (List.mem_of_getElem? hq)).2 hd
      exact inBag_append_left (hV.2.1 v hvN i j k hij hjk (hbag i hi) (hbag k hk))
  · intro u v hu huv
    obtain ⟨hu', _, hvu, _⟩ := hWF G hG u v huv
    have hdu : G.degree u ≠ 0 := by
      unfold Graph.degree
      exact Nat.pos_iff_ne_zero.mp (List.length_pos_of_mem huv)
    have hdv : G.degree v ≠ 0 := by
      unfold Graph.degree
      exact Nat.pos_iff_ne_zero.mp (List.length_pos_of_mem hvu)
    obtain ⟨B, hB', hmem⟩ := hV.2.2 u v ((hNodes u).mpr ⟨hu', hdu⟩) ((hAdj u v).mpr ⟨huv, hdu, hdv⟩)
    exact ⟨B, List.mem_append_left _ hB', hmem⟩

#print axioms CubicPathwidth.Alg.appendIsolatedValid_of

end CubicPathwidth.Alg
Back to top