CubicPathwidth.Alg.Proofs2.A2MixedWidth

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

import CubicPathwidth.Alg.Plan2

/-!
Stage 2 task A2: `AlgoMixedWidth` from `UndoWidth`.

With the flag false, the undo flag is false. Every operation produced by `reduceLoop`
is a reduction, so `deletedSet` of the record is empty. The bags `bagsH` of `algo_mixed`
equal `plainLayout H _` in both cases (for `H` without nodes, `plainLayout` is empty).
-/

namespace CubicPathwidth.Alg

open Graph

namespace A2

/-- The deleted vertices of the record of `reduceLoop` are those of the initial ops. -/
theorem deletedSet_reduceLoop (fuel : Nat) : ∀ (G : Graph) (stack : List Nat) (opsRev : List Op),
    deletedSet (reduceLoop fuel G stack opsRev).2.1 = deletedSet opsRev.reverse := by
  induction fuel with
  | zero =>
    intro G stack opsRev
    cases stack with
    | nil => simp [reduceLoop]
    | cons v rest => simp [reduceLoop]
  | succ f ih =>
    intro G stack opsRev
    cases stack with
    | nil => simp [reduceLoop]
    | cons v rest =>
      simp only [reduceLoop]
      split
      · exact ih _ _ _
      · rw [ih]
        simp [deletedSet, List.filterMap_append]

/-- `reduce_record` records no deletions. -/
theorem deletedSet_reduceRecordF (G : Graph) :
    deletedSet (reduceRecordF G).2.1 = [] := by
  unfold reduceRecordF
  rw [deletedSet_reduceLoop]
  rfl

/-- The bags of `algo_mixed` are `plainLayout H _` (also for `H` without nodes). -/
theorem bagsH_eq (H : Graph) (lab : Labeler) :
    (if H.numNodes = 0 then [] else plainLayout H (lab H)) = plainLayout H (lab H) := by
  by_cases h : H.numNodes = 0
  · have hn : H.nodes = [] := List.eq_nil_of_length_eq_zero h
    simp [h, plainLayout, plainOrder, hn]
  · simp [h]

end A2

/-- `algo_mixed` (Theorems 2(b,c), 3): the width is at most the width of the plain sweep
of the reduced graph plus `3 log₂ n + 1`. -/
theorem algoMixedWidth_of (h : UndoWidth) : AlgoMixedWidth := by
  unfold AlgoMixedWidth
  intro G hG lab hflag
  simp only [algoMixedF, Bool.or_eq_false_iff] at hflag
  simp only [algoMixed, algoMixedF]
  rw [A2.bagsH_eq]
  have hk := h G (reduceRecordF G.copy).1 (reduceRecordF G.copy).2.1
    (if (reduceRecordF G.copy).1.numNodes = 0 then []
      else plainLayout (reduceRecordF G.copy).1 (lab (reduceRecordF G.copy).1)) hG hflag.2
  rw [A2.deletedSet_reduceRecordF, A2.bagsH_eq] at hk
  simp only [List.toFinset_nil, Finset.card_empty, Nat.cast_zero, zero_add] at hk
  exact hk

#print axioms CubicPathwidth.Alg.algoMixedWidth_of

end CubicPathwidth.Alg
Back to top