Graph Theory v0.9.5

This is a maintenance release known to work with MathComp 2.0.0 to 2.2.0 and Coq 8.18 to 8.20.

Graph Theory v0.9.4

This is a maintenance release known to work with MathComp 2.0.0 to 2.2.0 and Coq 8.16 to 8.19.

Graph Theory v0.9.3

This is a maintenance release supporting MathComp 2.0.0 and tested with Coq 8.16 to 8.18. The main change is a port to MathComp 2.0 by Pierre Roux.

Graph Theory v0.9.2

This is a maintenance release supporting MathComp 1.13.0 to 1.17.0 and tested with Coq 8.14 to 8.17. It is planned to be the last release supporting the MathComp 1.X series, with the project supporting MathComp 2.X going forward.

Results related to planarity that depend on the Four Color Theorem (coq-fourcolor) have been split off into a separate package called coq-graph-theory-planar that depends on the main package (coq-graph-theory).

Graph Theory v0.9.1

This is a maintenance release for mathcomp-1.13 and mathcomp 1.14.

Other than using [export] for hints and type-class instances, there are no changes to the theory files.

Graph Theory v0.9

The main changes in this release are:

• A proof of the main direction of Wagner's theorem using hypermaps and supporting libraries (requires coq-fourcolor):
  • hmap_ops.v: operations on hypermaps
  • hcycle.v : faces of two-connected grahs are bounded by cycles
  • embedding.v : combinatorial (plane) embeddings for simple graphs
  • K4plane.v : a plane embedding for K4
  • wagner.v : main direction of Wagner's theorem and structural four-color theorem
• A proof of the weak perfect graph theorem (WPGT)
  • partition.v : basic lemmas about partitions
  • coloring.v : definitions and lemmas about stable set number, clique number, and chromatic number.
  • wpgt.v : perfect graphs and two proofs of the WPGT (via Lovasz replication lemma and via matrix rank argument)
• the concept of k-connectivity and associated lemmas (connectivity.v).
• a substantial collection of lemmas on the arc predicate (new file: arc.v).
• lemmas about the operation of merging two vertices (new file: smerge.v)

This release is compatible with mathcomp-1.12 on coq-8.12and coq-8.13.

Graph Theory v0.8

The main changes in this release are:

• New theory dom.v containing a proof of the Cockayne-Hedetniemi domination chain (with weighted parameters).
• The monolithic labels structure for multigraphs has been split into a (commutative) monoid for vertex labels and an elabelType to deal with edge-flipping isomorphisms.
• The aforementioned structures are now inferred automatically for the operations that require them, allowing multigraphs to be used without specifying structures.
• telescopes (e.g. for 2p- and 2pdom-algebras) have been replaced with packaged structures generated using hierarchy-builder (new dependency)
• added support for mathcomp-1.12.0
• dropped support for coq-8.10

Graph Theory v0.7 - Initial Release

This is the initial release of the GraphTheory library. The library features simple graphs, unlabeled directed graphs, and labeled multigraphs. The formalized results include various standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, and the excluded minor characterization of treewidth-two graphs) 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).

This release is compatible with mathcomp-1.10 and mathcomp-1.11.

Please note that the library is still in development. Hence, definitions and lemma names may still be subject to change.