CubicPathwidth.Alg.Proofs2.R6Confluent

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

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

/-!
# R6: confluence of `reduce_record` (`ReduceConfluent`)

Route (torso world, fixed core vertex set). Let `F = V₀` be the vertices of `G`
(as `Fin n`). Reduction-only states `(F, B)` form the relation `RR F B B'`: a single
step removes some `v ∈ B` of torso degree at most two in `(F, B)`.

* `RR_erase`: if `RR B B'` and `v ∈ B` has torso degree at most two in `(F, B)`, then
  `RR (B.erase v) (B'.erase v)` (degrees never increase along reductions).
* `RR_of_empty`: if `RR B ∅` and `RR B B'`, then `RR B' ∅` (greedy runs cannot be
  stuck, by `RR_erase`).
* `RR_nonempty_contra`: `RR X ∅` with `X ≠ ∅` needs a vertex of torso degree `≤ 2`.

The two records of `G` (an emptying one from `Emptiable`, and the output of
`reduce_record`) are simulated by `TorsoSim`; `ReduceRecordSpec` (Stage 1) gives that
`reduce_record` is red-only, well formed, and has nodes among those of `G`.
`ReduceRecordMaximal` gives minimum degree at least `3` on the output.
-/

noncomputable section

namespace CubicPathwidth.Alg.R6

open Graph

variable {n : ℕ} (S : SimpleGraph (Fin n))

/-- One reduction in the fixed core `F`: remove `v ∈ B` of torso degree at most two. -/
def RRstep (F B B' : Finset (Fin n)) : Prop :=
  ∃ v ∈ B, CubicPathwidth.T4.tdeg S F B v ≤ 2 ∧ B' = B.erase v

/-- Reduction-only reachability in the fixed core `F`. -/
abbrev RR (F : Finset (Fin n)) : Finset (Fin n) → Finset (Fin n) → Prop :=
  Relation.ReflTransGen (RRstep S F)

variable {S}

theorem RR_sub {F B B' : Finset (Fin n)} (h : RR S F B B') : B' ⊆ B := by
  induction h with
  | refl => exact Finset.Subset.rfl
  | @tail b c _ hs ih =>
    obtain ⟨v, _, _, rfl⟩ := hs
    exact (Finset.erase_subset _ _).trans ih

theorem RR_tdeg_le {F B B' : Finset (Fin n)} (hBF : B ⊆ F) (h : RR S F B B') :
    ∀ v ∈ B', CubicPathwidth.T4.tdeg S F B' v ≤ CubicPathwidth.T4.tdeg S F B v := by
  induction h with
  | refl => intro v _; exact le_rfl
  | @tail b c hab hs ih =>
    obtain ⟨u, hu, hdeg, rfl⟩ := hs
    intro v hv
    have hbF : b ⊆ F := (RR_sub hab).trans hBF
    have hvb : v ∈ b := Finset.mem_of_mem_erase hv
    exact (CubicPathwidth.T4.tdeg_erase_le S hbF hu hdeg hv).trans (ih v hvb)

theorem RR_erase {F B B' : Finset (Fin n)} (hBF : B ⊆ F) (h : RR S F B B') :
    ∀ v ∈ B, CubicPathwidth.T4.tdeg S F B v ≤ 2 → RR S F (B.erase v) (B'.erase v) := by
  induction h with
  | refl => intro v _ _; exact Relation.ReflTransGen.refl
  | @tail b c hab hs ih =>
    intro v hvB hvdeg
    obtain ⟨u, hu, hdeg, rfl⟩ := hs
    have hbF : b ⊆ F := (RR_sub hab).trans hBF
    have ih' := ih v hvB hvdeg
    by_cases hvb : v ∈ b
    · have hvdeg' : CubicPathwidth.T4.tdeg S F b v ≤ 2 :=
        (RR_tdeg_le hBF hab v hvb).trans hvdeg
      by_cases huv : u = v
      · subst huv
        rw [Finset.erase_idem]
        exact ih'
      · have hu' : u ∈ b.erase v := Finset.mem_erase.mpr ⟨huv, hu⟩
        have hdeg' : CubicPathwidth.T4.tdeg S F (b.erase v) u ≤ 2 :=
          (CubicPathwidth.T4.tdeg_erase_le S hbF hvb hvdeg' hu').trans hdeg
        rw [Finset.erase_right_comm]
        exact ih'.tail ⟨u, hu', hdeg', rfl⟩
    · rw [Finset.erase_eq_of_notMem hvb] at ih'
      rw [Finset.erase_eq_of_notMem (fun h => hvb (Finset.mem_of_mem_erase h))]
      exact ih'.tail ⟨u, hu, hdeg, rfl⟩

theorem RR_of_empty {F B B' : Finset (Fin n)} (hBF : B ⊆ F) (h : RR S F B B')
    (h0 : RR S F B ∅) : RR S F B' ∅ := by
  induction h with
  | refl => exact h0
  | @tail b c hab hs ih =>
    obtain ⟨u, hu, hdeg, rfl⟩ := hs
    have hbF : b ⊆ F := (RR_sub hab).trans hBF
    have := RR_erase hbF ih u hu hdeg
    simpa using this

theorem RR_nonempty_contra {F X : Finset (Fin n)} (h : RR S F X ∅) (hX : X.Nonempty)
    (hmin : ∀ v ∈ X, 3 ≤ CubicPathwidth.T4.tdeg S F X v) : False := by
  rcases Relation.ReflTransGen.cases_head h with heq | ⟨c, ⟨u, hu, hdeg, _⟩, _⟩
  · rw [heq] at hX
    exact Finset.not_nonempty_empty hX
  · have := hmin u hu
    omega

/-! ## Reachability with the core-set fixed -/

theorem reach_inv {F B : Finset (Fin n)} {p : Finset (Fin n) × Finset (Fin n)}
    (h : Relation.ReflTransGen (CubicPathwidth.T4.Step S) (F, B) p) (hBF : B ⊆ F) :
    p.2 ⊆ p.1 ∧ p.1 ⊆ F := by
  induction h with
  | refl => exact ⟨hBF, Finset.Subset.rfl⟩
  | @tail p1 p2 _ hs ih =>
    obtain ⟨ih1, ih2⟩ := ih
    cases hs with
    | reduce hv _ =>
      exact ⟨(Finset.erase_subset _ _).trans ih1, ih2⟩
    | delete hw =>
      exact ⟨Finset.erase_subset_erase _ ih1, (Finset.erase_subset _ _).trans ih2⟩

theorem RR_of_reach' {F B : Finset (Fin n)} {p : Finset (Fin n) × Finset (Fin n)}
    (h : Relation.ReflTransGen (CubicPathwidth.T4.Step S) (F, B) p) (hBF : B ⊆ F) :
    p.1 = F → RR S F B p.2 := by
  induction h with
  | refl => intro _; exact Relation.ReflTransGen.refl
  | @tail p1 p2 hp hs ih =>
    intro h2
    have hinv := reach_inv hp hBF
    cases hs with
    | reduce hv hdeg =>
      dsimp only at h2 ih
      subst h2
      exact (ih rfl).tail ⟨_, hv, hdeg, rfl⟩
    | delete hw =>
      exfalso
      have hwF : _ ∈ F := hinv.2 (hinv.1 hw)
      rw [← h2] at hwF
      simp at hwF

theorem RR_of_reach {F B B' : Finset (Fin n)} (hBF : B ⊆ F)
    (h : Relation.ReflTransGen (CubicPathwidth.T4.Step S) (F, B) (F, B')) :
    RR S F B B' :=
  RR_of_reach' h hBF rfl

/-! ## Counting torso neighbours -/

open Classical in

theorem card_adj_eq_degree (R : Graph) (hRWF : R.WF) (hn : ∀ w ∈ R.nodes, w < n)
    (x : Fin n) :
    (Finset.univ.filter fun y : Fin n => R.Adj x.val y.val).card = R.degree x.val := by
  have hmap : (Finset.univ.filter fun y : Fin n => R.Adj x.val y.val).map Fin.valEmbedding
      = (R.nbrs x.val).toFinset := by
    ext w
    simp only [Finset.mem_map, Finset.mem_filter, Finset.mem_univ, true_and,
      List.mem_toFinset, Fin.valEmbedding_apply]
    constructor
    · rintro ⟨y, hy, rfl⟩
      exact hy
    · intro hw
      have hwn : w ∈ R.nodes := hRWF.nbrs_sub _ _ hw
      exact ⟨⟨w, hn w hwn⟩, hw, rfl⟩
  rw [← Finset.card_map Fin.valEmbedding, hmap, List.toFinset_card_of_nodup (hRWF.nbrs_nodup _)]
  rfl

theorem deletedSet_nil {ops : List Op} (h : ∀ o ∈ ops, ∃ v nb, o = Op.red v nb) :
    deletedSet ops = [] := by
  unfold deletedSet
  rw [List.filterMap_eq_nil_iff]
  intro o ho
  obtain ⟨v, nb, rfl⟩ := h o ho
  rfl

/-! ## Main theorem -/

theorem reduceConfluent_of (hSim : TorsoSim) (hMax : ReduceRecordMaximal) (hMono : RecordMono)
    (hCongr : OpsRecordCongr) (hApp : OpsRecordAppend) : ReduceConfluent := by
  classical
  intro G hG hEm
  obtain ⟨opsE, hredE, hrecE⟩ := hEm
  have hRS := reduceRecordSpec G hG
  dsimp only at hRS
  obtain ⟨hRWF, hRnodes, -, hRops, -⟩ := hRS
  have hMx := hMax G hG
  dsimp only at hMx
  obtain ⟨hOps, hmin, -⟩ := hMx
  set R := (reduceRecord G).1 with hRdef
  set ops := (reduceRecord G).2 with hopsdef
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ v ∈ G.nodes, v < n :=
    ⟨G.nodes.sum + 1, fun v hv => Nat.lt_succ_of_le (List.le_sum_of_mem hv)⟩
  have hRn : ∀ w ∈ R.nodes, w < n := fun w hw => hn w (hRnodes w hw)
  obtain ⟨-, hReachE, -⟩ := hSim n G Graph.empty opsE hG hn hrecE
  obtain ⟨-, hReachR, hAdjR⟩ := hSim n G R ops hG hn hOps
  have hdelE : deletedSet opsE = [] := deletedSet_nil hredE
  have hdelR : deletedSet ops = [] := by
    apply deletedSet_nil
    intro o ho
    obtain ⟨v, nb, h, -⟩ := hRops o ho
    exact ⟨v, nb, h⟩
  have hF1 : ∀ ops' : List Op, deletedSet ops' = [] →
      (Finset.univ.filter fun x : Fin n => x.val ∈ G.nodes).filter
          (fun x : Fin n => x.val ∉ deletedSet ops') =
        Finset.univ.filter fun x : Fin n => x.val ∈ G.nodes := by
    intro ops' h
    apply Finset.filter_true_of_mem
    intro x _
    rw [h]
    simp
  rw [hF1 opsE hdelE] at hReachE
  rw [hF1 ops hdelR] at hReachR hAdjR
  have hB1E : (Finset.univ.filter fun x : Fin n => x.val ∈ (Graph.empty).nodes) = ∅ := by
    simp [Graph.empty]
  have hRE := RR_of_reach (Finset.Subset.refl _) hReachE
  rw [hB1E] at hRE
  have hRV := RR_of_reach (Finset.Subset.refl _) hReachR
  have hcore := RR_of_empty (Finset.Subset.refl _) hRV hRE
  have hminR : ∀ x ∈ Finset.univ.filter (fun x : Fin n => x.val ∈ R.nodes),
      3 ≤ CubicPathwidth.T4.tdeg (G.toSimpleGraph n)
        (Finset.univ.filter fun x : Fin n => x.val ∈ G.nodes)
        (Finset.univ.filter (fun x : Fin n => x.val ∈ R.nodes)) x := by
    intro x hx
    have hxR : x.val ∈ R.nodes := (Finset.mem_filter.mp hx).2
    rw [CubicPathwidth.T4.tdeg_eq_card, Finset.filter_congr (fun y _ => hAdjR x y),
      card_adj_eq_degree R hRWF hRn x]
    exact hmin x.val hxR
  have hB1empty : Finset.univ.filter (fun x : Fin n => x.val ∈ R.nodes) = ∅ := by
    by_contra hne
    exact RR_nonempty_contra hcore (Finset.nonempty_iff_ne_empty.mpr hne) hminR
  have hRnil : R.nodes = [] := by
    rw [List.eq_nil_iff_forall_not_mem]
    intro v hv
    have hvlt := hn v (hRnodes v hv)
    have hmem : (⟨v, hvlt⟩ : Fin n) ∈ Finset.univ.filter (fun x : Fin n => x.val ∈ R.nodes) := by
      simp [hv]
    rw [hB1empty] at hmem
    simp at hmem
  show R.nodes.length = 0
  rw [hRnil]
  rfl

end CubicPathwidth.Alg.R6

#print axioms CubicPathwidth.Alg.R6.reduceConfluent_of