key: cord-0046599-3ygklm4h
authors: Allamigeon, Xavier; Katz, Ricardo D.; Strub, Pierre-Yves
title: Formalizing the Face Lattice of Polyhedra
date: 2020-06-06
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51054-1_11
sha: 5901f26e3380d639cf69ce6d3e4ce7eb078a8dda
doc_id: 46599
cord_uid: 3ygklm4h

Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under sublattices.

A face of a polyhedron is defined as the set of points reaching the maximum (or minimum) of a linear function over the polyhedron. Faces are ubiquitous in the theory of polyhedra, and especially in the complexity analysis of optimization algorithms. As an illustration, the simplex method, one of the most widely used algorithms for solving linear programming, finds an optimal solution by iterating over the graph of the polyhedron, i.e. the adjacency graph of vertices and edges, which respectively constitute the 0and 1-dimensional faces. The problem of finding a pivoting rule, i.e. a way to iterate over the graph, which ensures to reach an optimal vertex in a polynomial number of steps, is a central problem in computational optimization, related with Smale's ninth problem for the twenty-first century [25] . Faces of polyhedra are also involved in the worst-case complexity analysis of other optimization methods, such as interior point methods; see [2, 13] . This has motivated several mathematical problems on the combinatorics of faces, which are of independent interest. For example, the question of finding a polynomial bound on the diameter of the graphs of polyhedra (in the dimension and the number of defining inequalities) is still unresolved, despite recent progress [6, 7, 23] . We refer to [12] for a recent account on the subject.

Other applications of polyhedra and their faces arise in formal verification, in which passing from a representation by inequalities to a representation as the convex hull of finitely many points and vice versa, is a critical computational step. The correctness analysis of the algorithms solving this problem, extensively relies on the understanding of the mathematical structure of faces, in particular of vertices, edges and facets (i.e. 1-co-dimensional faces).

In this paper, we formalize a significant part of the properties of faces in the proof assistant Coq. As usually happens in the formalization of mathematics, one of the key difficulties is to find the right representation for objects in the proof assistant. For polyhedra and their faces, the choice of the representation depends on the context. In more detail, every polyhedron admits infinitely many descriptions by linear inequality systems. In mathematics textbooks, proofs are carried out by choosing one (often arbitrary) inequality system for a polyhedron P, and then manipulating the faces of P or other subsequent polyhedra through inequality systems which derive from the one chosen for P. Proving that these are valid inequality systems is usually trivial for the reader, but not for the proof assistant. We exploit the so-called canonical structures of Coq in order to achieve this step automatically. This allows us to obtain proof scripts which only focus on the relevant mathematical content, and which are closer to what mathematicians write.

Thanks to this approach, we show that the faces of a polyhedron P form a finite lattice, in which the order is the set inclusion, the bottom and top elements are respectively the empty set and P, and the meet operation is the set intersection. We establish that the face lattice is both atomistic and coatomistic, meaning that every element is the join (resp. the meet) of a finite set of atoms (resp. coatoms). Atoms and coatoms respectively correspond to minimal and maximal elements distinct from the top and bottom elements. Moreover, we prove that the face lattice is graded, i.e. every maximal chain has the same length. Finally, we show that the family of face lattices of polytopes (convex hulls of finitely many points) is closed under taking sublattices, i.e. any sublattice of the face lattice of a polytope is isomorphic to the face lattice of another polytope. As a consequence of that, we prove that any sublattice of height two is isomorphic to a diamond.

Formalizing these results requires the introduction of several important and non-trivial notions. First of all, our work relies on the construction of a library manipulating polyhedra, which provides all the basic operations over them, including intersections, projections, convex hulls, as well as special classes of polyhedra such as affine subspaces. Dealing with faces also requires to formalize the dimension of a polyhedron, and its relation with the dimension of its affine hull, i.e. the smallest affine subspace containing it. Some classes of faces also retain a particular attention, such as vertices, edges and facets. For instance, we formalize the vertex figure, which is a geometric construction to manipulate the faces containing a fixed vertex.

Throughout this work, we have drawn much inspiration from the textbooks of Schrijver [24] and Ziegler [28] to guide us in our approach. The source code of our formalization is done within the Coq-Polyhedra project, and is available at https://github.com/Coq-Polyhedra/Coq-Polyhedra/tree/IJCAR-2020, in the directory theories. We rely on the Mathematical Components library [18] (abridged MathComp thereafter) for basic data structures such as finite sets, ordered fields, and vector spaces.

The paper is organized as follows. In Sect. 2, we present how we define the basic operations and constructions over polyhedra. Section 3 deals with the central problem of finding an appropriate representation of faces, and explains how this leads to a seamless formalization of important properties like the dimension. Section 4 demonstrates the practical usability of our approach, by presenting the formalization of the face lattice and its main characteristics. Finally, we discuss related work in Sect. 5. A link to the relevant source files is given beside section titles in order to help the reader finding the results in the source code of the formalization. We recall that a (convex) polyhedron of R n is defined as the intersection of finitely many halfspaces {x ∈ R n : α, x ≥ β}, where α ∈ R n , β ∈ R, and ·, · is the Euclidean scalar product, i.e. y, z := 1≤i≤n y i z i . Equivalently, a polyhedron can be represented as the solution set of a linear affine system Ax ≥ b, where A ∈ R m×n and b ∈ R m , in which case each inequality A i x ≥ b i corresponds to a halfspace.

Throughout the paper, we use the variable n : nat to represent the dimension of the ambient space. Instead of dealing with polyhedra over the reals, we introduce a variable R : realFieldType which represents an abstract ordered field with decidable ordering. In this setting, 'cV[R] _ n (or 'cV _ n for short) stands for the type of column vectors of size n over the field R.

As we mentioned earlier, the representation by inequalities (or halfspaces) of a convex polyhedron P is not unique. The first step in our work is to introduce a quotient structure, in order to define the basic operations (membership of a point, inclusion, etc.) regardless of the exact representation of the polyhedron. The quotient structure is based on a concrete type denoted by 'hpoly[R] _ n (or simply 'hpoly _ n, when R is clear from the context). The prefix letter "h" is taken from the terminology H-polyhedron or H-representation which is used to refer to representations by halfspaces. The elements of 'hpoly _ n are records consisting of a matrix A ∈ R m×n and a vector b ∈ R m representing the system Ax ≥ b:

Record hpoly := HPoly { m : nat; A : 'M _ (m,n); b : 'cV _ m }.

We equip 'hpoly _ n with a membership predicate stating that, given P : 'hpoly _ n and x : 'cV _ n, we have x \in P if and only if x satisfies the system of inequalities represented by P. Two H-polyhedra are equivalent when they correspond to the same solution set, i.e. their membership predicate agree. We prove that this equivalence relation is decidable, by exploiting the implementation of the simplex method of [3] . The latter allows us to check that an inequality α, x ≥ β is valid over an H-polyhedron P : 'hpoly _ n by minimizing the linear function x → α, x over P, and checking that the optimal value is greater than or equal to β. Then, deciding whether P Q : 'hpoly _ n are equivalent amounts to checking that each inequality in the system defining Q is valid over P, and vice versa.

The quotient structure is built following the approach of [10] . This introduces a quotient type, denoted here by 'poly[R] _ n (or simply 'poly _ n). Its elements are referred to as polyhedra and represent equivalence classes of H-polyhedra. In practice, each polyhedron is a record formed by a canonical representative of the class, and the proof that the representative is indeed the canonical one. We point out that the notion of canonical representative has no special mathematical meaning or structure.

We define the membership predicate of each P : 'poly _ n as the membership predicate of its canonical representative. As expected, equality between two polyhedra of 'poly _ n and extensional equality (denoted =i below) of their membership predicates are equivalent properties:

Lemma poly _ eqP {P Q : 'poly _ n} : (P = Q) <-> (P =i Q).

We first lift a number of basic primitives from the type 'hpoly _ n to the quotient type 'poly _ n, including the subset relation P`<=`Q and the intersection operation P`&`Q. The related properties are also lifted by using the fact that the membership predicate of any element of 'hpoly _ n is extentionally equivalent to the membership predicate of its equivalence class in 'poly _ n.

Even though we now work on the quotient type, we still need a way to build polyhedra from sets of inequalities. While H-polyhedra rely on inequality constraints under the matrix form, we choose now to be closer to the mathematical definition of polyhedra as the intersection of finitely many halfspaces. To this end, we introduce the type lrel[R] _ n (or simply lrel _ n when R is clear from the context), which is isomorphic to the cartesian product 'cV _ n * R of vectors of size n and elements of R. This type is used to construct linear affine inequalities or equalities. In more detail, if e represents the pair (α, β) ∈ R n × R, then the polyhedron [ (In the last two statements, the terms e.1 and e.2 respectively stand for the first and second component of the pair formed by e, while '[.,.] stands for the scalar product between two vectors.)

We can now construct polyhedra defined by sets of inequalities. To this aim, we use the type {fset lrel _ n} of finite sets of elements of type lrel _ n. Then, given base : {fset lrel _ n}, the polyhedron denoted by 'P(base) is defined as the intersection of the halfspaces [hs e] for e \in base. In particular, we introduce the empty polyhedron [poly0] and the full polyhedron [polyT] , which are defined by the inequality 1 ≤ 0 and by no inequality respectively. As we shall see in Sect. 3, the formalization of faces requires us to manipulate polyhedra defined by systems mixing inequalities and equalities. We denote such a polyhedron by 'P^=(base; I), where both base and I are of type {fset lrel _ n}. It represents the intersection of the polyhedron 'P(base) with the hyperplanes [hp e] for e \in I.

The cornerstone of more advanced constructions is the primitive proj0, which, given P : 'poly _ (n.+1), builds its projection on the last n components. This is carried out by implementing Fourier-Motzkin elimination algorithm (see e.g. [24, Chapter 12] ). In short, this algorithm starts from a system of linear inequalities, and constructs pairwise combinations of them in order to eliminate the first variable. The result is that the new system is a valid representation of the projected polyhedron. This is written as follows:

Theorem proj0P (P : 'poly _ (n.+1)) : reflect (exists2 y : 'cV _ (n.+1), x = row' 0 y & y \in P) (x \in proj0 P).

where row' 0 y : 'cV _ n is the projection of y on the last n components, and reflect stands for a logical equivalence between the two properties. This projection primitive then allows us to construct many more polyhedra. For example, we can build the image of a polyhedron P by the linear map represented by a matrix A ∈ R k×n . The latter is obtained by embedding P in a polyhedron over the variables (x, y) ∈ R n+k , intersecting it with the equality constraints y = Ax, and finally projecting it on the last k components. The construction of the convex hull of finitely many points immediately follows. Indeed, the convex hull of a finite set V = {v 1 , . . . , v p } ⊂ R n can be defined as the image of the simplex

We denote the convex hull by conv V where V : {fset 'cV _ n} represents a finite set of points, and we obtain (cf. Lemma in _ convP) that x \in conv V if and only if x is a barycentric combination of the points of V. The convex hull constructor yields some other elementary yet very useful constructions, such as polyhedra Finally, we recover some important results of the theory of polyhedra which were proved in [3] . In more detail, we lift a version of Farkas Lemma expressed on the type 'hpoly _ n, and then obtain the Strong Duality Theorem, the complementary slackness conditions (which are conditions characterizing the optimality of solutions of linear programs), and some separation results. We refer to Section Separation and Section Duality for further details on these statements.

Faces are commonly defined as sets of optimal solutions of linear programs, i.e. problems consisting in minimizing a linear function over a polyhedron.

We note that P is a face of itself (take c = 0). Figure 1 provides an illustration of this definition.

In formal proving, the choice of the definition plays a major role on the ability to prove complex properties of the considered objects. A drawback of the previous definition is that it does not directly exhibit some of the most basic properties of faces: for instance, the fact that a face is itself a polyhedron, the fact that the intersection of two faces is a face, or the fact that a polyhedron has finitely many faces. In contrast, these properties are straightforward consequences of the following characterization of faces:

Nevertheless, Theorem 1 is expressed in terms of a certain H-representation of the polyhedron P, while the property of being a face is intrinsic to the set P. This raises the problem of exploiting the most convenient representation of P to apply the characterization of Theorem 1. We illustrate this on the proof of the following property, which is used systematically (or even implicitly) in almost every proof of statements on faces:

Assume P is represented by the inequality system Ax ≥ b, and take I as in (1). Let F be a nonempty face of F. We apply Theorem 1 with F as P, by using the following H-representation of F :

and conclude that F is a face of P by applying Theorem 1. While the choice of the H-representation of P is irrelevant, we point out that the proof would not have been so immediate if we had initially chosen an arbitrary H-representation of F.

Theorem 1 leads us to the following strategy: when dealing with the faces of a polyhedron, and possibly with the faces of these faces, etc., we first set an H-representation of the top polyhedron, and then manipulate the subsequent Hrepresentations of faces in which some inequalities are strengthened into equalities, like in (1).

The top H-representation will be referred to as the ambient representation, and is formalized as a term base of type {fset lrel _ n} representing a finite set of inequalities. Then, we introduce the type {poly base}, which corresponds to the subtype of 'poly _ n whose inhabitants are the polyhedra Q satisfying the following property: where {fsubset base} is the type of subsets of base. We recall that 'P^=(base; I) denotes the polyhedron defined by the inequalities in base, with the additional constraint that the inequalities in the subset I are satisfied with equality. This means that {poly base} corresponds to the polyhedra defined by equalities or inequalities in base. The choice of the name base is reminiscent of the terminology used in fiber bundles. Indeed, as we shall see in the next sections, several proofs will adopt the scheme of fixing a base locally, and then working on polyhedra of type {poly base}. Following this analogy, the latter may be thought of as a fiber.

We now present a first formalization of the set of faces relying on the subtype Indeed, the inclusion argmin P c`<=`P is immediate from the definition of the polyhedron argmin P c. However, even once Lemma argmin _ baseP is proved, we cannot yet write a statement of the form argmin P c \in pb _ face _ set P due to the fact that argmin P c has type 'poly _ n. In order to turn it into an element of the subtype {poly base}, we need to explain in more detail how this type is defined. The type {poly base} is a short-hand notation for the following inductive type:

Inductive poly _ base base := PolyBase { pval :> 'poly _ n ; _ : has _ base base pval }.

In other words, an element of type {poly base} is a record formed by an element pval : 'poly _ n and a proof that the property has _ base base pval holds. While we could construct the element PolyBase (argmin _ baseP P c), we introduce a more general scheme to cast elements of type 'poly _ n to {poly base} whenever possible. This scheme relies on Coq canonical structures, which provide an automatic way to recover a term of record type from the head symbol. The association is declared as follows:

Canonical argmin _ base (P : {poly base}) c := PolyBase (argmin _ baseP P c).

One restriction of Coq is that canonical structures are resolved only when unifying types, and not arbitrary terms. This is why our primitive poly _ base _ of, which casts a Q : 'poly _ n to a {poly base}, encapsulates the value Q in a phantom type, i.e. a type isomorphic to the unit type, but with a dependency to Q.

Definition poly _ base _ of (Q : {poly base}) ( _ : phantom 'poly _ n Q) := Q.

Notation "Q %:poly _ base" := (poly _ base _ of (Phantom _ Q)).

In consequence, writing (argmin P c)%:poly _ base triggers the unification algorithm between the term argmin P c and a value of type {poly base}, which is resolved using the Canonical declared above. We finally end up with the following statement Lemma argmin _ pb _ face _ set base (P : {poly base}) c :

(argmin P c)%:poly _ base \in pb _ face _ set P. whose proof is trivial: it just amounts to proving the inclusion argmin P c`<=`P.

We declare other canonical structures over elementary constructions for which the property has _ base base _ can be shown to be satisfied. This includes the intersection P`&`Q of two elements P Q : {poly base}, the empty set [poly0 ], or polyhedra of the form 'P(base) or 'P^=(base; .). This allows us to cast complex terms to the type {poly base}, or, said differently, to prove automatically that they satisfy the property has _ base base _ . As an example, the term ('P^=(base; I)`&`argmin 'P(base) c)%:poly _ base typechecks thanks to multiple resolutions of canonical structures on the aforementioned declarations, without requiring extra proof from the user. We refer to [21] for the use of canonical structures in formal mathematics.

We point out that Lemma argmin _ pb _ face _ set is a proof of one side of the equivalence between the definition of faces brought by pb _ face _ set and Definition 1 (i.e. the equivalence in Theorem 1). The other side can be written as follows: When Q is nonempty, we use a set I such that Q = 'P^=(base, I), and we build c as the sum of the vectors -e.1 : 'cV _ n for e \in I. The equality Q = argmin P c follows from a routine verification of the complementary slackness conditions.

So far, we have worked with a fixed ambient representation base, and restricted the formalization of faces to polyhedra that can be expressed as terms of type {poly base}. We now describe how to formalize the set of faces of any polyhedron of type 'poly _ n as a finite set of polyhedra of the same type, without sacrificing the benefits brought by {poly base}.

First, we exploit the observation that for each polyhedron P : 'poly _ n, there exists base : {fset lrel _ n} and P' : {poly base} such that P = pval P' (recall that pval also stands for the coercion from the type {poly base} to 'poly _ n). This can be proved by exploiting the definition of the quotient type 'poly _ n.

Indeed, P admits a representative hrepr P : 'hpoly _ n corresponding to a certain H-representation, from which we can build a term base : {fset lrel _ n} such that P = pval 'P(base)%:poly _ base.

Second, we introduce another quotient structure over the type 'poly _ n, in order to deal with the fact that a polyhedron may correspond to several elements of type {poly base} for different values of base. Our construction amounts to showing that 'poly _ n is isomorphic to the quotient of the dependent sum type base {poly base} by the equivalence relation in which Q1 : {poly base1} and Q2 : {poly base2} are equivalent if pval Q1 = pval Q2. Given a polyhedron P of type 'poly _ n, this construction provides us a canonical ambient representation denoted 
epr _ base P : {fset lrel _ n}, and an associated canonical representative 
epr P of type {poly (
epr _ base P)} satisfying P = pval (
epr P).

We are now ready to define the set of faces of P in full generality: which corresponds to the image by the coercion pval of the face set of 
epr P (here, pval has type {poly (
epr _ base P)} -> 'poly _ n). Of course, we need to check that this definition is independent of the choice of the representative of P in this new quotient structure. This is written as follows: which means that, given a property to be proved on any polyhedron P : 'poly _ n, it is sufficient to prove it over the type {poly base} for any choice of base. In practice, Lemma polybW is used to introduce an ambient representation. Let us illustrate it on the proof that the intersection of two faces of P is a face of P:

Lemma face _ set _ polyI (P Q1 Q2 : 'poly _ n) : Q1 \in face _ set P -> Q2 \in face _ set P -> Q1`&`Q2 \in face _ set P. Qed.

The first line destructs P, and introduces the ambient representation base and an element still named P, now of type {poly base}. The second and third lines successively consume the assumptions that Q1 and Q2 are faces, then introduce two elements of type {poly base} having the same name and respectively satisfying Q1`<=`P and Q2`<=`P. Finally, the tactics rewrite face _ setE replaces the goal Q1`&`Q2 \in face _ set P by the following two subgoals: Q1`&`Q2`<=`P and has _ base base (Q1`&`Q2). Since (Q1`&`Q2)`<=`Q1 and Q1`<=`P, the former is proved by transitivity of the subset relation. The latter is automatically provided by the canonical structure mechanism described in Sect. 3.2, triggered by the generic statement Lemma pvalP base (P : {poly base}) : has _ base base P.

We argue that the approach that we have introduced to represent faces of polyhedra also perfectly fits the formalization of the affine hull and dimension of polyhedra. Recall that the affine hull of a polyhedron refers to the smallest (inclusionwise) affine subspace of R n containing it, and the dimension of the polyhedron is defined as the dimension of this subspace (i.e., the dimension of the underlying vector subspace).

To this end, given an ambient representation base and a polyhedron P of type {poly base}, we introduce the set of active inequalities of P, i.e. the set of e \in base such that the corresponding inequality is satisfied as equality over P. This is written as the inclusion P`<=`[hp e] (recall that [hp e] is the hyperplane '[e.1, x] = e.2). The active inequalities form a subset of base denoted {eq P}. Equivalently, when P is non-empty, {eq P} corresponds to the largest (inclusionwise) subset I such that P = 'P^=(base; I).

It is a classic property of polyhedra that the affine hull of a non-empty polyhedron is the affine subspace defined by the equalities in {eq P}. We take this property as a definition: The second definition lifts the affine hull from {poly base} to 'poly _ n. Of course, we show that the resulting affine subspace hull P is independent of the choice of base (cf. Lemma hullE). We establish that this definition is correct w.r.t. the usual mathematical definition discussed above, i.e.:

Lemma hullP P U : (P`<=`affine U) <-> (hull P`<=`affine U).

Here, U corresponds to a vector subspace of lrel _ n, and the term affine U stands for the affine subspace given by the intersection of the affine equalities represented by the elements of U. (The term << {eq P} >> above corresponds to the vector subspace spanned by the elements of {eq P}.)

We follow the same scheme to formalize the dimension dim P of a polyhedron P : 'poly _ n, which we define as one plus the co-dimension of the vector span of {eq P}. The shift by one originates from the fact that dim P ranges over the type nat of natural numbers. Therefore, we have to set the dimension of the empty set [poly0] to 0, while it is common to set it to −1 in the literature. As expected, we obtain the following statement:

Lemma dim _ hull (P : 'poly _ n) : dim P = dim (hull P).

Like in mathematics textbooks, Lemma dim _ hull is the natural way to establish the basic statements concerning the dimension, i.e. by reducing to elementary proofs over vector spaces. For instance, we establish that the dimension is monotone (Lemma dimS), and compute the dimension for important classes of polyhedra. This includes the fact that segments of two distinct points have dimension 2 (remember the shift by one of our formalization): (We point out that compact P is simply defined as the fact that P is a bounded set, as polyhedra are topologically closed.) Similarly, we prove that polyhedra reduced to a single point are precisely the ones having dimension 1, that proper hyperplanes have codimension 1, etc. We refer to Section Dimension for a detailed account of our results.

In this section, we illustrate how the framework that we have introduced in Sect. 3 serves as a foundation for formalizing the structural properties of faces. We refer to Fig. 2 for an example of the properties presented below.

At the core of the formalization lies the theory of ordered structures such as partial orders, semilattices and lattices. Some of these structures have been very recently introduced in the MathComp library -for instance, the non-distributive lattice structure has been introduced in early 2020. However, as we shall see in this section, the formalization of the face lattice requires to implement additional objects, such as graded lattices, sublattices, and lattice homomorphisms. This development is gathered in the module xorder.v of the Coq-Polyhedra project.

The first property that we can immediately formalize following the results of Sect. 3 is the finite lattice structure over the set face _ set P for P : 'poly _ n. The 

Recall that a lattice (L, ≺) is said to be graded if there exists a rank function Φ: L → N such that:

Equivalently, this is a lattice in which all maximal chains have the same length.

In the case of the face lattice, the rank function can be defined as the dimension of the face. Property (i) is proved as follows. If Q and Q' are both faces of P and Q`<`Q', then dim Q <= dim Q', as the dimension is monotone. Moreover, hull Q`<=`hull Q'. If we assume dim Q = dim Q', then we can prove that hull Q is equal to hull Q' (as affine subspaces of the same dimension). We conclude that Q = Q' by the fact that F = P`&`hull F for any face F of P.

The proof of Property (ii) (see Lemma graded) relies on the formalization of facets of polyhedra, and their combinatorial characterization in terms of active inequalities. We recall that a facet of a non-empty polyhedron P is a face of P of dimension dim P − 1. A classical result states that when P is given by a non-redundant system of inequalities Ax ≥ b (i.e. the H-representation is minimal inclusionwise), the facets are precisely the polyhedra of the form P∩{x ∈ R n : This allows to specialize P to a polyhedron of the form 'P(base) where base is a minimal set of inequalities defining P. Using the techniques of Sect. 3, we switch to a proof environment dealing with polyhedra in {poly base}, and establish that the facets of P are precisely the polyhedra of the form 'P^=(base; [fset i]) for i 

otin {eq P} (where [fset i] is the singleton consisting of i). We refer to the statements Lemma dim _ facet and Lemma facetP for the exact description.

Going back to the description of the proof of Property (ii), we assume that Q and Q' are two faces of P satisfying Q`<=`Q' and (dim Q).+1 < dim Q'. We first consider the case where Q' = P. Since Q`<`P, we can pick an element i in {eq Q} but not in {eq P}, and verify that the facet F := 'P^=(base; [fset i]) satisfies Q`<`F`<`P. The general case where Q' is a proper face of P is handled by using the fact that Q \in face _ set P and Q`<=`Q' ensures that Q is a face of Q' (see Lemma face _ set _ of _ face).

The atoms of a lattice L are the elements u ∈ L \{⊥} such that there is no v ∈ L satisfying ⊥ ≺ v ≺ u, where ⊥ denotes the bottom element of L. In the face lattice of a polyhedron P, they correspond to the faces F of P such that dim F = 1, i.e. to the vertices of P (remember the shift by one of our formalization). This motivates the introduction of the vertex set of P, which satisfies the following two characteristic properties: A central property is that if P is compact, then it coincides with the convex hull of its vertices:

Theorem conv _ vertex _ set (P : 'poly _ n) :

compact P -> P = conv (vertex _ set P).

Remark that this shows that any compact polyhedron is a polytope. Together with the converse statement (Lemma compact _ conv in polyheron.v), this brings a proof of Minkowski Theorem.

The latter result allows us to prove that, when P is compact, its face lattice is atomistic, meaning that any face of P is the join of a finite set of atoms: To prove this statement for Q, we set S to the set of vertices of Q. The latter are vertices of P as well, and thus correspond to atoms of the face lattice of P. The inclusion Q`<=`\join _ (x in vertex _ set Q) x is established by substituting Q by conv (vertex _ set Q) thanks to Lemma conv _ vertex _ set, which makes the statement obvious by construction of the convex hull and the join operator. The opposite inclusion Q`>=`\join _ (x in vertex _ set Q) x is trivial by property of the join operator, and this concludes the proof.

The coatoms of L are defined dually: these are the elements u ∈ L \ { } such that there is no v ∈ L satisfying u ≺ v ≺ , where denotes the top element of L. The coatomicity of face _ set P means that any face of P is the intersection of facets of P. Our proof exploits the characterization of facets presented in Sect. 4.1. We refer to Lemma face _ coatomistic for more details.

The closedness under sublattices of the face lattices of polytopes states that if Q and Q' are two faces of a polytope P such that Q`<=`Q', then the interval '[< Q; Q' >], i.e. the sublattice formed by the faces F : face _ set P satisfying Q`<=`F`<=`Q', is isomorphic to the face lattice of a polytope of dimension

The interest of this property is that it allows involved induction schemes on the height of the face lattice. As an example, we can establish the so-called diamond property, namely that every sublattice of height 2 of the face lattice consists of precisely four faces ordered as . Equivalently, this means that for any two faces F and F of a polytope P such that dim F = dim F +2 and F ⊂ F , there are precisely two faces between them (see Lemma diamond for the statement, and Fig. 2 for an illustration). The proof exploits the closedness by sublattices, and the subsequent isomorphism of any interval of height 2 with the face lattice of a polytope P' verifying dim P' = 2. Lemma dim2P reduces it to the face lattice of a segment [segm x; y], which is given by the following characterization: The proof of the closedness by sublattices is done as follows. First, we reduce to the case where Q' = P, since the face lattice of Q' is isomorphic to the sublattice of the faces of P contained in Q'. We are left with the following statement: The proof is done by induction on the dimension of Q. We restrict the exposition to the base case dim Q = 1, i.e. when Q corresponds to a vertex x of P, since the general case is just handled by iterating the process. When dim Q = 1, the construction of the polyhedron P' is achieved by the vertex figure method. It consists in slicing the polytope P with a hyperplane [hp e] separating the vertex In the sliced polytope P , the vertices (green) and edges (blue) are respectively in one-to-one correspondence with the edges and facets of P containing x. (Color figure online)

x from the other vertices (see Fig. 3 for an illustration). We define P' as the sliced polytope. It has dimension (dim P)-1, and its face lattice can be shown to be isomorphic to the sublattice '[< [pt x]; P >]. Once again, the isomorphism is proved by exposing the polyhedron P to the subtype {poly base} for some ambient representation base, and reducing to basic manipulations of sets {eq _ } of active inequalities of faces. Interestingly, two distinct ambient representations are used in the proof: base for the original polytope P, and its union e +|`base with the singleton {e} for the sliced polytope P'. Our use of canonical structures still applies to this setting, and provides the proof that any face of P sliced with the hyperplane [hp e] writes down over the base e +|`base of the sliced polytope P'.

Many software developments related with convex polyhedra have been motivated by applications to formal verification. Several libraries have been developed for this purpose, e.g. [4, 20] , and, despite being informal, it is worth noting that they are also used by mathematicians to perform computation over polyhedra and polytopes, for instance in [16, 27] . Initiatives on the development of formally verified polyhedral algorithms are more recent. The works of [26] and [8] in Isabelle/HOL aim at providing a formally proven yet practical and efficient algorithm to decide linear rational arithmetic for SMT-solving. The Micromega tactics [5] relies on polyhedra to prove automatically arithmetic goals over ordered rings in Coq. The Verified Polyhedral Library [9, 15] targets abstract interpretation, and brings the ability to verify polyhedral computations a posteriori in Coq.

There are far fewer developments focusing on formal mathematics. Euler formula, which relates the number of vertices, edges and facets of three-dimensional polytopes, has been proved in [14] in Coq and in [1] in Mizar. The generalization to polytopes in arbitrary dimension, namely Euler-Poincaré formula, has been formally proved in HOL-Light [19] , together with several intermediate properties of polyhedra and faces. In the intuitionistic setting, we are not aware of any work concerning faces and their properties. We point out that Fourier-Motzkin elimination has been formalized in Coq by [22] .

In this work, we have formalized a substantial part of the theory of polyhedra and their faces, which has allowed us to obtain some of the essential properties of face lattices. Beyond the mathematical results formally proven, a special attention has been paid to the usability of the library. This goes through a mechanism to bring the right representation of faces according to the context, and the automatic proof that these representations are valid thanks to the use of canonical structures.

This foundational work opens several perspectives. First, it has raised that an important development over ordered structures is still needed, in particular for the manipulation of ordered substructures such as sublattices, and the interplay between them through morphisms. The formalization of finite groups and subgroups in [17] may provide a possible source of inspiration to solve this problem. Second, there are many other interesting properties in relation with polyhedra and their faces to be formalized, such as getting upper bounds on the diameter of polytopes, or more generally, on the number of faces (the so-called f-vector theory). However, beyond the interest of formalizing already known mathematical results, we are even more interested in using proof assistants to help getting new ones. We think of mathematical results relying on computations that are not accessible by hand. To this extent, we aim at providing a way to compute with the objects introduced in this work, directly within the proof assistant, and to introduce all the needed mechanisms for the design and development of large scale reflection tactics. A basic goal is to compute the face lattice (or part of it) of a polyhedron defined by a set of inequalities. This requires us to formalize some algorithms based on faces, and to find a way to execute them on efficient data structures, in the spirit of the approach of [11] .

Euler's polyhedron formula in mizar

Log-barrier interior point methods are not strongly polynomial

A formalization of convex polyhedra based on the simplex method

The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems

Fast reflexive arithmetic tactics the linear case and beyond

On subdeterminants and the diameter of polyhedra

The diameters of network-flow polytopes satisfy the Hirsch conjecture

Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL

The verified polyhedron library: an overview

Pragmatic quotient types in Coq

Refinements for free!

Algebraic and topological tools in linear optimization

Central path curvature and iterationcomplexity for redundant Klee-Minty cubes

Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof

A certifying frontend for (sub)polyhedral abstract domains

polymake: a framework for analyzing convex polytopes

A small scale reflection extension for the Coq system

The HOL Light theory of Euclidean space

Apron: a library of numerical abstract domains for static analysis

Canonical structures for the working Coq user

A counterexample to the Hirsch conjecture

Theory of Linear and Integer Programming

Mathematical problems for the next century

Formalization of incremental simplex algorithm by stepwise refinement

The Sage Development Team

Lectures on Polytopes

Acknowledgments. We are grateful to Assia Mahboubi for helpful discussions on the subject. We thank the anonymous reviewers for their detailed comments and their suggestions to improve the presentation of the paper.