Basic digraph definitions

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

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

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

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

Equations

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

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

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

Equations

• G.IsSimplePath p = (G.IsDirectedPath p ∧ Function.Injective p)

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

The depth of a digraph is the length — number of nodes — of a longest directed walk in it. Walks are not required to be injective, so cyclic graphs have depth = 0 by the Nat.sSup convention on unbounded sets.

Equations

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

def Digraph.edgeFinset {V : Type u_1} [Fintype V] [DecidableEq 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] [DecidableEq 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.IsDirectedPath p}

theorem Digraph.deleteEdges_empty_depth {V : Type u_1} (G : Digraph V) : (G.deleteEdges ∅).depth = G.depth

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