CubicPathwidth.Alg.Proofs.C7Undo

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

import CubicPathwidth.Alg.Spec

/-!
# C7: `UndoValid` (validity of `undo`, Lemma A.28 (`lem:undo`))

Proof of `undoValid_of`, with all hypotheses supplied by other tasks. Helpers live in
the namespace `CubicPathwidth.Alg.C7`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace C7

/-! ## 1. Basic facts about `InBag` and index convexity -/

/-- Index convexity: the positions of the bags containing `v` form an interval.
This is the second clause of `ValidPD`, stated for an arbitrary list of bags. -/
def ConvL (L : List Bag) (v : Nat) : Prop :=
  ∀ i j k, i ≤ j → j ≤ k → InBag L i v → InBag L k v → InBag L j v

theorem inBag_append (X Y : List Bag) (i v : Nat) :
    InBag (X ++ Y) i v ↔
      (i < X.length ∧ InBag X i v) ∨ (X.length ≤ i ∧ InBag Y (i - X.length) v) := by
  unfold InBag
  by_cases h : i < X.length
  · rw [List.getElem?_append_left h]
    constructor
    · intro h'; exact Or.inl ⟨h, h'⟩
    · rintro (⟨_, h'⟩ | ⟨h2, _⟩)
      · exact h'
      · omega
  · rw [List.getElem?_append_right (by omega)]
    constructor
    · intro h'; exact Or.inr ⟨by omega, h'⟩
    · rintro (⟨h1, _⟩ | ⟨_, h'⟩)
      · omega
      · exact h'

theorem inBag_lt {L : List Bag} {i : Nat} {v : Nat} (h : InBag L i v) : i < L.length := by
  obtain ⟨B, hB, _⟩ := h
  exact (List.getElem?_eq_some_iff.1 hB).1

theorem inBag_mem {L : List Bag} {i v : Nat} (h : InBag L i v) : ∃ B ∈ L, v ∈ B := by
  obtain ⟨B, hB, hv⟩ := h
  exact ⟨B, List.mem_of_getElem? hB, hv⟩

theorem inBag_of_mem {L : List Bag} {B : Bag} {v : Nat} (hB : B ∈ L) (hv : v ∈ B) :
    ∃ i, InBag L i v := by
  obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.1 hB
  exact ⟨i, _, List.getElem?_eq_getElem hi, hv⟩

theorem inBag_full {L : List Bag} {v : Nat} (h : ∀ B ∈ L, v ∈ B) {j : Nat}
    (hj : j < L.length) : InBag L j v :=
  ⟨L[j], List.getElem?_eq_getElem hj, h _ (List.getElem_mem hj)⟩

theorem inBag_cons_succ (B : Bag) (L : List Bag) (i v : Nat) :
    InBag (B :: L) (i + 1) v ↔ InBag L i v := Iff.rfl

theorem inBag_cons_zero (B : Bag) (L : List Bag) (v : Nat) :
    InBag (B :: L) 0 v ↔ v ∈ B := by
  unfold InBag
  simp

theorem inBag_map (f : Bag → Bag) (L : List Bag) (v : Nat)
    (h : ∀ B ∈ L, (v ∈ f B ↔ v ∈ B)) (i : Nat) :
    InBag (L.map f) i v ↔ InBag L i v := by
  unfold InBag
  rw [List.getElem?_map]
  cases hL : L[i]? with
  | none => simp
  | some B =>
    have hB : B ∈ L := List.mem_of_getElem? hL
    simp only [Option.map_some, Option.some.injEq, exists_eq_left']
    exact h B hB

theorem convL_nil (v : Nat) : ConvL [] v := by
  intro i j k _ _ hi _
  exact absurd (inBag_lt hi) (by simp)

theorem convL_free {L : List Bag} {v : Nat} (h : ∀ B ∈ L, v ∉ B) : ConvL L v := by
  intro i j k _ _ hi _
  obtain ⟨B, hB, hv⟩ := inBag_mem hi
  exact absurd hv (h B hB)

theorem convL_full {L : List Bag} {v : Nat} (h : ∀ B ∈ L, v ∈ B) : ConvL L v := by
  intro i j k _ hjk _ hk
  exact inBag_full h (Nat.lt_of_le_of_lt hjk (inBag_lt hk))

theorem convL_of_cons {B : Bag} {L : List Bag} {v : Nat} (h : ConvL (B :: L) v) :
    ConvL L v := by
  intro i j k hij hjk hi hk
  have := h (i + 1) (j + 1) (k + 1) (by omega) (by omega)
    ((inBag_cons_succ B L i v).2 hi) ((inBag_cons_succ B L k v).2 hk)
  exact (inBag_cons_succ B L j v).1 this

/-- Touching concatenation: if one side is free of `v`, or the left side ends with a bag
containing `v` and the right side starts with one, the concatenation is convex. -/
theorem convL_append {X Y : List Bag} {v : Nat} (hX : ConvL X v) (hY : ConvL Y v)
    (h : (∀ B ∈ X, v ∉ B) ∨ (∀ B ∈ Y, v ∉ B) ∨
      (InBag X (X.length - 1) v ∧ InBag Y 0 v)) :
    ConvL (X ++ Y) v := by
  intro i j k hij hjk hi hk
  rw [inBag_append] at hi hk ⊢
  rcases hi with ⟨hin, hi⟩ | ⟨hin, hi⟩ <;> rcases hk with ⟨hkn, hk⟩ | ⟨hkn, hk⟩
  · -- i, k in X
    exact Or.inl ⟨by omega, hX i j k hij hjk hi hk⟩
  · -- i in X, k in Y: the touching cases
    rcases h with h | h | ⟨hlast, hhead⟩
    · obtain ⟨B, hB, hv⟩ := inBag_mem hi
      exact absurd hv (h B hB)
    · obtain ⟨B, hB, hv⟩ := inBag_mem hk
      exact absurd hv (h B hB)
    · by_cases hjn : j < X.length
      · exact Or.inl ⟨hjn, hX i j (X.length - 1) hij (by omega) hi hlast⟩
      · exact Or.inr ⟨by omega, hY 0 (j - X.length) (k - X.length) (Nat.zero_le _)
          (by omega) hhead hk⟩
  · -- i in Y, k in X: impossible since i ≤ k
    omega
  · -- both in Y
    exact Or.inr ⟨by omega, hY (i - X.length) (j - X.length) (k - X.length)
      (by omega) (by omega) hi hk⟩

/-- Mapping bags by `f` preserves convexity when `f` preserves membership of `v`. -/
theorem convL_map {L : List Bag} {v : Nat} (f : Bag → Bag)
    (h : ∀ B ∈ L, (v ∈ f B ↔ v ∈ B)) (hL : ConvL L v) : ConvL (L.map f) v := by
  intro i j k hij hjk hi hk
  have hi' := (inBag_map f L v h i).1 hi
  have hk' := (inBag_map f L v h k).1 hk
  exact (inBag_map f L v h j).2 (hL i j k hij hjk hi' hk')

/-! ## 2. Block structure of `undoF`

`plans` is the list of plans `(S, P, flag, idx)`, one per component. The bags of
`undoF` before the final `++ D` are `outFrom plans 0 bagsR ++ tailOf plans`. -/

/-- A plan `(S, P, flag, idx)` of `undoF`. -/
abbrev Plan := List Nat × List Bag × Bool × Option Nat

/-- The inserted copies `P_bag ∪ B` for the plans attached at index `k`. -/
def copies (plans : List Plan) (k : Nat) (B : Bag) : List Bag :=
  plans.flatMap fun ⟨_, P, _, idx⟩ => if idx == some k then P.map (bagUnion · B) else []

/-- Block `k` of `undo`: the bag `B = bagsR[k]`, followed by its inserted copies. -/
def blk (plans : List Plan) (k : Nat) (B : Bag) : List Bag := B :: copies plans k B

/-- The blocks of `bs` read from index `k` on (`out` of `undoF`). -/
def outFrom (plans : List Plan) : Nat → List Bag → List Bag
  | _, [] => []
  | k, B :: bs => blk plans k B ++ outFrom plans (k + 1) bs

/-- The tail: the bags `P` of the plans with `S = []`. -/
def tailOf (plans : List Plan) : List Bag :=
  plans.flatMap fun ⟨S, P, _, _⟩ => if S.isEmpty then P else []

theorem copies_append (X Y : List Plan) (k : Nat) (B : Bag) :
    copies (X ++ Y) k B = copies X k B ++ copies Y k B := by
  unfold copies
  rw [List.flatMap_append]

theorem copies_cons (p : Plan) (Y : List Plan) (k : Nat) (B : Bag) :
    copies (p :: Y) k B = copies [p] k B ++ copies Y k B := by
  rw [← copies_append]; rfl

theorem tailOf_append (X Y : List Plan) :
    tailOf (X ++ Y) = tailOf X ++ tailOf Y := by
  unfold tailOf
  rw [List.flatMap_append]

theorem mem_copies {plans : List Plan} {k : Nat} {B X : Bag} :
    X ∈ copies plans k B ↔ ∃ p ∈ plans, p.2.2.2 = some k ∧ ∃ Y ∈ p.2.1, X = Y ++ B := by
  unfold copies
  rw [List.mem_flatMap]
  constructor
  · rintro ⟨⟨S, P, f, idx⟩, hp, hX⟩
    dsimp only at hX
    by_cases hidx : (idx == some k) = true
    · rw [if_pos hidx] at hX
      obtain ⟨Y, hY, rfl⟩ := List.mem_map.1 hX
      exact ⟨(S, P, f, idx), hp, beq_iff_eq.1 hidx, Y, hY, rfl⟩
    · rw [if_neg hidx] at hX
      exact absurd hX (List.not_mem_nil)
  · rintro ⟨⟨S, P, f, idx⟩, hp, hidx, Y, hY, rfl⟩
    refine ⟨(S, P, f, idx), hp, ?_⟩
    have hidx' : (idx == some k) = true := beq_iff_eq.2 hidx
    dsimp only
    rw [if_pos hidx']
    exact List.mem_map.2 ⟨Y, hY, rfl⟩

theorem mem_tailOf {plans : List Plan} {Y : Bag} :
    Y ∈ tailOf plans ↔ ∃ p ∈ plans, p.1.isEmpty = true ∧ Y ∈ p.2.1 := by
  unfold tailOf
  rw [List.mem_flatMap]
  constructor
  · rintro ⟨⟨S, P, f, idx⟩, hp, hY⟩
    dsimp only at hY
    by_cases hS : S.isEmpty = true
    · rw [if_pos hS] at hY
      exact ⟨(S, P, f, idx), hp, hS, hY⟩
    · rw [if_neg hS] at hY
      exact absurd hY (List.not_mem_nil)
  · rintro ⟨⟨S, P, f, idx⟩, hp, hS, hY⟩
    refine ⟨(S, P, f, idx), hp, ?_⟩
    dsimp only at hS hY ⊢
    rw [if_pos hS]
    exact hY

theorem mem_outFrom_of_mem (plans : List Plan) :
    ∀ (bs : List Bag) (k : Nat) (B : Bag), B ∈ bs → B ∈ outFrom plans k bs
  | [], _, _, h => by simp at h
  | B' :: bs, k, B, h => by
    rcases List.mem_cons.1 h with rfl | h
    · show B ∈ blk plans k B ++ outFrom plans (k + 1) bs
      exact List.mem_append_left _ (List.mem_cons_self)
    · show B ∈ blk plans k B' ++ outFrom plans (k + 1) bs
      exact List.mem_append_right _ (mem_outFrom_of_mem plans bs (k + 1) B h)

/-- Copies at the position `k + j` of a bag `B` of `bs` lie in `outFrom plans k bs`. -/
theorem copies_sub_outFrom (plans : List Plan) :
    ∀ (bs : List Bag) (k j : Nat) (B X : Bag), bs[j]? = some B →
      X ∈ copies plans (k + j) B → X ∈ outFrom plans k bs
  | [], _, _, _, _, hj, _ => by simp at hj
  | B' :: bs, k, j, B, X, hj, hX => by
    cases j with
    | zero =>
      have hB : B' = B := by
        simpa using hj
      subst hB
      show X ∈ blk plans k B' ++ outFrom plans (k + 1) bs
      apply List.mem_append_left
      exact List.mem_cons_of_mem _ (by simpa using hX)
    | succ j =>
      show X ∈ blk plans k B' ++ outFrom plans (k + 1) bs
      apply List.mem_append_right
      have hX' : X ∈ copies plans ((k + 1) + j) B := by
        have : k + 1 + j = k + (j + 1) := by omega
        rw [this]; exact hX
      exact copies_sub_outFrom plans bs (k + 1) j B X (by simpa using hj) hX'

/-- The bags `out` of `undoF`, as written in the code (a `zipIdx` flatMap). -/
theorem zipIdx_outFrom (plans : List Plan) :
    ∀ (bs : List Bag) (k : Nat),
      (bs.zipIdx k).flatMap (fun ⟨B, i⟩ =>
        B :: plans.flatMap fun ⟨_, P, _, idx⟩ => if idx == some i then P.map (bagUnion · B) else [])
        = outFrom plans k bs
  | [], _ => by simp [outFrom]
  | B :: bs, k => by
    rw [List.zipIdx_cons, List.flatMap_cons, outFrom]
    congr 1
    exact zipIdx_outFrom plans bs (k + 1)

/-! ## 3. Index convexity of the block structure -/

theorem copies_vf {plans : List Plan} {v k : Nat} {B : Bag}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) (hB : v ∉ B) :
    ∀ X ∈ copies plans k B, v ∉ X := by
  intro X hX
  obtain ⟨p, hp, _, Y, hY, rfl⟩ := mem_copies.1 hX
  intro h
  rcases List.mem_append.1 h with h | h
  · exact hP p hp Y hY h
  · exact hB h

/-- Inside a block, every bag contains `v` iff the bag `B` does (when no plan bag has `v`). -/
theorem blk_uniform {plans : List Plan} {v : Nat}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) (k : Nat) (B : Bag) :
    ∀ X ∈ blk plans k B, (v ∈ X ↔ v ∈ B) := by
  intro X hX
  unfold blk at hX
  rcases List.mem_cons.1 hX with rfl | hX
  · exact Iff.rfl
  · obtain ⟨p, hp, _, Y, hY, rfl⟩ := mem_copies.1 hX
    constructor
    · intro h
      rcases List.mem_append.1 h with h | h
      · exact absurd h (hP p hp Y hY)
      · exact h
    · intro h
      exact List.mem_append.2 (Or.inr h)

theorem exists_mem_of_outFrom {plans : List Plan} {v : Nat}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) :
    ∀ (bs : List Bag) (k : Nat) (X : Bag), X ∈ outFrom plans k bs → v ∈ X →
      ∃ B ∈ bs, v ∈ B
  | [], _, X, hX, _ => by simp [outFrom] at hX
  | B :: bs, k, X, hX, hv => by
    have hX' : X ∈ blk plans k B ++ outFrom plans (k + 1) bs := hX
    rcases List.mem_append.1 hX' with h | h
    · exact ⟨B, List.mem_cons_self, (blk_uniform hP k B X h).1 hv⟩
    · obtain ⟨B', hB', hv'⟩ := exists_mem_of_outFrom hP bs (k + 1) X h hv
      exact ⟨B', List.mem_cons_of_mem _ hB', hv'⟩

theorem inBag_zero_outFrom (plans : List Plan) (v : Nat) :
    ∀ (bs : List Bag) (k : Nat), InBag bs 0 v → InBag (outFrom plans k bs) 0 v
  | [], _, h => absurd (inBag_lt h) (by simp)
  | B :: bs, k, h => by
    have hv : v ∈ B := (inBag_cons_zero B bs v).1 h
    show InBag (blk plans k B ++ outFrom plans (k + 1) bs) 0 v
    unfold blk
    rw [List.cons_append]
    exact (inBag_cons_zero _ _ v).2 hv

/-- Index convexity of the `R`-part: if `bs` is convex for `v` and no plan bag contains
`v`, then so are its blocks. -/
theorem convL_outFrom_R {plans : List Plan} {v : Nat}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) :
    ∀ (bs : List Bag) (k : Nat), ConvL bs v → ConvL (outFrom plans k bs) v
  | [], _, _ => by simpa [outFrom] using convL_nil v
  | B :: bs, k, hconv => by
    show ConvL (blk plans k B ++ outFrom plans (k + 1) bs) v
    have hbs : ConvL bs v := convL_of_cons hconv
    have hY : ConvL (outFrom plans (k + 1) bs) v := convL_outFrom_R hP bs (k + 1) hbs
    by_cases hB : v ∈ B
    · have hfull : ∀ X ∈ blk plans k B, v ∈ X := fun X hX => (blk_uniform hP k B X hX).2 hB
      by_cases hYv : ∃ X ∈ outFrom plans (k + 1) bs, v ∈ X
      · obtain ⟨X, hX, hvX⟩ := hYv
        obtain ⟨B0, hB0, hv0⟩ := exists_mem_of_outFrom hP bs (k + 1) X hX hvX
        obtain ⟨m, hm⟩ := inBag_of_mem hB0 hv0
        have h0 : InBag (B :: bs) 0 v := (inBag_cons_zero B bs v).2 hB
        have h1 : InBag (B :: bs) (m + 1) v := (inBag_cons_succ B bs m v).2 hm
        have h10 : InBag (B :: bs) 1 v := hconv 0 1 (m + 1) (by omega) (by omega) h0 h1
        have hbs0 : InBag bs 0 v := h10
        exact convL_append (convL_full hfull) hY
          (Or.inr (Or.inr ⟨by
              have : (blk plans k B).length - 1 < (blk plans k B).length := by
                unfold blk; simp
              exact inBag_full hfull this, inBag_zero_outFrom plans v bs (k + 1) hbs0⟩))
      · exact convL_append (convL_full hfull) hY
          (Or.inr (Or.inl (fun X hX hvX => hYv ⟨X, hX, hvX⟩)))
    · have hfree : ∀ X ∈ blk plans k B, v ∉ X := fun X hX h => hB ((blk_uniform hP k B X hX).1 h)
      exact convL_append (convL_free hfree) hY (Or.inl hfree)

theorem vf_outFrom_of_gt {plans : List Plan} {v k0 : Nat}
    (hV : ∀ k B, k ≠ k0 → v ∉ B → ∀ X ∈ blk plans k B, v ∉ X) :
    ∀ (bs : List Bag) (k : Nat), k0 < k → (∀ B ∈ bs, v ∉ B) →
      ∀ X ∈ outFrom plans k bs, v ∉ X
  | [], _, _, _, X, hX => by simp [outFrom] at hX
  | B :: bs, k, hk, hB, X, hX => by
    have hX' : X ∈ blk plans k B ++ outFrom plans (k + 1) bs := hX
    rcases List.mem_append.1 hX' with h | h
    · exact hV k B (by omega) (hB B List.mem_cons_self) X h
    · exact vf_outFrom_of_gt hV bs (k + 1) (by omega)
        (fun B' hB' => hB B' (List.mem_cons_of_mem _ hB')) X h

/-- Index convexity of the blocks when a single block index `k0` may contain `v`. -/
theorem convL_outFrom_C {plans : List Plan} {v k0 : Nat}
    (hV : ∀ k B, k ≠ k0 → v ∉ B → ∀ X ∈ blk plans k B, v ∉ X)
    (hP : ∀ B, v ∉ B → ConvL (blk plans k0 B) v) :
    ∀ (bs : List Bag) (k : Nat), (∀ B ∈ bs, v ∉ B) → ConvL (outFrom plans k bs) v
  | [], _, _ => by simpa [outFrom] using convL_nil v
  | B :: bs, k, hB => by
    have hbs : ∀ B' ∈ bs, v ∉ B' := fun B' h => hB B' (List.mem_cons_of_mem _ h)
    have hBv : v ∉ B := hB B List.mem_cons_self
    show ConvL (blk plans k B ++ outFrom plans (k + 1) bs) v
    by_cases hk : k = k0
    · subst hk
      have hY := vf_outFrom_of_gt hV bs (k + 1) (by omega) hbs
      exact convL_append (hP B hBv) (convL_free hY) (Or.inr (Or.inl hY))
    · have hXv := hV k B hk hBv
      exact convL_append (convL_free hXv) (convL_outFrom_C hV hP bs (k + 1) hbs) (Or.inl hXv)

theorem copies_single_pos {p : Plan} {k : Nat} {B : Bag} (h : p.2.2.2 = some k) :
    copies [p] k B = p.2.1.map (bagUnion · B) := by
  obtain ⟨S, P, f, idx⟩ := p
  dsimp only at h
  subst h
  unfold copies
  simp

theorem copies_single_neg {p : Plan} {k : Nat} {B : Bag} (h : p.2.2.2 ≠ some k) :
    copies [p] k B = [] := by
  obtain ⟨S, P, f, idx⟩ := p
  dsimp only at h
  have hne : (idx == some k) = false := by
    rw [beq_eq_false_iff_ne]; exact h
  have hne' : ¬ ((idx == some k) = true) := by rw [hne]; decide
  unfold copies
  rw [List.flatMap_cons, List.flatMap_nil, List.append_nil]
  dsimp only
  rw [if_neg hne']

/-- Blocks of a plan list `pre ++ p0 :: post` where the plan bags of `pre` and `post` avoid
`v`, `p0` is convex for `v`, and `p0` is attached only at `k0`. -/
theorem pivot_blocks {pre post : List Plan} {p0 : Plan} {v k0 : Nat}
    (hpre : ∀ p ∈ pre ++ post, ∀ Y ∈ p.2.1, v ∉ Y) (hP0 : ConvL p0.2.1 v)
    (hidx : ∀ k', p0.2.2.2 = some k' → k' = k0) :
    (∀ k B, k ≠ k0 → v ∉ B → ∀ X ∈ blk (pre ++ p0 :: post) k B, v ∉ X) ∧
    (∀ B, v ∉ B → ConvL (blk (pre ++ p0 :: post) k0 B) v) := by
  have hpreV : ∀ p ∈ pre, ∀ Y ∈ p.2.1, v ∉ Y := fun p hp => hpre p (List.mem_append_left _ hp)
  have hpostV : ∀ p ∈ post, ∀ Y ∈ p.2.1, v ∉ Y :=
    fun p hp => hpre p (List.mem_append_right _ hp)
  -- decomposition of a block of the concatenated plan list
  have hdec : ∀ k B, blk (pre ++ p0 :: post) k B
      = ([B] ++ copies pre k B) ++ (copies [p0] k B ++ copies post k B) := by
    intro k B
    unfold blk
    rw [copies_append, copies_cons]
    simp only [List.cons_append, List.nil_append]
  constructor
  · intro k B hk hB X hX
    have hnp : p0.2.2.2 ≠ some k := fun h => hk (hidx k h)
    rw [hdec] at hX
    rcases List.mem_append.1 hX with h | h
    · rcases List.mem_append.1 h with h | h
      · rw [List.mem_singleton.1 h]; exact hB
      · exact copies_vf hpreV hB X h
    · rw [copies_single_neg hnp, List.nil_append] at h
      exact copies_vf hpostV hB X h
  · intro B hB
    by_cases hp0 : p0.2.2.2 = some k0
    · have hMid : ConvL (copies [p0] k0 B) v := by
        rw [copies_single_pos hp0]
        exact convL_map (bagUnion · B)
          (fun Y _ => by
            simp only [bagUnion, List.mem_append]
            exact ⟨fun h => h.elim id (fun h' => absurd h' hB), Or.inl⟩)
          hP0
      have hpostX : ∀ X ∈ copies post k0 B, v ∉ X := copies_vf hpostV hB
      have hpreX : ∀ X ∈ copies pre k0 B, v ∉ X := copies_vf hpreV hB
      have hXfree : ∀ X ∈ [B] ++ copies pre k0 B, v ∉ X := by
        intro X hX
        rcases List.mem_append.1 hX with h | h
        · rw [List.mem_singleton.1 h]; exact hB
        · exact hpreX X h
      have hYc : ConvL (copies [p0] k0 B ++ copies post k0 B) v :=
        convL_append hMid (convL_free hpostX) (Or.inr (Or.inl hpostX))
      rw [hdec]
      exact convL_append (convL_free hXfree) hYc (Or.inl hXfree)
    · rw [hdec, copies_single_neg hp0, List.nil_append]
      apply convL_free
      intro X hX
      rcases List.mem_append.1 hX with h | h
      · rcases List.mem_append.1 h with h | h
        · rw [List.mem_singleton.1 h]; exact hB
        · exact copies_vf hpreV hB X h
      · exact copies_vf hpostV hB X h

/-- The tail of a plan list: bags of the plans with `S = []`. -/
theorem tailOf_vf {plans : List Plan} {v : Nat}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) : ∀ Y ∈ tailOf plans, v ∉ Y := by
  intro Y hY
  obtain ⟨p, hp, _, hYp⟩ := mem_tailOf.1 hY
  exact hP p hp Y hYp

/-! ## 4. Per-vertex claims -/

theorem blk_split (pre post : List Plan) (p0 : Plan) (k : Nat) (B : Bag) :
    blk (pre ++ p0 :: post) k B
      = ([B] ++ copies pre k B) ++ (copies [p0] k B ++ copies post k B) := by
  unfold blk
  rw [copies_append, copies_cons]
  simp only [List.cons_append, List.nil_append]

/-- Blocks at an index where `p0` is not attached avoid `v`. -/
theorem blk_vf_of_ne {pre post : List Plan} {p0 : Plan} {v k : Nat} {B : Bag}
    (hpre : ∀ p ∈ pre ++ post, ∀ Y ∈ p.2.1, v ∉ Y) (hnp : p0.2.2.2 ≠ some k) (hB : v ∉ B) :
    ∀ X ∈ blk (pre ++ p0 :: post) k B, v ∉ X := by
  have hpreV : ∀ p ∈ pre, ∀ Y ∈ p.2.1, v ∉ Y := fun p hp => hpre p (List.mem_append_left _ hp)
  have hpostV : ∀ p ∈ post, ∀ Y ∈ p.2.1, v ∉ Y :=
    fun p hp => hpre p (List.mem_append_right _ hp)
  intro X hX
  rw [blk_split, copies_single_neg hnp, List.nil_append] at hX
  rcases List.mem_append.1 hX with h | h
  · rcases List.mem_append.1 h with h | h
    · rw [List.mem_singleton.1 h]; exact hB
    · exact copies_vf hpreV hB X h
  · exact copies_vf hpostV hB X h

theorem tailOf_single_nil {p0 : Plan} (h : p0.1 = []) : tailOf [p0] = p0.2.1 := by
  obtain ⟨S, P, f, idx⟩ := p0
  dsimp only at h
  subst h
  unfold tailOf
  simp

theorem tailOf_single_ne {p0 : Plan} (h : p0.1 ≠ []) : tailOf [p0] = [] := by
  obtain ⟨S, P, f, idx⟩ := p0
  dsimp only at h
  cases S with
  | nil => exact absurd rfl h
  | cons a S' => unfold tailOf; simp

theorem tailOf_vf_ne {pre post : List Plan} {p0 : Plan} {v : Nat}
    (hpre : ∀ p ∈ pre ++ post, ∀ Y ∈ p.2.1, v ∉ Y) (hS : p0.1 ≠ []) :
    ∀ Y ∈ tailOf (pre ++ p0 :: post), v ∉ Y := by
  intro Y hY
  obtain ⟨p, hp, hem, hYp⟩ := mem_tailOf.1 hY
  rcases List.mem_append.1 hp with h | h
  · exact hpre p (List.mem_append_left _ h) Y hYp
  · rcases List.mem_cons.1 h with rfl | h
    · exact absurd (List.isEmpty_iff.1 hem) hS
    · exact hpre p (List.mem_append_right _ h) Y hYp

theorem vf_outFrom_all {plans : List Plan} {v : Nat}
    (hV : ∀ k B, v ∉ B → ∀ X ∈ blk plans k B, v ∉ X) :
    ∀ (bs : List Bag) (k : Nat), (∀ B ∈ bs, v ∉ B) → ∀ X ∈ outFrom plans k bs, v ∉ X
  | [], _, _, X, hX => by simp [outFrom] at hX
  | B :: bs, k, hB, X, hX => by
    have hX' : X ∈ blk plans k B ++ outFrom plans (k + 1) bs := hX
    rcases List.mem_append.1 hX' with h | h
    · exact hV k B (hB B List.mem_cons_self) X h
    · exact vf_outFrom_all hV bs (k + 1)
        (fun B' hB' => hB B' (List.mem_cons_of_mem _ hB')) X h

/-- The per-vertex claim for a vertex `v` of a component with plan `p0`, inserted in the
middle of the plans `pre ++ p0 :: post`: convexity of the bags and coverage with the
bags of `P0` (each bag of `P0` lies in a bag of the output, extended by the attachment). -/
theorem vertex_C {pre post : List Plan} {p0 : Plan} {v : Nat} {bagsR : List Bag}
    (hpre : ∀ p ∈ pre ++ post, ∀ Y ∈ p.2.1, v ∉ Y)
    (hP0 : ConvL p0.2.1 v) (hB : ∀ B ∈ bagsR, v ∉ B)
    (hS0 : (p0.1 = [] → p0.2.2.2 = none) ∧
      (p0.1 ≠ [] → ∃ i Bi, p0.2.2.2 = some i ∧ bagsR[i]? = some Bi ∧ ∀ x ∈ p0.1, x ∈ Bi)) :
    ConvL (outFrom (pre ++ p0 :: post) 0 bagsR ++ tailOf (pre ++ p0 :: post)) v ∧
    ∀ B0 ∈ p0.2.1, ∃ B ∈ outFrom (pre ++ p0 :: post) 0 bagsR ++ tailOf (pre ++ p0 :: post),
      (∀ x ∈ B0, x ∈ B) ∧ (∀ x ∈ p0.1, x ∈ B) := by
  have hpreV : ∀ p ∈ pre, ∀ Y ∈ p.2.1, v ∉ Y := fun p hp => hpre p (List.mem_append_left _ hp)
  have hpostV : ∀ p ∈ post, ∀ Y ∈ p.2.1, v ∉ Y :=
    fun p hp => hpre p (List.mem_append_right _ hp)
  by_cases hS : p0.1 = []
  · -- no attachment: the plan is in the tail, the blocks avoid `v`
    have hnone : p0.2.2.2 = none := hS0.1 hS
    have hVall : ∀ k B, v ∉ B → ∀ X ∈ blk (pre ++ p0 :: post) k B, v ∉ X :=
      fun k B hB' => blk_vf_of_ne hpre (by rw [hnone]; simp) hB'
    have hOutVF := vf_outFrom_all hVall bagsR 0 hB
    have hPre : ∀ Y ∈ tailOf pre, v ∉ Y := by
      intro Y hY
      obtain ⟨p, hp, _, hYp⟩ := mem_tailOf.1 hY
      exact hpre p (List.mem_append_left _ hp) Y hYp
    have hPost : ∀ Y ∈ tailOf post, v ∉ Y := by
      intro Y hY
      obtain ⟨p, hp, _, hYp⟩ := mem_tailOf.1 hY
      exact hpre p (List.mem_append_right _ hp) Y hYp
    have hTail : tailOf (pre ++ p0 :: post) = tailOf pre ++ (p0.2.1 ++ tailOf post) := by
      have h1 : p0 :: post = [p0] ++ post := rfl
      rw [h1, tailOf_append, tailOf_append, tailOf_single_nil hS]
    have hTailConv : ConvL (tailOf (pre ++ p0 :: post)) v := by
      rw [hTail]
      exact convL_append (convL_free hPre)
        (convL_append hP0 (convL_free hPost) (Or.inr (Or.inl hPost))) (Or.inl hPre)
    refine ⟨convL_append (convL_free hOutVF) hTailConv (Or.inl hOutVF), ?_⟩
    intro B0 hB0
    refine ⟨B0, List.mem_append_right _ ?_, fun x hx => hx, fun x hx => ?_⟩
    · rw [hTail]; exact List.mem_append_right _ (List.mem_append_left _ hB0)
    · rw [hS] at hx; exact absurd hx (List.not_mem_nil)
  · -- attached at `i`: the plan's bags go into the block of `bagsR[i]`
    obtain ⟨i, Bi, hi, hBi, hsub⟩ := hS0.2 hS
    have hidx : ∀ k', p0.2.2.2 = some k' → k' = i :=
      fun k' h => (Option.some.inj (hi.symm.trans h)).symm
    obtain ⟨hV, hPb⟩ := pivot_blocks hpre hP0 hidx
    have hOutConv : ConvL (outFrom (pre ++ p0 :: post) 0 bagsR) v :=
      convL_outFrom_C hV hPb bagsR 0 hB
    have hTailVF := tailOf_vf_ne hpre hS
    refine ⟨convL_append hOutConv (convL_free hTailVF) (Or.inr (Or.inl hTailVF)), ?_⟩
    intro B0 hB0
    have hX : B0 ++ Bi ∈ copies (pre ++ p0 :: post) (0 + i) Bi := by
      rw [Nat.zero_add]
      exact mem_copies.2 ⟨p0, List.mem_append_right _ List.mem_cons_self, hi, B0, hB0, rfl⟩
    have hX' : B0 ++ Bi ∈ outFrom (pre ++ p0 :: post) 0 bagsR :=
      copies_sub_outFrom (pre ++ p0 :: post) bagsR 0 i Bi (B0 ++ Bi) hBi hX
    refine ⟨B0 ++ Bi, List.mem_append_left _ hX', fun x hx => List.mem_append_left _ hx,
      fun x hx => List.mem_append_right _ (hsub x hx)⟩

/-- The per-vertex claim for an `R`-vertex. -/
theorem vertex_R {plans : List Plan} {bagsR : List Bag} {v : Nat}
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, v ∉ Y) (hconv : ConvL bagsR v) :
    ConvL (outFrom plans 0 bagsR ++ tailOf plans) v :=
  convL_append (convL_outFrom_R hP bagsR 0 hconv) (convL_free (tailOf_vf hP))
    (Or.inr (Or.inl (tailOf_vf hP)))

theorem outFrom_within {G : Graph} (plans : List Plan)
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, ∀ x ∈ Y, x ∈ G.nodes) :
    ∀ (bs : List Bag) (k : Nat), (∀ B ∈ bs, ∀ x ∈ B, x ∈ G.nodes) →
      ∀ X ∈ outFrom plans k bs, ∀ x ∈ X, x ∈ G.nodes
  | [], _, _, X, hX => by simp [outFrom] at hX
  | B :: bs, k, hbs, X, hX => by
    have hX' : X ∈ blk plans k B ++ outFrom plans (k + 1) bs := hX
    rcases List.mem_append.1 hX' with h | h
    · unfold blk at h
      rcases List.mem_cons.1 h with rfl | h
      · exact hbs X List.mem_cons_self
      · obtain ⟨p, hp, _, Y, hY, rfl⟩ := mem_copies.1 h
        intro x hx
        rcases List.mem_append.1 hx with hx | hx
        · exact hP p hp Y hY x hx
        · exact hbs B List.mem_cons_self x hx
    · exact outFrom_within plans hP bs (k + 1)
        (fun B' hB' => hbs B' (List.mem_cons_of_mem _ hB')) X h

theorem tailOf_within {G : Graph} (plans : List Plan)
    (hP : ∀ p ∈ plans, ∀ Y ∈ p.2.1, ∀ x ∈ Y, x ∈ G.nodes) :
    ∀ Y ∈ tailOf plans, ∀ x ∈ Y, x ∈ G.nodes := by
  intro Y hY
  obtain ⟨p, hp, _, hYp⟩ := mem_tailOf.1 hY
  exact hP p hp Y hYp

/-! ## 5. The attachment sets and the components of the rest -/

theorem mem_foldl_nbrs (Q : Nat → Bool) (x : Nat) : ∀ (l acc : List Nat),
    x ∈ l.foldl (fun acc y => if Q y || acc.contains y then acc else acc ++ [y]) acc ↔
      x ∈ acc ∨ (x ∈ l ∧ Q x = false)
  | [], acc => by simp
  | y :: l, acc => by
    have key : x ∈ (if Q y || acc.contains y then acc else acc ++ [y]) ↔
        x ∈ acc ∨ (x = y ∧ Q x = false) := by
      by_cases h : (Q y || acc.contains y) = true
      · rw [if_pos h]
        constructor
        · intro hx; exact Or.inl hx
        · rintro (hx | ⟨rfl, hQ⟩)
          · exact hx
          · simp [hQ] at h
            exact h
      · rw [if_neg h]
        have hQy : Q y = false := by
          cases hq : Q y
          · rfl
          · exact absurd (by simp [hq]) h
        constructor
        · intro hx
          rcases List.mem_append.1 hx with hx | hx
          · exact Or.inl hx
          · rw [List.mem_singleton] at hx
            subst hx
            exact Or.inr ⟨rfl, hQy⟩
        · rintro (hx | ⟨rfl, _⟩)
          · exact List.mem_append_left _ hx
          · exact List.mem_append_right _ List.mem_cons_self
    rw [List.foldl_cons, mem_foldl_nbrs Q x l, key]
    simp only [List.mem_cons]
    tauto

theorem mem_foldl_outer (Q : Nat → Bool) (G : Nat → List Nat) (x : Nat) :
    ∀ (C acc : List Nat),
      x ∈ C.foldl (fun acc c => (G c).foldl
        (fun acc y => if Q y || acc.contains y then acc else acc ++ [y]) acc) acc ↔
        x ∈ acc ∨ ∃ c ∈ C, x ∈ G c ∧ Q x = false
  | [], acc => by simp
  | c :: C, acc => by
    rw [List.foldl_cons, mem_foldl_outer Q G x C, mem_foldl_nbrs Q x (G c) acc]
    simp only [List.mem_cons]
    constructor
    · rintro ((hx | ⟨hx, hQ⟩) | ⟨c', hc', hx, hQ⟩)
      · exact Or.inl hx
      · exact Or.inr ⟨c, Or.inl rfl, hx, hQ⟩
      · exact Or.inr ⟨c', Or.inr hc', hx, hQ⟩
    · rintro (hx | ⟨c', hc', hx, hQ⟩)
      · exact Or.inl (Or.inl hx)
      · rcases hc' with rfl | hc'
        · exact Or.inl (Or.inr ⟨hx, hQ⟩)
        · exact Or.inr ⟨c', hc', hx, hQ⟩

/-- Membership in the attachment set: a neighbour of the component, outside the component and
outside the deleted set. -/
theorem mem_undoAttach (F : Graph) (D C : List Nat) (x : Nat) :
    x ∈ undoAttach F D C ↔ (∃ c ∈ C, x ∈ F.nbrs c) ∧ x ∉ C ∧ x ∉ D := by
  unfold undoAttach
  rw [mem_foldl_outer]
  simp only [List.not_mem_nil, false_or]
  constructor
  · rintro ⟨c, hc, hx, hQ⟩
    have h1 : x ∉ C ∧ x ∉ D := by
      simp only [Bool.or_eq_false_iff] at hQ
      exact ⟨by simpa using hQ.1, by simpa using hQ.2⟩
    exact ⟨⟨c, hc, hx⟩, h1⟩
  · rintro ⟨⟨c, hc, hx⟩, h1, h2⟩
    refine ⟨c, hc, hx, ?_⟩
    simp only [Bool.or_eq_false_iff]
    exact ⟨by simpa using h1, by simpa using h2⟩

/-- The rest graph: the induced subgraph on the vertices outside `D` and outside `R`. -/
def restG (F R : Graph) (D : List Nat) : Graph :=
  F.induced fun v => !D.contains v && !R.mem v

theorem keep_true_iff {R : Graph} (hR : R.WF) (D : List Nat) (x : Nat) :
    (!D.contains x && !R.mem x) = true ↔ x ∉ D ∧ x ∉ R.nodes := by
  rw [← hR.mem_iff x]
  simp

theorem mem_restG {F R : Graph} {D : List Nat} (hInd : InducedSpec) (hF : F.WF) (hR : R.WF)
    (x : Nat) : x ∈ (restG F R D).nodes ↔ x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes := by
  have h := (hInd F (fun v => !D.contains v && !R.mem v) hF).2.1 x
  constructor
  · intro hx
    obtain ⟨hF', hk⟩ := h.1 hx
    exact ⟨hF', ((keep_true_iff hR D x).1 hk).1, ((keep_true_iff hR D x).1 hk).2⟩
  · rintro ⟨hF', hD, hRx⟩
    exact h.2 ⟨hF', (keep_true_iff hR D x).2 ⟨hD, hRx⟩⟩

/-- Facts about the components of the rest graph, in the form used by `undoF`. -/
theorem restG_components_facts {F R : Graph} {D : List Nat} (hInd : InducedSpec)
    (hComp : ComponentsSpec) (hF : F.WF) (hR : R.WF) :
    (∀ C ∈ (restG F R D).components, ∀ x ∈ C, x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes) ∧
    (∀ x ∈ F.nodes, x ∈ D ∨ x ∈ R.nodes ∨ ∃ C ∈ (restG F R D).components, x ∈ C) ∧
    (restG F R D).components.flatten.Nodup ∧
    (∀ C ∈ (restG F R D).components, ∀ x ∈ C, ∀ y, F.Adj x y →
      y ∈ C ∨ y ∈ D ∨ y ∈ R.nodes) := by
  have hWF : (restG F R D).WF := (hInd F (fun v => !D.contains v && !R.mem v) hF).1
  obtain ⟨hperm, _, hclos⟩ := hComp (restG F R D) hWF
  have hmem : ∀ x, x ∈ (restG F R D).components.flatten ↔ x ∈ (restG F R D).nodes :=
    fun x => hperm.mem_iff
  have hA : ∀ C ∈ (restG F R D).components, ∀ x ∈ C, x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes := by
    intro C hC x hx
    exact (mem_restG hInd hF hR x).1 ((hmem x).1 (List.mem_flatten.2 ⟨C, hC, hx⟩))
  refine ⟨hA, ?_, ?_, ?_⟩
  · intro x hx
    by_cases hD : x ∈ D
    · exact Or.inl hD
    by_cases hRx : x ∈ R.nodes
    · exact Or.inr (Or.inl hRx)
    right; right
    have hxr : x ∈ (restG F R D).nodes := (mem_restG hInd hF hR x).2 ⟨hx, hD, hRx⟩
    obtain ⟨z, hz, hxz⟩ := List.mem_flatten.1 ((hmem x).2 hxr)
    exact ⟨z, hz, hxz⟩
  · exact (hperm.nodup_iff).2 hWF.nodup
  · intro C hC x hx y hxy
    by_cases hyD : y ∈ D
    · exact Or.inr (Or.inl hyD)
    by_cases hyR : y ∈ R.nodes
    · exact Or.inr (Or.inr hyR)
    have hxN := (mem_restG hInd hF hR x).1 ((hmem x).1 (List.mem_flatten.2 ⟨C, hC, hx⟩))
    have hyN : y ∈ (restG F R D).nodes :=
      (mem_restG hInd hF hR y).2 ⟨hF.nbrs_sub x y hxy, hyD, hyR⟩
    have hW := (hInd F (fun v => !D.contains v && !R.mem v) hF).2.2 x y
    have hadj : (restG F R D).Adj x y :=
      hW.2 ⟨hxy, (keep_true_iff hR D x).2 ⟨hxN.2.1, hxN.2.2⟩,
        (keep_true_iff hR D y).2 ⟨hyD, hyR⟩⟩
    exact Or.inl (hclos C hC x hx y hadj)

/-! ## 6. The plans of `undoF` and the output bags -/

/-- The plan of a component `C`: the body of the `map` in `undoF`. -/
def planOf (F : Graph) (D : List Nat) (bagsR : List Bag) (C : List Nat) : Plan :=
  (undoAttach F D C, (pdTw2F (F.induced C.contains)).1, (pdTw2F (F.induced C.contains)).2,
    if (undoAttach F D C).isEmpty then none
    else bagsR.findIdx? (subsetB (undoAttach F D C) ·))

/-- The output of `undoF` from the bags `L` (before the flag): `L ∪ D` bagwise, or `[D]`. -/
def resOf (D : List Nat) (L : List Bag) : List Bag :=
  if (L.map fun B => bagUnion B D).isEmpty then [D] else L.map fun B => bagUnion B D

theorem induced_mem_iff {F : Graph} (hInd : InducedSpec) (hF : F.WF) (C : List Nat) (x : Nat) :
    x ∈ (F.induced C.contains).nodes ↔ x ∈ F.nodes ∧ x ∈ C := by
  rw [(hInd F C.contains hF).2.1 x]
  simp

theorem induced_adj_iff {F : Graph} (hInd : InducedSpec) (hF : F.WF) (C : List Nat) (x y : Nat) :
    (F.induced C.contains).Adj x y ↔ F.Adj x y ∧ x ∈ C ∧ y ∈ C := by
  rw [(hInd F C.contains hF).2.2 x y]
  simp

/-- Two different components are disjoint: from `nodup` of the flattened list. -/
theorem disj_of_nodup_split {s t : List (List Nat)} {C0 : List Nat}
    (h : (s ++ C0 :: t).flatten.Nodup) :
    ∀ C' ∈ s ++ t, ∀ x ∈ C0, x ∉ C' := by
  have h' : (s.flatten ++ (C0 ++ t.flatten)).Nodup := by
    simpa [List.flatten_append] using h
  rw [List.nodup_append] at h'
  have h'' := List.nodup_append.1 h'.2.1
  intro C' hC' x hx hxC'
  rcases List.mem_append.1 hC' with hC' | hC'
  · exact h'.2.2 x (List.mem_flatten.2 ⟨C', hC', hxC'⟩) x (List.mem_append_left _ hx) rfl
  · exact h''.2.2 x hx x (List.mem_flatten.2 ⟨C', hC', hxC'⟩) rfl

/-- Facts about the bags of the `undoF` plans, given the component facts. -/
theorem plan_bags_in_comp {F : Graph} {D : List Nat} {bagsR : List Bag}
    {comps : List (List Nat)} (hInd : InducedSpec) (hF : F.WF)
    (hP : ∀ C ∈ comps, ValidPD (F.induced C.contains) (planOf F D bagsR C).2.1 ∧
      BagsWithin (F.induced C.contains) (planOf F D bagsR C).2.1) :
    ∀ C ∈ comps, ∀ Y ∈ (planOf F D bagsR C).2.1, ∀ x ∈ Y, x ∈ F.nodes ∧ x ∈ C := by
  intro C hC Y hY x hx
  have hB := (hP C hC).2 Y hY x hx
  exact (induced_mem_iff hInd hF C x).1 hB

theorem resOf_contains {D : List Nat} {L : List Bag} {X : Bag} (hX : X ∈ resOf D L) :
    ∀ x ∈ D, x ∈ X := by
  intro x hx
  unfold resOf at hX
  split at hX
  · rw [List.mem_singleton.1 hX]; exact hx
  · obtain ⟨B, _, rfl⟩ := List.mem_map.1 hX
    exact List.mem_append_right _ hx

theorem resOf_within {F : Graph} {D : List Nat} {L : List Bag} (hDF : ∀ x ∈ D, x ∈ F.nodes)
    (hL : ∀ B ∈ L, ∀ x ∈ B, x ∈ F.nodes) :
    ∀ X ∈ resOf D L, ∀ x ∈ X, x ∈ F.nodes := by
  intro X hX x hx
  unfold resOf at hX
  split at hX
  · rw [List.mem_singleton.1 hX] at hx; exact hDF x hx
  · obtain ⟨B, hB, rfl⟩ := List.mem_map.1 hX
    rcases List.mem_append.1 hx with hx | hx
    · exact hL B hB x hx
    · exact hDF x hx

theorem resOf_ne_nil_of_mem {D : List Nat} {L : List Bag} {B : Bag} (hB : B ∈ L) :
    ∃ X ∈ resOf D L, ∀ x ∈ B, x ∈ X := by
  refine ⟨bagUnion B D, ?_, fun x hx => List.mem_append_left _ hx⟩
  unfold resOf
  split
  · rename_i h
    exfalso
    obtain ⟨c, hc⟩ : ∃ c, c = B := ⟨B, rfl⟩
    simp only [List.isEmpty_iff, List.map_eq_nil_iff] at h
    subst h
    exact absurd hB (List.not_mem_nil)
  · exact List.mem_map.2 ⟨B, hB, rfl⟩

/-! ## 7. Assembly for the main branch -/

/-- The bags of `undoF` before the final `∪ D` (the list `out ++ tail` of the code). -/
def bags0Of (F : Graph) (D : List Nat) (bagsR : List Bag) (comps : List (List Nat)) :
    List Bag :=
  outFrom (comps.map (planOf F D bagsR)) 0 bagsR ++ tailOf (comps.map (planOf F D bagsR))

theorem bags0Of_split (F : Graph) (D : List Nat) (bagsR : List Bag) {comps : List (List Nat)}
    {s t : List (List Nat)} {C0 : List Nat} (hst : comps = s ++ C0 :: t) :
    bags0Of F D bagsR comps =
      outFrom (s.map (planOf F D bagsR) ++ planOf F D bagsR C0 :: t.map (planOf F D bagsR)) 0
          bagsR ++
        tailOf (s.map (planOf F D bagsR) ++ planOf F D bagsR C0 :: t.map (planOf F D bagsR)) := by
  unfold bags0Of
  rw [hst, List.map_append, List.map_cons]

theorem resOf_ne_nil (D : List Nat) (L : List Bag) : resOf D L ≠ [] := by
  unfold resOf
  split
  · exact List.cons_ne_nil _ _
  · rename_i h
    intro h'
    apply h
    simp [h']

theorem resOf_eq_map (D : List Nat) {L : List Bag} (hL : L ≠ []) :
    resOf D L = L.map fun B => bagUnion B D := by
  unfold resOf
  split
  · rename_i h
    exfalso
    apply hL
    simpa [List.isEmpty_iff, List.map_eq_nil_iff] using h
  · rfl

/-- Facts about the vertices of one component `C0` of the rest. -/
theorem comp_V {F R : Graph} {D : List Nat} {bagsR : List Bag} {comps : List (List Nat)}
    (hInd : InducedSpec) (hF : F.WF)
    (hBR : BagsWithin R bagsR)
    (hcomp_mem : ∀ C ∈ comps, ∀ x ∈ C, x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes)
    (hdisj : comps.flatten.Nodup)
    (hclos : ∀ C ∈ comps, ∀ x ∈ C, ∀ y, F.Adj x y → y ∈ C ∨ y ∈ D ∨ y ∈ R.nodes)
    (hP : ∀ C ∈ comps, ValidPD (F.induced C.contains) (planOf F D bagsR C).2.1 ∧
      BagsWithin (F.induced C.contains) (planOf F D bagsR C).2.1)
    (hok : ∀ C ∈ comps, (∀ x ∈ undoAttach F D C, x ∈ R.nodes) ∧
      (undoAttach F D C ≠ [] → ∃ i Bi, (planOf F D bagsR C).2.2.2 = some i ∧
        bagsR[i]? = some Bi ∧ ∀ x ∈ undoAttach F D C, x ∈ Bi))
    {C0 : List Nat} (hC0 : C0 ∈ comps) :
    (∀ v ∈ C0, ConvL (bags0Of F D bagsR comps) v) ∧
    (∀ v ∈ C0, ∃ B ∈ bags0Of F D bagsR comps, v ∈ B) ∧
    (∀ u ∈ C0, ∀ y, F.Adj u y → y ∉ D → ∃ B ∈ bags0Of F D bagsR comps, u ∈ B ∧ y ∈ B) := by
  obtain ⟨s, t, hst⟩ := List.append_of_mem hC0
  have hdec := bags0Of_split F D bagsR hst
  have hdisj' : (s ++ C0 :: t).flatten.Nodup := hst ▸ hdisj
  have hdisjC := disj_of_nodup_split hdisj'
  have hPlanC := plan_bags_in_comp hInd hF hP
  -- the plans of the other components avoid the vertices of `C0`
  have hpre : ∀ v ∈ C0, ∀ p ∈ s.map (planOf F D bagsR) ++ t.map (planOf F D bagsR),
      ∀ Y ∈ p.2.1, v ∉ Y := by
    intro v hv p hp Y hY hvY
    obtain ⟨C', hC', rfl⟩ : ∃ C' ∈ s ++ t, planOf F D bagsR C' = p := by
      rcases List.mem_append.1 hp with hp | hp
      · obtain ⟨C', hC', rfl⟩ := List.mem_map.1 hp
        exact ⟨C', List.mem_append_left _ hC', rfl⟩
      · obtain ⟨C', hC', rfl⟩ := List.mem_map.1 hp
        exact ⟨C', List.mem_append_right _ hC', rfl⟩
    have hC'comps : C' ∈ comps := by
      rw [hst]
      rcases List.mem_append.1 hC' with h | h
      · exact List.mem_append_left _ h
      · exact List.mem_append_right _ (List.mem_cons_of_mem _ h)
    have hvC' := (hPlanC C' hC'comps Y hY v hvY).2
    exact hdisjC C' hC' v hv hvC'
  have hS0 : ((planOf F D bagsR C0).1 = [] → (planOf F D bagsR C0).2.2.2 = none) ∧
      ((planOf F D bagsR C0).1 ≠ [] → ∃ i Bi, (planOf F D bagsR C0).2.2.2 = some i ∧
        bagsR[i]? = some Bi ∧ ∀ x ∈ (planOf F D bagsR C0).1, x ∈ Bi) := by
    refine ⟨fun h => ?_, fun h => ?_⟩
    · have h' : undoAttach F D C0 = [] := h
      simp [planOf, h']
    · exact (hok C0 hC0).2 h
  have key : ∀ v ∈ C0, ConvL (bags0Of F D bagsR comps) v ∧
      ∀ B0 ∈ (planOf F D bagsR C0).2.1, ∃ B ∈ bags0Of F D bagsR comps,
        (∀ x ∈ B0, x ∈ B) ∧ (∀ x ∈ undoAttach F D C0, x ∈ B) := by
    intro v hv
    have hvF : v ∈ (F.induced C0.contains).nodes :=
      (induced_mem_iff hInd hF C0 v).2 ⟨(hcomp_mem C0 hC0 v hv).1, hv⟩
    have hP0 : ConvL (planOf F D bagsR C0).2.1 v := (hP C0 hC0).1.2.1 v hvF
    have hB : ∀ B ∈ bagsR, v ∉ B := fun B hB hvB =>
      (hcomp_mem C0 hC0 v hv).2.2 (hBR B hB v hvB)
    have hVC := vertex_C (pre := s.map (planOf F D bagsR))
      (post := t.map (planOf F D bagsR)) (p0 := planOf F D bagsR C0) (hpre v hv) hP0 hB hS0
    rw [hdec]
    exact ⟨hVC.1, hVC.2⟩
  refine ⟨fun v hv => (key v hv).1, fun v hv => ?_, fun u hu y hadj hyD => ?_⟩
  · have hvF : v ∈ (F.induced C0.contains).nodes :=
      (induced_mem_iff hInd hF C0 v).2 ⟨(hcomp_mem C0 hC0 v hv).1, hv⟩
    obtain ⟨i, hi⟩ := (hP C0 hC0).1.1 v hvF
    obtain ⟨B0, hB0, hvB0⟩ := inBag_mem hi
    obtain ⟨B, hB, hsub, _⟩ := (key v hv).2 B0 hB0
    exact ⟨B, hB, hsub v hvB0⟩
  · have huF : u ∈ (F.induced C0.contains).nodes :=
      (induced_mem_iff hInd hF C0 u).2 ⟨(hcomp_mem C0 hC0 u hu).1, hu⟩
    rcases hclos C0 hC0 u hu y hadj with hyC | hyD' | hyR
    · have hadjI : (F.induced C0.contains).Adj u y :=
        (induced_adj_iff hInd hF C0 u y).2 ⟨hadj, hu, hyC⟩
      obtain ⟨B0, hB0, huB0, hyB0⟩ := (hP C0 hC0).1.2.2 u y huF hadjI
      obtain ⟨B, hB, hsub, _⟩ := (key u hu).2 B0 hB0
      exact ⟨B, hB, hsub u huB0, hsub y hyB0⟩
    · exact absurd hyD' hyD
    · have hyC0 : y ∉ C0 := fun hyC => (hcomp_mem C0 hC0 y hyC).2.2 hyR
      have hyS : y ∈ undoAttach F D C0 :=
        (mem_undoAttach F D C0 y).2 ⟨⟨u, hu, hadj⟩, hyC0, hyD⟩
      obtain ⟨i, hi⟩ := (hP C0 hC0).1.1 u huF
      obtain ⟨B0, hB0, huB0⟩ := inBag_mem hi
      obtain ⟨B, hB, hsub, hsubS⟩ := (key u hu).2 B0 hB0
      exact ⟨B, hB, hsub u huB0, hsubS y hyS⟩

/-- Facts about the vertices of `R`. -/
theorem R_V {F R : Graph} {D : List Nat} {bagsR : List Bag} {comps : List (List Nat)}
    (hInd : InducedSpec) (hF : F.WF)
    (hVR : ValidPD R bagsR)
    (hRadj : ∀ x y, x ∈ R.nodes → y ∈ R.nodes → F.Adj x y → R.Adj x y)
    (hcomp_mem : ∀ C ∈ comps, ∀ x ∈ C, x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes)
    (hP : ∀ C ∈ comps, ValidPD (F.induced C.contains) (planOf F D bagsR C).2.1 ∧
      BagsWithin (F.induced C.contains) (planOf F D bagsR C).2.1) :
    (∀ v ∈ R.nodes, ConvL (bags0Of F D bagsR comps) v) ∧
    (∀ v ∈ R.nodes, ∃ B ∈ bags0Of F D bagsR comps, v ∈ B) ∧
    (∀ u v, u ∈ R.nodes → v ∈ R.nodes → F.Adj u v →
      ∃ B ∈ bags0Of F D bagsR comps, u ∈ B ∧ v ∈ B) := by
  have hPlanC := plan_bags_in_comp hInd hF hP
  have hPl : ∀ v ∈ R.nodes, ∀ p ∈ comps.map (planOf F D bagsR), ∀ Y ∈ p.2.1, v ∉ Y := by
    intro v hv p hp Y hY hvY
    obtain ⟨C, hC, rfl⟩ := List.mem_map.1 hp
    exact (hcomp_mem C hC v (hPlanC C hC Y hY v hvY).2).2.2 hv
  refine ⟨fun v hv => ?_, fun v hv => ?_, fun u v hu hv hadj => ?_⟩
  · unfold bags0Of
    exact vertex_R (hPl v hv) (hVR.2.1 v hv)
  · obtain ⟨i, hi⟩ := hVR.1 v hv
    obtain ⟨B, hB, hvB⟩ := inBag_mem hi
    exact ⟨B, List.mem_append_left _ (mem_outFrom_of_mem _ bagsR 0 B hB), hvB⟩
  · obtain ⟨B, hB, huB, hvB⟩ := hVR.2.2 u v hu (hRadj u v hu hv hadj)
    exact ⟨B, List.mem_append_left _ (mem_outFrom_of_mem _ bagsR 0 B hB), huB, hvB⟩

/-! ## 8. The main branch of `undoF` -/

theorem core_valid {F R : Graph} {D : List Nat} {bagsR : List Bag} {comps : List (List Nat)}
    (hInd : InducedSpec) (hF : F.WF)
    (hVR : ValidPD R bagsR) (hBR : BagsWithin R bagsR)
    (hRadj : ∀ x y, x ∈ R.nodes → y ∈ R.nodes → F.Adj x y → R.Adj x y)
    (hRsub : ∀ x ∈ R.nodes, x ∈ F.nodes)
    (hcomp_mem : ∀ C ∈ comps, ∀ x ∈ C, x ∈ F.nodes ∧ x ∉ D ∧ x ∉ R.nodes)
    (hcov : ∀ x ∈ F.nodes, x ∈ D ∨ x ∈ R.nodes ∨ ∃ C ∈ comps, x ∈ C)
    (hdisj : comps.flatten.Nodup)
    (hclos : ∀ C ∈ comps, ∀ x ∈ C, ∀ y, F.Adj x y → y ∈ C ∨ y ∈ D ∨ y ∈ R.nodes)
    (hP : ∀ C ∈ comps, ValidPD (F.induced C.contains) (planOf F D bagsR C).2.1 ∧
      BagsWithin (F.induced C.contains) (planOf F D bagsR C).2.1)
    (hok : ∀ C ∈ comps, (∀ x ∈ undoAttach F D C, x ∈ R.nodes) ∧
      (undoAttach F D C ≠ [] → ∃ i Bi, (planOf F D bagsR C).2.2.2 = some i ∧
        bagsR[i]? = some Bi ∧ ∀ x ∈ undoAttach F D C, x ∈ Bi)) :
    ValidPD F (resOf D (bags0Of F D bagsR comps)) ∧
      ((∀ x ∈ D, x ∈ F.nodes) → BagsWithin F (resOf D (bags0Of F D bagsR comps))) := by
  have hCV : ∀ C0 ∈ comps, (∀ v ∈ C0, ConvL (bags0Of F D bagsR comps) v) ∧
      (∀ v ∈ C0, ∃ B ∈ bags0Of F D bagsR comps, v ∈ B) ∧
      (∀ u ∈ C0, ∀ y, F.Adj u y → y ∉ D → ∃ B ∈ bags0Of F D bagsR comps, u ∈ B ∧ y ∈ B) :=
    fun C0 hC0 => comp_V hInd hF hBR hcomp_mem hdisj hclos hP hok hC0
  have hRV := R_V hInd hF hVR hRadj hcomp_mem hP
  have hPF : ∀ p ∈ comps.map (planOf F D bagsR), ∀ Y ∈ p.2.1, ∀ x ∈ Y, x ∈ F.nodes := by
    intro p hp Y hY x hx
    obtain ⟨C, hC, rfl⟩ := List.mem_map.1 hp
    exact (plan_bags_in_comp hInd hF hP C hC Y hY x hx).1
  have hbagsF : ∀ B ∈ bags0Of F D bagsR comps, ∀ x ∈ B, x ∈ F.nodes := by
    intro B hB x hx
    unfold bags0Of at hB
    rcases List.mem_append.1 hB with hB | hB
    · exact outFrom_within (G := F) _ hPF bagsR 0
        (fun B' hB' x' hx' => hRsub x' (hBR B' hB' x' hx')) B hB x hx
    · exact tailOf_within (G := F) _ hPF B hB x hx
  -- every vertex of `F` outside `D` is covered, convex, and each edge is covered
  have hV1 : ∀ v ∈ F.nodes, v ∉ D → ∃ B ∈ bags0Of F D bagsR comps, v ∈ B := by
    intro v hv hvD
    rcases hcov v hv with h | h | ⟨C0, hC0, hvC0⟩
    · exact absurd h hvD
    · exact hRV.2.1 v h
    · exact (hCV C0 hC0).2.1 v hvC0
  have hV2 : ∀ v ∈ F.nodes, v ∉ D → ConvL (bags0Of F D bagsR comps) v := by
    intro v hv hvD
    rcases hcov v hv with h | h | ⟨C0, hC0, hvC0⟩
    · exact absurd h hvD
    · exact hRV.1 v h
    · exact (hCV C0 hC0).1 v hvC0
  have hV3 : ∀ u v, u ∈ F.nodes → v ∈ F.nodes → u ∉ D → v ∉ D → F.Adj u v →
      ∃ B ∈ bags0Of F D bagsR comps, u ∈ B ∧ v ∈ B := by
    intro u v hu hv huD hvD hadj
    rcases hcov u hu with h | h | ⟨C0, hC0, huC0⟩
    · exact absurd h huD
    · rcases hcov v hv with h' | h' | ⟨C1, hC1, hvC1⟩
      · exact absurd h' hvD
      · exact hRV.2.2 u v h h' hadj
      · obtain ⟨B, hB, hvB, huB⟩ := (hCV C1 hC1).2.2 v hvC1 u (hF.symm u v hadj) huD
        exact ⟨B, hB, huB, hvB⟩
    · exact (hCV C0 hC0).2.2 u huC0 v hadj hvD
  have hcovRes : ∀ v ∈ F.nodes, ∃ X ∈ resOf D (bags0Of F D bagsR comps), v ∈ X := by
    intro v hv
    by_cases hvD : v ∈ D
    · obtain ⟨X, hX⟩ := List.exists_mem_of_ne_nil _ (resOf_ne_nil D (bags0Of F D bagsR comps))
      exact ⟨X, hX, resOf_contains hX v hvD⟩
    · obtain ⟨B, hB, hvB⟩ := hV1 v hv hvD
      obtain ⟨X, hX, hBX⟩ := resOf_ne_nil_of_mem (D := D) hB
      exact ⟨X, hX, hBX v hvB⟩
  have hValid : ValidPD F (resOf D (bags0Of F D bagsR comps)) := by
    refine ⟨fun v hv => ?_, fun v hv => ?_, fun u v hu hadj => ?_⟩
    · obtain ⟨X, hX, hvX⟩ := hcovRes v hv
      exact inBag_of_mem hX hvX
    · by_cases hvD : v ∈ D
      · exact convL_full (fun X hX => resOf_contains hX v hvD)
      · obtain ⟨B, hB, _⟩ := hV1 v hv hvD
        have hne : bags0Of F D bagsR comps ≠ [] := fun h => by simp [h] at hB
        have hconvRes : ConvL (resOf D (bags0Of F D bagsR comps)) v := by
          rw [resOf_eq_map D hne]
          exact convL_map _ (fun B' _ => by
            simp only [bagUnion, List.mem_append]
            exact ⟨fun h => h.elim id (fun h' => absurd h' hvD), Or.inl⟩)
            (hV2 v hv hvD)
        exact hconvRes
    · have hvF : v ∈ F.nodes := hF.nbrs_sub u v hadj
      by_cases huD : u ∈ D
      · obtain ⟨X, hX, hvX⟩ := hcovRes v hvF
        exact ⟨X, hX, resOf_contains hX u huD, hvX⟩
      by_cases hvD : v ∈ D
      · obtain ⟨X, hX, huX⟩ := hcovRes u hu
        exact ⟨X, hX, huX, resOf_contains hX v hvD⟩
      · obtain ⟨B, hB, huB, hvB⟩ := hV3 u v hu hvF huD hvD hadj
        obtain ⟨X, hX, hBX⟩ := resOf_ne_nil_of_mem (D := D) hB
        exact ⟨X, hX, hBX u huB, hBX v hvB⟩
  refine ⟨hValid, fun hDF => ?_⟩
  exact fun X hX x hx => resOf_within hDF hbagsF X hX x hx

/-! ## 9. Fallback, plan extraction, and the main theorem -/

theorem fallback_valid {F : Graph} (hF : F.WF) :
    ValidPD F [F.nodes] ∧ BagsWithin F [F.nodes] := by
  refine ⟨⟨fun v hv => ⟨0, F.nodes, by simp, hv⟩,
    fun v hv => convL_full (fun B hB => by rw [List.mem_singleton.1 hB]; exact hv),
    fun u v hu hadj => ⟨F.nodes, List.mem_singleton.2 rfl, hu,
      hF.nbrs_sub u v hadj⟩⟩, fun B hB x hx => ?_⟩
  rw [List.mem_singleton.1 hB] at hx
  exact hx

/-- The attachment data of a component that passes the check of `undoF`. -/
theorem ok_extract {F R : Graph} {D : List Nat} {bagsR : List Bag} {C : List Nat} (hR : R.WF)
    (h1 : (undoAttach F D C).all R.mem = true)
    (h2 : (undoAttach F D C).isEmpty = true ∨ (planOf F D bagsR C).2.2.2.isSome = true) :
    (∀ x ∈ undoAttach F D C, x ∈ R.nodes) ∧
    (undoAttach F D C ≠ [] → ∃ i Bi, (planOf F D bagsR C).2.2.2 = some i ∧
      bagsR[i]? = some Bi ∧ ∀ x ∈ undoAttach F D C, x ∈ Bi) := by
  refine ⟨fun x hx => (hR.mem_iff x).1 (List.all_eq_true.1 h1 x hx), fun hne => ?_⟩
  have hfalse : (undoAttach F D C).isEmpty = false := by
    simpa [List.isEmpty_iff] using hne
  have hsome : (planOf F D bagsR C).2.2.2.isSome = true := h2.resolve_left (by rw [hfalse]; decide)
  have hidx : (planOf F D bagsR C).2.2.2 = bagsR.findIdx? (subsetB (undoAttach F D C) ·) := by
    simp only [planOf, hfalse]
    simp
  rw [hidx] at hsome ⊢
  obtain ⟨i, hi⟩ := Option.isSome_iff_exists.1 hsome
  rw [hi]
  obtain ⟨hlt, hp, _⟩ := List.findIdx?_eq_some_iff_getElem.1 hi
  refine ⟨i, bagsR[i], rfl, List.getElem?_eq_getElem hlt, fun x hx => ?_⟩
  have hp' : subsetB (undoAttach F D C) bagsR[i] = true := hp
  unfold subsetB at hp'
  exact List.contains_iff_mem.1 (List.all_eq_true.1 hp' x hx)

end C7

open C7

theorem undoValid_of (hWF : WFBasics) (hInd : InducedSpec) (hComp : ComponentsSpec)
    (hPd : PdTw2Valid) : UndoValid := by
  intro F R ops bagsR hF hR hRsub hRadj hVR hBR
  unfold undo
  unfold undoF
  dsimp only
  split
  · exact ⟨(fallback_valid hF).1, fun _ => (fallback_valid hF).2⟩
  · rename_i hnot
    generalize hD : deletedSet ops = D at hRsub hnot ⊢
    simp only [Bool.not_eq_true', Bool.not_eq_false] at hnot
    rw [zipIdx_outFrom]
    obtain ⟨hcomp_mem, hcov, hdisj, hclos⟩ :=
      restG_components_facts (D := D) hInd hComp hF hR
    have hP : ∀ C ∈ (restG F R D).components,
        ValidPD (F.induced C.contains) (planOf F D bagsR C).2.1 ∧
          BagsWithin (F.induced C.contains) (planOf F D bagsR C).2.1 :=
      fun C _ => hPd (F.induced C.contains) ((hInd F C.contains hF).1)
    have hok : ∀ C ∈ (restG F R D).components, (∀ x ∈ undoAttach F D C, x ∈ R.nodes) ∧
        (undoAttach F D C ≠ [] → ∃ i Bi, (planOf F D bagsR C).2.2.2 = some i ∧
          bagsR[i]? = some Bi ∧ ∀ x ∈ undoAttach F D C, x ∈ Bi) := by
      intro C hC
      have h1 := List.all_eq_true.1 hnot (planOf F D bagsR C) (List.mem_map.2 ⟨C, hC, rfl⟩)
      have h2 : (undoAttach F D C).all R.mem = true ∧
          ((undoAttach F D C).isEmpty = true ∨ (planOf F D bagsR C).2.2.2.isSome = true) := by
        simp only [planOf, Bool.and_eq_true, Bool.or_eq_true] at h1
        exact ⟨h1.1.1, h1.2⟩
      exact ok_extract hR h2.1 h2.2
    exact core_valid hInd hF hVR hBR hRadj (fun x hx => (hRsub x hx).1) hcomp_mem hcov hdisj
      hclos hP hok

#print axioms CubicPathwidth.Alg.undoValid_of

end CubicPathwidth.Alg