Weighted Directed Graphs

Stream: CSLib

[Abdalrhman M Mohamed]

Hi all, I'm interested in verifying properties of graph algorithms (e.g., shortest path) where both edge weights and directions are essential. While exploring Mathlib's graph definitions, I noticed that none of the existing structures fully capture what I need:

• Graph: weighted and but undirected
• DiGraph: directed but unweighted
• SimpleGraph: undirected, loopless, and unweighted

I'm interested in CS applications, so I started this topic in the CSLib channel to ask:
Would there be interest in modifying one of these definitions or introducing a new one that supports both directionality and edge weights?

To make this more concrete, I'm envisioning something along the lines of:

structure WeightedDirectedGraph (α : Type u) (β : Type v) where
  /-- The adjacency relation of a digraph. -/
  Adj : β → α → α → Prop

This is similar to DiGraph, but allows edge identifiers (or weights) via β. Alternatively, a more elaborate structure inspired by Graph might look like:

structure WeightedDirectedGraph (α : Type u) (β : Type v) where
  /-- The binary incidence predicate, stating that `x` and `y` are the ends of an edge `e`. -/
  IsLink : β → α → α → Prop

  /-- The vertex set. -/
  vertexSet : Set α := {x | ∃ e y, IsLink e x y ∨ IsLink e y x}

  /-- The edge set. -/
  edgeSet : Set (β × α × α) := {(e, x, y) | IsLink e x y}

  /-- An edge `e` is incident to `x` and `y` if and only if `(e, x, y)` is in the edge set. -/
  edge_mem_iff_exists_isLink : ∀ e x y, (e, x, y) ∈ edgeSet ↔ IsLink e x y := by exact fun _ _ _ ↦ Iff.rfl

  /-- If some edge `e` is incident to `x`, then `x ∈ V`. -/
  left_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet := by exact fun e x y h ↦ ⟨e, ⟨y, Or.inl h⟩⟩

  /-- If some edge `e` is incident to `y`, then `y ∈ V`. -/
  right_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → y ∈ vertexSet := by exact fun e x y h ↦ ⟨e, ⟨x, Or.inr h⟩⟩

This version is closer in spirit to Graph, but adapted for directed edges and edge data. I'd like to hear thoughts on whether this fits within CSLib's (or Mathlib's) scope or if there's an existing effort I could contribute to.

[Vlad Tsyrklevich]

This seems like it could be represented by an auxiliary definition instead of being a part of the graph structure—could weights be an edge labeling a la #30047?

[Abdalrhman M Mohamed]

Thanks for pointing me to #30047. I hadn't seen it before! That approach definitely seems promising, especially since it avoids major refactoring of existing graph definitions.

That said, I do wonder about potential fragmentation: if we keep layering auxiliary structures or wrappers, we might end up with several parallel graph definitions that don't interoperate easily. Ideally, we'd be able to reuse algorithms written for more general graph types (e.g., weighted, directed) when working with specialized ones. I'd love to explore whether there's a clean way to unify these representations or at least ensure good composability across them.

[Vlad Tsyrklevich]

Doesn't using a definition on top of an existing graph _avoid_ parallel definitions?

[Vlad Tsyrklevich]

That said, I definitely find the current situation in Mathlib sub-optimal, preferably SimpleGraph would be a specialization and all of it's basic infrastructure would be shared with e.g. Digraph. I'm sure there has been previous discussion about this but I have not invested the time to find and go through it

[Abdalrhman M Mohamed]

Vlad Tsyrklevich said:

Doesn't using a definition on top of an existing graph _avoid_ parallel definitions?

Yes, this does help avoid completely separate implementations and redundant code. We wouldn't need to reimplement all the operations already available in DiGraph for a graph with edge labels.

That said, I'm thinking about this from a generality perspective. Conceptually, DiGraph could be seen as a special case of a weighted graph where the edge type is Unit and SimpleGraph is a structure that extends DiGraph with symmetry and loopless properties. Many algorithms designed for weighted graphs (like shortest path) work just as well for unweighted graphs. Ideally, we'd have a unified implementation of these algorithms (say, for a general weighted directed graph) that can be reused seamlessly by DiGraph, Graph, and SimpleGraph, along with their associated properties.

I agree with your second point: the current fragmentation in Mathlib is somewhat suboptimal. I haven't dug into past discussions either (will do so when I have when I have more free time), but I'd be interested in exploring ways to move toward that kind of unification.

[Snir Broshi]

Vlad Tsyrklevich said:

That said, I definitely find the current situation in Mathlib sub-optimal, preferably SimpleGraph would be a specialization and all of it's basic infrastructure would be shared with e.g. Digraph. I'm sure there has been previous discussion about this but I have not invested the time to find and go through it

#graph theory is the place, e.g. #graph theory > (Undirected) hypergraphs

The current state of graphs is quite a mess, but if cslib diverges instead of contributing to Mathlib it'll be an even bigger mess :(

[Pieter Cuijpers]

I don't recall where I had the discussion on graphs before, exactly. But there seem to be two flavours of definitions - one suitable if you want to prove theorems about a graph that is fixed, and one that is more suitable if you want to prove theorems about graph transformations. We will probably run into that in CSLib in exactly the same way, so it makes sense to at least understand what happened in Mathlib.

[Alex Meiburg]

There was also some discussion of the mess at #maths > Graph Minors