CubicPathwidth.Alg.Proofs2.U3UndoNoFallback

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

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

/-!
# U3: `UndoNoFallback` from the attachment invariant

Task U3 of the formalisation. Helpers live in the namespace
`CubicPathwidth.Alg.U3`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace U3

theorem copy_wf (G : Graph) (hG : G.WF) : G.copy.WF :=
  (inducedSpec G (fun _ => true) hG).1

theorem induced_wf (G : Graph) (keep : Nat → Bool) (hG : G.WF) : (G.induced keep).WF :=
  (inducedSpec G keep hG).1

theorem sameGraph_copy (G : Graph) (hG : G.WF) : SameGraph G G.copy := by
  have h := inducedSpec G (fun _ => true) hG
  refine ⟨fun v => ?_, fun u v => ?_⟩
  · show v ∈ G.nodes ↔ v ∈ (G.induced fun _ => true).nodes
    rw [h.2.1 v]
    simp
  · show G.Adj u v ↔ (G.induced fun _ => true).Adj u v
    rw [h.2.2 u v]
    simp

theorem emptiable_copy_of {G : Graph} (hG : G.WF) (hCongr : OpsRecordCongr)
    (hE : Emptiable G) : Emptiable G.copy := by
  obtain ⟨ops, hred, hrec⟩ := hE
  exact ⟨ops, hred, hCongr G G.copy Graph.empty ops hG (copy_wf G hG)
    (sameGraph_copy G hG) hrec⟩

/-- The no-fallback flag of `pd_tw2` on a component `F[C]` that is emptiable. -/
theorem pdFlag_false (hPd : PdTw2NoFallback) (hConf : ReduceConfluent)
    (hCongr : OpsRecordCongr) {F : Graph} (hF : F.WF) (C : List Nat)
    (hE : Emptiable (F.induced C.contains)) :
    (pdTw2F (F.induced C.contains)).2 = false := by
  have hWF := induced_wf F C.contains hF
  exact hPd _ hWF (hConf _ (copy_wf _ hWF) (emptiable_copy_of hWF hCongr hE))

/-- A set `S` of at most two vertices of `R`, which are adjacent when there are two,
lies in one bag of a valid decomposition of `R`. -/
theorem exists_bag {R : Graph} {bagsR : List Bag} (hVR : ValidPD R bagsR)
    (S : List Nat) (h1 : ∀ x ∈ S, x ∈ R.nodes) (h2 : S.length ≤ 2)
    (h3 : ∀ a b, S = [a, b] → R.Adj a b) (hne : S ≠ []) :
    ∃ B ∈ bagsR, subsetB S B = true := by
  match S, h1, h2, h3, hne with
  | [], _, _, _, hne => exact absurd rfl hne
  | [a], h1, _, _, _ =>
    obtain ⟨i, B, hB, haB⟩ := hVR.1 a (h1 a (by simp))
    exact ⟨B, List.mem_of_getElem? hB, by simp [subsetB, haB]⟩
  | [a, b], h1, _, h3, _ =>
    obtain ⟨B, hB, haB, hbB⟩ := hVR.2.2 a b (h1 a (by simp)) (h3 a b rfl)
    exact ⟨B, hB, by simp [subsetB, haB, hbB]⟩
  | _ :: _ :: _ :: _, _, h2, _, _ => simp at h2

end U3

open U3

theorem undoNoFallback_of (hAtt : AttachInvariant) (hPd : PdTw2NoFallback)
    (hConf : ReduceConfluent) (hCongr : OpsRecordCongr) : UndoNoFallback := by
  intro F R ops bagsR hF hR hOps hVR
  have hA := hAtt F R ops hF hR hOps
  unfold undoF
  dsimp only
  split
  · rename_i hnot
    exfalso
    simp only [Bool.not_eq_true', List.all_eq_false] at hnot
    obtain ⟨x, hx, hfx⟩ := hnot
    obtain ⟨C, hC, rfl⟩ := List.mem_map.1 hx
    dsimp only at hfx
    apply hfx
    obtain ⟨h1, h2, h3, _⟩ := hA C hC
    generalize undoAttach F (deletedSet ops) C = S at h1 h2 h3 ⊢
    have hall : S.all R.mem = true := List.all_eq_true.2 fun x hx => (hR.mem_iff x).2 (h1 x hx)
    have hidx : S = [] ∨ (bagsR.findIdx? (fun x => subsetB S x)).isSome = true := by
      by_cases hne : S = []
      · exact Or.inl hne
      · right
        obtain ⟨B, hB, hsub⟩ := exists_bag hVR S h1 h2 h3 hne
        rw [List.findIdx?_isSome, List.any_eq_true]
        exact ⟨B, hB, hsub⟩
    rcases hidx with rfl | hidx
    · simp
    · rcases S with _ | ⟨a, _ | ⟨b, _ | ⟨c, S⟩⟩⟩
      · simp
      · simp [hall, hidx]
      · have he : R.hasEdge a b = true := List.contains_iff_mem.2 (h3 a b rfl)
        simp [hall, he, hidx]
      · simp at h2
  · rename_i hnot
    dsimp only
    rw [List.any_eq_false]
    intro x hx
    obtain ⟨C, hC, rfl⟩ := List.mem_map.1 hx
    have hf := pdFlag_false hPd hConf hCongr hF C (hA C hC).2.2.2
    simp [hf]

#print axioms undoNoFallback_of

end CubicPathwidth.Alg
Back to top