THEME 1 OPERATION3

!!! Translation in progress... !!!

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 (2009-2011) "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

Nous menons une étude formelle dans le domaine de la modélisation et de la géométrie algorithmique, afin d'améliorer les techniques de programmation et d'assurer la correction des algorithmes. Nous faisons une étude de cas en géométrie algorithmique en nous intéressant à un problème classique qui met en jeu la subdivision de surface la plus simple : le calcul incrémental de l'enveloppe convexe d'un ensemble fini de points du plan.

L'originalité des moyens utilisés s'appuie d'une part sur les spécifications et les preuves formelles de programmes qui sont exprimées dans le formalisme du calcul des constructions inductives mis en oeuvre dans le système d'aide à la preuve Coq, et de l'autre sur le fait que nous utilisons un cadre de modélisation géométrique à base topologique où les subdivisions de surface sont représentées par des hypercartes.

Notre travail consiste en la conception d'un algorithme fonctionnel, l'extraction automatique d'un programme en Ocaml permettant la saisie des données et une visualisation graphique du résultat, et la preuve formelle de sa correction totale par la vérification de sa terminaison et la mise en évidence de nombreuses propriétés topologiques et géométriques.

Ces travaux ont fait l'objet d'une présentation lors des journées du GDR GPL en novembre 2008.

Parallèlement, nous travaillons sur une représentation alternative des cartes en Coq. Une structure chaînée, contenant pour chaque brin ses successeurs et prédécesseurs aux deux dimensions ainsi que son plongement, présente en effet l'avantage d'être proche des implantations usuelles des cartes dans les langages impératifs. Nous avons repris la théorie des cartes initialement développée dans Coq et travaillons à l'adaptation des définitions et des démonstrations à la nouvelle structure de données considérée. Nous travaillons avec l'équipe de Catherine Dubois du CNAM qui a développé une approche ensembliste de la modélisation des g-cartes afin de déterminer les caractéristiques communes à nos deux modélisations ainsi que les passerelles à construire pour rendre nos deux développements Coq compatibles et réutilisables.

Automatic formal proof in geometry

La géométrie est l'un des domaines les plus fructueux de la démonstration automatique. Il existe des méthodes efficaces qui permettent de démontrer de nombreux théorèmes. Parmi ces méthodes, nous pouvons distinguer les méthodes algébriques des méthodes qui tente de simuler le raisonnement humain. La méthode des aires de Chou, Gao et Zhang est une méthode semi-analytique qui permet d'obtenir des preuves à la fois courtes et lisibles. En 2004, Julien Narboux a formalisé une version de cette méthode pour la géométrie affine. En 2009, la formalisation de la méthode a été généralisée afin de pouvoir traiter la géométrie euclidienne. Cette formalisation à l'aide de l'assistant de preuve Coq permet de garantir la correction des preuves générées.

Actuellement, nous travaillons à la formalisation de méthodes de démonstration automatique algèbriques.

Formalization of projective geometry and treatment of degenerate cases in geometry

Lorsque un théorème en géométrie ne s'applique pas dans certain cas particuliers (quand trois points sont collineaires ou deux point sont confondus par exemple), nous appelons cela un cas dégénéré. Les cas dégénérés sont la source principale des difficultés lors de preuves formelles et d'erreurs dans la algorithmes géométriques. Nicolas Magaud, Julien Narboux et Pascal Schreck ont proposé une nouvelle méthode de formalisation en géométrie à base du concept de rang. Cette méthode a été appliquée à la preuve du théorème de Desargues en géométrie projective. Nous avons aussi proposé des techniques de formalisation en géométrie projective afin de pouvoir mimer des raisonnement informels comme celui qui consiste à raisonner par dualité par exemple. Ces travaux constituent les fondements pour des nos travaux sur les contraintes géométriques (voir Opération 2).