import CubicPathwidth.Alg.Spec

/-!
# B1: bridge from a list of bags to a frozen `PathDecomposition`

Proves `CubicPathwidth.Alg.validPDBridge_of : ValidPDBridge`.

Construction: `lastIndex = bags.length - 1` and the bag with index `i` is the set of
`v : Fin n` with `v.val ∈ bags.getD i []`. If `bags = []` then `lastIndex = 0` and the
single bag is empty, which is the required one-empty-bag decomposition (the coverage
hypothesis forces `n = 0` in that case).
-/

noncomputable section

namespace CubicPathwidth.Alg

namespace B1

open CubicPathwidth

/-- The bag of index `i` of the decomposition built from `bags`. -/
def bagOf (n : ℕ) (bags : List Bag) (i : ℕ) : Finset (Fin n) :=
  Finset.univ.filter (fun v : Fin n => v.val ∈ bags.getD i [])

lemma mem_bagOf (n : ℕ) (bags : List Bag) (i : ℕ) (v : Fin n) :
    v ∈ bagOf n bags i ↔ v.val ∈ bags.getD i [] := by
  simp [bagOf]

/-- `InBag` is membership in the `getD` list. -/
lemma inBag_iff_getD (bags : List Bag) (i v : ℕ) :
    InBag bags i v ↔ v ∈ bags.getD i [] := by
  unfold InBag
  rw [List.getD_eq_getElem?_getD]
  cases h : bags[i]? with
  | none => simp
  | some B => simp

/-- An index with a bag lies below the length. -/
lemma lt_length_of_inBag {bags : List Bag} {i v : ℕ} (h : InBag bags i v) :
    i < bags.length := by
  obtain ⟨B, hB, _⟩ := h
  obtain ⟨hlt, _⟩ := List.getElem?_eq_some_iff.1 hB
  exact hlt

/-- Every bag of `bags` has at most `maxBagCard bags` elements (as a finset). -/
lemma le_maxBagCard (bags : List Bag) : ∀ B ∈ bags, B.toFinset.card ≤ maxBagCard bags := by
  induction bags with
  | nil => simp
  | cons C cs ih =>
    intro B hB
    simp only [maxBagCard, List.map_cons, List.foldr_cons] at ih ⊢
    rcases List.mem_cons.1 hB with rfl | hB
    · exact le_max_left _ _
    · exact le_trans (ih B hB) (le_max_right _ _)

/-- Every `getD` bag has at most `maxBagCard bags` elements. -/
lemma getD_card_le (bags : List Bag) (i : ℕ) :
    (bags.getD i []).toFinset.card ≤ maxBagCard bags := by
  rw [List.getD_eq_getElem?_getD]
  cases h : bags[i]? with
  | none => simp
  | some B =>
    simpa using le_maxBagCard bags B (List.mem_of_getElem? h)

lemma bagOf_card_le (n : ℕ) (bags : List Bag) (i : ℕ) :
    (bagOf n bags i).card ≤ maxBagCard bags := by
  refine le_trans ?_ (getD_card_le bags i)
  refine Finset.card_le_card_of_injOn (fun v : Fin n => v.val) ?_ ?_
  · intro v hv
    simp only [Finset.mem_coe] at hv
    simp only [Finset.mem_coe, List.mem_toFinset]
    exact (mem_bagOf n bags i v).1 hv
  · exact Fin.val_injective.injOn

/-- Coverage of the built decomposition. -/
lemma vertex_covered_of (n : ℕ) (G : Graph) (bags : List Bag)
    (hn : ∀ v, v ∈ G.nodes ↔ v < n) (hV : ValidPD G bags) (v : Fin n) :
    ∃ i : Fin (bags.length - 1 + 1), v ∈ bagOf n bags i.val := by
  obtain ⟨i, hi⟩ := hV.1 v.val ((hn v.val).2 v.isLt)
  have hlt : i < bags.length := lt_length_of_inBag hi
  refine ⟨⟨i, by omega⟩, ?_⟩
  rw [mem_bagOf]
  exact (inBag_iff_getD bags i v.val).1 hi

/-- Adjacency in the simple graph gives a common bag. -/
lemma edge_covered_of (n : ℕ) (G : Graph) (bags : List Bag)
    (hn : ∀ v, v ∈ G.nodes ↔ v < n) (hV : ValidPD G bags) (u v : Fin n)
    (huv : (G.toSimpleGraph n).Adj u v) :
    ∃ i : Fin (bags.length - 1 + 1), u ∈ bagOf n bags i.val ∧ v ∈ bagOf n bags i.val := by
  have key : ∀ a b : Fin n, G.Adj a.val b.val →
      ∃ i : Fin (bags.length - 1 + 1), a ∈ bagOf n bags i.val ∧ b ∈ bagOf n bags i.val := by
    intro a b hab
    obtain ⟨B, hB, haB, hbB⟩ := hV.2.2 a.val b.val ((hn a.val).2 a.isLt) hab
    obtain ⟨i, hi⟩ := List.mem_iff_getElem?.1 hB
    obtain ⟨hlt, _⟩ := List.getElem?_eq_some_iff.1 hi
    refine ⟨⟨i, by omega⟩, ?_, ?_⟩
    · rw [mem_bagOf, List.getD_eq_getElem?_getD, hi]
      simpa using haB
    · rw [mem_bagOf, List.getD_eq_getElem?_getD, hi]
      simpa using hbB
  rcases (SimpleGraph.fromRel_adj _ _ _).1 huv with ⟨_, h | h⟩
  · exact key u v h
  · obtain ⟨i, h1, h2⟩ := key v u h
    exact ⟨i, h2, h1⟩

/-- Interval property of the built decomposition. -/
lemma interval_of (n : ℕ) (G : Graph) (bags : List Bag)
    (hn : ∀ v, v ∈ G.nodes ↔ v < n) (hV : ValidPD G bags)
    (i j k : Fin (bags.length - 1 + 1)) (hij : i ≤ j) (hjk : j ≤ k) (v : Fin n)
    (hv : v ∈ bagOf n bags i.val ∧ v ∈ bagOf n bags k.val) :
    v ∈ bagOf n bags j.val := by
  obtain ⟨hvi, hvk⟩ := hv
  rw [mem_bagOf] at hvi hvk ⊢
  have hij' : i.val ≤ j.val := Fin.le_def.1 hij
  have hjk' : j.val ≤ k.val := Fin.le_def.1 hjk
  exact (inBag_iff_getD bags j.val v.val).1
    (hV.2.1 v.val ((hn v.val).2 v.isLt) i.val j.val k.val hij' hjk'
      ((inBag_iff_getD bags i.val v.val).2 hvi)
      ((inBag_iff_getD bags k.val v.val).2 hvk))

/-- The path decomposition built from a valid list of bags. -/
def decomp (n : ℕ) (G : Graph) (bags : List Bag)
    (hn : ∀ v, v ∈ G.nodes ↔ v < n) (hV : ValidPD G bags) :
    PathDecomposition (G.toSimpleGraph n) where
  lastIndex := bags.length - 1
  bag i := bagOf n bags i.val
  vertex_covered := vertex_covered_of n G bags hn hV
  edge_covered := edge_covered_of n G bags hn hV
  interval := interval_of n G bags hn hV

lemma decomp_width (n : ℕ) (G : Graph) (bags : List Bag)
    (hn : ∀ v, v ∈ G.nodes ↔ v < n) (hV : ValidPD G bags) :
    (decomp n G bags hn hV).WidthAtMost (pdWidth bags) := by
  intro i
  have h : (bagOf n bags i.val).card ≤ maxBagCard bags := bagOf_card_le n bags i.val
  have h' : ((bagOf n bags i.val).card : ℝ) ≤ (maxBagCard bags : ℝ) := by exact_mod_cast h
  unfold pdWidth
  show ((bagOf n bags i.val).card : ℝ) ≤ ((maxBagCard bags : ℝ) - 1) + 1
  linarith

end B1

open B1 in
/-- A valid decomposition of a well-formed graph on `{0, …, n-1}` gives
`HasPathwidthAtMost` for its simple graph, with the width of the bags. -/
theorem validPDBridge_of (hWF : WFBasics) : ValidPDBridge := by
  intro n G bags _hG hn hV
  exact ⟨decomp n G bags hn hV, decomp_width n G bags hn hV⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.validPDBridge_of