CubicPathwidth.Alg.Spec

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

import CubicPathwidth
import CubicPathwidth.Alg.Port

/-!
# Validity statements for the port of `sweep.py` (Stage 1 approval surface)

STATUS: DRAFT FOR APPROVAL. Every `def … : Prop` below is a proposition that we DEFINE;
nothing is proved here and nothing is assumed. Proofs go in separate files
(`CubicPathwidth/Alg/Proofs/*.lean`), one theorem per Prop, e.g.
`theorem plainLayoutValid : PlainLayoutValid`.

Sections.
1. `ValidPD` (mirror of `check_pd`) and `BagsWithin`.
2. Bridge to the frozen `PathDecomposition` / `HasPathwidthAtMost` of `CubicPathwidth.lean`.
3. Graph-operation facts used by the proofs.
4. Contracts of the ported functions.
5. Bookkeeping of the deletion process (`algo_T4`).
6. Top-level validity, and the exported statements on `SimpleGraph (Fin n)`.
7. Stage 2: the fallbacks never fire (believed true; not needed for validity).

Every statement is about the Lean semantics, which coincides with `sweep.py` under the
iteration model M whenever Python does not raise; the fallbacks replace the Python
exceptions and keep the outputs valid. The top-level statements (Section 6) are stated
for every graph and every labeling; `AlgoT1Valid` has the degree hypothesis that
Python needs, and `SwitchedLayoutValid` shows the Lean version needs none.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

/-! ## 1. Path decompositions over `Graph` -/

/-- Vertex `v` lies in the bag with index `i`. -/
def InBag (bags : List Bag) (i v : Nat) : Prop :=
  ∃ B, bags[i]? = some B ∧ v ∈ B

/-- Mirror of Python `check_pd(G, bags)` (sweep.py lines 19-30): every node of `G` is in
some bag; the bags containing a node of `G` form an interval of indices; every edge of
`G` lies in some bag. Vertices outside `G` are ignored, as in `check_pd`. -/
def ValidPD (G : Graph) (bags : List Bag) : Prop :=
  (∀ v ∈ G.nodes, ∃ i, InBag bags i v) ∧
  (∀ v ∈ G.nodes, ∀ i j k, i ≤ j → j ≤ k → InBag bags i v → InBag bags k v → InBag bags j v) ∧
  (∀ u v, u ∈ G.nodes → G.Adj u v → ∃ B ∈ bags, u ∈ B ∧ v ∈ B)

/-- Every bag only contains nodes of `G` (needed to compose decompositions). -/
def BagsWithin (G : Graph) (bags : List Bag) : Prop :=
  ∀ B ∈ bags, ∀ v ∈ B, v ∈ G.nodes

/-- The largest bag size (bags read as sets), `0` for no bags. -/
def maxBagCard (bags : List Bag) : Nat :=
  (bags.map fun B => B.toFinset.card).foldr max 0

/-- Python's width `max(len(B)) - 1` (and `-1` for no bags, matching the frozen
convention for the empty graph). -/
def pdWidth (bags : List Bag) : ℝ := (maxBagCard bags : ℝ) - 1

/-! ## 2. Bridge to the frozen specification -/

/-- The simple graph on `Fin n` with `u ~ v` iff `u ≠ v` and one lists the other. -/
def Graph.toSimpleGraph (G : Graph) (n : ℕ) : SimpleGraph (Fin n) :=
  SimpleGraph.fromRel fun u v => G.Adj u.val v.val

/-- The `Graph` of a simple graph on `Fin n`: nodes `0, …, n-1`, neighbours increasing. -/
def Graph.ofSimpleGraph {n : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] : Graph :=
  Graph.ofAdjLists (List.range n)
    ((List.finRange n).map fun u => ((List.finRange n).filter fun v => decide (S.Adj u v)).map Fin.val)

/-- A valid decomposition of a well-formed graph on the vertex set `{0, …, n-1}` gives
`HasPathwidthAtMost` for its simple graph, with the width of the bags. (If `bags = []`,
then `n = 0` and one empty bag is used.) -/
def ValidPDBridge : Prop :=
  ∀ (n : ℕ) (G : Graph) (bags : List Bag), G.WF → (∀ v, v ∈ G.nodes ↔ v < n) →
    ValidPD G bags → HasPathwidthAtMost (G.toSimpleGraph n) (pdWidth bags)

/-- `ofSimpleGraph` is well formed, has vertex set `{0, …, n-1}`, gives back `S`, and
keeps the degree bound of `IsSubcubic`. -/
def OfSimpleGraphSpec : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
    (Graph.ofSimpleGraph S).WF ∧
    (∀ v, v ∈ (Graph.ofSimpleGraph S).nodes ↔ v < n) ∧
    (Graph.ofSimpleGraph S).toSimpleGraph n = S ∧
    (IsSubcubic S → (Graph.ofSimpleGraph S).MaxDegLE 3)

/-! ## 3. Graph-operation facts -/

/-- `G.WF` gives `mem` as membership in `nodes`, and adjacency only between nodes. -/
def WFBasics : Prop :=
  ∀ G : Graph, G.WF → ∀ u v, G.Adj u v → u ∈ G.nodes ∧ v ∈ G.nodes ∧ G.Adj v u ∧ u ≠ v

/-- `addEdge` of two distinct vertices. -/
def AddEdgeSpec : Prop :=
  ∀ (G : Graph) (u v : Nat), G.WF → u ≠ v →
    (G.addEdge u v).WF ∧
    (∀ x, x ∈ (G.addEdge u v).nodes ↔ x ∈ G.nodes ∨ x = u ∨ x = v) ∧
    (∀ x y, (G.addEdge u v).Adj x y ↔ G.Adj x y ∨ (x = u ∧ y = v) ∨ (x = v ∧ y = u))

/-- `removeNode`. -/
def RemoveNodeSpec : Prop :=
  ∀ (G : Graph) (v : Nat), G.WF →
    (G.removeNode v).WF ∧
    (∀ x, x ∈ (G.removeNode v).nodes ↔ x ∈ G.nodes ∧ x ≠ v) ∧
    (∀ x y, (G.removeNode v).Adj x y ↔ G.Adj x y ∧ x ≠ v ∧ y ≠ v)

/-- `induced` (Python `subgraph(S).copy()`; `copy` is the case `keep = fun _ => true`). -/
def InducedSpec : Prop :=
  ∀ (G : Graph) (keep : Nat → Bool), G.WF →
    (G.induced keep).WF ∧
    (∀ x, x ∈ (G.induced keep).nodes ↔ x ∈ G.nodes ∧ keep x = true) ∧
    (∀ x y, (G.induced keep).Adj x y ↔ G.Adj x y ∧ keep x = true ∧ keep y = true)

/-- `components`: a partition of the nodes into nonempty, neighbour-closed parts. -/
def ComponentsSpec : Prop :=
  ∀ G : Graph, G.WF →
    G.components.flatten.Perm G.nodes ∧
    (∀ c ∈ G.components, c ≠ []) ∧
    (∀ c ∈ G.components, ∀ x ∈ c, ∀ y, G.Adj x y → y ∈ c)

/-- `unionAll` (Python `R.add_nodes_from(J); R.add_edges_from(J.edges())`). -/
def UnionAllSpec : Prop :=
  ∀ gs : List Graph, (∀ J ∈ gs, J.WF) →
    (unionAll gs).WF ∧
    (∀ x, x ∈ (unionAll gs).nodes ↔ ∃ J ∈ gs, x ∈ J.nodes) ∧
    (∀ x y, (unionAll gs).Adj x y ↔ ∃ J ∈ gs, J.Adj x y)

/-- Concatenating decompositions of vertex-disjoint graphs decomposes their union. -/
def ConcatValid : Prop :=
  ∀ parts : List (Graph × List Bag),
    (∀ p ∈ parts, p.1.WF ∧ ValidPD p.1 p.2 ∧ BagsWithin p.1 p.2) →
    parts.Pairwise (fun A B => ∀ x, x ∈ A.1.nodes → x ∉ B.1.nodes) →
    ValidPD (unionAll (parts.map (·.1))) (parts.flatMap (·.2)) ∧
      BagsWithin (unionAll (parts.map (·.1))) (parts.flatMap (·.2))

/-- Gluing at a separator `X` (the shape of `pd_tw2`): if `parts` lists sets `c` that
partition the nodes outside `X`, each closed under adjacency up to `X`, with valid
decompositions inside `H[c]`, then adding `X` to every bag of their concatenation (or
taking the single bag `X` if there is no bag) decomposes `H`. -/
def SeparatorGlueValid : Prop :=
  ∀ (H : Graph) (X : List Nat) (parts : List (List Nat × List Bag)),
    H.WF → (∀ x ∈ X, x ∈ H.nodes) →
    (parts.map (·.1)).flatten.Perm (H.nodes.filter fun v => !X.contains v) →
    (∀ p ∈ parts, ∀ x ∈ p.1, ∀ y, H.Adj x y → y ∈ p.1 ∨ y ∈ X) →
    (∀ p ∈ parts, ValidPD (H.induced p.1.contains) p.2 ∧
      BagsWithin (H.induced p.1.contains) p.2) →
    let out := parts.flatMap fun p => p.2.map (bagUnion · X)
    let res := if out.isEmpty then [X] else out
    ValidPD H res ∧ BagsWithin H res

/-! ## 4. Contracts of the ported functions -/

/-- `plainOrder` is a permutation of the nodes. -/
def PlainOrderPerm : Prop :=
  ∀ (G : Graph) (Y : Labels), (plainOrder G Y).Perm G.nodes

/-- The plain sweep (`plain_layout`) is valid for every graph and labeling. -/
def PlainLayoutValid : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels,
    ValidPD G (plainLayout G Y) ∧ BagsWithin G (plainLayout G Y)

/-- `connector_order` outputs exactly the elements of `Qs` (fallback included). This is
all that the validity of the switched layout uses. -/
def ConnectorOrderMem : Prop :=
  ∀ (Qs : List Nat) (items : List (List Nat)), (∀ e ∈ items, ∀ z ∈ e, z ∈ Qs) →
    ∀ x, x ∈ connectorOrder Qs items ↔ x ∈ Qs

/-- `switchedOrder` is a permutation of the nodes. -/
def SwitchedOrderPerm : Prop :=
  ∀ (G : Graph) (Y : Labels), (switchedOrder G Y).Perm G.nodes

/-- The median-switched layout is valid for EVERY graph and labeling (with the
connector fallback; Python can raise `IndexError` when the maximum degree is `≥ 4`). -/
def SwitchedLayoutValid : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels,
    ValidPD G (switchedLayout G Y) ∧ BagsWithin G (switchedLayout G Y)

/-- `reduce_record`: the result is a well-formed graph on a subset of the nodes, keeps
every edge between surviving vertices, and its ops are reductions of nodes of `G` that
no longer survive, covering every removed node. -/
def ReduceRecordSpec : Prop :=
  ∀ G : Graph, G.WF →
    let r := reduceRecord G
    r.1.WF ∧
    (∀ x, x ∈ r.1.nodes → x ∈ G.nodes) ∧
    (∀ x y, x ∈ r.1.nodes → y ∈ r.1.nodes → G.Adj x y → r.1.Adj x y) ∧
    (∀ o ∈ r.2, ∃ v nb, o = Op.red v nb ∧ v ∈ G.nodes ∧ v ∉ r.1.nodes ∧ ∀ x ∈ nb, x ∈ G.nodes) ∧
    (∀ x ∈ G.nodes, x ∈ r.1.nodes ∨ x ∈ redVertices r.2)

/-- `pd_tw2` is valid for every graph (fallbacks included). -/
def PdTw2Valid : Prop :=
  ∀ H : Graph, H.WF → ValidPD H (pdTw2 H) ∧ BagsWithin H (pdTw2 H)

/-- `undo` (Lemma A.28, `lem:undo`) is valid under these preconditions: `R` is a well-formed graph on
nodes of `F` outside the deleted set (I0), containing every edge of `F` between its
nodes (I1), and `bagsR` is a valid decomposition of `R` inside `R`. Invariant (I2),
which Python asserts, is NOT needed for validity (if it fails the fallback fires).
The calls in `algoMixed` (with `R = H`, `D = ∅`), in `t4Decompose` (with `R` empty) and
in `algoT4Full` (with `R` the union of the final components) satisfy them. -/
def UndoValid : Prop :=
  ∀ (F R : Graph) (ops : List Op) (bagsR : List Bag),
    F.WF → R.WF →
    (∀ x ∈ R.nodes, x ∈ F.nodes ∧ x ∉ deletedSet ops) →
    (∀ x y, x ∈ R.nodes → y ∈ R.nodes → F.Adj x y → R.Adj x y) →
    ValidPD R bagsR → BagsWithin R bagsR →
    ValidPD F (undo F ops R bagsR) ∧
      ((∀ x ∈ deletedSet ops, x ∈ F.nodes) → BagsWithin F (undo F ops R bagsR))

/-! ## 5. Bookkeeping of the deletion process (`algo_T4`) -/

/-- The invariant of the work loop of `algo_T4` relative to `G0` (Python's `G0`), for
the list `gs` of graphs in `work` and in `final`, and the global `ops`: the graphs are
well formed and pairwise vertex-disjoint, their nodes are nodes of `G0` outside the
deleted set, the deleted vertices are nodes of `G0`, and every edge of `G0` between
two vertices that occur in `gs` is an edge of one graph of `gs`. -/
def T4Inv (G0 : Graph) (gs : List Graph) (ops : List Op) : Prop :=
  (∀ J ∈ gs, J.WF) ∧
  gs.Pairwise (fun A B => ∀ x, x ∈ A.nodes → x ∉ B.nodes) ∧
  (∀ J ∈ gs, ∀ x ∈ J.nodes, x ∈ G0.nodes ∧ x ∉ deletedSet ops) ∧
  (∀ x ∈ deletedSet ops, x ∈ G0.nodes) ∧
  (∀ x y, G0.Adj x y → (∃ J ∈ gs, x ∈ J.nodes) → (∃ J ∈ gs, y ∈ J.nodes) →
    ∃ J ∈ gs, J.Adj x y)

/-- Thin entries record the deletion of one of their own vertices. -/
def ThinOK (final : List FinalEntry) : Prop :=
  ∀ e ∈ final, ∀ x ∈ deletedSet e.tops, x ∈ e.graph.nodes

/-- The invariant holds for the initial work list. -/
def T4InitInv : Prop :=
  ∀ G : Graph, G.WF →
    let r := reduceRecordF (nonIsolated G).copy
    T4Inv (nonIsolated G) (componentGraphs r.1) r.2.1

/-- One run of the work loop preserves the invariant and `ThinOK`. -/
def T4LoopPreserves : Prop :=
  ∀ (G0 : Graph) (fuel : Nat) (stack : List Graph) (final : List FinalEntry) (ops : List Op),
    G0.WF → T4Inv G0 (stack ++ final.map (·.graph)) ops → ThinOK final →
    let r := t4Loop fuel stack final ops
    T4Inv G0 (r.1.map (·.graph)) r.2.1 ∧ ThinOK r.1

/-- Appending one bag per isolated vertex extends a decomposition of `nonIsolated G`
(inside it) to one of `G`. -/
def AppendIsolatedValid : Prop :=
  ∀ G : Graph, G.WF → ∀ bags : List Bag,
    ValidPD (nonIsolated G) bags → BagsWithin (nonIsolated G) bags →
    ValidPD G (bags ++ isolatedBags G)

/-! ## 6. Top-level validity -/

/-- Theorem 1 algorithm (`algo_T1`): valid for every graph of maximum degree `≤ 3` and
every labeling. -/
def AlgoT1Valid : Prop :=
  ∀ G : Graph, G.WF → G.MaxDegLE 3 → ∀ Y : Labels, ValidPD G (algoT1 G Y)

/-- Theorem 2(a) algorithm (`algo_T2a`): valid for every graph and labeling. -/
def AlgoT2aValid : Prop :=
  ∀ G : Graph, G.WF → ∀ Y : Labels, ValidPD G (algoT2a G Y)

/-- Theorems 2(b,c), 3 algorithm (`algo_mixed`): valid for every graph and labeler. -/
def AlgoMixedValid : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, ValidPD G (algoMixed G lab)

/-- Theorem 4 algorithm (`algo_T4`): valid for every graph and labeler. -/
def AlgoT4Valid : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, ValidPD G (algoT4 G lab)

/-- Exported form on the frozen types: Theorem 1 algorithm. -/
def AlgoT1Exported : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj], IsSubcubic S →
    ∀ Y : Labels, HasPathwidthAtMost S (pdWidth (algoT1 (Graph.ofSimpleGraph S) Y))

/-- Exported form: Theorem 2(a) algorithm. -/
def AlgoT2aExported : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
    ∀ Y : Labels, HasPathwidthAtMost S (pdWidth (algoT2a (Graph.ofSimpleGraph S) Y))

/-- Exported form: mixed algorithm. -/
def AlgoMixedExported : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
    ∀ lab : Labeler, HasPathwidthAtMost S (pdWidth (algoMixed (Graph.ofSimpleGraph S) lab))

/-- Exported form: Theorem 4 algorithm. -/
def AlgoT4Exported : Prop :=
  ∀ (n : ℕ) (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
    ∀ lab : Labeler, HasPathwidthAtMost S (pdWidth (algoT4 (Graph.ofSimpleGraph S) lab))

/-! ## 7. Stage 2: the fallbacks never fire (not needed for validity)

These say that the Lean port computes exactly what `sweep.py` computes (under model M)
on every input where Python is claimed not to raise. They follow from Lemma A.33 (`lem:connector-linear`) of the
paper (connector), Claims 9 and 10 and invariants (I1), (I2) of the reduction lemma
(pd_tw2 and undo), and the counting bounds behind the fuels. -/

/-- The connector greedy never runs dry when every item has one or two elements. -/
def ConnectorNoFallback : Prop :=
  ∀ (Qs : List Nat) (items : List (List Nat)), Qs.Nodup →
    (∀ e ∈ items, e.Nodup ∧ 1 ≤ e.length ∧ e.length ≤ 2 ∧ ∀ z ∈ e, z ∈ Qs) →
    (connectorOrderF Qs items).2 = false

/-- The reduction loop never runs out of fuel. -/
def ReduceRecordNoFallback : Prop :=
  ∀ G : Graph, G.WF → (reduceRecordF G).2.2 = false

/-- `pd_tw2` never falls back on a graph that reduces to the empty graph
(treewidth at most 2). -/
def PdTw2NoFallback : Prop :=
  ∀ H : Graph, H.WF → (reduceRecord H.copy).1.numNodes = 0 → (pdTw2F H).2 = false

/-- `algo_T1` has no fallback for maximum degree `≤ 3`. -/
def AlgoT1NoFallback : Prop :=
  ∀ G : Graph, G.WF → G.MaxDegLE 3 → ∀ Y : Labels, (algoT1F G Y).2 = false

/-- `algo_mixed` has no fallback (every graph). -/
def AlgoMixedNoFallback : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoMixedF G lab).2 = false

/-- `algo_T4` has no fallback (every graph). -/
def AlgoT4NoFallback : Prop :=
  ∀ G : Graph, G.WF → ∀ lab : Labeler, (algoT4Full G lab).fallback = false

end CubicPathwidth.Alg