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.

"Théorème du genre" and Euler formula

Nous nous sommes ensuite attachés à simplifier et généraliser ces spécifications en considérant des hypercartes combinatoires (au sens de Cori). Nous avons développé à partir de zéro (from scratch) une bibliothèque de spécification sur les hypercartes, en partant d'un type inductif de cartes libres, que nous avons contraint progressivement par des invariants jusqu'à obtenir un type d'hypercartes satisfaisant sur lequel nous avons défini des opérations et prouvé des propriétés intéressantes pour la modélisation géométrique. Ainsi, nous défini avons pu énoncer et prouver le théorème du genre affirmant que le genre g = c – K/2 d'une hypercarte est toujours en entier naturel, où c est le nombre de composantes connexes, et K la caractéristique d'Euler, définie par K = v – e + f, où v, e et f dénombrent les sommets, arêtes et faces de l'hypercarte. Un corollaire est alors la formule d'Euler-Poincaré v – e + f = 2c pour les hypercartes planaires, c'est-à-dire de genre nul. La correspondance hypercartes-surfaces closes orientables permet de transposer ces résultats aux surfaces elles-mêmes. Ces résultats ont pu être prouvés en Coq essentiellement par une technique d'induction structurelle (Jean-François Dufourd, 2006). Ce travail, qui est en cours de publication, a été partiellement présenté à la conférence ACM SAC'07 [4-DUF07] puis publié de manière exhaustive dans [2-DUf08a]. C'est, semble-t-il, la première fois qu'une preuve de la formule d'Euler est formalisée, si l'on se réfère à la liste des théorèmes classiques (top 100) maintenue par Freek Weidijk (http://www.cs.ru.nl/~freek/100/).

Hyper-maps, planarity criterion and discrete Jordan theorem

Récemment, ce travail a été repris de manière à simplifier et élargir nos propositions. La révision porte notamment sur une définition allégée du type des hypercartes et une définition générique grâce à la notion de signature et de module paramétré de Coq, des parcours d'orbites (sommets, arêtes, faces) avec détermination d'une période. Il en est résulté la possibilité de prouver la symétrie du parcours d'orbites, ce qui n'avait jamais pu être obtenu auparavant, ainsi qu'un critère de planarité constructif complet, c'est-à-dire une condition nécessaire et suffisante de maintien de la planarité lors de la construction d'une hypercarte. Ces résultats (Jean-François Dufourd, 2006) n’ont pas encore été publiés. Ils seront à comparer avec le travail de formalisation des hypercartes effectué par G. Gonthier et al. pour leur formidable preuve en Coq du théorème des 4 couleurs mise en exergue au moment de la création du laboratoire commun INRIA-Microsoft (Gonthier et al., 2005). Nos propositions sont différentes, et nous avons la faiblesse de penser qu'elles sont plus simples. Une prolongation de ce travail est la définition des notions d'anneau de faces dans une hypercarte et de coupure le long d'un anneau. Elles permettent d'énoncer un théorème de Jordan discret affirmant que, dans une hypercarte planaire, la coupure selon un anneau ajoute une composante connexe. Ce résultat a été complètement prouvé en Coq et publié dans le Journal of Automated Reasoning [2-Duf09a], où l'on trouve également une comparaison avec le critère de Jordan prouvé par G. Gonthier et al. dans la preuve du théorème des 4 couleurs.

Hyper-maps and certification of image segmentation

Par ailleurs, nous avons voulu faire une première incursion dans le domaine de la conception et de la certification d'algorithmes. Nous avons choisi comme benchmark un classique de l'imagerie : la segmentation d'images colorées 2D par fusion de cellules. Notre subdivision en cellules (pixels au départ) est modélisée par une hypercarte (ou une carte comme cas particulier) colorée. Elle est segmentée en deux phases par un algorithme fonctionnel décrit en Coq par une récursion structurelle sur l'hypercarte. La correction totale, terminaison et correction partielle, par rapport à certains critères a pu être prouvée. Nous avons ensuite dérivé un programme impératif optimal faisant la segmentation sur une hypercarte représentée comme une liste chaînée de brins, comme cela est la règle dans les modeleurs que nous avions conçus. Ce travail mené par Jean-François Dufourd a été présenté aux Journées de l'AFIG 06 [4-DUF06], aux JFLA 07 [5-DUF07], et publié dans la revue 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).