import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# Task A3: width of `algo_T4` from `UndoWidth` (`Spec2.lean` §4, `AlgoT4Width`)

`algoT4Width_of` takes the Stage 2 statement `UndoWidth` as hypothesis and proves
`AlgoT4Width`.

Route: `algo_T4 G = bags ++ isolatedBags G`, where `bags` is `undo G0 ops R bagsR` with
`G0 = nonIsolated G`. A fallback-free run has `undo` without fallback, so `UndoWidth`
bounds its width by `|D| + pdWidth bagsR + 3 log₂ |V(G0)| + 1`, and `|D|` is at most
the length of `deletedSet ops`. Each isolated bag is a singleton (width `0`), and the
right-hand side is `≥ 0`. The width of an append is the maximum of the widths.
-/

namespace CubicPathwidth.Alg

open Graph

namespace A3Width

/-- A bag of a list has at most the largest bag size of the list. -/
theorem le_maxBagCard {l : List Bag} {B : Bag} (hB : B ∈ l) :
    B.toFinset.card ≤ maxBagCard l := by
  induction l with
  | nil => simp at hB
  | cons a l ih =>
    unfold maxBagCard at ih ⊢
    simp only [List.map_cons, List.foldr_cons]
    rcases List.mem_cons.1 hB with rfl | hB
    · exact le_max_left _ _
    · exact le_max_of_le_right (ih hB)

/-- A list of bags whose sizes are at most `n` has largest bag size at most `n`. -/
theorem maxBagCard_le {l : List Bag} {n : ℕ} (h : ∀ B ∈ l, B.toFinset.card ≤ n) :
    maxBagCard l ≤ n := by
  induction l with
  | nil => simp [maxBagCard]
  | cons a l ih =>
    unfold maxBagCard at ih ⊢
    simp only [List.map_cons, List.foldr_cons]
    exact max_le (h a List.mem_cons_self)
      (ih fun B hB => h B (List.mem_cons_of_mem _ hB))

/-- The largest bag size of an append is at most the larger of the two. -/
theorem maxBagCard_append_le (A B : List Bag) :
    maxBagCard (A ++ B) ≤ max (maxBagCard A) (maxBagCard B) := by
  apply maxBagCard_le
  intro C hC
  rcases List.mem_append.1 hC with h | h
  · exact le_trans (le_maxBagCard h) (le_max_left _ _)
  · exact le_trans (le_maxBagCard h) (le_max_right _ _)

/-- The width of an append is bounded by any common bound of the two widths. -/
theorem pdWidth_append_le {A B : List Bag} {X : ℝ} (hA : pdWidth A ≤ X)
    (hB : pdWidth B ≤ X) : pdWidth (A ++ B) ≤ X := by
  unfold pdWidth at hA hB ⊢
  have h' : ((maxBagCard (A ++ B) : ℕ) : ℝ) ≤
      max (maxBagCard A : ℝ) (maxBagCard B : ℝ) := by
    exact_mod_cast maxBagCard_append_le A B
  have hm : max (maxBagCard A : ℝ) (maxBagCard B : ℝ) ≤ X + 1 :=
    max_le (by linarith) (by linarith)
  linarith

/-- The width is at least `-1`. -/
theorem neg_one_le_pdWidth (bags : List Bag) : -1 ≤ pdWidth bags := by
  unfold pdWidth
  have : (0 : ℝ) ≤ (maxBagCard bags : ℝ) := Nat.cast_nonneg _
  linarith

/-- Isolated vertices contribute bags of size one, of width `≤ 0`. -/
theorem isolated_width (G : Graph) : pdWidth (isolatedBags G) ≤ 0 := by
  unfold pdWidth
  have h : maxBagCard (isolatedBags G) ≤ 1 := by
    apply maxBagCard_le
    intro B hB
    unfold isolatedBags at hB
    obtain ⟨v, _, rfl⟩ := List.mem_map.1 hB
    simp
  have : (maxBagCard (isolatedBags G) : ℝ) ≤ 1 := by exact_mod_cast h
  linarith

/-- The bound for the bags of `algo_T4` before the isolated vertices are appended. -/
theorem core (h : UndoWidth) (G0 : Graph) (hG0 : G0.WF) (ops : List Op) (R : Graph)
    (bagsR : List Bag) (Gall : Graph) (hu : (undoF G0 ops R bagsR).2 = false) :
    pdWidth ((undoF G0 ops R bagsR).1 ++ isolatedBags Gall) ≤
      ((deletedSet ops).length : ℝ) + pdWidth bagsR + 3 * (Nat.log 2 G0.numNodes : ℝ) + 1 := by
  have hA : pdWidth (undoF G0 ops R bagsR).1 ≤
      ((deletedSet ops).toFinset.card : ℝ) + pdWidth bagsR +
        3 * (Nat.log 2 G0.numNodes : ℝ) + 1 := h G0 R ops bagsR hG0 hu
  have hcard : ((deletedSet ops).toFinset.card : ℝ) ≤ ((deletedSet ops).length : ℝ) := by
    exact_mod_cast List.toFinset_card_le _
  have hX : 0 ≤ ((deletedSet ops).length : ℝ) + pdWidth bagsR +
      3 * (Nat.log 2 G0.numNodes : ℝ) + 1 := by
    have h1 := neg_one_le_pdWidth bagsR
    have h2 : (0 : ℝ) ≤ ((deletedSet ops).length : ℝ) := Nat.cast_nonneg _
    have h3 : (0 : ℝ) ≤ (Nat.log 2 G0.numNodes : ℝ) := Nat.cast_nonneg _
    linarith
  refine pdWidth_append_le ?_ ?_
  · linarith
  · linarith [isolated_width Gall]

end A3Width

/-- `algo_T4` width bridge (`Spec2.lean` §4), from the `undo` width bridge. -/
theorem algoT4Width_of (h : UndoWidth) : AlgoT4Width := by
  intro G hG lab hfb
  unfold algoT4Full at hfb
  simp only [Bool.or_eq_false_iff] at hfb
  exact A3Width.core h (nonIsolated G) (inducedSpec G (fun v => G.degree v != 0) hG).1 _ _ _
    G hfb.2

#print axioms CubicPathwidth.Alg.algoT4Width_of

end CubicPathwidth.Alg