CubicPathwidth.Alg.Proofs.G6UnionAll

Source file CubicPathwidth/Alg/Proofs/G6UnionAll.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Spec

/-!
# G6: `UnionAllSpec`

`unionAll gs = gs.foldl addGraph empty`, where `addGraph R J` adds the nodes of `J`
(`addNode`) and then the edges of `J.edgeList` (`addEdge`). We prove:

* `addNode_spec`: `addNode` keeps well-formedness, adds exactly the new node, and does
  not change adjacency;
* `edgeList_sound`, `edgeList_complete`: `J.edgeList` lists only edges of `J` and, for
  every edge `x y` of `J`, the pair `(x, y)` or `(y, x)` (the earlier endpoint in
  `J.nodes` emits the pair);
* `addEdges_spec`, `addGraph_spec`, `unionAll_gen`: folds of `addEdge` (using the
  hypothesis `AddEdgeSpec`), of `addGraph`, and `unionAll` on a general start graph.

The theorem `unionAllSpec_of` takes `WFBasics` and `AddEdgeSpec` as hypotheses.
-/

noncomputable section

namespace CubicPathwidth.Alg

namespace G6

open Graph

/-! ## 1. `addNode` -/

theorem fresh_nbrs (G : Graph) (v : Nat) (x : Nat) :
    (⟨G.nodes ++ [v], G.adj.insert v []⟩ : Graph).nbrs x
      = if x = v then [] else G.nbrs x := by
  show (G.adj.insert v []).getD x [] = if x = v then [] else G.adj.getD x []
  rw [Std.HashMap.getD_insert]
  by_cases hx : x = v
  · subst hx; simp
  · rw [if_neg hx]
    simp [Ne.symm hx]

theorem fresh_wf (G : Graph) (hG : G.WF) (v : Nat) (hv : v ∉ G.nodes) (hnb : G.nbrs v = []) :
    (⟨G.nodes ++ [v], G.adj.insert v []⟩ : Graph).WF := by
  have hmem : ∀ x, x ∈ G.nodes ++ [v] ↔ x ∈ G.nodes ∨ x = v := by
    intro x; simp
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  · show (G.nodes ++ [v]).Nodup
    rw [List.nodup_append]
    refine ⟨hG.nodup, by simp, ?_⟩
    intro a ha b hb
    simp only [List.mem_singleton] at hb
    subst hb
    exact fun h => hv (h ▸ ha)
  · intro w
    show (G.adj.insert v []).contains w = true ↔ w ∈ G.nodes ++ [v]
    rw [Std.HashMap.contains_insert, hmem]
    have h := hG.mem_iff w
    simp only [Graph.mem] at h
    rw [← h]
    simp only [Bool.or_eq_true, beq_iff_eq]
    tauto
  · intro w
    rw [fresh_nbrs]
    by_cases hw : w = v
    · simp [hw]
    · simp only [hw, ite_false]
      exact hG.nbrs_nodup w
  · intro u w h
    rw [fresh_nbrs] at h
    rw [hmem]
    by_cases hu : u = v
    · simp [hu] at h
    · simp only [hu, ite_false] at h
      exact Or.inl (hG.nbrs_sub u w h)
  · intro u w h
    rw [fresh_nbrs] at h ⊢
    by_cases hu : u = v
    · simp [hu] at h
    · simp only [hu, ite_false] at h
      have hwv : w ≠ v := by
        intro hwv
        subst hwv
        exact hv (hG.nbrs_sub u w h)
      simp only [hwv, ite_false]
      exact hG.symm u w h
  · intro w h
    rw [fresh_nbrs] at h
    by_cases hw : w = v
    · simp [hw] at h
    · simp only [hw, ite_false] at h
      exact hG.loopless w h

theorem addNode_spec (G : Graph) (hG : G.WF) (v : Nat) :
    (G.addNode v).WF ∧ (∀ x, x ∈ (G.addNode v).nodes ↔ x ∈ G.nodes ∨ x = v) ∧
      (∀ x y, (G.addNode v).Adj x y ↔ G.Adj x y) := by
  by_cases hm : G.mem v = true
  · have hv : v ∈ G.nodes := (hG.mem_iff v).1 hm
    have heq : G.addNode v = G := by simp [Graph.addNode, hm]
    rw [heq]
    refine ⟨hG, fun x => ?_, fun x y => Iff.rfl⟩
    constructor
    · intro h; exact Or.inl h
    · rintro (h | h)
      · exact h
      · rw [h]; exact hv
  · have hv : v ∉ G.nodes := fun h => hm ((hG.mem_iff v).2 h)
    have hnb : G.nbrs v = [] := by
      unfold Graph.nbrs
      apply Std.HashMap.getD_eq_fallback_of_contains_eq_false
      simpa [Graph.mem] using hm
    have hfresh : G.addNode v = ⟨G.nodes ++ [v], G.adj.insert v []⟩ := by
      simp [Graph.addNode, hm]
    rw [hfresh]
    have hW := fresh_wf G hG v hv hnb
    refine ⟨hW, fun x => ?_, fun x y => ?_⟩
    · show x ∈ G.nodes ++ [v] ↔ _
      simp
    · show y ∈ (⟨G.nodes ++ [v], G.adj.insert v []⟩ : Graph).nbrs x ↔ y ∈ G.nbrs x
      rw [fresh_nbrs]
      by_cases hx : x = v
      · rw [if_pos hx, hx, hnb]
      · rw [if_neg hx]

theorem addNodes_spec (ns : List Nat) : ∀ R : Graph, R.WF →
    (ns.foldl addNode R).WF ∧
    (∀ x, x ∈ (ns.foldl addNode R).nodes ↔ x ∈ R.nodes ∨ x ∈ ns) ∧
    (∀ x y, (ns.foldl addNode R).Adj x y ↔ R.Adj x y) := by
  induction ns with
  | nil => intro R hR; exact ⟨hR, fun x => by simp, fun x y => by simp⟩
  | cons v ns ih =>
    intro R hR
    obtain ⟨h1, h2, h3⟩ := addNode_spec R hR v
    obtain ⟨h4, h5, h6⟩ := ih (R.addNode v) h1
    rw [List.foldl_cons]
    refine ⟨h4, fun x => ?_, fun x y => ?_⟩
    · rw [h5, h2]
      simp only [List.mem_cons]
      tauto
    · rw [h6, h3]

/-! ## 2. `edgeList` -/

/-- One step of the fold defining `edgeList`, as a named function. -/
def stepE (G : Graph) (acc : Std.HashSet Nat × Array (Nat × Nat)) (u : Nat) :
    Std.HashSet Nat × Array (Nat × Nat) :=
  (acc.1.insert u,
    (G.nbrs u).foldl (fun o v => if acc.1.contains v then o else o.push (u, v)) acc.2)

theorem edgeList_eq (G : Graph) :
    G.edgeList = (G.nodes.foldl (stepE G)
      ((∅ : Std.HashSet Nat), (#[] : Array (Nat × Nat)))).2.toList := rfl

/-- The pairs emitted when processing the list `p` with `S` already seen (in order). -/
def E (G : Graph) : List Nat → List Nat → List (Nat × Nat)
  | _, [] => []
  | S, u :: p => ((G.nbrs u).filter (fun v => !S.contains v)).map (fun v => (u, v))
      ++ E G (u :: S) p

theorem nbrs_fold (u : Nat) (seen : Std.HashSet Nat) (S : List Nat)
    (hS : ∀ z, seen.contains z = true ↔ z ∈ S) :
    ∀ (l : List Nat) (out : Array (Nat × Nat)),
      (l.foldl (fun o v => if seen.contains v then o else o.push (u, v)) out).toList
        = out.toList ++ (l.filter (fun v => !S.contains v)).map (fun v => (u, v)) := by
  intro l
  induction l with
  | nil => intro out; simp
  | cons v l ih =>
    intro out
    simp only [List.foldl_cons]
    by_cases hv : seen.contains v = true
    · have hvS : v ∈ S := (hS v).1 hv
      have hvS' : (!S.contains v) = false := by simp [hvS]
      rw [if_pos hv, ih, List.filter_cons, hvS']
      simp
    · have hvS : v ∉ S := fun h => hv ((hS v).2 h)
      have hvS' : (!S.contains v) = true := by simp [hvS]
      rw [if_neg hv, ih, List.filter_cons, hvS']
      simp [Array.toList_push]

theorem foldl_E (G : Graph) : ∀ (p S : List Nat) (acc : Std.HashSet Nat × Array (Nat × Nat)),
    (∀ z, acc.1.contains z = true ↔ z ∈ S) →
    (p.foldl (stepE G) acc).2.toList = acc.2.toList ++ E G S p := by
  intro p
  induction p with
  | nil => intro S acc _; simp [E]
  | cons u p ih =>
    intro S acc hS
    rw [List.foldl_cons]
    have h1 : (stepE G acc u).2.toList
        = acc.2.toList ++ ((G.nbrs u).filter (fun v => !S.contains v)).map (fun v => (u, v)) := by
      unfold stepE
      exact nbrs_fold u acc.1 S hS (G.nbrs u) acc.2
    have h2 : ∀ z, (stepE G acc u).1.contains z = true ↔ z ∈ u :: S := by
      intro z
      show (acc.1.insert u).contains z = true ↔ z ∈ u :: S
      rw [Std.HashSet.contains_insert, Bool.or_eq_true, beq_iff_eq, hS z, List.mem_cons]
      exact or_congr eq_comm Iff.rfl
    rw [ih (u :: S) (stepE G acc u) h2, h1]
    simp only [E, List.append_assoc]

theorem edgeList_eq_E (G : Graph) : G.edgeList = E G [] G.nodes := by
  rw [edgeList_eq]
  have := foldl_E G G.nodes [] ((∅ : Std.HashSet Nat), (#[] : Array (Nat × Nat)))
    (by intro z; simp)
  simpa using this

theorem E_sound (G : Graph) : ∀ (p S : List Nat) (u v : Nat),
    (u, v) ∈ E G S p → u ∈ p ∧ v ∈ G.nbrs u := by
  intro p
  induction p with
  | nil => intro S u v h; simp [E] at h
  | cons w p ih =>
    intro S u v h
    simp only [E, List.mem_append, List.mem_map, List.mem_filter] at h
    rcases h with ⟨x, ⟨hx, _⟩, hxe⟩ | h
    · simp only [Prod.mk.injEq] at hxe
      obtain ⟨rfl, rfl⟩ := hxe
      exact ⟨List.mem_cons_self, hx⟩
    · obtain ⟨h1, h2⟩ := ih (w :: S) u v h
      exact ⟨List.mem_cons_of_mem w h1, h2⟩

theorem E_mem_of (G : Graph) : ∀ (a S b : List Nat) (x y : Nat),
    y ∈ G.nbrs x → y ∉ S → y ∉ a → (x, y) ∈ E G S (a ++ x :: b) := by
  intro a
  induction a with
  | nil =>
    intro S b x y hy hS _
    simp only [List.nil_append, E, List.mem_append, List.mem_map, List.mem_filter]
    left
    exact ⟨y, ⟨hy, by simp [hS]⟩, rfl⟩
  | cons c a ih =>
    intro S b x y hy hS hya
    simp only [List.cons_append, E, List.mem_append]
    right
    have hc : y ≠ c := fun h => hya (by simp [h])
    have hya' : y ∉ a := fun h => hya (List.mem_cons_of_mem c h)
    apply ih (c :: S) b x y hy
    · simp only [List.mem_cons, not_or]
      exact ⟨hc, hS⟩
    · exact hya'

theorem nodup_split {a b : List Nat} {x : Nat} (h : (a ++ x :: b).Nodup) :
    ∀ y ∈ b, y ∉ a := by
  intro y hyb hya
  exact (List.nodup_append.1 h).2.2 y hya y (List.mem_cons_of_mem x hyb) rfl

/-- Every listed pair is an edge of `J` between two nodes. -/
theorem edgeList_sound (J : Graph) (hJ : J.WF) (u v : Nat) (h : (u, v) ∈ J.edgeList) :
    J.Adj u v ∧ u ∈ J.nodes ∧ v ∈ J.nodes := by
  rw [edgeList_eq_E] at h
  obtain ⟨hu, hv⟩ := E_sound J J.nodes [] u v h
  exact ⟨hv, hu, hJ.nbrs_sub u v hv⟩

/-- For every edge `x y` of a well-formed graph, one of the two pairs is listed. -/
theorem edgeList_complete (J : Graph) (hJ : J.WF) (hW : WFBasics) (x y : Nat)
    (hxy : J.Adj x y) : (x, y) ∈ J.edgeList ∨ (y, x) ∈ J.edgeList := by
  rw [edgeList_eq_E]
  have hne : x ≠ y := (hW J hJ x y hxy).2.2.2
  have hy : y ∈ J.nodes := hJ.nbrs_sub x y hxy
  have hyx : x ∈ J.nbrs y := hJ.symm x y hxy
  have hx : x ∈ J.nodes := hJ.nbrs_sub y x hyx
  obtain ⟨a, b, hab⟩ := List.append_of_mem hx
  have hnd : (a ++ x :: b).Nodup := hab ▸ hJ.nodup
  by_cases hyb : y ∈ b
  · left
    rw [hab]
    exact E_mem_of J a [] b x y hxy (by simp) (nodup_split hnd y hyb)
  · right
    have hya : y ∈ a := by
      rw [hab] at hy
      rcases List.mem_append.1 hy with h | h
      · exact h
      · rcases List.mem_cons.1 h with h | h
        · exact absurd h.symm hne
        · exact absurd h hyb
    obtain ⟨a1, a2, hsplit⟩ := List.append_of_mem hya
    have hJ' : J.nodes = a1 ++ y :: (a2 ++ x :: b) := by
      rw [hab, hsplit]; simp
    have hnd' : (a1 ++ y :: (a2 ++ x :: b)).Nodup := hJ' ▸ hJ.nodup
    rw [hJ']
    have hxa1 : x ∉ a1 := nodup_split hnd' x (by simp)
    exact E_mem_of J a1 [] (a2 ++ x :: b) y x hyx (by simp) hxa1

/-! ## 3. Folds of `addEdge` and `addGraph` -/

theorem addEdges_spec (hAdd : AddEdgeSpec) (es : List (Nat × Nat)) : ∀ R : Graph, R.WF →
    (∀ e ∈ es, e.1 ≠ e.2) →
    (es.foldl (fun R e => R.addEdge e.1 e.2) R).WF ∧
    (∀ x, x ∈ (es.foldl (fun R e => R.addEdge e.1 e.2) R).nodes ↔
      x ∈ R.nodes ∨ ∃ e ∈ es, x = e.1 ∨ x = e.2) ∧
    (∀ x y, (es.foldl (fun R e => R.addEdge e.1 e.2) R).Adj x y ↔
      R.Adj x y ∨ ∃ e ∈ es, (x = e.1 ∧ y = e.2 ∨ x = e.2 ∧ y = e.1)) := by
  induction es with
  | nil => intro R hR _; exact ⟨hR, fun x => by simp, fun x y => by simp⟩
  | cons e es ih =>
    intro R hR hne
    obtain ⟨h1, h2, h3⟩ := hAdd R e.1 e.2 hR (hne e List.mem_cons_self)
    obtain ⟨h4, h5, h6⟩ := ih (R.addEdge e.1 e.2) h1
      (fun e' he' => hne e' (List.mem_cons_of_mem e he'))
    refine ⟨?_, fun x => ?_, fun x y => ?_⟩
    · rw [List.foldl_cons]; exact h4
    · rw [List.foldl_cons, h5, h2]
      simp only [List.mem_cons, exists_eq_or_imp, or_assoc]
    · rw [List.foldl_cons, h6, h3]
      simp only [List.mem_cons, exists_eq_or_imp, or_assoc]

theorem edgeList_adj_iff (J : Graph) (hJ : J.WF) (hW : WFBasics) (x y : Nat) :
    (∃ e ∈ J.edgeList, (x = e.1 ∧ y = e.2 ∨ x = e.2 ∧ y = e.1)) ↔ J.Adj x y := by
  constructor
  · rintro ⟨e, he, h | h⟩
    · obtain ⟨hadj, _, _⟩ := edgeList_sound J hJ e.1 e.2 he
      obtain ⟨rfl, rfl⟩ := h
      exact hadj
    · obtain ⟨hadj, _, _⟩ := edgeList_sound J hJ e.1 e.2 he
      obtain ⟨rfl, rfl⟩ := h
      exact hJ.symm _ _ hadj
  · intro h
    rcases edgeList_complete J hJ hW x y h with h1 | h1
    · exact ⟨(x, y), h1, Or.inl ⟨rfl, rfl⟩⟩
    · exact ⟨(y, x), h1, Or.inr ⟨rfl, rfl⟩⟩

theorem addGraph_spec (hAdd : AddEdgeSpec) (hW : WFBasics) (R J : Graph) (hR : R.WF)
    (hJ : J.WF) :
    (addGraph R J).WF ∧ (∀ x, x ∈ (addGraph R J).nodes ↔ x ∈ R.nodes ∨ x ∈ J.nodes) ∧
      (∀ x y, (addGraph R J).Adj x y ↔ R.Adj x y ∨ J.Adj x y) := by
  obtain ⟨h1, h2, h3⟩ := addNodes_spec J.nodes R hR
  have hne : ∀ e ∈ J.edgeList, e.1 ≠ e.2 := by
    intro e he
    exact (hW J hJ e.1 e.2 (edgeList_sound J hJ e.1 e.2 he).1).2.2.2
  obtain ⟨h4, h5, h6⟩ := addEdges_spec hAdd J.edgeList _ h1 hne
  unfold Graph.addGraph
  refine ⟨h4, fun x => ?_, fun x y => ?_⟩
  · rw [h5, h2]
    constructor
    · rintro (h | ⟨e, he, h | h⟩)
      · exact h
      · right; rw [h]; exact (edgeList_sound J hJ e.1 e.2 he).2.1
      · right; rw [h]; exact (edgeList_sound J hJ e.1 e.2 he).2.2
    · rintro (h | h)
      · exact Or.inl (Or.inl h)
      · exact Or.inl (Or.inr h)
  · rw [h6, h3]
    constructor
    · rintro (h | h)
      · exact Or.inl h
      · exact Or.inr ((edgeList_adj_iff J hJ hW x y).1 h)
    · rintro (h | h)
      · exact Or.inl h
      · exact Or.inr ((edgeList_adj_iff J hJ hW x y).2 h)

theorem unionAll_gen (hAdd : AddEdgeSpec) (hW : WFBasics) (gs : List Graph) :
    ∀ R : Graph, R.WF → (∀ J ∈ gs, J.WF) →
    (gs.foldl addGraph R).WF ∧
    (∀ x, x ∈ (gs.foldl addGraph R).nodes ↔ x ∈ R.nodes ∨ ∃ J ∈ gs, x ∈ J.nodes) ∧
    (∀ x y, (gs.foldl addGraph R).Adj x y ↔ R.Adj x y ∨ ∃ J ∈ gs, J.Adj x y) := by
  induction gs with
  | nil => intro R hR _; exact ⟨hR, fun x => by simp, fun x y => by simp⟩
  | cons J gs ih =>
    intro R hR hgs
    obtain ⟨h1, h2, h3⟩ := addGraph_spec hAdd hW R J hR (hgs J List.mem_cons_self)
    obtain ⟨h4, h5, h6⟩ := ih (addGraph R J) h1 (fun J' hJ' => hgs J' (List.mem_cons_of_mem J hJ'))
    refine ⟨?_, fun x => ?_, fun x y => ?_⟩
    · rw [List.foldl_cons]; exact h4
    · rw [List.foldl_cons, h5, h2]
      simp only [List.mem_cons, exists_eq_or_imp, or_assoc]
    · rw [List.foldl_cons, h6, h3]
      simp only [List.mem_cons, exists_eq_or_imp, or_assoc]

theorem empty_wf : (Graph.empty).WF := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  · exact List.nodup_nil
  · intro v; simp [Graph.empty, Graph.mem]
  · intro v; simp [Graph.empty, Graph.nbrs]
  · intro u v h; simp [Graph.empty, Graph.nbrs] at h
  · intro u v h; simp [Graph.empty, Graph.nbrs] at h
  · intro v h; simp [Graph.empty, Graph.nbrs] at h

end G6

/-- G6: `unionAll` satisfies `UnionAllSpec` (from the hypotheses `WFBasics` and
`AddEdgeSpec`, proved in other files). -/
theorem unionAllSpec_of (hWF : WFBasics) (hAdd : AddEdgeSpec) : UnionAllSpec := by
  unfold UnionAllSpec
  intro gs hgs
  obtain ⟨h1, h2, h3⟩ := G6.unionAll_gen hAdd hWF gs Graph.empty G6.empty_wf hgs
  unfold Graph.unionAll
  refine ⟨h1, fun x => ?_, fun x y => ?_⟩
  · rw [h2 x]; simp [Graph.empty]
  · rw [h3 x y]; simp [Graph.empty, Graph.Adj, Graph.nbrs]

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.unionAllSpec_of