CubicPathwidth.Alg.Proofs2.D4LoopFuel

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

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

/-!
# Task D4: the deletion loop of `algo_T4` never runs out of fuel (`Spec2.lean` §2)

`t4LoopNoFallback_of` takes `ReduceRecordNoFallback` as hypothesis and proves
`T4LoopNoFallback`.

Route. The measure is `S(stack) = ∑_{J ∈ stack} |V(J)|`. Every graph in the work list is
well formed and has at least one node (components are nonempty and `induced` keeps the
nodes of a component). A sweep or thin step removes one graph of `S`-size `≥ 1`. A
commit step on `J` replaces `J` by the component graphs of `Js`, the reduction of
`K = J - w` with `w ∈ V(J)`, so the new total is at most `|V(J)| - 1 + S(rest)`
(`Js ⊆ K` and `|K| + 1 ≤ |J|`). Hence `S` drops by at least one per step, and the
initial total is at most `|V(H)| < 2|V(H)| + 1` (the fuel). The reduction flags inside
`t4Loop` are `false` by `ReduceRecordNoFallback`, applied to `J.copy.removeNode w`
(well formed by `copy_remove_facts`).
-/

namespace CubicPathwidth.Alg

open Graph

namespace D4

/-- Termwise comparison of sums over lists of naturals. -/
theorem sum_map_le {α : Type} (f g : α → ℕ) (l : List α) (h : ∀ a ∈ l, f a ≤ g a) :
    (l.map f).sum ≤ (l.map g).sum := by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [List.map_cons, List.sum_cons]
    exact Nat.add_le_add (h a (by simp)) (ih fun b hb => h b (List.mem_cons_of_mem _ hb))

/-- Reversing a list does not change the sum of the node counts. -/
theorem sum_reverse_map (L : List Graph) :
    (L.reverse.map Graph.numNodes).sum = (L.map Graph.numNodes).sum :=
  ((List.reverse_perm L).map Graph.numNodes).sum_eq

/-- Each component graph is well formed and has at least one node. -/
theorem componentGraphs_good {Js : Graph} (hJs : Js.WF) :
    ∀ C ∈ componentGraphs Js, C.WF ∧ 1 ≤ C.numNodes := by
  intro C hC
  obtain ⟨c, hc, rfl⟩ := T3.componentGraphs_mem hC
  refine ⟨(inducedSpec Js c.contains hJs).1, ?_⟩
  obtain ⟨hperm, hne, _⟩ := componentsSpec Js hJs
  obtain ⟨x, hx⟩ : ∃ x, x ∈ c := List.exists_mem_of_ne_nil c (hne c hc)
  have hxJs : x ∈ Js.nodes := hperm.subset (List.mem_flatten.2 ⟨c, hc, hx⟩)
  have hxC : x ∈ (Js.induced c.contains).nodes :=
    ((inducedSpec Js c.contains hJs).2.1 x).2 ⟨hxJs, List.contains_iff_mem.2 hx⟩
  unfold Graph.numNodes
  exact List.length_pos_of_mem hxC

/-- The node counts of the component graphs of `Js` add up to at most `Js.numNodes`. -/
theorem sum_numNodes_componentGraphs {Js : Graph} (hJs : Js.WF) :
    ((componentGraphs Js).map Graph.numNodes).sum ≤ Js.numNodes := by
  obtain ⟨hperm, _, _⟩ := componentsSpec Js hJs
  have hlen : (Js.components.map List.length).sum = Js.numNodes := by
    rw [← List.length_flatten, hperm.length_eq]
    rfl
  have hterm : ∀ c ∈ Js.components,
      (Js.induced c.contains).numNodes ≤ (fun c : List Nat => c.length) c := by
    intro c _
    have hw := (inducedSpec Js c.contains hJs).1
    have hsub : ∀ x ∈ (Js.induced c.contains).nodes, x ∈ c := by
      intro x hx
      exact List.contains_iff_mem.1 ((((inducedSpec Js c.contains hJs).2.1 x).1 hx).2)
    unfold Graph.numNodes
    exact (hw.nodup.subperm hsub).length_le
  unfold componentGraphs
  rw [List.map_map, ← hlen]
  exact sum_map_le _ _ _ fun c hc => hterm c hc

/-- The loop with fuel bounded below by the measure never raises the reduction flag. -/
theorem loop_noflag (hR1 : ReduceRecordNoFallback) :
    ∀ (fuel : ℕ) (stack : List Graph) (final : List FinalEntry) (ops : List Op),
      (∀ J ∈ stack, J.WF ∧ 1 ≤ J.numNodes) →
      (stack.map Graph.numNodes).sum ≤ fuel →
      (t4Loop fuel stack final ops).2.2 = false := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack final ops hst hsum
    cases stack with
    | nil => rw [t4Loop]
    | cons J rest =>
      exfalso
      have h1 := (hst J List.mem_cons_self).2
      simp only [List.map_cons, List.sum_cons] at hsum
      omega
  | succ f ih =>
    intro stack final ops hst hsum
    cases stack with
    | nil => rw [t4Loop]
    | cons J rest =>
      obtain ⟨hJ, hJn⟩ := hst J List.mem_cons_self
      have hrest : ∀ K ∈ rest, K.WF ∧ 1 ≤ K.numNodes :=
        fun K hK => hst K (List.mem_cons_of_mem _ hK)
      simp only [List.map_cons, List.sum_cons] at hsum
      by_cases hmax : J.maxDegree ≤ 5
      · rw [t4Loop]
        simp only [hmax, ↓reduceIte]
        exact ih rest _ ops hrest (by omega)
      · have hpos : 0 < J.maxDegree := by omega
        have hwmem := T3.t4ChooseW_mem J hpos
        have hK := T3.copy_remove_facts removeNodeSpec inducedSpec J hJ (t4ChooseW J)
        have hspec := T3.red_specs reduceRecordSpec _ hK.1
        have hRF := hR1 _ hK.1
        rw [t4Loop]
        simp only [hmax, ↓reduceIte]
        by_cases hz : (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.numNodes = 0
        · simp only [hz, ↓reduceIte]
          exact Bool.or_eq_false_iff.2 ⟨ih rest _ _ hrest (by omega), hRF⟩
        · simp only [hz, ↓reduceIte]
          -- the commit step
          set w := t4ChooseW J with hw
          set K := J.copy.removeNode w with hKdef
          set Js := (reduceRecordF K).1 with hJsdef
          have hJsWF : Js.WF := hspec.1
          have hJsSub : ∀ x ∈ Js.nodes, x ∈ K.nodes := hspec.2.1
          have hJsle : Js.numNodes ≤ K.numNodes := by
            unfold Graph.numNodes
            exact (hJsWF.nodup.subperm hJsSub).length_le
          have hwK : w ∉ K.nodes := fun h => ((hK.2.1 w).1 h).2 rfl
          have hnd : (w :: K.nodes).Nodup := List.nodup_cons.2 ⟨hwK, hK.1.nodup⟩
          have hsubJ : ∀ x ∈ w :: K.nodes, x ∈ J.nodes := by
            intro x hx
            rcases List.mem_cons.1 hx with rfl | hx
            · exact hwmem
            · exact ((hK.2.1 x).1 hx).1
          have hKlt : K.numNodes + 1 ≤ J.numNodes := by
            unfold Graph.numNodes
            simpa using (hnd.subperm hsubJ).length_le
          have hnew : ∀ C ∈ (componentGraphs Js).reverse ++ rest, C.WF ∧ 1 ≤ C.numNodes := by
            intro C hC
            rcases List.mem_append.1 hC with hC | hC
            · exact componentGraphs_good hJsWF C (List.mem_reverse.1 hC)
            · exact hrest C hC
          have hsumC := sum_numNodes_componentGraphs hJsWF
          have hsumNew : (((componentGraphs Js).reverse ++ rest).map Graph.numNodes).sum ≤ f := by
            rw [List.map_append, List.sum_append, sum_reverse_map]
            omega
          exact Bool.or_eq_false_iff.2 ⟨ih _ _ _ hnew hsumNew, hRF⟩

end D4

/-- `algo_T4`'s deletion loop has no fallback from the initial call (`Spec2.lean` §2),
from `ReduceRecordNoFallback`. -/
theorem t4LoopNoFallback_of (hR1 : ReduceRecordNoFallback) : T4LoopNoFallback := by
  intro G hG
  have hG0 : (nonIsolated G).WF := (inducedSpec G (fun v => G.degree v != 0) hG).1
  have hc : (nonIsolated G).copy.WF := (inducedSpec _ (fun _ => true) hG0).1
  have hH : (reduceRecordF (nonIsolated G).copy).1.WF := (reduceRecordSpec _ hc).1
  have hstack : ∀ J ∈ (componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse,
      J.WF ∧ 1 ≤ J.numNodes := by
    intro J hJ
    exact D4.componentGraphs_good hH J (List.mem_reverse.1 hJ)
  have hsum : ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse.map
      Graph.numNodes).sum ≤ 2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1 := by
    rw [D4.sum_reverse_map]
    have := D4.sum_numNodes_componentGraphs hH
    omega
  exact D4.loop_noflag hR1 _ _ [] _ hstack hsum

#print axioms CubicPathwidth.Alg.t4LoopNoFallback_of

end CubicPathwidth.Alg