CubicPathwidth.Alg.Proofs.C2PlainLayout

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

import CubicPathwidth.Alg.Spec

/-!
# C2: validity of `plain_layout` (`PlainLayoutValid`)

Task C2 of the formalisation. Imports only `CubicPathwidth.Alg.Spec`.
The hypotheses `WFBasics` (graph layer) and `PlainOrderPerm` (C1) are taken as
arguments. Helpers live in the namespace `CubicPathwidth.Alg.C2`.

Idea. With `idx` the position map and `last v = max over v's neighbours of idx`
(starting at `idx v`), bag `i` of `plainLayout` is `{v ∈ G | idx v ≤ i ≤ last v}`
for `i < order.length`. Each vertex is in the bag `idx v`; the bags containing a
vertex form an interval; an edge `uv` with `idx u ≤ idx v` lies in bag `idx v`,
since `v ∈ nbrs u` gives `idx v ≤ last u`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace C2

/-- Python `idx` of `plain_layout`: the position map built from `order.zipIdx`, default `0`. -/
def idxOf (order : List Nat) : Nat → Nat :=
  fun v => (order.zipIdx.foldl (fun m p => m.insert p.1 p.2) (∅ : Std.HashMap Nat Nat)).getD v 0

/-- Python `last` of `plain_layout`: the maximum of `idx` over `v` and its neighbours. -/
def lastF (G : Graph) (idx : Nat → Nat) (v : Nat) : Nat :=
  (G.nbrs v).foldl (fun m u => max m (idx u)) (idx v)

/-- The bags of `plain_layout` given the position map and the number `L` of bags. -/
def bagsFrom (G : Graph) (idx : Nat → Nat) (L : Nat) : List Bag :=
  (List.range L).map fun i => G.nodes.filter fun v => idx v ≤ i && i ≤ lastF G idx v

theorem foldl_insert_getD_lt (N : Nat) :
    ∀ (l : List (Nat × Nat)), (∀ p ∈ l, p.2 < N) →
      ∀ (m : Std.HashMap Nat Nat), (∀ k, m.getD k 0 < N) →
        ∀ k, (l.foldl (fun m p => m.insert p.1 p.2) m).getD k 0 < N
  | [], _, _, hm, k => hm k
  | p :: l, hl, m, hm, k => by
    rw [List.foldl_cons]
    refine foldl_insert_getD_lt N l (fun q hq => hl q (List.mem_cons_of_mem _ hq)) _ ?_ k
    intro k'
    rw [Std.HashMap.getD_insert]
    split
    · exact hl p (by simp)
    · exact hm k'

theorem idxOf_lt (order : List Nat) (v : Nat) (hv : 0 < order.length) :
    idxOf order v < order.length := by
  unfold idxOf
  refine foldl_insert_getD_lt order.length order.zipIdx (fun p hp => ?_) ∅ (fun k => ?_) v
  · have := List.snd_lt_of_mem_zipIdx hp
    omega
  · rw [Std.HashMap.getD_empty]
    exact hv

theorem le_foldl_max (f : Nat → Nat) : ∀ (l : List Nat) (a : Nat),
    a ≤ l.foldl (fun m u => max m (f u)) a
  | [], a => le_refl a
  | u :: l, a => by
    rw [List.foldl_cons]
    exact le_trans (Nat.le_max_left a (f u)) (le_foldl_max f l _)

theorem le_foldl_max_of_mem (f : Nat → Nat) : ∀ (l : List Nat) (a x : Nat), x ∈ l →
    f x ≤ l.foldl (fun m u => max m (f u)) a
  | [], _, _, hx => by simp at hx
  | u :: l, a, x, hx => by
    rw [List.foldl_cons]
    rcases List.mem_cons.1 hx with rfl | hx
    · exact le_trans (Nat.le_max_right a (f x)) (le_foldl_max f l _)
    · exact le_foldl_max_of_mem f l _ x hx

theorem idx_le_lastF (G : Graph) (idx : Nat → Nat) (v : Nat) : idx v ≤ lastF G idx v :=
  le_foldl_max idx (G.nbrs v) (idx v)

theorem idx_le_lastF_of_mem (G : Graph) (idx : Nat → Nat) {u v : Nat} (h : v ∈ G.nbrs u) :
    idx v ≤ lastF G idx u :=
  le_foldl_max_of_mem idx (G.nbrs u) (idx u) v h

theorem inBag_bagsFrom (G : Graph) (idx : Nat → Nat) (L i v : Nat) :
    InBag (bagsFrom G idx L) i v ↔
      i < L ∧ v ∈ G.nodes ∧ idx v ≤ i ∧ i ≤ lastF G idx v := by
  by_cases hi : i < L
  · simp [InBag, bagsFrom, hi, List.mem_filter]
  · have hnone : (bagsFrom G idx L)[i]? = none := by
      unfold bagsFrom
      rw [List.getElem?_eq_none]
      simp only [List.length_map, List.length_range]
      omega
    simp [InBag, hnone, hi]

theorem bagsFrom_valid (G : Graph) (hWF : WFBasics) (hG : G.WF) (idx : Nat → Nat) (L : Nat)
    (hL : ∀ v ∈ G.nodes, idx v < L) :
    ValidPD G (bagsFrom G idx L) ∧ BagsWithin G (bagsFrom G idx L) := by
  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
  · intro v hv
    exact ⟨idx v, (inBag_bagsFrom G idx L _ v).2 ⟨hL v hv, hv, le_refl _, idx_le_lastF G idx v⟩⟩
  · intro v hv i j k hij hjk hi hk
    obtain ⟨hi1, _, hi2, _⟩ := (inBag_bagsFrom G idx L i v).1 hi
    obtain ⟨hk1, _, _, hk2⟩ := (inBag_bagsFrom G idx L k v).1 hk
    exact (inBag_bagsFrom G idx L j v).2 ⟨by omega, hv, by omega, by omega⟩
  · intro u v hu huv
    obtain ⟨_, hv, hvu, _⟩ := hWF G hG u v huv
    have hbag : ∀ i, InBag (bagsFrom G idx L) i u → InBag (bagsFrom G idx L) i v →
        ∃ B ∈ bagsFrom G idx L, u ∈ B ∧ v ∈ B := by
      intro i hi hj
      obtain ⟨B, hB, hu'⟩ := hi
      obtain ⟨B', hB', hv'⟩ := hj
      have hBB : B = B' := Option.some.inj (hB.symm.trans hB')
      subst hBB
      exact ⟨B, List.mem_of_getElem? hB, hu', hv'⟩
    rcases le_total (idx u) (idx v) with h | h
    · apply hbag (idx v)
      · exact (inBag_bagsFrom G idx L _ u).2 ⟨hL v hv, hu, h, idx_le_lastF_of_mem G idx huv⟩
      · exact (inBag_bagsFrom G idx L _ v).2 ⟨hL v hv, hv, le_refl _, idx_le_lastF G idx v⟩
    · apply hbag (idx u)
      · exact (inBag_bagsFrom G idx L _ u).2 ⟨hL u hu, hu, le_refl _, idx_le_lastF G idx u⟩
      · exact (inBag_bagsFrom G idx L _ v).2 ⟨hL u hu, hv, h, idx_le_lastF_of_mem G idx hvu⟩
  · intro B hB x hx
    obtain ⟨i, _, rfl⟩ := List.mem_map.1 hB
    exact (List.mem_filter.1 hx).1

end C2

/-- C2: `plain_layout` is a valid path decomposition of every well-formed graph, for every
labeling, given the basic graph facts and that `plainOrder` is a permutation of the nodes. -/
theorem plainLayoutValid_of (hWF : WFBasics) (hP : PlainOrderPerm) : PlainLayoutValid := by
  intro G hG Y
  have hlen : (plainOrder G Y).length = G.nodes.length := (hP G Y).length_eq
  have hbags : plainLayout G Y =
      C2.bagsFrom G (C2.idxOf (plainOrder G Y)) (plainOrder G Y).length := rfl
  have hL : ∀ v ∈ G.nodes, C2.idxOf (plainOrder G Y) v < (plainOrder G Y).length :=
    fun v hv => C2.idxOf_lt _ v (by rw [hlen]; exact List.length_pos_of_mem hv)
  rw [hbags]
  exact C2.bagsFrom_valid G hWF hG _ _ hL

#print axioms CubicPathwidth.Alg.plainLayoutValid_of

end CubicPathwidth.Alg
Back to top