coq-community / graph-theory

Graph Theory [maintainers=@chdoc,@damien-pous]

Graph Theory

A library of formalized graph theory results, including various standard results from the literature (e.g., Menger's Theorem, Hall's Marriage Theorem, the excluded minor characterization of treewidth-two graphs, and Wagner's Theorem) as well as some more recent results arising from the study of relation algebra within the ERC CoVeCe project (e.g., soundness and completeness of an axiomatization of graph isomorphism).

Meta

• Author(s):
  • Christian Doczkal (initial)
  • Damien Pous (initial)
  • Daniel Severín (external contributor)
• Coq-community maintainer(s):
  • Christian Doczkal (@chdoc)
  • Damien Pous (@damien-pous)
• License: CeCILL-B
• Compatible Coq versions: 8.18 or later
• Additional dependencies:
  • MathComp's SSReflect library, version 2.0 or later
  • MathComp's Algebra library
  • MathComp's finmap library
  • Hierarchy Builder, version 1.5.0 or later
  • Gonthier's formal proof of the Four-Color Theorem (optional dependency)
• Coq namespace: GraphTheory
• Related publication(s):
  • A Variant of Wagner's Theorem Based on Combinatorial Hypermaps doi:10.4230/LIPIcs.ITP.2021.17
  • Graph Theory in Coq - Minors, Treewidth, and Isomorphisms doi:10.1007/s10817-020-09543-2
  • Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq doi:10.1145/3372885.3373831
  • A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs doi:10.1007/978-3-319-94821-8_11
  • Formalization of the Domination Chain with Weighted Parameters (Short Paper) doi:10.4230/LIPIcs.ITP.2019.36

Building and installation instructions

To manually build and install the whole project, including Wagner's theorem which requires the Coq proof of the Four-Color Theorem, do:

git clone https://github.com/coq-community/graph-theory.git
cd graph-theory
make   # or make -j <number-of-cores-on-your-machine> 
make install

However, the easiest way to install released versions of Graph Theory libraries selectively is via opam:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-graph-theory # core library
opam install coq-graph-theory-planar # planarity results depending on coq-fourcolor

Documentation

This project contains:

• a general purpose Coq library about graph theory:
  • directed graphs, simple graphs, multigraphs
  • paths, trees, forests, isomorphism, connected components, etc.
  • minors and tree decompositions
  • Menger's theorem and some of its corollaries (Hall's marriage theorem and König's theorem)
  • the excluded-minor characterisation of treewidth at most two graphs (as those excluding K4 as a minor)
• soundness and completeness of an axiomatization of isomorphism of two-pointed treewidth-two (2p) multigraphs:
  • isomorphisms up to label-equivalence and edge-flipping for multigraphs
  • 2p graphs form a 2p algebra and thus also a 2pdom algebra
  • every K4-free graph can be represented by a 2p-term
  • 2pdom axioms are complete w.r.t. graph isomorphism for connected 2p graphs.
• a proof of Wagner's theorem (planarity of K5 and K3,3 graphs) based on combinatorial hypermaps
• two proofs of the weak perfect graph theorem (WPGT):
  • one proof based on Lovasz's replication lemma
  • one proof based on a matrix rank argument

Additional information on the contents of individual files is available at the project website.

graph-theory's Issues

Consitently use documentation comments (** *) for explanations.

In order to obtain decently looking documentation, we should consistent in our use of comments and documentation:

• documentation comments (** *) for everything that qualifies as explanation (rendered in highlighted boxes in the documentation).
• regular comments (* *) for TODO and TOTHINK comments and the like, that are internal (rendered as greyed-out text)

(edit: comments inside proofs must always be regular comments, as documentation inside proofs messes up coqdocjs code folding)

Meta-issue: blockers for v0.8

Blockers:

• stable version of finmap #79

Propagate finmap results to upstream

The file finmap_plus.v contains many general finite map results that could be propagated upstream to the finmap project (or may have already been added to recent releases).

This is a memento that these results exist to enable tracking Coq ecosystem consolidation.

GitHub release or tag for Coq 8.11 and MathComp 1.10.0

It would be very useful (e.g., for reusing/integrating code) if the project had a GitHub release or Git tag which is guaranteed to support Coq 8.11 and MathComp 1.9.0 + 1.10.0. The main rationale is that when looking only at repository code, it's usually a lot of work to figure out the compatibility status of a given revision.