I can't find an implementation of graph theory in Mathlib. Am I overlooking the file, or is it particularly difficult to do this, or has no one been interested in taking this on yet?
If it hasn't been done, what would be a good way to model the vertices of a graph? This seems to be the first crucial task, as once this is complete edges are easy to define, as are weights, vertex neighbors, etc. My general vision is that we should define types
Vertex and have
VertexSet be a set of types
Edge could be a 2-element set of types
Vertex belonging to a particular
EdgeSet be a set of types
Graph could extend typeclasses
EdgeSet, I think.
But perhaps this is too difficult. Could
Graph just be a typeclass with fields including a vertex set of
Nats, hence abusing the order of
Nat to order vertices, and an edge set of 2-element sets of vertices? I'd appreciate any intuition on this matter from more-experienced engineers. I'm certain I'm overlooking something.
I'm also thinking about how to define
Graph such that it can be extended to
WeightedGraph, etc. Adding weights could be an extension of
Graph to include a
w : E -> Real, where
E is the edge set, as a new field. This would make it simple to call the weights, as well. How would we extend
Digraph, which requires us to tag vertices in edges with
tail somehow? I've considered adding functions
tail mapping the edge set to the vertex set, but is there a way to require that these functions take values in the two vertices associated with the edge, or is this even necessary? Another idea would be that
Digraph doesn't even need to extend
Graph at all, and we could define it so that it's edge set is a set of pairs of vertices, so that we can call them separately. I'd also appreciate help thinking about this.