Theoretical Computer Science
planar-graphs coq proof-assistants
Updated Mon, 20 Jun 2022 06:15:08 GMT

Representations of Planar Graphs in Coq

I would like to formalize some simple properties of planar graphs in the Coq proof assistant.

1) How are planar graphs formalized in the Coq proof assistant? Is there a "standard" definition that is widely used? For instance, a definition that is already in some library for the manipulation of planar graphs?

2) Even better: Is there any inductive definition that is widely used?


The obvious resource for planar graphs in Coq would be the (modern port of) the four color theorem in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs.

It's not immediately obvious to me how planar graphs are characterized, though the relevant file is here and it seems to involve a combination of Euler characteristic and Jordan paths.

One could conceivably use the forbidden minor characterization, and use the modern library by Doczkal and Pous though I have a hard time imagining that it's easy to prove anything using that characterization. It'd be more interesting to prove that it is a characterization. This again uses SSReflect. See also the paper.

Finally, using any of the existing (mature) libraries for graphs, one might want to use the definition used in the flyspec project, described here, which defines (in section 2.3) planar graphs in terms of faces, which need to be orientable, connected to other faces with inverse orientation, with a cycle around each vertex, and obeying the Euler theorem. The paper is very nice, and describes the Gonthier approach as well in the subsequent sections.