CubicPathwidth.Alg.Proofs2.L1PlainBags

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

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

/-!
# L1: the bags of the plain sweep (`PlainLayoutBags`)

Task L1 of the formalisation. Imports `Plan2` and the Stage 1 helpers
`C1Perm` (`plainOrderPerm`) and `C2PlainLayout` (`C2.idxOf`, `C2.lastF`, `C2.bagsFrom`).
It does not import any other Stage 2 file.

Idea. `plainLayout G Y = C2.bagsFrom G (C2.idxOf order) order.length` with `order` the
nodup permutation `plainOrder G Y` of the nodes. For a node `v` with position `p`,
`v` lies in bag `i` iff `p ≤ i` and `i ≤ last v`, where `last v` is the largest position
among `v` and its neighbours. Hence `v` is in bag `i` iff `p = i` (then `v = order[i]`)
or `p < i` and some neighbour sits at a position `≥ i` (then `v ∈ take i` and that
neighbour is outside `take i`).
-/

namespace CubicPathwidth.Alg

open Graph

namespace L1

/-- The position map of a list, read off the `zipIdx` fold, for a nodup list. -/
theorem idxMap_getD (l : List Nat) (hl : l.Nodup) :
    ∀ (off : Nat) (m : Std.HashMap Nat Nat) (k : Nat),
      ((l.zipIdx off).foldl (fun m p => m.insert p.1 p.2) m).getD k 0 =
        (if k ∈ l then off + l.idxOf k else m.getD k 0) := by
  induction l with
  | nil => intro off m k; simp
  | cons a l ih =>
    intro off m k
    rw [List.nodup_cons] at hl
    obtain ⟨ha, hl⟩ := hl
    rw [List.zipIdx_cons, List.foldl_cons, ih hl (off + 1) (m.insert a off) k]
    by_cases hka : k = a
    · subst hka
      have hk : k ∉ l := ha
      simp [hk]
    · have hk : (a == k) = false := by simp [Ne.symm hka]
      simp [List.idxOf_cons, Std.HashMap.getD_insert, hk, hka]
      split_ifs <;> simp_all
      all_goals omega

/-- `C2.idxOf` of a nodup list is the position of its members. -/
theorem idxOf_mem (order : List Nat) (hnd : order.Nodup) (v : Nat) (hv : v ∈ order) :
    C2.idxOf order v = order.idxOf v := by
  unfold C2.idxOf
  rw [idxMap_getD order hnd 0 ∅ v]
  simp [hv]

/-- The position of `order[i]` is `i`. -/
theorem idxOf_getElem_pos (order : List Nat) (hnd : order.Nodup) (i : Nat)
    (hi : i < order.length) : C2.idxOf order order[i] = i := by
  rw [idxOf_mem order hnd _ (List.getElem_mem hi)]
  exact hnd.idxOf_getElem i hi

/-- Membership in a prefix, read off the position. -/
theorem mem_take_iff_idxOf (order : List Nat) (hnd : order.Nodup) (v : Nat)
    (hv : v ∈ order) (i : Nat) : v ∈ order.take i ↔ order.idxOf v < i := by
  rw [List.mem_take_iff_getElem]
  constructor
  · rintro ⟨j, hj, rfl⟩
    rw [hnd.idxOf_getElem j (lt_of_lt_of_le hj (min_le_right _ _))]
    exact lt_of_lt_of_le hj (min_le_left _ _)
  · intro h
    have hlt : order.idxOf v < order.length := List.idxOf_lt_length_of_mem hv
    refine ⟨order.idxOf v, lt_min h hlt, ?_⟩
    exact List.getElem_idxOf hlt

/-- `v = order[i]` exactly when `v` sits at position `i`. -/
theorem eq_getElem_iff_idxOf (order : List Nat) (hnd : order.Nodup) (v : Nat)
    (hv : v ∈ order) (i : Nat) (hi : i < order.length) :
    v = order[i] ↔ order.idxOf v = i := by
  constructor
  · rintro rfl
    exact hnd.idxOf_getElem i hi
  · intro h
    have hlt : order.idxOf v < order.length := List.idxOf_lt_length_of_mem hv
    subst h
    exact (List.getElem_idxOf hlt).symm

/-- Position of a bag condition through the `lastF` maximum. -/
theorem le_foldl_max_iff (f : Nat → Nat) (i : Nat) : ∀ (l : List Nat) (a : Nat),
    i ≤ l.foldl (fun m u => max m (f u)) a ↔ i ≤ a ∨ ∃ u ∈ l, i ≤ f u
  | [], a => by simp
  | u :: l, a => by
    rw [List.foldl_cons, le_foldl_max_iff f i l (max a (f u))]
    constructor
    · rintro (h | ⟨x, hx, h⟩)
      · rcases le_max_iff.1 h with h | h
        · exact Or.inl h
        · exact Or.inr ⟨u, List.mem_cons_self, h⟩
      · exact Or.inr ⟨x, List.mem_cons_of_mem _ hx, h⟩
    · rintro (h | ⟨x, hx, h⟩)
      · exact Or.inl (le_max_of_le_left h)
      · rcases List.mem_cons.1 hx with rfl | hx
        · exact Or.inl (le_max_of_le_right h)
        · exact Or.inr ⟨x, hx, h⟩

theorem le_lastF_iff (G : Graph) (idx : Nat → Nat) (i v : Nat) :
    i ≤ C2.lastF G idx v ↔ i ≤ idx v ∨ ∃ u ∈ G.nbrs v, i ≤ idx u :=
  le_foldl_max_iff idx i (G.nbrs v) (idx v)

theorem plainLayout_eq (G : Graph) (Y : Labels) :
    plainLayout G Y = C2.bagsFrom G (C2.idxOf (plainOrder G Y)) (plainOrder G Y).length :=
  rfl

/-- `PlainLayoutBags` for one graph and labeling (the two conjuncts are proved together). -/
theorem plainLayoutBags_aux (G : Graph) (hG : G.WF) (Y : Labels) :
    (plainLayout G Y).length = G.numNodes ∧
    ∀ i, i < G.numNodes → ∀ v,
      v ∈ (plainLayout G Y).getD i [] ↔
        v = (plainOrder G Y).getD i 0 ∨
          (v ∈ (plainOrder G Y).take i ∧ ∃ x ∈ G.nbrs v, x ∉ (plainOrder G Y).take i) := by
  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 hidx : ∀ w, w ∈ plainOrder G Y → C2.idxOf (plainOrder G Y) w =
      (plainOrder G Y).idxOf w := fun w hw => idxOf_mem _ hnd w hw
  refine ⟨?_, ?_⟩
  · rw [plainLayout_eq, C2.bagsFrom, List.length_map, List.length_range, hlen]
  · intro i hi v
    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 : (plainLayout G Y).getD i [] =
        G.nodes.filter fun w => C2.idxOf (plainOrder G Y) w ≤ i &&
          i ≤ C2.lastF G (C2.idxOf (plainOrder G Y)) w := by
      simp [plainLayout_eq, C2.bagsFrom, List.getD_eq_getElem?_getD, hi']
    -- neighbours of a node lie in the order; they are outside `take i` iff at position `≥ i`
    have hnb : ∀ x ∈ G.nbrs v, x ∈ plainOrder G Y ∧
        (x ∉ (plainOrder G Y).take i ↔ i ≤ (plainOrder G Y).idxOf x) := by
      intro x hx
      have hxo : x ∈ plainOrder G Y := (hmem x).2 (hG.nbrs_sub v x hx)
      refine ⟨hxo, ?_⟩
      rw [mem_take_iff_idxOf _ hnd x hxo i, not_lt]
    rw [hbag, hget]
    simp only [List.mem_filter, Bool.and_eq_true, decide_eq_true_eq]
    constructor
    · rintro ⟨hvn, hle1, hle2⟩
      have hvo : v ∈ plainOrder G Y := (hmem v).2 hvn
      rw [hidx v hvo] at hle1
      rw [le_lastF_iff] at hle2
      rcases Nat.lt_or_ge ((plainOrder G Y).idxOf v) i with hlt | hge
      · right
        refine ⟨(mem_take_iff_idxOf _ hnd v hvo i).2 hlt, ?_⟩
        rcases hle2 with h | ⟨x, hx, h⟩
        · rw [hidx v hvo] at h
          omega
        · refine ⟨x, hx, ?_⟩
          rw [hidx x (hnb x hx).1] at h
          exact (hnb x hx).2.2 h
      · left
        have hvi : v = (plainOrder G Y)[i] := by
          rw [eq_getElem_iff_idxOf _ hnd v hvo i hi']
          omega
        exact hvi
    · rintro (rfl | ⟨hvt, x, hx, hxt⟩)
      · have hvo : (plainOrder G Y)[i] ∈ plainOrder G Y := List.getElem_mem hi'
        refine ⟨(hmem _).1 hvo, ?_, ?_⟩
        · rw [hidx _ hvo, hnd.idxOf_getElem i hi']
        · rw [le_lastF_iff]
          left
          rw [hidx _ hvo, hnd.idxOf_getElem i hi']
      · have hvo : v ∈ plainOrder G Y := List.mem_of_mem_take hvt
        refine ⟨(hmem v).1 hvo, ?_, ?_⟩
        · have hlt := (mem_take_iff_idxOf _ hnd v hvo i).1 hvt
          rw [hidx v hvo]
          omega
        · rw [le_lastF_iff]
          right
          refine ⟨x, hx, ?_⟩
          rw [hidx x (hnb x hx).1]
          exact (hnb x hx).2.1 hxt

end L1

/-- Task L1: the exact bags of the plain sweep (`Spec2.lean` §6.1 interface). -/
theorem plainLayoutBags : PlainLayoutBags := by
  intro G hG Y
  exact L1.plainLayoutBags_aux G hG Y

#print axioms CubicPathwidth.Alg.plainLayoutBags

end CubicPathwidth.Alg