The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

My opinion is "yes". More Coq development is always a good thing, and
I am sure the focus on "it's easy to express algorithms" of Martin
Edwig's work will interest other Coq users.

There is a Graphs-Basics library on Coq "contribs" base of
developments that follows a relatively similar approach, and was
proposed by Jean Duprat in 2001 (see the corresponding research
report, "A Coq toolkit for graph theory"). The representation is
relatively close to Erwig's, in that it is also inductive. Instead of
a constructor that adds "a new vertex and all its edges to vertices
already in the graph", there are separate constructors, one for a new
vertex, and one for a new edge (I assume this is more convenient in
some cases and less convenient in others).

II suspect there are many formalisations of the basics of graph theory
on which independent larger developments have been built (some
references are given in Duprat's research report). There is some in
the CoLoR library ( http://color.inria.fr/ ), where finite (directed)
graphs are represented as maps from vertices to sets of their
neighbors -- there are also various graph algorithms in CoLoR. There
is also a nice inductive presentation of the DPS traversal of a graph
in François Pottier's formalisation of strongly-connected components (
http://gallium.inria.fr/~fpottier/publis/fpottier-dfs-scc.pdf ).

On Thu, Oct 15, 2015 at 2:44 PM, Ilmārs Cīrulis
<ilmars.cirulis AT gmail.com>
 wrote:
> Hello, coq-club!
>
> I started to develop library of graph theory, based on "inductive graph"
> idea by Martin Erwig (see here:
> https://web.engr.oregonstate.edu/~erwig/papers/InductiveGraphs_JFP01.pdf).
> It's is primarily to get some experience, but I wonder if it has some
> potential usefulness too.
>
> What's your opinion?