CubicPathwidth.Alg.Proofs2.U5ThinWidth

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

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

/-!
# Task U5: width of a thin final component (`Spec2.lean` §4, `ThinComponentWidth`)

`thinComponentWidth_of` takes the Stage 2 statement `UndoWidth` as hypothesis and proves
`ThinComponentWidth`.

Route. A thin entry of `algo_T4` has `tops = Op.del w :: red`, where `red` is the output
of `reduceRecordF`, so `red` consists of reductions only (`reduceLoop_red`) and the
deleted set of `tops` is `[w]`. Its decomposition is `undoF e.graph tops Graph.empty []`.
Its flag is `false` because the global fallback flag is `false`, and `e.graph` is
well formed by the Stage 1 invariant `T4Inv` (`t4InitInv`, `t4LoopPreserves`). The bound
of `UndoWidth` then reads `1 + (-1) + 3 log₂ |V(e.graph)| + 1`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace U5

/-- Ops of a thin entry: a deletion followed by reductions only. -/
def ThinShape (t : List Op) : Prop :=
  ∃ w ops', t = Op.del w :: ops' ∧ ∀ o ∈ ops', ∃ v nb, o = Op.red v nb

/-- The loop of `reduceRecord` only produces reductions. -/
theorem reduceLoop_red : ∀ (fuel : ℕ) (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
  intro fuel
  induction fuel with
  | zero =>
    intro G stack opsRev hO
    cases stack with
    | nil =>
      rw [reduceLoop]
      intro o ho
      exact hO o (List.mem_reverse.1 ho)
    | cons v rest =>
      rw [reduceLoop]
      intro o ho
      exact hO o (List.mem_reverse.1 ho)
  | succ f ih =>
    intro G stack opsRev hO
    cases stack with
    | nil =>
      rw [reduceLoop]
      intro o ho
      exact hO o (List.mem_reverse.1 ho)
    | cons v rest =>
      rw [reduceLoop]
      by_cases hs : (!G.mem v || G.degree v > 2) = true
      · simp only [hs, ↓reduceIte]
        exact ih G rest opsRev hO
      · simp only [hs]
        apply ih
        intro o ho
        rcases List.mem_cons.1 ho with rfl | ho
        · exact ⟨v, G.nbrs v, rfl⟩
        · exact hO o ho

/-- Thin entries created by `t4Loop` have the shape `ThinShape`. -/
theorem thin_shape_loop : ∀ (fuel : ℕ) (stack : List Graph) (final : List FinalEntry)
    (ops : List Op), (∀ e ∈ final, e.kind = FinalKind.thin → ThinShape e.tops) →
    ∀ e ∈ (t4Loop fuel stack final ops).1, e.kind = FinalKind.thin → ThinShape e.tops := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack final ops hfin
    cases stack with
    | nil =>
      rw [t4Loop]
      exact hfin
    | cons J rest =>
      rw [t4Loop]
      intro e he hk
      rcases List.mem_append.1 he with he | he
      · exact hfin e he hk
      · obtain ⟨J', _, rfl⟩ := List.mem_map.1 he
        simp at hk
  | succ f ih =>
    intro stack final ops hfin
    cases stack with
    | nil =>
      rw [t4Loop]
      exact hfin
    | cons J rest =>
      by_cases hmax : J.maxDegree ≤ 5
      · rw [t4Loop]
        simp only [hmax, ↓reduceIte]
        refine ih rest _ ops ?_
        intro e he hk
        rcases List.mem_append.1 he with he | he
        · exact hfin e he hk
        · obtain rfl := List.mem_singleton.1 he
          simp at hk
      · rw [t4Loop]
        simp only [hmax, ↓reduceIte]
        by_cases hz : (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.numNodes = 0
        · simp only [hz, ↓reduceIte]
          refine ih rest _ _ ?_
          intro e he hk
          rcases List.mem_append.1 he with he | he
          · exact hfin e he hk
          · obtain rfl := List.mem_singleton.1 he
            refine ⟨t4ChooseW J, _, rfl, ?_⟩
            exact reduceLoop_red _ _ _ [] (by simp)
        · simp only [hz, ↓reduceIte]
          exact ih _ final _ hfin

end U5

/-- Width of a thin final component (`Spec2.lean` §4), from the `undo` width bridge. -/
theorem thinComponentWidth_of (h : UndoWidth) : ThinComponentWidth := by
  intro G hG lab hfb e he hk
  -- every decomposition of a final entry has flag `false`
  have hparts : ∀ e' ∈ (algoT4Full G lab).final, (t4Decompose lab e').2 = false := by
    have hf := hfb
    unfold algoT4Full at hf
    simp only [Bool.or_eq_false_iff, List.any_eq_false] at hf
    intro e' he'
    have h1 := hf.1.2 _ (List.mem_map_of_mem (f := t4Decompose lab) he')
    exact Bool.eq_false_iff.2 h1
  -- the final graphs are well formed (Stage 1 invariant)
  have hG0 : (nonIsolated G).WF := (inducedSpec G (fun v => G.degree v != 0) hG).1
  have hT0 : T4Inv (nonIsolated G) (componentGraphs (reduceRecordF (nonIsolated G).copy).1)
      (reduceRecordF (nonIsolated G).copy).2.1 := t4InitInv G hG
  have hStart : T4Inv (nonIsolated G)
      ((componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse ++
        ([] : List FinalEntry).map (·.graph))
      (reduceRecordF (nonIsolated G).copy).2.1 := by
    rw [List.map_nil, List.append_nil]
    exact T3.T4Inv_perm hT0 (List.reverse_perm _).symm
  have hL := t4LoopPreserves (nonIsolated G)
    (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1) _ [] _ hG0 hStart
    (by unfold ThinOK; intro e he; simp at he)
  obtain ⟨hT, _⟩ := hL
  have hWF : e.graph.WF := hT.1 e.graph (List.mem_map_of_mem he)
  -- the shape of the ops of a thin entry
  have hshape : U5.ThinShape e.tops :=
    U5.thin_shape_loop (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
      (componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse [] _ (by simp) e he hk
  obtain ⟨w, ops', htops, hred⟩ := hshape
  have hcard : (deletedSet e.tops).toFinset.card ≤ 1 := by
    rw [htops, T3.deletedSet_del_cons, T3.deletedSet_nil_of_red ops' hred]
    simp
  have hdec : t4Decompose lab e = undoF e.graph e.tops Graph.empty [] := by
    simp [t4Decompose, hk]
  have hflag : (undoF e.graph e.tops Graph.empty []).2 = false := by
    rw [← hdec]
    exact hparts e he
  have hw : pdWidth (undoF e.graph e.tops Graph.empty []).1 ≤
      ((deletedSet e.tops).toFinset.card : ℝ) + pdWidth [] +
        3 * (Nat.log 2 e.graph.numNodes : ℝ) + 1 :=
    h e.graph Graph.empty e.tops [] hWF hflag
  have hp : pdWidth [] = -1 := by
    unfold pdWidth maxBagCard
    simp
  have hc : ((deletedSet e.tops).toFinset.card : ℝ) ≤ 1 := by exact_mod_cast hcard
  rw [hdec]
  linarith

#print axioms CubicPathwidth.Alg.thinComponentWidth_of

end CubicPathwidth.Alg