Representations of Planar Graphs in Coq

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.

Solved by user3984 (13,157 )
Jul 04, 2019 at 15:22