import CubicPathwidth.Alg.Spec

/-!
# G3: `removeNode` satisfies `RemoveNodeSpec`

Task G3 of the formalisation. `removeNode G v` (for `v ∈ G`) folds
`a.insert u ((a.getD u []).erase v)` over the neighbour list of `v`, then erases the key
`v` and the node `v`. Neighbour lists are duplicate-free, so `v` occurs at most once in
each list; symmetry of `G` says that `v` occurs only in the lists of its neighbours.
-/

namespace CubicPathwidth.Alg

open Graph

namespace G3

/-- Folding the erasure of `v` over a duplicate-free list `l`: the value at `x` is
`(a.getD x []).erase v` if `x ∈ l`, and unchanged otherwise. -/
theorem fold_getD (v x : Nat) (l : List Nat) (a : Std.HashMap Nat (List Nat))
    (hl : l.Nodup) :
    (l.foldl (fun a u => a.insert u ((a.getD u []).erase v)) a).getD x [] =
      if x ∈ l then (a.getD x []).erase v else a.getD x [] := by
  induction l generalizing a with
  | nil => simp
  | cons u l ih =>
    rw [List.nodup_cons] at hl
    obtain ⟨hu, hl⟩ := hl
    simp only [List.foldl_cons]
    rw [ih _ hl]
    by_cases hx : x = u
    · subst hx
      have hxl : x ∉ l := hu
      simp [hxl]
    · have hx' : u ≠ x := fun h => hx h.symm
      simp [Std.HashMap.getD_insert, hx', hx]

/-- Membership in the key set after folding the insertions: keys are added. -/
theorem fold_contains (v : Nat) (l : List Nat) (a : Std.HashMap Nat (List Nat)) (x : Nat) :
    (l.foldl (fun a u => a.insert u ((a.getD u []).erase v)) a).contains x =
      (a.contains x || decide (x ∈ l)) := by
  induction l generalizing a with
  | nil => simp
  | cons u l ih =>
    simp only [List.foldl_cons, ih, Std.HashMap.contains_insert, List.mem_cons]
    by_cases hx : x = u
    · subst hx; simp
    · have hb : (u == x) = false := by simp [Ne.symm hx]
      simp [hb, hx]

variable {G : Graph} {v : Nat}

/-- The adjacency map of `removeNode` when `v` is a node. -/
theorem removeNode_adj (hm : G.mem v = true) :
    (G.removeNode v).adj =
      ((G.nbrs v).foldl (fun a u => a.insert u ((a.getD u []).erase v)) G.adj).erase v := by
  unfold Graph.removeNode
  simp [hm]

theorem removeNode_nodes (hm : G.mem v = true) :
    (G.removeNode v).nodes = G.nodes.erase v := by
  unfold Graph.removeNode
  simp [hm]

/-- Neighbour lists after `removeNode`. -/
theorem removeNode_nbrs (hG : G.WF) (hm : G.mem v = true) (x : Nat) :
    (G.removeNode v).nbrs x =
      if x = v then [] else if x ∈ G.nbrs v then (G.nbrs x).erase v else G.nbrs x := by
  show ((G.removeNode v).adj).getD x [] = _
  rw [removeNode_adj hm, Std.HashMap.getD_erase, fold_getD v x _ _ (hG.nbrs_nodup v)]
  by_cases hx : x = v
  · subst hx; simp
  · by_cases h : x ∈ G.nbrs v <;> simp [hx, Ne.symm hx, h] <;> rfl

/-- Adjacency after `removeNode` (with `v` a node). -/
theorem removeNode_adj_iff (hG : G.WF) (hm : G.mem v = true) (x y : Nat) :
    y ∈ (G.removeNode v).nbrs x ↔ y ∈ G.nbrs x ∧ x ≠ v ∧ y ≠ v := by
  rw [removeNode_nbrs hG hm x]
  by_cases hx : x = v
  · subst hx; simp
  · by_cases hxv : x ∈ G.nbrs v
    · simp only [hx, hxv, ↓reduceIte]
      rw [(hG.nbrs_nodup x).mem_erase_iff]
      constructor
      · rintro ⟨h1, h2⟩; exact ⟨h2, hx, h1⟩
      · rintro ⟨h2, _, h1⟩; exact ⟨h1, h2⟩
    · simp only [hx, hxv, ↓reduceIte]
      constructor
      · intro h
        refine ⟨h, hx, ?_⟩
        rintro rfl
        exact hxv (hG.symm _ _ h)
      · rintro ⟨h, _, _⟩; exact h

/-- Membership in the key set after `removeNode`. -/
theorem removeNode_mem (hG : G.WF) (hm : G.mem v = true) (x : Nat) :
    (G.removeNode v).mem x = true ↔ x ∈ G.nodes.erase v := by
  unfold Graph.mem
  rw [removeNode_adj hm, Std.HashMap.contains_erase, fold_contains, hG.nodup.mem_erase_iff]
  have hc : G.adj.contains x = true ↔ x ∈ G.nodes := hG.mem_iff x
  by_cases hxv : x = v
  · subst hxv; simp
  · by_cases hn : x ∈ G.nodes
    · have h1 := hc.mpr hn
      simp [h1, hn, hxv, Ne.symm hxv]
    · have h1 : G.adj.contains x = false := by
        rw [Bool.eq_false_iff]; exact fun h => hn (hc.mp h)
      have h2 : x ∉ G.nbrs v := fun h => hn (hG.nbrs_sub v x h)
      simp [h1, h2, hn]

/-- `removeNode` on a node. -/
theorem removeNode_wf (hG : G.WF) (hm : G.mem v = true) : (G.removeNode v).WF := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  · rw [removeNode_nodes hm]; exact hG.nodup.erase v
  · intro x
    rw [removeNode_mem hG hm x, removeNode_nodes hm]
  · intro x
    rw [removeNode_nbrs hG hm x]
    split_ifs
    · exact List.nodup_nil
    · exact (hG.nbrs_nodup x).erase v
    · exact hG.nbrs_nodup x
  · intro u w hw
    have h := (removeNode_adj_iff hG hm u w).mp hw
    rw [removeNode_nodes hm, hG.nodup.mem_erase_iff]
    exact ⟨h.2.2, hG.nbrs_sub u w h.1⟩
  · intro u w hw
    rw [removeNode_adj_iff hG hm] at hw ⊢
    exact ⟨hG.symm _ _ hw.1, hw.2.2, hw.2.1⟩
  · intro u hu
    rw [removeNode_adj_iff hG hm] at hu
    exact hG.loopless u hu.1

end G3

/-- `removeNode` satisfies its specification. -/
theorem removeNodeSpec_of (hWF : WFBasics) : RemoveNodeSpec := by
  intro G v hG
  by_cases hm : G.mem v = true
  · refine ⟨G3.removeNode_wf hG hm, ?_, ?_⟩
    · intro x
      rw [G3.removeNode_nodes hm, (hG.nodup).mem_erase_iff]
      exact and_comm
    · intro x y
      exact G3.removeNode_adj_iff hG hm x y
  · have hH : G.removeNode v = G := by
      unfold Graph.removeNode
      simp [hm]
    have hvn : v ∉ G.nodes := fun h => hm ((hG.mem_iff v).mpr h)
    have hnb : G.nbrs v = [] := by
      cases h : G.nbrs v with
      | nil => rfl
      | cons z zs =>
        have hz : z ∈ G.nbrs v := by rw [h]; exact List.mem_cons_self
        exact absurd (hG.nbrs_sub z v (hG.symm v z hz)) hvn
    rw [hH]
    refine ⟨hG, ?_, ?_⟩
    · intro x
      constructor
      · intro hx
        exact ⟨hx, fun h => hvn (h ▸ hx)⟩
      · exact fun h => h.1
    · intro x y
      constructor
      · intro hxy
        refine ⟨hxy, ?_, ?_⟩
        · rintro rfl
          rw [Graph.Adj, hnb] at hxy
          exact List.not_mem_nil hxy
        · rintro rfl
          exact hvn (hG.nbrs_sub x _ hxy)
      · exact fun h => h.1

#print axioms CubicPathwidth.Alg.removeNodeSpec_of

end CubicPathwidth.Alg