CubicPathwidth.Alg.Proofs2.U1PdTw2Width

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

import CubicPathwidth.Alg.Spec2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# U1: width of `pd_tw2` (`PdTw2Width`)

Induction on the fuel, generalizing the graph. Cases:
* `N = 0`: no bags. `N ≤ 3`: the single bag `H.nodes` has `N ≤ 3 ⌊log₂ N⌋ + 1` vertices.
* `N ≥ 4`, fuel `f + 1`, flag `false`: the reduction reached the empty graph, the
  elimination bag `X = v :: nb` is found, every component `c` of `H[V \ X]` satisfies
  `2|c| ≤ N`, and every recursive call has flag `false`. An elimination bag has
  `|X| ≤ 3` (only nodes of degree `≤ 2` are recorded, so `|nb| ≤ 2`). For a component
  `c`, `H[c]` has `|c|` nodes and `log₂|c| + 1 ≤ log₂ N` (from `2|c| ≤ N`), so each
  output bag `B ++ X` has size `≤ 3 log₂|c| + 4 ≤ 3 log₂ N + 1`. If the output is
  empty the single bag `X` has size `≤ 3`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace U1

/-- Every recorded reduction of `reduceLoop` has at most two neighbours. -/
theorem reduceLoop_red_len : ∀ (fuel : Nat) (G : Graph) (stack : List Nat) (opsRev : List Op),
    (∀ o ∈ opsRev, ∀ v nb, o = Op.red v nb → nb.length ≤ 2) →
    ∀ o ∈ (reduceLoop fuel G stack opsRev).2.1, ∀ v nb, o = Op.red v nb → nb.length ≤ 2
  | fuel, G, [], opsRev, h => by
    intro o ho v nb hov
    have e : (reduceLoop fuel G [] opsRev).2.1 = opsRev.reverse := by
      cases fuel <;> simp [reduceLoop]
    rw [e] at ho
    exact h o (List.mem_reverse.1 ho) v nb hov
  | 0, G, v :: rest, opsRev, h => by
    intro o ho v' nb hov
    have e : (reduceLoop 0 G (v :: rest) opsRev).2.1 = opsRev.reverse := by
      simp [reduceLoop]
    rw [e] at ho
    exact h o (List.mem_reverse.1 ho) v' nb hov
  | fuel + 1, G, v :: rest, opsRev, h => by
    unfold reduceLoop
    split
    · exact reduceLoop_red_len fuel G rest opsRev h
    · rename_i hv
      refine reduceLoop_red_len fuel _ _ _ ?_
      intro o ho v' nb hov
      rcases List.mem_cons.1 ho with rfl | ho
      · obtain ⟨rfl, rfl⟩ := Op.red.inj hov
        have hd : G.degree v ≤ 2 := by
          by_contra hc
          exact hv (by simp [show 2 < G.degree v by omega])
        exact hd
      · exact h o ho v' nb hov

/-- The elimination bags of `reduceRecordF` have at most `3` elements. -/
theorem reduceRecordF_bag_card (G : Graph) (X : Bag)
    (hX : X ∈ elimBags (reduceRecordF G).2.1) : X.toFinset.card ≤ 3 := by
  unfold elimBags at hX
  rw [List.mem_filterMap] at hX
  obtain ⟨o, ho, hXo⟩ := hX
  cases o with
  | del w => simp at hXo
  | red v nb =>
    simp only [Option.some.injEq] at hXo
    subst hXo
    have hlen : nb.length ≤ 2 := by
      unfold reduceRecordF at ho
      exact reduceLoop_red_len _ _ _ [] (by simp) _ ho v nb rfl
    have h1 : (v :: nb).toFinset.card ≤ (v :: nb).length := List.toFinset_card_le _
    simp only [List.length_cons] at h1
    omega

/-- `maxBagCard` is at most `K` as soon as every bag has at most `K` elements. -/
theorem maxBagCard_le_of (bags : List Bag) (K : Nat) (h : ∀ B ∈ bags, B.toFinset.card ≤ K) :
    maxBagCard bags ≤ K := by
  induction bags with
  | nil => simp [maxBagCard]
  | cons B bs ih =>
    have hB : B.toFinset.card ≤ K := h B (List.mem_cons_self)
    have hbs : maxBagCard bs ≤ K := ih fun B' hB' => h B' (List.mem_cons_of_mem _ hB')
    show max B.toFinset.card (maxBagCard bs) ≤ K
    exact max_le hB hbs

/-- Each bag is at most `maxBagCard`. -/
theorem card_le_maxBagCard (bags : List Bag) (B : Bag) (hB : B ∈ bags) :
    B.toFinset.card ≤ maxBagCard bags := by
  induction bags with
  | nil => simp at hB
  | cons B' bs ih =>
    show B.toFinset.card ≤ max B'.toFinset.card (maxBagCard bs)
    rcases List.mem_cons.1 hB with rfl | hB
    · exact le_max_left _ _
    · exact le_trans (ih hB) (le_max_right _ _)

/-- The logarithm step: `2m ≤ N` and `2 ≤ N` give `log₂ m + 1 ≤ log₂ N`. -/
theorem log_half (m N : Nat) (hN : 2 ≤ N) (hm : 2 * m ≤ N) :
    Nat.log 2 m + 1 ≤ Nat.log 2 N := by
  by_cases h0 : m = 0
  · subst h0
    have := Nat.log_pos (b := 2) (n := N) (by norm_num) hN
    simp only [Nat.log_zero_right]
    omega
  · have e : Nat.log 2 (m * 2) = Nat.log 2 m + 1 :=
      Nat.log_mul_base (by norm_num) h0
    have hmono : Nat.log 2 (m * 2) ≤ Nat.log 2 N :=
      Nat.log_mono_right (by omega)
    omega

/-- A single bag of at most three nodes. -/
theorem le_three_log (N : Nat) (hN : N ≤ 3) : N ≤ 3 * Nat.log 2 N + 1 := by
  by_cases h1 : N ≤ 1
  · omega
  · have := Nat.log_pos (b := 2) (n := N) (by norm_num) (by omega)
    omega

/-- The single bag `[H.nodes]` of a graph with at most three nodes. -/
theorem single_bound (H : Graph) (hH : H.WF) (h3 : H.numNodes ≤ 3) :
    maxBagCard [H.nodes] ≤ 3 * Nat.log 2 H.numNodes + 1 := by
  have hc : maxBagCard [H.nodes] = H.numNodes := by
    unfold maxBagCard
    simp only [List.map_cons, List.map_nil, List.foldr_cons, List.foldr_nil]
    rw [List.toFinset_card_of_nodup hH.nodup]
    unfold numNodes
    omega
  rw [hc]
  exact le_three_log _ h3

/-- The node count of an induced subgraph on a component: `|H[c]| = |c|`. -/
theorem numNodes_induced_comp (H : Graph) (hH : H.WF) (X : Bag) (c : List Nat)
    (hc : c ∈ (H.induced fun v => !X.contains v).components) :
    (H.induced c.contains).numNodes = c.length := by
  have hK := inducedSpec H (fun v => !X.contains v) hH
  have hcs := componentsSpec _ hK.1
  have hflat := hcs.1
  have hcSub : ∀ x ∈ c, x ∈ H.nodes := by
    intro x hx
    have hx' : x ∈ (H.induced fun v => !X.contains v).nodes :=
      hflat.mem_iff.1 (List.mem_flatten.2 ⟨c, hc, hx⟩)
    exact ((hK.2.1 x).1 hx').1
  have hcNodup : c.Nodup := by
    have hn := (List.nodup_flatten.1 (hflat.nodup_iff.2 hK.1.nodup)).1 c hc
    exact hn
  have hI := inducedSpec H c.contains hH
  have hperm : (H.induced c.contains).nodes.Perm c := by
    rw [List.perm_ext_iff_of_nodup hI.1.nodup hcNodup]
    intro x
    rw [hI.2.1 x]
    constructor
    · intro hx
      simpa using hx.2
    · intro hx
      exact ⟨hcSub x hx, by simpa using hx⟩
  unfold numNodes
  exact hperm.length_eq

/-- Every output bag of the gluing step has at most `3 log₂ N + 1` elements. -/
theorem out_card (H : Graph) (hH : H.WF) (f : Nat) (X : Bag)
    (hX3 : X.toFinset.card ≤ 3) (hN : 4 ≤ H.numNodes)
    (hsz : ∀ c ∈ (H.induced fun v => !X.contains v).components, 2 * c.length ≤ H.numNodes)
    (hfl : ∀ c ∈ (H.induced fun v => !X.contains v).components,
      (pdTw2Fuel f (H.induced c.contains)).2 = false)
    (ih : ∀ K : Graph, K.WF → (pdTw2Fuel f K).2 = false →
      maxBagCard (pdTw2Fuel f K).1 ≤ 3 * Nat.log 2 K.numNodes + 1)
    (B : Bag)
    (hB : B ∈ (((H.induced fun v => !X.contains v).components.map
      fun c => pdTw2Fuel f (H.induced c.contains)).flatMap
        fun p => p.1.map fun B => bagUnion B X)) :
    B.toFinset.card ≤ 3 * Nat.log 2 H.numNodes + 1 := by
  rw [List.mem_flatMap] at hB
  obtain ⟨p, hp, hBp⟩ := hB
  rw [List.mem_map] at hp
  obtain ⟨c, hc, rfl⟩ := hp
  rw [List.mem_map] at hBp
  obtain ⟨B0, hB0, rfl⟩ := hBp
  have hnum := numNodes_induced_comp H hH X c hc
  have hih := ih (H.induced c.contains) (inducedSpec H _ hH).1 (hfl c hc)
  have hB0le : B0.toFinset.card ≤ 3 * Nat.log 2 (H.induced c.contains).numNodes + 1 :=
    le_trans (card_le_maxBagCard _ B0 hB0) hih
  rw [hnum] at hB0le
  have hlog := log_half c.length H.numNodes (by omega) (hsz c hc)
  show (B0 ++ X).toFinset.card ≤ _
  rw [List.toFinset_append]
  have := Finset.card_union_le B0.toFinset X.toFinset
  omega

/-- Main induction on the fuel. -/
theorem main_fuel (fuel : Nat) : ∀ H : Graph, H.WF → (pdTw2Fuel fuel H).2 = false →
    maxBagCard (pdTw2Fuel fuel H).1 ≤ 3 * Nat.log 2 H.numNodes + 1 := by
  induction fuel with
  | zero =>
    intro H hH hfl
    by_cases h0 : H.numNodes = 0
    · have e : pdTw2Fuel 0 H = ([], false) := by
        unfold pdTw2Fuel
        rw [if_pos h0]
      rw [e]
      simp [maxBagCard]
    by_cases h3 : H.numNodes ≤ 3
    · have e : pdTw2Fuel 0 H = ([H.nodes], false) := by
        unfold pdTw2Fuel
        rw [if_neg h0, if_pos h3]
      rw [e]
      exact single_bound H hH h3
    · have e : pdTw2Fuel 0 H = ([H.nodes], true) := by
        unfold pdTw2Fuel
        rw [if_neg h0, if_neg h3]
      rw [e] at hfl
      exact absurd hfl (by simp)
  | succ f ih =>
    intro H hH hfl
    by_cases h0 : H.numNodes = 0
    · have e : pdTw2Fuel (f + 1) H = ([], false) := by
        unfold pdTw2Fuel
        rw [if_pos h0]
      rw [e]
      simp [maxBagCard]
    by_cases h3 : H.numNodes ≤ 3
    · have e : pdTw2Fuel (f + 1) H = ([H.nodes], false) := by
        unfold pdTw2Fuel
        rw [if_neg h0, if_pos h3]
      rw [e]
      exact single_bound H hH h3
    have hN : 4 ≤ H.numNodes := by omega
    rcases hres : pdTw2Fuel (f + 1) H with ⟨out, fl⟩
    rw [hres] at hfl
    dsimp only at hfl
    unfold pdTw2Fuel at hres
    rw [if_neg h0, if_neg h3] at hres
    dsimp only at hres
    split at hres
    · -- the reduction does not reach the empty graph: flag true
      simp only [Prod.mk.injEq] at hres
      obtain ⟨-, rfl⟩ := hres
      exact absurd hfl (by simp)
    · split at hres
      · -- no balanced bag: flag true
        simp only [Prod.mk.injEq] at hres
        obtain ⟨-, rfl⟩ := hres
        exact absurd hfl (by simp)
      · rename_i X hfind
        have hXm := List.mem_of_find?_eq_some hfind
        have hXp := List.find?_some hfind
        have hsz : ∀ c ∈ (H.induced fun v => !X.contains v).components,
            2 * c.length ≤ H.numNodes := by
          intro c hc
          have := List.all_eq_true.1 hXp c hc
          simpa using this
        have hX3 := reduceRecordF_bag_card H.copy X hXm
        simp only [Prod.mk.injEq] at hres
        obtain ⟨hout, hfl'⟩ := hres
        rw [← hfl'] at hfl
        simp only [Bool.or_eq_false_iff] at hfl
        have hpart : ∀ c ∈ (H.induced fun v => !X.contains v).components,
            (pdTw2Fuel f (H.induced c.contains)).2 = false := by
          intro c hc
          have := List.any_eq_false.1 hfl.2 _ (List.mem_map_of_mem hc)
          simpa using this
        subst hout
        dsimp only
        split_ifs with hem
        · apply maxBagCard_le_of
          intro B hB
          simp only [List.mem_singleton] at hB
          subst hB
          have := Nat.log_pos (b := 2) (n := H.numNodes) (by norm_num) (by omega)
          omega
        · exact maxBagCard_le_of _ _ (fun B hB =>
            out_card H hH f X hX3 hN hsz hpart ih B hB)

end U1

/-- Theorem `PdTw2Width` (`pd_tw2` width bound). -/
theorem pdTw2Width : PdTw2Width := by
  intro fuel H hH hfl
  exact U1.main_fuel fuel H hH hfl

#print axioms CubicPathwidth.Alg.pdTw2Width

end CubicPathwidth.Alg