Résumé :
Cette étude s'inscrit dans le cadre de l'utilisation de méthodes formelles en informatique graphique, un des thèmes de recherche de l'équipe ``Méthodes Axiomatiques pour la Modélisation Géométrique'' du LSIIT de Strasbourg dirigée par le professeur J.-F. Dufourd. À l'aide d'un ``prover'' , nous tentons de formaliser un domaine particulier de la modélisation géométrique à base topologique.
Mots-clé :
modélisation géométrique, cartes combinatoires, méthodologie de preuves, démonstration automatique, Coq
Notre objectif est de proposer les prémices de ce qui pourrait constituer une méthodologie de spécifications et de preuves semi-automatisées en modélisation géométrique à base topologique et d'obtenir un cadre logiquement incontestable dans lequel des propriétés puissent être mécaniquement vérifiées. Dans cette recherche expérimentale, nous tentons de formaliser progressivement un domaine suffisant pour attaquer la démonstration de résultats fondamentaux, tel par exemple un théorème de Jordan discret.
Le but de la modélisation géométrique est de décrire des objets et opérations géométriques. Classiquement, on distingue deux familles principales de modèles [6] : les modèles CSG (Constructive Solid Geometry : Géométrie Constructive de Solides) où l'on manipule des solides élémentaires (sphères, cylindres, etc) en leur appliquant des opérations booléennes (union, intersection, etc) et les modèles B-Rep (Boundary Representation : Représentation par les Bords) où l'on définit un objet par son bord à travers une subdivision de l'espace 3D en un nombre fini de cellules (sommets, arêtes, faces) et des informations de plongement associant à chaque cellule un objet géométrique. Depuis quelques années, de nombreux modèles élargissant le champ d'action de la B-Rep sont étudiés : subdivisions d'espaces topologiques de dimension quelconque, orientables ou non, objets avec ou sans bords [5]. Nous nous limitons à l'étude de la topologie d'objets sans bords et sans informations de plongement, dans un espace de dimension 2.
Le concept de carte combinatoire [3] [4] s'est révélé bien adapté à la représentation d'une topologie de ce type [2]. Nous l'avons donc spécifié et avons prouvé un certain nombre de propriétés désirables le concernant. Il nous a semblé pertinent et prudent de définir d'abord des objets simples, généraux et facilement manipulables pour les ramener ensuite à des objets plus complexes mais modélisant pleinement et correctement l'être mathématique abstrait qu'est la carte combinatoire. Cette approche ``poupées gigognes'' permet d'échelonner les problèmes et d'isoler les difficultés. En outre, les preuves s'en trouvent simplifiées. Notre spécification commence donc par définir des cartes sans aucune contrainte, ou cartes libres. Dans le langage des spécifications algébriques, il s'agit de décrire l'algèbre de ces cartes. Puis, nous raffinons les cartes libres en quasi-cartes par l'introduction de pré-conditions restreignant le domaine d'étude. Enfin, nous montrons comment en déduire la notion de carte combinatoire. Un exemple de carte combinatoire est donné dans la figure ci-dessous.
Figure 1: Exemple de carte combinatoire
Les axiomatisations sont exprimées dans le Calcul des
Constructions Inductives (CCI) [7],
une variété de théorie des types enrichie avec la
possibilité de manipuler des définitions primitives inductives.
CCI est basé sur le 
-calcul polymorphe de Girard, un système fonctionnel très
puissant dans lequel des structures de preuve en logique d'ordre supérieur
peuvent être représentée et sur la Théorie
Intuitioniste des Types de Martin-Löf's, une tentative de fondation
des mathématiques sur des principes constructifs. Ces deux systèmes
sont combinés grâce à l'isomorphisme de Curry-Howard
qui énonce l'équivalence entre le
-calcul, notation utilisée à l'origine pour exprimer la fonctionnalité,
et les preuves en déduction naturelle. En bref, CIC est un mélange
de calcul des prédicats, de définitions inductives de prédicats
``à-la-PROLOG'' et de définitions récursives de fonctions
``à-la-ML''.
Les preuves sont élaborées et mécaniquement vérifiées dans Coq [1], un assistant à la preuve construit sur CIC. Une notation de haut niveau permet la paramétrisation et la déclaration d'axiomes , la définition de types et d'objets aussi bien concrets qu'abstraits et un développement hiérarchique de théories à travers un mécanisme de sections. Un dialogue interactif avec le ``prover'' est réalisé par l'application de tactiques pré-définies ou programmables par l'utilisateur, dans un processus ``top-down'' de démonstration.
La copie d'écran ci-dessous présente un développement typique d'une preuve dans Coq. L'énoncé du théorème à prouver exp_inv ainsi que le script de la démonstration proposée par l'utilisateur sont visibles en haut à gauche. En dessous, le ``buffer'' d'interaction avec Coq montre ce qu'il reste à prouver après que l'utilisateur ait appliqué la tactique 'Intros k z t x y m expfl; Inversion_clear expfl', qui correspond à la première ligne du script du dessus. Puis, l'utilisateur requiert l'affichage de ce qui a été prouvé jusqu'à présent, en langue naturelle, par la commande 'Show Natural Proof'. Le résultat, automatiquement généré par Coq, est affiché à droite.
