CubicPathwidth.Alg.Proofs2.L3Connected

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.G5Components

/-!
# L3: `components` is connected (`ComponentsConnected`, Plan2 §6.1)

Route. For a component found from the start `v` (a `some r` branch), every element is
reachable from `v` (`G5.reachAux_spec`), so two elements are connected through `v`
(symmetry of `Adj`). The `none` branch is unreachable for a well-formed graph:

1. `unseen G s` counts the nodes not in `s`. One pop of `reachAux` with the neighbour fold
   conserves `stack.length + unseen seen`, except that the pop removes one stack entry.
   This is `fold_count` and `unseen_insert`.
2. Hence `reachAux_some`: if `stack.length + unseen seen ≤ fuel`, the search returns.
   The start `[v]`, `{v}` has measure `≤ 1 + numNodes`, so fuel `numNodes + 1` suffices.
3. `go_conn`: every component in the output of `components.go` is connected.

Helpers live in `CubicPathwidth.Alg.L3`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace L3

/-- Number of nodes outside the set `s`. -/
def unseen (G : Graph) (s : Std.HashSet Nat) : Nat :=
  (G.nodes.filter (fun x => !s.contains x)).length

theorem unseen_le (G : Graph) (s : Std.HashSet Nat) : unseen G s ≤ G.numNodes :=
  List.length_filter_le _ _

/-- Inserting a new element of a duplicate-free list lowers the count by one. -/
theorem countIns (y : Nat) (s : Std.HashSet Nat) : ∀ (L : List Nat), L.Nodup → y ∈ L →
    s.contains y = false →
    (L.filter (fun x => !(s.insert y).contains x)).length + 1 =
      (L.filter (fun x => !s.contains x)).length := by
  intro L
  induction L with
  | nil => intro _ hy _; exact absurd hy (by simp)
  | cons a L ih =>
    intro hnd hy hs
    rw [List.nodup_cons] at hnd
    obtain ⟨haL, hndL⟩ := hnd
    by_cases hay : a = y
    · subst hay
      have hfilt : L.filter (fun x => !(s.insert a).contains x) =
          L.filter (fun x => !s.contains x) := by
        apply List.filter_congr
        intro x hx
        have hxa : x ≠ a := fun h => haL (h ▸ hx)
        rw [Std.HashSet.contains_insert, beq_eq_false_iff_ne.2 (Ne.symm hxa), Bool.false_or]
      have ha1 : (!(s.insert a).contains a) = false := by simp [Std.HashSet.contains_insert]
      have ha2 : (!s.contains a) = true := by simp [hs]
      simp only [List.filter_cons, ha1, ha2, hfilt]
      simp
    · have hyL : y ∈ L := by
        rcases List.mem_cons.1 hy with h | h
        · exact absurd h.symm hay
        · exact h
      have hIH := ih hndL hyL hs
      have hpa : (!(s.insert y).contains a) = (!s.contains a) := by
        rw [Std.HashSet.contains_insert, beq_eq_false_iff_ne.2 (Ne.symm hay), Bool.false_or]
      simp only [List.filter_cons, hpa]
      split_ifs with h
      · simp only [List.length_cons]
        omega
      · exact hIH

theorem unseen_insert (G : Graph) (hnd : G.nodes.Nodup) (s : Std.HashSet Nat) (y : Nat)
    (hy : y ∈ G.nodes) (hs : s.contains y = false) :
    unseen G (s.insert y) + 1 = unseen G s :=
  countIns y s G.nodes hnd hy hs

/-- One neighbour fold conserves `stack.length + unseen seen` up to the pushes, which are
exactly the new seen elements. -/
theorem fold_count (G : Graph) (hnd : G.nodes.Nodup) : ∀ (L : List Nat),
    (∀ y ∈ L, y ∈ G.nodes) → ∀ (s : Std.HashSet Nat) (st : List Nat),
    (L.foldl (fun (acc : Std.HashSet Nat × List Nat) y =>
        if acc.1.contains y then acc else (acc.1.insert y, y :: acc.2)) (s, st)).2.length +
      unseen G (L.foldl (fun (acc : Std.HashSet Nat × List Nat) y =>
        if acc.1.contains y then acc else (acc.1.insert y, y :: acc.2)) (s, st)).1 =
      st.length + unseen G s := by
  intro L
  induction L with
  | nil => intro _ s st; simp
  | cons y L ih =>
    intro hL s st
    rw [List.foldl_cons]
    have hyG : y ∈ G.nodes := hL y List.mem_cons_self
    have hL' : ∀ z ∈ L, z ∈ G.nodes := fun z hz => hL z (List.mem_cons_of_mem _ hz)
    by_cases hc : s.contains y = true
    · simp only [hc, ite_true]
      exact ih hL' s st
    · have hc' : s.contains y = false := by simpa using hc
      simp only [hc', Bool.false_eq_true, ite_false]
      rw [ih hL' (s.insert y) (y :: st)]
      have hu := unseen_insert G hnd s y hyG hc'
      simp only [List.length_cons]
      omega

/-- The search returns whenever the fuel covers `stack.length + unseen seen`. -/
theorem reachAux_some (G : Graph) (hG : G.WF) : ∀ (fuel : Nat) (stack : List Nat)
    (seen : Std.HashSet Nat), stack.length + unseen G seen ≤ fuel →
    ∃ r, G.reachAux fuel stack seen = some r := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack seen h
    cases stack with
    | nil => exact ⟨seen, G5.reachAux_nil G 0 seen⟩
    | cons x rest =>
      simp only [List.length_cons] at h
      omega
  | succ n ih =>
    intro stack seen h
    cases stack with
    | nil => exact ⟨seen, G5.reachAux_nil G (n + 1) seen⟩
    | cons x rest =>
      have hL : ∀ y ∈ G.nbrs x, y ∈ G.nodes := fun y hy => hG.nbrs_sub x y hy
      have hf := fold_count G hG.nodup (G.nbrs x) hL seen rest
      simp only [List.length_cons] at h
      rw [Graph.reachAux]
      exact ih _ _ (by omega)

end L3

open L3 in

/-- Every component found by `components.go` from a start `v` has a root connected to all of
its elements (for a well-formed graph; the `none` branch is excluded). -/
theorem go_conn (G : Graph) (hG : G.WF) : ∀ (vs : List Nat) (assigned : Std.HashSet Nat)
    (acc : List (List Nat)),
    (∀ c ∈ acc, ∃ w ∈ c, ∀ x ∈ c, Relation.ReflTransGen G.Adj w x) →
    (∀ x ∈ vs, x ∈ G.nodes) →
    ∀ c ∈ components.go G vs assigned acc, ∃ w ∈ c, ∀ x ∈ c, Relation.ReflTransGen G.Adj w x := by
  intro vs
  induction vs with
  | nil =>
    intro assigned acc hacc _ c hc
    rw [components.go] at hc
    exact hacc c (List.mem_reverse.1 hc)
  | cons v vs ih =>
    intro assigned acc hacc hvs c hc
    rw [components.go] at hc
    have hv : v ∈ G.nodes := hvs v List.mem_cons_self
    have hvs' : ∀ x ∈ vs, x ∈ G.nodes := fun x hx => hvs x (List.mem_cons_of_mem _ hx)
    by_cases hA : assigned.contains v = true
    · simp only [hA, ite_true] at hc
      exact ih assigned acc hacc hvs' c hc
    · rw [if_neg hA] at hc
      split at hc
      · rename_i r hr
        obtain ⟨hr1, hr2, _⟩ :=
          G5.reachAux_spec G v (G.numNodes + 1) [v] _ r (G5.searchInv_init G v) hr
        have hsv : ((∅ : Std.HashSet Nat).insert v).contains v = true :=
          (G5.contains_single v v).2 rfl
        have hvc : v ∈ G.nodes.filter r.contains :=
          List.mem_filter.2 ⟨hv, hr2 v hsv⟩
        have key : ∀ c' ∈ (G.nodes.filter r.contains) :: acc,
            ∃ w ∈ c', ∀ x ∈ c', Relation.ReflTransGen G.Adj w x := by
          intro c' hc'
          rcases List.mem_cons.1 hc' with h | h
          · rw [h]
            exact ⟨v, hvc, fun x hx => hr1 x (List.mem_filter.1 hx).2⟩
          · exact hacc c' h
        exact ih _ _ key hvs' c hc
      · rename_i hr
        exfalso
        have hb : ([v] : List Nat).length + unseen G ((∅ : Std.HashSet Nat).insert v) ≤
            G.numNodes + 1 := by
          have := unseen_le G ((∅ : Std.HashSet Nat).insert v)
          simp only [List.length_singleton]
          omega
        obtain ⟨r, hr'⟩ := reachAux_some G hG (G.numNodes + 1) [v]
          ((∅ : Std.HashSet Nat).insert v) hb
        rw [hr] at hr'
        exact absurd hr' (by simp)

/-- `ComponentsConnected` (Plan2 §6.1): every component of a well-formed graph is connected. -/
theorem componentsConnected : ComponentsConnected := by
  intro G hG c hc x hx y hy
  have hc' : c ∈ components.go G G.nodes ∅ [] := hc
  have hsymm : ∀ u w, G.Adj u w → G.Adj w u := fun u w h => hG.symm u w h
  obtain ⟨v, _, hall⟩ := go_conn G hG G.nodes ∅ [] (by simp) (fun x hx => hx) c hc'
  exact (G5.rtg_symm G hsymm (hall x hx)).trans (hall y hy)

#print axioms CubicPathwidth.Alg.componentsConnected