CubicPathwidth.Alg.Proofs2.R3Records

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets

/-!
# R3: records respect `SameGraph`; records compose

Task R3 of the formalisation (§6.2). Proves `opsRecordCongr : OpsRecordCongr`
and `opsRecordAppend : OpsRecordAppend` (`Plan2.lean`), using only the Stage 1 contracts
`addEdgeSpec` and `removeNodeSpec` (`Proofs/Targets.lean`) and the statements of
`Spec2.lean`.

Reusable helpers (namespace `CubicPathwidth.Alg.R3`):
* `sameGraph_refl`, `sameGraph_symm`, `sameGraph_trans`;
* `removeNode_congr`, `addEdge_congr`, `addEdge_comm` (for WF graphs);
* `numNodes_eq_of_mem_iff`, `numNodes_removeNode` (`G.removeNode v` has one node less);
* `stepL` (the graph part of `redStep`), `stepL_props` (WF and node count of one
  reduction step), `redStep_eq`, `redStep_wf_numNodes`, `redStep_congr`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace R3

theorem sameGraph_refl (G : Graph) : SameGraph G G :=
  ⟨fun _ => Iff.rfl, fun _ _ => Iff.rfl⟩

theorem sameGraph_symm {G H : Graph} (h : SameGraph G H) : SameGraph H G :=
  ⟨fun v => (h.1 v).symm, fun u v => (h.2 u v).symm⟩

theorem sameGraph_trans {G H K : Graph} (h : SameGraph G H) (h' : SameGraph H K) :
    SameGraph G K :=
  ⟨fun v => (h.1 v).trans (h'.1 v), fun u v => (h.2 u v).trans (h'.2 u v)⟩

/-- Removing the same vertex from two graphs with the same nodes and edges. -/
theorem removeNode_congr {G H : Graph} (hG : G.WF) (hH : H.WF) (h : SameGraph G H)
    (v : Nat) : SameGraph (G.removeNode v) (H.removeNode v) := by
  obtain ⟨_, hn1, ha1⟩ := removeNodeSpec G v hG
  obtain ⟨_, hn2, ha2⟩ := removeNodeSpec H v hH
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [hn1 x, hn2 x, h.1 x]
  · rw [ha1 x y, ha2 x y, h.2 x y]

/-- Adding the same edge to two graphs with the same nodes and edges. -/
theorem addEdge_congr {G H : Graph} (hG : G.WF) (hH : H.WF) (h : SameGraph G H)
    {a b : Nat} (hab : a ≠ b) : SameGraph (G.addEdge a b) (H.addEdge a b) := by
  obtain ⟨_, hn1, ha1⟩ := addEdgeSpec G a b hG hab
  obtain ⟨_, hn2, ha2⟩ := addEdgeSpec H a b hH hab
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [hn1 x, hn2 x, h.1 x]
  · rw [ha1 x y, ha2 x y, h.2 x y]

/-- The order of the two endpoints of an added edge does not matter. -/
theorem addEdge_comm {G : Graph} (hG : G.WF) {a b : Nat} (hab : a ≠ b) :
    SameGraph (G.addEdge a b) (G.addEdge b a) := by
  obtain ⟨_, hn1, ha1⟩ := addEdgeSpec G a b hG hab
  obtain ⟨_, hn2, ha2⟩ := addEdgeSpec G b a hG (Ne.symm hab)
  refine ⟨fun x => ?_, fun x y => ?_⟩
  · rw [hn1 x, hn2 x]
    tauto
  · rw [ha1 x y, ha2 x y]
    tauto

/-- Two lists without repeats and with the same members have the same length. -/
theorem length_eq_of_mem_iff {l l' : List Nat} (hl : l.Nodup) (hl' : l'.Nodup)
    (h : ∀ x, x ∈ l ↔ x ∈ l') : l.length = l'.length :=
  ((List.perm_ext_iff_of_nodup hl hl').2 h).length_eq

/-- Two well-formed graphs with the same nodes have the same number of nodes. -/
theorem numNodes_eq_of_mem_iff {G H : Graph} (hG : G.WF) (hH : H.WF)
    (h : ∀ x, x ∈ G.nodes ↔ x ∈ H.nodes) : G.numNodes = H.numNodes :=
  length_eq_of_mem_iff hG.nodup hH.nodup h

/-- Removing a node lowers the node count by one. -/
theorem numNodes_removeNode {G : Graph} (hG : G.WF) {v : Nat} (hv : v ∈ G.nodes) :
    (G.removeNode v).numNodes + 1 = G.numNodes := by
  have hR := removeNodeSpec G v hG
  have hperm : (G.removeNode v).nodes.length = (G.nodes.erase v).length :=
    length_eq_of_mem_iff hR.1.nodup (hG.nodup.erase v) (fun x => by
      rw [hR.2.1 x, hG.nodup.mem_erase_iff]
      tauto)
  simp only [Graph.numNodes]
  rw [hperm, List.length_erase_of_mem hv]
  have := List.length_pos_of_mem hv
  omega

/-- The graph part of one step of `reduceLoop` (`G1` = `G` after `removeNode v`, `nb`
= the neighbour list of `v`). Same as `C5.stepG`. -/
def stepL (G1 : Graph) (nb : List Nat) : Graph :=
  match nb with
  | [a, b] => G1.addEdge a b
  | _ => G1

theorem redStep_eq (G : Graph) (v : Nat) :
    redStep G v = stepL (G.removeNode v) (G.nbrs v) := rfl

/-- A reduction step on a well-formed graph keeps well-formedness and the node count
drops by one (if the neighbours are nodes of `G1`, distinct). -/
theorem stepL_props {G1 : Graph} (hG1 : G1.WF) {nb : List Nat} (hnd : nb.Nodup)
    (hl : ∀ a ∈ nb, a ∈ G1.nodes) :
    (stepL G1 nb).WF ∧ (stepL G1 nb).numNodes = G1.numNodes := by
  rcases nb with _ | ⟨a, _ | ⟨b, _ | ⟨c, t⟩⟩⟩
  · exact ⟨hG1, rfl⟩
  · exact ⟨hG1, rfl⟩
  · have hab : a ≠ b := by
      intro h
      subst h
      simp at hnd
    have ha : a ∈ G1.nodes := hl a (by simp)
    have hb : b ∈ G1.nodes := hl b (by simp)
    obtain ⟨hw, hn, _⟩ := addEdgeSpec G1 a b hG1 hab
    have hcount : (G1.addEdge a b).numNodes = G1.numNodes := by
      apply numNodes_eq_of_mem_iff hw hG1
      intro x
      rw [hn x]
      constructor
      · rintro (h | rfl | rfl)
        · exact h
        · exact ha
        · exact hb
      · intro h
        exact Or.inl h
    exact ⟨hw, hcount⟩
  · exact ⟨hG1, rfl⟩

/-- `redStep` keeps well-formedness and removes exactly one node, for `v` a node. -/
theorem redStep_wf_numNodes {G : Graph} (hG : G.WF) {v : Nat} (hv : v ∈ G.nodes) :
    (redStep G v).WF ∧ (redStep G v).numNodes + 1 = G.numNodes := by
  have hRem := removeNodeSpec G v hG
  have hl : ∀ a ∈ G.nbrs v, a ∈ (G.removeNode v).nodes := by
    intro a ha
    have hav : a ≠ v := fun h => hG.loopless v (h ▸ ha)
    exact (hRem.2.1 a).2 ⟨hG.nbrs_sub v a ha, hav⟩
  obtain ⟨hw, hcount⟩ := stepL_props hRem.1 (hG.nbrs_nodup v) hl
  refine ⟨?_, ?_⟩
  · rw [redStep_eq]
    exact hw
  · rw [redStep_eq, hcount]
    exact numNodes_removeNode hG hv

theorem stepL_pair (G1 : Graph) (a b : Nat) : stepL G1 [a, b] = G1.addEdge a b := rfl

theorem stepL_of_ne {G1 : Graph} {nb : List Nat} (h : ∀ a b, nb ≠ [a, b]) :
    stepL G1 nb = G1 := by
  rcases nb with _ | ⟨a, _ | ⟨b, _ | ⟨c, t⟩⟩⟩
  · rfl
  · rfl
  · exact absurd rfl (h a b)
  · rfl

theorem exists_pair_of_length_two : ∀ l : List Nat, l.length = 2 → ∃ a b, l = [a, b]
  | [a, b], _ => ⟨a, b, rfl⟩
  | [], h => by simp at h
  | [_], h => by simp at h
  | _ :: _ :: _ :: _, h => by simp at h

/-- Two reduction steps on the same node set with the same neighbour sets give
`SameGraph` results (the lists may be reversed; then the edge is added in the other
order, which `addEdge_comm` handles). -/
theorem stepL_congr {G1 G1' : Graph} (h1 : G1.WF) (h1' : G1'.WF) (hS : SameGraph G1 G1')
    {l l' : List Nat} (hnd : l.Nodup) (hnd' : l'.Nodup) (hmem : ∀ x, x ∈ l ↔ x ∈ l') :
    SameGraph (stepL G1 l) (stepL G1' l') := by
  have hlen : l.length = l'.length := length_eq_of_mem_iff hnd hnd' hmem
  by_cases hp : ∃ a b, l = [a, b]
  · obtain ⟨a, b, rfl⟩ := hp
    have hl'2 : l'.length = 2 := by simpa using hlen.symm
    obtain ⟨a', b', rfl⟩ := exists_pair_of_length_two l' hl'2
    have hab : a ≠ b := by
      intro h
      subst h
      simp at hnd
    have hab' : a' ≠ b' := by
      intro h
      subst h
      simp at hnd'
    have h1m : a ∈ [a', b'] := (hmem a).1 (by simp)
    have h2m : b ∈ [a', b'] := (hmem b).1 (by simp)
    have h3m : a' ∈ [a, b] := (hmem a').2 (by simp)
    have h4m : b' ∈ [a, b] := (hmem b').2 (by simp)
    simp only [List.mem_cons, List.not_mem_nil, or_false] at h1m h2m h3m h4m
    have key : (a' = a ∧ b' = b) ∨ (a' = b ∧ b' = a) := by omega
    rw [stepL_pair, stepL_pair]
    rcases key with ⟨h5, h6⟩ | ⟨h5, h6⟩
    · rw [h5, h6]
      exact addEdge_congr h1 h1' hS hab
    · rw [h5, h6]
      exact sameGraph_trans (addEdge_congr h1 h1' hS hab) (addEdge_comm h1' hab)
  · have hne : ∀ a b, l ≠ [a, b] := fun a b h => hp ⟨a, b, h⟩
    have hp' : ¬ ∃ a' b', l' = [a', b'] := by
      rintro ⟨a', b', rfl⟩
      exact hp (exists_pair_of_length_two l (by simpa using hlen))
    have hne' : ∀ a' b', l' ≠ [a', b'] := fun a' b' h => hp' ⟨a', b', h⟩
    rw [stepL_of_ne hne, stepL_of_ne hne']
    exact hS

/-- `redStep` respects `SameGraph` (for well-formed graphs; no degree or membership
assumption is needed, since the neighbour lists have the same members). -/
theorem redStep_congr {F F' : Graph} (hF : F.WF) (hF' : F'.WF) (hS : SameGraph F F')
    (v : Nat) : SameGraph (redStep F v) (redStep F' v) := by
  have hRem := removeNode_congr hF hF' hS v
  have hmem : ∀ x, x ∈ F.nbrs v ↔ x ∈ F'.nbrs v := fun x => hS.2 v x
  rw [redStep_eq, redStep_eq]
  exact stepL_congr (removeNodeSpec F v hF).1 (removeNodeSpec F' v hF').1 hRem
    (hF.nbrs_nodup v) (hF'.nbrs_nodup v) hmem

end R3

open R3 in

/-- Records only depend on the graph up to `SameGraph`. -/
theorem opsRecordCongr : OpsRecordCongr := by
  intro F F' R ops
  induction ops generalizing F F' with
  | nil =>
    intro hF hF' hS hR
    exact sameGraph_trans (sameGraph_symm hS) hR
  | cons o ops ih =>
    intro hF hF' hS hR
    cases o with
    | red v nb =>
      obtain ⟨hv, hnd, hlen, hadj, hrest⟩ := hR
      have hv' : v ∈ F'.nodes := (hS.1 v).1 hv
      refine ⟨hv', hnd, hlen, fun x => (hadj x).trans (hS.2 v x), ?_⟩
      exact ih (redStep F v) (redStep F' v) (redStep_wf_numNodes hF hv).1
        (redStep_wf_numNodes hF' hv').1 (redStep_congr hF hF' hS v) hrest
    | del w =>
      obtain ⟨hw, hrest⟩ := hR
      have hw' : w ∈ F'.nodes := (hS.1 w).1 hw
      refine ⟨hw', ?_⟩
      exact ih (F.removeNode w) (F'.removeNode w) (removeNodeSpec F w hF).1
        (removeNodeSpec F' w hF').1 (removeNode_congr hF hF' hS w) hrest

open R3 in

/-- Records compose. -/
theorem opsRecordAppend : OpsRecordAppend := by
  intro F M R ops₁ ops₂
  induction ops₁ generalizing F with
  | nil =>
    intro hF hM h1 h2
    exact opsRecordCongr M F R ops₂ hM hF (sameGraph_symm h1) h2
  | cons o ops₁ ih =>
    intro hF hM h1 h2
    cases o with
    | red v nb =>
      obtain ⟨hv, hnd, hlen, hadj, hrest⟩ := h1
      exact ⟨hv, hnd, hlen, hadj, ih (redStep F v) (redStep_wf_numNodes hF hv).1 hM hrest h2⟩
    | del w =>
      obtain ⟨hw, hrest⟩ := h1
      exact ⟨hw, ih (F.removeNode w) (removeNodeSpec F w hF).1 hM hrest h2⟩

#print axioms opsRecordCongr
#print axioms opsRecordAppend

end CubicPathwidth.Alg