import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.C3Connector

/-!
# N1: `ConnectorNoFallback` (Spec.lean §7)

Route (`lem:connector-linear` of the paper, the part that concerns the fallbacks of the port).

1. Incidence (`inc`): `k ∈ inc z ↔ z ∈ items k`, and `(inc z).length = Σ_e count z e`.
2. Components (`connectorComponents`): each component is nodup, has a head `x` and every
   member is reachable from `x` in the item relation `R` (`ReflTransGen`). The DFS never
   runs out of fuel and always ends with an empty stack (potential `|stack| + |unassigned|`
   drops by one per pop).
3. Greedy (`connectorGreedy`): potential `|stack| + Σ_{z ∈ Qs, z ∉ present} |inc z|`
   drops by one per pop and is at most `Σ|items| + 1` initially, so the fuel suffices.
   When the stack is empty, every item with exactly one endpoint in `present` is absent
   from the stack, so `present` is closed under `R`, hence contains the component.
   Then the flag `present.size < c.length` is `false`.

Helpers live in `CubicPathwidth.Alg.N1`.
-/

namespace CubicPathwidth.Alg

namespace N1

/-! ## 1. Incidence -/

/-- One item `e` with index `k` inserted into the incidence map. -/
theorem fold_inner_getD (k : Nat) (e : List Nat) (m : Std.HashMap Nat (List Nat)) (z : Nat) :
    (e.foldl (fun m x => m.insert x (m.getD x [] ++ [k])) m).getD z [] =
      m.getD z [] ++ List.replicate (e.count z) k := by
  induction e generalizing m with
  | nil => simp
  | cons x e ih =>
    rw [List.foldl_cons, ih, Std.HashMap.getD_insert, List.count_cons]
    by_cases hxz : x = z
    · subst hxz
      simp [List.append_assoc, ← List.replicate_succ]
    · have : (x == z) = false := by simpa using hxz
      simp [this]

/-- The fold over the indexed items. -/
theorem fold_items_getD (ps : List (List Nat × Nat)) (m : Std.HashMap Nat (List Nat)) (z : Nat) :
    (ps.foldl (fun m p => p.1.foldl (fun m x => m.insert x (m.getD x [] ++ [p.2])) m) m).getD
        z [] =
      m.getD z [] ++ (ps.map fun p => List.replicate (p.1.count z) p.2).flatten := by
  induction ps generalizing m with
  | nil => simp
  | cons p ps ih =>
    rw [List.foldl_cons, ih, fold_inner_getD, List.map_cons, List.flatten_cons, List.append_assoc]

/-- The incidence lists of `connectorIncidence`. -/
theorem inc_getD (Qs : List Nat) (items : List (List Nat)) (z : Nat) :
    (connectorIncidence Qs items).getD z [] =
      (items.zipIdx.map fun p => List.replicate (p.1.count z) p.2).flatten := by
  unfold connectorIncidence
  rw [fold_items_getD]
  simp

/-- Membership in the incidence lists. -/
theorem mem_inc_iff (Qs : List Nat) (items : List (List Nat)) (k z : Nat) :
    k ∈ (connectorIncidence Qs items).getD z [] ↔ z ∈ items.getD k [] := by
  rw [inc_getD, List.mem_flatten]
  constructor
  · rintro ⟨l, hl, hk⟩
    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hl
    have hpk : p.2 = k := by
      rw [List.mem_replicate] at hk
      exact hk.2.symm
    have hcount : z ∈ p.1 := by
      rw [List.mem_replicate] at hk
      have := hk.1
      exact List.count_pos_iff.mp (Nat.pos_of_ne_zero this)
    have hget : items[k]? = some p.1 := by
      have := (List.mem_zipIdx_iff_getElem?).mp hp
      rw [hpk] at this
      exact this
    rw [List.getD_eq_getElem?_getD, hget]
    simpa using hcount
  · intro hz
    rw [List.getD_eq_getElem?_getD] at hz
    cases hk : items[k]? with
    | none => simp [hk] at hz
    | some e =>
      rw [hk] at hz
      simp only [Option.getD_some] at hz
      refine ⟨List.replicate (e.count z) k, ?_, ?_⟩
      · refine List.mem_map.mpr ⟨(e, k), ?_, ?_⟩
        · exact (List.mem_zipIdx_iff_getElem?).mpr hk
        · rfl
      · rw [List.mem_replicate]
        exact ⟨Nat.pos_iff_ne_zero.mp (List.count_pos_iff.mpr hz), rfl⟩

/-- The length of `inc z` is the number of occurrences of `z` in the items. -/
theorem length_inc (Qs : List Nat) (items : List (List Nat)) (z : Nat) :
    ((connectorIncidence Qs items).getD z []).length = (items.map fun e => e.count z).sum := by
  rw [inc_getD, List.length_flatten]
  simp only [List.map_map, Function.comp_def, List.length_replicate]
  conv_rhs => rw [← List.zipIdx_map_fst 0 items]
  simp only [List.map_map, Function.comp_def]

/-! ## 2. Counting -/

/-- Removing one element of a nodup list from a weighted filter. -/
theorem sum_filter_erase (P : Nat → Bool) (f : Nat → Nat) (z : Nat) :
    ∀ (Qs : List Nat), Qs.Nodup → z ∈ Qs → P z = true →
      ((Qs.filter fun y => P y && y != z).map f).sum + f z = ((Qs.filter P).map f).sum
  | [], _, hz, _ => by simp at hz
  | a :: Qs, hQ, hz, hP => by
    rw [List.nodup_cons] at hQ
    obtain ⟨haQ, hQ'⟩ := hQ
    by_cases haz : a = z
    · subst haz
      have hfilt : Qs.filter (fun y => P y && y != a) = Qs.filter P := by
        apply List.filter_congr
        intro y hy
        have hya : y ≠ a := fun h => haQ (h ▸ hy)
        simp [hya]
      simp [List.filter_cons, hP, hfilt]
      omega
    · have hzQs : z ∈ Qs := by
        rcases List.mem_cons.mp hz with h | h
        · exact absurd h.symm haz
        · exact h
      have ih := sum_filter_erase P f z Qs hQ' hzQs hP
      have hne : (a == z) = false := by simpa using haz
      by_cases hPa : P a = true
      · simp [List.filter_cons, hPa, haz, hne]
        omega
      · have hPa' : P a = false := by simpa using hPa
        simp [List.filter_cons, hPa', ih]

/-- Counting one element of a nodup list. -/
theorem sum_ite_eq_le (x : Nat) : ∀ (L : List Nat), L.Nodup →
    (L.map fun z => if x == z then 1 else 0).sum = if x ∈ L then 1 else 0
  | [], _ => by simp
  | z :: L, hL => by
    rw [List.nodup_cons] at hL
    rw [List.map_cons, List.sum_cons, sum_ite_eq_le x L hL.2]
    by_cases hxz : x = z
    · subst hxz
      have : x ∉ L := hL.1
      simp [this]
    · have : (x == z) = false := by simpa using hxz
      simp [this, hxz]

/-- Occurrences of the elements of a nodup list in `e` are at most the length of `e`. -/
theorem sum_count_le (L : List Nat) (hL : L.Nodup) : ∀ e : List Nat,
    (L.map fun z => e.count z).sum ≤ e.length
  | [] => by simp
  | x :: e => by
    have ih := sum_count_le L hL e
    have hite : (L.map fun z => if x == z then 1 else 0).sum ≤ 1 := by
      rw [sum_ite_eq_le x L hL]
      split <;> omega
    simp only [List.count_cons]
    rw [List.sum_map_add]
    simp only [List.length_cons]
    omega

theorem sum_swap (L : List Nat) : ∀ items : List (List Nat),
    (L.map fun z => (items.map fun e => e.count z).sum).sum =
      (items.map fun e => (L.map fun z => e.count z).sum).sum
  | [] => by simp
  | e :: es => by
    have ih := sum_swap L es
    simp only [List.map_cons, List.sum_cons]
    rw [← ih, ← List.sum_map_add]

theorem sum_map_le (f g : List Nat → Nat) : ∀ items : List (List Nat),
    (∀ e ∈ items, f e ≤ g e) → (items.map f).sum ≤ (items.map g).sum
  | [], _ => by simp
  | e :: es, h => by
    simp only [List.map_cons, List.sum_cons]
    have h1 := h e List.mem_cons_self
    have h2 := sum_map_le f g es (fun e' he' => h e' (List.mem_cons_of_mem _ he'))
    omega

/-- The total size of the incidence lists is at most the total size of the items. -/
theorem total_inc_le (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat)) :
    (Qs.map fun z => ((connectorIncidence Qs items).getD z []).length).sum ≤
      (items.map List.length).sum := by
  simp only [length_inc]
  rw [sum_swap]
  exact sum_map_le _ _ items (fun e _ => sum_count_le Qs hQ e)

/-! ## 3. Components: each one is a nodup, item-connected list with a head -/

/-- Two elements sharing an item. -/
def Rel (items : List (List Nat)) (x y : Nat) : Prop :=
  ∃ k, x ∈ items.getD k [] ∧ y ∈ items.getD k []

/-- A component in the form the greedy and the lemmas below use: head `x`, nodup, every
member in `Qs` and item-reachable from `x`. -/
def Good (Qs : List Nat) (items : List (List Nat)) (c : List Nat) : Prop :=
  ∃ x c', c = x :: c' ∧ c.Nodup ∧ ∀ z ∈ c, z ∈ Qs ∧ Relation.ReflTransGen (Rel items) x z

/-- Invariant of the DFS state `(stack, assigned, memRev)` for the root `x`. -/
def DInv (Qs : List Nat) (items : List (List Nat)) (x : Nat)
    (T : List Nat × Std.HashSet Nat × List Nat) : Prop :=
  (∀ w ∈ T.1, w ∈ T.2.2) ∧ (∀ w ∈ T.2.2, T.2.1.contains w = true) ∧ T.2.2.Nodup ∧
    (∀ w ∈ T.2.2, w ∈ Qs ∧ Relation.ReflTransGen (Rel items) x w)

/-- DFS potential: stack length plus the number of unassigned elements of `Qs`. -/
def Psi (Qs : List Nat) (T : List Nat × Std.HashSet Nat × List Nat) : Nat :=
  T.1.length + (Qs.filter fun y => !T.2.1.contains y).length

theorem filter_insert_length (Qs : List Nat) (hQ : Qs.Nodup) (A : Std.HashSet Nat) (z : Nat)
    (hz : z ∈ Qs) (hA : A.contains z = false) :
    (Qs.filter fun y => !(A.insert z).contains y).length + 1 =
      (Qs.filter fun y => !A.contains y).length := by
  have h := sum_filter_erase (fun y => !A.contains y) (fun _ => 1) z Qs hQ hz (by simp [hA])
  have hf : Qs.filter (fun y => !(A.insert z).contains y) =
      Qs.filter (fun y => (!A.contains y) && y != z) := by
    apply List.filter_congr
    intro y _
    by_cases hyz : y = z
    · subst hyz
      simp [Std.HashSet.contains_insert]
    · have hzy : (z == y) = false := beq_false_of_ne (Ne.symm hyz)
      have hyz' : (y != z) = true := bne_iff_ne.mpr hyz
      rw [Std.HashSet.contains_insert, hzy, hyz']
      simp [Bool.and_comm]
  rw [hf]
  simpa using h

/-- One element pushed by the DFS keeps the invariant. -/
theorem dfs_inner (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat)) (x : Nat) :
    ∀ (L : List Nat), (∀ z ∈ L, z ∈ Qs ∧ Relation.ReflTransGen (Rel items) x z) →
    ∀ T : List Nat × Std.HashSet Nat × List Nat, DInv Qs items x T →
      DInv Qs items x (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)) T) ∧
      Psi Qs (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)) T) =
        Psi Qs T ∧
      ∃ L', (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)) T).2.2 =
          L' ++ T.2.2
  | [], _, T, hT => ⟨hT, rfl, [], by simp⟩
  | z :: L, hL, T, hT => by
    obtain ⟨hz, hzR⟩ := hL z List.mem_cons_self
    simp only [List.foldl_cons]
    by_cases hc : T.2.1.contains z = true
    · have hstep : (if T.2.1.contains z then T
          else (z :: T.1, T.2.1.insert z, z :: T.2.2)) = T := by simp [hc]
      rw [hstep]
      exact dfs_inner Qs hQ items x L (fun w hw => hL w (List.mem_cons_of_mem _ hw)) T hT
    · have hc' : T.2.1.contains z = false := by simpa using hc
      have hstep : (if T.2.1.contains z then T
          else (z :: T.1, T.2.1.insert z, z :: T.2.2)) =
          (z :: T.1, T.2.1.insert z, z :: T.2.2) := by simp [hc']
      rw [hstep]
      have hzM : z ∉ T.2.2 := by
        intro h
        have := hT.2.1 z h
        rw [hc'] at this
        exact Bool.false_ne_true this
      have hT' : DInv Qs items x (z :: T.1, T.2.1.insert z, z :: T.2.2) := by
        refine ⟨fun w hw => ?_, fun w hw => ?_, ?_, ?_⟩
        · rcases List.mem_cons.mp hw with rfl | hw
          · exact List.mem_cons_self
          · exact List.mem_cons_of_mem _ (hT.1 w hw)
        · rcases List.mem_cons.mp hw with rfl | hw
          · simp [Std.HashSet.contains_insert]
          · rw [Std.HashSet.contains_insert]
            simp [hT.2.1 w hw]
        · exact List.nodup_cons.mpr ⟨hzM, hT.2.2.1⟩
        · intro w hw
          rcases List.mem_cons.mp hw with rfl | hw
          · exact ⟨hz, hzR⟩
          · exact hT.2.2.2 w hw
      have hPsi : Psi Qs (z :: T.1, T.2.1.insert z, z :: T.2.2) = Psi Qs T := by
        unfold Psi
        simp only [List.length_cons]
        have := filter_insert_length Qs hQ T.2.1 z hz hc'
        omega
      obtain ⟨h1, h2, L', h3⟩ := dfs_inner Qs hQ items x L
        (fun w hw => hL w (List.mem_cons_of_mem _ hw))
        (z :: T.1, T.2.1.insert z, z :: T.2.2) hT'
      refine ⟨h1, h2.trans hPsi, L' ++ [z], ?_⟩
      rw [h3]
      simp

/-- The outer fold of one DFS step: pushes along all items of `inc y`. -/
theorem dfs_outer (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat)) (x : Nat) :
    ∀ (ks : List Nat), (∀ k ∈ ks, ∀ z ∈ items.getD k [],
        z ∈ Qs ∧ Relation.ReflTransGen (Rel items) x z) →
    ∀ T : List Nat × Std.HashSet Nat × List Nat, DInv Qs items x T →
      DInv Qs items x (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) T) ∧
      Psi Qs (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) T) =
        Psi Qs T ∧
      ∃ L', (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) T).2.2 =
          L' ++ T.2.2
  | [], _, T, hT => ⟨hT, rfl, [], by simp⟩
  | k :: ks, hk, T, hT => by
    simp only [List.foldl_cons]
    obtain ⟨h1, h2, L1, h3⟩ := dfs_inner Qs hQ items x (items.getD k []) (fun z hz => hk k List.mem_cons_self z hz) T hT
    obtain ⟨h4, h5, L2, h6⟩ := dfs_outer Qs hQ items x ks (fun k' hk' => hk k' (List.mem_cons_of_mem _ hk')) _ h1
    refine ⟨h4, h5.trans h2, L2 ++ L1, ?_⟩
    rw [h6, h3]
    simp

/-- The DFS `connDfs` with enough fuel empties its stack and keeps the invariant. -/
theorem dfs_main (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat)) (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs) (x : Nat) :
    ∀ (fuel : Nat) (T : List Nat × Std.HashSet Nat × List Nat),
      DInv Qs items x T → Psi Qs T ≤ fuel →
      (connectorComponents.connDfs items inc fuel T.1 T.2.1 T.2.2).1 = [] ∧
      DInv Qs items x (connectorComponents.connDfs items inc fuel T.1 T.2.1 T.2.2) ∧
      ∃ L', (connectorComponents.connDfs items inc fuel T.1 T.2.1 T.2.2).2.2 = L' ++ T.2.2
  | 0, T, hD, hΨ => by
    have hs : T.1 = [] := by
      have h0 : T.1.length = 0 := by
        unfold Psi at hΨ
        omega
      exact List.eq_nil_of_length_eq_zero h0
    rw [connectorComponents.connDfs.eq_1]
    exact ⟨hs, hD, [], by simp⟩
  | f + 1, T, hD, hΨ => by
    obtain ⟨stack, A, M⟩ := T
    cases stack with
    | nil =>
      rw [connectorComponents.connDfs]
      exact ⟨rfl, hD, [], by simp⟩
    | cons y rest =>
      have hyM : y ∈ M := hD.1 y List.mem_cons_self
      have hyR : Relation.ReflTransGen (Rel items) x y := (hD.2.2.2 y hyM).2
      have hks : ∀ k ∈ inc.getD y [], ∀ z ∈ items.getD k [],
          z ∈ Qs ∧ Relation.ReflTransGen (Rel items) x z := by
        intro k hk z hz
        have hyk : y ∈ items.getD k [] := (hinc k y).mp hk
        exact ⟨hitems k z hz, Relation.ReflTransGen.tail hyR ⟨k, hyk, hz⟩⟩
      have hT0 : DInv Qs items x (rest, A, M) :=
        ⟨fun w hw => hD.1 w (List.mem_cons_of_mem _ hw), hD.2.1, hD.2.2.1, hD.2.2.2⟩
      obtain ⟨h1, h2, L1, h3⟩ := dfs_outer Qs hQ items x (inc.getD y []) hks (rest, A, M) hT0
      have hΨid : Psi Qs (y :: rest, A, M) = Psi Qs (rest, A, M) + 1 := by
        simp only [Psi, List.length_cons]
        omega
      have hΨ0 : Psi Qs (rest, A, M) ≤ f := by omega
      obtain ⟨g1, g2, L2, g3⟩ := dfs_main Qs hQ items inc hinc hitems x f _ h1
        (by rw [h2]; exact hΨ0)
      rw [connectorComponents.connDfs]
      refine ⟨g1, g2, L2 ++ L1, ?_⟩
      rw [g3, h3]
      simp

/-- Every component of the outer scan is `Good`. -/
theorem outer_good (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat))
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs) (fuel : Nat) (hfuel : Qs.length + 1 ≤ fuel) :
    ∀ (qs : List Nat) (A : Std.HashSet Nat) (comps : List (List Nat)),
      (∀ y ∈ qs, y ∈ Qs) → (∀ c ∈ comps, Good Qs items c) →
      ∀ c ∈ connectorComponents.connOuter items inc Qs fuel qs A comps, Good Qs items c
  | [], _, comps, _, hc => by
    rw [connectorComponents.connOuter.eq_1]
    intro c hc'
    exact hc c (List.mem_reverse.mp hc')
  | x :: qs, A, comps, hqs, hc => by
    have hxQ : x ∈ Qs := hqs x List.mem_cons_self
    have hqs' : ∀ y ∈ qs, y ∈ Qs := 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]
      exact outer_good Qs hQ items inc hinc hitems fuel hfuel qs A comps hqs' hc
    · simp only [hx, Bool.false_eq_true, ↓reduceIte]
      have hD : DInv Qs items x ([x], A.insert x, [x]) := by
        refine ⟨fun w hw => hw, fun w hw => ?_, by simp, fun w hw => ?_⟩
        · simp only [List.mem_singleton] at hw
          subst hw
          simp [Std.HashSet.contains_insert]
        · simp only [List.mem_singleton] at hw
          subst hw
          exact ⟨hxQ, Relation.ReflTransGen.refl⟩
      have hΨ : Psi Qs ([x], A.insert x, [x]) ≤ fuel := by
        unfold Psi
        have := List.length_filter_le (fun y => !(A.insert x).contains y) Qs
        simp only [List.length_singleton]
        omega
      have hr := dfs_main Qs hQ items inc hinc hitems x fuel ([x], A.insert x, [x]) hD hΨ
      simp only at hr
      obtain ⟨hr1, hr2, L1, hL1⟩ := hr
      have hne : (connectorComponents.connDfs items inc fuel [x] (A.insert x) [x]).1.isEmpty
          = true := by
        rw [hr1]
        rfl
      rw [if_pos hne]
      apply outer_good Qs hQ items inc hinc hitems fuel hfuel qs _ _ hqs'
      intro c' hc'
      rcases List.mem_cons.mp hc' with rfl | hc'
      · refine ⟨x, L1.reverse, ?_, ?_, ?_⟩
        · rw [hL1]
          simp
        · exact List.nodup_reverse.mpr hr2.2.2.1
        · intro z hz
          exact hr2.2.2.2 z (List.mem_reverse.mp hz)
      · exact hc c' hc'

/-! ## 4. Greedy order -/

/-- An item with two elements, exactly one of them present. -/
def Act (items : List (List Nat)) (present : Std.HashSet Nat) (k : Nat) : Prop :=
  (items.getD k []).length = 2 ∧ (∃ u ∈ items.getD k [], present.contains u = true) ∧
    (∃ v ∈ items.getD k [], present.contains v = false)

/-- Greedy potential: stack length plus the incidence weight of the absent elements of `Qs`. -/
def Phi (Qs : List Nat) (inc : Std.HashMap Nat (List Nat)) (stack : List Nat)
    (present : Std.HashSet Nat) : Nat :=
  stack.length + ((Qs.filter fun y => !present.contains y).map fun y => (inc.getD y []).length).sum

theorem two_le_len (e : List Nat) (hnd : e.Nodup) (x y : Nat) (hx : x ∈ e) (hy : y ∈ e)
    (hxy : x ≠ y) : 2 ≤ e.length := by
  have hn : [x, y].Nodup := by simp [hxy]
  have hsub : List.Subperm [x, y] e := hn.subperm (by
    intro w hw
    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hw
    rcases hw with rfl | rfl <;> assumption)
  have := hsub.length_le
  simpa using this

theorem filter_two (a b : Nat) (hab : a ≠ b) (present : Std.HashSet Nat) (z : Nat)
    (h : [a, b].filter (fun y => !present.contains y) = [z]) :
    (z = a ∧ present.contains b = true) ∨ (z = b ∧ present.contains a = true) := by
  by_cases ha : present.contains a = true <;> by_cases hb : present.contains b = true <;>
    simp_all [List.filter_cons]

theorem filter_two_exists (a b : Nat) (hab : a ≠ b) (present : Std.HashSet Nat)
    (hu : present.contains a = true ∨ present.contains b = true)
    (hv : present.contains a = false ∨ present.contains b = false) :
    ∃ z, [a, b].filter (fun y => !present.contains y) = [z] := by
  by_cases ha : present.contains a = true <;> by_cases hb : present.contains b = true <;>
    simp_all [List.filter_cons]

/-- The closure property: with no active item, the present set is closed under `Rel`. -/
theorem closed_of_no_act (items : List (List Nat)) (hnd : ∀ k, (items.getD k []).Nodup)
    (hlen : ∀ k, (items.getD k []).length ≤ 2) (present : Std.HashSet Nat)
    (hA : ∀ k, ¬ Act items present k) (x y : Nat) (hx : present.contains x = true)
    (hR : Rel items x y) : present.contains y = true := by
  obtain ⟨k, hxk, hyk⟩ := hR
  by_contra hy
  have hy' : present.contains y = false := by simpa using hy
  have hxy : x ≠ y := by
    intro h
    subst h
    rw [hx] at hy'
    exact Bool.noConfusion hy'
  have h2 : (items.getD k []).length = 2 :=
    le_antisymm (hlen k) (two_le_len _ (hnd k) x y hxk hyk hxy)
  exact hA k ⟨h2, ⟨x, hxk, hx⟩, ⟨y, hyk, hy'⟩⟩

theorem present_of_rtg (items : List (List Nat)) (hnd : ∀ k, (items.getD k []).Nodup)
    (hlen : ∀ k, (items.getD k []).length ≤ 2) (present : Std.HashSet Nat)
    (hA : ∀ k, ¬ Act items present k) (start : Nat) (hs : present.contains start = true) :
    ∀ z, Relation.ReflTransGen (Rel items) start z → present.contains z = true := by
  intro z hz
  induction hz with
  | refl => exact hs
  | tail _ hbc ih => exact closed_of_no_act items hnd hlen present hA _ _ ih hbc

theorem size_ge_of (c : List Nat) (hc : c.Nodup) (present : Std.HashSet Nat)
    (h : ∀ z ∈ c, present.contains z = true) : c.length ≤ present.size := by
  have hsub : List.Subperm c present.toList := hc.subperm (by
    intro z hz
    exact Std.HashSet.mem_toList.mpr (Std.HashSet.mem_iff_contains.mpr (h z hz)))
  have := hsub.length_le
  rwa [Std.HashSet.length_toList] at this

/-- Weighted filter identity for one insertion. -/
theorem sum_filter_insert (Qs : List Nat) (hQ : Qs.Nodup) (inc : Std.HashMap Nat (List Nat))
    (present : Std.HashSet Nat) (z : Nat) (hz : z ∈ Qs) (hP : present.contains z = false) :
    ((Qs.filter fun y => !(present.insert z).contains y).map
        fun y => (inc.getD y []).length).sum + (inc.getD z []).length =
      ((Qs.filter fun y => !present.contains y).map fun y => (inc.getD y []).length).sum := by
  have h := sum_filter_erase (fun y => !present.contains y) (fun y => (inc.getD y []).length) z Qs
    hQ hz (by simp [hP])
  have hf : Qs.filter (fun y => !(present.insert z).contains y) =
      Qs.filter (fun y => (!present.contains y) && y != z) := by
    apply List.filter_congr
    intro y _
    by_cases hyz : y = z
    · subst hyz
      simp [Std.HashSet.contains_insert]
    · have hzy : (z == y) = false := beq_false_of_ne (Ne.symm hyz)
      have hyz' : (y != z) = true := bne_iff_ne.mpr hyz
      rw [Std.HashSet.contains_insert, hzy, hyz']
      simp [Bool.and_comm]
  rw [hf]
  exact h

theorem pair_other (e : List Nat) (hnd : e.Nodup) (hL : e.length = 2) (present : Std.HashSet Nat)
    (z : Nat) (hF : e.filter (fun y => !present.contains y) = [z]) :
    z ∈ e ∧ ∃ w ∈ e, w ≠ z ∧ present.contains w = true := by
  obtain ⟨a, b, rfl⟩ := List.length_eq_two.mp hL
  have hab : a ≠ b := by
    intro h
    subst h
    simp at hnd
  rcases filter_two a b hab present z hF with ⟨rfl, hb⟩ | ⟨rfl, ha⟩
  · exact ⟨by simp, b, by simp, fun h => hab h.symm, hb⟩
  · exact ⟨by simp, a, by simp, hab, ha⟩

theorem filter_exists_act (e : List Nat) (hnd : e.Nodup) (hL : e.length = 2)
    (present : Std.HashSet Nat) (u v : Nat) (hu : u ∈ e) (hv : v ∈ e)
    (hpu : present.contains u = true) (hpv : present.contains v = false) :
    ∃ z, e.filter (fun y => !present.contains y) = [z] := by
  obtain ⟨a, b, hE⟩ := List.length_eq_two.mp hL
  rw [hE] at hu hv ⊢
  simp only [List.mem_cons, List.mem_nil_iff, or_false] at hu hv
  rcases hu with hu | hu <;> rcases hv with hv | hv <;> rw [hu] at hpu <;> rw [hv] at hpv <;>
    by_cases ha : present.contains a = true <;> by_cases hb : present.contains b = true <;>
    simp_all [List.filter_cons]

theorem loop_flag (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat))
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs)
    (hnd : ∀ k, (items.getD k []).Nodup) (hlen : ∀ k, (items.getD k []).length ≤ 2)
    (c : List Nat) (start : Nat) (hconn : ∀ z ∈ c, Relation.ReflTransGen (Rel items) start z)
    (hcnd : c.Nodup)
    (mk : Std.HashSet Nat → List Nat → Bool → List Nat × Bool)
    (hmk : ∀ P O F, (mk P O F).2 = F) :
    ∀ (fuel : Nat) (stack : List Nat) (present : Std.HashSet Nat) (ordRev : List Nat) (fl : Bool),
      fl = false → present.contains start = true → (∀ k, Act items present k → k ∈ stack) →
      Phi Qs inc stack present ≤ fuel →
      (connectorGreedy.loop items inc c mk fuel stack present ordRev fl).2 = false := by
  intro fuel
  induction fuel with
  | zero =>
    intro stack present ordRev fl hfl hs hH hΦ
    have hst : stack = [] := by
      unfold Phi at hΦ
      exact List.eq_nil_of_length_eq_zero (by omega)
    subst hst
    have hA : ∀ k, ¬ Act items present k := fun k hk => by simpa using hH k hk
    have hcov : c.length ≤ present.size :=
      size_ge_of c hcnd present (fun z hz => present_of_rtg items hnd hlen present hA start hs z (hconn z hz))
    rw [connectorGreedy.loop.eq_1, hmk]
    simp [hfl, hcov]
  | succ f ih =>
    intro stack present ordRev fl hfl hs hH hΦ
    cases stack with
    | nil =>
      have hA : ∀ k, ¬ Act items present k := fun k hk => by simpa using hH k hk
      have hcov : c.length ≤ present.size :=
        size_ge_of c hcnd present (fun z hz => present_of_rtg items hnd hlen present hA start hs z (hconn z hz))
      rw [connectorGreedy.loop, hmk]
      simp [hfl, hcov]
    | cons k stack =>
      rw [connectorGreedy.loop]
      split
      · rw [hmk]
        exact hfl
      · dsimp only
        split
        · rename_i z hF hL
          obtain ⟨hzE, w, hwE, hwz, hwP⟩ := pair_other (items.getD k []) (hnd k) hL present z hF
          have hzP : present.contains z = false := by
            have hmem : z ∈ List.filter (fun y => !present.contains y) (items.getD k []) := by
              rw [hF]; exact List.mem_singleton_self z
            simpa using (List.mem_filter.mp hmem).2
          have hzQ : z ∈ Qs := hitems k z hzE
          have hs' : (present.insert z).contains start = true := by
            rw [Std.HashSet.contains_insert]
            simp [hs]
          apply ih ((inc.getD z []).reverse ++ stack) (present.insert z) (z :: ordRev) fl hfl hs'
          · intro k' hk'
            by_cases hzk' : z ∈ items.getD k' []
            · exact List.mem_append.mpr (Or.inl (List.mem_reverse.mpr ((hinc k' z).mpr hzk')))
            · obtain ⟨hl', ⟨u, hu, hpu⟩, ⟨v, hv, hpv⟩⟩ := hk'
              have hzu : z ≠ u := fun h => hzk' (by rw [h]; exact hu)
              have hzv : z ≠ v := fun h => hzk' (by rw [h]; exact hv)
              have hpu' : present.contains u = true := by
                rw [Std.HashSet.contains_insert, beq_false_of_ne hzu, Bool.false_or] at hpu
                exact hpu
              have hpv' : present.contains v = false := by
                rw [Std.HashSet.contains_insert, beq_false_of_ne hzv, Bool.false_or] at hpv
                exact hpv
              have hk'ne : k' ≠ k := fun h => hzk' (by rw [h]; exact hzE)
              rcases List.mem_cons.mp (hH k' ⟨hl', ⟨u, hu, hpu'⟩, ⟨v, hv, hpv'⟩⟩) with h | h
              · exact absurd h hk'ne
              · exact List.mem_append.mpr (Or.inr h)
          · unfold Phi at hΦ ⊢
            have hsum := sum_filter_insert Qs hQ inc present z hzQ hzP
            simp only [List.length_append, List.length_reverse, List.length_cons] at hΦ ⊢
            omega
        · rename_i _ _ hnot
          apply ih stack present ordRev fl hfl hs
          · intro k' hk'
            rcases List.mem_cons.mp (hH k' hk') with h | h
            · exfalso
              rw [h] at hk'
              obtain ⟨hl, ⟨u, hu, hpu⟩, ⟨v, hv, hpv⟩⟩ := hk'
              obtain ⟨z', hz'⟩ := filter_exists_act (items.getD k []) (hnd k) hl present u v hu hv hpu hpv
              exact hnot z' hz' hl
            · exact h
          · unfold Phi at hΦ ⊢
            simp only [List.length_cons] at hΦ
            omega

/-- The greedy flag of one good component is `false`. -/
theorem greedy_flag (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat))
    (hinc : ∀ k y, k ∈ inc.getD y [] ↔ y ∈ items.getD k [])
    (hsum : (Qs.map fun z => (inc.getD z []).length).sum ≤ (items.map List.length).sum)
    (hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs)
    (hnd : ∀ k, (items.getD k []).Nodup) (hlen : ∀ k, (items.getD k []).length ≤ 2)
    (c : List Nat) (hG : Good Qs items c) :
    (connectorGreedy items inc c).2 = false := by
  obtain ⟨start, c', rfl, hcnd, hall⟩ := hG
  have hstart : start ∈ Qs := (hall start List.mem_cons_self).1
  have hΦ : Phi Qs inc ((inc.getD start []).reverse) ((∅ : Std.HashSet Nat).insert start) ≤
      (items.map List.length).sum + 1 := by
    unfold Phi
    rw [List.length_reverse]
    have hf : Qs.filter (fun y => !((∅ : Std.HashSet Nat).insert start).contains y) =
        Qs.filter (fun y => y != start) := by
      apply List.filter_congr
      intro y _
      by_cases hy : y = start
      · subst hy
        simp [Std.HashSet.contains_insert]
      · simp [Std.HashSet.contains_insert, hy, Ne.symm hy, bne]
    rw [hf]
    have h : ((Qs.filter fun y => y != start).map fun y => (inc.getD y []).length).sum +
        (inc.getD start []).length = (Qs.map fun z => (inc.getD z []).length).sum := by
      have := sum_filter_erase (fun _ => true) (fun y => (inc.getD y []).length) start Qs hQ
        hstart rfl
      simpa using this
    omega
  have hH : ∀ k, Act items ((∅ : Std.HashSet Nat).insert start) k → k ∈ (inc.getD start []).reverse := by
    intro k hk
    obtain ⟨_, ⟨u, hu, hpu⟩, _⟩ := hk
    have hus : u = start := by
      rw [Std.HashSet.contains_insert, Std.HashSet.contains_empty] at hpu
      simp at hpu
      exact hpu.symm
    rw [List.mem_reverse]
    exact (hinc k start).mpr (hus ▸ hu)
  have hs : ((∅ : Std.HashSet Nat).insert start).contains start = true := by
    simp
  have key := loop_flag Qs hQ items inc hinc hitems hnd hlen (start :: c') start
    (fun z hz => (hall z hz).2) hcnd
    (fun present ordRev fl => (ordRev.reverse ++ (start :: c').filter (fun z => !present.contains z), fl))
    (fun _ _ _ => rfl) ((items.map List.length).sum + 1) ((inc.getD start []).reverse)
    ((∅ : Std.HashSet Nat).insert start) [start] false rfl hs hH hΦ
  unfold connectorGreedy
  exact key

/-- The components of `connectorComponents` are `Good`. -/
theorem connectorComponents_good (Qs : List Nat) (hQ : Qs.Nodup) (items : List (List Nat))
    (hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs) :
    ∀ c ∈ connectorComponents Qs items (connectorIncidence Qs items), Good Qs items c := by
  intro c hc
  unfold connectorComponents at hc
  exact outer_good Qs hQ items (connectorIncidence Qs items) (mem_inc_iff Qs items) hitems
    _ (by omega) Qs ∅ [] (fun y hy => hy) (fun c hc => by simp at hc) c hc

theorem getD_mem_of_lt (l : List (List Nat)) (i : Nat) (hi : i < l.length) :
    l.getD i [] ∈ l := by
  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi]
  simpa using List.getElem_mem hi

theorem getD_mem_or_nil (items : List (List Nat)) (k : Nat) :
    items.getD k [] = [] ∨ items.getD k [] ∈ items := by
  rw [List.getD_eq_getElem?_getD]
  cases hk : items[k]? with
  | none => left; simp
  | some e => right; simpa using List.mem_of_getElem? hk

end N1

/-- N1: the connector greedy never runs dry (`Spec.lean` §7). -/
theorem connectorNoFallback : ConnectorNoFallback := by
  intro Qs items hQ hI
  have hitems : ∀ k, ∀ z ∈ items.getD k [], z ∈ Qs := fun k z hz => by
    obtain ⟨e, he, hze⟩ := C3.mem_getD_items hz
    exact (hI e he).2.2.2 z hze
  have hnd : ∀ k, (items.getD k []).Nodup := fun k => by
    rcases N1.getD_mem_or_nil items k with h | h
    · rw [h]; exact List.nodup_nil
    · exact (hI _ h).1
  have hlen : ∀ k, (items.getD k []).length ≤ 2 := fun k => by
    rcases N1.getD_mem_or_nil items k with h | h
    · rw [h]; simp
    · exact (hI _ h).2.2.1
  have hcomp := N1.connectorComponents_good Qs hQ items hitems
  unfold connectorOrderF
  dsimp only
  rw [List.any_eq_false]
  intro x hx
  obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hx
  obtain ⟨hpr, _⟩ := List.of_mem_zip ((List.mergeSort_perm _ _).mem_iff.mp hp)
  have hmem := N1.getD_mem_of_lt _ _ (List.mem_range.mp hpr)
  have hG := hcomp _ hmem
  have hfl := N1.greedy_flag Qs hQ items _ (N1.mem_inc_iff Qs items)
    (N1.total_inc_le Qs hQ items) hitems hnd hlen _ hG
  intro h
  rw [hfl] at h
  exact Bool.false_ne_true h

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.connectorNoFallback