THEME 1 OPERATION3

!!! Document in french !!! Translation in progress...

Opération 3 : Spécifications et preuves en géométrie

Responsable : Jean-François Dufourd, PR CE2

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

Doctorants : Christophe Brun

Présentation générale

Dans l'opération 3, nous visons la définition formelle d'univers d'objets géométriques et d'opérations, la preuve de propriétés de ces objets et la dérivation d'algorithmes géométriques certifiés corrects. Nous envisageons de plus en plus ces activités comme devant être assistées par ordinateur pour en assurer la faisabilité pratique, et en garantir la rigueur et la qualité. Les retombées sont en modélisation géométrique, en algorithmique géométrique, en géométrie pure et en enseignement des mathématiques. Nous avons voulu séparer de ces activités l'opération 2 Résolution de contraintes géométriques, qui utilise des techniques spécifiques, pour mieux faire ressortir les deux thématiques. Cependant, elles gardent des liens très forts, notamment dans la manière symbolique d'aborder les problèmes, et des projets communs se dessineront à nouveau. Cette opération est très impliquée dans le projet ANR blanc GALAPAGOS (2009-2011) "Géométrie algorithmique et preuves assistées par ordinateur". Ce projet est piloté par Yves Bertot (DR INRIA) et associe l'INRIA (équipe-projet Marelle, Sophia), le LSIIT (équipe IGG, Strasbourg), le SIC (Poitiers), le CEDRIC (CNAM, Paris) et l'ENS (Lyon). Son objectif est de promouvoir les méthodes d'axiomatisation et de preuves assistées en Coq dans les domaines de l'algorithmique géométrique et des constructions géométriques.

Historique

On trouve l'origine de ces préoccupations dans les années 90-97 avec la promotion des spécifications algébriques et de la réécriture dans les modèles topologiques et géométriques de cartes combinatoires et leurs extensions. Ces travaux ont permis de développer de manière rationnelle plusieurs logiciels, comme un modeleur interactif volumique à base topologique, appelé Topofil (thèse de Yves Bertrand), un prototype fonctionnel en Ocaml pour définir et manipuler des courbes, surfaces et volumes (thèse de Laurent Fuchs), et une bibliothèque d'opérations ensemblistes, ou "booléennes", sur des subdivisions du plan et de l'espace, avec comme opération de base le raffinement de subdivisions (thèse de David Cazier, 1997).

Plus tard, dans les années 98-04, nous avons voulu que ces spécifications servent d'axiomatique pour des preuves de propriétés d'objets topologiques. Nous souhaitions également que ces preuves soient, sinon automatiques, au moins assistées et vérifiées par ordinateur. Les logiciels de spécification algébriques tels que OBJ3 (ou Maude, CaféOBJ, Larch) que nous utilisions n'offrant guère d'outils d'assistance, nous avons cherché des systèmes mieux adaptés. Nous nous sommes alors tout naturellement tournés vers le système Coq de l'INRIA. Il nous a permis de reprendre et adapter nos anciennes spécifications et d'aller bien au-delà en direction des preuves.

Nous avons d'abord formalisé de manière constructive en Coq les cartes combinatoires comme un type inductif avec invariant, puis donné et démontré une condition suffisante de préservation de la planarité lors d'une construction. Nous avons enfin énoncé et prouvé une forme simple du théorème de Jordan discret (thèse de François Puitg, 2000).

Contributions récentes

Classification des surfaces combinatoires

Voulant montrer le caractère effectif de nos propositions et leur généralité, nous nous sommes attaqués aux surfaces combinatoires et à un grand théorème de topologie (thèse de Christophe Dehlinger, 2003). Il s'agit du théorème de classification des surfaces ouvertes par des triplets d'entiers caractéristiques (p,q,r), où p, q et r dénombrent respectivement les anneaux (ou oreilles droites), les torsions (ou bandes de Moebius, ou oreilles torses) et les tunnels (ou ponts). Dans les preuves classiques (Griffiths, Fomenko), la preuve est décomposée en deux parties. La première consiste à simplifier le maillage en un plan de construction normalisé de mêmes caractéristiques : c'est le sous-théorème de normalisation. La seconde consiste à échanger, quand q >= 3, 2 oreilles torses contre 1 pont : c'est le sous-théorème d'échange (trading theorem). Ainsi, le théorème de classification en entier affirme que toute surface ouverte peut être rangée dans une seule classe topologique correspondant à un triplet (p,q,r), avec q <= 2, où les surfaces sont homéomorphes. Ce travail a été l'occasion de fournir une spécification inductive des cartes généralisées. Le sous-théorème d'échange a été prouvé à l'aide de Coq par une technique d'induction structurelle sur les cartes généralisées. Ce travail a été publié dans deux papiers joints de la revue Theoretical Computer Science [2-DD04, 2-DD04]. Le sous-théorème de normalisation l'a ensuite été par une induction noethérienne faisant intervenir une distance assez complexe entre deux cartes.

Théorème du genre et formule d'Euler

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/).

Hypercartes, critère de planarité et théorème de Jordan discret

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.

Hypercartes et certification de la segmentation d'images

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].

Structures de données et algorithmique géométrique 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.

Preuve formelle automatique en géométrie

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.

Formalisation de la géométrie projective et traitement des cas dégénérés en géométrie

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).