CubicPathwidth.Alg.Proofs2.L2PlainWidth

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.C1Perm

/-!
# L2: width of the plain sweep (`PlainLayoutWidth`)

Task L2 of the formalisation. Imports `Plan2` and the Stage 1 permutation
lemma `plainOrderPerm`. It does NOT import `L1PlainBags`: the bag description is taken
as the hypothesis `hB : PlainLayoutBags`.

Idea. Let `order = plainOrder G Y` (nodes by decreasing label, injective labels). Then
`order[i]` has the largest label among the entries at positions `≥ i`, and every entry
of `order.take i` has a strictly larger label than `order[i]`. Bag `i` consists of
`order[i]` and of vertices of `take i` with a neighbour outside `take i`; each such
vertex lies above `order[i]` and has a neighbour at or below it, i.e. it is in
`outerFr G Y (Y order[i])`. So each bag has at most `1 + |outerFr|` elements.
-/

namespace CubicPathwidth.Alg

open Graph

namespace L2

/-- The comparator of `plainOrder`, named. -/
def cmp (Y : Labels) (a b : Nat) : Bool :=
  decide (Y b < Y a) || (decide (Y a = Y b) && decide (a ≤ b))

theorem cmp_trans (Y : Labels) : ∀ a b c : Nat,
    cmp Y a b = true → cmp Y b c = true → cmp Y a c = true := by
  intro a b c h1 h2
  simp only [cmp, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at h1 h2 ⊢
  rcases h1 with h1 | ⟨h1, h1'⟩ <;> rcases h2 with h2 | ⟨h2, h2'⟩
  · exact Or.inl (lt_trans h2 h1)
  · exact Or.inl (by linarith)
  · exact Or.inl (by linarith)
  · exact Or.inr ⟨h1.trans h2, Nat.le_trans h1' h2'⟩

theorem cmp_total (Y : Labels) : ∀ a b : Nat, (cmp Y a b || cmp Y b a) = true := by
  intro a b
  simp only [cmp, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq]
  rcases lt_trichotomy (Y a) (Y b) with h | h | h
  · exact Or.inr (Or.inl h)
  · rcases le_total a b with h' | h'
    · exact Or.inl (Or.inr ⟨h, h'⟩)
    · exact Or.inr (Or.inr ⟨h.symm, h'⟩)
  · exact Or.inl (Or.inl h)

/-- A list of naturals whose entries are all `≤ c` (real) has a maximum `≤ c`. -/
theorem foldr_max_cast_le (c : ℝ) (hc : 0 ≤ c) : ∀ l : List Nat,
    (∀ x ∈ l, (x : ℝ) ≤ c) → ((l.foldr max 0 : ℕ) : ℝ) ≤ c
  | [], _ => by simpa using hc
  | x :: l, h => by
    rw [List.foldr_cons, Nat.cast_max]
    exact max_le (h x List.mem_cons_self)
      (foldr_max_cast_le c hc l fun y hy => h y (List.mem_cons_of_mem _ hy))

/-- The core: under the bag description and the sorting, every bag has at most
`1 + |outerFr G Y (Y v)|` elements, where `v` is the vertex at its index. -/
theorem plainLayoutWidth_aux (hB : PlainLayoutBags) (G : Graph) (hG : G.WF) (Y : Labels)
    (hinj : LabelsInjOn G Y) (w : ℝ)
    (hw : ∀ t : ℚ, ((outerFr G Y t).length : ℝ) ≤ w) :
    pdWidth (plainLayout G Y) ≤ w := by
  have hw0 : 0 ≤ w := le_trans (Nat.cast_nonneg _) (hw 0)
  have hperm : (plainOrder G Y).Perm G.nodes := plainOrderPerm G Y
  have hnd : (plainOrder G Y).Nodup := hperm.nodup_iff.2 hG.nodup
  have hlen : (plainOrder G Y).length = G.numNodes := hperm.length_eq
  have hmem : ∀ v, v ∈ plainOrder G Y ↔ v ∈ G.nodes := fun v => hperm.mem_iff
  have hord : plainOrder G Y = G.nodes.mergeSort (cmp Y) := rfl
  have hpair : (plainOrder G Y).Pairwise (fun a b => cmp Y a b = true) := by
    rw [hord]
    exact List.pairwise_mergeSort (cmp_trans Y) (cmp_total Y) G.nodes
  have hpw : ∀ i j (hi : i < (plainOrder G Y).length) (hj : j < (plainOrder G Y).length),
      i < j → cmp Y (plainOrder G Y)[i] (plainOrder G Y)[j] = true := fun i j hi hj hij =>
    (List.pairwise_iff_getElem.1 hpair) i j hi hj hij
  -- entries strictly before position `i` have strictly larger labels than entry `i`
  have hAbove : ∀ i (hi : i < (plainOrder G Y).length), ∀ u ∈ (plainOrder G Y).take i,
      Y ((plainOrder G Y)[i]) < Y u := by
    intro i hi u hu
    obtain ⟨j, hj, rfl⟩ := List.mem_take_iff_getElem.1 hu
    have hji : j < i := lt_of_lt_of_le hj (min_le_left _ _)
    have hjl : j < (plainOrder G Y).length := lt_of_lt_of_le hj (min_le_right _ _)
    have hc := hpw j i hjl hi hji
    simp only [cmp, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at hc
    rcases hc with hc | ⟨hc, _⟩
    · exact hc
    · exfalso
      have hmj : (plainOrder G Y)[j] ∈ G.nodes := (hmem _).1 (List.getElem_mem hjl)
      have hmi : (plainOrder G Y)[i] ∈ G.nodes := (hmem _).1 (List.getElem_mem hi)
      have heq : (plainOrder G Y)[j] = (plainOrder G Y)[i] :=
        hinj _ hmj _ hmi hc
      have := (hnd.getElem_inj_iff).1 heq
      omega
  -- entries outside `take i` have labels at most that of entry `i`
  have hBelow : ∀ i (hi : i < (plainOrder G Y).length), ∀ x ∈ G.nodes,
      x ∉ (plainOrder G Y).take i → Y x ≤ Y ((plainOrder G Y)[i]) := by
    intro i hi x hx hxt
    have hxo : x ∈ plainOrder G Y := (hmem x).2 hx
    obtain ⟨j, hj, hjx⟩ := List.mem_iff_getElem.1 hxo
    subst hjx
    by_cases hij : j < i
    · exact absurd (List.mem_take_iff_getElem.2 ⟨j, lt_min hij hj, rfl⟩) hxt
    · rcases Nat.lt_or_ge i j with h | h
      · have hc := hpw i j hi hj h
        simp only [cmp, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at hc
        rcases hc with hc | ⟨hc, _⟩
        · exact le_of_lt hc
        · exact le_of_eq hc.symm
      · have hij' : i = j := by omega
        subst hij'
        exact le_refl _
  -- the bag at index `i` has at most `1 + |outerFr|` elements
  have hbagcard : ∀ i (hi : i < G.numNodes),
      (((plainLayout G Y).getD i []).toFinset.card : ℝ) ≤ w + 1 := by
    intro i hi
    have hi' : i < (plainOrder G Y).length := by rw [hlen]; exact hi
    have hget : (plainOrder G Y).getD i 0 = (plainOrder G Y)[i] := by
      simp [List.getD_eq_getElem?_getD, hi']
    have hbag := (hB G hG Y).2 i hi
    rw [hget] at hbag
    have hsub : ((plainLayout G Y).getD i []).toFinset ⊆
        insert ((plainOrder G Y)[i])
          (outerFr G Y (Y ((plainOrder G Y)[i]))).toFinset := by
      intro u hu
      rw [List.mem_toFinset] at hu
      rw [Finset.mem_insert, List.mem_toFinset]
      rcases (hbag u).1 hu with h | ⟨hut, x, hx, hxt⟩
      · exact Or.inl h
      · right
        have hun : u ∈ G.nodes := (hmem u).1 (List.mem_of_mem_take hut)
        simp only [outerFr, List.mem_filter, Bool.and_eq_true, decide_eq_true_eq,
          List.any_eq_true]
        exact ⟨hun, hAbove i hi' u hut, x, hx, hBelow i hi' x (hG.nbrs_sub u x hx) hxt⟩
    have hc1 := Finset.card_le_card hsub
    have hc2 := Finset.card_insert_le ((plainOrder G Y)[i])
      (outerFr G Y (Y ((plainOrder G Y)[i]))).toFinset
    have hc3 := List.toFinset_card_le (outerFr G Y (Y ((plainOrder G Y)[i])))
    have hw' := hw (Y ((plainOrder G Y)[i]))
    have hnat : ((plainLayout G Y).getD i []).toFinset.card ≤
        (outerFr G Y (Y ((plainOrder G Y)[i]))).length + 1 := by omega
    have hreal : (((plainLayout G Y).getD i []).toFinset.card : ℝ) ≤
        ((outerFr G Y (Y ((plainOrder G Y)[i]))).length : ℝ) + 1 := by
      exact_mod_cast hnat
    linarith
  -- all bags
  have hmax : (maxBagCard (plainLayout G Y) : ℝ) ≤ w + 1 := by
    unfold maxBagCard
    apply foldr_max_cast_le (w + 1) (by linarith)
    intro x hx
    obtain ⟨B, hB1, hxB⟩ := List.mem_map.1 hx
    obtain ⟨i, hi, hiB⟩ := List.mem_iff_getElem.1 hB1
    have hi2 : i < G.numNodes := by
      rw [(hB G hG Y).1] at hi
      exact hi
    have hg : (plainLayout G Y).getD i [] = B := by
      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi, Option.getD_some, hiB]
    rw [← hxB, ← hg]
    exact hbagcard i hi2
  unfold pdWidth
  linarith

end L2

/-- Task L2: the plain sweep has width at most the largest outer frontier (given the
exact bag description `PlainLayoutBags` of task L1, taken as a hypothesis). -/
theorem plainLayoutWidth_of (hB : PlainLayoutBags) : PlainLayoutWidth := by
  intro G hG Y hinj w hw
  exact L2.plainLayoutWidth_aux hB G hG Y hinj w hw

#print axioms CubicPathwidth.Alg.plainLayoutWidth_of

end CubicPathwidth.Alg