CubicPathwidth.Alg.Proofs.B2OfSimpleGraph

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

import CubicPathwidth.Alg.Spec

/-!
# B2: `ofSimpleGraph` of a simple graph on `Fin n`

Proves `OfSimpleGraphSpec` (see `Spec.lean`, section 2): the graph `Graph.ofSimpleGraph S`
is well formed, has vertex set `{0, …, n-1}`, gives back `S` under `toSimpleGraph n`, and
has maximum degree at most `3` when `S` is subcubic.

Strategy. `Graph.ofSimpleGraph S` is `Graph.ofAdjLists (List.range n) (…)`, that is the
fold `insert` over the association list `adjPairs S` whose keys are `List.range n` (no
repeats) and whose values are the neighbour lists `nbList S u` (increasing, duplicate free).
Folding `insert` over a list with distinct keys gives `getD k = l` for the value `l` of
the pair with key `k`, and `contains k` iff `k` is a key.
-/

namespace CubicPathwidth.Alg.B2

open CubicPathwidth.Alg

variable {n : ℕ}

/-- The increasing neighbour list of `u` in `S`, as in `Graph.ofSimpleGraph`. -/
def nbList (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) : List Nat :=
  ((List.finRange n).filter fun v => decide (S.Adj u v)).map Fin.val

/-- The association list folded by `Graph.ofAdjLists (List.range n) …`. -/
def adjPairs (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] : List (Nat × List Nat) :=
  (List.range n).zip ((List.finRange n).map (nbList S))

theorem ofSimpleGraph_eq (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] :
    Graph.ofSimpleGraph S =
      ⟨List.range n, (adjPairs S).foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) ∅⟩ :=
  rfl

/-! ### Folding `insert` over an association list -/

theorem fold_getD_none (ps : List (Nat × List Nat)) :
    ∀ (m : Std.HashMap Nat (List Nat)) (k : Nat), k ∉ ps.map Prod.fst →
      (ps.foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) m).getD k [] = m.getD k [] := by
  induction ps with
  | nil => intro m k _; rfl
  | cons p ps ih =>
    intro m k hk
    rcases p with ⟨a, b⟩
    simp only [List.map_cons, List.mem_cons, not_or] at hk
    rw [List.foldl_cons, ih _ k hk.2, Std.HashMap.getD_insert]
    have hne : (a == k) = false := by
      simpa [beq_iff_eq] using (Ne.symm hk.1)
    simp [hne]

theorem fold_getD (ps : List (Nat × List Nat)) :
    ∀ (m : Std.HashMap Nat (List Nat)) (k : Nat) (l : List Nat),
      (ps.map Prod.fst).Nodup → (k, l) ∈ ps →
      (ps.foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) m).getD k [] = l := by
  induction ps with
  | nil => intro m k l _ h; simp at h
  | cons p ps ih =>
    intro m k l hnd hmem
    rcases p with ⟨a, b⟩
    simp only [List.map_cons, List.nodup_cons] at hnd
    rw [List.foldl_cons]
    rcases List.mem_cons.1 hmem with h | h
    · simp only [Prod.mk.injEq] at h
      obtain ⟨rfl, rfl⟩ := h
      rw [fold_getD_none ps _ _ hnd.1]
      simp
    · exact ih _ k l hnd.2 h

theorem fold_contains (ps : List (Nat × List Nat)) :
    ∀ (m : Std.HashMap Nat (List Nat)) (k : Nat),
      (ps.foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) m).contains k = true ↔
        k ∈ ps.map Prod.fst ∨ m.contains k = true := by
  induction ps with
  | nil => intro m k; simp
  | cons p ps ih =>
    intro m k
    rcases p with ⟨a, b⟩
    rw [List.foldl_cons, ih, Std.HashMap.contains_insert]
    simp only [List.map_cons, List.mem_cons, Bool.or_eq_true, beq_iff_eq]
    tauto

/-! ### The association list of `ofSimpleGraph` -/

theorem adjPairs_fst (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] :
    (adjPairs S).map Prod.fst = List.range n := by
  unfold adjPairs
  rw [List.map_fst_zip]
  simp

theorem mem_adjPairs (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    (u.val, nbList S u) ∈ adjPairs S := by
  unfold adjPairs
  rw [List.mem_iff_getElem]
  refine ⟨u.val, by simp [u.isLt], ?_⟩
  simp

/-! ### Neighbour lists -/

theorem mem_nbList {w : Nat} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    w ∈ nbList S u ↔ ∃ x : Fin n, x.val = w ∧ S.Adj u x := by
  unfold nbList
  simp only [List.mem_map, List.mem_filter, List.mem_finRange, decide_eq_true_eq, true_and]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, rfl, hx⟩
  · rintro ⟨x, rfl, hx⟩
    exact ⟨x, hx, rfl⟩

theorem nbList_lt {w : Nat} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n)
    (h : w ∈ nbList S u) : w < n := by
  obtain ⟨x, rfl, -⟩ := (mem_nbList S u).1 h
  exact x.isLt

theorem nbrs_eq (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    (Graph.ofSimpleGraph S).nbrs u.val = nbList S u := by
  rw [ofSimpleGraph_eq]
  unfold Graph.nbrs
  exact fold_getD _ _ _ _ (by rw [adjPairs_fst]; exact List.nodup_range) (mem_adjPairs S u)

theorem nbrs_ge (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (k : Nat) (hk : n ≤ k) :
    (Graph.ofSimpleGraph S).nbrs k = [] := by
  rw [ofSimpleGraph_eq]
  unfold Graph.nbrs
  show ((adjPairs S).foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) ∅).getD k [] = []
  rw [fold_getD_none _ _ _ (by rw [adjPairs_fst, List.mem_range]; omega), Std.HashMap.getD_empty]

theorem mem_nbrs_iff (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u v : Fin n) :
    v.val ∈ (Graph.ofSimpleGraph S).nbrs u.val ↔ S.Adj u v := by
  rw [nbrs_eq, mem_nbList]
  constructor
  · rintro ⟨x, hx, hadj⟩
    have : x = v := Fin.ext hx
    subst this
    exact hadj
  · intro h
    exact ⟨v, rfl, h⟩

theorem subU (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u v : Nat)
    (hv : v ∈ (Graph.ofSimpleGraph S).nbrs u) : u < n ∧ v < n := by
  by_cases hu : u < n
  · refine ⟨hu, ?_⟩
    have e : (Graph.ofSimpleGraph S).nbrs u = nbList S ⟨u, hu⟩ := nbrs_eq S ⟨u, hu⟩
    rw [e] at hv
    exact nbList_lt S _ hv
  · rw [nbrs_ge S u (by omega)] at hv
    simp at hv

theorem nodes_eq (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] :
    (Graph.ofSimpleGraph S).nodes = List.range n :=
  rfl

theorem mem_iff (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (k : Nat) :
    (Graph.ofSimpleGraph S).mem k = true ↔ k < n := by
  rw [ofSimpleGraph_eq]
  unfold Graph.mem
  show ((adjPairs S).foldl (fun (a : Std.HashMap Nat (List Nat)) (p : Nat × List Nat) => a.insert p.1 p.2) ∅).contains k = true ↔ k < n
  rw [fold_contains, adjPairs_fst]
  simp

/-! ### Well-formedness -/

theorem wf (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] : (Graph.ofSimpleGraph S).WF := by
  have nd : ∀ u, ((Graph.ofSimpleGraph S).nbrs u).Nodup := by
    intro u
    by_cases hu : u < n
    · have e : (Graph.ofSimpleGraph S).nbrs u = nbList S ⟨u, hu⟩ := nbrs_eq S ⟨u, hu⟩
      rw [e]
      unfold nbList
      exact ((List.nodup_finRange n).filter _).map Fin.val_injective
    · rw [nbrs_ge S u (by omega)]
      exact List.nodup_nil
  refine ⟨List.nodup_range, fun v => ?_, nd, fun u v hv => ?_, fun u v hv => ?_, fun v hv => ?_⟩
  · rw [mem_iff S v]
    show v < n ↔ v ∈ List.range n
    simp
  · exact List.mem_range.2 (subU S u v hv).2
  · obtain ⟨hu, hv'⟩ := subU S u v hv
    have h := (mem_nbrs_iff S ⟨u, hu⟩ ⟨v, hv'⟩).1 hv
    exact (mem_nbrs_iff S ⟨v, hv'⟩ ⟨u, hu⟩).2 (S.adj_symm h)
  · obtain ⟨hv', -⟩ := subU S v v hv
    exact S.irrefl ((mem_nbrs_iff S ⟨v, hv'⟩ ⟨v, hv'⟩).1 hv)

/-! ### Bridge to `SimpleGraph` and degrees -/

theorem toSimpleGraph_eq (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] :
    (Graph.ofSimpleGraph S).toSimpleGraph n = S := by
  ext u v
  unfold Graph.toSimpleGraph
  rw [SimpleGraph.fromRel_adj]
  constructor
  · rintro ⟨-, h | h⟩
    · exact (mem_nbrs_iff S u v).1 h
    · exact S.adj_symm ((mem_nbrs_iff S v u).1 h)
  · intro h
    exact ⟨S.ne_of_adj h, Or.inl ((mem_nbrs_iff S u v).2 h)⟩

theorem card_filter_eq_length (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    (Finset.univ.filter (S.Adj u)).card = (nbList S u).length := by
  unfold nbList
  rw [List.length_map, Finset.card_def, Finset.filter_val, Fin.univ_def]
  simp [Multiset.filter_coe, Multiset.coe_card]

theorem degree_eq_length (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    S.degree u = (nbList S u).length := by
  rw [← SimpleGraph.card_neighborFinset_eq_degree, ← card_filter_eq_length]
  congr 1
  ext x
  simp [SimpleGraph.mem_neighborFinset]

theorem maxDegLE (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (hS : CubicPathwidth.IsSubcubic S) :
    (Graph.ofSimpleGraph S).MaxDegLE 3 := by
  unfold CubicPathwidth.IsSubcubic at hS
  intro v hv
  have hvn : v < n := by
    have : v ∈ List.range n := hv
    exact List.mem_range.1 this
  have e : (Graph.ofSimpleGraph S).nbrs v = nbList S ⟨v, hvn⟩ := nbrs_eq S ⟨v, hvn⟩
  have h3 := hS ⟨v, hvn⟩
  unfold Graph.degree
  rw [e]
  rw [← degree_eq_length]
  convert h3

end CubicPathwidth.Alg.B2

namespace CubicPathwidth.Alg

open B2

/-- `ofSimpleGraph` is well formed, has vertex set `{0, …, n-1}`, gives back `S`, and keeps
the degree bound of `IsSubcubic`. -/
theorem ofSimpleGraphSpec : OfSimpleGraphSpec := by
  intro n S _inst
  refine ⟨B2.wf S, fun v => ?_, B2.toSimpleGraph_eq S, fun hS => B2.maxDegLE S hS⟩
  rw [B2.nodes_eq]
  exact List.mem_range

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.ofSimpleGraphSpec