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.19 or later
• Additional dependencies:
  • MathComp's SSReflect library, version 2.5.0 or later
  • MathComp's Algebra library
  • MathComp's finmap library
  • MathComp's Algebra tactics
  • 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.