CubicPathwidth.Alg.Proofs2.DeletionBound

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.SeqH
import CubicPathwidth.T4.BasicPsi

/-!
# (D5) The deletion-process bound and the final facts of `algo_T4`

Proves `deletionProcessBound_of` and `t4FinalFacts_of` (`Plan2Deletion.lean`, task D5)
from the Stage 2 hypotheses `T4LoopRun`, `T4LoopInvInit`, `ReduceRecordMaximal`, and the
Stage 1 graph facts `inducedSpec`, `componentsSpec`, `reduceRecordSpec`, and the bootstrap
sequence `T4.seqClaim_h`.

Route. Run `T4LoopRun` from the initial state of `algoT4Full`. The start value
`∑ ψ⁻(components of H) ≤ ψ(H) ≤ ψ(G0.copy) = ψ(G0) = ψ(G)` (`H` the reduced graph),
using `ψ`-monotonicity of `T4.sigma`, degrees not increasing under reduction, and
`σ 0 = 0` for isolated vertices. The final facts come from the invariant at the end.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace D5

/-! ## Generic list and sum facts -/

theorem list_sum_map_le {α : Type} (f g : α → ℝ) : ∀ L : List α,
    (∀ x ∈ L, f x ≤ g x) → (L.map f).sum ≤ (L.map g).sum
  | [], _ => by simp
  | x :: xs, h => by
    simp only [List.map_cons, List.sum_cons]
    exact add_le_add (h x (by simp))
      (list_sum_map_le f g xs fun y hy => h y (by simp [hy]))

theorem sum_filter_eq (f : Nat → ℝ) (p : Nat → Bool) : ∀ L : List Nat,
    (∀ x ∈ L, p x = false → f x = 0) → (L.map f).sum = ((L.filter p).map f).sum
  | [], _ => by simp
  | x :: xs, h => by
    have ih := sum_filter_eq f p xs fun y hy hp => h y (List.mem_cons_of_mem _ hy) hp
    by_cases hx : p x = true
    · simp [hx, ih]
    · have hx' : p x = false := by simpa using hx
      have h0 := h x (by simp) hx'
      simp [hx', h0, ih]

theorem sum_le_of_sub {f : Nat → ℝ} (hf : ∀ x, 0 ≤ f x) {L M : List Nat}
    (hL : L.Nodup) (hM : M.Nodup) (hsub : ∀ x ∈ L, x ∈ M) :
    (L.map f).sum ≤ (M.map f).sum := by
  rw [← List.sum_toFinset f hL, ← List.sum_toFinset f hM]
  apply Finset.sum_le_sum_of_subset_of_nonneg
  · intro x hx
    simp only [List.mem_toFinset] at hx ⊢
    exact hsub x hx
  · intro x _ _
    exact hf x

/-! ## Bootstrap sequences -/

theorem bp_mono {b : ℕ → ℝ} (hb : T4.BootProps b) : Monotone b := by
  apply monotone_nat_of_le_succ
  intro n
  rcases Nat.lt_or_ge n 2 with h | h
  · interval_cases n <;> simp [hb.zero.1, hb.zero.2.1, hb.zero.2.2]
  · have := hb.mono (n + 1) (by omega)
    simpa using this

theorem bp_nonneg {b : ℕ → ℝ} (hb : T4.BootProps b) (d : ℕ) : 0 ≤ b d := by
  have := bp_mono hb (Nat.zero_le d)
  rwa [hb.zero.1] at this

theorem sigma_bp : T4.BootProps T4.sigma := T4.seqClaim_h.1

/-! ## Degrees and `psiPort` -/

theorem degree_eq_of_mem_iff {J K : Graph} {x : Nat} (hJ : (J.nbrs x).Nodup)
    (hK : (K.nbrs x).Nodup) (h : ∀ y, y ∈ J.nbrs x ↔ y ∈ K.nbrs x) :
    J.degree x = K.degree x :=
  ((List.perm_ext_iff_of_nodup hJ hK).2 h).length_eq

theorem psi_congr {b : ℕ → ℝ} {J K : Graph} (hJ : J.WF) (hK : K.WF)
    (hperm : J.nodes.Perm K.nodes) (hadj : ∀ x y, J.Adj x y ↔ K.Adj x y) :
    psiPort b J = psiPort b K := by
  unfold psiPort
  calc (J.nodes.map fun v => b (J.degree v)).sum
      = (K.nodes.map fun v => b (J.degree v)).sum := (hperm.map _).sum_eq
    _ = (K.nodes.map fun v => b (K.degree v)).sum := by
        refine congrArg List.sum (List.map_congr_left ?_)
        intro x _
        congr 1
        exact degree_eq_of_mem_iff (hJ.nbrs_nodup x) (hK.nbrs_nodup x) fun y => hadj x y

theorem psi_nonIsolated {b : ℕ → ℝ} (h0 : b 0 = 0) {G : Graph} (hG : G.WF) :
    psiPort b (nonIsolated G) = psiPort b G := by
  have hI := inducedSpec G (fun v => G.degree v != 0) hG
  have hperm : (G.nodes.filter fun v => G.degree v != 0).Perm (nonIsolated G).nodes :=
    (List.perm_ext_iff_of_nodup (hG.nodup.filter _) hI.1.nodup).2 fun x => by
      rw [hI.2.1 x, List.mem_filter]
  have hkeep : ∀ x y, G.Adj x y → (G.degree y != 0) = true := by
    intro x y hxy
    have hx : x ∈ G.nbrs y := hG.symm x y hxy
    have hpos := List.length_pos_of_mem hx
    unfold Graph.degree
    simp only [bne_iff_ne, ne_eq]
    omega
  have hsub : ∀ x ∈ G.nodes, (fun v => G.degree v != 0) x = false →
      (fun v => b (G.degree v)) x = 0 := by
    intro x _ hx
    have hd : G.degree x = 0 := by
      simp only [bne_eq_false_iff_eq] at hx
      exact hx
    simp [hd, h0]
  unfold psiPort
  rw [sum_filter_eq (fun v => b (G.degree v)) (fun v => G.degree v != 0) G.nodes hsub]
  calc ((nonIsolated G).nodes.map fun v => b ((nonIsolated G).degree v)).sum
      = ((G.nodes.filter fun v => G.degree v != 0).map
          fun v => b ((nonIsolated G).degree v)).sum := (hperm.symm.map _).sum_eq
    _ = ((G.nodes.filter fun v => G.degree v != 0).map fun v => b (G.degree v)).sum := by
        refine congrArg List.sum (List.map_congr_left ?_)
        intro x hx
        have hxk : (G.degree x != 0) = true := by
          have := (List.mem_filter.1 hx).2
          simpa using this
        congr 1
        apply degree_eq_of_mem_iff (hI.1.nbrs_nodup x) (hG.nbrs_nodup x)
        intro y
        refine (hI.2.2 x y).trans ?_
        constructor
        · exact fun h => h.1
        · intro h
          exact ⟨h, by simpa using hxk, by simpa using hkeep x y h⟩

theorem psi_copy {b : ℕ → ℝ} {G : Graph} (hG : G.WF) :
    psiPort b G.copy = psiPort b G := by
  apply psi_congr (inducedSpec G _ hG).1 hG
  · exact (List.perm_ext_iff_of_nodup (inducedSpec G _ hG).1.nodup hG.nodup).2
      fun x => by rw [(inducedSpec G _ hG).2.1 x]; simp
  · intro x y
    rw [(inducedSpec G _ hG).2.2 x y]
    simp

theorem psi_le_of_reduce {b : ℕ → ℝ} (hb : T4.BootProps b) {G H : Graph} (hG : G.WF)
    (hH : H.WF) (hsub : ∀ x ∈ H.nodes, x ∈ G.nodes)
    (hdeg : ∀ v ∈ H.nodes, H.degree v ≤ G.degree v) :
    psiPort b H ≤ psiPort b G := by
  unfold psiPort
  calc (H.nodes.map fun v => b (H.degree v)).sum
      ≤ (H.nodes.map fun v => b (G.degree v)).sum :=
        list_sum_map_le _ _ _ fun x hx => bp_mono hb (hdeg x hx)
    _ ≤ (G.nodes.map fun v => b (G.degree v)).sum :=
        sum_le_of_sub (fun x => bp_nonneg hb _) hH.nodup hG.nodup hsub

/-! ## Components -/

theorem sum_map_sum_eq (f : Nat → ℝ) : ∀ L : List (List Nat),
    (L.map fun c => (c.map f).sum).sum = ((L.flatten).map f).sum
  | [] => by simp
  | c :: cs => by
    simp only [List.map_cons, List.sum_cons, List.flatten_cons, List.map_append,
      List.sum_append, sum_map_sum_eq f cs]

theorem components_psi (b : ℕ → ℝ) {H : Graph} (hH : H.WF) :
    ((componentGraphs H).map (psiPort b)).sum = psiPort b H := by
  obtain ⟨hperm, _, hclos⟩ := componentsSpec H hH
  have hcomp : ∀ c ∈ H.components,
      psiPort b (H.induced c.contains) = (c.map fun v => b (H.degree v)).sum := by
    intro c hc
    have hcnd : c.Nodup := by
      have hfl : H.components.flatten.Nodup := hperm.nodup_iff.2 hH.nodup
      exact (List.nodup_flatten.1 hfl).1 c hc
    have hsubH : ∀ x ∈ c, x ∈ H.nodes := fun x hx =>
      hperm.subset (List.mem_flatten.2 ⟨c, hc, hx⟩)
    have hperm2 : (H.nodes.filter c.contains).Perm c := by
      apply (List.perm_ext_iff_of_nodup (hH.nodup.filter _) hcnd).2
      intro x
      simp only [List.mem_filter, List.elem_eq_mem, decide_eq_true_eq]
      constructor
      · exact fun h => h.2
      · exact fun h => ⟨hsubH x h, h⟩
    unfold psiPort
    have hdeg : ∀ x ∈ H.nodes.filter c.contains,
        b ((H.induced c.contains).degree x) = b (H.degree x) := by
      intro x hx
      have hxc : x ∈ c := by
        have := (List.mem_filter.1 hx).2
        simpa using this
      congr 1
      apply degree_eq_of_mem_iff ((inducedSpec H _ hH).1.nbrs_nodup x) (hH.nbrs_nodup x)
      intro y
      show (H.induced c.contains).Adj x y ↔ H.Adj x y
      rw [(inducedSpec H _ hH).2.2 x y]
      constructor
      · exact fun h => h.1
      · intro h
        refine ⟨h, by simpa using hxc, ?_⟩
        simpa using hclos c hc x hxc y h
    have hperm3 : (H.induced c.contains).nodes.Perm (H.nodes.filter c.contains) :=
      (List.perm_ext_iff_of_nodup (inducedSpec H _ hH).1.nodup (hH.nodup.filter _)).2
        fun x => by rw [(inducedSpec H _ hH).2.1 x, List.mem_filter]
    rw [(hperm3.map _).sum_eq, List.map_congr_left hdeg]
    exact (hperm2.map _).sum_eq
  have hmap : (componentGraphs H).map (psiPort b)
      = H.components.map fun c => (c.map fun v => b (H.degree v)).sum := by
    unfold componentGraphs
    rw [List.map_map]
    exact List.map_congr_left fun c hc => hcomp c hc
  rw [hmap, sum_map_sum_eq]
  unfold psiPort
  exact (hperm.map _).sum_eq

theorem psiMinus_comps_le {b : ℕ → ℝ} (hb : T4.BootProps b) {H : Graph} (hH : H.WF) :
    ((componentGraphs H).map (psiMinusPort b)).sum ≤ psiPort b H := by
  rw [← components_psi b hH]
  apply list_sum_map_le _ _ _
  intro C _
  unfold psiMinusPort
  linarith [T4.BasicAux.runMin_nonneg hb (minDegree C)]

/-! ## The start value and the initial deletions -/

theorem reduceLoop_noDel (fuel : Nat) : ∀ (G : Graph) (stack : List Nat) (opsRev : List Op),
    (∀ o ∈ opsRev, ∀ w, o ≠ Op.del w) →
    ∀ o ∈ (reduceLoop fuel G stack opsRev).2.1, ∀ w, o ≠ Op.del w := by
  induction fuel with
  | zero =>
    intro G stack opsRev h o ho
    cases stack <;> simp only [reduceLoop, List.mem_reverse] at ho <;> exact h o ho
  | succ k 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 G rest opsRev h o ho
      · split at ho
        · exact ih _ _ _ (by
            intro o' ho' w hw
            rcases List.mem_cons.1 ho' with rfl | ho''
            · cases hw
            · exact h o' ho'' w hw) o ho
        · exact ih _ _ _ (by
            intro o' ho' w hw
            rcases List.mem_cons.1 ho' with rfl | ho''
            · cases hw
            · exact h o' ho'' w hw) o ho

theorem deletedSet_nil_of {ops : List Op} (h : ∀ o ∈ ops, ∀ w, o ≠ Op.del w) :
    deletedSet ops = [] := by
  unfold deletedSet
  rw [List.filterMap_eq_nil_iff]
  intro a ha
  cases a with
  | red v nb => rfl
  | del w => exact absurd rfl (h _ ha w)

theorem reduceRecordF_deleted (G : Graph) : deletedSet (reduceRecordF G).2.1 = [] := by
  apply deletedSet_nil_of
  intro o ho w
  unfold reduceRecordF at ho
  exact reduceLoop_noDel _ _ _ _ (by simp) o ho w

/-- The state of the loop in `algoT4Full` (with its fuel), as a function of `G`. -/
def t4Run (G : Graph) : List FinalEntry × List Op × Bool :=
  t4Loop (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
    (componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse []
    (reduceRecordF (nonIsolated G).copy).2.1

theorem start_le (hMax : ReduceRecordMaximal) {G : Graph} (hG : G.WF) :
    T4Pot T4.sigma ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse) []
      (reduceRecordF (nonIsolated G).copy).2.1 ≤ psiPort T4.sigma G := by
  have hG0 : (nonIsolated G).WF := (inducedSpec G _ hG).1
  have hC : (nonIsolated G).copy.WF := (inducedSpec _ _ hG0).1
  have hm := hMax _ hC
  have hs := reduceRecordSpec _ hC
  have hperm : (((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse).map
      (psiMinusPort T4.sigma)).sum
      = ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).map
      (psiMinusPort T4.sigma)).sum :=
    ((List.reverse_perm _).map _).sum_eq
  simp only [T4Pot, reduceRecordF_deleted, List.map_nil, List.append_nil, List.length_nil,
    Nat.cast_zero, zero_add]
  rw [hperm]
  calc _ ≤ psiPort T4.sigma (reduceRecordF (nonIsolated G).copy).1 :=
        psiMinus_comps_le sigma_bp hs.1
    _ ≤ psiPort T4.sigma (nonIsolated G).copy :=
        psi_le_of_reduce sigma_bp hC hs.1 hs.2.1 hm.2.2
    _ = psiPort T4.sigma (nonIsolated G) := psi_copy hG0
    _ = psiPort T4.sigma G := psi_nonIsolated sigma_bp.zero.1 hG

/-! ## The run -/

theorem run_facts (hRun : T4LoopRun) (hInit : T4LoopInvInit) (G : Graph) (hG : G.WF) :
    T4LoopInv (nonIsolated G) [] (t4Run G).1 (t4Run G).2.1 ∧
    T4Pot T4.sigma [] (t4Run G).1 (t4Run G).2.1 ≤
      T4Pot T4.sigma ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse) []
        (reduceRecordF (nonIsolated G).copy).2.1 ∧
    ((t4Run G).2.2 = false → ∀ e ∈ (t4Run G).1, e.kind = FinalKind.sweep →
      e.graph.maxDegree ≤ 5) := by
  refine hRun (nonIsolated G) (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
    ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse) [] _
    (inducedSpec G _ hG).1 (hInit G hG) ?_
  intro e he
  simp at he

theorem fallback_run {G : Graph} {lab : Labeler} (hfb : (algoT4Full G lab).fallback = false) :
    (t4Run G).2.2 = false := by
  have h : ((reduceRecordF (nonIsolated G).copy).2.2 || (t4Run G).2.2 ||
      (((t4Run G).1.map (t4Decompose lab)).any (·.2)) ||
      (undoF (nonIsolated G) (t4Run G).2.1 (unionAll ((t4Run G).1.map (·.graph)))
        (((t4Run G).1.map (t4Decompose lab)).flatMap (·.1))).2) = false := hfb
  simp only [Bool.or_eq_false_iff] at h
  exact h.1.1.2

/-! ## Maximum degree -/

theorem foldl_max_ge (G : Graph) : ∀ (l : List Nat) (m : Nat),
    m ≤ l.foldl (fun m v => max m (G.degree v)) m
  | [], _ => le_rfl
  | x :: xs, m => le_trans (le_max_left m (G.degree x)) (foldl_max_ge G xs _)

theorem foldl_max_mem (G : Graph) : ∀ (l : List Nat) (m v : Nat), v ∈ l →
    G.degree v ≤ l.foldl (fun m v => max m (G.degree v)) m
  | [], _, _, h => by simp at h
  | x :: xs, m, v, h => by
    rw [List.foldl_cons]
    rcases List.mem_cons.1 h with rfl | h'
    · exact le_trans (le_max_right _ _) (foldl_max_ge G xs _)
    · exact foldl_max_mem G xs _ v h'

theorem maxDegLE_of_maxDegree {G : Graph} {k : Nat} (h : G.maxDegree ≤ k) :
    G.MaxDegLE k := by
  intro v hv
  have := foldl_max_mem G G.nodes 0 v hv
  unfold Graph.maxDegree at h
  exact le_trans this h

end D5

open D5 in

/-- (D5, first theorem) The deletion-process bound from the run of `t4Loop`. -/
theorem deletionProcessBound_of (hRun : T4LoopRun) (hInit : T4LoopInvInit)
    (hMax : ReduceRecordMaximal) : DeletionProcessBound := by
  intro G hG lab hfb
  obtain ⟨_, h2, _⟩ := run_facts hRun hInit G hG
  have hs := start_le hMax hG
  have hfin : ((algoT4Full G lab).numDeleted : ℝ) +
      ((algoT4Full G lab).final.map fun e => psiMinusPort T4.sigma e.graph).sum
      = ((deletedSet (t4Run G).2.1).length : ℝ) +
        (((t4Run G).1.map fun e => e.graph).map (psiMinusPort T4.sigma)).sum := by
    simp only [List.map_map]
    rfl
  rw [hfin]
  unfold T4Pot at h2 hs
  simp only [List.nil_append] at h2 hs
  linarith

open D5 in

/-- (D5, second theorem) The final facts of `algo_T4` without fallback. -/
theorem t4FinalFacts_of (hRun : T4LoopRun) (hInit : T4LoopInvInit) : T4FinalFacts := by
  intro G hG lab hfb e he
  obtain ⟨h1, _, h3⟩ := run_facts hRun hInit G hG
  have hl := fallback_run hfb
  have he' : e ∈ (t4Run G).1 := he
  have hmem : e.graph ∈ ([] ++ (t4Run G).1.map (·.graph)) := by
    simpa using List.mem_map_of_mem (f := fun e : FinalEntry => e.graph) he'
  have hwf : e.graph.WF := h1.1.1 e.graph hmem
  have hsub : ∀ x ∈ e.graph.nodes, x ∈ (nonIsolated G).nodes := fun x hx =>
    (h1.1.2.2.1 e.graph hmem x hx).1
  refine ⟨h1.2.2.2.1 e.graph hmem, ?_, ?_⟩
  · exact (hwf.nodup.subperm hsub).length_le
  · intro hk
    exact maxDegLE_of_maxDegree (h3 hl e he' hk)

#print axioms deletionProcessBound_of
#print axioms t4FinalFacts_of

end CubicPathwidth.Alg