THEME 1 OPERATION3

Operation 3 : Specifications and proofs in geometry

Head : Jean-François Dufourd, PR CE2

Participants : Nicolas Magaud AP, Julien Narboux AP, Pascal Schreck PR1

Ph.D. candidates : Christophe Brun

General overview

In Operation 3 we target the formal definition of universes of geometric objects and operations, the property proofs of these objects and the derivation of geometric algorithms proved correct. We consider more and more these activities as needing to be computer-assisted in order to ensure the practical feasibility and guarantee its rigor and quality. The applications are in geometric modeling, computational geometry, pure geometry and math teaching. We separated from these activities the Operation 2 Solving of geometric constraints - which uses specific techniques - to best highlight the two topics. Nevertheless they keep very strong connections, in particular in the symbolic way of approaching the problems and common projects will again occur in the future. This Operation is much implicated in the project ANR blanc GALAPAGOS (2007-2010) "Géométrie algorithmique et preuves assistées par ordinateur" (Computational geometry and computer-aided proofs). This project is headed by Yves Bertot (DR INRIA) and associates the INRIA (Marelle, Sophia), the LSIIT (IGG, Strasbourg), the SIC (Poitiers), the CEDRIC (CNAM, Paris) and the ENS (Lyon). Its objective is to promote axiomatization methods and Coq-assisted proofs in the fields of computational geometry and geometric constructions.

History

We find the origin of these concerns in the years 1990-97 with the promotion of algebraic specifications and the re-writing of combinatorial maps (and extensions) in topological and geometric models. These works allowed to rationally develop several softwares, such as an interactive topology-based volume modeler - called Topofil (thesis of Yves Bertrand) -, a functional OCaml prototype to define and manipulate curves, surfaces and volumes (thesis of Laurent Fuchs), and a library of set operations, or boolean, on plane and space subdivision with base operation the refinement of subdivisions (thesis of David Cazier, 1997).

Later, in the years 1998-2004, we wished that these specifications would serve as axiomatics for proofs of objects topological properties. We also wished that these proofs would be, if not automatic, at least computer assisted and proven. The softwares of algebraic specification such as OBJ3 (or Maude, CaféOBJ, Larch) that we used didn't offer assistance tools, therefore we searched for better suited systems. We thus naturally turned to the system Coq from INRIA. It allowed us to retake and adapt our old specifications and go much further in the direction of proofs.

We first constructively formalized in Coq the combinatorial maps as an inductive type with invariant and then set and demonstrated a sufficient condition of preservation of planarity during a construction. We finally stated and proved a simple form of Jordan's discrete theorem (thesis of François Puitg, 2000).

Recent contributions

Combinatorial surfaces classification

Willing to show the effective nature of our propositions and their generality we approached the combinatorial surfaces and a big topology theorem (thesis of Christophe Dehlinger, 2003). It is the theorem of surfaces (with border) classification by triplets of feature integers (p,q,r), where p, q and r denote respectively the rings (or right ears), the torsions (or Moebius bands, or twisted ears) and the tunnels (or bridges). In classical proofs (Griffiths, Fomenko), the proof is decomposed in two parts. The first consists in simplifying the mesh into a construction plane normalized with the same features : it is the normalization theorem. The second consists in switching, when q>=3, 2 twisted ears with a bridge : this is the trading theorem. Thus the classification theorem in its whole states that any surface with border can be classified into a single topological class corresponding to a triplet (p,q,r), with q<=2, where the surfaces are homeomorphic. This work has been the chance to provide an inductive specification of generalized maps. The trading theorem has been proved using Coq by a structural induction technique over generalized maps. It has been published in two joint papers of the journal Theoretical Computer Science [2-DD04, 2-DD04]. The normalization theorem has later been proved by a noetherian induction using a quite complex distance between two maps.

Genus theorem and Euler formula

We then approached the topic of simplification and generalization of these specifications by considering combinatorial hyper-maps in the sense of Cori. We developed, from scratch, a specification library over hyper-maps, by starting from an inductive type of free maps that we progressively constrained by invariants until we obtained a type of satisfying hyper-maps on which we defined operations and proved interesting properties for geometric modeling. Thus we were able to state and prove the genus theorem saying that the genus g = c – K/2 of a hyper-map is always an integer, where c is the number of connected components, and K Euler's characteristic defined by K = v – e + f, where v, e, and f denote the vertices, edges and faces of the hyper-map. A corollary is then Euler-Poincaré formula v – e + f = 2c for planar hyper-maps, i.e. of genus zero. The matching hyper-maps / orientated closed surfaces allows to transport these results to surfaces themselves. These results were proved by Coq essentially by a structural induction technique (Jean-François Dufourd, 2006). This work, which is in the process of publication, has been partially presented at the conference ACM SAC'07 [4-DUF07] and then published in an exhaustive fashion in [2-DUf08a]. It appears to be the first time that Euler's formula has been formalized, if we refer to the list of classical theorems (top 100) maintained by Freek Weidijk (http://www.cs.ru.nl/~freek/100/).

Hyper-maps, planarity criterion and discrete Jordan theorem

Recently this work has been reconsidered in order to simplify and extend our propositions. The revision especially focuses on a softened definition of the type of hyper-maps and a generic definition thanks to the notion of Coq's signature and parametrized modulus, orbit traversal (vertices, edges, faces) with period determination. A result was the possibility of proving the symmetry of the orbit traversal - which could never be obtained previously - and a constructive and complete planarity criterion, i.e. a necessary and sufficient condition of planarity maintaining during the hyper-map construction. These results (Jean-François Dufourd, 2006) haven't yet been published. They will need to be compared to the formalization of hyper-maps performed by G. Gonthier et al. for their amazing proof in Coq of the four-color theorem done at the time of the common INRIA-Microsoft lab creation (Gonthier et al., 2005). Our propositions are different but not necessarily simpler. An extension of this work is the definition of the notion of rings of faces in a hyper-map and cut along a ring. They allow to formulate a discrete Jordan theorem stating that, in a planar hyper-map, the cut along a ring adds a connected component. This result has been completely proven in Coq and published in the Journal of Automated Reasoning [2-Duf09a], where we also find a comparison with Jordan's criterion proven by G. Gonthier et al. in the four-color theorem.

Hyper-maps and certification of image segmentation

Also we wanted to do a first incursion in the field of conception and certification of algorithms. We chose as benchmark a classical in imaging : segmentation of 2D colored images by cells fusion. Our cells subdivision (starting with pixels) is modeled by a colored hyper-map (or a map as special case). It is segmented in two steps by a functional algorithm described in Coq by a structural recursion on the hyper-map. The overall correctness, termination and partial correctness regarding certain criteria was proven. We then derived an imperative optimal program performing segmentation on a hyper-map represented as a chained list of darts, following the rule for our conceived modelers. This work conducted by Jean-François Dufourd was presented at Journées de l'AFIG 06 [4-DUF06], JFLA 07 [5-DUF07], and published in the journal Pattern Recognition [2-DUF07].

Data structures and computational geometry

We conduct an informal study in the field of modeling and computational geometry in order to improve programming techniques and ensure the correctness of the algorithms. We perform a case-study in computational geometry and focus on a classical problem calling the simplest surface subdivision : the incremental computation of the convex hull of a finite set of points in the plane.

The originality of the used techniques rests on, one side, the specifications and formal programing proofs expressed in the formalism of inductive construction calculus set up in Coq, and on the other side on the fact that we use a topology-based geometric modeling framework where subdivision surfaces are represented by hyper-maps.

Our work consists of the conception of a functional algorithm, the automatic extraction of a program in OCaml allowing data input and a graphical visualization of the result, and the formal proof of its overall correctness by the verification of its termination and highlight of numerous topological and geometric properties.

These works have been presented during the "journées du GDR GPL" in November 2008.

In parallel we work on an alternate representation of maps in Coq. A chained structure, containing for each dart its successors and predecessors (in the two dimensions) and the embedding, presents indeed the benefit of being close to usual implementations of maps in imperative languages. We came back to the maps theory initially developed in Coq and work on the adaption of the definitions and proofs to the new considered data structure. We work with the team of Catherine Dubois from CNAM who developed a set approach of g-maps modeling in order to determine the common features to our two modelings and the bridges to be built to make our two Coq developments compatible and reusable.

Automatic formal proof in geometry

Geometry is one of the most fruitful fields for automatic theorem proving. There are efficient methods which can prove numerous theorems. Among these methods we can distinguish algebraic methods from methods which try to simulate human reasoning. The areas method of Chou, Gao and Zhang is a semi-analytic method that offers proofs that are both short and readable. In 2004, Julien Narboux formalized a version of this method for affine geometry. In 2009, the formalization of the method has been generalized in order to treat euclidian geometry. This formalization, with the support of Coq's proof assistant, allows to guarantee the correctness of the generated proofs.

Currently we work on the formalization of methods for algebraic automatic theorem proving.

Formalization of projective geometry and treatment of degenerate cases in geometry

When a theorem in geometry doesn't apply to certain special cases (e.g. when three points are collinear or two points are equal), we call it a degenerate case. Degenerate cases are the major source of difficulties during formal proofs and errors in geometric algorithms. Nicolas Magaud, Julien Narboux and Pascal Schreck have proposed a new formalization method in geometry based on the rank concept. This method has been applied to the proof of Desargues' theorem in projective geometry. We also proposed formalization methods in projective geometry in order to mimic informal reasoning such as the one consisting of e.g. reasoning by duality. This works are the basis for our research on geometric constraints (see Operation 2).