CubicPathwidth.Alg.Proofs2.R5RecordMono

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# R5: a legal record restricted to a subgraph is a legal record of the subgraph

Proves `RecordMono` (`Plan2.lean` §6.2). Induction on the operations. A reduction at `v`
is replayed on the subgraph `G'` when `v` is a node of `G'` (its `G'`-neighbours are
among its `G`-neighbours, so there are at most two of them); otherwise it is skipped.
The graph helpers `redStep_facts` and its lemmas are copied from `Proofs2/R4TorsoSim.lean`.
-/

noncomputable section

namespace CubicPathwidth.Alg.R5

/-! ## Graph facts about `redStep` -/

theorem mem_of_len_le_one {L : List Nat} (h : L.length ≤ 1) {x y : Nat}
    (hx : x ∈ L) (hy : y ∈ L) : x = y := by
  rcases L with _ | ⟨a, _ | ⟨b, t⟩⟩
  · simp at hx
  · simp at hx hy
    omega
  · simp at h

theorem redStep_cases (G : Graph) (v : Nat) :
    (∃ a b, G.nbrs v = [a, b] ∧ redStep G v = (G.removeNode v).addEdge a b) ∨
    ((G.nbrs v).length ≤ 1 ∧ redStep G v = G.removeNode v) ∨
    (3 ≤ (G.nbrs v).length ∧ redStep G v = G.removeNode v) := by
  unfold redStep
  rcases h : G.nbrs v with _ | ⟨a, _ | ⟨b, _ | ⟨c, t⟩⟩⟩
  · right; left; simp
  · right; left; simp
  · left; exact ⟨a, b, rfl, rfl⟩
  · right; right; simp

theorem nbrs_len_eq (G : Graph) (hG : G.WF) (v : Nat) (nb : List Nat) (hnb : nb.Nodup)
    (hmem : ∀ x, x ∈ nb ↔ G.Adj v x) : (G.nbrs v).length = nb.length := by
  have hperm : (G.nbrs v).Perm nb :=
    (List.perm_ext_iff_of_nodup (hG.nbrs_nodup v) hnb).2 (fun x => (hmem x).symm)
  exact hperm.length_eq

/-- The graph after one reduction at `v` (with neighbour list `nb`, as in `OpsRecord`):
nodes are the old nodes except `v`, and the adjacency is the torso adjacency of
`(F, B.erase v)` (joining the two neighbours of `v`). -/
theorem redStep_facts (G : Graph) (hG : G.WF) (v : Nat) (nb : List Nat)
    (hnb : nb.Nodup) (hlen : nb.length ≤ 2)
    (hmem : ∀ x, x ∈ nb ↔ G.Adj v x) :
    (redStep G v).WF ∧
    (∀ x, x ∈ (redStep G v).nodes ↔ x ∈ G.nodes ∧ x ≠ v) ∧
    (∀ x y, (redStep G v).Adj x y ↔
      x ≠ v ∧ y ≠ v ∧ (G.Adj x y ∨ (x ≠ y ∧ G.Adj x v ∧ G.Adj y v))) := by
  have hL : (G.nbrs v).length ≤ 2 := by
    rw [nbrs_len_eq G hG v nb hnb hmem]; exact hlen
  have hRem := removeNodeSpec G v hG
  have hsymm : ∀ x, G.Adj x v ↔ G.Adj v x :=
    fun x => ⟨fun h => hG.symm x v h, fun h => hG.symm v x h⟩
  rcases redStep_cases G v with ⟨a, b, hab, hred⟩ | ⟨hlen1, hred⟩ | ⟨hlen3, _⟩
  · -- two neighbours `a ≠ b`
    have hnodup := hG.nbrs_nodup v
    rw [hab] at hnodup
    have hab' : a ≠ b := by simpa using hnodup
    have haN : a ∈ G.nbrs v := by rw [hab]; simp
    have hbN : b ∈ G.nbrs v := by rw [hab]; simp
    have hav : a ≠ v := fun h => hG.loopless v (h ▸ haN)
    have hbv : b ≠ v := fun h => hG.loopless v (h ▸ hbN)
    have haV : a ∈ G.nodes := hG.nbrs_sub v a haN
    have hbV : b ∈ G.nodes := hG.nbrs_sub v b hbN
    have hxa : ∀ x, G.Adj x v ↔ (x = a ∨ x = b) := by
      intro x
      rw [hsymm x]
      show x ∈ G.nbrs v ↔ _
      rw [hab]; simp
    have hA := addEdgeSpec (G.removeNode v) a b hRem.1 hab'
    rw [hred]
    refine ⟨hA.1, fun x => ?_, fun x y => ?_⟩
    · rw [hA.2.1 x, hRem.2.1 x]
      constructor
      · rintro (h | rfl | rfl)
        · exact h
        · exact ⟨haV, hav⟩
        · exact ⟨hbV, hbv⟩
      · intro h
        exact Or.inl h
    · rw [hA.2.2 x y, hRem.2.2 x y, hxa x, hxa y]
      constructor
      · rintro ((⟨h, h1, h2⟩) | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
        · exact ⟨h1, h2, Or.inl h⟩
        · exact ⟨hav, hbv, Or.inr ⟨hab', Or.inl rfl, Or.inr rfl⟩⟩
        · exact ⟨hbv, hav, Or.inr ⟨fun e => hab' e.symm, Or.inr rfl, Or.inl rfl⟩⟩
      · rintro ⟨h1, h2, h | ⟨hne, hx, hy⟩⟩
        · exact Or.inl ⟨h, h1, h2⟩
        · rcases hx with rfl | rfl <;> rcases hy with rfl | rfl
          · exact absurd rfl hne
          · exact Or.inr (Or.inl ⟨rfl, rfl⟩)
          · exact Or.inr (Or.inr ⟨rfl, rfl⟩)
          · exact absurd rfl hne
  · -- at most one neighbour
    rw [hred]
    refine ⟨hRem.1, fun x => hRem.2.1 x, fun x y => ?_⟩
    rw [hRem.2.2 x y]
    constructor
    · rintro ⟨h, h1, h2⟩
      exact ⟨h1, h2, Or.inl h⟩
    · rintro ⟨h1, h2, h | ⟨hne, hx, hy⟩⟩
      · exact ⟨h, h1, h2⟩
      · exact absurd (mem_of_len_le_one hlen1 ((hsymm x).mp hx) ((hsymm y).mp hy)) hne
  · omega

end CubicPathwidth.Alg.R5

namespace CubicPathwidth.Alg

open Graph

theorem recordMono_aux (ops : List Op) :
    ∀ (G G' R : Graph), G.WF → G'.WF →
      (∀ v ∈ G'.nodes, v ∈ G.nodes) → (∀ u v, G'.Adj u v → G.Adj u v) →
      (∀ w, Op.del w ∈ ops → w ∉ G'.nodes) →
      OpsRecord G ops R →
      ∃ ops' R', RedOnly ops' ∧ OpsRecord G' ops' R' ∧
        (∀ v ∈ R'.nodes, v ∈ R.nodes) ∧ (∀ u v, R'.Adj u v → R.Adj u v) ∧
        (∀ v ∈ R'.nodes, v ∈ G'.nodes) := by
  induction ops with
  | nil =>
    intro G G' R hG hG' hn ha _ hops
    simp only [OpsRecord] at hops
    obtain ⟨hV, hA⟩ := hops
    refine ⟨[], G', ?_, ?_, ?_, ?_, ?_⟩
    · intro o ho
      simp at ho
    · simp only [OpsRecord]
      exact ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩
    · intro v hv
      exact (hV v).1 (hn v hv)
    · intro u v h
      exact (hA u v).1 (ha u v h)
    · intro v hv
      exact hv
  | cons o ops ih =>
    intro G G' R hG hG' hn ha hdel hops
    cases o with
    | del w =>
      simp only [OpsRecord] at hops
      obtain ⟨hwN, hrest⟩ := hops
      have hwG' : w ∉ G'.nodes := hdel w (by simp)
      have hRem := removeNodeSpec G w hG
      obtain ⟨ops', R', h1, h2, h3, h4, h5⟩ :=
        ih (G.removeNode w) G' R hRem.1 hG'
          (fun x hx => (hRem.2.1 x).2 ⟨hn x hx, fun e => hwG' (by rw [← e]; exact hx)⟩)
          (fun u v h => by
            obtain ⟨hu, hv, _, _⟩ := wfBasics G' hG' u v h
            exact (hRem.2.2 u v).2 ⟨ha u v h,
              fun e => hwG' (by rw [← e]; exact hu),
              fun e => hwG' (by rw [← e]; exact hv)⟩)
          (fun w' hw => hdel w' (List.mem_cons_of_mem _ hw))
          hrest
      exact ⟨ops', R', h1, h2, h3, h4, h5⟩
    | red v nb =>
      simp only [OpsRecord] at hops
      obtain ⟨hvN, hnb, hlen, hmem, hrest⟩ := hops
      obtain ⟨hW1, hN1, hA1⟩ := R5.redStep_facts G hG v nb hnb hlen hmem
      by_cases hvG' : v ∈ G'.nodes
      · -- replay the reduction on `G'` with its own neighbour list
        have hnb' : (G'.nbrs v).Nodup := hG'.nbrs_nodup v
        have hsub : G'.nbrs v ⊆ nb := fun x hx => (hmem x).2 (ha v x hx)
        have hlen' : (G'.nbrs v).length ≤ 2 :=
          le_trans (hnb'.length_le_of_subset hsub) hlen
        have hmem' : ∀ x, x ∈ G'.nbrs v ↔ G'.Adj v x := fun x => Iff.rfl
        obtain ⟨hW1', hN1', hA1'⟩ := R5.redStep_facts G' hG' v (G'.nbrs v) hnb' hlen' hmem'
        obtain ⟨ops', R', h1, h2, h3, h4, h5⟩ :=
          ih (redStep G v) (redStep G' v) R hW1 hW1'
            (fun x hx =>
              (hN1 x).2 ⟨hn x ((hN1' x).1 hx).1, ((hN1' x).1 hx).2⟩)
            (fun a b hab => by
              obtain ⟨h1, h2, h3⟩ := (hA1' a b).1 hab
              refine (hA1 a b).2 ⟨h1, h2, ?_⟩
              rcases h3 with h | ⟨hne, h4, h5⟩
              · exact Or.inl (ha a b h)
              · exact Or.inr ⟨hne, ha a v h4, ha b v h5⟩)
            (fun w' hw hw'mem => hdel w' (List.mem_cons_of_mem _ hw) ((hN1' w').1 hw'mem).1)
            hrest
        refine ⟨Op.red v (G'.nbrs v) :: ops', R', ?_, ?_, h3, h4,
          fun x hx => ((hN1' x).1 (h5 x hx)).1⟩
        · intro o ho
          rcases List.mem_cons.1 ho with rfl | ho
          · exact ⟨v, _, rfl⟩
          · exact h1 o ho
        · exact ⟨hvG', hnb', hlen', hmem', h2⟩
      · -- `G'` avoids `v`: skip the reduction
        obtain ⟨ops', R', h1, h2, h3, h4, h5⟩ :=
          ih (redStep G v) G' R hW1 hG'
            (fun x hx =>
              (hN1 x).2 ⟨hn x hx, fun e => hvG' (by rw [← e]; exact hx)⟩)
            (fun a b hab => by
              obtain ⟨ha', hb', _, _⟩ := wfBasics G' hG' a b hab
              refine (hA1 a b).2 ⟨fun e => hvG' (by rw [← e]; exact ha'),
                fun e => hvG' (by rw [← e]; exact hb'), Or.inl (ha a b hab)⟩)
            (fun w' hw => hdel w' (List.mem_cons_of_mem _ hw))
            hrest
        exact ⟨ops', R', h1, h2, h3, h4, h5⟩

/-- `RecordMono` (`Plan2.lean` §6.2): replaying a legal record on a subgraph. -/
theorem recordMono : RecordMono := by
  intro G G' R ops hG hG' hn ha hdel hops
  exact recordMono_aux ops G G' R hG hG' hn ha hdel hops

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.recordMono