import CubicPathwidth.T2.Defs
import CubicPathwidth.C3.Intervals

/-!
# Plain-sweep layout (O1)

Kinnersley's argument: with `rank` as the time of each vertex, the interval of `v`
runs from the least rank in its closed neighbourhood to its own rank. The bag at
time `t` lies in `{v_t} ∪ Fr(y v_t)`.
-/

noncomputable section

namespace CubicPathwidth
namespace T2

open Classical in
theorem plainLayout_s : PlainLayoutClaim := by
  intro n G y hy w hw
  classical
  -- start time of each vertex
  let S : Fin n → Finset ℕ := fun v =>
    insert (C3.rank y v) ((Finset.univ.filter fun u => G.Adj v u).image (C3.rank y))
  have hSne : ∀ v, (S v).Nonempty := fun v => ⟨_, Finset.mem_insert_self _ _⟩
  let s : Fin n → ℕ := fun v => (S v).min' (hSne v)
  have hs_le_rank : ∀ v, s v ≤ C3.rank y v := fun v =>
    Finset.min'_le _ _ (Finset.mem_insert_self _ _)
  have hs_le_adj : ∀ v u, G.Adj v u → s v ≤ C3.rank y u := fun v u h =>
    Finset.min'_le _ _ (Finset.mem_insert_of_mem
      (Finset.mem_image.mpr ⟨u, by simp [h], rfl⟩))
  have hs_cases : ∀ v, s v = C3.rank y v ∨ ∃ u, G.Adj v u ∧ s v = C3.rank y u := by
    intro v
    have hm := Finset.min'_mem (S v) (hSne v)
    rcases Finset.mem_insert.mp hm with h | h
    · exact Or.inl h
    · obtain ⟨u, hu, hu'⟩ := Finset.mem_image.mp h
      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hu
      exact Or.inr ⟨u, hu, hu'.symm⟩
  refine C3.hasPathwidth_of_intervals G (n - 1) s (C3.rank y) hs_le_rank ?_ ?_ w ?_
  · intro v
    have := C3.rank_lt_n y v
    omega
  · intro u v huv
    have hne : y u ≠ y v := fun h => G.ne_of_adj huv (hy h)
    rcases lt_or_gt_of_ne hne with h | h
    · have h' : C3.rank y u < C3.rank y v := (C3.rank_lt_iff hy).mpr h
      exact ⟨C3.rank y u, hs_le_rank u, le_rfl, hs_le_adj v u huv.symm, h'.le⟩
    · have h' : C3.rank y v < C3.rank y u := (C3.rank_lt_iff hy).mpr h
      exact ⟨C3.rank y v, hs_le_adj u v huv, h'.le, hs_le_rank v, le_rfl⟩
  · intro t ht
    by_cases hex : ∃ v, C3.rank y v = t
    · obtain ⟨vt, hvt⟩ := hex
      have hsub : C3.intervalBag s (C3.rank y) t ⊆ insert vt (C3.outerFrontier G y (y vt)) := by
        intro v hv
        simp only [C3.intervalBag, Finset.mem_filter, Finset.mem_univ, true_and] at hv
        obtain ⟨hv1, hv2⟩ := hv
        by_cases hveq : v = vt
        · exact Finset.mem_insert.mpr (Or.inl hveq)
        · apply Finset.mem_insert_of_mem
          have hne : C3.rank y v ≠ t := fun h => hveq (C3.rank_injective hy (h.trans hvt.symm))
          have hlt : C3.rank y vt < C3.rank y v := by omega
          have hyv : y vt < y v := (C3.rank_lt_iff hy).mp hlt
          simp only [C3.outerFrontier, Finset.mem_filter, Finset.mem_univ, true_and]
          refine ⟨hyv, ?_⟩
          rcases hs_cases v with h | ⟨u, hu, hu'⟩
          · omega
          · refine ⟨u, hu.symm, ?_⟩
            have : C3.rank y u ≤ C3.rank y vt := by omega
            exact (C3.rank_le_iff hy).mp this
      calc ((C3.intervalBag s (C3.rank y) t).card : ℝ)
          ≤ ((insert vt (C3.outerFrontier G y (y vt))).card : ℝ) := by
            exact_mod_cast Finset.card_le_card hsub
        _ ≤ ((C3.outerFrontier G y (y vt)).card : ℝ) + 1 := by
            exact_mod_cast Finset.card_insert_le _ _
        _ ≤ w + 1 := by linarith [hw (y vt)]
    · have hn : n = 0 := by
        by_contra hn
        exact hex (C3.exists_rank_eq hy (i := t) (by omega))
      subst hn
      have hempty : C3.intervalBag s (C3.rank y) t = ∅ := by
        ext v; exact v.elim0
      rw [hempty]
      have h0 := hw 0
      have : (0 : ℝ) ≤ ((C3.outerFrontier G y 0).card : ℝ) := Nat.cast_nonneg _
      simp only [Finset.card_empty, Nat.cast_zero]
      linarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.plainLayout_s