CubicPathwidth.Alg.Proofs.G5Components

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

import CubicPathwidth.Alg.Spec

/-!
# G5: `components` satisfies `ComponentsSpec`

Proof of `ComponentsSpec` (Spec.lean, section 3) for `Graph.components`.
Helpers live in `CubicPathwidth.Alg.G5`.

1. `fold_spec`: the neighbour fold of `reachAux`, for an arbitrary initial accumulator.
2. `reachAux_spec`: invariant of the depth-first search, giving a reachable and closed
   result.
3. `go_good`: invariant of `components.go` (disjoint closed nonempty parts, covering
   the processed nodes), including the fallback branch.
-/

namespace CubicPathwidth.Alg

open Graph

namespace G5

/-- The neighbour-fold step of `Graph.reachAux` (same function as the lambda there). -/
abbrev stepF (acc : Std.HashSet Nat × List Nat) (y : Nat) : Std.HashSet Nat × List Nat :=
  if acc.1.contains y then acc else (acc.1.insert y, y :: acc.2)

/-- Behaviour of the neighbour fold, for an arbitrary initial accumulator. -/
theorem fold_spec (L : List Nat) : ∀ (acc : Std.HashSet Nat × List Nat),
    (∀ y ∈ L, (L.foldl stepF acc).1.contains y = true) ∧
    (∀ z, acc.1.contains z = true → (L.foldl stepF acc).1.contains z = true) ∧
    (∀ z ∈ acc.2, z ∈ (L.foldl stepF acc).2) ∧
    (∀ z, (L.foldl stepF acc).1.contains z = true →
        acc.1.contains z = true ∨ (z ∈ L ∧ z ∈ (L.foldl stepF acc).2)) ∧
    (∀ z ∈ (L.foldl stepF acc).2, z ∈ acc.2 ∨ z ∈ L) := by
  induction L with
  | nil =>
    intro acc
    simp only [List.foldl_nil]
    exact ⟨fun y hy => absurd hy (by simp), fun _ hz => hz, fun _ hz => hz,
      fun _ hz => Or.inl hz, fun _ hz => Or.inl hz⟩
  | cons y L ih =>
    intro acc
    rw [List.foldl_cons]
    by_cases hc : acc.1.contains y = true
    · have hstep : stepF acc y = acc := by simp [stepF, hc]
      rw [hstep]
      obtain ⟨h1, h2, h3, h4, h5⟩ := ih acc
      refine ⟨?_, h2, h3, ?_, ?_⟩
      · intro y' hy'
        rcases List.mem_cons.1 hy' with h | h
        · subst h; exact h2 _ hc
        · exact h1 y' h
      · intro z hz
        rcases h4 z hz with h | ⟨hzL, hzr⟩
        · exact Or.inl h
        · exact Or.inr ⟨List.mem_cons_of_mem _ hzL, hzr⟩
      · intro z hz
        rcases h5 z hz with h | h
        · exact Or.inl h
        · exact Or.inr (List.mem_cons_of_mem _ h)
    · have hc' : acc.1.contains y = false := by simpa using hc
      have hstep : stepF acc y = (acc.1.insert y, y :: acc.2) := by simp [stepF, hc']
      rw [hstep]
      obtain ⟨h1, h2, h3, h4, h5⟩ := ih (acc.1.insert y, y :: acc.2)
      refine ⟨?_, ?_, ?_, ?_, ?_⟩
      · intro y' hy'
        rcases List.mem_cons.1 hy' with h | h
        · subst h; exact h2 _ (by simp)
        · exact h1 y' h
      · intro z hz
        exact h2 z (by simp [hz])
      · intro z hz
        exact h3 z (List.mem_cons_of_mem _ hz)
      · intro z hz
        rcases h4 z hz with h | ⟨hzL, hzr⟩
        · simp only [Std.HashSet.contains_insert, Bool.or_eq_true, beq_iff_eq] at h
          rcases h with h | h
          · subst h
            exact Or.inr ⟨List.mem_cons_self, h3 _ List.mem_cons_self⟩
          · exact Or.inl h
        · exact Or.inr ⟨List.mem_cons_of_mem _ hzL, hzr⟩
      · intro z hz
        rcases h5 z hz with h | h
        · rcases List.mem_cons.1 h with h | h
          · subst h; exact Or.inr List.mem_cons_self
          · exact Or.inl h
        · exact Or.inr (List.mem_cons_of_mem _ h)

/-- Invariant of the depth-first search `reachAux` from the start `s`: every seen vertex
is reachable from `s`; every stacked vertex is seen; every seen vertex is on the stack or
has all its neighbours seen. -/
def SearchInv (G : Graph) (s : Nat) (stack : List Nat) (seen : Std.HashSet Nat) : Prop :=
  (∀ z, seen.contains z = true → Relation.ReflTransGen G.Adj s z) ∧
  (∀ z ∈ stack, seen.contains z = true) ∧
  (∀ z, seen.contains z = true → z ∈ stack ∨ ∀ y, G.Adj z y → seen.contains y = true)

/-- One pop of the search preserves the invariant. -/
theorem searchInv_step (G : Graph) (s x : Nat) (rest : List Nat) (seen : Std.HashSet Nat)
    (hInv : SearchInv G s (x :: rest) seen) :
    SearchInv G s ((G.nbrs x).foldl stepF (seen, rest)).2
      ((G.nbrs x).foldl stepF (seen, rest)).1 := by
  obtain ⟨h1, h2, h3⟩ := hInv
  obtain ⟨f1, f2, f3, f4, f5⟩ := fold_spec (G.nbrs x) (seen, rest)
  have hx : seen.contains x = true := h2 x List.mem_cons_self
  refine ⟨?_, ?_, ?_⟩
  · intro z hz
    rcases f4 z hz with h | ⟨hzL, _⟩
    · exact h1 z h
    · exact Relation.ReflTransGen.tail (h1 x hx) hzL
  · intro z hz
    rcases f5 z hz with h | h
    · exact f2 z (h2 z (List.mem_cons_of_mem _ h))
    · exact f1 z h
  · intro z hz
    rcases f4 z hz with h | ⟨_, hzr⟩
    · rcases h3 z h with h' | h'
      · rcases List.mem_cons.1 h' with h'' | h''
        · subst h''
          exact Or.inr (fun y hy => f1 y hy)
        · exact Or.inl (f3 z h'')
      · exact Or.inr (fun y hy => f2 y (h' y hy))
    · exact Or.inl hzr

theorem contains_single (s z : Nat) :
    ((∅ : Std.HashSet Nat).insert s).contains z = true ↔ s = z := by
  rw [Std.HashSet.contains_insert, Std.HashSet.contains_empty, Bool.or_false, beq_iff_eq]

theorem searchInv_init (G : Graph) (s : Nat) :
    SearchInv G s [s] ((∅ : Std.HashSet Nat).insert s) := by
  refine ⟨?_, ?_, ?_⟩
  · intro z hz
    rw [contains_single] at hz
    subst hz
    exact Relation.ReflTransGen.refl
  · intro z hz
    rw [List.mem_singleton] at hz
    subst hz
    exact (contains_single _ _).2 rfl
  · intro z hz
    rw [contains_single] at hz
    subst hz
    exact Or.inl List.mem_cons_self

theorem reachAux_nil (G : Graph) (fuel : Nat) (seen : Std.HashSet Nat) :
    G.reachAux fuel [] seen = some seen := by
  cases fuel <;> rfl

/-- Correctness of `reachAux`: a returned set consists of reachable vertices, contains the
initial seen set, and is closed under adjacency. -/
theorem reachAux_spec (G : Graph) (s : Nat) (fuel : Nat) :
    ∀ (stack : List Nat) (seen r : Std.HashSet Nat), SearchInv G s stack seen →
      G.reachAux fuel stack seen = some r →
      (∀ z, r.contains z = true → Relation.ReflTransGen G.Adj s z) ∧
      (∀ z, seen.contains z = true → r.contains z = true) ∧
      (∀ z, r.contains z = true → ∀ y, G.Adj z y → r.contains y = true) := by
  induction fuel with
  | zero =>
    intro stack seen r hInv hr
    cases stack with
    | nil =>
      rw [reachAux_nil] at hr
      cases hr
      refine ⟨hInv.1, fun _ hz => hz, fun z hz y hy => ?_⟩
      rcases hInv.2.2 z hz with h | h
      · exact absurd h (by simp)
      · exact h y hy
    | cons x rest =>
      rw [reachAux] at hr
      cases hr
  | succ n ih =>
    intro stack seen r hInv hr
    cases stack with
    | nil =>
      rw [reachAux_nil] at hr
      cases hr
      refine ⟨hInv.1, fun _ hz => hz, fun z hz y hy => ?_⟩
      rcases hInv.2.2 z hz with h | h
      · exact absurd h (by simp)
      · exact h y hy
    | cons x rest =>
      rw [reachAux] at hr
      have hI := searchInv_step G s x rest seen hInv
      obtain ⟨f1, f2, f3, f4, f5⟩ := fold_spec (G.nbrs x) (seen, rest)
      obtain ⟨i1, i2, i3⟩ := ih _ _ r hI hr
      refine ⟨i1, fun z hz => i2 z (f2 z hz), i3⟩

/-! ## Part 2: closure, the accumulator invariant of `components.go`, the result -/

/-- `c` is closed under adjacency. -/
def Closed (G : Graph) (c : List Nat) : Prop := ∀ x ∈ c, ∀ y, G.Adj x y → y ∈ c

theorem closed_rtg (G : Graph) (c : List Nat) (hc : Closed G c) {a b : Nat} (ha : a ∈ c)
    (h : Relation.ReflTransGen G.Adj a b) : b ∈ c := by
  induction h with
  | refl => exact ha
  | tail _ hbc ih => exact hc _ ih _ hbc

theorem rtg_symm (G : Graph) (hs : ∀ u v, G.Adj u v → G.Adj v u) {a b : Nat}
    (h : Relation.ReflTransGen G.Adj a b) : Relation.ReflTransGen G.Adj b a := by
  induction h with
  | refl => exact Relation.ReflTransGen.refl
  | tail _ hbc ih => exact Relation.ReflTransGen.head (hs _ _ hbc) ih

theorem foldInsert_contains (l : List Nat) : ∀ (s : Std.HashSet Nat) (x : Nat),
    (l.foldl (fun s y => s.insert y) s).contains x = true ↔ x ∈ l ∨ s.contains x = true := by
  induction l with
  | nil => intro s x; simp
  | cons y l ih =>
    intro s x
    rw [List.foldl_cons, ih, Std.HashSet.contains_insert, Bool.or_eq_true, beq_iff_eq,
      List.mem_cons]
    constructor
    · rintro (h | h | h)
      · exact Or.inl (Or.inr h)
      · exact Or.inl (Or.inl h.symm)
      · exact Or.inr h
    · rintro ((h | h) | h)
      · exact Or.inr (Or.inl h.symm)
      · exact Or.inl h
      · exact Or.inr (Or.inr h)

/-- The shape of the output of `components`: disjoint, nonempty, closed parts; the parts
together contain exactly the nodes (flatten nodup). -/
def Good (G : Graph) (res : List (List Nat)) : Prop :=
  (∀ c ∈ res, c ≠ [] ∧ (∀ x ∈ c, x ∈ G.nodes) ∧ Closed G c) ∧
  res.flatten.Nodup ∧ (∀ x, x ∈ res.flatten ↔ x ∈ G.nodes)

theorem good_reverse (G : Graph) {res : List (List Nat)} (h : Good G res) :
    Good G res.reverse := by
  obtain ⟨h1, h2, h3⟩ := h
  have hp := (List.reverse_perm res).flatten
  exact ⟨fun c hc => h1 c (List.mem_reverse.1 hc), hp.nodup_iff.2 h2,
    fun x => by rw [hp.mem_iff]; exact h3 x⟩

/-- Invariant of `components.go G vs assigned acc` (with `acc` the components found so far,
in reverse order). -/
structure GoInv (G : Graph) (vs : List Nat) (assigned : Std.HashSet Nat)
    (acc : List (List Nat)) : Prop where
  comp_ne : ∀ c ∈ acc, c ≠ []
  comp_sub : ∀ c ∈ acc, ∀ x ∈ c, x ∈ G.nodes
  comp_closed : ∀ c ∈ acc, Closed G c
  flat_nodup : acc.flatten.Nodup
  assigned_iff : ∀ x, assigned.contains x = true ↔ x ∈ acc.flatten
  cover : ∀ x ∈ G.nodes, x ∉ vs → x ∈ acc.flatten
  vs_sub : ∀ x ∈ vs, x ∈ G.nodes

theorem final_good (G : Graph) {acc : List (List Nat)} (hI : GoInv G [] assigned acc) :
    Good G acc := by
  refine ⟨fun c hc => ⟨hI.comp_ne c hc, hI.comp_sub c hc, hI.comp_closed c hc⟩,
    hI.flat_nodup, fun x => ⟨fun h => ?_, fun h => ?_⟩⟩
  · obtain ⟨c, hc, hxc⟩ := List.mem_flatten.1 h
    exact hI.comp_sub c hc x hxc
  · exact hI.cover x h (List.not_mem_nil)

theorem fallback_good (G : Graph) (hG : G.WF) (assigned : Std.HashSet Nat)
    (acc : List (List Nat)) (vs : List Nat) (v : Nat)
    (hI : GoInv G (v :: vs) assigned acc) (hv : v ∈ G.nodes)
    (hA : ¬ assigned.contains v = true) :
    Good G ((G.nodes.filter (fun x => !assigned.contains x)) :: acc).reverse := by
  have hmem : ∀ x, x ∈ G.nodes.filter (fun x => !assigned.contains x) ↔
      x ∈ G.nodes ∧ assigned.contains x = false := by
    intro x
    rw [List.mem_filter]
    simp
  have hsymm : ∀ u w, G.Adj u w → G.Adj w u := fun u w h => hG.symm u w h
  have hclosed : Closed G (G.nodes.filter (fun x => !assigned.contains x)) := by
    intro x hx y hxy
    rw [hmem] at hx ⊢
    refine ⟨hG.nbrs_sub x y hxy, ?_⟩
    by_cases hy : assigned.contains y = true
    · exfalso
      have hyf := (hI.assigned_iff y).1 hy
      obtain ⟨c, hc, hyc⟩ := List.mem_flatten.1 hyf
      have hxc : x ∈ c := hI.comp_closed c hc y hyc x (hsymm x y hxy)
      have hxa : assigned.contains x = true :=
        (hI.assigned_iff x).2 (List.mem_flatten.2 ⟨c, hc, hxc⟩)
      rw [hx.2] at hxa
      exact Bool.false_ne_true hxa
    · exact Bool.eq_false_iff.2 hy
  have hG' : Good G ((G.nodes.filter (fun x => !assigned.contains x)) :: acc) := by
    refine ⟨?_, ?_, ?_⟩
    · intro c hc
      rcases List.mem_cons.1 hc with h | h
      · subst h
        refine ⟨List.ne_nil_of_mem ((hmem v).2 ⟨hv, by simpa using hA⟩), ?_, hclosed⟩
        intro x hx
        exact ((hmem x).1 hx).1
      · exact ⟨hI.comp_ne c h, hI.comp_sub c h, hI.comp_closed c h⟩
    · rw [List.flatten_cons, List.nodup_append]
      refine ⟨hG.nodup.filter _, hI.flat_nodup, ?_⟩
      intro a ha b hb hab
      subst hab
      have hain := (hI.assigned_iff a).2 hb
      rw [((hmem a).1 ha).2] at hain
      exact Bool.false_ne_true hain
    · intro x
      rw [List.flatten_cons, List.mem_append]
      constructor
      · rintro (h | h)
        · exact ((hmem x).1 h).1
        · obtain ⟨c, hc, hxc⟩ := List.mem_flatten.1 h
          exact hI.comp_sub c hc x hxc
      · intro hx
        by_cases hxa : assigned.contains x = true
        · exact Or.inr ((hI.assigned_iff x).1 hxa)
        · exact Or.inl ((hmem x).2 ⟨hx, Bool.eq_false_iff.2 hxa⟩)
  exact good_reverse G hG'

/-- Invariant of `components.go` and its result: for every state satisfying `GoInv`, the
output is `Good`. Induction on the remaining nodes `vs`. -/
theorem go_good (G : Graph) (hG : G.WF) :
    ∀ (vs : List Nat) (assigned : Std.HashSet Nat) (acc : List (List Nat)),
      GoInv G vs assigned acc → Good G (components.go G vs assigned acc) := by
  intro vs
  induction vs with
  | nil =>
    intro assigned acc hI
    rw [components.go]
    exact good_reverse G (final_good G hI)
  | cons v vs ih =>
    intro assigned acc hI
    have hv : v ∈ G.nodes := hI.vs_sub v List.mem_cons_self
    by_cases hA : assigned.contains v = true
    · rw [components.go, ite_eq_left hA]
      apply ih
      refine GoInv.mk hI.comp_ne hI.comp_sub hI.comp_closed hI.flat_nodup hI.assigned_iff ?_ ?_
      · intro x hx hxn
        by_cases hxv : x = v
        · rw [hxv]
          exact (hI.assigned_iff v).1 hA
        · exact hI.cover x hx (fun h => by
            rcases List.mem_cons.1 h with h' | h'
            · exact hxv h'
            · exact hxn h')
      · intro x hx
        exact hI.vs_sub x (List.mem_cons_of_mem _ hx)
    · rw [components.go, ite_eq_right hA]
      split
      · rename_i r hr
        obtain ⟨hr1, hr2, hr3⟩ :=
          reachAux_spec G v (G.numNodes + 1) [v] _ r (searchInv_init G v) hr
        have hsv : ((∅ : Std.HashSet Nat).insert v).contains v = true :=
          (contains_single v v).2 rfl
        have hmemc : ∀ x, x ∈ G.nodes.filter r.contains ↔
            x ∈ G.nodes ∧ r.contains x = true := by
          intro x
          rw [List.mem_filter]
        have hvc : v ∈ G.nodes.filter r.contains := (hmemc v).2 ⟨hv, hr2 v hsv⟩
        have hsymm : ∀ u w, G.Adj u w → G.Adj w u := fun u w h => hG.symm u w h
        apply ih
        refine GoInv.mk ?_ ?_ ?_ ?_ ?_ ?_ ?_
        · intro c hc
          rcases List.mem_cons.1 hc with h | h
          · rw [h]
            exact List.ne_nil_of_mem hvc
          · exact hI.comp_ne c h
        · intro c hc x hx
          rcases List.mem_cons.1 hc with h | h
          · rw [h] at hx
            exact ((hmemc x).1 hx).1
          · exact hI.comp_sub c h x hx
        · intro c hc
          rcases List.mem_cons.1 hc with h | h
          · rw [h]
            intro x hx y hxy
            have hxr := ((hmemc x).1 hx).2
            exact (hmemc y).2 ⟨hG.nbrs_sub x y hxy, hr3 x hxr y hxy⟩
          · exact hI.comp_closed c h
        · rw [List.flatten_cons, List.nodup_append]
          refine ⟨hG.nodup.filter _, hI.flat_nodup, ?_⟩
          intro a ha b hb hab
          subst hab
          obtain ⟨c, hc, hac⟩ := List.mem_flatten.1 hb
          have hav : Relation.ReflTransGen G.Adj a v :=
            rtg_symm G hsymm (hr1 a ((hmemc a).1 ha).2)
          have hvc' : v ∈ c := closed_rtg G c (hI.comp_closed c hc) hac hav
          exact hA ((hI.assigned_iff v).2 (List.mem_flatten.2 ⟨c, hc, hvc'⟩))
        · intro x
          rw [foldInsert_contains, List.flatten_cons, List.mem_append, hI.assigned_iff x]
        · intro x hx hxv
          rw [List.flatten_cons, List.mem_append]
          by_cases hxe : x = v
          · left
            rw [hxe]
            exact hvc
          · right
            exact hI.cover x hx (fun h => by
              rcases List.mem_cons.1 h with h' | h'
              · exact hxe h'
              · exact hxv h')
        · intro x hx
          exact hI.vs_sub x (List.mem_cons_of_mem _ hx)
      · rename_i hr
        exact fallback_good G hG assigned acc vs v hI hv hA

end G5

/-- `components` satisfies `ComponentsSpec` (G5). The hypothesis `WFBasics` is not needed. -/
theorem componentsSpec_of (hWF : WFBasics) : ComponentsSpec := by
  intro G hG
  have hI0 : G5.GoInv G G.nodes ∅ [] :=
    { comp_ne := by simp
      comp_sub := by simp
      comp_closed := by simp
      flat_nodup := by simp
      assigned_iff := by intro x; simp
      cover := fun x hx hn => absurd hx hn
      vs_sub := fun x hx => hx }
  obtain ⟨h1, h2, h3⟩ := G5.go_good G hG G.nodes ∅ [] hI0
  have hc : G.components = components.go G G.nodes ∅ [] := rfl
  rw [hc]
  exact ⟨(List.perm_ext_iff_of_nodup h2 hG.nodup).2 h3,
    fun c hc' => (h1 c hc').1,
    fun c hc' x hx y hxy => (h1 c hc').2.2 x hx y hxy⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.componentsSpec_of