CubicPathwidth.Alg.Graph

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

import Std.Data.HashMap
import Std.Data.HashSet

/-!
# A networkx-like graph type for the port of `sweep.py`

This file mirrors the parts of `networkx.Graph` (networkx 3.7, CPython 3.14) that
`ancillary/experiments/sweep-algorithms/sweep.py` uses, with the SAME iteration orders, so that
the Lean port in `Port.lean` can be compared exactly with the Python implementation.

## Representation

`Graph` stores
* `nodes : List Nat` — the keys of networkx's `G._node`, in insertion order
  (Python `for v in G`);
* `adj : Std.HashMap Nat (List Nat)` — `adj[v]` is the list of keys of `G._adj[v]`,
  in insertion order (Python `for u in G[v]`).

Why this choice.
* Exact orders: Python dicts are insertion ordered; a `List` per vertex and a `List` of
  nodes reproduce this exactly, including `remove_node` (deletion keeps the order of the
  others) and `add_edge` (appends to both lists, no-op if present).
* Speed: `mem`, `nbrs` are hash lookups; `removeNode` is `O(n + deg)`; `induced`
  (= `subgraph(S).copy()`) is `O(n + m·deg)`. This is fine for `n` up to a few
  thousand, even in the interpreter (`lake env lean --run`), for the sizes the
  differential harness uses.
* Proofs: everything is stated through `G.nodes`, `G.nbrs v` and `G.mem v`; the
  `Std.HashMap` lemmas needed are `getD_insert`, `getD_erase`, `contains_insert`,
  `contains_erase`, `getD_empty`, `contains_empty`. The predicate `Graph.WF` collects
  what networkx guarantees (symmetric, loopless, duplicate-free).

Vertices are natural numbers (the harness only produces integer-labelled graphs).

## Iteration model (the semantics the port follows)

Model "M": CPython + networkx 3.7, except that
1. a subgraph VIEW `G.subgraph(S)` iterates its nodes in the parent's node order
   (networkx does this whenever `2|S| ≥ |G|`; otherwise it iterates the Python set `S`);
2. in `switched_layout`, `connector_order` receives `Wp` and the items in the node
   order of `G` (Python iterates the sets `Wp` and `Up`).
Under M, `G.subgraph(S).copy()` is `G.induced (· ∈ S)` below. The harness
`lean_diff.py` runs `sweep.py` under M (by monkeypatching networkx's filter views and
wrapping `connector_order`, never editing `sweep.py`), and checks on the atlas graphs
(all labels < 8, so every CPython int set iterates increasingly and all node orders
are increasing) that M and unpatched CPython give identical outputs.

## Copy semantics (important, verified against networkx)

`G.copy()` and `G.subgraph(S).copy()` do NOT keep adjacency orders: they re-add the
edges with `add_edges_from` while scanning `u` in node order and `v ∈ G[u]`, so in the
copy, `adj[x]` = (neighbours of `x` that precede `x` in node order, in node order) ++
(the remaining neighbours of `x`, in the old order of `adj[x]`). `induced` reproduces
this literally by calling `addEdge` in the same order.
-/

namespace CubicPathwidth.Alg

/-- A bag of a path decomposition, read as a SET (Python bags are sets). Duplicates
are harmless: validity only uses membership, widths use the deduplicated size, and
the harness compares bags after sorting and deduplicating. -/
abbrev Bag := List Nat

/-- An undirected graph with networkx insertion orders. See the module docstring. -/
structure Graph where
  /-- Python `list(G)`: nodes in insertion order. -/
  nodes : List Nat
  /-- Python `list(G[v])` for each node `v`; absent keys mean "not a node". -/
  adj : Std.HashMap Nat (List Nat)

instance : Inhabited Graph := ⟨⟨[], ∅⟩⟩

namespace Graph

/-- `nx.Graph()`. -/
def empty : Graph := ⟨[], ∅⟩

/-- Python `v in G`. -/
def mem (G : Graph) (v : Nat) : Bool := G.adj.contains v

/-- Python `list(G[v])` (empty if `v` is not a node). -/
def nbrs (G : Graph) (v : Nat) : List Nat := G.adj.getD v []

/-- Python `G.degree(v)`. -/
def degree (G : Graph) (v : Nat) : Nat := (G.nbrs v).length

/-- Python `G.number_of_nodes()`. -/
def numNodes (G : Graph) : Nat := G.nodes.length

/-- Python `G.has_edge(u, v)`. -/
def hasEdge (G : Graph) (u v : Nat) : Bool := (G.nbrs u).contains v

/-- Adjacency as a proposition: `v` is listed among the neighbours of `u`. -/
def Adj (G : Graph) (u v : Nat) : Prop := v ∈ G.nbrs u

/-- `max(d for _, d in G.degree())`, with default `0` for the empty graph. -/
def maxDegree (G : Graph) : Nat := G.nodes.foldl (fun m v => max m (G.degree v)) 0

/-- Every node has degree at most `k`. -/
def MaxDegLE (G : Graph) (k : Nat) : Prop := ∀ v ∈ G.nodes, G.degree v ≤ k

/-- Python `G.add_node(v)`: appended at the end if absent, no-op otherwise. -/
def addNode (G : Graph) (v : Nat) : Graph :=
  if G.mem v then G else ⟨G.nodes ++ [v], G.adj.insert v []⟩

/-- One half of `add_edge`: Python `G._adj[u][v] = dd`, i.e. append `v` to the
neighbour list of `u` unless it is already there (assumes `u` is a node). -/
def appendNbr (G : Graph) (u v : Nat) : Graph :=
  let l := G.nbrs u
  if l.contains v then G else { G with adj := G.adj.insert u (l ++ [v]) }

/-- Python `G.add_edge(u, v)`: add missing nodes (`u` first), then
`adj[u][v] = dd; adj[v][u] = dd` (append if absent, keep position if present). -/
def addEdge (G : Graph) (u v : Nat) : Graph :=
  (((G.addNode u).addNode v).appendNbr u v).appendNbr v u

/-- Python `G.remove_node(v)` (a no-op if `v` is absent; Python would raise):
delete `v` from each neighbour's list, then delete `v` itself. Orders of the
remaining entries are kept. -/
def removeNode (G : Graph) (v : Nat) : Graph :=
  if G.mem v then
    let adj := (G.nbrs v).foldl (fun a u => a.insert u ((a.getD u []).erase v)) G.adj
    ⟨G.nodes.erase v, adj.erase v⟩
  else G

/-- Python `G.subgraph(S).copy()` under model M, and `G.copy()` for `keep = fun _ => true`.

Nodes: `G.nodes.filter keep` (parent order). Edges: re-added with `addEdge` while
scanning `u` in that order and `v ∈ G.nbrs u` with `keep v`, exactly as networkx's
`copy` does (`add_edges_from` over `self._adj.items()`). The node list is built
directly; this equals folding `addNode` because `G.nodes` is duplicate-free for a
well-formed graph. -/
def induced (G : Graph) (keep : Nat → Bool) : Graph :=
  let ns := G.nodes.filter keep
  let H : Graph := ⟨ns, ns.foldl (fun a v => a.insert v []) ∅⟩
  ns.foldl (fun H u => (G.nbrs u).foldl (fun H v => if keep v then H.addEdge u v else H) H) H

/-- Python `G.copy()`. -/
def copy (G : Graph) : Graph := G.induced (fun _ => true)

/-- Python `list(G.edges())`: for `u` in node order, the neighbours `v ∈ G[u]` that
are not earlier nodes (networkx's `EdgeView.__iter__`). -/
def edgeList (G : Graph) : List (Nat × Nat) :=
  let step := fun (acc : Std.HashSet Nat × Array (Nat × Nat)) (u : Nat) =>
    let (seen, out) := acc
    let out := (G.nbrs u).foldl (fun o v => if seen.contains v then o else o.push (u, v)) out
    (seen.insert u, out)
  (G.nodes.foldl step (∅, #[])).2.toList

/-- Python `R.add_nodes_from(J); R.add_edges_from(J.edges())`. -/
def addGraph (R J : Graph) : Graph :=
  J.edgeList.foldl (fun R e => R.addEdge e.1 e.2) (J.nodes.foldl addNode R)

/-- The union of a list of graphs, built as in `algo_T4` (`R = nx.Graph()` and
`addGraph` for each graph in order). -/
def unionAll (gs : List Graph) : Graph := gs.foldl addGraph empty

/-- Depth-first reachability: `reachAux fuel stack seen` pops `x` from `stack`, marks
and pushes its unseen neighbours. Returns `none` if the fuel runs out first. Every
vertex is pushed at most once (when it is marked), so fuel `numNodes + 1` suffices
for a well-formed graph. -/
def reachAux (G : Graph) : Nat → List Nat → Std.HashSet Nat → Option (Std.HashSet Nat)
  | _, [], seen => some seen
  | 0, _ :: _, _ => none
  | fuel + 1, x :: rest, seen =>
    let r := (G.nbrs x).foldl
      (fun (acc : Std.HashSet Nat × List Nat) y =>
        if acc.1.contains y then acc else (acc.1.insert y, y :: acc.2)) (seen, rest)
    reachAux G fuel r.2 r.1

/-- Python `list(nx.connected_components(G))`, components listed in the order networkx
yields them (by their first vertex in node order). Each component is returned as a
LIST in node order (Python returns sets; under model M only membership and size of a
component are used). Fallback (never used for well-formed graphs): if a search runs
out of fuel, all not yet assigned nodes form the last component, which keeps the
result a partition into neighbour-closed parts. -/
def components (G : Graph) : List (List Nat) :=
  go G.nodes ∅ []
where
  go : List Nat → Std.HashSet Nat → List (List Nat) → List (List Nat)
  | [], _, acc => acc.reverse
  | v :: vs, assigned, acc =>
    if assigned.contains v then go vs assigned acc
    else
      match G.reachAux (G.numNodes + 1) [v] (({} : Std.HashSet Nat).insert v) with
      | some r =>
        let comp := G.nodes.filter r.contains
        go vs (comp.foldl (fun s x => s.insert x) assigned) (comp :: acc)
      | none =>
        ((G.nodes.filter (fun x => !assigned.contains x)) :: acc).reverse

/-- Build a graph from explicit orders (used for JSON input): `nodes` in order and,
for each node, its neighbour list in order. No checks are made. -/
def ofAdjLists (nodes : List Nat) (adjs : List (List Nat)) : Graph :=
  ⟨nodes, (nodes.zip adjs).foldl (fun a p => a.insert p.1 p.2) ∅⟩

/-- The neighbour lists in node order (for printing and JSON output). -/
def adjLists (G : Graph) : List (List Nat) := G.nodes.map G.nbrs

instance : Repr Graph where
  reprPrec G _ := repr (G.nodes.map fun v => (v, G.nbrs v))

/-- Well-formedness: what networkx guarantees for a simple undirected `nx.Graph`
built by the operations above. -/
structure WF (G : Graph) : Prop where
  nodup : G.nodes.Nodup
  mem_iff : ∀ v, G.mem v = true ↔ v ∈ G.nodes
  nbrs_nodup : ∀ v, (G.nbrs v).Nodup
  nbrs_sub : ∀ u v, v ∈ G.nbrs u → v ∈ G.nodes
  symm : ∀ u v, v ∈ G.nbrs u → u ∈ G.nbrs v
  loopless : ∀ v, v ∉ G.nbrs v

end Graph

/-- Python `B | X` for bags: union read as a set (here concatenation). -/
def bagUnion (B X : Bag) : Bag := B ++ X

/-- Python `S <= B` for sets given as lists. -/
def subsetB (S B : List Nat) : Bool := S.all B.contains

/-! ## Sanity checks against networkx (outputs recorded from networkx 3.7) -/

section Checks
open Graph

-- networkx: G = Graph(); add_nodes_from([5,1,9,3]);
-- add_edges_from([(9,1),(9,5),(3,9),(1,3),(5,1)])

private def g0 : Graph :=
  [(9, 1), (9, 5), (3, 9), (1, 3), (5, 1)].foldl (fun G e => G.addEdge e.1 e.2)
    ([5, 1, 9, 3].foldl addNode empty)

-- networkx: {5: [9, 1], 1: [9, 3, 5], 9: [1, 5, 3], 3: [9, 1]}
#guard (g0.nodes, g0.adjLists) == ([5, 1, 9, 3], [[9, 1], [9, 3, 5], [1, 5, 3], [9, 1]])
-- networkx copy: {5: [9, 1], 1: [5, 9, 3], 9: [5, 1, 3], 3: [1, 9]}
#guard (g0.copy.nodes, g0.copy.adjLists) == ([5, 1, 9, 3], [[9, 1], [5, 9, 3], [5, 1, 3], [1, 9]])
-- networkx subgraph({9,1,3}).copy(): nodes [1, 9, 3], {1: [9, 3], 9: [1, 3], 3: [1, 9]}
#guard ((g0.induced ([9, 1, 3].contains ·)).nodes,
    (g0.induced ([9, 1, 3].contains ·)).adjLists) == ([1, 9, 3], [[9, 3], [1, 3], [1, 9]])
-- networkx remove_node(1): nodes [5, 9, 3], {5: [9], 9: [5, 3], 3: [9]}
#guard ((g0.removeNode 1).nodes, (g0.removeNode 1).adjLists) == ([5, 9, 3], [[9], [5, 3], [9]])
-- then add_edge(3, 5): {5: [9, 3], 9: [5, 3], 3: [9, 5]}
#guard (((g0.removeNode 1).addEdge 3 5).adjLists) == [[9, 3], [5, 3], [9, 5]]
-- add_edge of an existing edge is a no-op
#guard ((g0.addEdge 1 9).adjLists) == g0.adjLists
-- edges(): [(5, 9), (5, 1), (1, 9), (1, 3), (9, 3)]
#guard g0.edgeList == [(5, 9), (5, 1), (1, 9), (1, 3), (9, 3)]
-- components of a graph with isolated vertices and two paths

private def g1 : Graph :=
  [(4, 2), (0, 6), (2, 7)].foldl (fun G e => G.addEdge e.1 e.2)
    ([7, 0, 3, 4, 2, 6].foldl addNode empty)
#guard g1.components == [[7, 4, 2], [0, 6], [3]]
#guard (g1.removeNode 2).components == [[7], [0, 6], [3], [4]]
#guard g1.maxDegree == 2
#guard (unionAll [g1.induced ([0, 6].contains ·), g0]).nodes == [0, 6, 5, 1, 9, 3]

end Checks

end CubicPathwidth.Alg