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

/-!
# Task N3: `algo_mixed` never falls back (`Spec.lean` §7)

`algoMixedNoFallback_of` takes the four Stage 2 statements `ReduceRecordNoFallback`,
`ReduceRecordMaximal`, `OpsRecordCongr`, `UndoNoFallback` as hypotheses and proves
`AlgoMixedNoFallback`.

Route: `G.copy` has the same graph as `G` (`inducedSpec`), so the recorded operations of
`reduce_record G.copy` are a legal record from `G` to `H` (`OpsRecordCongr`). The
reduction flag is `false` by `ReduceRecordNoFallback`. The bags of `H` are valid:
`plainLayoutValid` when `H` is nonempty, and `[]` when `H` is empty. Then `undo` does
not fall back (`UndoNoFallback`).
-/

namespace CubicPathwidth.Alg

open Graph

namespace N3

/-- The copy of a well-formed graph has the same nodes and adjacency. -/
theorem sameGraph_copy (hInd : InducedSpec) {G : Graph} (hG : G.WF) :
    SameGraph G.copy G := by
  have h := hInd G (fun _ => true) hG
  unfold Graph.copy
  refine ⟨fun v => ?_, fun u v => ?_⟩
  · rw [h.2.1 v]
    simp
  · rw [h.2.2 u v]
    simp

/-- The empty bag list decomposes the graph with no nodes. -/
theorem validPD_of_numNodes_zero {H : Graph} (h0 : H.numNodes = 0) : ValidPD H [] := by
  have hnil : H.nodes = [] := List.length_eq_zero_iff.1 h0
  unfold ValidPD
  refine ⟨?_, ?_, ?_⟩
  · intro v hv
    rw [hnil] at hv
    simp at hv
  · intro v hv
    rw [hnil] at hv
    simp at hv
  · intro u v hu
    rw [hnil] at hu
    simp at hu

end N3

/-- `algo_mixed` never falls back (`Spec.lean` §7), from the Stage 2 contracts of the
reduction layer and of `undo`. -/
theorem algoMixedNoFallback_of (hR1 : ReduceRecordNoFallback) (hMax : ReduceRecordMaximal)
    (hCongr : OpsRecordCongr) (hU : UndoNoFallback) : AlgoMixedNoFallback := by
  intro G hG lab
  have hc : G.copy.WF := (inducedSpec G (fun _ => true) hG).1
  have hR := hMax G.copy hc
  have hrec : OpsRecord G (reduceRecordF G.copy).2.1 (reduceRecordF G.copy).1 :=
    hCongr G.copy G _ _ hc hG (N3.sameGraph_copy inducedSpec hG) hR.1
  have hHwf : (reduceRecordF G.copy).1.WF := (reduceRecordSpec G.copy hc).1
  have hbags : ValidPD (reduceRecordF G.copy).1
      (if (reduceRecordF G.copy).1.numNodes = 0 then []
        else plainLayout (reduceRecordF G.copy).1 (lab (reduceRecordF G.copy).1)) := by
    by_cases h0 : (reduceRecordF G.copy).1.numNodes = 0
    · simp only [h0, ↓reduceIte]
      exact N3.validPD_of_numNodes_zero h0
    · simp only [h0, ↓reduceIte]
      exact (plainLayoutValid _ hHwf (lab (reduceRecordF G.copy).1)).1
  have hu := hU G (reduceRecordF G.copy).1 (reduceRecordF G.copy).2.1 _ hG hHwf hrec hbags
  unfold algoMixedF
  simp only [hR1 G.copy hc, hu, Bool.or_false]

#print axioms CubicPathwidth.Alg.algoMixedNoFallback_of

end CubicPathwidth.Alg