CubicPathwidth.Alg.Proofs2.U2PdTw2NoFallback

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

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

/-!
# U2: `pd_tw2` never falls back (Stage 2, task U2)

Route. Generalize to `pdTw2Fuel fuel H` with `numNodes ≤ fuel` and `Emptiable H`, and
induct on `fuel`. For `H` with more than 3 nodes: `reduceRecordF H.copy` empties the
copy (`ReduceConfluent` on `H.copy`, which is `Emptiable` by `OpsRecordCongr`), its
flag is `false` (`ReduceRecordNoFallback`), and `BalancedElimBag` gives a bag at which
`find?` succeeds. For a component `c` of the balanced bag, `H.induced c.contains` has at
most `c.length ≤ fuel` nodes and is `Emptiable` (`RecordMono` with the empty graph as
the final graph), so the induction hypothesis applies to it.

The top-level theorem converts `(reduceRecord H.copy).1.numNodes = 0` into `Emptiable H`
using `ReduceRecordMaximal`, `ReduceRecordSpec` (well-formedness of the output) and
`OpsRecordCongr`; the recorded operations are reductions only (`reduceLoop` emits only
`Op.red`).
-/

namespace CubicPathwidth.Alg

open Graph

namespace U2

/-! ## Elementary facts about `SameGraph` and records -/

theorem sameGraph_refl (G : Graph) : SameGraph G G :=
  ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩

theorem sameGraph_symm {G H : Graph} (h : SameGraph G H) : SameGraph H G :=
  ⟨fun v => (h.1 v).symm, fun u v => (h.2 u v).symm⟩

theorem sameGraph_trans {G H K : Graph} (h₁ : SameGraph G H) (h₂ : SameGraph H K) :
    SameGraph G K :=
  ⟨fun v => (h₁.1 v).trans (h₂.1 v), fun u v => (h₁.2 u v).trans (h₂.2 u v)⟩

/-- A record can be re-targeted along `SameGraph` at its end. -/
theorem opsRecord_sameEnd (ops : List Op) :
    ∀ (F R R' : Graph), OpsRecord F ops R → SameGraph R R' → OpsRecord F ops R' := by
  induction ops with
  | nil =>
    intro F R R' h h'
    exact sameGraph_trans h h'
  | cons o ops ih =>
    intro F R R' h h'
    cases o with
    | red v nb =>
      obtain ⟨h1, h2, h3, h4, h5⟩ := h
      exact ⟨h1, h2, h3, h4, ih _ _ _ h5 h'⟩
    | del w =>
      obtain ⟨h1, h2⟩ := h
      exact ⟨h1, ih _ _ _ h2 h'⟩

theorem empty_not_adj (u v : Nat) : ¬ (Graph.empty).Adj u v := by
  simp [Graph.Adj, Graph.nbrs, Graph.empty]

/-! ## Operations of `reduce_record` are reductions -/

/-- `reduceLoop` only ever records reductions. -/
theorem reduceLoop_redOnly (fuel : Nat) :
    ∀ (G : Graph) (stack : List Nat) (opsRev : List Op),
      (∀ o ∈ opsRev, ∃ v nb, o = Op.red v nb) →
      ∀ o ∈ (reduceLoop fuel G stack opsRev).2.1, ∃ v nb, o = Op.red v nb := by
  induction fuel with
  | zero =>
    intro G stack opsRev h o ho
    cases stack with
    | nil =>
      simp only [reduceLoop, List.mem_reverse] at ho
      exact h o ho
    | cons _ _ =>
      simp only [reduceLoop, List.mem_reverse] at ho
      exact h o ho
  | succ f ih =>
    intro G stack opsRev h o ho
    cases stack with
    | nil =>
      simp only [reduceLoop, List.mem_reverse] at ho
      exact h o ho
    | cons v rest =>
      simp only [reduceLoop] at ho
      split at ho
      · exact ih _ _ _ h o ho
      · refine ih _ _ _ ?_ o ho
        intro o' ho'
        rcases List.mem_cons.mp ho' with rfl | ho'
        · exact ⟨_, _, rfl⟩
        · exact h o' ho'

theorem reduceRecordF_redOnly (G : Graph) : RedOnly (reduceRecordF G).2.1 := by
  intro o ho
  exact reduceLoop_redOnly _ _ _ _ (fun o h => by simp at h) o ho

/-! ## Copies -/

theorem copy_wf {H : Graph} (hH : H.WF) : H.copy.WF :=
  (inducedSpec H (fun _ => true) hH).1

theorem copy_sameGraph {H : Graph} (hH : H.WF) : SameGraph H H.copy := by
  have hI := inducedSpec H (fun _ => true) hH
  refine ⟨fun x => ?_, fun u v => ?_⟩
  · have := hI.2.1 x
    simp only [Graph.copy]
    simp only [this, and_true]
  · have := hI.2.2 u v
    simp only [Graph.copy]
    simp only [this, and_true]

/-! ## Induced subgraphs of an emptiable graph are emptiable -/

theorem emptiable_induced (hMono : RecordMono) {H : Graph} (hH : H.WF) (hE : Emptiable H)
    (keep : Nat → Bool) : Emptiable (H.induced keep) := by
  obtain ⟨ops, hred, hops⟩ := hE
  have hI := inducedSpec H keep hH
  obtain ⟨ops', R', hr', hops', hN', hA', _⟩ :=
    hMono H (H.induced keep) Graph.empty ops hH hI.1
      (fun v hv => ((hI.2.1 v).1 hv).1)
      (fun u v h => ((hI.2.2 u v).1 h).1)
      (fun w hw => by obtain ⟨v, nb, h⟩ := hred _ hw; cases h) hops
  refine ⟨ops', hr', ?_⟩
  refine opsRecord_sameEnd ops' _ R' Graph.empty hops' ⟨fun v => ?_, fun u v => ?_⟩
  · constructor
    · intro hv
      have := hN' v hv
      simp [Graph.empty] at this
    · intro hv
      simp [Graph.empty] at hv
  · constructor
    · intro h
      exact absurd (hA' u v h) (empty_not_adj u v)
    · intro h
      exact absurd h (empty_not_adj u v)

/-- The reductions of an emptiable graph empty its copy (`ReduceConfluent`). -/
theorem reduce_copy_empty (hCongr : OpsRecordCongr) (hConf : ReduceConfluent)
    {H : Graph} (hH : H.WF) (hE : Emptiable H) :
    (reduceRecordF H.copy).1.numNodes = 0 := by
  obtain ⟨ops, hr, hops⟩ := hE
  have hcE : Emptiable H.copy :=
    ⟨ops, hr, hCongr H H.copy Graph.empty ops hH (copy_wf hH) (copy_sameGraph hH) hops⟩
  exact hConf H.copy (copy_wf hH) hcE

/-- A component's induced graph has at most `c.length` nodes. -/
theorem comp_numNodes_le {H : Graph} (hH : H.WF) (c : List Nat) :
    (H.induced c.contains).numNodes ≤ c.length := by
  have hI := inducedSpec H c.contains hH
  have hsub : (H.induced c.contains).nodes ⊆ c := fun x hx => by
    have := (hI.2.1 x).1 hx
    simpa using this.2
  exact hI.1.nodup.length_le_of_subset hsub

/-! ## Main induction -/

/-- Generalized statement: no fallback for every fuel at least the number of nodes. -/
theorem pdTw2Fuel_noFallback (hR1 : ReduceRecordNoFallback) (hCongr : OpsRecordCongr)
    (hMono : RecordMono) (hConf : ReduceConfluent) (hBal : BalancedElimBag) :
    ∀ (fuel : Nat) (H : Graph), H.WF → H.numNodes ≤ fuel → Emptiable H →
      (pdTw2Fuel fuel H).2 = false := by
  intro fuel
  induction fuel with
  | zero =>
    intro H _ hN _
    have h0 : H.numNodes = 0 := by omega
    simp [pdTw2Fuel, h0]
  | succ f ih =>
    intro H hH hN hE
    by_cases h0 : H.numNodes = 0
    · simp [pdTw2Fuel, h0]
    by_cases h3 : H.numNodes ≤ 3
    · simp [pdTw2Fuel, h0, h3]
    have hRed0 : (reduceRecordF H.copy).1.numNodes = 0 :=
      reduce_copy_empty hCongr hConf hH hE
    have hflag : (reduceRecordF H.copy).2.2 = false := hR1 H.copy (copy_wf hH)
    obtain ⟨X, hXmem, hXbal⟩ := hBal H hH (by omega) hRed0
    simp only [pdTw2Fuel, h0, h3, ite_false, Bool.false_eq_true, hRed0, bne_self_eq_false]
    split
    · rename_i hnone
      exfalso
      refine (List.find?_eq_none.mp hnone) X hXmem ?_
      simp only [List.all_eq_true, decide_eq_true_eq]
      exact fun c hc => hXbal c hc
    · rename_i X' hfind
      have hX' := List.find?_some hfind
      simp only [List.all_eq_true, decide_eq_true_eq] at hX'
      simp only [hflag, Bool.false_or]
      rw [List.any_eq_false]
      intro p hp
      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hp
      have hcb : 2 * c.length ≤ H.numNodes := hX' c hc
      have hlen : c.length ≤ f := by omega
      have hNle : (H.induced c.contains).numNodes ≤ f :=
        Nat.le_trans (comp_numNodes_le hH c) hlen
      have hEmp : Emptiable (H.induced c.contains) := emptiable_induced hMono hH hE c.contains
      have hWF : (H.induced c.contains).WF := (inducedSpec H c.contains hH).1
      show ¬ (pdTw2Fuel f (H.induced c.contains)).2 = true
      rw [ih _ hWF hNle hEmp]
      simp

/-- An emptying run of `reduce_record` on the copy yields `Emptiable H`. -/
theorem emptiable_of_reduce (hMax : ReduceRecordMaximal) (hCongr : OpsRecordCongr)
    {H : Graph} (hH : H.WF) (h0 : (reduceRecord H.copy).1.numNodes = 0) : Emptiable H := by
  have hc := copy_wf hH
  have hM := hMax H.copy hc
  have hRS := reduceRecordSpec H.copy hc
  dsimp only at hM hRS
  obtain ⟨hops, -, -⟩ := hM
  have hWF' : (reduceRecord H.copy).1.WF := hRS.1
  have hnil : (reduceRecord H.copy).1.nodes = [] := List.length_eq_zero_iff.mp h0
  have hsame : SameGraph (reduceRecord H.copy).1 Graph.empty := by
    refine ⟨fun v => ?_, fun u v => ?_⟩
    · rw [hnil]
      simp [Graph.empty]
    · constructor
      · intro h
        have hmem := hWF'.nbrs_sub u v h
        rw [hnil] at hmem
        simp at hmem
      · intro h
        exact absurd h (empty_not_adj u v)
  have hE' : OpsRecord H.copy (reduceRecord H.copy).2 Graph.empty :=
    opsRecord_sameEnd _ _ _ _ hops hsame
  exact ⟨((reduceRecord H.copy).2), reduceRecordF_redOnly H.copy, hCongr H.copy H Graph.empty _ hc hH (sameGraph_symm (copy_sameGraph hH)) hE'⟩

end U2

/-- `pd_tw2` never falls back on a graph that reduces to the empty graph (Stage 2 task U2;
`Spec.lean` §7 `PdTw2NoFallback`). -/
theorem pdTw2NoFallback_of (hR1 : ReduceRecordNoFallback) (hMax : ReduceRecordMaximal)
    (hCongr : OpsRecordCongr) (hMono : RecordMono) (hConf : ReduceConfluent)
    (hBal : BalancedElimBag) : PdTw2NoFallback := by
  intro H hH h0
  have hE := U2.emptiable_of_reduce hMax hCongr hH h0
  exact U2.pdTw2Fuel_noFallback hR1 hCongr hMono hConf hBal H.numNodes H hH le_rfl hE

#print axioms CubicPathwidth.Alg.pdTw2NoFallback_of

end CubicPathwidth.Alg