CubicPathwidth.Alg.Proofs.G2AddEdge

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

import CubicPathwidth.Alg.Spec

/-!
# G2: `addEdge` preserves well-formedness and adjacency (task G2)

Proves `AddEdgeSpec` for `Graph.addEdge`. Helpers live in `CubicPathwidth.Alg.G2`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace G2

/-- `addNode` does not change any neighbour list (a fresh node has list `[]`). -/
theorem nbrs_addNode (G : Graph) (w x : Nat) : (G.addNode w).nbrs x = G.nbrs x := by
  unfold addNode
  split
  · rfl
  · rename_i hw
    have hw' : G.adj.contains w = false := by simpa [Graph.mem] using hw
    unfold Graph.nbrs
    rw [Std.HashMap.getD_insert]
    by_cases hx : w = x
    · subst hx
      simp [Std.HashMap.getD_eq_fallback_of_contains_eq_false hw']
    · have h2 : (w == x) = false := by simpa using hx
      simp [h2]

theorem mem_addNode_iff (G : Graph) (w x : Nat) :
    (G.addNode w).mem x = true ↔ G.mem x = true ∨ x = w := by
  unfold addNode
  split
  · rename_i hw
    constructor
    · intro h; exact Or.inl h
    · rintro (h | h)
      · exact h
      · subst h; exact hw
  · simp only [Graph.mem, Std.HashMap.contains_insert, Bool.or_eq_true, beq_iff_eq]
    constructor
    · rintro (h | h)
      · exact Or.inr h.symm
      · exact Or.inl h
    · rintro (h | h)
      · exact Or.inr h
      · exact Or.inl h.symm

theorem nodes_addNode_iff (G : Graph) (hG : G.WF) (w x : Nat) :
    x ∈ (G.addNode w).nodes ↔ x ∈ G.nodes ∨ x = w := by
  unfold addNode
  split
  · rename_i hw
    have hwn : w ∈ G.nodes := (hG.mem_iff w).1 hw
    constructor
    · exact Or.inl
    · rintro (h | h)
      · exact h
      · subst h; exact hwn
  · simp

theorem nodup_addNode (G : Graph) (hG : G.WF) (w : Nat) : (G.addNode w).nodes.Nodup := by
  unfold addNode
  split
  · exact hG.nodup
  · rename_i hw
    have hw' : w ∉ G.nodes := fun h => by
      have := (hG.mem_iff w).2 h
      simp_all
    show (G.nodes ++ [w]).Nodup
    rw [List.nodup_append]
    refine ⟨hG.nodup, by simp, ?_⟩
    intro a ha b hb
    simp only [List.mem_singleton] at hb
    subst hb
    intro h
    exact hw' (h ▸ ha)

theorem wf_addNode (G : Graph) (hG : G.WF) (w : Nat) : (G.addNode w).WF := by
  refine ⟨nodup_addNode G hG w, ?_, ?_, ?_, ?_, ?_⟩
  · intro x
    rw [mem_addNode_iff, nodes_addNode_iff G hG, hG.mem_iff x]
  · intro x
    rw [nbrs_addNode]
    exact hG.nbrs_nodup x
  · intro u v h
    rw [nbrs_addNode] at h
    rw [nodes_addNode_iff G hG]
    exact Or.inl (hG.nbrs_sub u v h)
  · intro u v h
    rw [nbrs_addNode] at h ⊢
    exact hG.symm u v h
  · intro v
    rw [nbrs_addNode]
    exact hG.loopless v

/-- `appendNbr` leaves the node list unchanged. -/
theorem nodes_appendNbr (G : Graph) (u v : Nat) : (G.appendNbr u v).nodes = G.nodes := by
  dsimp only [appendNbr]
  split <;> rfl

/-- `appendNbr` changes only the list of `u`, by appending `v` if absent. -/
theorem nbrs_appendNbr (G : Graph) (u v x : Nat) :
    (G.appendNbr u v).nbrs x =
      if x = u then (if v ∈ G.nbrs u then G.nbrs u else G.nbrs u ++ [v]) else G.nbrs x := by
  dsimp only [appendNbr]
  by_cases hc : (G.nbrs u).contains v = true
  · have hm : v ∈ G.nbrs u := by simpa using hc
    simp only [hc, ite_true, hm]
    by_cases hx : x = u
    · simp [hx]
    · simp [hx]
  · have hc' : (G.nbrs u).contains v = false := by simpa using hc
    have hm : v ∉ G.nbrs u := fun h => hc (by simpa using h)
    simp only [hc', Bool.false_eq_true, ite_false, hm]
    unfold Graph.nbrs
    by_cases hx : x = u
    · subst hx
      simp [Std.HashMap.getD_insert]
    · have h2 : (u == x) = false := by simpa using (Ne.symm hx)
      simp [Std.HashMap.getD_insert, h2, hx]

/-- Membership in a neighbour list after appending `a` if absent. -/
theorem mem_ins (L : List Nat) (a y : Nat) :
    y ∈ (if a ∈ L then L else L ++ [a]) ↔ (y ∈ L ∨ y = a) := by
  split_ifs with h
  · constructor
    · exact Or.inl
    · rintro (h' | rfl)
      · exact h'
      · exact h
  · simp

theorem nodup_ins (L : List Nat) (a : Nat) (h : L.Nodup) :
    (if a ∈ L then L else L ++ [a]).Nodup := by
  split_ifs with ha
  · exact h
  · rw [List.nodup_append]
    refine ⟨h, by simp, ?_⟩
    intro x hx y hy
    simp only [List.mem_singleton] at hy
    subst hy
    intro e
    exact ha (e ▸ hx)

/-- The neighbour lists of `addEdge u v` for distinct `u v`. -/
theorem nbrs_addEdge (G : Graph) (u v : Nat) (huv : u ≠ v) (x : Nat) :
    (G.addEdge u v).nbrs x =
      if x = u then (if v ∈ G.nbrs u then G.nbrs u else G.nbrs u ++ [v])
      else if x = v then (if u ∈ G.nbrs v then G.nbrs v else G.nbrs v ++ [u])
      else G.nbrs x := by
  have huv' : v ≠ u := fun h => huv h.symm
  unfold addEdge
  simp only [nbrs_appendNbr, nbrs_addNode]
  by_cases hxu : x = u
  · simp [hxu, huv, huv']
  · by_cases hxv : x = v
    · simp [hxv, hxu, huv, huv']
    · simp [hxu, hxv]

theorem adj_addEdge (G : Graph) (u v : Nat) (huv : u ≠ v) (x y : Nat) :
    (G.addEdge u v).Adj x y ↔ G.Adj x y ∨ (x = u ∧ y = v) ∨ (x = v ∧ y = u) := by
  unfold Graph.Adj
  rw [nbrs_addEdge G u v huv x]
  by_cases hxu : x = u
  · rw [if_pos hxu, mem_ins]
    simp [hxu, huv]
  · by_cases hxv : x = v
    · rw [if_neg hxu, if_pos hxv, mem_ins]
      simp [hxv, huv.symm]
    · rw [if_neg hxu, if_neg hxv]
      simp [hxu, hxv]

theorem nodes_addEdge_iff (G : Graph) (hG : G.WF) (u v : Nat) (x : Nat) :
    x ∈ (G.addEdge u v).nodes ↔ x ∈ G.nodes ∨ x = u ∨ x = v := by
  unfold addEdge
  rw [nodes_appendNbr, nodes_appendNbr, nodes_addNode_iff _ (wf_addNode G hG u) v,
    nodes_addNode_iff G hG u, or_assoc]

theorem mem_appendNbr (G : Graph) (u v x : Nat) (hu : G.mem u = true) :
    (G.appendNbr u v).mem x = G.mem x := by
  dsimp only [appendNbr]
  split
  · rfl
  · simp only [Graph.mem, Std.HashMap.contains_insert]
    by_cases hx : u = x
    · subst hx; simp [Graph.mem] at hu ⊢; simp [hu]
    · have h2 : (u == x) = false := by simpa using hx
      simp [h2]

theorem mem_addEdge_iff (G : Graph) (u v x : Nat) :
    (G.addEdge u v).mem x = true ↔ G.mem x = true ∨ x = u ∨ x = v := by
  have h1 : (G.addNode u).mem u = true := (mem_addNode_iff _ _ _).2 (Or.inr rfl)
  have h2 : ((G.addNode u).addNode v).mem u = true :=
    (mem_addNode_iff _ _ _).2 (Or.inl h1)
  have h3 : ((G.addNode u).addNode v).mem v = true := (mem_addNode_iff _ _ _).2 (Or.inr rfl)
  have h4 : ((G.addNode u).addNode v |>.appendNbr u v).mem v = true := by
    rw [mem_appendNbr _ _ _ _ h2]; exact h3
  unfold addEdge
  rw [mem_appendNbr _ _ _ _ h4, mem_appendNbr _ _ _ _ h2, mem_addNode_iff, mem_addNode_iff,
    or_assoc]

theorem addEdge_WF (G : Graph) (hG : G.WF) (u v : Nat) (huv : u ≠ v) :
    (G.addEdge u v).WF := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  · unfold addEdge
    simp only [nodes_appendNbr]
    exact nodup_addNode _ (wf_addNode G hG u) v
  · intro x
    rw [mem_addEdge_iff, nodes_addEdge_iff G hG u v x, hG.mem_iff x]
  · intro x
    rw [nbrs_addEdge G u v huv x]
    by_cases h1 : x = u
    · rw [if_pos h1]; exact nodup_ins _ _ (hG.nbrs_nodup u)
    · rw [if_neg h1]
      by_cases h2 : x = v
      · rw [if_pos h2]; exact nodup_ins _ _ (hG.nbrs_nodup v)
      · rw [if_neg h2]; exact hG.nbrs_nodup x
  · intro x y h
    change (G.addEdge u v).Adj x y at h
    rw [adj_addEdge G u v huv] at h
    rw [nodes_addEdge_iff G hG u v y]
    rcases h with h | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
    · exact Or.inl (hG.nbrs_sub x y h)
    · exact Or.inr (Or.inr rfl)
    · exact Or.inr (Or.inl rfl)
  · intro x y h
    change (G.addEdge u v).Adj x y at h
    show (G.addEdge u v).Adj y x
    rw [adj_addEdge G u v huv] at h ⊢
    rcases h with h | ⟨h1, h2⟩ | ⟨h1, h2⟩
    · exact Or.inl (hG.symm x y h)
    · exact Or.inr (Or.inr ⟨h2, h1⟩)
    · exact Or.inr (Or.inl ⟨h2, h1⟩)
  · intro x h
    change (G.addEdge u v).Adj x x at h
    rw [adj_addEdge G u v huv] at h
    rcases h with h | ⟨h1, h2⟩ | ⟨h1, h2⟩
    · exact hG.loopless x h
    · exact huv (h1.symm.trans h2)
    · exact huv (h2.symm.trans h1)

end G2

/-- `addEdge` of two distinct vertices (Spec `AddEdgeSpec`). -/
theorem addEdgeSpec : AddEdgeSpec := by
  intro G u v hG huv
  exact ⟨G2.addEdge_WF G hG u v huv,
    fun x => G2.nodes_addEdge_iff G hG u v x,
    fun x y => G2.adj_addEdge G u v huv x y⟩

#print axioms CubicPathwidth.Alg.addEdgeSpec

end CubicPathwidth.Alg