Team IGG : Computer Graphics and Geometry

Difference between revisions of "THEME 1 OPERATION3"

From Team IGG : Computer Graphics and Geometry
Jump to navigation Jump to search
 
 
(19 intermediate revisions by 2 users not shown)
Line 1: Line 1:
−
== Opération 3 : Spécifications et preuves en géométrie ==
+
== Operation 3 : Specifications and proofs in geometry ==
  
−
'''Responsable''' : Jean-François Dufourd, PR CE2
+
'''Head''' : Jean-François Dufourd, PR CE2
  
−
'''Participants''' : Nicolas Magaud, MC, nommé au 1-09-2005, Julien Narboux, MC, nommé au 1-09-2007
+
'''Participants''' : Nicolas Magaud AP, Julien Narboux AP, Pascal Schreck PR1
  
−
'''Doctorants''' : Christophe Brun.
+
'''Ph.D. candidates''' : Christophe Brun
  
−
'''Non permanents''' : Christophe Dehlinger (Docteur, ATER 2003-2004), Sabine Carouge (DEA 2004), Aurélie Vielcastel (Allocataire-monitrice, 2004-2005, abandon), Christophe Brun (M2R 2007)
+
=== General overview ===
  
−
=== Présentation générale ===
+
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.
  
−
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.
+
=== History ===
  
−
=== Historique ===
+
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).
  
−
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).  
+
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.
  
−
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.  
+
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).
  
−
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 ===  
+
=== Recent contributions ===  
−
'''Classification des surfaces combinatoires'''  
+
 
 +
'''Combinatorial surfaces classification'''  
  
 
[[Image:Jfd_hmap1.png|right|thumb|120px]]  
 
[[Image:Jfd_hmap1.png|right|thumb|120px]]  
Line 30: Line 30:
 
[[Image:Jfd_nf.png|right|thumb|120px]]
 
[[Image:Jfd_nf.png|right|thumb|120px]]
  
−
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.  
+
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 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]. 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/).
+
'''Genus theorem and Euler formula'''  
  
−
'''Hypercartes et critère de planarité'''
+
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/).
  
−
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.  
+
 
 +
'''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.
  
 
[[Image:Jfd_seg_subd1seg.png|right|thumb|120px]]  
 
[[Image:Jfd_seg_subd1seg.png|right|thumb|120px]]  
Line 46: Line 48:
 
[[Image:Jfd_seg_hmap3seg.png|right|thumb|120px]]
 
[[Image:Jfd_seg_hmap3seg.png|right|thumb|120px]]
  
−
'''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 était à l'origine le sujet de thèse d'Aurélie Vielcastel. Il a été mené par Jean-François Dufourd après l'abandon de celle-ci pour convenances personnelles. Il a été récemment 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].
+
'''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].
 +
 
 
   
 
   
−
'''Structures de données et algorithmique géométrique'''  
+
'''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'''
 +
 
 +
[[Image:AreaMethod.png|right|thumb|240px]]
 +
 
 +
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'''
 +
 
 +
[[Image:desargues.png|right|thumb|240px]]
 +
 
 +
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 [[THEME_1_OPERATION2 |Operation 2]]).
  
−
Nous avons également commencé à explorer un premier problème d'algorithmique géométrique où interviennent des notions de cartes combinatoires et de plongement. Il s'agit de la construction de l'enveloppe convexe de points du plan. Selon le même principe que ci-dessus, nous avons conçu un algorithme fonctionnel en Coq travaillant par induction structurelle sur nos contours et s'inspirant de l'algorithme incrémental classique. Très rapidement, un prototype en OCaml a pu en être extrait et testé à l'aide d'une interface graphique ad hoc. La preuve de correction de cet algorithme, basé sur une classification fine des brins et de leurs propriétés, est en bonne voie (Christophe Brun, Nicolas Magaud, Jean-François Dufourd). Ce travail a été présenté en juin 2007 aux Journées de Géométrie et Informatique (Nice-Sophia, ERCIM, juin 2007) du nouveau GDR IM. 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. Ce travail, commencé par Christophe Brun et Nicolas Magaud au cours de l'été 2006, se poursuit actuellement.
+
[[fr:THEME_1_OPERATION3]]

Latest revision as of 10:36, 5 August 2009

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

Jfd hmap1.png
Jfd hmap1Torus.png
Jfd polyhedra1.png
Jfd hmap2.png
Jfd nf.png

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.

Jfd seg subd1seg.png
Jfd seg hmap2.png
Jfd seg hmap3.png
Jfd seg hmap2seg.png
Jfd seg hmap3seg.png


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

AreaMethod.png

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

Desargues.png

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

Retrieved from "https://igg.icube.unistra.fr/en/index.php?title=THEME_1_OPERATION3&oldid=1882"