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.
   

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:

• We focus on providing a general-purpose library about simple graphs, directed graphs and multigraphs. In particular, we provide Menger's theorem and a few of its corollaries.
• We simplify the proof of the characterisation TW2=K4-free by relying on Menger's theorem.
• We additionally prove that graphs form a 2p-algebra, using a compositional approach to graph isomorphism.

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:

• yellow modules form preliminary infrastructure;
• orange modules are general purpose graph theory modules [4];
• red modules are about the 2p algebra of graphs and the extraction of terms from TW2/K4-free graphs [3,4];
• violet modules are about the 2pdom-algebra of graphs and completenes of 2pdom axioms [5].

preliminary infrastructure

• edone: small extension of the [done] tactic
• bounded: fixpoint operator for bounded recursion
• preliminaries: miscellaneous basic lemmas missing from the standard libraries
• finmap_plus: additions to the mathcomp-finmap library
• set_tac: a simple tactic for reasoning about finite sets
• bij: computationally relevant bijections between sets
• finite_quotient: abstraction layer for mathcomp quotients
• equiv: lemmas about equivalence closure

general purpose graph library [4]

• digraph: directed graphs, paths
• sgraph: simple graphs, trees and forests
• helly: Helly property for trees
• treewidth: tree decompositions, treewidth
• minor: minors, links with treewidth
• menger: Menger's theorem and corollaries
• separators: separators, proof of TW2 = K4-free via Menger's theorem
• checkpoint: checkpoints
• dom: Cockayne-Hedetniemi domination chain theorem

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

• ptt: 2p-algebras, initial algebra of terms, tests (reworked along [5])
• mgraph: labelled multigraphs (reworked along [5])
• mgraph2: pointed multigraphs, 2p algebra of such graphs (reworked along [5])
• skeleton: skeletons of multigraphs
• mgraph2_tw2: subalgebra of treewidth at most two multigraphs
• cp_minor: links between checkpoints and minors, for extraction
• extraction_def: definition of the extraction function in the connected case
• extraction_iso: correctness of the extraction function (connected case)
• extraction_top: extension to the general case, TW2 = K4-free as a corollary

completeness of 2pdom axioms [5]

• structures: setoids, bisetoids, monoids
• pttdom: 2pdom-algebras, initial algebra of terms, tests
• mgraph: labelled multigraphs
• mgraph2: pointed multigraphs, 2pdom algebra of such graphs
• rewriting: definition of the rewriting system
• reduction: rewriting system powerful enough to reach normal forms
• open_confluence: open graphs, open local confluence proof
• transfer: transfer lemmas between the open and packed representations of 2p-graphs
• completeness: wrapping up everything into a completeness proof

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)

• Browse Coq Development (CoqDocJS with foldable proofs)
• Download theory files (requires coq-8.6.1 and mathcomp-1.6.1 or newer, updated 15-05-2018)

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

(This code completely subsumes the one just above.)

• Browse Coq Development (CoqDocJS with foldable proofs)
• Download theory files (requires coq-8.9.1 and mathcomp-1.9.0, updated 2019-12-13)

[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.)

• Browse Coq Development (CoqDocJS with foldable proofs)
• Download theory files (requires coq-8.9.1 or coq-8.10, mathcomp-ssreflect-1.9.0, and mathcomp-finmap-1.3.3, updated 2019-12-13)

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).