CubicPathwidth.Alg.Proofs.C3Connector

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

import CubicPathwidth.Alg.Spec

/-!
# C3: `ConnectorOrderMem` (set membership of `connector_order`)

Only membership is proved, so no duplicate-freeness is used.
Structure:
* `greedy_props`: a greedy order of a component `c` contains `c` and only elements of
  `c` or of items (loop invariant `present ⊆ ordRev`, `ordRev ⊆ c ∪ items`, generalised
  over the fuel, stack and state).
* `connDfs_ok`, `connOuter_ok`: the DFS and the outer scan of `connectorComponents`
  produce components inside `Qs` covering `Qs` (the fallback part is the complement of
  the assigned elements, so the cover is complete in every branch).
* `order_mem`: the output is the concatenation of the greedy orders of all components,
  taken along a permutation of the component indices (`mergeSort_perm`).
-/

namespace CubicPathwidth.Alg

namespace C3

/-! ## Basic facts -/

/-- An element of `items.getD k []` lies in some item. -/
theorem mem_getD_items {items : List (List Nat)} {k z : Nat} (h : z ∈ items.getD k []) :
    ∃ e ∈ items, z ∈ e := by
  rw [List.getD_eq_getElem?_getD] at h
  cases hk : items[k]? with
  | none => simp [hk] at h
  | some e =>
    refine ⟨e, List.mem_of_getElem? hk, ?_⟩
    simpa [hk] using h

/-- Every element of a member of `comps.getD i []` lies in `Qs`. -/
theorem comps_getD_sub {Qs : List Nat} {comps : List (List Nat)}
    (hC : ∀ c ∈ comps, ∀ y ∈ c, y ∈ Qs) (i : Nat) : ∀ y ∈ comps.getD i [], y ∈ Qs := by
  intro y hy
  rw [List.getD_eq_getElem?_getD] at hy
  cases hi : comps[i]? with
  | none => simp [hi] at hy
  | some c => exact hC c (List.mem_of_getElem? hi) y (by simpa [hi] using hy)

/-! ## Greedy order (`connectorGreedy`) -/

/-- Loop invariant of `connectorGreedy.loop`, for an arbitrary fuel, stack and state.
The output is `mk P O F` for the final state `(P, O)`; `P ⊆ O`, `O ⊆ c ∪ items`, and
the initial `ordRev` survives in `O`. -/
theorem greedy_loop (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (c : List Nat) (mk : Std.HashSet Nat → List Nat → Bool → List Nat × Bool) :
    ∀ (fuel : Nat) (stack : List Nat) (present : Std.HashSet Nat) (ordRev : List Nat)
      (fl : Bool),
      (∀ z, present.contains z = true → z ∈ ordRev) →
      (∀ z ∈ ordRev, z ∈ c ∨ ∃ e ∈ items, z ∈ e) →
      ∃ P O F, connectorGreedy.loop items inc c mk fuel stack present ordRev fl = mk P O F ∧
        (∀ z, P.contains z = true → z ∈ O) ∧
        (∀ z ∈ O, z ∈ c ∨ ∃ e ∈ items, z ∈ e) ∧
        (∀ z ∈ ordRev, z ∈ O) := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack present ordRev fl hI hJ
    exact ⟨present, ordRev, _, by rw [connectorGreedy.loop.eq_1], hI, hJ, fun z hz => hz⟩
  | succ f ih =>
    intro stack present ordRev fl hI hJ
    cases stack with
    | nil =>
      exact ⟨present, ordRev, _, by rw [connectorGreedy.loop], hI, hJ, fun z hz => hz⟩
    | cons k stack =>
      rw [connectorGreedy.loop]
      split
      · exact ⟨present, ordRev, _, rfl, hI, hJ, fun z hz => hz⟩
      · dsimp only
        split
        · rename_i z hfilt hlen2
          have hzmem : z ∈ items.getD k [] := by
            have : z ∈ (items.getD k []).filter (fun z => !present.contains z) := by
              rw [hfilt]; exact List.mem_singleton_self z
            exact (List.mem_filter.mp this).1
          obtain ⟨e, he, hze⟩ := mem_getD_items hzmem
          obtain ⟨P, O, F, heq, hI', hJ', hO⟩ := ih ((inc.getD z []).reverse ++ stack)
            (present.insert z) (z :: ordRev) fl
            (by
              intro w hw
              rw [Std.HashSet.contains_insert] at hw
              simp only [Bool.or_eq_true, beq_iff_eq] at hw
              rcases hw with rfl | hw
              · exact List.mem_cons_self
              · exact List.mem_cons_of_mem _ (hI w hw))
            (by
              intro w hw
              rcases List.mem_cons.mp hw with rfl | hw
              · exact Or.inr ⟨e, he, hze⟩
              · exact hJ w hw)
          exact ⟨P, O, F, heq, hI', hJ', fun w hw => hO w (List.mem_cons_of_mem _ hw)⟩
        · exact ih stack present ordRev fl hI hJ

/-- Membership facts of the greedy order of one component. -/
theorem greedy_props (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (c : List Nat) :
    (∀ x ∈ c, x ∈ (connectorGreedy items inc c).1) ∧
    (∀ y ∈ (connectorGreedy items inc c).1, y ∈ c ∨ ∃ e ∈ items, y ∈ e) := by
  cases c with
  | nil => simp [connectorGreedy]
  | cons start c' =>
    have key := greedy_loop items inc (start :: c')
      (fun present ordRev fl =>
        (ordRev.reverse ++ (start :: c').filter (fun z => !present.contains z), fl))
      ((items.map List.length).sum + 1) ((inc.getD start []).reverse)
      ((∅ : Std.HashSet Nat).insert start) [start] false
      (by
        intro z hz
        rw [Std.HashSet.contains_insert, Std.HashSet.contains_empty] at hz
        simp only [Bool.or_false, beq_iff_eq] at hz
        simp [hz])
      (by
        intro z hz
        left
        rw [List.mem_singleton] at hz
        simp [hz])
    obtain ⟨P, O, F, heq, hI, hJ, _⟩ := key
    have hres : connectorGreedy items inc (start :: c') =
        (O.reverse ++ (start :: c').filter (fun z => !P.contains z), F) := by
      unfold connectorGreedy
      exact heq
    rw [hres]
    constructor
    · intro x hx
      by_cases hP : P.contains x = true
      · exact List.mem_append_left _ (List.mem_reverse.mpr (hI x hP))
      · exact List.mem_append_right _ (List.mem_filter.mpr ⟨hx, by simpa using hP⟩)
    · intro y hy
      rcases List.mem_append.mp hy with h | h
      · exact hJ y (List.mem_reverse.mp h)
      · exact Or.inl (List.mem_filter.mp h).1

/-! ## Components (`connectorComponents`) -/

/-- Postcondition of the DFS `connDfs` from the start state `(A0, M0)`: old assigned
elements stay assigned; newly assigned elements are recorded in the member list; the old
members are kept; every member lies in `all`. -/
def DfsOK (all : List Nat) (A0 : Std.HashSet Nat) (M0 : List Nat)
    (r : List Nat × Std.HashSet Nat × List Nat) : Prop :=
  (∀ w, A0.contains w = true → r.2.1.contains w = true) ∧
  (∀ w, r.2.1.contains w = true → w ∈ r.2.2 ∨ A0.contains w = true) ∧
  (∀ w ∈ M0, w ∈ r.2.2) ∧
  (∀ w ∈ r.2.2, w ∈ all)

theorem dfsOK_self {all : List Nat} {A : Std.HashSet Nat} {M : List Nat} (stk : List Nat)
    (hM : ∀ w ∈ M, w ∈ all) : DfsOK all A M (stk, A, M) :=
  ⟨fun _ hw => hw, fun _ hw => Or.inr hw, fun _ hw => hw, hM⟩

theorem dfsOK_trans {all : List Nat} {A0 : Std.HashSet Nat} {M0 : List Nat}
    {r1 r2 : List Nat × Std.HashSet Nat × List Nat}
    (h1 : DfsOK all A0 M0 r1) (h2 : DfsOK all r1.2.1 r1.2.2 r2) : DfsOK all A0 M0 r2 := by
  obtain ⟨a1, b1, c1, _⟩ := h1
  obtain ⟨a2, b2, c2, d2⟩ := h2
  refine ⟨fun w hw => a2 w (a1 w hw), fun w hw => ?_, fun w hw => c2 _ (c1 w hw), d2⟩
  rcases b2 w hw with h | h
  · exact Or.inl h
  · rcases b1 w h with h' | h'
    · exact Or.inl (c2 _ h')
    · exact Or.inr h'

/-- One inner fold step of `connDfs` over a list of candidates. -/
theorem fold_inner_ok {all : List Nat} (L : List Nat) (hL : ∀ z ∈ L, z ∈ all) :
    ∀ acc : List Nat × Std.HashSet Nat × List Nat, (∀ w ∈ acc.2.2, w ∈ all) →
      DfsOK all acc.2.1 acc.2.2 (L.foldl (fun (acc : List Nat × Std.HashSet Nat × List Nat)
        (z : Nat) => if acc.2.1.contains z then acc
          else (z :: acc.1, acc.2.1.insert z, z :: acc.2.2)) acc) := by
  induction L with
  | nil =>
    intro acc hM
    exact dfsOK_self _ hM
  | cons z L ih =>
    intro acc hM
    simp only [List.foldl_cons]
    by_cases hz : acc.2.1.contains z = true
    · simp only [hz, ↓reduceIte]
      exact ih (fun z' hz' => hL z' (List.mem_cons_of_mem _ hz')) acc hM
    · simp only [hz, Bool.false_eq_true]
      have hzall : z ∈ all := hL z (List.mem_cons_self)
      have h1 : DfsOK all acc.2.1 acc.2.2 (z :: acc.1, acc.2.1.insert z, z :: acc.2.2) := by
        refine ⟨fun w hw => ?_, fun w hw => ?_, fun w hw => List.mem_cons_of_mem _ hw, ?_⟩
        · rw [Std.HashSet.contains_insert]
          simp [hw]
        · rw [Std.HashSet.contains_insert] at hw
          simp only [Bool.or_eq_true, beq_iff_eq] at hw
          rcases hw with rfl | hw
          · exact Or.inl List.mem_cons_self
          · exact Or.inr hw
        · intro w hw
          rcases List.mem_cons.mp hw with rfl | hw
          · exact hzall
          · exact hM w hw
      have hM' : ∀ w ∈ (z :: acc.1, acc.2.1.insert z, z :: acc.2.2).2.2, w ∈ all := by
        intro w hw
        rcases List.mem_cons.mp hw with rfl | hw
        · exact hzall
        · exact hM w hw
      exact dfsOK_trans h1
        (ih (fun z' hz' => hL z' (List.mem_cons_of_mem _ hz')) _ hM')

/-- Folding over the item indices of `inc.getD y`. -/
theorem fold_items_ok {all : List Nat} (items : List (List Nat))
    (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ all) :
    ∀ (ks : List Nat) (acc : List Nat × Std.HashSet Nat × List Nat),
      (∀ w ∈ acc.2.2, w ∈ all) →
      DfsOK all acc.2.1 acc.2.2 (ks.foldl (fun (acc : List Nat × Std.HashSet Nat × List Nat)
        (k : Nat) => (items.getD k []).foldl (fun (acc : List Nat × Std.HashSet Nat × List Nat)
          (z : Nat) => if acc.2.1.contains z then acc
            else (z :: acc.1, acc.2.1.insert z, z :: acc.2.2)) acc) acc) := by
  intro ks
  induction ks with
  | nil =>
    intro acc hM
    exact dfsOK_self _ hM
  | cons k ks ih =>
    intro acc hM
    simp only [List.foldl_cons]
    have hk : ∀ z ∈ items.getD k [], z ∈ all := by
      intro z hz
      obtain ⟨e, he, hze⟩ := mem_getD_items hz
      exact hitems e he z hze
    have h1 := fold_inner_ok (items.getD k []) hk acc hM
    exact dfsOK_trans h1 (ih _ h1.2.2.2)

/-- `connDfs` is correct for every fuel, stack and start state. -/
theorem connDfs_ok (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (all : List Nat) (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ all) :
    ∀ (fuel : Nat) (stack : List Nat) (A : Std.HashSet Nat) (M : List Nat),
      (∀ w ∈ M, w ∈ all) →
      DfsOK all A M (connectorComponents.connDfs items inc fuel stack A M) := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack A M hM
    rw [connectorComponents.connDfs.eq_1]
    exact dfsOK_self _ hM
  | succ f ih =>
    intro stack A M hM
    cases stack with
    | nil =>
      rw [connectorComponents.connDfs]
      exact dfsOK_self _ hM
    | cons y rest =>
      rw [connectorComponents.connDfs]
      have h1 := fold_items_ok items hitems (inc.getD y []) (rest, A, M) hM
      exact dfsOK_trans h1 (ih _ _ _ h1.2.2.2)

/-- `connOuter` covers the remaining list `qs`, keeps the given components, and every
component lies in `all`. Induction on `qs` for an arbitrary assigned set and component
list; the fallback branch keeps the complement of the assigned elements as last part. -/
theorem connOuter_ok (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (all : List Nat) (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ all) (fuel : Nat) :
    ∀ (qs : List Nat) (A : Std.HashSet Nat) (comps : List (List Nat)),
      (∀ y ∈ qs, y ∈ all) → (∀ c ∈ comps, ∀ y ∈ c, y ∈ all) →
      (∀ y, A.contains y = true → ∃ c ∈ comps, y ∈ c) →
      (∀ c ∈ connectorComponents.connOuter items inc all fuel qs A comps, ∀ y ∈ c, y ∈ all) ∧
      (∀ y ∈ qs, ∃ c ∈ connectorComponents.connOuter items inc all fuel qs A comps, y ∈ c) ∧
      (∀ c ∈ comps, c ∈ connectorComponents.connOuter items inc all fuel qs A comps) := by
  intro qs
  induction qs with
  | nil =>
    intro A comps _ hcomps _
    rw [connectorComponents.connOuter]
    refine ⟨fun c hc y hy => hcomps c (List.mem_reverse.mp hc) y hy,
      fun y hy => by simp at hy, fun c hc => List.mem_reverse.mpr hc⟩
  | cons x qs ih =>
    intro A comps hqs hcomps hA
    have hxall : x ∈ all := hqs x List.mem_cons_self
    have hqs' : ∀ y ∈ qs, y ∈ all := fun y hy => hqs y (List.mem_cons_of_mem _ hy)
    rw [connectorComponents.connOuter.eq_2]
    by_cases hx : A.contains x = true
    · simp only [hx, ↓reduceIte]
      obtain ⟨h1, h2, h3⟩ := ih A comps hqs' hcomps hA
      refine ⟨h1, ?_, h3⟩
      intro y hy
      rcases List.mem_cons.mp hy with rfl | hy
      · obtain ⟨c, hc, hyc⟩ := hA y hx
        exact ⟨c, h3 c hc, hyc⟩
      · exact h2 y hy
    · simp only [hx, Bool.false_eq_true, ↓reduceIte]
      have hr := connDfs_ok items inc all hitems fuel [x] (A.insert x) [x]
        (by intro w hw; rw [List.mem_singleton] at hw; rw [hw]; exact hxall)
      generalize connectorComponents.connDfs items inc fuel [x] (A.insert x) [x] = r at hr ⊢
      obtain ⟨ra, rb, rc, rd⟩ := hr
      have hxr : x ∈ r.2.2 := rc x List.mem_cons_self
      -- every element assigned in `r` lies in one of the new components
      have hcov' : ∀ y, r.2.1.contains y = true →
          ∃ c ∈ (r.2.2.reverse :: comps), y ∈ c := by
        intro y hy
        rcases rb y hy with h | h
        · exact ⟨r.2.2.reverse, List.mem_cons_self, List.mem_reverse.mpr h⟩
        · rw [Std.HashSet.contains_insert] at h
          simp only [Bool.or_eq_true, beq_iff_eq] at h
          rcases h with rfl | h
          · exact ⟨r.2.2.reverse, List.mem_cons_self, List.mem_reverse.mpr hxr⟩
          · obtain ⟨c, hc, hyc⟩ := hA y h
            exact ⟨c, List.mem_cons_of_mem _ hc, hyc⟩
      have hcomps' : ∀ c ∈ (r.2.2.reverse :: comps), ∀ y ∈ c, y ∈ all := by
        intro c hc y hy
        rcases List.mem_cons.mp hc with rfl | hc
        · exact rd y (List.mem_reverse.mp hy)
        · exact hcomps c hc y hy
      by_cases he : r.1.isEmpty = true
      · simp only [he, ↓reduceIte]
        obtain ⟨h1, h2, h3⟩ := ih r.2.1 (r.2.2.reverse :: comps) hqs' hcomps' hcov'
        refine ⟨h1, ?_, fun c hc => h3 c (List.mem_cons_of_mem _ hc)⟩
        intro y hy
        rcases List.mem_cons.mp hy with rfl | hy
        · exact ⟨r.2.2.reverse, h3 _ List.mem_cons_self, List.mem_reverse.mpr hxr⟩
        · exact h2 y hy
      · simp only [he, Bool.false_eq_true, ↓reduceIte]
        generalize hrest : List.filter (fun y => !r.2.1.contains y) all = rest
        have hrest_mem : ∀ y ∈ rest, y ∈ all ∧ r.2.1.contains y = false := by
          intro y hy
          rw [← hrest, List.mem_filter] at hy
          exact ⟨hy.1, by simpa using hy.2⟩
        -- the list of components to return, before reversal
        have hP1 : ∀ c ∈ (r.2.2.reverse :: comps), c ∈ (if rest.isEmpty = true then
            (r.2.2.reverse :: comps) else rest :: (r.2.2.reverse :: comps)) := by
          intro c hc
          split
          · exact hc
          · exact List.mem_cons_of_mem _ hc
        have hP2 : ∀ c ∈ (if rest.isEmpty = true then (r.2.2.reverse :: comps)
            else rest :: (r.2.2.reverse :: comps)), c ∈ (r.2.2.reverse :: comps) ∨ c = rest := by
          intro c hc
          split at hc
          · exact Or.inl hc
          · rcases List.mem_cons.mp hc with h | h
            · exact Or.inr h
            · exact Or.inl h
        have hP3 : rest ≠ [] → rest ∈ (if rest.isEmpty = true then (r.2.2.reverse :: comps)
            else rest :: (r.2.2.reverse :: comps)) := by
          intro hne
          have : ¬ rest.isEmpty = true := by simpa [List.isEmpty_iff] using hne
          simp only [this]
          exact List.mem_cons_self
        refine ⟨?_, ?_, ?_⟩
        · intro c hc y hy
          rw [List.mem_reverse] at hc
          rcases hP2 c hc with h | h
          · exact hcomps' c h y hy
          · subst h
            exact (hrest_mem y hy).1
        · intro y hy
          have hyall := hqs y hy
          by_cases hyA : r.2.1.contains y = true
          · obtain ⟨c, hc, hyc⟩ := hcov' y hyA
            exact ⟨c, List.mem_reverse.mpr (hP1 c hc), hyc⟩
          · have hyr : y ∈ rest := by
              rw [← hrest, List.mem_filter]
              exact ⟨hyall, by simp [hyA]⟩
            exact ⟨rest, List.mem_reverse.mpr (hP3 (List.ne_nil_of_mem hyr)), hyr⟩
        · intro c hc
          rw [List.mem_reverse]
          exact hP1 c (List.mem_cons_of_mem _ hc)

/-- Components lie in `Qs` and cover `Qs` (for `items ⊆ Qs`). -/
theorem components_props (Qs : List Nat) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat)) (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ Qs) :
    (∀ c ∈ connectorComponents Qs items inc, ∀ y ∈ c, y ∈ Qs) ∧
    (∀ x ∈ Qs, ∃ c ∈ connectorComponents Qs items inc, x ∈ c) := by
  have h := connOuter_ok items inc Qs hitems
    (Qs.length + (items.map List.length).sum + 1) Qs ∅ []
    (fun y hy => hy) (fun c hc => by simp at hc) (fun y hy => by simp at hy)
  unfold connectorComponents
  exact ⟨h.1, fun x hx => h.2.1 x hx⟩

/-- The order: a permutation of the component indices, each contributing its greedy
order (membership form). -/
theorem order_mem (Qs : List Nat) (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (comps : List (List Nat)) (hC : ∀ c ∈ comps, ∀ y ∈ c, y ∈ Qs)
    (hcov : ∀ x ∈ Qs, ∃ c ∈ comps, x ∈ c) (hitems : ∀ e ∈ items, ∀ z ∈ e, z ∈ Qs)
    (x : Nat) :
    x ∈ ((((List.range comps.length).zip (connectorExcess items comps)).mergeSort
        (fun a b => decide (a.2 ≤ b.2))).map
          (fun (p : Nat × Int) => connectorGreedy items inc (comps.getD p.1 []))).flatMap
            (fun (g : List Nat × Bool) => g.1) ↔ x ∈ Qs := by
  set exc := connectorExcess items comps with hexc
  set ordered := ((List.range comps.length).zip exc).mergeSort
    (fun a b => decide (a.2 ≤ b.2)) with hordered
  have hlen : exc.length = comps.length := by
    simp [hexc, connectorExcess]
  have hperm : (ordered.map Prod.fst).Perm (List.range comps.length) := by
    have h1 := (List.mergeSort_perm ((List.range comps.length).zip exc)
      (fun a b => decide (a.2 ≤ b.2))).map Prod.fst
    rw [List.map_fst_zip (by simp [hlen])] at h1
    exact h1
  have hmemj : ∀ j ∈ List.range comps.length, ∃ p ∈ ordered, p.1 = j := by
    intro j hj
    have hj' : j ∈ ordered.map Prod.fst := hperm.symm.mem_iff.mp hj
    obtain ⟨p, hp, hpj⟩ := List.mem_map.mp hj'
    exact ⟨p, hp, hpj⟩
  constructor
  · intro hx
    rw [List.mem_flatMap] at hx
    obtain ⟨a, ha, hxa⟩ := hx
    obtain ⟨p, _, rfl⟩ := List.mem_map.mp ha
    rcases (greedy_props items inc (comps.getD p.1 [])).2 x hxa with h | ⟨e, he, hxe⟩
    · exact comps_getD_sub hC p.1 x h
    · exact hitems e he x hxe
  · intro hx
    obtain ⟨c, hc, hxc⟩ := hcov x hx
    obtain ⟨j, hj, hcj⟩ := List.mem_iff_getElem.mp hc
    obtain ⟨p, hp, hpj⟩ := hmemj j (List.mem_range.mpr hj)
    have hgetD : comps.getD p.1 [] = c := by
      rw [hpj, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hj]
      simp [hcj]
    rw [List.mem_flatMap]
    refine ⟨connectorGreedy items inc (comps.getD p.1 []), List.mem_map.mpr ⟨p, hp, rfl⟩, ?_⟩
    rw [hgetD]
    exact (greedy_props items inc c).1 x hxc

end C3

/-- C3: `connector_order` has exactly the elements of `Qs` (for items inside `Qs`). -/
theorem connectorOrderMem : ConnectorOrderMem := by
  unfold ConnectorOrderMem
  intro Qs items hitems x
  have hcp := C3.components_props Qs items (connectorIncidence Qs items) hitems
  unfold connectorOrder connectorOrderF
  exact C3.order_mem Qs items (connectorIncidence Qs items)
    (connectorComponents Qs items (connectorIncidence Qs items)) hcp.1 hcp.2 hitems x

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.connectorOrderMem