Digraph extensions for Mathlib

General-purpose definitions on top of Mathlib's Digraph: directed walks and simple paths, depth (longest simple-path length on a finite graph), IsAcyclic, the edgeFinset of a digraph with decidable adjacency on a finite vertex type, and deleteEdges.

The depth measure is exported together with its general bounds, public for downstream reuse and as upstreaming candidates: pathLength_bddAbove (simple-path lengths are bounded by the vertex count), depth_le_card (depth ≤ Fintype.card V), one_le_depth (a nonempty graph has positive depth), and depth_deleteEdges_empty (deleting the empty edge set preserves depth). These hold for every finite digraph, with no acyclicity assumption.

This file lives in Complexitylib/Mathlib/ because it extends a Mathlib type in its home (root) namespace — the one sanctioned exception to the Complexity root-namespace rule. Its contents are candidates for upstreaming to Mathlib.

Depth-reduction-specific machinery (canonical labeling, acyclicity arguments, edge partitions by first-differing bit, etc.) lives in Complexitylib.Circuits.Internal.Valiant.

def Digraph.IsDirectedWalk {V : Type u_1} (G : Digraph V) {m : ℕ} (p : Fin m → V) : Prop

G.IsDirectedWalk p says that p : Fin m → V is a directed walk in the digraph G: consecutive vertices are joined by an edge.

Equations

• G.IsDirectedWalk p = ∀ (i : Fin m) (h : ↑i + 1 < m), G.Adj (p i) (p ⟨↑i + 1, h⟩)

def Digraph.IsPath {V : Type u_1} (G : Digraph V) {m : ℕ} (p : Fin m → V) : Prop

G.IsPath p says that p : Fin m → V is a simple directed path: an injective directed walk.

Equations

• G.IsPath p = (G.IsDirectedWalk p ∧ Function.Injective p)

theorem Digraph.pathLength_bddAbove {V : Type u_1} [Fintype V] (G : Digraph V) : BddAbove {m : ℕ | ∃ (p : Fin m → V), G.IsPath p}

The lengths of simple paths in a finite graph are bounded by its vertex cardinality.

noncomputable def Digraph.depth {V : Type u_1} [Fintype V] (G : Digraph V) : ℕ

The depth of a finite digraph is the maximum length — number of vertices — of a simple directed path. Using simple paths makes depth a total, honest finite measure even when the graph contains a cycle. Results whose proofs require a DAG state IsAcyclic explicitly.

Equations

• G.depth = sSup {m : ℕ | ∃ (p : Fin m → V), G.IsPath p}

theorem Digraph.depth_le_card {V : Type u_1} [Fintype V] (G : Digraph V) : G.depth ≤ Fintype.card V

A finite digraph's simple-path depth is at most its number of vertices.

theorem Digraph.one_le_depth {V : Type u_1} [Fintype V] [Nonempty V] (G : Digraph V) : 1 ≤ G.depth

A finite nonempty digraph has a one-vertex path, hence positive depth.

def Digraph.edgeFinset {V : Type u_1} [Fintype V] (G : Digraph V) [DecidableRel G.Adj] : Finset (V × V)

The directed edge set of a digraph with decidable adjacency on a finite vertex type.

Equations

• G.edgeFinset = {p : V × V | G.Adj p.1 p.2}

theorem Digraph.mem_edgeFinset {V : Type u_1} [Fintype V] {G : Digraph V} [DecidableRel G.Adj] {e : V × V} : e ∈ G.edgeFinset ↔ G.Adj e.1 e.2

def Digraph.deleteEdges {V : Type u_1} (G : Digraph V) (F : Finset (V × V)) : Digraph V

The digraph obtained from G by deleting a finite set of directed edges F.

Equations

• G.deleteEdges F = { Adj := fun (u v : V) => G.Adj u v ∧ (u, v) ∉ F }

@[implicit_reducible]

instance Digraph.instDecidableRelAdjDeleteEdgesOfDecidableEq {V : Type u_1} [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj] (F : Finset (V × V)) : DecidableRel (G.deleteEdges F).Adj

Equations

• G.instDecidableRelAdjDeleteEdgesOfDecidableEq F u v = Digraph.instDecidableRelAdjDeleteEdgesOfDecidableEq._aux_1 G F u v

def Digraph.IsAcyclic {V : Type u_1} (G : Digraph V) : Prop

A digraph is acyclic when its set of directed-walk lengths is bounded. For finite vertex types this is equivalent to having no directed cycles.

Equations

• G.IsAcyclic = BddAbove {m : ℕ | ∃ (p : Fin m → V), G.IsDirectedWalk p}

theorem Digraph.depth_deleteEdges_empty {V : Type u_1} [Fintype V] (G : Digraph V) : (G.deleteEdges ∅).depth = G.depth

The simple-path set of G.deleteEdges ∅ agrees with that of G, so the two graphs have the same depth.

noncomputable def Digraph.canonicalLabel {V : Type u_2} (G : Digraph V) (v : V) : ℕ

The canonical labeling of G: the length — node count — of a longest simple directed path ending at v. Parameterized by edge count n, with the outer + 1 converting to node count; the single-vertex path ![v] always witnesses n = 0, so the label is automatically at least 1.

Equations

• G.canonicalLabel v = sSup {n : ℕ | ∃ (p : Fin (n + 1) → V), G.IsPath p ∧ p (Fin.last n) = v} + 1