CubicPathwidth.Alg.Proofs.C5ReduceRecord

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

import CubicPathwidth.Alg.Spec

/-!
# C5: `ReduceRecordSpec` (invariant of the reduction loop)

Task C5 of the formalisation. The statement `reduceRecordSpec_of` takes the
hypotheses `WFBasics`, `AddEdgeSpec`, `RemoveNodeSpec` (proved in other files; only the
last two are used).

Strategy. For arbitrary fuel, stack and accumulated ops `L` (order irrelevant), the
invariant `Inv G0 G L` says: `G` is well formed; its nodes are nodes of `G0`; an edge of
`G0` between nodes of `G` is an edge of `G`; every op of `L` is `red v nb` with `v` a node
of `G0` no longer in `G`, and `nb` in `G0`; every node of `G0` is in `G` or among the
removed vertices of `L`. `reduceLoop` preserves it by induction on the fuel.
-/

namespace CubicPathwidth.Alg

open Graph

namespace C5

/-- The graph part of one step of `reduceLoop`: `G1` is the graph after `removeNode v` and
`nb` the neighbour list of `v`; two neighbours are joined by `addEdge`. -/
def stepG (G1 : Graph) (nb : List Nat) : Graph :=
  match nb with
  | [a, b] => G1.addEdge a b
  | _ => G1

/-- The invariant of the reduction loop relative to its start `G0`. -/
def Inv (G0 G : Graph) (L : List Op) : Prop :=
  G.WF ∧ (∀ x ∈ G.nodes, x ∈ G0.nodes) ∧
  (∀ x y, x ∈ G.nodes → y ∈ G.nodes → G0.Adj x y → G.Adj x y) ∧
  (∀ o ∈ L, ∃ v nb, o = Op.red v nb ∧ v ∈ G0.nodes ∧ v ∉ G.nodes ∧ ∀ x ∈ nb, x ∈ G0.nodes) ∧
  (∀ x ∈ G0.nodes, x ∈ G.nodes ∨ x ∈ redVertices L)

theorem mem_redVertices_reverse (L : List Op) (x : Nat) :
    x ∈ redVertices L.reverse ↔ x ∈ redVertices L := by
  unfold redVertices
  rw [List.mem_filterMap, List.mem_filterMap]
  simp only [List.mem_reverse]

theorem inv_reverse {G0 G : Graph} {L : List Op} (h : Inv G0 G L) :
    Inv G0 G L.reverse := by
  obtain ⟨h1, h2, h3, h4, h5⟩ := h
  refine ⟨h1, h2, h3, ?_, fun x hx => ?_⟩
  · intro o ho
    exact h4 o (List.mem_reverse.1 ho)
  · rcases h5 x hx with h | h
    · exact Or.inl h
    · exact Or.inr ((mem_redVertices_reverse L x).2 h)

/-- The graph step keeps well-formedness, the node set of `G1` and the edges of `G1`
(`AddEdgeSpec` adds edges only between nodes; here the two neighbours are nodes of `G1`
and distinct, by `nbrs_nodup`). -/
theorem stepG_props (hAdd : AddEdgeSpec) (G1 : Graph) (nb : List Nat) (hG1 : G1.WF)
    (hnb : nb.Nodup) (hnbN : ∀ x ∈ nb, x ∈ G1.nodes) :
    (stepG G1 nb).WF ∧ (∀ x, x ∈ (stepG G1 nb).nodes ↔ x ∈ G1.nodes) ∧
      (∀ x y, G1.Adj x y → (stepG G1 nb).Adj x y) := by
  rcases nb with _ | ⟨a, _ | ⟨b, _ | ⟨c, l⟩⟩⟩
  · exact ⟨hG1, fun _ => Iff.rfl, fun _ _ h => h⟩
  · exact ⟨hG1, fun _ => Iff.rfl, fun _ _ h => h⟩
  · have hab : a ≠ b := by
      intro h
      subst h
      simp at hnb
    have ha : a ∈ G1.nodes := hnbN a (by simp)
    have hb : b ∈ G1.nodes := hnbN b (by simp)
    obtain ⟨h1, h2, h3⟩ := hAdd G1 a b hG1 hab
    refine ⟨h1, ?_, ?_⟩
    · intro x
      show x ∈ (G1.addEdge a b).nodes ↔ x ∈ G1.nodes
      rw [h2 x]
      constructor
      · rintro (h | rfl | rfl)
        · exact h
        · exact ha
        · exact hb
      · intro h
        exact Or.inl h
    · intro x y h
      show (G1.addEdge a b).Adj x y
      rw [h3 x y]
      exact Or.inl h
  · exact ⟨hG1, fun _ => Iff.rfl, fun _ _ h => h⟩

/-- One non-skipped step of the loop preserves the invariant. -/
theorem step_inv (hRem : RemoveNodeSpec) (hAdd : AddEdgeSpec) (G0 G : Graph) (L : List Op)
    (v : Nat) (hI : Inv G0 G L) (hm : G.mem v = true) :
    Inv G0 (stepG (G.removeNode v) (G.nbrs v)) (Op.red v (G.nbrs v) :: L) := by
  obtain ⟨hG, hsub, hedge, hops, hcov⟩ := hI
  have hv : v ∈ G.nodes := (hG.mem_iff v).1 hm
  obtain ⟨hR1, hR2, hR3⟩ := hRem G v hG
  have hnbN : ∀ x ∈ G.nbrs v, x ∈ (G.removeNode v).nodes := by
    intro x hx
    rw [hR2]
    exact ⟨hG.nbrs_sub v x hx, fun h => hG.loopless v (h ▸ hx)⟩
  obtain ⟨hS1, hS2, hS3⟩ :=
    stepG_props hAdd (G.removeNode v) (G.nbrs v) hR1 (hG.nbrs_nodup v) hnbN
  refine ⟨hS1, ?_, ?_, ?_, ?_⟩
  · intro x hx
    rw [hS2, hR2] at hx
    exact hsub x hx.1
  · intro x y hx hy hG0
    rw [hS2, hR2] at hx hy
    have hGxy := hedge x y hx.1 hy.1 hG0
    exact hS3 x y ((hR3 x y).2 ⟨hGxy, hx.2, hy.2⟩)
  · intro o ho
    rcases List.mem_cons.1 ho with rfl | ho
    · refine ⟨v, G.nbrs v, rfl, hsub v hv, ?_, fun x hx => hsub x (hG.nbrs_sub v x hx)⟩
      rw [hS2, hR2]
      simp
    · obtain ⟨v', nb', h1, h2, h3, h4⟩ := hops o ho
      refine ⟨v', nb', h1, h2, ?_, h4⟩
      intro hmem
      exact h3 ((hR2 v').1 ((hS2 v').1 hmem)).1
  · intro x hx
    rcases hcov x hx with h | h
    · by_cases hxv : x = v
      · right
        rw [hxv]
        simp [redVertices]
      · left
        rw [hS2, hR2]
        exact ⟨h, hxv⟩
    · right
      have h' : x ∈ redVertices (Op.red v (G.nbrs v) :: L) := by
        simp only [redVertices, List.filterMap_cons] at h ⊢
        exact List.mem_cons_of_mem _ h
      exact h'

/-- The loop preserves the invariant, for every fuel, stack and start. -/
theorem loop_inv (hRem : RemoveNodeSpec) (hAdd : AddEdgeSpec) (G0 : Graph) (fuel : Nat) :
    ∀ (G : Graph) (stack : List Nat) (L : List Op), Inv G0 G L →
      Inv G0 (reduceLoop fuel G stack L).1 (reduceLoop fuel G stack L).2.1 := by
  induction fuel with
  | zero =>
    intro G stack L hI
    cases stack with
    | nil =>
      simp only [reduceLoop]
      exact inv_reverse hI
    | cons v rest =>
      simp only [reduceLoop]
      exact inv_reverse hI
  | succ n ih =>
    intro G stack L hI
    cases stack with
    | nil =>
      simp only [reduceLoop]
      exact inv_reverse hI
    | cons v rest =>
      by_cases hc : (!G.mem v || G.degree v > 2) = true
      · simp only [reduceLoop, hc]
        exact ih G rest L hI
      · have hm : G.mem v = true := by
          cases h : G.mem v
          · exact absurd (by simp [h] at hc ⊢) hc
          · rfl
        simp only [reduceLoop, hc]
        exact ih _ _ _ (step_inv hRem hAdd G0 G L v hI hm)

end C5

/-- C5: `reduce_record` (`reduceRecord`) satisfies `ReduceRecordSpec`. -/
theorem reduceRecordSpec_of (hWF : WFBasics) (hAdd : AddEdgeSpec) (hRem : RemoveNodeSpec) :
    ReduceRecordSpec := by
  unfold ReduceRecordSpec
  intro G hG
  have hI : C5.Inv G G [] :=
    ⟨hG, fun _ hx => hx, fun _ _ _ _ h => h,
      fun o ho => absurd ho (List.not_mem_nil), fun _ hx => Or.inl hx⟩
  have key := C5.loop_inv hRem hAdd G (3 * G.numNodes + 1) G
    (G.nodes.filter fun v => G.degree v ≤ 2).reverse [] hI
  dsimp only [reduceRecord, reduceRecordF]
  exact ⟨key.1, key.2.1, key.2.2.1, key.2.2.2.1, key.2.2.2.2⟩

#print axioms CubicPathwidth.Alg.reduceRecordSpec_of

end CubicPathwidth.Alg