import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets

/-!
# Task N4: `AlgoT4NoFallback` (Stage 2, task N4)

`algoT4NoFallback_of` takes the Stage 2 statements `ReduceRecordNoFallback` (R1),
`T4LoopNoFallback` (D4), `UndoNoFallback` (U3), `T4LoopRun` (D2c) and `T4LoopInvInit`
(D2a1) as hypotheses and proves `AlgoT4NoFallback` (`Spec.lean` §7).

Route. Let `G0 := nonIsolated G`, `H`, `ops0` the output of `reduceRecordF G0.copy`,
`lp := t4Loop (2 |H| + 1) (componentGraphs H).reverse [] ops0`, `final := lp.1`,
`ops := lp.2.1`. The four flags of `algoT4Full` are:
* `reduceRecordF G0.copy`: R1;
* `lp`: D4;
* the parts: `.sweep` parts have no flag (`plainLayout`); a `.thin` part is
  `undoF e.graph e.tops Graph.empty []`, flag false by U3 with `R = Graph.empty`
  (the invariant gives `OpsRecord e.graph e.tops Graph.empty`);
* `undoF G0 ops R bagsR`: U3 with `R = unionAll final` and `bagsR` the concatenated
  decompositions, valid by `ConcatValid` and the Stage 1 part lemmas (as in
  `A3.finalStep`, which proves the same validity statement with `UndoValid`).
The invariant `T4LoopInv G0 [] final ops` comes from D2c applied at the initial state.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace N4

/-- Validity of the concatenated decompositions of the final graphs (the part of
`A3.finalStep` before the undo step). -/
theorem finalValidPD (hCat : ConcatValid) (hPL : PlainLayoutValid) (hUndo : UndoValid)
    (lab : Labeler) (G0 : Graph) (final : List FinalEntry) (ops : List Op)
    (hT : T4Inv G0 (final.map (·.graph)) ops) (hTh : ThinOK final) :
    ValidPD (unionAll (final.map (·.graph))) ((final.map (t4Decompose lab)).flatMap (·.1)) := by
  obtain ⟨hWF, hPw, -, -, -⟩ := hT
  have hPart := A3.finalPart hPL hUndo lab final hWF hTh
  have hparts : ∀ p ∈ final.map (fun e => (e.graph, (t4Decompose lab e).1)),
      p.1.WF ∧ ValidPD p.1 p.2 ∧ BagsWithin p.1 p.2 := by
    intro p hp
    obtain ⟨e, he, rfl⟩ := List.mem_map.1 hp
    exact ⟨hWF _ (List.mem_map_of_mem (f := fun e : FinalEntry => e.graph) he),
      (hPart e he).1, (hPart e he).2⟩
  have hdis : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).Pairwise
      (fun A B => ∀ x, x ∈ A.1.nodes → x ∉ B.1.nodes) :=
    List.pairwise_map.2 (List.pairwise_map.1 hPw)
  obtain ⟨hV, -⟩ := hCat (final.map (fun e => (e.graph, (t4Decompose lab e).1))) hparts hdis
  have e1 : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).map (·.1) =
      final.map (·.graph) := by
    simp only [List.map_map]
    rfl
  have e2 : (final.map (fun e => (e.graph, (t4Decompose lab e).1))).flatMap (·.2) =
      (final.map (t4Decompose lab)).flatMap (·.1) := A3.flatMap_parts lab final
  rw [e1, e2] at hV
  exact hV

/-- The flags of the parts and of the final undo, for a run that ends with the
invariant `T4LoopInv G0 [] final ops`. -/
theorem tailFlags (hU3 : UndoNoFallback) (hU : UnionAllSpec) (hCat : ConcatValid)
    (hPL : PlainLayoutValid) (hUndo : UndoValid) (lab : Labeler) (G0 : Graph)
    (final : List FinalEntry) (ops : List Op) (hG0 : G0.WF)
    (hInv : T4LoopInv G0 [] final ops) :
    (∀ e ∈ final, (t4Decompose lab e).2 = false) ∧
      (undoF G0 ops (unionAll (final.map (·.graph)))
        ((final.map (t4Decompose lab)).flatMap (·.1))).2 = false := by
  obtain ⟨hT, hTh, hOps, hPc, hThin⟩ := hInv
  simp only [List.nil_append] at hT hOps
  constructor
  · intro e he
    cases hk : e.kind with
    | sweep => simp [t4Decompose, hk]
    | thin =>
      have hw : e.graph.WF := hT.1 e.graph (List.mem_map_of_mem (f := fun e : FinalEntry => e.graph) he)
      obtain ⟨hR, -⟩ := hThin e he hk
      unfold t4Decompose
      rw [hk]
      exact hU3 e.graph Graph.empty e.tops [] hw A3.empty_wf hR A3.validPD_empty
  · have hRU := hU (final.map (·.graph)) (fun J hJ => hT.1 J hJ)
    exact hU3 G0 (unionAll (final.map (·.graph))) ops
      ((final.map (t4Decompose lab)).flatMap (·.1)) hG0 hRU.1 hOps
      (finalValidPD hCat hPL hUndo lab G0 final ops hT hTh)

end N4

/-- `AlgoT4NoFallback` from the Stage 2 hypotheses (task N4). -/
theorem algoT4NoFallback_of (hR1 : ReduceRecordNoFallback) (hD4 : T4LoopNoFallback)
    (hU3 : UndoNoFallback) (hRun : T4LoopRun) (hInit : T4LoopInvInit) :
    AlgoT4NoFallback := by
  intro G hG lab
  have hG0 : (nonIsolated G).WF := (inducedSpec G (fun v => G.degree v != 0) hG).1
  have hCopy : (nonIsolated G).copy.WF := (inducedSpec (nonIsolated G) (fun _ => true) hG0).1
  have hR0 := hR1 (nonIsolated G).copy hCopy
  have hLp := hD4 G hG
  have hInv := (hRun (nonIsolated G)
    (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
    (componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse []
    (reduceRecordF (nonIsolated G).copy).2.1 hG0 (hInit G hG)
    (by intro e he; simp at he)).1
  obtain ⟨hParts, hUn⟩ := N4.tailFlags hU3 unionAllSpec concatValid plainLayoutValid undoValid
    lab (nonIsolated G) _ _ hG0 hInv
  have hPa : ((t4Loop (2 * (reduceRecordF (nonIsolated G).copy).1.numNodes + 1)
      (componentGraphs (reduceRecordF (nonIsolated G).copy).1).reverse []
      (reduceRecordF (nonIsolated G).copy).2.1).1.map (t4Decompose lab)).any (·.2) = false := by
    rw [List.any_eq_false]
    intro p hp
    obtain ⟨e, he, rfl⟩ := List.mem_map.1 hp
    simp [hParts e he]
  unfold algoT4Full
  simp only [Bool.or_eq_false_iff]
  exact ⟨⟨⟨hR0, hLp⟩, hPa⟩, hUn⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.N4.finalValidPD
#print axioms CubicPathwidth.Alg.N4.tailFlags
#print axioms CubicPathwidth.Alg.algoT4NoFallback_of