CubicPathwidth.Alg.Proofs.G4Induced

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

import CubicPathwidth.Alg.Spec

/-!
# G4: `InducedSpec` (Python `subgraph(S).copy()` under model M)

`Graph.induced` starts from the edgeless graph on `ns = G.nodes.filter keep` and folds
`addEdge u v` over the pairs `u ∈ ns`, `v ∈ G.nbrs u` with `keep v`. The helpers below
state the fold for an arbitrary initial graph (induction on the lists), using the
hypothesis `AddEdgeSpec` for one `addEdge` step, and then specialise.
-/

namespace CubicPathwidth.Alg

open Graph

namespace G4

/-- The edgeless graph on the list `ns` (the start graph of `Graph.induced`). -/
def startGraph (ns : List Nat) : Graph :=
  ⟨ns, ns.foldl (fun (a : Std.HashMap Nat (List Nat)) (v : Nat) => a.insert v []) ∅⟩

theorem startGraph_nodes (ns : List Nat) : (startGraph ns).nodes = ns := rfl

/-- Membership in the keys of a fold of `insert _ []`. -/
theorem foldInsert_contains (l : List Nat) :
    ∀ (m : Std.HashMap Nat (List Nat)) (x : Nat),
      (l.foldl (fun (a : Std.HashMap Nat (List Nat)) (v : Nat) => a.insert v []) m).contains x = true ↔ x ∈ l ∨ m.contains x = true := by
  induction l with
  | nil => intro m x; simp
  | cons a l ih =>
    intro m x
    rw [List.foldl_cons, ih, Std.HashMap.contains_insert]
    simp only [beq_iff_eq, Bool.or_eq_true, 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)

/-- Values of a fold of `insert _ []` over a map whose values are all `[]`. -/
theorem foldInsert_getD (l : List Nat) :
    ∀ (m : Std.HashMap Nat (List Nat)), (∀ x, m.getD x [] = []) →
      ∀ x, (l.foldl (fun (a : Std.HashMap Nat (List Nat)) (v : Nat) => a.insert v []) m).getD x [] = [] := by
  induction l with
  | nil => intro m hm x; exact hm x
  | cons a l ih =>
    intro m hm x
    rw [List.foldl_cons]
    apply ih
    intro y
    rw [Std.HashMap.getD_insert]
    split
    · rfl
    · exact hm y

theorem startGraph_nbrs (ns : List Nat) (u : Nat) : (startGraph ns).nbrs u = [] :=
  foldInsert_getD ns ∅ (fun _ => Std.HashMap.getD_empty) u

theorem startGraph_not_adj (ns : List Nat) (x y : Nat) : ¬ (startGraph ns).Adj x y := by
  intro h
  rw [Graph.Adj, startGraph_nbrs] at h
  exact List.not_mem_nil h

theorem startGraph_wf (ns : List Nat) (hnd : ns.Nodup) : (startGraph ns).WF := by
  refine ⟨hnd, ?_, ?_, ?_, ?_, ?_⟩
  · intro v
    unfold Graph.mem
    show (ns.foldl (fun (a : Std.HashMap Nat (List Nat)) (v : Nat) => a.insert v []) ∅).contains v = true ↔ v ∈ ns
    rw [foldInsert_contains]
    simp
  · intro v
    rw [startGraph_nbrs]
    exact List.nodup_nil
  · intro u v h
    rw [startGraph_nbrs] at h
    exact absurd h (List.not_mem_nil)
  · intro u v h
    rw [startGraph_nbrs] at h
    exact absurd h (List.not_mem_nil)
  · intro v h
    rw [startGraph_nbrs] at h
    exact absurd h (List.not_mem_nil)

/-- The inner fold: `addEdge u v` for the neighbours `v ∈ l` with `keep v`. -/
theorem inner_fold (hAdd : AddEdgeSpec) (keep : Nat → Bool) (S : Nat → Prop) (u : Nat) :
    ∀ (l : List Nat) (H : Graph), H.WF → (∀ x, x ∈ H.nodes ↔ S x) → S u →
      (∀ v ∈ l, keep v = true → S v) → (∀ v ∈ l, v ≠ u) →
      (l.foldl (fun H v => if keep v then H.addEdge u v else H) H).WF ∧
      (∀ x, x ∈ (l.foldl (fun H v => if keep v then H.addEdge u v else H) H).nodes ↔
        x ∈ H.nodes) ∧
      (∀ x y, (l.foldl (fun H v => if keep v then H.addEdge u v else H) H).Adj x y ↔
        (H.Adj x y ∨ ∃ v ∈ l, keep v = true ∧ ((x = u ∧ y = v) ∨ (x = v ∧ y = u)))) := by
  intro l
  induction l with
  | nil =>
    intro H hH _ _ _ _
    refine ⟨hH, fun x => Iff.rfl, fun x y => ?_⟩
    simp
  | cons v l ih =>
    intro H hH hS hSu hSl hne
    have hv : v ≠ u := hne v (by simp)
    have hSl' : ∀ w ∈ l, keep w = true → S w := fun w hw => hSl w (by simp [hw])
    have hne' : ∀ w ∈ l, w ≠ u := fun w hw => hne w (by simp [hw])
    rw [List.foldl_cons]
    by_cases hk : keep v = true
    · simp only [hk, ↓reduceIte]
      have hvS : S v := hSl v (by simp) hk
      have huN : u ∈ H.nodes := (hS u).mpr hSu
      have hvN : v ∈ H.nodes := (hS v).mpr hvS
      obtain ⟨hW1, hN1, hA1⟩ := hAdd H u v hH (Ne.symm hv)
      have hN1'' : ∀ x, x ∈ (H.addEdge u v).nodes ↔ x ∈ H.nodes := by
        intro x
        rw [hN1 x]
        constructor
        · rintro (h | rfl | rfl)
          · exact h
          · exact huN
          · exact hvN
        · intro h
          exact Or.inl h
      obtain ⟨hWR, hNR, hAR⟩ :=
        ih (H.addEdge u v) hW1 (fun x => (hN1'' x).trans (hS x)) hSu hSl' hne'
      refine ⟨hWR, fun x => (hNR x).trans (hN1'' x), fun x y => ?_⟩
      rw [hAR x y, hA1 x y]
      constructor
      · rintro ((h | h | h) | ⟨w, hw, hk2, hxy⟩)
        · exact Or.inl h
        · exact Or.inr ⟨v, by simp, hk, Or.inl h⟩
        · exact Or.inr ⟨v, by simp, hk, Or.inr h⟩
        · exact Or.inr ⟨w, by simp [hw], hk2, hxy⟩
      · rintro (h | ⟨w, hw, hk2, hxy⟩)
        · exact Or.inl (Or.inl h)
        · rcases List.mem_cons.1 hw with hwv | hw'
          · subst hwv
            exact Or.inl (Or.inr hxy)
          · exact Or.inr ⟨w, hw', hk2, hxy⟩
    · have hk' : keep v = false := by simpa using hk
      simp only [hk', Bool.false_eq_true, ↓reduceIte]
      obtain ⟨hWR, hNR, hAR⟩ := ih H hH hS hSu hSl' hne'
      refine ⟨hWR, hNR, fun x y => ?_⟩
      rw [hAR x y]
      constructor
      · rintro (h | ⟨w, hw, hk2, hxy⟩)
        · exact Or.inl h
        · exact Or.inr ⟨w, by simp [hw], hk2, hxy⟩
      · rintro (h | ⟨w, hw, hk2, hxy⟩)
        · exact Or.inl h
        · rcases List.mem_cons.1 hw with hwv | hw'
          · subst hwv
            exact absurd hk2 hk
          · exact Or.inr ⟨w, hw', hk2, hxy⟩

/-- The outer fold over the list `us` of vertices. -/
theorem outer_fold (hAdd : AddEdgeSpec) (G : Graph) (keep : Nat → Bool) (hG : G.WF)
    (S : Nat → Prop)
    (hcl : ∀ u, S u → ∀ v ∈ G.nbrs u, keep v = true → S v) :
    ∀ (us : List Nat) (H : Graph), H.WF → (∀ x, x ∈ H.nodes ↔ S x) → (∀ u ∈ us, S u) →
      (us.foldl (fun H u => (G.nbrs u).foldl (fun H v => if keep v then H.addEdge u v else H) H)
        H).WF ∧
      (∀ x, x ∈ (us.foldl (fun H u => (G.nbrs u).foldl
          (fun H v => if keep v then H.addEdge u v else H) H) H).nodes ↔ x ∈ H.nodes) ∧
      (∀ x y, (us.foldl (fun H u => (G.nbrs u).foldl
          (fun H v => if keep v then H.addEdge u v else H) H) H).Adj x y ↔
        (H.Adj x y ∨ ∃ u ∈ us, ∃ v ∈ G.nbrs u,
          keep v = true ∧ ((x = u ∧ y = v) ∨ (x = v ∧ y = u)))) := by
  intro us
  induction us with
  | nil =>
    intro H hH _ _
    refine ⟨hH, fun x => Iff.rfl, fun x y => ?_⟩
    simp
  | cons u us ih =>
    intro H hH hS hus
    have hSu : S u := hus u (by simp)
    have hus' : ∀ u' ∈ us, S u' := fun u' hu' => hus u' (by simp [hu'])
    simp only [List.foldl_cons]
    obtain ⟨hW1, hN1, hA1⟩ :=
      inner_fold hAdd keep S u (G.nbrs u) H hH hS hSu
        (fun v hv hk => hcl u hSu v hv hk)
        (fun v hv heq => by
          subst heq
          exact hG.loopless _ hv)
    obtain ⟨hW2, hN2, hA2⟩ :=
      ih _ hW1 (fun x => (hN1 x).trans (hS x)) hus'
    refine ⟨hW2, fun x => (hN2 x).trans (hN1 x), fun x y => ?_⟩
    rw [hA2 x y, hA1 x y]
    simp only [List.mem_cons, exists_eq_or_imp, or_assoc]

end G4

open G4

/-- `induced` (Python `subgraph(S).copy()` under model M) is well formed, has the nodes
`G.nodes` with `keep`, and the edges of `G` between kept vertices. -/
theorem inducedSpec_of (hWF : WFBasics) (hAdd : AddEdgeSpec) : InducedSpec := by
  intro G keep hG
  have hnd : (G.nodes.filter keep).Nodup := hG.nodup.filter _
  have hS0 := startGraph_wf (G.nodes.filter keep) hnd
  have hcl : ∀ u, (u ∈ G.nodes ∧ keep u = true) → ∀ v ∈ G.nbrs u, keep v = true →
      (v ∈ G.nodes ∧ keep v = true) :=
    fun u _ v hv hk => ⟨hG.nbrs_sub u v hv, hk⟩
  have hInd : G.induced keep = (G.nodes.filter keep).foldl
      (fun H u => (G.nbrs u).foldl (fun H v => if keep v then H.addEdge u v else H) H)
      (startGraph (G.nodes.filter keep)) := rfl
  have hNodes : ∀ x, x ∈ (startGraph (G.nodes.filter keep)).nodes ↔
      (x ∈ G.nodes ∧ keep x = true) := by
    intro x
    rw [startGraph_nodes]
    exact List.mem_filter
  obtain ⟨h1, h2, h3⟩ := outer_fold hAdd G keep hG (fun x => x ∈ G.nodes ∧ keep x = true) hcl
    (G.nodes.filter keep) (startGraph (G.nodes.filter keep)) hS0 hNodes
    (fun u hu => List.mem_filter.1 hu)
  rw [hInd]
  refine ⟨h1, fun x => (h2 x).trans (hNodes x), fun x y => ?_⟩
  rw [h3 x y]
  constructor
  · rintro (h | ⟨u, hu, v, hv, hk, hxy⟩)
    · exact absurd h (startGraph_not_adj _ x y)
    · obtain ⟨hu1, hku⟩ := List.mem_filter.1 hu
      rcases hxy with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
      · exact ⟨hv, hku, hk⟩
      · exact ⟨hG.symm _ _ hv, hk, hku⟩
  · rintro ⟨hadj, hkx, hky⟩
    have hx : x ∈ G.nodes := hG.nbrs_sub y x (hG.symm x y hadj)
    exact Or.inr ⟨x, List.mem_filter.2 ⟨hx, hkx⟩, y, hadj, hky, Or.inl ⟨rfl, rfl⟩⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.inducedSpec_of