<p>The obvious resource for planar graphs in Coq would be the (modern port of) the <a href="https://github.com/math-comp/fourcolor/tree/master/theories" rel="noreferrer">four color theorem</a> in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs.</p>

<p>It's not immediately obvious to me how planar graphs are characterized, though the relevant file is <a href="https://github.com/math-comp/fourcolor/blob/master/theories/hypermap.v" rel="noreferrer">here</a> and it seems to involve a combination of Euler characteristic and Jordan paths.</p>

<p>One could conceivably use the forbidden minor characterization, and use the modern library by <a href="https://perso.ens-lyon.fr/christian.doczkal/graphs/" rel="noreferrer">Doczkal and Pous</a> 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 <em>is</em> a characterization. This again uses SSReflect. See also the <a href="https://hal.archives-ouvertes.fr/hal-02127698/document" rel="noreferrer">paper</a>.</p>

<p>Finally, using any of the existing (mature) libraries for graphs, one might want to use the definition used in the flyspec project, described <a href="https://mediatum.ub.tum.de/doc/601794/document.pdf" rel="noreferrer">here</a>, 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.</p>

CC BY-SA 4.0
2019-07-04T15:22:54.943Z
2019-07-04T15:22:54.943Z
cody
<p>I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2).</p>

<p>First, Gonthier goes into detail about the representation of planar maps used for the formalization of 4CT in his technical report <a href="http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf" rel="nofollow noreferrer">A computer-checked proof of the Four Colour Theorem</a>. This representation is based on the classical (and quite beautiful) idea of a "<a href="https://en.wikipedia.org/wiki/Combinatorial_map" rel="nofollow noreferrer">combinatorial map</a>", where an embedding of a graph into a surface is determined up to isomorphism by specifying a triple of permutations <span class="math-container">$(v,e,f)$</span> that compose to the identity.  Here's a picture from the Wikipedia article that will give you the idea:</p>

<p><img src="https://upload.wikimedia.org/wikipedia/commons/1/1a/Combinatorial_map_planar_graph_example.svg" width="200">
<img src="https://upload.wikimedia.org/wikipedia/commons/9/94/Combinatorial_map_example.svg" width="200"></p>

<p><span class="math-container">\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}</span>
The genus <span class="math-container">$g$</span> of a map is fixed by the Euler characteristic formula
<span class="math-container">$$\chi = \#\text{ vertices} - \#\text{ edges} + \#\text{ faces} = 2 - 2g$$</span>
and so a planar map can be defined as a combinatorial map with Euler characteristic <span class="math-container">$\chi = 2$</span> (and hence <span class="math-container">$g=0$</span>), which simply reduces to counting the number of cycles in the permutations <span class="math-container">$v$</span>, <span class="math-container">$e$</span>, and <span class="math-container">$f$</span>.  (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 <span class="math-container">$e$</span> is an involution.)</p>

<p>(Notice that in the paragraph above I used the word "planar map" rather than "planar graph".  The literature is inconsistent about whether "planar graph" refers to a graph that happens to have an embedding into the plane/sphere, or to a graph equipped with such an embedding, in other words, whether planarity is treated as a <em>property</em> or as a <em>structure</em>.  Sometimes people use the terms "planar graph" vs "plane graph" to distinguish planarity-as-property vs planarity-as-structure. This distinction is important because of the notion of isomorphism it induces: two planar graphs are isomorphic if they are isomorphic as abstract graphs, but two plane graphs are isomorphic just in case there is an isomorphism between them that respects the planarity structure.  Planar map is a synonym for plane graph.)</p>

<p>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 <span class="math-container">$v,e,f$</span> 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:</p>

<p><a href="https://i.sstatic.net/azCFZ.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/azCFZ.png" alt="picture of a rooted map"></a></p>

<p>Such <em>rooted planar maps</em> admit a direct inductive description going back to Tutte's work on combinatorics from the 1960s, that works by examining what happens around the root.  There are actually a number of ways to do this, but see for example the description in Section 3.2 of <a href="https://hal.archives-ouvertes.fr/hal-01670709/document" rel="nofollow noreferrer">Tests and proofs for enumerative combinatorics</a> by Dubois, Giorgetti, and Genestier.  Somewhat surprisingly, this way of representing rooted planar maps also has connections to lambda calculus!  If you're interested in that, my best advice is to go check out this <a href="https://jcreedcmu.github.io/demo/lambda-map-drawer/public/" rel="nofollow noreferrer">web app</a> developed by Jason Reed.</p>

CC BY-SA 4.0
2019-07-05T07:19:48.930Z
2019-07-05T07:19:48.930Z
Noam Zeilberger
<p>I would like to formalize some simple properties of planar graphs in the Coq proof assistant. </p>

<p>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? </p>

<p>2) Even better: Is there any inductive definition that is widely used? </p>

CC BY-SA 4.0
2019-07-04T12:32:44.277Z
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
<planar-graphs><coq><proof-assistants>
Representations of Planar Graphs in Coq
Springberg
# Representations of Planar Graphs in Coq

(Asked by: username_0 on 2019-07-04)

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?

**Tags:** planar-graphs, coq, proof-assistants

> **Comments:**
> **username_1**: 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?  

---

## 2 answers

### Answer by username_2 on 2019-07-04. Score: 5 | Accepted answer

The obvious resource for planar graphs in Coq would be the (modern port of) the [four color theorem](https://github.com/math-comp/fourcolor/tree/master/theories) 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](https://github.com/math-comp/fourcolor/blob/master/theories/hypermap.v) 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](https://perso.ens-lyon.fr/christian.doczkal/graphs/) 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](https://hal.archives-ouvertes.fr/hal-02127698/document).

Finally, using any of the existing (mature) libraries for graphs, one might want to use the definition used in the flyspec project, described [here](https://mediatum.ub.tum.de/doc/601794/document.pdf), 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.


---

### Answer by username_3 on 2019-07-05. Score: 4

I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2).

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](http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf). This representation is based on the classical (and quite beautiful) idea of a "[combinatorial map](https://en.wikipedia.org/wiki/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:

![](https://upload.wikimedia.org/wikipedia/commons/1/1a/Combinatorial_map_planar_graph_example.svg)
![](https://upload.wikimedia.org/wikipedia/commons/9/94/Combinatorial_map_example.svg)

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

(Notice that in the paragraph above I used the word "planar map" rather than "planar graph". The literature is inconsistent about whether "planar graph" refers to a graph that happens to have an embedding into the plane/sphere, or to a graph equipped with such an embedding, in other words, whether planarity is treated as a *property* or as a *structure*. Sometimes people use the terms "planar graph" vs "plane graph" to distinguish planarity-as-property vs planarity-as-structure. This distinction is important because of the notion of isomorphism it induces: two planar graphs are isomorphic if they are isomorphic as abstract graphs, but two plane graphs are isomorphic just in case there is an isomorphism between them that respects the planarity structure. Planar map is a synonym for plane graph.)

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:

[![picture of a rooted map](https://i.sstatic.net/azCFZ.png)](https://i.sstatic.net/azCFZ.png)

Such *rooted planar maps* admit a direct inductive description going back to Tutte's work on combinatorics from the 1960s, that works by examining what happens around the root. There are actually a number of ways to do this, but see for example the description in Section 3.2 of [Tests and proofs for enumerative combinatorics](https://hal.archives-ouvertes.fr/hal-01670709/document) by Dubois, Giorgetti, and Genestier. Somewhat surprisingly, this way of representing rooted planar maps also has connections to lambda calculus! If you're interested in that, my best advice is to go check out this [web app](https://jcreedcmu.github.io/demo/lambda-map-drawer/public/) developed by Jason Reed.


---

