CubicPathwidth.Alg.Proofs.C6PdTw2

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

import CubicPathwidth.Alg.Spec

/-!
# C6: validity of `pd_tw2` (`PdTw2Valid`)

Induction on the fuel. Base cases and fallbacks give a single bag `H.nodes` (or `[]` when
`H` has no nodes). The main case glues, at the separator `X = v :: nb` of a reduction
recorded by `reduceRecordF H.copy` (`SeparatorGlueValid`), the recursive decompositions of
the induced graphs `H[c]` for the components `c` of `H[V \ X]`.
Hypotheses are taken from `Spec.lean`: `WFBasics`, `InducedSpec`, `ComponentsSpec`,
`SeparatorGlueValid`, `ReduceRecordSpec`.
-/

namespace CubicPathwidth.Alg

open Graph

namespace C6

/-- The single bag `[H.nodes]` is a valid decomposition of a well-formed graph. -/
theorem single_valid (H : Graph) (hH : H.WF) :
    ValidPD H [H.nodes] ∧ BagsWithin H [H.nodes] := by
  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
  · intro v hv
    exact ⟨0, H.nodes, rfl, hv⟩
  · intro v hv i j k hij hjk hi hk
    obtain ⟨B, hB, hvB⟩ := hk
    have hk0 : k = 0 := by
      rcases k with _ | k
      · rfl
      · simp at hB
    subst hk0
    have hj0 : j = 0 := by omega
    subst hj0
    exact ⟨H.nodes, rfl, hv⟩
  · intro u v hu huv
    exact ⟨H.nodes, List.mem_singleton.2 rfl, hu, hH.nbrs_sub u v huv⟩
  · intro B hB v hv
    rw [List.mem_singleton] at hB
    subst hB
    exact hv

/-- The empty decomposition is valid for a graph with no nodes. -/
theorem empty_valid (H : Graph) (h0 : H.numNodes = 0) :
    ValidPD H [] ∧ BagsWithin H [] := by
  have hlen : H.nodes.length = 0 := h0
  have hn : H.nodes = [] := List.length_eq_zero_iff.1 hlen
  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
  · intro v hv
    rw [hn] at hv
    simp at hv
  · intro v hv
    rw [hn] at hv
    simp at hv
  · intro u v hu _
    rw [hn] at hu
    simp at hu
  · intro B hB
    simp at hB

/-- Membership in the elimination bags: `X = v :: nb` for a recorded reduction. -/
theorem mem_elimBags_iff (ops : List Op) (X : Bag) (h : X ∈ elimBags ops) :
    ∃ v nb, Op.red v nb ∈ ops ∧ X = v :: nb := by
  unfold elimBags at h
  rw [List.mem_filterMap] at h
  obtain ⟨o, ho, hX⟩ := h
  cases o with
  | red v nb =>
    simp only at hX
    exact ⟨v, nb, ho, (Option.some.inj hX).symm⟩
  | del w =>
    simp at hX

/-- The node list of an induced graph is a permutation of the filtered node list. -/
theorem induced_nodes_perm (H : Graph) (keep : Nat → Bool) (hH : H.WF)
    (hInd : InducedSpec) :
    (H.induced keep).nodes.Perm (H.nodes.filter keep) := by
  have hI := hInd H keep hH
  rw [List.perm_ext_iff_of_nodup hI.1.nodup (List.Nodup.filter keep hH.nodup)]
  intro a
  rw [hI.2.1 a, List.mem_filter]

/-- The components of `H[V \ X]`. -/
def compsOf (H : Graph) (X : List Nat) : List (List Nat) :=
  (H.induced fun v => !X.contains v).components

/-- The output of the gluing step of `pd_tw2`, written as in `pdTw2Fuel`. -/
def glueOut (H : Graph) (X : List Nat) (f : Nat) : List Bag :=
  let parts := (compsOf H X).map fun c => pdTw2Fuel f (H.induced c.contains)
  let out := parts.flatMap fun p => p.1.map fun B => bagUnion B X
  if out.isEmpty then [X] else out

/-- The gluing step is valid, given the induction hypothesis for fuel `f`. -/
theorem glue_valid (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hGlue : SeparatorGlueValid) (f : Nat)
    (ih : ∀ K : Graph, K.WF → ValidPD K (pdTw2Fuel f K).1 ∧ BagsWithin K (pdTw2Fuel f K).1)
    (H : Graph) (X : List Nat) (hH : H.WF) (hX : ∀ x ∈ X, x ∈ H.nodes) :
    ValidPD H (glueOut H X f) ∧ BagsWithin H (glueOut H X f) := by
  have hI := hInd H (fun v => !X.contains v) hH
  have hH' : (H.induced fun v => !X.contains v).WF := hI.1
  have hcp := hComp _ hH'
  -- the parts, paired with their recursive decompositions
  have hpm : ((compsOf H X).map fun c => (c, (pdTw2Fuel f (H.induced c.contains)).1)).map
      (fun p => p.1) = compsOf H X := by
    rw [List.map_map]
    exact List.map_id _
  have hperm : (((compsOf H X).map fun c =>
      (c, (pdTw2Fuel f (H.induced c.contains)).1)).map (fun p => p.1)).flatten.Perm
      (H.nodes.filter fun v => !X.contains v) := by
    rw [hpm]
    exact hcp.1.trans (induced_nodes_perm H (fun v => !X.contains v) hH hInd)
  have hclos : ∀ p ∈ (compsOf H X).map (fun c => (c, (pdTw2Fuel f (H.induced c.contains)).1)),
      ∀ x ∈ p.1, ∀ y, H.Adj x y → y ∈ p.1 ∨ y ∈ X := by
    intro p hp x hx y hxy
    obtain ⟨c, hc, rfl⟩ := List.mem_map.1 hp
    change x ∈ c at hx
    change y ∈ c ∨ y ∈ X
    by_cases hyX : y ∈ X
    · exact Or.inr hyX
    · left
      have hxN : x ∈ (H.induced fun v => !X.contains v).nodes :=
        hcp.1.mem_iff.1 (List.mem_flatten.2 ⟨c, hc, hx⟩)
      have hxk : (!X.contains x) = true := ((hI.2.1 x).1 hxN).2
      have hyk : (!X.contains y) = true := by simp [hyX]
      have hadj : (H.induced fun v => !X.contains v).Adj x y :=
        (hI.2.2 x y).2 ⟨hxy, hxk, hyk⟩
      exact hcp.2.2 c hc x hx y hadj
  have hrec : ∀ p ∈ (compsOf H X).map (fun c => (c, (pdTw2Fuel f (H.induced c.contains)).1)),
      ValidPD (H.induced p.1.contains) p.2 ∧ BagsWithin (H.induced p.1.contains) p.2 := by
    intro p hp
    obtain ⟨c, _, rfl⟩ := List.mem_map.1 hp
    exact ih (H.induced c.contains) (hInd H _ hH).1
  have hglue := hGlue H X _ hH hX hperm hclos hrec
  dsimp only at hglue
  simp only [List.flatMap_map] at hglue
  unfold glueOut
  simp only [List.flatMap_map]
  exact hglue

/-- Main induction: `pd_tw2` with fuel `fuel` is valid on every well-formed graph. -/
theorem main_fuel (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hGlue : SeparatorGlueValid) (hRed : ReduceRecordSpec) :
    ∀ (fuel : Nat) (H : Graph), H.WF →
      ValidPD H (pdTw2Fuel fuel H).1 ∧ BagsWithin H (pdTw2Fuel fuel H).1 := by
  intro fuel
  induction fuel with
  | zero =>
    intro H hH
    by_cases h0 : H.numNodes = 0
    · have e : (pdTw2Fuel 0 H).1 = [] := by
        unfold pdTw2Fuel
        rw [if_pos h0]
      rw [e]
      exact empty_valid H h0
    · have e : (pdTw2Fuel 0 H).1 = [H.nodes] := by
        unfold pdTw2Fuel
        rw [if_neg h0]
        split <;> rfl
      rw [e]
      exact single_valid H hH
  | succ f ih =>
    intro H hH
    by_cases h0 : H.numNodes = 0
    · have e : (pdTw2Fuel (f + 1) H).1 = [] := by
        unfold pdTw2Fuel
        rw [if_pos h0]
      rw [e]
      exact empty_valid H h0
    by_cases h3 : H.numNodes ≤ 3
    · have e : (pdTw2Fuel (f + 1) H).1 = [H.nodes] := by
        unfold pdTw2Fuel
        rw [if_neg h0, if_pos h3]
      rw [e]
      exact single_valid H hH
    have hcopy : H.copy.WF := (hInd H (fun _ => true) hH).1
    have hops := (hRed H.copy hcopy).2.2.2.1
    unfold pdTw2Fuel
    rw [if_neg h0, if_neg h3]
    dsimp only
    split
    · exact single_valid H hH
    · split
      · exact single_valid H hH
      · rename_i X heq
        have hXm := List.mem_of_find?_eq_some heq
        obtain ⟨v, nb, hop, rfl⟩ := mem_elimBags_iff _ _ hXm
        have hX : ∀ x ∈ v :: nb, x ∈ H.nodes := by
          obtain ⟨v', nb', he, hv', -, hnb'⟩ := hops (Op.red v nb) hop
          obtain ⟨rfl, rfl⟩ := Op.red.inj he
          intro x hx
          rcases List.mem_cons.1 hx with rfl | hx
          · exact ((hInd H (fun _ => true) hH).2.1 x).1 hv' |>.1
          · exact ((hInd H (fun _ => true) hH).2.1 x).1 (hnb' x hx) |>.1
        exact glue_valid hInd hComp hGlue f ih H (v :: nb) hH hX

end C6

/-- Theorem `pd_tw2` (`PdTw2Valid`): valid for every well-formed graph. -/
theorem pdTw2Valid_of (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hGlue : SeparatorGlueValid) (hRed : ReduceRecordSpec) : PdTw2Valid := by
  intro H hH
  exact C6.main_fuel hWF hInd hComp hGlue hRed H.numNodes H hH

#print axioms CubicPathwidth.Alg.pdTw2Valid_of

end CubicPathwidth.Alg