CubicPathwidth.Alg.Proofs2.R4TorsoSim

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.TorsoDyn

/-!
# R4: the record of reductions and deletions is a torso simulation

Proves `TorsoSim` (`Plan2.lean` §6.2) from the torso dynamics `T4.torsoDynamics`
(`T4/TorsoDyn.lean`). The invariant `Inv` says that the current graph of the record is
the torso of the state `(F, B)`: `B` is the node set and the torso adjacency is the
adjacency of the current graph.
-/

noncomputable section

namespace CubicPathwidth.Alg.R4

/-! ## 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

/-! ## The invariant relating the torso of a state to the current graph -/

/-- The current graph `G` of the record is the torso of `(F, B)` over `S`: the node set of
`G` is `B` and the torso adjacency is the adjacency of `G`. -/
def Inv {n : ℕ} (S : SimpleGraph (Fin n)) (G : Graph) (F B : Finset (Fin n)) : Prop :=
  (∀ x : Fin n, x ∈ B ↔ x.val ∈ G.nodes) ∧
    ∀ x y : Fin n, (T4.tgraph S F B).Adj x y ↔ G.Adj x.val y.val

/-- Torso degree at most `2` when the torso neighbours of `v` are listed in `L`. -/
theorem tdeg_le_two {n : ℕ} (S : SimpleGraph (Fin n)) (F B : Finset (Fin n)) (v : Fin n)
    (L : List Nat) (hlen : L.length ≤ 2)
    (hadj : ∀ x : Fin n, (T4.tgraph S F B).Adj v x ↔ x.val ∈ L) :
    T4.tdeg S F B v ≤ 2 := by
  classical
  rw [T4.tdeg_eq_card]
  have hle := Finset.card_le_card_of_injOn (fun u : Fin n => u.val)
    (s := Finset.univ.filter fun u => (T4.tgraph S F B).Adj v u) (t := L.toFinset)
    (by
      intro u hu
      rw [Finset.mem_coe, Finset.mem_filter] at hu
      exact Finset.mem_coe.mpr (List.mem_toFinset.mpr ((hadj u).1 hu.2)))
    (by
      intro a _ b _ hab
      exact Fin.ext hab)
  have h2 := List.toFinset_card_le L
  omega

/-- The initial state: the torso of `(V0, V0)` is the graph `F` on its nodes. -/
theorem init_inv {n : ℕ} (F : Graph) (hF : F.WF) (S : SimpleGraph (Fin n))
    (hS : ∀ x y : Fin n, S.Adj x y ↔ F.Adj x.val y.val) :
    Inv S F (Finset.univ.filter fun x : Fin n => x.val ∈ F.nodes)
      (Finset.univ.filter fun x : Fin n => x.val ∈ F.nodes) := by
  refine ⟨fun x => by simp, fun x y => ?_⟩
  have hc : CubicPathwidth.components S (∅ : Finset (Fin n)) = ∅ := by
    unfold CubicPathwidth.components
    simp
  rw [T4.tgraph_adj_iff, Finset.sdiff_self, hc, hS]
  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.notMem_empty, false_and,
    exists_false, or_false]
  constructor
  · rintro ⟨_, h1, h2, h⟩
    exact h
  · intro h
    obtain ⟨h1, h2, _, h4⟩ := wfBasics F hF x.val y.val h
    exact ⟨fun e => h4 (congrArg Fin.val e), h1, h2, h⟩

/-- Filtering by the deleted set after erasing a core vertex. -/
theorem filter_erase_del {n : ℕ} (F : Finset (Fin n)) (wF : Fin n) (w : Nat)
    (hwF : wF.val = w) (D : List Nat) :
    (F.erase wF).filter (fun x => x.val ∉ D) =
      F.filter (fun x => x.val ∉ w :: D) := by
  ext x
  simp only [Finset.mem_filter, Finset.mem_erase, List.mem_cons, not_or, ne_eq, Fin.ext_iff,
    hwF]
  tauto

/-- Main induction: running the record from a state simulating `F` reaches the state of the
final graph, and the final torso is the final graph. -/
theorem aux {n : ℕ} (S : SimpleGraph (Fin n)) (ops : List Op) :
    ∀ (G R : Graph) (F B : Finset (Fin n)),
      G.WF → (∀ v ∈ G.nodes, v < n) → OpsRecord G ops R →
      T4.Good S F B → Inv S G F B →
      T4.Reach S (F, B)
          (F.filter (fun x => x.val ∉ deletedSet ops),
            Finset.univ.filter (fun x => x.val ∈ R.nodes)) ∧
      Inv S R (F.filter (fun x => x.val ∉ deletedSet ops))
          (Finset.univ.filter (fun x => x.val ∈ R.nodes)) := by
  induction ops with
  | nil =>
    intro G R F B hG hn hops hgood hinv
    simp only [OpsRecord] at hops
    obtain ⟨hnodes, hadj⟩ := hops
    have hD : deletedSet ([] : List Op) = [] := by simp [deletedSet]
    have hF : F.filter (fun x => x.val ∉ deletedSet ([] : List Op)) = F := by
      rw [hD]; ext x; simp
    have hB : B = Finset.univ.filter (fun x => x.val ∈ R.nodes) := by
      ext x
      rw [hinv.1 x, Finset.mem_filter]
      simp [hnodes x.val]
    rw [hF, ← hB]
    refine ⟨T4.Reach.refl S _, ?_⟩
    refine ⟨fun x => ?_, fun x y => ?_⟩
    · exact (hinv.1 x).trans (hnodes x.val)
    · exact (hinv.2 x y).trans (hadj x.val y.val)
  | cons op rest ih =>
    intro G R F B hG hn hops hgood hinv
    cases op with
    | red v nb =>
      simp only [OpsRecord] at hops
      obtain ⟨hvN, hnb, hlen, hmem, hrest⟩ := hops
      have hvn : v < n := hn v hvN
      obtain ⟨vF, hvF⟩ : ∃ vF : Fin n, vF.val = v := ⟨⟨v, hvn⟩, rfl⟩
      have hvB : vF ∈ B := (hinv.1 vF).2 (by rw [hvF]; exact hvN)
      have hdeg : T4.tdeg S F B vF ≤ 2 := by
        apply tdeg_le_two S F B vF nb hlen
        intro x
        rw [hinv.2 vF x, hvF]
        exact (hmem x.val).symm
      have hgood' : T4.Good S F (B.erase vF) :=
        hgood.reach (T4.Reach.single (T4.Step.reduce hvB hdeg))
      obtain ⟨hWF, hNodes, hAdj⟩ := redStep_facts G hG v nb hnb hlen hmem
      have hdyn := T4.torsoDynamics n S F B hgood
      have hinv' : Inv S (redStep G v) F (B.erase vF) := by
        refine ⟨fun x => ?_, fun x y => ?_⟩
        · rw [Finset.mem_erase, hinv.1 x, hNodes]
          simp only [ne_eq, Fin.ext_iff, hvF]
          tauto
        · rw [hdyn.2.1 vF hvB hdeg x y, hinv.2 x y, hinv.2 x vF, hinv.2 y vF, hAdj x.val y.val]
          simp only [ne_eq, Fin.ext_iff, hvF]
      have ih' := ih (redStep G v) R F (B.erase vF) hWF
        (fun u hu => hn u ((hNodes u).1 hu).1) hrest hgood' hinv'
      have hD : deletedSet (Op.red v nb :: rest) = deletedSet rest := by simp [deletedSet]
      rw [hD]
      exact ⟨(T4.Reach.single (T4.Step.reduce hvB hdeg)).trans ih'.1, ih'.2⟩
    | del w =>
      simp only [OpsRecord] at hops
      obtain ⟨hwN, hrest⟩ := hops
      have hwn : w < n := hn w hwN
      obtain ⟨wF, hwF⟩ : ∃ wF : Fin n, wF.val = w := ⟨⟨w, hwn⟩, rfl⟩
      have hwB : wF ∈ B := (hinv.1 wF).2 (by rw [hwF]; exact hwN)
      have hgood' : T4.Good S (F.erase wF) (B.erase wF) :=
        hgood.reach (T4.Reach.single (T4.Step.delete hwB))
      have hRem := removeNodeSpec G w hG
      have hdyn := T4.torsoDynamics n S F B hgood
      have hinv' : Inv S (G.removeNode w) (F.erase wF) (B.erase wF) := by
        refine ⟨fun x => ?_, fun x y => ?_⟩
        · rw [Finset.mem_erase, hinv.1 x, hRem.2.1 x.val]
          simp only [ne_eq, Fin.ext_iff, hwF]
          tauto
        · rw [hdyn.1 wF hwB x y, hinv.2 x y, hRem.2.2 x.val y.val]
          simp only [ne_eq, Fin.ext_iff, hwF]
      have ih' := ih (G.removeNode w) R (F.erase wF) (B.erase wF) hRem.1
        (fun u hu => hn u ((hRem.2.1 u).1 hu).1) hrest hgood' hinv'
      have hD : deletedSet (Op.del w :: rest) = w :: deletedSet rest := by simp [deletedSet]
      rw [hD, ← filter_erase_del F wF w hwF (deletedSet rest)]
      exact ⟨(T4.Reach.single (T4.Step.delete hwB)).trans ih'.1, ih'.2⟩

end CubicPathwidth.Alg.R4

namespace CubicPathwidth.Alg

/-- Simulation of the record by the torso (`TorsoSim`). -/
theorem torsoSim : TorsoSim := by
  intro n F R ops hF hn hops S V0 F1 B1
  have hS : ∀ x y : Fin n, S.Adj x y ↔ F.Adj x.val y.val := by
    intro x y
    simp only [S, Graph.toSimpleGraph, SimpleGraph.fromRel_adj]
    constructor
    · rintro ⟨_, h | h⟩
      · exact h
      · exact hF.symm y.val x.val h
    · intro h
      obtain ⟨_, _, _, h4⟩ := wfBasics F hF x.val y.val h
      exact ⟨fun e => h4 (congrArg Fin.val e), Or.inl h⟩
  have hGood : T4.Good S V0 V0 := by
    have := T4.reach_delete_set S Finset.univ Finset.univ (Finset.univ \ V0)
      (Finset.subset_univ _)
    rw [Finset.sdiff_sdiff_eq_self (Finset.subset_univ V0)] at this
    exact this
  have hinv0 : R4.Inv S F V0 V0 := R4.init_inv F hF S hS
  obtain ⟨hreach, hfin⟩ := R4.aux S ops F R V0 V0 hF hn hops hGood hinv0
  exact ⟨hGood, hreach, hfin.2⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.torsoSim