K4-free/TW2 graphs, free algebras, Coq proofs

This page is a web appendix to the following papers:

  1. K4-free Graphs as a Free Algebra, extended.pdf.
    E. Cosme Llopez, D. Pous, in Proc. MFCS'17.
  2. Treewidth-Two Graphs as a Free Algebra, .pdf.
    C. Doczkal, D. Pous, in Proc. MFCS'18.

  3. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs, .pdf.
    C. Doczkal, G. Combette, D. Pous, in Proc. ITP'18.
  4. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms, .pdf.
    C. Doczkal, D. Pous, to appear in JAR special issue of ITP'18.
  5. Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq, .pdf.
    C. Doczkal, D. Pous, submitted.
(The first two papers are `pen-and-pencil' papers; the last three are `computer-assisted' papers using Coq.)

It is a well-known result that graphs of treewidth at most two (TW2) are the ones excluding the clique with four vertices (K4) as a minor, or equivalently, the graphs whose biconnected components are series-parallel.

In [1], we turn those graphs into a free algebra, answering positively a question by Courcelle and Engelfriet, in the case of treewidth two.
First we propose a syntax for denoting them: in addition to parallel composition and series composition, it suffices to consider the neutral elements of those operations and a unary transpose operation. Then we give a finite equational presentation (2p-algebra) and we prove it complete: two terms from the syntax are congruent if and only if they denote the same graph.
Our proof is based on an precise analysis of the structure of K4-free graphs; it actually requires us to (re)prove that those have treewidth at most two.

In [2], we give a simpler proof of the main result from the first paper, not using minors at all: we use a confluent rewriting system to extract terms from TW2 graphs. This approach is more flexible and allows us to handle variants of 2p-algebras: 2pdom-algebras for connected graphs and 1-free 2p-algebras for graphs with distinct input and output and without self-loops.

In [3] we give the first formal and constructive proof in Coq/Ssreflect that the graphs of treewidth two are exactly those that do not admit K4 as a minor. It is extended in [4], where:

In [5] we formalise the completeness theorem for 2pdom algebras, following the proof in the MFCS'18 paper [2].
This formalisation effort is rather orthogonal to the one above: we are not concerned at all with minors and treewidth here. We reprove that graphs form a 2pdom algebra here because we need a slight generalisation, but this is the only overlap with [4].
This requires us to use two representations for graphs, the one from the previous papers, which is dependently typed, and a more classical one.

Coq library for [3,4,5]

We only maintain and develop a single library for the aforementioned formalisations. It is available on github/coq-community and opam (package coq-graph-theory). Since version 0.8, the library also contains a module dom containing a proof of Cockayne-Hedetniemi domination chain (with weighted parameters).
The code can be browsed online (CoqDocJS with foldable proofs). Its modules dependencies are given on the right, where:

The nodes are links to the documentation for each module; each of them is described succinctly below.

preliminary infrastructure

general purpose graph library [4]

2p-algebra of multigraphs [4], term extraction [3,4]

completeness of 2pdom axioms [5]

Snapshots for each paper (subsumed by the above library)

For reference, we also provide the code as it was at submission/publication time for the three formalisation papers

[3] TW2=K4-free (ITP'18)

[4] Coq graph library with Menger's theorem, TW2=K4-free, and soundness of 2p axioms

(This code completely subsumes the one just above.)

[5] Completeness of 2pdom axioms, via a confluent graph rewrite system

(Rather orthogonal to the one just above: only soundness is repeated since it had to be generalised.)

Independence of the 2p-algebra axioms

In the MFCS'17 paper [1], we claim independence of the 2p-algebra axioms. We prove the independence of the axioms by exhibiting finite (partial) models.
We automatically checked those models in the Coq proof assistant, see the proof script here or download it there.
These counter-models have at most four elements; the converse operation is always taken to be the identity, except for the independence of axioms A6 and A7.

When looking for those counter-models, we found that there are 11 2p-algebras with three elements and 236 with four elements (up to isomorphism).