import CubicPathwidth.Alg.Spec

/-!
# T3: one run of the work loop of `algo_T4` preserves the invariant

Proof of `T4LoopPreserves` (Spec.lean, section 5) from the graph-layer specs as hypotheses.
Induction on the fuel. Sweep and thin steps only move a graph between the stack and
`final` (a permutation of the graph list, same `ops`). A commit step replaces the
graph `J` by the component graphs of the reduced `J.copy.removeNode w`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace T3

/-! ## Deleted sets and permutations -/

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

theorem deletedSet_nil_of_red (l : List Op) (h : ∀ o ∈ l, ∃ v nb, o = Op.red v nb) :
    deletedSet l = [] := by
  unfold deletedSet
  rw [List.filterMap_eq_nil_iff]
  intro o ho
  obtain ⟨v, nb, rfl⟩ := h o ho
  rfl

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

theorem symm_disj {A B : Graph} (h : ∀ x, x ∈ A.nodes → x ∉ B.nodes) :
    ∀ x, x ∈ B.nodes → x ∉ A.nodes :=
  fun x hxB hxA => h x hxA hxB

/-- `T4Inv` depends on the list of graphs only through its membership, up to permutation. -/
theorem T4Inv_perm {G0 : Graph} {gs gs' : List Graph} {ops : List Op}
    (h : T4Inv G0 gs ops) (hp : gs.Perm gs') : T4Inv G0 gs' ops := by
  obtain ⟨h1, h2, h3, h4, h5⟩ := h
  refine ⟨fun J hJ => h1 J (hp.symm.subset hJ), ?_,
    fun J hJ => h3 J (hp.symm.subset hJ), h4, ?_⟩
  · exact (List.Perm.pairwise_iff (R := fun A B : Graph => ∀ x, x ∈ A.nodes → x ∉ B.nodes)
      (fun {A B} h => symm_disj h) hp).1 h2
  · intro x y hxy hx hy
    obtain ⟨J, hJ, hxJ⟩ := hx
    obtain ⟨J', hJ', hyJ'⟩ := hy
    obtain ⟨K, hK, hA⟩ :=
      h5 x y hxy ⟨J, hp.symm.subset hJ, hxJ⟩ ⟨J', hp.symm.subset hJ', hyJ'⟩
    exact ⟨K, hp.subset hK, hA⟩

/-! ## Maximum degree and the choice of `w` -/

theorem foldl_max_attained (f : Nat → Nat) (l : List Nat) (m0 : Nat) :
    l.foldl (fun m v => max m (f v)) m0 = m0 ∨
      ∃ v ∈ l, l.foldl (fun m v => max m (f v)) m0 = f v := by
  induction l generalizing m0 with
  | nil => exact Or.inl rfl
  | cons a l ih =>
    rw [List.foldl_cons]
    rcases ih (max m0 (f a)) with h | ⟨v, hv, h⟩
    · by_cases hc : m0 ≤ f a
      · right
        exact ⟨a, List.mem_cons_self, by rw [h, max_eq_right hc]⟩
      · left
        rw [h, max_eq_left (le_of_lt (not_le.mp hc))]
    · right
      exact ⟨v, List.mem_cons_of_mem a hv, h⟩

theorem maxDegree_attained (J : Graph) (h : 0 < J.maxDegree) :
    ∃ v ∈ J.nodes, J.degree v = J.maxDegree := by
  unfold Graph.maxDegree at h ⊢
  rcases foldl_max_attained (fun v => J.degree v) J.nodes 0 with h0 | ⟨v, hv, hfv⟩
  · rw [h0] at h
    omega
  · exact ⟨v, hv, hfv.symm⟩

theorem min?_pool_mem (pool : List Nat) (hne : pool ≠ []) :
    ∃ m, pool.min? = some m ∧ m ∈ pool := by
  obtain ⟨m, hm⟩ := Option.isSome_iff_exists.1 (List.isSome_min?_of_ne_nil hne)
  exact ⟨m, hm, List.min?_mem hm⟩

theorem pool_choose_mem (J : Graph) (pool : List Nat) (hne : pool ≠ [])
    (hsub : ∀ a ∈ pool, a ∈ J.nodes) : (pool.min?).getD 0 ∈ J.nodes := by
  obtain ⟨m, hm, hmp⟩ := min?_pool_mem pool hne
  rw [hm, Option.getD_some]
  exact hsub m hmp

theorem t4ChooseW_mem (J : Graph) (h : 0 < J.maxDegree) : t4ChooseW J ∈ J.nodes := by
  obtain ⟨v, hv, hdeg⟩ := maxDegree_attained J h
  unfold t4ChooseW
  dsimp only
  have hvc : v ∈ J.nodes.filter (fun u => J.degree u == J.maxDegree) :=
    List.mem_filter.2 ⟨hv, by simp [hdeg]⟩
  refine pool_choose_mem J _ ?_ ?_
  · split
    · intro h'
      rw [h'] at hvc
      simp at hvc
    · rename_i hg
      intro h'
      simp [h'] at hg
  · split
    · intro a ha
      exact (List.mem_filter.1 ha).1
    · intro a ha
      exact (List.mem_filter.1 (List.mem_filter.1 ha).1).1

/-! ## Reduction of one commit step -/

theorem pairwise_disj_of_nodup_flatten (L : List (List Nat)) (h : L.flatten.Nodup) :
    L.Pairwise (fun a b => ∀ x ∈ a, x ∉ b) :=
  ((List.nodup_flatten.1 h).2).imp fun hab _ hx hy => hab hx hy

theorem componentGraphs_mem {Js C : Graph} (hC : C ∈ componentGraphs Js) :
    ∃ c ∈ Js.components, Js.induced c.contains = C := by
  unfold componentGraphs at hC
  exact List.mem_map.1 hC

theorem mem_componentGraphs_of {Js : Graph} {c : List Nat} (hc : c ∈ Js.components) :
    Js.induced c.contains ∈ componentGraphs Js := by
  unfold componentGraphs
  exact List.mem_map.2 ⟨c, hc, rfl⟩

/-- Invariant after a commit step: the component graphs of `Js` replace `J` in front of
`rest ++ F`, and the new deleted vertex `w` (the only one added to `deletedSet`) is a
node of `J` that lies in no other graph. -/
theorem commit_inv (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (G0 J K Js : Graph) (rest F : List Graph) (ops red : List Op) (w : Nat)
    (hInv : T4Inv G0 (J :: (rest ++ F)) ops)
    (hw : w ∈ J.nodes)
    (hK : ∀ x, x ∈ K.nodes ↔ x ∈ J.nodes ∧ x ≠ w)
    (hKadj : ∀ x y, x ≠ w → y ≠ w → J.Adj x y → K.Adj x y)
    (hJsWF : Js.WF)
    (hJsSub : ∀ x ∈ Js.nodes, x ∈ K.nodes)
    (hJsAdj : ∀ x y, x ∈ Js.nodes → y ∈ Js.nodes → K.Adj x y → Js.Adj x y)
    (hred : ∀ o ∈ red, ∃ v nb, o = Op.red v nb) :
    T4Inv G0 (componentGraphs Js ++ (rest ++ F)) (ops ++ (Op.del w :: red)) := by
  obtain ⟨hWFs, hPair, hNodes, hDel, hEdge⟩ := hInv
  have hJWF : J.WF := hWFs J List.mem_cons_self
  have hJdisj : ∀ B ∈ rest ++ F, ∀ x ∈ J.nodes, x ∉ B.nodes :=
    fun B hB x hx => (List.pairwise_cons.1 hPair).1 B hB x hx
  have hPairRest : (rest ++ F).Pairwise (fun A B : Graph => ∀ x, x ∈ A.nodes → x ∉ B.nodes) :=
    (List.pairwise_cons.1 hPair).2
  obtain ⟨hcperm, _, hclosed⟩ := hComp Js hJsWF
  have hcompDisj : (Js.components).Pairwise (fun a b => ∀ x ∈ a, x ∉ b) :=
    pairwise_disj_of_nodup_flatten _ (hcperm.nodup_iff.2 hJsWF.nodup)
  have hCnodes : ∀ c : List Nat, ∀ z, z ∈ (Js.induced c.contains).nodes ↔
      z ∈ Js.nodes ∧ c.contains z = true :=
    fun c z => (hInd Js c.contains hJsWF).2.1 z
  have hCsWF : ∀ C ∈ componentGraphs Js, C.WF := by
    intro C hC
    obtain ⟨c, _, rfl⟩ := componentGraphs_mem hC
    exact (hInd Js c.contains hJsWF).1
  have hCsJc : ∀ c : List Nat, ∀ z ∈ (Js.induced c.contains).nodes,
      z ∈ Js.nodes ∧ z ∈ J.nodes ∧ z ≠ w := by
    intro c z hz
    have hzJs := ((hCnodes c z).1 hz).1
    obtain ⟨hzJ, hzw⟩ := (hK z).1 (hJsSub z hzJs)
    exact ⟨hzJs, hzJ, hzw⟩
  have hCsJ : ∀ C ∈ componentGraphs Js, ∀ z ∈ C.nodes,
      z ∈ Js.nodes ∧ z ∈ J.nodes ∧ z ≠ w := by
    intro C hC z hz
    obtain ⟨c, _, rfl⟩ := componentGraphs_mem hC
    exact hCsJc c z hz
  have hCsMem : ∀ z ∈ Js.nodes, ∃ c ∈ Js.components, z ∈ c := by
    intro z hz
    obtain ⟨c, hc, hzc⟩ := List.mem_flatten.1 (hcperm.symm.subset hz)
    exact ⟨c, hc, hzc⟩
  have hdelNew : ∀ x, x ∉ deletedSet ops → x ≠ w →
      x ∉ deletedSet (ops ++ (Op.del w :: red)) := by
    intro x hxo hxw hmem
    rw [deletedSet_append, deletedSet_del_cons, deletedSet_nil_of_red red hred] at hmem
    rcases List.mem_append.1 hmem with h | h
    · exact hxo h
    · simp at h
      exact hxw h
  have hdelMem : ∀ x, x ∈ deletedSet (ops ++ (Op.del w :: red)) ↔
      x ∈ deletedSet ops ∨ x = w := by
    intro x
    rw [deletedSet_append, deletedSet_del_cons, deletedSet_nil_of_red red hred]
    simp
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro C hC
    rcases List.mem_append.1 hC with hC | hC
    · exact hCsWF C hC
    · exact hWFs C (List.mem_cons_of_mem _ hC)
  · rw [List.pairwise_append]
    refine ⟨?_, hPairRest, ?_⟩
    · unfold componentGraphs
      rw [List.pairwise_map]
      refine hcompDisj.imp ?_
      intro a b hab x hxa hxb
      exact hab x (List.contains_iff_mem.1 ((hCnodes a x).1 hxa).2)
        (List.contains_iff_mem.1 ((hCnodes b x).1 hxb).2)
    · intro a ha b hb
      obtain ⟨c, _, rfl⟩ := componentGraphs_mem ha
      intro x hx hxb
      exact hJdisj b hb x (hCsJc c x hx).2.1 hxb
  · intro C hC x hx
    rcases List.mem_append.1 hC with hC | hC
    · obtain ⟨_, hxJ, hxw⟩ := hCsJ C hC x hx
      obtain ⟨hG, hnd⟩ := hNodes J List.mem_cons_self x hxJ
      exact ⟨hG, hdelNew x hnd hxw⟩
    · have hxw : x ≠ w := fun h => hJdisj C hC w hw (h ▸ hx)
      obtain ⟨hG, hnd⟩ := hNodes C (List.mem_cons_of_mem _ hC) x hx
      exact ⟨hG, hdelNew x hnd hxw⟩
  · intro x hx
    rcases (hdelMem x).1 hx with hx | hx
    · exact hDel x hx
    · rw [hx]
      exact (hNodes J List.mem_cons_self w hw).1
  · intro x y hxy hx hy
    obtain ⟨Cx, hCx, hxCx⟩ := hx
    obtain ⟨Cy, hCy, hyCy⟩ := hy
    have hox : ∃ B ∈ J :: (rest ++ F), x ∈ B.nodes := by
      rcases List.mem_append.1 hCx with h | h
      · exact ⟨J, List.mem_cons_self, (hCsJ Cx h x hxCx).2.1⟩
      · exact ⟨Cx, List.mem_cons_of_mem _ h, hxCx⟩
    have hoy : ∃ B ∈ J :: (rest ++ F), y ∈ B.nodes := by
      rcases List.mem_append.1 hCy with h | h
      · exact ⟨J, List.mem_cons_self, (hCsJ Cy h y hyCy).2.1⟩
      · exact ⟨Cy, List.mem_cons_of_mem _ h, hyCy⟩
    obtain ⟨B, hB, hBadj⟩ := hEdge x y hxy hox hoy
    rcases List.mem_cons.1 hB with hBJ | hB'
    · subst hBJ
      obtain ⟨hxJ, hyJ, _, _⟩ := hWF B hJWF x y hBadj
      have hxJs : x ∈ Js.nodes := by
        rcases List.mem_append.1 hCx with h | h
        · exact (hCsJ Cx h x hxCx).1
        · exact absurd hxCx (hJdisj Cx h x hxJ)
      have hyJs : y ∈ Js.nodes := by
        rcases List.mem_append.1 hCy with h | h
        · exact (hCsJ Cy h y hyCy).1
        · exact absurd hyCy (hJdisj Cy h y hyJ)
      have hxw : x ≠ w := ((hK x).1 (hJsSub x hxJs)).2
      have hyw : y ≠ w := ((hK y).1 (hJsSub y hyJs)).2
      have hJsadj : Js.Adj x y := hJsAdj x y hxJs hyJs (hKadj x y hxw hyw hBadj)
      obtain ⟨c, hc, hxc⟩ := hCsMem x hxJs
      have hyc : y ∈ c := hclosed c hc x hxc y hJsadj
      refine ⟨Js.induced c.contains, List.mem_append_left _ (mem_componentGraphs_of hc), ?_⟩
      rw [(hInd Js c.contains hJsWF).2.2]
      exact ⟨hJsadj, List.contains_iff_mem.2 hxc, List.contains_iff_mem.2 hyc⟩
    · exact ⟨B, List.mem_append_right _ hB', hBadj⟩

/-- The commit step, in the order used by `t4Loop` (`componentGraphs Js` reversed). -/
theorem commit_inv' (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (G0 J K Js : Graph) (rest F : List Graph) (ops red : List Op) (w : Nat)
    (hInv : T4Inv G0 (J :: (rest ++ F)) ops)
    (hw : w ∈ J.nodes)
    (hK : ∀ x, x ∈ K.nodes ↔ x ∈ J.nodes ∧ x ≠ w)
    (hKadj : ∀ x y, x ≠ w → y ≠ w → J.Adj x y → K.Adj x y)
    (hJsWF : Js.WF)
    (hJsSub : ∀ x ∈ Js.nodes, x ∈ K.nodes)
    (hJsAdj : ∀ x y, x ∈ Js.nodes → y ∈ Js.nodes → K.Adj x y → Js.Adj x y)
    (hred : ∀ o ∈ red, ∃ v nb, o = Op.red v nb) :
    T4Inv G0 ((componentGraphs Js).reverse ++ rest ++ F) (ops ++ (Op.del w :: red)) := by
  refine T4Inv_perm (commit_inv hWF hInd hComp G0 J K Js rest F ops red w hInv hw hK hKadj
    hJsWF hJsSub hJsAdj hred) ?_
  rw [List.append_assoc]
  exact ((List.reverse_perm _).append_right _).symm

/-- The specs of `reduceRecordF` on a well-formed graph. -/
theorem red_specs (hRed : ReduceRecordSpec) (K : Graph) (hK : K.WF) :
    (reduceRecordF K).1.WF ∧ (∀ x ∈ (reduceRecordF K).1.nodes, x ∈ K.nodes) ∧
    (∀ x y, x ∈ (reduceRecordF K).1.nodes → y ∈ (reduceRecordF K).1.nodes →
      K.Adj x y → (reduceRecordF K).1.Adj x y) ∧
    (∀ o ∈ (reduceRecordF K).2.1, ∃ v nb, o = Op.red v nb) := by
  have h := hRed K hK
  refine ⟨h.1, h.2.1, h.2.2.1, fun o ho => ?_⟩
  obtain ⟨v, nb, e, _⟩ := h.2.2.2.1 o ho
  exact ⟨v, nb, e⟩

/-- The facts about `K = J.copy.removeNode w` used by the commit step. -/
theorem copy_remove_facts (hRem : RemoveNodeSpec) (hInd : InducedSpec) (J : Graph)
    (hJ : J.WF) (w : Nat) :
    (J.copy.removeNode w).WF ∧
    (∀ x, x ∈ (J.copy.removeNode w).nodes ↔ x ∈ J.nodes ∧ x ≠ w) ∧
    (∀ x y, x ≠ w → y ≠ w → J.Adj x y → (J.copy.removeNode w).Adj x y) := by
  have hc := hInd J (fun _ => true) hJ
  have hcW : J.copy.WF := hc.1
  have hr := hRem J.copy w hcW
  refine ⟨hr.1, fun x => ?_, fun x y hxw hyw hadj => ?_⟩
  · rw [hr.2.1 x]
    exact ⟨fun h => ⟨((hc.2.1 x).1 h.1).1, h.2⟩, fun h => ⟨(hc.2.1 x).2 ⟨h.1, rfl⟩, h.2⟩⟩
  · rw [hr.2.2 x y]
    exact ⟨(hc.2.2 x y).2 ⟨hadj, rfl, rfl⟩, hxw, hyw⟩

/-- Moving the last element of a list to the front, up to permutation. -/
theorem perm_snoc (rest F : List Graph) (J : Graph) :
    (rest ++ (F ++ [J])).Perm (J :: (rest ++ F)) := by
  have h := @List.perm_append_comm _ (rest ++ F) [J]
  simpa [List.append_assoc] using h

theorem thinOK_sweep (final : List FinalEntry) (hThin : ThinOK final) (J : Graph) :
    ThinOK (final ++ [FinalEntry.mk J FinalKind.sweep []]) := by
  intro e he x hx
  rcases List.mem_append.1 he with he | he
  · exact hThin e he x hx
  · rw [List.mem_singleton] at he
    subst he
    simp [deletedSet] at hx

theorem thinOK_sweep_list (final : List FinalEntry) (hThin : ThinOK final) (L : List Graph) :
    ThinOK (final ++ L.map fun J => FinalEntry.mk J FinalKind.sweep []) := by
  intro e he x hx
  rcases List.mem_append.1 he with he | he
  · exact hThin e he x hx
  · obtain ⟨J, _, rfl⟩ := List.mem_map.1 he
    simp [deletedSet] at hx

theorem thinOK_thin (final : List FinalEntry) (hThin : ThinOK final) (J : Graph) (w : Nat)
    (red : List Op) (hred : ∀ o ∈ red, ∃ v nb, o = Op.red v nb) (hw : w ∈ J.nodes) :
    ThinOK (final ++ [FinalEntry.mk J FinalKind.thin (Op.del w :: red)]) := by
  intro e he x hx
  rcases List.mem_append.1 he with he | he
  · exact hThin e he x hx
  · rw [List.mem_singleton] at he
    subst he
    rw [deletedSet_del_cons, deletedSet_nil_of_red red hred] at hx
    simp only [List.mem_singleton] at hx
    subst hx
    exact hw

theorem map_graph_append_sweep (F : List FinalEntry) (L : List Graph) :
    (F ++ L.map fun J => FinalEntry.mk J FinalKind.sweep []).map (fun e => e.graph) =
      F.map (fun e => e.graph) ++ L := by
  rw [List.map_append, List.map_map]
  congr 1
  exact List.map_id' L

/-- Appending one entry `⟨J, k, t⟩` to `final` moves `J` (up to permutation) to the front of
the stack. -/
theorem perm_entry_snoc (rest : List Graph) (final : List FinalEntry) (J : Graph)
    (k : FinalKind) (t : List Op) :
    (J :: (rest ++ final.map (fun e => e.graph))).Perm
      (rest ++ (final ++ [FinalEntry.mk J k t]).map (fun e => e.graph)) := by
  have hm : (final ++ [FinalEntry.mk J k t]).map (fun e => e.graph) =
      final.map (fun e => e.graph) ++ [J] := by
    simp
  rw [hm]
  exact (perm_snoc rest _ J).symm

/-- One run of the work loop, by induction on the fuel. -/
theorem loop_preserves (hWF : WFBasics) (hRem : RemoveNodeSpec) (hInd : InducedSpec)
    (hComp : ComponentsSpec) (hRed : ReduceRecordSpec) : T4LoopPreserves := by
  unfold T4LoopPreserves
  intro G0 fuel
  induction fuel with
  | zero =>
    intro stack final ops _ hInv hThin
    cases stack with
    | nil =>
      rw [t4Loop]
      exact ⟨by simpa using hInv, hThin⟩
    | cons J rest =>
      rw [t4Loop]
      refine ⟨T4Inv_perm hInv ?_, thinOK_sweep_list final hThin (J :: rest)⟩
      rw [map_graph_append_sweep]
      exact List.perm_append_comm
  | succ f ih =>
    intro stack final ops hG0 hInv hThin
    cases stack with
    | nil =>
      rw [t4Loop]
      exact ⟨by simpa using hInv, hThin⟩
    | cons J rest =>
      have hJ : J.WF := hInv.1 J List.mem_cons_self
      by_cases hmax : J.maxDegree ≤ 5
      · rw [t4Loop]; simp only [hmax, ↓reduceIte]
        exact ih rest (final ++ [FinalEntry.mk J FinalKind.sweep []]) ops hG0
          (T4Inv_perm hInv (perm_entry_snoc rest final J FinalKind.sweep []))
          (thinOK_sweep final hThin J)
      · have hpos : 0 < J.maxDegree := by omega
        have hwmem := t4ChooseW_mem J hpos
        have hK := copy_remove_facts hRem hInd J hJ (t4ChooseW J)
        have hspec := red_specs hRed _ hK.1
        rw [t4Loop]; simp only [hmax, ↓reduceIte]
        by_cases hz : (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1.numNodes = 0
        · simp only [hz, ↓reduceIte]
          exact ih rest (final ++ [FinalEntry.mk J FinalKind.thin
              (Op.del (t4ChooseW J) :: (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1)])
            ops hG0
            (T4Inv_perm hInv (perm_entry_snoc rest final J FinalKind.thin _))
            (thinOK_thin final hThin J (t4ChooseW J) _ hspec.2.2.2 hwmem)
        · simp only [hz, ↓reduceIte]
          exact 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))
            hG0
            (commit_inv' hWF hInd hComp G0 J (J.copy.removeNode (t4ChooseW J))
              (reduceRecordF (J.copy.removeNode (t4ChooseW J))).1 rest
              (final.map (fun e : FinalEntry => e.graph))
              ops (reduceRecordF (J.copy.removeNode (t4ChooseW J))).2.1 (t4ChooseW J) hInv hwmem
              hK.2.1 hK.2.2 hspec.1 hspec.2.1 hspec.2.2.1 hspec.2.2.2) hThin

end T3

/-- Theorem T3 (Stage 1): one run of the work loop of `algo_T4` preserves the
invariant `T4Inv` and `ThinOK`, from the graph-layer specs. -/
theorem t4LoopPreserves_of (hWF : WFBasics) (hRem : RemoveNodeSpec) (hInd : InducedSpec)
    (hComp : ComponentsSpec) (hRed : ReduceRecordSpec) : T4LoopPreserves :=
  T3.loop_preserves hWF hRem hInd hComp hRed

end CubicPathwidth.Alg

end

#print axioms CubicPathwidth.Alg.t4LoopPreserves_of