import CubicPathwidth.Alg.Plan2Deletion

/-!
Stage 2 task D2c: `t4LoopRun_of` (the whole run of `t4Loop`, any fuel).

Hypotheses: `T4LoopInvStep` (D2a2) and `CommitBound` (D2b). Induction on `fuel`,
generalizing the stack, the final list and the ops. Sweep and thin steps only move a
graph between the stack and `final` (the potential is unchanged). A commit step appends
one deletion, so `deletedSet` grows by one, and the component graphs of the reduced
`J.copy.removeNode w` replace `J` in the potential, which does not increase by
`CommitBound`. Fuel exhaustion sets the flag `true`, so the sweep-degree clause is
vacuous there.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace D2c

/-! ## Deleted sets -/

theorem deletedSet_append' (a b : List Op) :
    deletedSet (a ++ b) = deletedSet a ++ deletedSet b := by
  unfold deletedSet
  exact List.filterMap_append

theorem deletedSet_del_cons' (w : Nat) (l : List Op) :
    deletedSet (Op.del w :: l) = w :: deletedSet l := by
  unfold deletedSet
  simp

/-- `reduce_record` records no deletions (every operation is a reduction). -/
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]

theorem deletedSet_reduceRecordF' (G : Graph) :
    deletedSet (reduceRecordF G).2.1 = [] := by
  unfold reduceRecordF
  rw [deletedSet_reduceLoop']
  rfl

/-! ## The potential along one step -/

/-- The potential is unchanged when a graph `J` moves from the head of the stack to the
end of `final` (as the entry `e` with graph `J`). -/
theorem pot_move (J : Graph) (rest : List Graph) (final : List FinalEntry) (ops : List Op)
    (e : FinalEntry) (he : e.graph = J) :
    T4Pot T4.sigma rest (final ++ [e]) ops = T4Pot T4.sigma (J :: rest) final ops := by
  unfold T4Pot
  simp only [List.map_append, List.map_cons, List.map_nil, List.sum_append, List.sum_cons,
    List.sum_nil, he, List.cons_append]
  ring

/-! ## The run -/

/-- The run, with the hypotheses as arguments; `G0.WF` is fixed. -/
theorem run_aux (hStep : T4LoopInvStep) (hCommit : CommitBound) (G0 : Graph) (hG0 : G0.WF)
    (fuel : Nat) :
    ∀ (stack : List Graph) (final : List FinalEntry) (ops : List Op),
      T4LoopInv G0 stack final ops →
      (∀ e ∈ final, e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5) →
      let r := t4Loop fuel stack final ops
      T4LoopInv G0 [] r.1 r.2.1 ∧
        T4Pot T4.sigma [] r.1 r.2.1 ≤ T4Pot T4.sigma stack final ops ∧
        (r.2.2 = false → ∀ e ∈ r.1, e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5) := by
  induction fuel with
  | zero =>
    intro stack final ops hInv hSw
    cases stack with
    | nil =>
      simp only [t4Loop]
      exact ⟨hInv, le_refl _, fun _ => hSw⟩
    | cons J rest =>
      simp only [t4Loop]
      refine ⟨hStep.1 G0 (J :: rest) final ops hG0 hInv, le_of_eq ?_, ?_⟩
      · unfold T4Pot
        simp only [List.map_append, List.map_map, List.map_cons, List.map_nil, List.sum_append,
          List.sum_cons, List.sum_nil, Function.comp_def]
        ring
      · intro h
        simp at h
  | succ f ih =>
    intro stack final ops hInv hSw
    cases stack with
    | nil =>
      simp only [t4Loop]
      exact ⟨hInv, le_refl _, fun _ => hSw⟩
    | cons J rest =>
      have hS := hStep.2 G0 J rest final ops hG0 hInv
      have hPiece : T4Piece J := hInv.2.2.2.1 J (List.mem_append_left _ List.mem_cons_self)
      by_cases hJ : J.maxDegree ≤ 5
      · -- sweep: `J` moves to `final`
        have hInv' := hS.1 hJ
        have hSw' : ∀ e ∈ final ++ [FinalEntry.mk J FinalKind.sweep []],
            e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5 := by
          intro e he hk
          rcases List.mem_append.mp he with h | h
          · exact hSw e h hk
          · rw [List.mem_singleton] at h
            subst h
            exact hJ
        obtain ⟨h1, h2, h3⟩ := ih rest _ ops hInv' hSw'
        have hEq : t4Loop (f + 1) (J :: rest) final ops =
            t4Loop f rest (final ++ [FinalEntry.mk J FinalKind.sweep []]) ops := by
          rw [t4Loop, if_pos hJ]
        rw [hEq]
        refine ⟨h1, le_trans h2 (le_of_eq (pot_move J rest final ops _ rfl)), h3⟩
      · -- not a sweep: thin finalization, or commit
        have hThinC := hS.2 hJ
        by_cases hr : (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.numNodes = 0
        · have hI := hThinC.1 hr
          have hSw' : ∀ e ∈ final ++ [FinalEntry.mk J FinalKind.thin
              (Op.del (t4ChooseW J) :: (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1)],
              e.kind = FinalKind.sweep → e.graph.maxDegree ≤ 5 := by
            intro e he hk
            rcases List.mem_append.mp he with h | h
            · exact hSw e h hk
            · rw [List.mem_singleton] at h
              subst h
              simp at hk
          obtain ⟨h1, h2, h3⟩ := ih rest _ ops hI hSw'
          rw [t4Loop, if_neg hJ]
          simp only [hr, ite_true]
          refine ⟨h1, le_trans h2 (le_of_eq (pot_move J rest final ops _ rfl)), ?_⟩
          intro hf
          exact h3 (Bool.or_eq_false_iff.mp hf).1
        · have hI := hThinC.2 hr
          have hC := hCommit J hPiece hJ hr
          obtain ⟨h1, h2, h3⟩ := ih ((componentGraphs (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1).reverse ++ rest) final
            (ops ++ (Op.del (t4ChooseW J) :: (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1)) hI hSw
          rw [t4Loop, if_neg hJ]
          simp only [hr, ite_false]
          refine ⟨h1, le_trans h2 ?_, ?_⟩
          · unfold T4Pot
            rw [deletedSet_append', deletedSet_del_cons', deletedSet_reduceRecordF']
            simp only [List.map_append, List.sum_append, List.map_reverse, List.sum_reverse,
              List.length_append, List.length_cons, List.length_nil, List.map_cons,
              List.sum_cons]
            push_cast
            linarith
          · intro hf
            exact h3 (Bool.or_eq_false_iff.mp hf).1

end D2c

/-- (D2c) The whole run of `t4Loop` (any fuel) from a state satisfying the invariant. -/
theorem t4LoopRun_of (hStep : T4LoopInvStep) (hCommit : CommitBound) : T4LoopRun := by
  intro G0 fuel stack final ops hG0 hInv hSw
  exact D2c.run_aux hStep hCommit G0 hG0 fuel stack final ops hInv hSw

#print axioms t4LoopRun_of

end CubicPathwidth.Alg

end