# 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?

• With formalization it is always important to keep in mind what you'd like to do with the planar graphs once you've formalized them. What theorems and/or constructions do you have in mind? – Andrej Bauer Jul 4 '19 at 12:32

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.

First, Gonthier goes into detail about the representation of planar maps used for the formalization of 4CT in his technical report A computer-checked proof of the Four Colour Theorem. This representation is based on the classical (and quite beautiful) idea of a "combinatorial map", where an embedding of a graph into a surface is determined up to isomorphism by specifying a triple of permutations $$(v,e,f)$$ that compose to the identity. Here's a picture from the Wikipedia article that will give you the idea:
$$\begin{array}\\ v = (1\ 7\ 9)(2\ 3)(4\ 18\ 5)(6\ 15\ 14\ 8)(10\ 11)(12\ 13)(16\ 17) \\ e = (1\ 2)(3\ 4)(5\ 6)(7\ 8)(9\ 10)(11\ 12)(13\ 14)(15\ 16)(17\ 18) \\ f = (1\ 3\ 5\ 8)(2\ 9\ 11\ 13\ 15\ 17\ 4)(6\ 18\ 16)(7\ 14\ 12\ 10) \\ \end{array}$$ The genus $$g$$ of a map is fixed by the Euler characteristic formula $$\chi = \#\text{ vertices} - \#\text{ edges} + \#\text{ faces} = 2 - 2g$$ and so a planar map can be defined as a combinatorial map with Euler characteristic $$\chi = 2$$ (and hence $$g=0$$), which simply reduces to counting the number of cycles in the permutations $$v$$, $$e$$, and $$f$$. (In the formalization that Cody linked to, it is shown that this Euler characteristic condition is equivalent to an alternative condition based on Jordan paths. Also, Gonthier explains why it is convenient to use combinatorial "hypermaps", which relax the usual condition on combinatorial maps that the permutation $$e$$ is an involution.)
Finally, I'm not completely sure what you mean by "inductive definition", but let me try to address that question. I'll assume that by inductive you mean a type introduced by a fixed collection of constructors and supporting an induction principle. The definition of combinatorial map is not inductive both because it involves conditions on the permutations $$v,e,f$$ and because we need to consider them up to relabelling of the underlying elements. However, it is possible to give an inductive definition of planar maps if we assume that they come equipped with a distinguished "flag", as in this picture: