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.
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. 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.)
(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:
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 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 developed by Jason Reed.
