CubicPathwidth.Alg.Proofs.C4Switched

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

import CubicPathwidth.Alg.Spec

/-!
# C4: validity of the median-switched layout (`SwitchedLayoutValid`)

Membership-level mirror of `switchedLayoutF` (`layoutB`), the block lemmas, and the
proof that the layout is a valid path decomposition (plan task C4).
-/

namespace CubicPathwidth.Alg

open Graph

namespace C4

/-! ## Definitions (membership-level mirror of `switchedLayoutF`) -/

/-- Python `Wp`: `Wset \ D`. -/
def wpF (G : Graph) (Y : Labels) (x : Nat) : Bool := inW G Y x && !inD G Y x

/-- Python `P` (the connector items come from these). -/
def pSet (G : Graph) (Y : Labels) : List Nat :=
  G.nodes.filter fun u => inU G Y u && !inD G Y u && (G.nbrs u).any (wpF G Y)

/-- Python `e u`. -/
def eSet (G : Graph) (Y : Labels) (u : Nat) : List Nat := (G.nbrs u).filter (wpF G Y)

/-- The number of low nodes (`ell`). -/
def nLow (G : Graph) (Y : Labels) : Nat := (G.nodes.filter (isLow Y)).length

/-- Inner bag `i` (`i < ell`). -/
def innerB (G : Graph) (order : List Nat) (i : Nat) : Bag :=
  order.getD i 0 :: (order.take i).filter fun u =>
    (G.nbrs u).any fun x => !decide (x ∈ order.take i)

/-- The bag `C_{-1}`. -/
def cm1B (G : Graph) (Y : Labels) : Bag :=
  G.nodes.filter fun v => inU G Y v || (inD G Y v && inW G Y v)

/-- The bag `C_j`. -/
def csB (G : Graph) (Y : Labels) (q : List Nat) (j : Nat) : Bag :=
  G.nodes.filter (inD G Y) ++ (pSet G Y).filter (fun u => !subsetB (eSet G Y u) (q.take (j - 1)))
    ++ q.take j

/-- Outer bag `k`. -/
def outB (G : Graph) (Y : Labels) (order : List Nat) (k : Nat) : Bag :=
  order.getD (nLow G Y + k) 0 :: G.nodes.filter fun x =>
    !decide (x ∈ G.nodes.filter (isLow Y) ++ (order.drop (nLow G Y)).take (k + 1)) &&
      (G.nbrs x).any fun u =>
        decide (u ∈ G.nodes.filter (isLow Y) ++ (order.drop (nLow G Y)).take (k + 1))

/-- The whole layout, block by block: inner, `C_{-1}`, `C_0 … C_m`, outer. -/
def layoutB (G : Graph) (Y : Labels) (order q : List Nat) : List Bag :=
  (List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y] ++
    (List.range (q.length + 1)).map (csB G Y q) ++
    (List.range (order.length - nLow G Y)).map (outB G Y order)

/-- Hypotheses on the order and the connector list used by the proof. -/
structure OrdOK (G : Graph) (Y : Labels) (order q : List Nat) : Prop where
  perm : order.Perm G.nodes
  split : order = order.filter (isLow Y) ++ order.filter (fun x => !isLow Y x)
  qmem : ∀ x, x ∈ q ↔ x ∈ G.nodes.filter (wpF G Y)

/-! ## Equality with `switchedLayout` -/

theorem hs_contains (T : List Nat) (x : Nat) :
    (T.foldl (fun s y => s.insert y) (∅ : Std.HashSet Nat)).contains x = decide (x ∈ T) := by
  have key : ∀ (T : List Nat) (s : Std.HashSet Nat),
      (T.foldl (fun s y => s.insert y) s).contains x = (s.contains x || decide (x ∈ T)) := by
    intro T
    induction T with
    | nil => intro s; simp
    | cons a T ih =>
      intro s
      simp only [List.foldl_cons, ih, Std.HashSet.contains_insert, List.mem_cons]
      grind
  rw [key]
  simp


/-! ## Order facts -/

/-- A list whose elements are "low before high" splits as `filter p ++ filter (not p)`. -/
theorem lows_first {α : Type} (p : α → Bool) : ∀ (l : List α),
    l.Pairwise (fun a b => p b = true → p a = true) →
    l = l.filter p ++ l.filter (fun x => !p x)
  | [], _ => by simp
  | a :: t, h => by
    rw [List.pairwise_cons] at h
    obtain ⟨ha, ht⟩ := h
    have IH := lows_first p t ht
    by_cases hpa : p a = true
    · have h1 : (a :: t).filter p = a :: t.filter p := by simp [hpa]
      have h2 : (a :: t).filter (fun x => !p x) = t.filter (fun x => !p x) := by
        simp [hpa]
      rw [h1, h2]
      exact congrArg (a :: ·) IH
    · have hT : ∀ b ∈ t, p b = false := fun b hb => by
        cases hb' : p b with
        | false => rfl
        | true => exact absurd (ha b hb hb') hpa
      have h1 : t.filter p = [] := List.filter_eq_nil_iff.2 (fun b hb => by simp [hT b hb])
      have h2 : t.filter (fun x => !p x) = t := List.filter_eq_self.2 (fun b hb => by simp [hT b hb])
      have h3 : (a :: t).filter p = [] := by simp [hpa, h1]
      have h4 : (a :: t).filter (fun x => !p x) = a :: t := by
        simp [hpa, h2]
      rw [h3, h4]
      simp

/-- Every element of `G.nodes` is in `order` (membership form of the permutation). -/
theorem OrdOK.mem {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {v : Nat} : v ∈ order ↔ v ∈ G.nodes :=
  h.perm.mem_iff

theorem OrdOK.nodup {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    (hnd : G.nodes.Nodup) : order.Nodup :=
  h.perm.nodup_iff.2 hnd

theorem OrdOK.length {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q) :
    order.length = G.nodes.length :=
  h.perm.length_eq

theorem nLow_le {G : Graph} {Y : Labels} : nLow G Y ≤ G.nodes.length :=
  List.length_filter_le _ _

/-- The first `nLow` entries of `order` are the low nodes. -/
theorem OrdOK.take_nLow {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q) :
    order.take (nLow G Y) = order.filter (isLow Y) := by
  have hlen : (order.filter (isLow Y)).length = nLow G Y :=
    (h.perm.filter (isLow Y)).length_eq
  have key := List.take_left' (l₁ := order.filter (isLow Y))
    (l₂ := order.filter (fun x => !isLow Y x)) hlen
  rw [← h.split] at key
  exact key

/-- A node is low iff its position is below `nLow`. -/
theorem OrdOK.low_iff {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {v : Nat} (hv : v ∈ G.nodes) : isLow Y v = true ↔ order.idxOf v < nLow G Y := by
  have hvo : v ∈ order := h.mem.2 hv
  rw [← List.mem_take_iff_idxOf_lt hvo, h.take_nLow, List.mem_filter]
  simp [hvo]

/-- Position of a node in `order` (for nodup `order`). -/
theorem getD_idxOf {order : List Nat} {v : Nat} (hv : v ∈ order) :
    order.getD (order.idxOf v) 0 = v := by
  have hlt : order.idxOf v < order.length := List.idxOf_lt_length_iff.2 hv
  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hlt]
  simp only [Option.getD_some]
  exact List.getElem_idxOf hlt

theorem idxOf_getD {order : List Nat} (hnd : order.Nodup) {i : Nat} (hi : i < order.length) :
    order.idxOf (order.getD i 0) = i := by
  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi]
  simp only [Option.getD_some]
  exact hnd.idxOf_getElem i hi

theorem getD_eq_iff {order : List Nat} (hnd : order.Nodup) {i v : Nat}
    (hi : i < order.length) (hv : v ∈ order) :
    order.getD i 0 = v ↔ order.idxOf v = i := by
  constructor
  · intro e
    rw [← e, idxOf_getD hnd hi]
  · intro e
    rw [← e]
    exact getD_idxOf hv

/-- Membership in the `T` of the outer bags: the first `nLow + k + 1` positions. -/
theorem OrdOK.mem_T {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {k x : Nat} (hx : x ∈ G.nodes) :
    x ∈ G.nodes.filter (isLow Y) ++ (order.drop (nLow G Y)).take (k + 1) ↔
      order.idxOf x < nLow G Y + k + 1 := by
  have hxo : x ∈ order := h.mem.2 hx
  have e : nLow G Y + k + 1 = nLow G Y + (k + 1) := by omega
  rw [← List.mem_take_iff_idxOf_lt hxo, e, List.take_add (i := nLow G Y) (j := k + 1), h.take_nLow]
  simp [List.mem_append, List.mem_filter, hxo, hx]

/-! ## Block membership -/

theorem inBag_append_lt {A B : List Bag} {g : Nat} {v : Nat} (hg : g < A.length) :
    InBag (A ++ B) g v ↔ InBag A g v := by
  unfold InBag
  rw [List.getElem?_append_left hg]

theorem inBag_append_ge {A B : List Bag} {g : Nat} {v : Nat} (hg : A.length ≤ g) :
    InBag (A ++ B) g v ↔ InBag B (g - A.length) v := by
  unfold InBag
  rw [List.getElem?_append_right hg]

theorem inBag_map_range (f : Nat → Bag) (k g v : Nat) :
    InBag ((List.range k).map f) g v ↔ g < k ∧ v ∈ f g := by
  unfold InBag
  by_cases hg : g < k
  · simp [hg]
  · have : ((List.range k).map f)[g]? = none := by
      rw [List.getElem?_eq_none]
      simp only [List.length_map, List.length_range]
      omega
    simp [hg]

theorem inBag_singleton (B : Bag) (g v : Nat) : InBag [B] g v ↔ g = 0 ∧ v ∈ B := by
  unfold InBag
  cases g <;> simp

/-- Predicate form of `List.any` (pointwise on the list). -/
theorem any_iff_of {l : List Nat} {f : Nat → Bool} {P : Nat → Prop}
    (h : ∀ x ∈ l, (f x = true ↔ P x)) : l.any f = true ↔ ∃ x ∈ l, P x := by
  rw [List.any_eq_true]
  constructor
  · rintro ⟨x, hx, hx2⟩
    exact ⟨x, hx, (h x hx).1 hx2⟩
  · rintro ⟨x, hx, hx2⟩
    exact ⟨x, hx, (h x hx).2 hx2⟩

/-- Membership in the inner bag `i`. -/
theorem mem_inner {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {i v : Nat} (hi : i < nLow G Y) (hv : v ∈ G.nodes) :
    v ∈ innerB G order i ↔
      (order.idxOf v = i ∨ (order.idxOf v < i ∧ ∃ x ∈ G.nbrs v, i ≤ order.idxOf x)) := by
  have hnlen : nLow G Y ≤ order.length := by rw [h.length]; exact nLow_le
  have hi' : i < order.length := by omega
  have hvo : v ∈ order := h.mem.2 hv
  have hnd : order.Nodup := h.nodup hG.nodup
  have hnb : ∀ x ∈ G.nbrs v, (x ∈ order.take i ↔ order.idxOf x < i) := fun x hx =>
    List.mem_take_iff_idxOf_lt (h.mem.2 (hG.nbrs_sub v x hx))
  have hany : (G.nbrs v).any (fun x => !decide (x ∈ order.take i)) = true ↔
      ∃ x ∈ G.nbrs v, i ≤ order.idxOf x := by
    refine any_iff_of (fun x hx => ?_)
    have h1 := hnb x hx
    simp only [Bool.not_eq_true', decide_eq_false_iff_not, h1, not_lt]
  have hg : (v = order.getD i 0) ↔ order.idxOf v = i := by
    rw [eq_comm]
    exact getD_eq_iff hnd hi' hvo
  unfold innerB
  rw [List.mem_cons, List.mem_filter, hg, List.mem_take_iff_idxOf_lt hvo, hany]

theorem mem_cm1 {G : Graph} {Y : Labels} {v : Nat} :
    v ∈ cm1B G Y ↔ v ∈ G.nodes ∧ (inU G Y v = true ∨ (inD G Y v = true ∧ inW G Y v = true)) := by
  unfold cm1B
  simp [List.mem_filter, Bool.or_eq_true, Bool.and_eq_true]

theorem mem_pSet {G : Graph} {Y : Labels} {v : Nat} :
    v ∈ pSet G Y ↔ v ∈ G.nodes ∧ inU G Y v = true ∧ inD G Y v = false ∧
      ∃ x ∈ G.nbrs v, wpF G Y x = true := by
  unfold pSet
  simp [List.mem_filter, Bool.and_eq_true, List.any_eq_true, and_assoc]

/-- Membership in `C_j`. -/
theorem mem_cs {G : Graph} {Y : Labels} {q : List Nat} {j v : Nat} :
    v ∈ csB G Y q j ↔ (v ∈ G.nodes ∧ inD G Y v = true) ∨
      (v ∈ G.nodes ∧ inU G Y v = true ∧ inD G Y v = false ∧ (∃ x ∈ G.nbrs v, wpF G Y x = true) ∧
        subsetB (eSet G Y v) (q.take (j - 1)) = false) ∨ v ∈ q.take j := by
  unfold csB
  rw [List.mem_append, List.mem_append, List.mem_filter, List.mem_filter, mem_pSet]
  simp only [Bool.not_eq_true']
  constructor
  · rintro ((⟨h1, h2⟩ | ⟨⟨h1, h2, h3, h4⟩, h5⟩) | h6)
    · exact Or.inl ⟨h1, h2⟩
    · exact Or.inr (Or.inl ⟨h1, h2, h3, h4, h5⟩)
    · exact Or.inr (Or.inr h6)
  · rintro (⟨h1, h2⟩ | ⟨h1, h2, h3, h4, h5⟩ | h6)
    · exact Or.inl (Or.inl ⟨h1, h2⟩)
    · exact Or.inl (Or.inr ⟨⟨h1, h2, h3, h4⟩, h5⟩)
    · exact Or.inr h6

/-- Membership in the outer bag `k` (the node itself at its own index, then the
neighbours of the first `nLow + k + 1` positions). -/
theorem mem_out {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {k v : Nat} (hk : k < order.length - nLow G Y) (hv : v ∈ G.nodes) :
    v ∈ outB G Y order k ↔ order.idxOf v = nLow G Y + k ∨
      (nLow G Y + k < order.idxOf v ∧ ∃ x ∈ G.nbrs v, order.idxOf x ≤ nLow G Y + k) := by
  have hnlen : nLow G Y ≤ order.length := by rw [h.length]; exact nLow_le
  have hi' : nLow G Y + k < order.length := by omega
  have hvo : v ∈ order := h.mem.2 hv
  have hnd : order.Nodup := h.nodup hG.nodup
  have hT : ∀ x ∈ G.nodes, (x ∈ G.nodes.filter (isLow Y) ++ (order.drop (nLow G Y)).take (k + 1) ↔
      order.idxOf x < nLow G Y + k + 1) := fun x hx => h.mem_T hx
  have hany : (G.nbrs v).any (fun x => decide (x ∈ G.nodes.filter (isLow Y) ++
      (order.drop (nLow G Y)).take (k + 1))) = true ↔
      ∃ x ∈ G.nbrs v, order.idxOf x < nLow G Y + k + 1 := by
    refine any_iff_of (fun x hx => ?_)
    rw [decide_eq_true_eq, hT x (hG.nbrs_sub v x hx)]
  have hnot : ¬ (v ∈ G.nodes.filter (isLow Y) ++ (order.drop (nLow G Y)).take (k + 1)) ↔
      nLow G Y + k < order.idxOf v := by
    rw [hT v hv]
    omega
  unfold outB
  have hg : (v = order.getD (nLow G Y + k) 0) ↔ order.idxOf v = nLow G Y + k := by
    rw [eq_comm]
    exact getD_eq_iff hnd hi' hvo
  rw [List.mem_cons, List.mem_filter, hg]
  simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, hany]
  constructor
  · rintro (h1 | ⟨_, h2, x, hx, hx2⟩)
    · exact Or.inl h1
    · exact Or.inr ⟨hnot.1 h2, x, hx, by omega⟩
  · rintro (h1 | ⟨h2, x, hx, hx2⟩)
    · exact Or.inl h1
    · exact Or.inr ⟨hv, hnot.2 h2, x, hx, by omega⟩

/-- The block structure of `InBag` for the whole layout. -/
theorem inBag_layout {G : Graph} {Y : Labels} {order q : List Nat} (g v : Nat) :
    InBag (layoutB G Y order q) g v ↔
      (g < nLow G Y ∧ v ∈ innerB G order g) ∨ (g = nLow G Y ∧ v ∈ cm1B G Y) ∨
      (nLow G Y + 1 ≤ g ∧ g ≤ nLow G Y + 1 + q.length ∧
        v ∈ csB G Y q (g - (nLow G Y + 1))) ∨
      (nLow G Y + 2 + q.length ≤ g ∧ g - (nLow G Y + 2 + q.length) < order.length - nLow G Y ∧
        v ∈ outB G Y order (g - (nLow G Y + 2 + q.length))) := by
  unfold layoutB
  have hA1 : ((List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y]).length =
      nLow G Y + 1 := by
    simp
  have hA2 : ((List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y] ++
      (List.range (q.length + 1)).map (csB G Y q)).length = nLow G Y + 2 + q.length := by
    simp only [List.length_append, List.length_map, List.length_range, List.length_singleton]
    omega
  by_cases h4 : nLow G Y + 2 + q.length ≤ g
  · rw [inBag_append_ge (A := (List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y] ++
      (List.range (q.length + 1)).map (csB G Y q)) (by rw [hA2]; exact h4), hA2, inBag_map_range]
    constructor
    · rintro ⟨h5, h6⟩
      exact Or.inr (Or.inr (Or.inr ⟨h4, h5, h6⟩))
    · rintro (⟨h5, _⟩ | ⟨h5, _⟩ | ⟨h5, _⟩ | ⟨_, h5, h6⟩)
      · omega
      · omega
      · omega
      · exact ⟨h5, h6⟩
  · rw [inBag_append_lt (A := (List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y] ++
      (List.range (q.length + 1)).map (csB G Y q)) (by rw [hA2]; omega)]
    by_cases h3 : nLow G Y + 1 ≤ g
    · rw [inBag_append_ge (A := (List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y])
        (by rw [hA1]; exact h3), hA1]
      by_cases h2 : g < nLow G Y + 1 + (q.length + 1)
      · rw [inBag_map_range]
        constructor
        · rintro ⟨h5, h6⟩
          exact Or.inr (Or.inr (Or.inl ⟨h3, by omega, by
            have : g - (nLow G Y + 1) = g - (nLow G Y + 1) := rfl
            exact h6⟩))
        · rintro (⟨h5, _⟩ | ⟨h5, _⟩ | ⟨h5, h6, h7⟩ | ⟨h5, _⟩)
          · omega
          · omega
          · exact ⟨by omega, h7⟩
          · omega
      · rw [inBag_map_range]
        constructor
        · rintro ⟨h5, _⟩
          omega
        · rintro (⟨h5, _⟩ | ⟨h5, _⟩ | ⟨h5, h6, h7⟩ | ⟨h5, _⟩)
          · omega
          · omega
          · omega
          · omega
    · rw [inBag_append_lt (A := (List.range (nLow G Y)).map (innerB G order) ++ [cm1B G Y])
        (by rw [hA1]; omega)]
      by_cases h1 : g < nLow G Y
      · rw [inBag_append_lt (A := (List.range (nLow G Y)).map (innerB G order))
          (by simp only [List.length_map, List.length_range]; omega), inBag_map_range]
        constructor
        · rintro ⟨h5, h6⟩
          exact Or.inl ⟨h5, h6⟩
        · rintro (⟨h5, h6⟩ | ⟨h5, _⟩ | ⟨h5, _⟩ | ⟨h5, _⟩)
          · exact ⟨h5, h6⟩
          · omega
          · omega
          · omega
      · rw [inBag_append_ge (A := (List.range (nLow G Y)).map (innerB G order))
          (by simp only [List.length_map, List.length_range]; omega), inBag_singleton]
        constructor
        · rintro ⟨h5, h6⟩
          exact Or.inr (Or.inl ⟨by simp only [List.length_map, List.length_range] at h5; omega, h6⟩)
        · rintro (⟨h5, _⟩ | ⟨h5, h6⟩ | ⟨h5, _⟩ | ⟨h5, _⟩)
          · omega
          · simp only [List.length_map, List.length_range]
            exact ⟨by omega, h6⟩
          · omega
          · omega


/-! ## Local facts about the classes -/

theorem inU_iff {G : Graph} {Y : Labels} {v : Nat} :
    inU G Y v = true ↔ isLow Y v = true ∧ ∃ x ∈ G.nbrs v, isLow Y x = false := by
  simp [inU, Bool.and_eq_true, List.any_eq_true]

theorem inW_iff {G : Graph} {Y : Labels} {v : Nat} :
    inW G Y v = true ↔ isLow Y v = false ∧ ∃ x ∈ G.nbrs v, isLow Y x = true := by
  simp [inW, Bool.and_eq_true, List.any_eq_true]

theorem inD_iff {G : Graph} {Y : Labels} {v : Nat} :
    inD G Y v = true ↔ G.degree v = 3 ∧ ∀ x ∈ G.nbrs v, (isLow Y x != isLow Y v) = true := by
  simp [inD, Bool.and_eq_true, List.all_eq_true, degree]

theorem wpF_iff {G : Graph} {Y : Labels} {v : Nat} :
    wpF G Y v = true ↔ (isLow Y v = false ∧ ∃ x ∈ G.nbrs v, isLow Y x = true) ∧ inD G Y v = false := by
  simp [wpF, Bool.and_eq_true, inW_iff]

/-- A degree-3 vertex has a neighbour. -/
theorem exists_nbr_of_degree3 {G : Graph} {v : Nat} (h : G.degree v = 3) :
    ∃ x, x ∈ G.nbrs v := by
  unfold degree at h
  cases hl : G.nbrs v with
  | nil => rw [hl] at h; simp at h
  | cons x t => exact ⟨x, by simp⟩

/-- A low degree-3 node with all neighbours high is in `U`. -/
theorem inU_of_inD_low {G : Graph} {Y : Labels} {v : Nat}
    (hd : inD G Y v = true) (hl : isLow Y v = true) : inU G Y v = true := by
  obtain ⟨hdeg, hall⟩ := inD_iff.1 hd
  obtain ⟨x, hx⟩ := exists_nbr_of_degree3 hdeg
  have hx2 := hall x hx
  have hxh : isLow Y x = false := by
    rw [hl] at hx2
    cases hxl : isLow Y x <;> simp_all
  exact inU_iff.2 ⟨hl, x, hx, hxh⟩

/-- A high degree-3 node is in `W`. -/
theorem inW_of_inD_high {G : Graph} {Y : Labels} {v : Nat}
    (hd : inD G Y v = true) (hh : isLow Y v = false) : inW G Y v = true := by
  obtain ⟨hdeg, hall⟩ := inD_iff.1 hd
  obtain ⟨x, hx⟩ := exists_nbr_of_degree3 hdeg
  have hx2 := hall x hx
  have hxl : isLow Y x = true := by
    rw [hh] at hx2
    cases hxl : isLow Y x <;> simp_all
  exact inW_iff.2 ⟨hh, x, hx, hxl⟩

/-! ## Existence of thresholds and extrema -/

/-- A downward closed predicate true at `0` is an initial segment of `[0, L]`. -/
theorem exists_thr (Q : Nat → Prop) (hdown : ∀ j k, j ≤ k → Q k → Q j) (h0 : Q 0) (L : Nat) :
    ∃ J, J ≤ L ∧ ∀ j, j ≤ L → (Q j ↔ j ≤ J) := by
  induction L with
  | zero => exact ⟨0, le_refl 0, fun j hj => by
      have : j = 0 := by omega
      subst this
      simp [h0]⟩
  | succ L ih =>
    obtain ⟨J, hJL, hJ⟩ := ih
    by_cases hQ : Q (L + 1)
    · refine ⟨L + 1, le_refl _, fun j hj => ?_⟩
      exact ⟨fun _ => hj, fun _ => hdown j (L + 1) hj hQ⟩
    · refine ⟨J, by omega, fun j hj => ?_⟩
      by_cases hjL : j ≤ L
      · exact hJ j hjL
      · have : j = L + 1 := by omega
        subst this
        exact ⟨fun h => absurd h hQ, fun h => by omega⟩

/-- The maximum of finitely many positions above a threshold `p`. -/
theorem exists_max (l : List Nat) (f : Nat → Nat) (p B : Nat) (hp : p < B)
    (hf : ∀ x ∈ l, f x < B) :
    ∃ c, p ≤ c ∧ c < B ∧ ∀ i, p < i → ((∃ x ∈ l, i ≤ f x) ↔ i ≤ c) := by
  induction l with
  | nil => exact ⟨p, le_refl p, hp, fun i hi => by simp; omega⟩
  | cons x t ih =>
    obtain ⟨c', hpc', hc'B, hc'⟩ := ih (fun y hy => hf y (List.mem_cons_of_mem x hy))
    refine ⟨max (f x) c', le_trans hpc' (le_max_right _ _), ?_, fun i hi => ?_⟩
    · exact max_lt (hf x (by simp)) hc'B
    · constructor
      · rintro ⟨y, hy, hiy⟩
        rcases List.mem_cons.1 hy with rfl | hy
        · exact le_max_of_le_left hiy
        · exact le_max_of_le_right ((hc' i hi).1 ⟨y, hy, hiy⟩)
      · intro hm
        rcases le_max_iff.1 hm with h1 | h1
        · exact ⟨x, by simp, h1⟩
        · obtain ⟨y, hy, hiy⟩ := (hc' i hi).2 h1
          exact ⟨y, List.mem_cons_of_mem x hy, hiy⟩

/-- The minimum of positions of a list, capped at `B`: `∃ x, f x ≤ c` is `a ≤ c` for `c < B`. -/
theorem exists_lower (l : List Nat) (f : Nat → Nat) (B : Nat) :
    ∃ a, a ≤ B ∧ ∀ c, c < B → ((∃ x ∈ l, f x ≤ c) ↔ a ≤ c) := by
  induction l with
  | nil => exact ⟨B, le_refl B, fun c hc => by simp; omega⟩
  | cons x t ih =>
    obtain ⟨a', ha'B, ha'⟩ := ih
    refine ⟨min (f x) a', le_trans (min_le_right _ _) ha'B, fun c hc => ?_⟩
    constructor
    · rintro ⟨y, hy, hyc⟩
      rcases List.mem_cons.1 hy with rfl | hy
      · exact le_trans (min_le_left _ _) hyc
      · exact le_trans (min_le_right _ _) ((ha' c hc).1 ⟨y, hy, hyc⟩)
    · intro hm
      rcases min_le_iff.1 hm with h1 | h1
      · exact ⟨x, by simp, h1⟩
      · obtain ⟨y, hy, hyc⟩ := (ha' c hc).2 h1
        exact ⟨y, List.mem_cons_of_mem x hy, hyc⟩



/-! ## Small helpers -/

theorem q_mem {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q) {x : Nat} :
    x ∈ q ↔ x ∈ G.nodes ∧ wpF G Y x = true := by
  rw [h.qmem, List.mem_filter]

theorem idx_of_low {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {x : Nat} (hx : x ∈ G.nodes) (hl : isLow Y x = true) : order.idxOf x < nLow G Y :=
  (h.low_iff hx).1 hl

theorem idx_of_high {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {x : Nat} (hx : x ∈ G.nodes) (hl : isLow Y x = false) : nLow G Y ≤ order.idxOf x := by
  by_contra hc
  have h1 : isLow Y x = true := (h.low_iff hx).2 (by omega)
  rw [hl] at h1
  exact absurd h1 (by simp)

theorem idx_lt_length {G : Graph} {Y : Labels} {order q : List Nat} (h : OrdOK G Y order q)
    {x : Nat} (hx : x ∈ G.nodes) : order.idxOf x < order.length :=
  List.idxOf_lt_length_iff.2 (h.mem.2 hx)

theorem subsetB_iff {S B : List Nat} : subsetB S B = true ↔ ∀ x ∈ S, x ∈ B := by
  simp [subsetB, List.all_eq_true]

theorem Qv_down (S q : List Nat) (j k : Nat) (hjk : j ≤ k)
    (hk : subsetB S (q.take (k - 1)) = false) : subsetB S (q.take (j - 1)) = false := by
  cases hj : subsetB S (q.take (j - 1))
  · rfl
  · exfalso
    have hsub := subsetB_iff.1 hj
    have hmono : q.take (j - 1) ⊆ q.take (k - 1) := List.take_subset_take_left q (by omega)
    have h2 : subsetB S (q.take (k - 1)) = true := subsetB_iff.2 (fun x hx => hmono (hsub x hx))
    rw [hk] at h2
    exact absurd h2 (by simp)

theorem Qv_zero (S q : List Nat) (hS : ∃ x, x ∈ S) : subsetB S (q.take (0 - 1)) = false := by
  obtain ⟨x, hx⟩ := hS
  cases hc : subsetB S (q.take (0 - 1))
  · rfl
  · have := subsetB_iff.1 hc x hx
    simp at this

/-- Outer blocks never contain a low node. -/
theorem not_out_low {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {k v : Nat} (hk : k < order.length - nLow G Y) (hv : v ∈ G.nodes)
    (hl : isLow Y v = true) : v ∉ outB G Y order k := by
  intro h3
  have hlt := idx_of_low h hv hl
  rcases (mem_out hG h hk hv).1 h3 with h4 | ⟨h4, _⟩ <;> omega

/-- The inner bag at `g` contains a low node `v` iff its position is at most `g`, when `v`
has a high neighbour. -/
theorem inner_of_high_nbr {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v x0 : Nat} (hv : v ∈ G.nodes) (hx0 : x0 ∈ G.nbrs v)
    (hx0h : isLow Y x0 = false) {g : Nat} (hg : g < nLow G Y) :
    v ∈ innerB G order g ↔ order.idxOf v ≤ g := by
  rw [mem_inner hG h hg hv]
  have hx0i : nLow G Y ≤ order.idxOf x0 := idx_of_high h (hG.nbrs_sub v x0 hx0) hx0h
  constructor
  · rintro (h1 | ⟨h1, _⟩) <;> omega
  · intro hle
    by_cases heq : order.idxOf v = g
    · exact Or.inl heq
    · exact Or.inr ⟨by omega, x0, hx0, by omega⟩


/-! ## Low nodes -/

/-- Low node in `D`: inner bags up to `nLow - 1`, `C_{-1}`, and all `C_j`. -/
theorem case_LA {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hl : isLow Y v = true)
    (hd : inD G Y v = true) (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      order.idxOf v ≤ g ∧ g ≤ nLow G Y + 1 + q.length := by
  obtain ⟨x0, hx0, hx0h⟩ := (inU_iff.1 (inU_of_inD_low hd hl)).2
  have hpl := idx_of_low h hv hl
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, _⟩ | ⟨h1, h2, _⟩ | ⟨h1, h2, h3⟩)
    · rw [inner_of_high_nbr hG h hv hx0 hx0h h1] at h2
      omega
    · omega
    · omega
    · exact absurd h3 (not_out_low hG h h2 hv hl)
  · rintro ⟨hh1, hh2⟩
    by_cases h1 : g < nLow G Y
    · exact Or.inl ⟨h1, (inner_of_high_nbr hG h hv hx0 hx0h h1).2 hh1⟩
    · by_cases h2 : g = nLow G Y
      · exact Or.inr (Or.inl ⟨h2, mem_cm1.2 ⟨hv, Or.inl (inU_of_inD_low hd hl)⟩⟩)
      · exact Or.inr (Or.inr (Or.inl ⟨by omega, hh2,
          mem_cs.2 (Or.inl ⟨hv, hd⟩)⟩))

/-- Low node in `U \ D` with a neighbour in `W'`, threshold `J` for `C_j`. -/
theorem case_LB {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hl : isLow Y v = true)
    (hnd : inD G Y v = false) (hu : inU G Y v = true)
    (hw : ∃ x ∈ G.nbrs v, wpF G Y x = true) {J : Nat} (hJL : J ≤ q.length)
    (hJ : ∀ j, j ≤ q.length → (subsetB (eSet G Y v) (q.take (j - 1)) = false ↔ j ≤ J))
    (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      order.idxOf v ≤ g ∧ g ≤ nLow G Y + 1 + J := by
  obtain ⟨x0, hx0, hx0h⟩ := (inU_iff.1 hu).2
  have hpl := idx_of_low h hv hl
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, _⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩)
    · rw [inner_of_high_nbr hG h hv hx0 hx0h h1] at h2
      omega
    · omega
    · rcases (mem_cs).1 h3 with ⟨_, h4⟩ | ⟨_, _, h4, _, h5⟩ | h6
      · rw [hnd] at h4
        exact absurd h4 (by simp)
      · have := (hJ _ (by omega)).1 h5
        exact ⟨by omega, by omega⟩
      · have hvq := (q_mem h).1 (List.mem_of_mem_take h6)
        have h7 := (wpF_iff.1 hvq.2).1.1
        rw [hl] at h7
        exact absurd h7 (by simp)
    · exact absurd h3 (not_out_low hG h h2 hv hl)
  · rintro ⟨hh1, hh2⟩
    by_cases h1 : g < nLow G Y
    · exact Or.inl ⟨h1, (inner_of_high_nbr hG h hv hx0 hx0h h1).2 hh1⟩
    · by_cases h2 : g = nLow G Y
      · exact Or.inr (Or.inl ⟨h2, mem_cm1.2 ⟨hv, Or.inl hu⟩⟩)
      · refine Or.inr (Or.inr (Or.inl ⟨by omega, by omega, mem_cs.2 (Or.inr (Or.inl ⟨hv, hu, hnd, hw, ?_⟩))⟩))
        exact (hJ _ (by omega)).2 (by omega)

/-- Low node in `U \ D` without a neighbour in `W'`: inner bags and `C_{-1}` only. -/
theorem case_LC {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hl : isLow Y v = true)
    (hnd : inD G Y v = false) (hu : inU G Y v = true)
    (hw : ¬ ∃ x ∈ G.nbrs v, wpF G Y x = true) (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      order.idxOf v ≤ g ∧ g ≤ nLow G Y := by
  obtain ⟨x0, hx0, hx0h⟩ := (inU_iff.1 hu).2
  have hpl := idx_of_low h hv hl
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, _⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩)
    · rw [inner_of_high_nbr hG h hv hx0 hx0h h1] at h2
      omega
    · omega
    · rcases (mem_cs).1 h3 with ⟨_, h4⟩ | ⟨_, _, _, h4, _⟩ | h6
      · rw [hnd] at h4
        exact absurd h4 (by simp)
      · exact absurd h4 hw
      · have hvq := (q_mem h).1 (List.mem_of_mem_take h6)
        have h7 := (wpF_iff.1 hvq.2).1.1
        rw [hl] at h7
        exact absurd h7 (by simp)
    · exact absurd h3 (not_out_low hG h h2 hv hl)
  · rintro ⟨hh1, hh2⟩
    by_cases h1 : g < nLow G Y
    · exact Or.inl ⟨h1, (inner_of_high_nbr hG h hv hx0 hx0h h1).2 hh1⟩
    · have h2 : g = nLow G Y := by omega
      exact Or.inr (Or.inl ⟨h2, mem_cm1.2 ⟨hv, Or.inl hu⟩⟩)

/-- Low node not in `U`: its inner bags reach up to a bound `c < nLow`. -/
theorem case_LD {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hl : isLow Y v = true)
    (hnu : inU G Y v = false) {c : Nat} (hcl : c < nLow G Y) (hpc : order.idxOf v ≤ c)
    (hc : ∀ i, order.idxOf v < i → ((∃ x ∈ G.nbrs v, i ≤ order.idxOf x) ↔ i ≤ c))
    (g : Nat) :
    InBag (layoutB G Y order q) g v ↔ order.idxOf v ≤ g ∧ g ≤ c := by
  have hpl := idx_of_low h hv hl
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩)
    · rw [mem_inner hG h h1 hv] at h2
      rcases h2 with h2 | ⟨h2, x, hx, hx2⟩
      · omega
      · exact ⟨by omega, (hc g h2).1 ⟨x, hx, hx2⟩⟩
    · have := mem_cm1.1 h2
      rcases this with ⟨_, h4 | ⟨h4, _⟩⟩
      · rw [hnu] at h4
        exact absurd h4 (by simp)
      · have := inU_of_inD_low h4 hl
        rw [hnu] at this
        exact absurd this (by simp)
    · rcases (mem_cs).1 h3 with ⟨_, h4⟩ | ⟨_, h4, _⟩ | h6
      · have := inU_of_inD_low h4 hl
        rw [hnu] at this
        exact absurd this (by simp)
      · rw [hnu] at h4
        exact absurd h4 (by simp)
      · have hvq := (q_mem h).1 (List.mem_of_mem_take h6)
        have h7 := (wpF_iff.1 hvq.2).1.1
        rw [hl] at h7
        exact absurd h7 (by simp)
    · exact absurd h3 (not_out_low hG h h2 hv hl)
  · rintro ⟨hh1, hh2⟩
    have h1 : g < nLow G Y := by omega
    refine Or.inl ⟨h1, (mem_inner hG h h1 hv).2 ?_⟩
    by_cases heq : order.idxOf v = g
    · exact Or.inl heq
    · exact Or.inr ⟨by omega, (hc g (by omega)).2 hh2⟩

/-! ## High nodes -/

/-- High node in `D`: `C_{-1}`, all `C_j`, and outer bags up to its own index. -/
theorem case_HA {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hh : isLow Y v = false)
    (hd : inD G Y v = true) (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      nLow G Y ≤ g ∧ g ≤ order.idxOf v + 2 + q.length := by
  have hpi := idx_of_high h hv hh
  obtain ⟨x0, hx0, hx0h⟩ := (inW_iff.1 (inW_of_inD_high hd hh)).2
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, _⟩ | ⟨h1, h2, h3⟩)
    · have := (mem_inner hG h h1 hv).1 h2
      omega
    · omega
    · omega
    · have := (mem_out hG h h2 hv).1 h3
      rcases this with h4 | ⟨h4, _⟩ <;> omega
  · rintro ⟨hh1, hh2⟩
    by_cases h1 : g ≤ nLow G Y
    · have h2 : g = nLow G Y := by omega
      exact Or.inr (Or.inl ⟨h2, mem_cm1.2 ⟨hv, Or.inr ⟨hd, inW_of_inD_high hd hh⟩⟩⟩)
    · by_cases h3 : g ≤ nLow G Y + 1 + q.length
      · exact Or.inr (Or.inr (Or.inl ⟨by omega, h3, mem_cs.2 (Or.inl ⟨hv, hd⟩)⟩))
      · have hk : g - (nLow G Y + 2 + q.length) < order.length - nLow G Y := by
          have := idx_lt_length h hv
          omega
        refine Or.inr (Or.inr (Or.inr ⟨by omega, hk, ?_⟩))
        rw [mem_out hG h hk hv]
        by_cases heq : nLow G Y + (g - (nLow G Y + 2 + q.length)) = order.idxOf v
        · exact Or.inl (by omega)
        · exact Or.inr ⟨by omega, x0, hx0, by have := idx_of_low h (hG.nbrs_sub v x0 hx0) hx0h; omega⟩

/-- High node in `W \ D` (so in `q`): `C_j` for `j` beyond its first position in `q`, and
outer bags up to its own index. -/
theorem case_HB {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hh : isLow Y v = false)
    (hvq : v ∈ q) (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      nLow G Y + 2 + q.idxOf v ≤ g ∧ g ≤ order.idxOf v + 2 + q.length := by
  have hwp := (q_mem h).1 hvq
  have hwpi := wpF_iff.1 hwp.2
  have hnd : inD G Y v = false := hwpi.2
  obtain ⟨x0, hx0, hx0h⟩ := hwpi.1.2
  have hpi := idx_of_high h hv hh
  have hfq : q.idxOf v < q.length := List.idxOf_lt_length_iff.2 hvq
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩)
    · have := (mem_inner hG h h1 hv).1 h2
      rcases this with h4 | ⟨h4, _⟩ <;> omega
    · rcases mem_cm1.1 h2 with ⟨_, h4 | ⟨h4, _⟩⟩
      · have h5 : isLow Y v = true := (inU_iff.1 h4).1
        rw [hh] at h5
        exact absurd h5 (by simp)
      · rw [hnd] at h4
        exact absurd h4 (by simp)
    · rcases (mem_cs).1 h3 with ⟨_, h4⟩ | ⟨_, h4, _⟩ | h6
      · rw [hnd] at h4
        exact absurd h4 (by simp)
      · have h5 : isLow Y v = true := (inU_iff.1 h4).1
        rw [hh] at h5
        exact absurd h5 (by simp)
      · have h7 := (List.mem_take_iff_idxOf_lt hvq).1 h6
        exact ⟨by omega, by omega⟩
    · rcases (mem_out hG h h2 hv).1 h3 with h4 | ⟨h4, _⟩ <;> omega
  · rintro ⟨hh1, hh2⟩
    by_cases h1 : g ≤ nLow G Y + 1 + q.length
    · exact Or.inr (Or.inr (Or.inl ⟨by omega, h1,
        mem_cs.2 (Or.inr (Or.inr ((List.mem_take_iff_idxOf_lt hvq).2 (by omega))))⟩))
    · have hk : g - (nLow G Y + 2 + q.length) < order.length - nLow G Y := by
        have := idx_lt_length h hv
        omega
      refine Or.inr (Or.inr (Or.inr ⟨by omega, hk, ?_⟩))
      rw [mem_out hG h hk hv]
      by_cases heq : nLow G Y + (g - (nLow G Y + 2 + q.length)) = order.idxOf v
      · exact Or.inl (by omega)
      · refine Or.inr ⟨by omega, x0, hx0, ?_⟩
        have := idx_of_low h (hG.nbrs_sub v x0 hx0) hx0h
        omega

/-- High node not in `W` (so not in `q`, not in `D`): only outer bags, from the first
position of a neighbour (`a`) up to its own index. -/
theorem case_HC {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) (hh : isLow Y v = false)
    (hw : ¬ inW G Y v = true) {a : Nat} (ha : a ≤ order.idxOf v)
    (hac : ∀ c, c < order.idxOf v → ((∃ x ∈ G.nbrs v, order.idxOf x ≤ c) ↔ a ≤ c))
    (g : Nat) :
    InBag (layoutB G Y order q) g v ↔
      a + 2 + q.length ≤ g ∧ g ≤ order.idxOf v + 2 + q.length := by
  have hpi := idx_of_high h hv hh
  have hnl : ∀ x ∈ G.nbrs v, nLow G Y ≤ order.idxOf x := by
    intro x hx
    by_contra hc
    have hxl : isLow Y x = true := (h.low_iff (hG.nbrs_sub v x hx)).2 (by omega)
    exact hw (inW_iff.2 ⟨hh, x, hx, hxl⟩)
  have hanL : nLow G Y ≤ a := by
    by_contra hc
    obtain ⟨x, hx, hxa⟩ := (hac a (by omega)).2 le_rfl
    have := hnl x hx
    omega
  rw [inBag_layout]
  constructor
  · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, h3⟩ | ⟨h1, h2, h3⟩)
    · rcases (mem_inner hG h h1 hv).1 h2 with h4 | ⟨h4, _⟩ <;> omega
    · rcases mem_cm1.1 h2 with ⟨_, h4 | ⟨h4, _⟩⟩
      · have h5 : isLow Y v = true := (inU_iff.1 h4).1
        rw [hh] at h5
        exact absurd h5 (by simp)
      · exact absurd (inW_of_inD_high h4 hh) hw
    · rcases (mem_cs).1 h3 with ⟨_, h4⟩ | ⟨_, h4, _⟩ | h6
      · exact absurd (inW_of_inD_high h4 hh) hw
      · have h5 : isLow Y v = true := (inU_iff.1 h4).1
        rw [hh] at h5
        exact absurd h5 (by simp)
      · have hwp := (q_mem h).1 (List.mem_of_mem_take h6)
        exact absurd (inW_iff.2 (wpF_iff.1 hwp.2).1) hw
    · rcases (mem_out hG h h2 hv).1 h3 with h4 | ⟨h4, x, hx, hx2⟩
      · omega
      · have := (hac (nLow G Y + (g - (nLow G Y + 2 + q.length))) h4).1 ⟨x, hx, hx2⟩
        omega
  · rintro ⟨hh1, hh2⟩
    have hk : g - (nLow G Y + 2 + q.length) < order.length - nLow G Y := by
      have := idx_lt_length h hv
      omega
    refine Or.inr (Or.inr (Or.inr ⟨by omega, hk, ?_⟩))
    rw [mem_out hG h hk hv]
    by_cases heq : nLow G Y + (g - (nLow G Y + 2 + q.length)) = order.idxOf v
    · exact Or.inl (by omega)
    · obtain ⟨x, hx, hx2⟩ := (hac (nLow G Y + (g - (nLow G Y + 2 + q.length))) (by omega)).2
        (by omega)
      exact Or.inr ⟨by omega, x, hx, hx2⟩

/-- Every node occupies an interval of bag indices, with explicit ends. -/
theorem vertex_interval {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {v : Nat} (hv : v ∈ G.nodes) :
    ∃ a b, a ≤ b ∧ ∀ g, InBag (layoutB G Y order q) g v ↔ a ≤ g ∧ g ≤ b := by
  by_cases hl : isLow Y v = true
  · have hpl := idx_of_low h hv hl
    by_cases hd : inD G Y v = true
    · exact ⟨order.idxOf v, nLow G Y + 1 + q.length, by omega,
        fun g => case_LA hG h hv hl hd g⟩
    · have hd' : inD G Y v = false := by simpa using hd
      by_cases hu : inU G Y v = true
      · by_cases hw : ∃ x ∈ G.nbrs v, wpF G Y x = true
        · have hdown : ∀ j k, j ≤ k → subsetB (eSet G Y v) (q.take (k - 1)) = false →
              subsetB (eSet G Y v) (q.take (j - 1)) = false :=
            fun j k hjk hk => Qv_down _ q j k hjk hk
          have hz : subsetB (eSet G Y v) (q.take (0 - 1)) = false := by
            obtain ⟨x, hx, hwx⟩ := hw
            exact Qv_zero _ q ⟨x, List.mem_filter.2 ⟨hx, hwx⟩⟩
          obtain ⟨J, hJL, hJ⟩ := exists_thr (fun j => subsetB (eSet G Y v) (q.take (j - 1)) = false)
            hdown hz q.length
          exact ⟨order.idxOf v, nLow G Y + 1 + J, by omega,
            fun g => case_LB hG h hv hl hd' hu hw hJL (fun j hj => hJ j hj) g⟩
        · have hw' : ¬ ∃ x ∈ G.nbrs v, wpF G Y x = true := hw
          exact ⟨order.idxOf v, nLow G Y, by omega, fun g => case_LC hG h hv hl hd' hu hw' g⟩
      · have hnu : inU G Y v = false := by simpa using hu
        have hall : ∀ x ∈ G.nbrs v, order.idxOf x < nLow G Y := by
          intro x hx
          apply idx_of_low h (hG.nbrs_sub v x hx)
          by_contra hc
          have hx0 : isLow Y x = false := by simpa using hc
          exact hu (inU_iff.2 ⟨hl, x, hx, hx0⟩)
        obtain ⟨c, hpc, hcl, hc⟩ := exists_max (G.nbrs v) (fun x => order.idxOf x)
          (order.idxOf v) (nLow G Y) hpl hall
        exact ⟨order.idxOf v, c, hpc, fun g => case_LD hG h hv hl hnu hcl hpc hc g⟩
  · have hh : isLow Y v = false := by simpa using hl
    have hpi := idx_of_high h hv hh
    by_cases hd : inD G Y v = true
    · exact ⟨nLow G Y, order.idxOf v + 2 + q.length, by omega, fun g => case_HA hG h hv hh hd g⟩
    · have hd' : inD G Y v = false := by simpa using hd
      by_cases hw : inW G Y v = true
      · have hvq : v ∈ q := (q_mem h).2 ⟨hv, wpF_iff.2 ⟨inW_iff.1 hw, hd'⟩⟩
        have hfq : q.idxOf v < q.length := List.idxOf_lt_length_iff.2 hvq
        exact ⟨nLow G Y + 2 + q.idxOf v, order.idxOf v + 2 + q.length, by omega,
          fun g => case_HB hG h hv hh hvq g⟩
      · obtain ⟨a, ha, hac⟩ := exists_lower (G.nbrs v) (fun x => order.idxOf x) (order.idxOf v)
        exact ⟨a + 2 + q.length, order.idxOf v + 2 + q.length, by omega,
          fun g => case_HC hG h hv hh hw ha hac g⟩


/-! ## Edges -/

/-- Two low nodes `a` (earlier) and `b` (later) adjacent: inner bag of `b`. -/
theorem edge_LL {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {a b : Nat} (ha : a ∈ G.nodes) (hb : b ∈ G.nodes)
    (_hla : isLow Y a = true) (hlb : isLow Y b = true) (hab : b ∈ G.nbrs a)
    (hlt : order.idxOf a < order.idxOf b) :
    InBag (layoutB G Y order q) (order.idxOf b) a ∧
      InBag (layoutB G Y order q) (order.idxOf b) b := by
  have hbl := idx_of_low h hb hlb
  constructor
  · rw [inBag_layout]
    exact Or.inl ⟨hbl, (mem_inner hG h hbl ha).2 (Or.inr ⟨hlt, b, hab, le_rfl⟩)⟩
  · rw [inBag_layout]
    exact Or.inl ⟨hbl, (mem_inner hG h hbl hb).2 (Or.inl rfl)⟩

/-- Two high nodes `a` (earlier) and `b` (later) adjacent: outer bag of `a`. -/
theorem edge_HH {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {a b : Nat} (ha : a ∈ G.nodes) (hb : b ∈ G.nodes)
    (hha : isLow Y a = false) (_hhb : isLow Y b = false) (hab : a ∈ G.nbrs b)
    (hlt : order.idxOf a < order.idxOf b) :
    InBag (layoutB G Y order q) (order.idxOf a + 2 + q.length) a ∧
      InBag (layoutB G Y order q) (order.idxOf a + 2 + q.length) b := by
  have hpa := idx_of_high h ha hha
  have hlen := idx_lt_length h ha
  have hk : order.idxOf a + 2 + q.length - (nLow G Y + 2 + q.length) < order.length - nLow G Y := by
    omega
  constructor
  · rw [inBag_layout]
    exact Or.inr (Or.inr (Or.inr ⟨by omega, hk,
      (mem_out hG h hk ha).2 (Or.inl (by omega))⟩))
  · rw [inBag_layout]
    exact Or.inr (Or.inr (Or.inr ⟨by omega, hk,
      (mem_out hG h hk hb).2 (Or.inr ⟨by omega, a, hab, by omega⟩)⟩))

/-- A low node `u` adjacent to a high node `x`. -/
theorem edge_LH {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {u x : Nat} (hu : u ∈ G.nodes) (hx : x ∈ G.nodes)
    (hlu : isLow Y u = true) (hhx : isLow Y x = false) (hux : x ∈ G.nbrs u) :
    ∃ g, InBag (layoutB G Y order q) g u ∧ InBag (layoutB G Y order q) g x := by
  have hxu : u ∈ G.nbrs x := hG.symm u x hux
  have hpx := idx_of_high h hx hhx
  by_cases hdx : inD G Y x = true
  · refine ⟨nLow G Y, ?_, ?_⟩
    · rw [inBag_layout]
      exact Or.inr (Or.inl ⟨rfl, mem_cm1.2 ⟨hu, Or.inl (inU_iff.2 ⟨hlu, x, hux, hhx⟩)⟩⟩)
    · rw [inBag_layout]
      exact Or.inr (Or.inl ⟨rfl, mem_cm1.2 ⟨hx, Or.inr ⟨hdx, inW_of_inD_high hdx hhx⟩⟩⟩)
  · have hdx' : inD G Y x = false := by simpa using hdx
    have hwpx : wpF G Y x = true := wpF_iff.2 ⟨⟨hhx, u, hxu, hlu⟩, hdx'⟩
    have hxq : x ∈ q := (q_mem h).2 ⟨hx, hwpx⟩
    have hfq : q.idxOf x < q.length := List.idxOf_lt_length_iff.2 hxq
    by_cases hdu : inD G Y u = true
    · refine ⟨nLow G Y + 1 + q.length, ?_, ?_⟩
      · rw [inBag_layout]
        refine Or.inr (Or.inr (Or.inl ⟨by omega, by omega, mem_cs.2 (Or.inl ⟨hu, hdu⟩)⟩))
      · rw [inBag_layout]
        refine Or.inr (Or.inr (Or.inl ⟨by omega, by omega, mem_cs.2 (Or.inr (Or.inr ?_))⟩))
        exact (List.mem_take_iff_idxOf_lt hxq).2 (by omega)
    · have hdu' : inD G Y u = false := by simpa using hdu
      have hf : nLow G Y + 2 + q.idxOf x - (nLow G Y + 1) - 1 = q.idxOf x := by omega
      refine ⟨nLow G Y + 2 + q.idxOf x, ?_, ?_⟩
      · rw [inBag_layout]
        refine Or.inr (Or.inr (Or.inl ⟨by omega, by omega, mem_cs.2 (Or.inr (Or.inl ?_))⟩))
        refine ⟨hu, inU_iff.2 ⟨hlu, x, hux, hhx⟩, hdu', ⟨x, hux, hwpx⟩, ?_⟩
        rw [hf]
        cases hc : subsetB (eSet G Y u) (q.take (q.idxOf x)) with
        | false => rfl
        | true =>
          have hm := subsetB_iff.1 hc x (List.mem_filter.2 ⟨hux, hwpx⟩)
          rw [List.mem_take_iff_idxOf_lt hxq] at hm
          omega
      · rw [inBag_layout]
        refine Or.inr (Or.inr (Or.inl ⟨by omega, by omega, mem_cs.2 (Or.inr (Or.inr ?_))⟩))
        exact (List.mem_take_iff_idxOf_lt hxq).2 (by omega)

/-- Every edge lies in one block. -/
theorem edge_covered {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) {u x : Nat} (hu : u ∈ G.nodes) (hx : x ∈ G.nodes)
    (hux : x ∈ G.nbrs u) :
    ∃ g, InBag (layoutB G Y order q) g u ∧ InBag (layoutB G Y order q) g x := by
  have hxu : u ∈ G.nbrs x := hG.symm u x hux
  have hne : u ≠ x := by
    intro e
    subst e
    exact hG.loopless _ hux
  by_cases hlu : isLow Y u = true
  · by_cases hlx : isLow Y x = true
    · rcases lt_trichotomy (order.idxOf u) (order.idxOf x) with hlt | heq | hgt
      · obtain ⟨h1, h2⟩ := edge_LL hG h hu hx hlu hlx hux hlt
        exact ⟨_, h1, h2⟩
      · exfalso
        apply hne
        calc u = order.getD (order.idxOf u) 0 := (getD_idxOf (h.mem.2 hu)).symm
          _ = order.getD (order.idxOf x) 0 := by rw [heq]
          _ = x := getD_idxOf (h.mem.2 hx)
      · obtain ⟨h1, h2⟩ := edge_LL hG h hx hu hlx hlu hxu hgt
        exact ⟨_, h2, h1⟩
    · have hhx : isLow Y x = false := by simpa using hlx
      exact edge_LH hG h hu hx hlu hhx hux
  · have hhu : isLow Y u = false := by simpa using hlu
    by_cases hlx : isLow Y x = true
    · obtain ⟨g, h1, h2⟩ := edge_LH hG h hx hu hlx hhu hxu
      exact ⟨g, h2, h1⟩
    · have hhx : isLow Y x = false := by simpa using hlx
      rcases lt_trichotomy (order.idxOf u) (order.idxOf x) with hlt | heq | hgt
      · obtain ⟨h1, h2⟩ := edge_HH hG h hu hx hhu hhx hxu hlt
        exact ⟨_, h1, h2⟩
      · exfalso
        apply hne
        calc u = order.getD (order.idxOf u) 0 := (getD_idxOf (h.mem.2 hu)).symm
          _ = order.getD (order.idxOf x) 0 := by rw [heq]
          _ = x := getD_idxOf (h.mem.2 hx)
      · obtain ⟨h1, h2⟩ := edge_HH hG h hx hu hhx hhu hux hgt
        exact ⟨_, h2, h1⟩

/-- Two bag indices holding both ends of a pair give a bag holding both. -/
theorem exists_bag_pair {bags : List Bag} {g : Nat} {u x : Nat}
    (h1 : InBag bags g u) (h2 : InBag bags g x) : ∃ B ∈ bags, u ∈ B ∧ x ∈ B := by
  obtain ⟨B1, hB1, hu⟩ := h1
  obtain ⟨B2, hB2, hx⟩ := h2
  rw [hB1] at hB2
  cases hB2
  exact ⟨B1, List.mem_of_getElem? hB1, hu, hx⟩

/-- Every vertex of a block of the layout is a node. -/
theorem getD_mem_order {order : List Nat} {i : Nat} (hi : i < order.length) :
    order.getD i 0 ∈ order := by
  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi]
  simp only [Option.getD_some]
  exact List.getElem_mem hi

theorem layout_valid {G : Graph} {Y : Labels} {order q : List Nat} (hG : G.WF)
    (h : OrdOK G Y order q) :
    ValidPD G (layoutB G Y order q) ∧ BagsWithin G (layoutB G Y order q) := by
  constructor
  · refine ⟨?_, ?_, ?_⟩
    · intro v hv
      obtain ⟨a, b, hab, hI⟩ := vertex_interval hG h hv
      exact ⟨a, (hI a).2 ⟨le_rfl, hab⟩⟩
    · intro v hv i j k hij hjk hi hk
      obtain ⟨a, b, hab, hI⟩ := vertex_interval hG h hv
      exact (hI j).2 ⟨by have := (hI i).1 hi; omega, by have := (hI k).1 hk; omega⟩
    · intro u x hu hux
      obtain ⟨g, h1, h2⟩ := edge_covered hG h hu (hG.nbrs_sub u x hux) hux
      obtain ⟨B, hB, hu', hx'⟩ := exists_bag_pair h1 h2
      exact ⟨B, hB, hu', hx'⟩
  · intro B hB v hv
    unfold layoutB at hB
    simp only [List.mem_append, List.mem_map, List.mem_range, List.mem_singleton] at hB
    rcases hB with ((⟨i, hi, rfl⟩ | rfl) | ⟨j, hj, rfl⟩) | ⟨k, hk, rfl⟩
    · unfold innerB at hv
      have hnl : nLow G Y ≤ order.length := by rw [h.length]; exact nLow_le
      rcases List.mem_cons.1 hv with rfl | hv
      · exact h.mem.1 (getD_mem_order (by omega))
      · exact h.mem.1 (List.mem_of_mem_take (List.mem_of_mem_filter hv))
    · exact (mem_cm1.1 hv).1
    · rcases mem_cs.1 hv with ⟨h1, _⟩ | ⟨h1, _⟩ | h3
      · exact h1
      · exact h1
      · exact ((q_mem h).1 (List.mem_of_mem_take h3)).1
    · unfold outB at hv
      have hnl : nLow G Y ≤ order.length := by rw [h.length]; exact nLow_le
      rcases List.mem_cons.1 hv with rfl | hv
      · exact h.mem.1 (getD_mem_order (by omega))
      · exact (List.mem_filter.1 hv).1


/-! ## Sortedness and the link with `switchedLayout` -/

/-- The key comparator of `switchedOrder` is transitive and total. -/
theorem switchedOrder_pairwise (G : Graph) (Y : Labels) :
    (switchedOrder G Y).Pairwise (fun a b => isLow Y b = true → isLow Y a = true) := by
  have trans : ∀ a b c : Nat,
      (decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))) = true →
      (decide (Y b < Y c) || (decide (Y b = Y c) && decide (b ≤ c))) = true →
      (decide (Y a < Y c) || (decide (Y a = Y c) && decide (a ≤ c))) = true := by
    intro a b c h1 h2
    simp only [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 h1 h2)
    · exact Or.inl (by rw [← h2]; exact h1)
    · exact Or.inl (by rw [h1]; exact h2)
    · exact Or.inr ⟨h1.trans h2, by omega⟩
  have total : ∀ a b : Nat,
      ((decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))) ||
        (decide (Y b < Y a) || (decide (Y b = Y a) && decide (b ≤ a)))) = true := by
    intro a b
    simp only [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.inl (Or.inl h)
    · rcases le_total a b with hab | hab
      · exact Or.inl (Or.inr ⟨h, hab⟩)
      · exact Or.inr (Or.inr ⟨h.symm, hab⟩)
    · exact Or.inr (Or.inl h)
  have hs := List.pairwise_mergeSort trans total G.nodes
  unfold switchedOrder
  refine hs.imp ?_
  intro a b hab hb
  simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at hab
  unfold isLow at hb ⊢
  simp only [decide_eq_true_eq] at hb ⊢
  rcases hab with h | ⟨h, _⟩
  · exact lt_trans h hb
  · rw [h]
    exact hb

theorem switchedLayout_eq (G : Graph) (Y : Labels) :
    switchedLayout G Y = layoutB G Y (switchedOrder G Y)
      (connectorOrder (G.nodes.filter (wpF G Y)) ((pSet G Y).map (eSet G Y))) := by
  unfold switchedLayout switchedLayoutF layoutB innerB outB cm1B csB nLow pSet eSet wpF
  simp only [hs_contains]
  rfl

end C4

/-- Main statement (plan C4): the median-switched layout is valid for every graph and
labeling. -/
theorem switchedLayoutValid_of (hWF : WFBasics) (hP : SwitchedOrderPerm)
    (hC : ConnectorOrderMem) : SwitchedLayoutValid := by
  intro G hG Y
  have hperm : (switchedOrder G Y).Perm G.nodes := hP G Y
  have hsplit : switchedOrder G Y = (switchedOrder G Y).filter (isLow Y) ++
      (switchedOrder G Y).filter (fun x => !isLow Y x) :=
    C4.lows_first (isLow Y) _ (C4.switchedOrder_pairwise G Y)
  have hitems : ∀ e ∈ (C4.pSet G Y).map (C4.eSet G Y), ∀ z ∈ e,
      z ∈ G.nodes.filter (C4.wpF G Y) := by
    intro e he z hz
    obtain ⟨u, _, rfl⟩ := List.mem_map.1 he
    unfold C4.eSet at hz
    obtain ⟨hz1, hz2⟩ := List.mem_filter.1 hz
    exact List.mem_filter.2 ⟨hG.nbrs_sub u z hz1, hz2⟩
  have hqmem : ∀ x, x ∈ connectorOrder (G.nodes.filter (C4.wpF G Y))
      ((C4.pSet G Y).map (C4.eSet G Y)) ↔ x ∈ G.nodes.filter (C4.wpF G Y) :=
    fun x => hC _ _ hitems x
  have hOK : C4.OrdOK G Y (switchedOrder G Y)
      (connectorOrder (G.nodes.filter (C4.wpF G Y)) ((C4.pSet G Y).map (C4.eSet G Y))) :=
    ⟨hperm, hsplit, hqmem⟩
  rw [C4.switchedLayout_eq]
  exact C4.layout_valid hG hOK

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.switchedLayoutValid_of