CubicPathwidth.Alg.Port

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

import CubicPathwidth.Alg.Graph

/-!
# Port of `ancillary/experiments/sweep-algorithms/sweep.py` (SKELETON)

Every function of `sweep.py` that produces a decomposition is ported here with its
exact signature, a docstring (Python function, line range in `sweep.py`, semantics,
contract) and, where marked with a todo-port comment, a TEMPORARY placeholder body that is
trivially total. Placeholders are to be replaced one at a time;
each replacement must compile, contain no `sorry`, and match Python on the harness
(`lean_diff.py` + `DiffMain.lean`).

Conventions.
* Iteration model M (see `Graph.lean`): subgraph views iterate in parent
  order; `connector_order` receives `Wp` and the items in the node order of `G`.
* Python sets are `List Nat` read as sets. Where Python iterates a set and the order
  matters, the docstring says which order the port uses.
* Python list used as a stack (`append`/`extend` at the end, `pop()` from the end) is
  ported as a Lean list whose HEAD is the Python END: `pop` = take the head,
  `extend(xs)` = `xs.reverse ++ stack`.
* Labels are not ported. `Y : Nat → Rat` replaces the label dict; `lab : Labeler`
  gives the labels used for each graph to which the plain sweep is applied.
* Python `assert`s (and crashes) become FALLBACKS that keep the output valid; each
  function `fooF` returns `(result, flag)` where `flag = true` iff some fallback fired
  (in this call or a nested one). `foo := (fooF ..).1`. Stage 2 must show the flags are
  `false` on the relevant inputs (statements in `Spec.lean`, section "Stage 2").
* Loops and recursion are total through explicit fuel; running out of fuel is a
  fallback (flagged) that keeps the output valid.
-/

-- Placeholders leave arguments unused; remove this option once every body is ported.
set_option linter.unusedVariables false

namespace CubicPathwidth.Alg

open Graph

/-! ## Data (final, not placeholders) -/

/-- A recorded operation: Python `("red", v, nbrs)` (vertex `v` removed by a reduction,
`nbrs` = its neighbour list at that time, in adjacency order) or `("del", w)`. -/
inductive Op where
  | red (v : Nat) (nbrs : List Nat)
  | del (w : Nat)
  deriving BEq, Repr, Inhabited, DecidableEq

/-- Labels for one graph: Python `Y[v]` (floats exported exactly as rationals). -/
abbrev Labels := Nat → Rat

/-- A labeler: the labels used when the plain sweep is applied to a graph `J`
(Python `labels(J, q_mixed(J), h, rng, True)`; the rng is not ported). -/
abbrev Labeler := Graph → Nat → Rat

/-- Python `D = {o[1] for o in ops if o[0] == "del"}`, as a list in op order. -/
def deletedSet (ops : List Op) : List Nat :=
  ops.filterMap fun | .del w => some w | .red _ _ => none

/-- The vertices removed by reductions, in op order. -/
def redVertices (ops : List Op) : List Nat :=
  ops.filterMap fun | .red v _ => some v | .del _ => none

/-- Python `[frozenset((v,) + nb) for _, v, nb in ops]` (pd_tw2, line 155): the
elimination bags `v :: nb`, in op order (deletions are skipped; pd_tw2 has none). -/
def elimBags (ops : List Op) : List Bag :=
  ops.filterMap fun | .red v nb => some (v :: nb) | .del _ => none

/-- Python `[G.subgraph(c).copy() for c in nx.connected_components(G)]` (lines 216, 230):
the induced graphs of the components, in component order. (Final.) -/
def componentGraphs (G : Graph) : List Graph :=
  G.components.map fun c => G.induced c.contains

/-- Python `G.subgraph([v for v in G if G.degree(v) > 0]).copy()` (line 214). (Final.) -/
def nonIsolated (G : Graph) : Graph :=
  G.induced fun v => G.degree v != 0

/-- Python `[{v} for v in G if G.degree(v) == 0]` (line 239). (Final.) -/
def isolatedBags (G : Graph) : List Bag :=
  (G.nodes.filter fun v => G.degree v == 0).map fun v => [v]

/-! ## Plain sweep (`plain_layout`, sweep.py lines 57-65) -/

/-- Python `sorted(G, key=lambda v: (-Y[v], v))`: nodes by DECREASING `Y`, ties by
INCREASING vertex number. Implement with `List.mergeSort` and the comparator
`fun a b => decide (Y b < Y a) || (decide (Y a = Y b) && decide (a ≤ b))`.
Contract: a permutation of `G.nodes`. -/
def plainOrder (G : Graph) (Y : Labels) : List Nat :=
  G.nodes.mergeSort fun a b => decide (Y b < Y a) || (decide (Y a = Y b) && decide (a ≤ b))

/-- Python `plain_layout(G, Y)` (lines 57-65). With `order := plainOrder G Y`,
`idx v` = position of `v` in `order` (via a `Std.HashMap Nat Nat` built from
`order.zipIdx`, default `0`), `last v := (G.nbrs v).foldl (fun m u => max m (idx u)) (idx v)`,
the output has `order.length` bags and bag `i` is the set `{v ∈ G | idx v ≤ i ≤ last v}`.
REQUIRED form (for the proofs; `O(n²)`, fast enough for the harness):
`(List.range order.length).map fun i => G.nodes.filter fun v => idx v ≤ i && i ≤ last v`.
Contract (`PlainLayoutValid`): for `G.WF` and every `Y`, a valid path decomposition of
`G` whose bags only contain nodes of `G`. -/
def plainLayout (G : Graph) (Y : Labels) : List Bag :=
  let order := plainOrder G Y
  let idxMap : Std.HashMap Nat Nat := order.zipIdx.foldl (fun m p => m.insert p.1 p.2) ∅
  let idx : Nat → Nat := fun v => idxMap.getD v 0
  let last : Nat → Nat := fun v => (G.nbrs v).foldl (fun m u => max m (idx u)) (idx v)
  (List.range order.length).map fun i => G.nodes.filter fun v => idx v ≤ i && i ≤ last v

/-! ## Connector order (`connector_order`, sweep.py lines 69-99) -/

/-- Python `inc` (lines 71-74): `inc[x]` = the indices `k` (increasing) of the items
containing `x`, for every `x` occurring in an item (`getD x []` for others).
Python's `inc` has keys `Qs`; items are assumed to lie in `Qs`. -/
def connectorIncidence (Qs : List Nat) (items : List (List Nat)) :
    Std.HashMap Nat (List Nat) :=
  items.zipIdx.foldl (fun m p => p.1.foldl (fun m x => m.insert x (m.getD x [] ++ [p.2])) m) ∅

/-- Python lines 75-86: the components of the hypergraph on `Qs` with edges `items`,
each as its `members` list, in the order Python creates them (scan `x ∈ Qs`; a new
component starts at an unassigned `x`; DFS with `stack.pop()` from the end, scanning
`k ∈ inc[y]` and `z ∈ items[k]` in list order, appending newly assigned `z` to
`members` and to the stack). `members.head` is the start `x`.
Totality: a DFS with fuel `Qs.length + (items.map List.length).sum + 1`; on exhaustion
the not yet assigned elements of `Qs` form a last component (cannot happen when the
items lie in `Qs`). Contract: a partition of `Qs` (when `Qs.Nodup` and items ⊆ `Qs`). -/
def connectorComponents (Qs : List Nat) (items : List (List Nat))
    (inc : Std.HashMap Nat (List Nat)) : List (List Nat) :=
  connOuter Qs (Qs.length + (items.map List.length).sum + 1) Qs ∅ []
where
  /-- DFS step: state `(stack, assigned, memRev)`, stack head = Python end. -/
  connDfs (fuel : Nat) (stack : List Nat) (assigned : Std.HashSet Nat) (memRev : List Nat) :
      List Nat × Std.HashSet Nat × List Nat :=
    match fuel, stack with
    | 0, _ => (stack, assigned, memRev)
    | _ + 1, [] => ([], assigned, memRev)
    | f + 1, y :: rest =>
      let st := (inc.getD y []).foldl (fun (acc : List Nat × Std.HashSet Nat × List Nat) k =>
        (items.getD k []).foldl (fun (acc : List Nat × Std.HashSet Nat × List Nat) z =>
          if acc.2.1.contains z then acc
          else (z :: acc.1, acc.2.1.insert z, z :: acc.2.2)) acc) (rest, assigned, memRev)
      connDfs f st.1 st.2.1 st.2.2
  /-- Outer scan over `Qs` (Python `for x in Qs`); `all` = `Qs` for the last component. -/
  connOuter (all : List Nat) (fuel : Nat) : List Nat → Std.HashSet Nat → List (List Nat) →
      List (List Nat)
    | [], _, comps => comps.reverse
    | x :: qs, assigned, comps =>
      if assigned.contains x then connOuter all fuel qs assigned comps
      else
        let r := connDfs fuel [x] (assigned.insert x) [x]
        let comps' := r.2.2.reverse :: comps
        if r.1.isEmpty then connOuter all fuel qs r.2.1 comps'
        else
          let rest := all.filter (fun y => !r.2.1.contains y)
          (if rest.isEmpty then comps' else rest :: comps').reverse

/-- Python line 87: `exc[i] = len(comps[i]) - #{k | comp[first(items[k])] = i}`, where
`first(e)` is any element of `e` (all lie in one component); use `e.head?` and skip
empty items. One entry per component, in component order. -/
def connectorExcess (items : List (List Nat)) (comps : List (List Nat)) : List Int :=
  let idxOf : Std.HashMap Nat Nat :=
    comps.zipIdx.foldl (fun m p => p.1.foldl (fun m x => m.insert x p.2) m) ∅
  let cnt : Std.HashMap Nat Nat :=
    (items.filterMap List.head?).foldl (fun m x =>
      let i := idxOf.getD x 0
      m.insert i (m.getD i 0 + 1)) ∅
  comps.zipIdx.map fun p => (p.1.length : Int) - (cnt.getD p.2 0 : Int)

/-- Python lines 90-98 for one component `c` (`start = c[0]`): greedy order.
State: `present` (set), `order`, `frontier` (Python list; Lean stack with head = Python
end). Initially `present = {start}`, `order = [start]`, `frontier = inc[start]`.
Loop while `present.size < c.length`: pop `k` from the frontier; let
`miss = items[k].filter (∉ present)`; if `miss.length = 1 ∧ items[k].length = 2`, add
`z = miss[0]` to `present` and `order` and extend the frontier by `inc[z]`; otherwise
discard `k`.
Fuel: `(items.map List.length).sum + 1` pops.
When the loop stops, ALWAYS append the members of `c` not yet present (in `c` order).
If the loop stopped because `present.size ≥ c.length` this appends nothing (every
element added lies in `c`, by the closure of components), so it is Python's behaviour;
it makes "every member of `c` is output" trivial to prove.
FALLBACK (Python: `IndexError` on `frontier.pop()` from an empty list, which happens
only when some item has size `> 2`, i.e. maximum degree `≥ 4`): if the loop stopped on
an empty frontier or exhausted fuel while `present.size < c.length`, set the flag.
Returns `(order of c, flag)`. -/
def connectorGreedy (items : List (List Nat)) (inc : Std.HashMap Nat (List Nat))
    (c : List Nat) : List Nat × Bool :=
  match c with
  | [] => ([], false)
  | start :: _ =>
    let mkRes : Std.HashSet Nat → List Nat → Bool → List Nat × Bool := fun present ordRev fl =>
      (ordRev.reverse ++ c.filter (fun z => !present.contains z), fl)
    let rec loop : Nat → List Nat → Std.HashSet Nat → List Nat → Bool → List Nat × Bool
      | 0, _, present, ordRev, fl => mkRes present ordRev (fl || decide (present.size < c.length))
      | _ + 1, [], present, ordRev, fl =>
        mkRes present ordRev (fl || decide (present.size < c.length))
      | f + 1, k :: stack, present, ordRev, fl =>
        if c.length ≤ present.size then mkRes present ordRev fl
        else
          let its := items.getD k []
          match its.filter (fun z => !present.contains z), its.length with
          | [z], 2 => loop f ((inc.getD z []).reverse ++ stack) (present.insert z) (z :: ordRev) fl
          | _, _ => loop f stack present ordRev fl
    loop ((items.map List.length).sum + 1) ((inc.getD start []).reverse)
      ((∅ : Std.HashSet Nat).insert start) [start] false

/-- Python `connector_order(Q, items)` (lines 69-99) with `Qs = list(Q)` given as a
list (model M: the caller passes `Wp` in node order). Components are processed in
the order `sorted(range(len(comps)), key=exc)`: a STABLE sort by `exc` (use
`List.mergeSort` on `(index, exc)` pairs with `≤` on `exc`), and the greedy orders are
concatenated. The flag is the `||` of the greedy flags.
Contract (`ConnectorOrderMem`): if every item lies in `Qs`, the output has exactly the
elements of `Qs` (as a set). Stage 2 (`ConnectorNoFallback`): if moreover every item is
duplicate-free of length 1 or 2, the flag is `false`. -/
def connectorOrderF (Qs : List Nat) (items : List (List Nat)) : List Nat × Bool :=
  let inc := connectorIncidence Qs items
  let comps := connectorComponents Qs items inc
  let exc := connectorExcess items comps
  let ordered := ((List.range comps.length).zip exc).mergeSort fun a b => decide (a.2 ≤ b.2)
  let parts := ordered.map fun p => connectorGreedy items inc (comps.getD p.1 [])
  (parts.flatMap (·.1), parts.any (·.2))

/-- `connector_order` without the flag. -/
def connectorOrder (Qs : List Nat) (items : List (List Nat)) : List Nat :=
  (connectorOrderF Qs items).1

/-! ## Median-switched layout (`switched_layout`, sweep.py lines 102-128) -/

/-- Python `low`: `Y[v] < 0`. (Final.) -/
def isLow (Y : Labels) (v : Nat) : Bool := decide (Y v < 0)

/-- Python `U` (line 106): low vertices with a neighbour that is not low. (Final.) -/
def inU (G : Graph) (Y : Labels) (u : Nat) : Bool :=
  isLow Y u && (G.nbrs u).any (fun x => !isLow Y x)

/-- Python `Wset` (line 107): non-low vertices with a low neighbour. (Final.) -/
def inW (G : Graph) (Y : Labels) (w : Nat) : Bool :=
  !isLow Y w && (G.nbrs w).any (fun u => isLow Y u)

/-- Python `Dset` (line 108): vertices of degree 3 all of whose neighbours lie on the
other side. (Final.) -/
def inD (G : Graph) (Y : Labels) (v : Nat) : Bool :=
  G.degree v == 3 && (G.nbrs v).all (fun u => isLow Y u != isLow Y v)

/-- Python `sorted(G, key=lambda v: (Y[v], v))`: INCREASING `Y`, ties by increasing
vertex number (`List.mergeSort` with
`fun a b => decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))`). -/
def switchedOrder (G : Graph) (Y : Labels) : List Nat :=
  G.nodes.mergeSort fun a b => decide (Y a < Y b) || (decide (Y a = Y b) && decide (a ≤ b))

/-- Python `switched_layout(G, Y)` (lines 102-128) under model M.
With `order := switchedOrder G Y`, `ell :=` number of low nodes, `Up := U \ D`,
`Wp := Wset \ D`:
* `P := G.nodes.filter (fun u => inU u && !inD u && (G.nbrs u).any Wp)` (model M:
  node order; Python iterates the set `Up`);
* `e u := (G.nbrs u).filter Wp`;
* `(q, flag) := connectorOrderF (G.nodes.filter Wp) (P.map e)` (model M: node order;
  Python iterates the set `Wp`);
* inner bags, `i < ell`, `v = order[i]`, `T = order.take i`:
  `v :: T.filter (fun u => (G.nbrs u).any (· ∉ T))`;
* `C₋₁ := G.nodes.filter (fun v => inU v || (inD v && inW v))`;
* for `j = 0, …, q.length`: `C_j := G.nodes.filter inD ++
  P.filter (fun u => !subsetB (e u) (q.take (j - 1))) ++ q.take j`
  (Python `prev = q[:max(j-1, 0)]`; natural subtraction gives the same);
* outer bags, `ell ≤ i < order.length`, `v = order[i]`, `T = low ∪ order[ell..i]`
  (inclusive): `v :: G.nodes.filter (fun x => x ∉ T && (G.nbrs x).any (· ∈ T))`.
Output: inner ++ [C₋₁] ++ [C₀..C_m] ++ outer, and the connector flag.
Contract (`SwitchedLayoutValid`): for every `G.WF` and `Y` (any maximum degree, thanks
to the connector fallback) a valid path decomposition with bags inside `G`.
Stage 2: for maximum degree `≤ 3` the flag is `false`. -/
def switchedLayoutF (G : Graph) (Y : Labels) : List Bag × Bool :=
  let order := switchedOrder G Y
  let lowL := G.nodes.filter (isLow Y)
  let ell := lowL.length
  let Wp : Nat → Bool := fun x => inW G Y x && !inD G Y x
  let P := G.nodes.filter fun u => inU G Y u && !inD G Y u && (G.nbrs u).any Wp
  let e : Nat → List Nat := fun u => (G.nbrs u).filter Wp
  let qf := connectorOrderF (G.nodes.filter Wp) (P.map e)
  let q := qf.1
  let inner := (List.range ell).map fun i =>
    let v := order.getD i 0
    let T := order.take i
    let TS : Std.HashSet Nat := T.foldl (fun s x => s.insert x) ∅
    v :: T.filter (fun u => (G.nbrs u).any (fun x => !TS.contains x))
  let cm1 := G.nodes.filter fun v => inU G Y v || (inD G Y v && inW G Y v)
  let Dl := G.nodes.filter (inD G Y)
  let cs := (List.range (q.length + 1)).map fun j =>
    Dl ++ P.filter (fun u => !subsetB (e u) (q.take (j - 1))) ++ q.take j
  let outer := (List.range (order.length - ell)).map fun k =>
    let v := order.getD (ell + k) 0
    let T := lowL ++ (order.drop ell).take (k + 1)
    let TS : Std.HashSet Nat := T.foldl (fun s x => s.insert x) ∅
    v :: G.nodes.filter (fun x => !TS.contains x && (G.nbrs x).any (fun u => TS.contains u))
  (inner ++ [cm1] ++ cs ++ outer, qf.2)

/-- `switched_layout` without the flag. -/
def switchedLayout (G : Graph) (Y : Labels) : List Bag := (switchedLayoutF G Y).1

/-! ## Reductions (`reduce_record`, sweep.py lines 132-143) -/

/-- The loop of `reduce_record` (lines 135-143). `stack` is Python's `stack` (head =
Python end). One step with `fuel + 1`: pop `v`; if `!G.mem v || G.degree v > 2`, skip;
else `nb := G.nbrs v`, record `.red v nb`, `G := G.removeNode v`, if `nb.length = 2`
then `G := G.addEdge nb[0] nb[1]` (R3, or R4 if present), and push `nb`
(`stack := nb.reverse ++ stack`).
Returns `(final graph, ops in chronological order, flag)`; `opsRev` accumulates the
ops in REVERSE order. Fuel `0` with a nonempty stack: stop and set the flag (the
result is still a valid record of reductions, only not maximal).
Termination bound: at most `|initial stack| + 2·numNodes` pops. -/
def reduceLoop (fuel : Nat) (G : Graph) (stack : List Nat) (opsRev : List Op) :
    Graph × List Op × Bool :=
  match fuel, stack with
  | _, [] => (G, opsRev.reverse, false)
  | 0, _ :: _ => (G, opsRev.reverse, true)
  | fuel + 1, v :: rest =>
    if !G.mem v || G.degree v > 2 then reduceLoop fuel G rest opsRev
    else
      let nb := G.nbrs v
      let G1 := G.removeNode v
      let G2 := match nb with
        | [a, b] => G1.addEdge a b
        | _ => G1
      reduceLoop fuel G2 (nb.reverse ++ rest) (Op.red v nb :: opsRev)

/-- Python `reduce_record(G, ops)` (lines 132-143): apply R1-R4 until none applies.
Python mutates `G` and appends to `ops`; the port returns the final graph and the NEW
ops. Initial stack: `[v for v in G if G.degree(v) <= 2]`, i.e.
`(G.nodes.filter (G.degree · ≤ 2)).reverse` as a Lean stack. Fuel
`3 * G.numNodes + 1`.
Contract (`ReduceRecordSpec`). Stage 2 (`ReduceRecordNoFallback`): flag `false`. -/
def reduceRecordF (G : Graph) : Graph × List Op × Bool :=
  reduceLoop (3 * G.numNodes + 1) G ((G.nodes.filter fun v => G.degree v ≤ 2).reverse) []

/-- `reduce_record` without the flag. -/
def reduceRecord (G : Graph) : Graph × List Op :=
  let r := reduceRecordF G
  (r.1, r.2.1)

/-! ## Width-2 elimination with balanced bags (`pd_tw2`, sweep.py lines 146-164) -/

/-- Python `pd_tw2(H)` (lines 146-164), with fuel:
* `H.numNodes = 0`: `([], false)`; `H.numNodes ≤ 3`: `([H.nodes], false)`;
* fuel `0` (otherwise): FALLBACK `([H.nodes], true)`;
* fuel `f + 1`: `(G', ops, fl) := reduceRecordF H.copy`.
  FALLBACK if `G'.numNodes ≠ 0` (Python: `assert ... "graph has a K4 minor"`):
  `([H.nodes], true)`.
  Otherwise let `N := H.numNodes` and, for a bag `X`,
  `comps X := (H.induced (fun v => !X.contains v)).components`. Take the FIRST
  `X ∈ elimBags ops` with `∀ c ∈ comps X, 2 * c.length ≤ N` (Python `len(c) <= N / 2`).
  FALLBACK if none (Python: `raise AssertionError("no balanced bag found")`):
  `([H.nodes], true)`.
  Otherwise, for each `c ∈ comps X` in order, `(Pc, fc) := pdTw2Fuel f
  (H.induced c.contains)` (Python `H.subgraph(c).copy()`), output the concatenation of
  `Pc.map (bagUnion · X)`, or `[X]` if that is empty; flag `fl || any fc`.
Contract (`PdTw2Valid`): for every `H.WF`, a valid path decomposition of `H` with
bags inside `H` (fallbacks included). Stage 2: no flag when `H` has treewidth `≤ 2`
(reduces to the empty graph) and `fuel ≥ H.numNodes`. -/
def pdTw2Fuel (fuel : Nat) (H : Graph) : List Bag × Bool :=
  if H.numNodes = 0 then ([], false)
  else if H.numNodes ≤ 3 then ([H.nodes], false)
  else match fuel with
    | 0 => ([H.nodes], true)
    | f + 1 =>
      let r := reduceRecordF H.copy
      if r.1.numNodes != 0 then ([H.nodes], true)
      else
        let N := H.numNodes
        let compsOf : Bag → List (List Nat) := fun X =>
          (H.induced fun v => !X.contains v).components
        match (elimBags r.2.1).find? (fun X => (compsOf X).all fun c => decide (2 * c.length ≤ N)) with
        | none => ([H.nodes], true)
        | some X =>
          let parts := (compsOf X).map fun c => pdTw2Fuel f (H.induced c.contains)
          let out := parts.flatMap fun p => p.1.map fun B => bagUnion B X
          (if out.isEmpty then [X] else out, r.2.2 || parts.any fun p => p.2)

/-- `pd_tw2` with fuel `H.numNodes` (recursive calls have at most `N/2 < N` nodes). -/
def pdTw2F (H : Graph) : List Bag × Bool := pdTw2Fuel H.numNodes H

/-- `pd_tw2` without the flag. -/
def pdTw2 (H : Graph) : List Bag := (pdTw2F H).1

/-! ## Undoing reductions and deletions (`undo`, sweep.py lines 167-187) -/

/-- Python line 175: `S = {x for c in C for x in F[c] if x not in C and x not in D}`,
as a duplicate-free list in first-occurrence order (scan `c ∈ C`, `x ∈ F.nbrs c`). -/
def undoAttach (F : Graph) (D : List Nat) (C : List Nat) : List Nat :=
  C.foldl (fun acc c =>
    (F.nbrs c).foldl (fun acc x =>
      if C.contains x || D.contains x || acc.contains x then acc else acc ++ [x]) acc) []

/-- Python `undo(F, ops, R, bagsR)` (lines 167-187) under model M.
* `D := deletedSet ops`; `rest := F.induced (fun v => !D.contains v && !R.mem v)`.
* For each component `C` of `rest` (in `rest.components` order): `S := undoAttach F D C`.
  FALLBACK (Python `assert ... "invariant (I2) fails"`) unless
  `S.all R.mem && S.length ≤ 2 && (S.length < 2 || R.hasEdge S[0] S[1])`.
  `(P, fP) := pdTw2F (F.induced C.contains)`.
  If `S = []`, append `P` to `tail`. Otherwise `i :=` the FIRST index with
  `subsetB S bagsR[i]` (FALLBACK if none; Python `next(...)` would raise
  `StopIteration`) and append `P.map (bagUnion · bagsR[i])` to `inserts[i]`.
* `out := (for each i: bagsR[i] :: inserts[i]) ++ tail`; result
  `out.map (bagUnion · D)`, or `[D]` if `out = []`.
* FALLBACK result: `([F.nodes], true)` (one bag with every vertex of `F`).
* The flag also includes every `fP`.
Contract (`UndoValid`): under the preconditions stated there (implied by the calls in
`algoMixed` and `algoT4`), a valid path decomposition of `F`. -/
def undoF (F : Graph) (ops : List Op) (R : Graph) (bagsR : List Bag) : List Bag × Bool :=
  let D := deletedSet ops
  let rest := F.induced fun v => !D.contains v && !R.mem v
  -- one plan per component C of `rest`: (S, P, fP, attachment index if S ≠ [])
  let plans : List (List Nat × List Bag × Bool × Option Nat) := rest.components.map fun C =>
    let S := undoAttach F D C
    let Pf := pdTw2F (F.induced C.contains)
    (S, Pf.1, Pf.2, if S.isEmpty then none else bagsR.findIdx? (subsetB S ·))
  let validS : List Nat → Bool := fun S => S.all R.mem && match S with
    | [] => true
    | [_] => true
    | [a, b] => R.hasEdge a b
    | _ => false
  let ok := plans.all fun ⟨S, _, _, idx⟩ => validS S && (S.isEmpty || idx.isSome)
  if !ok then ([F.nodes], true) else
  let fl := plans.any fun ⟨_, _, f, _⟩ => f
  let tail := plans.flatMap fun ⟨S, P, _, _⟩ => if S.isEmpty then P else []
  let out := bagsR.zipIdx.flatMap fun ⟨B, i⟩ =>
    B :: plans.flatMap fun ⟨_, P, _, idx⟩ => if idx == some i then P.map (bagUnion · B) else []
  let res := (out ++ tail).map (bagUnion · D)
  (if res.isEmpty then [D] else res, fl)

/-- `undo` without the flag. -/
def undo (F : Graph) (ops : List Op) (R : Graph) (bagsR : List Bag) : List Bag :=
  (undoF F ops R bagsR).1

/-! ## The algorithms (sweep.py lines 191-241) -/

/-- Python `algo_T1(G, rng, h)` (lines 195-197) with the labels `Y` given:
`switched_layout(G, Y)`. (Final.) -/
def algoT1F (G : Graph) (Y : Labels) : List Bag × Bool := switchedLayoutF G Y

/-- `algo_T1` without the flag. -/
def algoT1 (G : Graph) (Y : Labels) : List Bag := (algoT1F G Y).1

/-- Python `algo_T2a(G, rng, h)` (lines 200-202) with the labels `Y` given:
`plain_layout(G, Y)`. (Final.) -/
def algoT2a (G : Graph) (Y : Labels) : List Bag := plainLayout G Y

/-- Python `algo_mixed(G, rng, h)` (lines 205-209):
`(H, ops, f1) := reduceRecordF G.copy`;
`bagsH := if H.numNodes = 0 then [] else plainLayout H (lab H)`;
`(bags, f2) := undoF G ops H bagsH`; result `(bags, f1 || f2)`.
Contract (`AlgoMixedValid`): valid for every `G.WF` and every labeler. -/
def algoMixedF (G : Graph) (lab : Labeler) : List Bag × Bool :=
  let r := reduceRecordF G.copy
  let H := r.1
  let bagsH := if H.numNodes = 0 then [] else plainLayout H (lab H)
  let u := undoF G r.2.1 H bagsH
  (u.1, r.2.2 || u.2)

/-- `algo_mixed` without the flag. -/
def algoMixed (G : Graph) (lab : Labeler) : List Bag := (algoMixedF G lab).1

/-- The kind of a final component in `algo_T4`. -/
inductive FinalKind where
  | sweep
  | thin
  deriving BEq, Repr, Inhabited, DecidableEq

/-- An entry `(J, kind, tops)` of Python's `final` (`tops = []` for Python `None`). -/
structure FinalEntry where
  graph : Graph
  kind : FinalKind
  tops : List Op
  deriving Inhabited

/-- The result of `algo_T4`: Python's `(bags, Dn, final)` plus the fallback flag. -/
structure T4Result where
  bags : List Bag
  numDeleted : Nat
  final : List FinalEntry
  fallback : Bool
  deriving Inhabited

/-- Python lines 223-225: among the nodes of maximum degree `Dl := J.maxDegree`
(`cands`, node order), those with a neighbour of smaller degree (`good`); the result
is the numerically smallest element of `good` if nonempty, else of `cands`
(`min(good or cands)`), `0` if `J` is empty. -/
def t4ChooseW (J : Graph) : Nat :=
  let Dl := J.maxDegree
  let cands := J.nodes.filter fun v => J.degree v == Dl
  let good := cands.filter fun v => (J.nbrs v).any fun u => J.degree u < Dl
  let pool := if good.isEmpty then cands else good
  (pool.min?).getD 0

/-- The `while work:` loop of `algo_T4` (lines 218-230). `stack` is Python's `work`
(head = Python end), `final` is Python's `final` (in Python order), `ops` the global
ops (chronological). One step with `fuel + 1`, `J :: stack`:
* if `J.maxDegree ≤ 5`: `final := final ++ [⟨J, .sweep, []⟩]`;
* else `w := t4ChooseW J`, `(Js, red, f) := reduceRecordF (J.copy.removeNode w)`,
  `tops := .del w :: red`; if `Js.numNodes = 0` then `final := final ++ [⟨J, .thin, tops⟩]`,
  else `ops := ops ++ tops` and push the components of `Js`
  (Python `work += [Js.subgraph(c).copy() for c in nx.connected_components(Js)]`, so
  `stack := (componentGraphs Js).reverse ++ stack`).
Empty stack: `(final, ops, false)`. Fuel `0` with a nonempty stack: FALLBACK, the
remaining graphs (in stack order) are appended to `final` as `.sweep` entries, flag
`true`. The flag also includes every `f`. Fuel bound: `2 * numNodes` rounds. -/
def t4Loop (fuel : Nat) (stack : List Graph) (final : List FinalEntry) (ops : List Op) :
    List FinalEntry × List Op × Bool :=
  match fuel, stack with
  | _, [] => (final, ops, false)
  | 0, _ :: _ => (final ++ stack.map fun J => FinalEntry.mk J FinalKind.sweep [], ops, true)
  | fuel + 1, J :: rest =>
    if J.maxDegree ≤ 5 then
      t4Loop fuel rest (final ++ [FinalEntry.mk J FinalKind.sweep []]) ops
    else
      let w := t4ChooseW J
      let red := reduceRecordF (J.copy.removeNode w)
      let tops := Op.del w :: red.2.1
      if red.1.numNodes = 0 then
        let r := t4Loop fuel rest (final ++ [FinalEntry.mk J FinalKind.thin tops]) ops
        (r.1, r.2.1, r.2.2 || red.2.2)
      else
        let r := t4Loop fuel ((componentGraphs red.1).reverse ++ rest) final (ops ++ tops)
        (r.1, r.2.1, r.2.2 || red.2.2)

/-- The decomposition of a final component (lines 234-237): `.sweep` →
`(plainLayout e.graph (lab e.graph), false)`; `.thin` →
`undoF e.graph e.tops Graph.empty []`. -/
def t4Decompose (lab : Labeler) (e : FinalEntry) : List Bag × Bool :=
  match e.kind with
  | .sweep => (plainLayout e.graph (lab e.graph), false)
  | .thin => undoF e.graph e.tops Graph.empty []

/-- Python `algo_T4(G, rng, h)` (lines 212-241) under model M:
* `G0 := nonIsolated G`; `(H, ops0, f0) := reduceRecordF G0.copy`;
* `work := componentGraphs H` (Python order);
* `(final, ops, f1) := t4Loop (2 * H.numNodes + 1) work.reverse [] ops0`;
* `R := unionAll (final.map (·.graph))`; `parts := final.map (t4Decompose lab)`;
  `bagsR := parts.flatMap (·.1)`;
* `(bags, f2) := undoF G0 ops R bagsR`; result bags `bags ++ isolatedBags G`;
* `numDeleted := (deletedSet ops).length`; `fallback := f0 || f1 || any parts flag || f2`.
Contract (`AlgoT4Valid`): valid for every `G.WF` and every labeler. -/
def algoT4Full (G : Graph) (lab : Labeler) : T4Result :=
  let G0 := nonIsolated G
  let r0 := reduceRecordF G0.copy
  let H := r0.1
  let work := componentGraphs H
  let lp := t4Loop (2 * H.numNodes + 1) work.reverse [] r0.2.1
  let final := lp.1
  let R := unionAll (final.map (·.graph))
  let parts := final.map (t4Decompose lab)
  let bagsR := parts.flatMap (·.1)
  let u := undoF G0 lp.2.1 R bagsR
  ⟨u.1 ++ isolatedBags G, (deletedSet lp.2.1).length, final,
    r0.2.2 || lp.2.2 || parts.any (·.2) || u.2⟩

/-- `algo_T4`'s bags. -/
def algoT4 (G : Graph) (lab : Labeler) : List Bag := (algoT4Full G lab).bags

end CubicPathwidth.Alg