Abstract
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bauer, G., Nipkow, T.: The 5 Colour Theorem in Isabelle/Isar. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 67–82. Springer, Heidelberg (2002)
de Berg, M., Cheong, O., van Kreveld, M., Overmars, M.: Computational Geometry: Algorithms and Applications, 3rd edn. Springer, Heidelberg (2008)
Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graphical Models and Image Processing 56(1), 29–60 (1994)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions, Text in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Bertot, Y., Magaud, N., Zimmermann, P.: A proof of GMP square root. Journal of Automated Reasoning 29, 225–252 (2002)
Besson, F.: Fast Reflexive Arithmetic Tactics: the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007)
Boissonnat, J.-D., Devillers, O., Pion, S., Teillaud, M., Yvinec, M.: Tiangulations in CGAL. Comp. Geom. - Th and Appl. 22(1-3), 5–9 (2002); Spec. iss. SOCG’00 (2002)
Brun, C., Dufourd, J.-F., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. (submitted 2009)
The Coq Development Team: The Coq Proof Assistant Reference Manual - Version 8.2. INRIA, France (2009), http://coq.inria.fr
Cori, R.: Un Code pour les Graphes Planaires et ses Applications. Astérisque 27 (1970); Société Math. de France
Dehlinger, C., Dufourd, J.-F.: Formalizing the trading theorem in Coq. Theoretical Computer Science 323, 399–442 (2004)
Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial oriented maps. Comp. Geometry - Th. and Appl. 16(2), 129–156 (2000)
Dufourd, J.-F.: Design and formal proof of a new optimal image segmentation program with hypermaps. Pattern Recognition 40, 2974–2993 (2007)
Dufourd, J.-F.: Polyhedra genus theorem and Euler Formula: A hypermap-formalized intuitionistic proof. Theor. Comp. Sc. 403, 133–159 (2008)
Dufourd, J.-F.: An Intuitionistic Proof of a Discrete Form of the Jordan Theorem Formalized in Coq with Hypermaps. Journal of Automated Reasoning 43, 19–51 (2009)
Dufourd, J.-F.: Reasoning formally with Split, Merge and Flip in plane triangulations (submitted 2009), http://lsiit.u-strasbg.fr/Publications/index.php
Dufourd, J.-F., Bertot, Y.: Formal proof of Delaunay by edge flipping (2010), http://galapagos.gforge.inria.fr/devel/DelaunayFlip.tgz
Edelsbrunner, H.: Triangulations and meshes in combinatorial geometry. In: Acta Numerica, pp. 1–81. Cambridge Univ. Press, Cambridge (2000)
Flato, E., et al.: The Design and Implementation of Planar Maps in CGAL. WAE 1999 16 (2000); In: Vitter, J.S., Zaroliagis, C.D. (eds.) WAE 1999. LNCS, vol. 1668, pp. 154–168. Springer, Heidelberg (1999)
Fousse, L., et al.: MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2) (2007)
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)
Gonthier, G.: Formal proof - the four-Colour theorem. Not. Am. Math. Soc. 55, 1382–1393 (2008)
Guibas, L., Stolfi, J.: Primitives for the Manipulation of General Subdivisions and the Computation of Voronoi Diagrams. ACM TOG 4(2), 74–123 (1985)
Kettener, L., Mehlhorn, K., Pion, S., Scirra, S., Yap, C.: Classroom examples of robustness problems in geometric computations. Computational Geometry - Theory and Applications 40, 61–78 (2008)
Knuth, D.E.: Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992)
Meikle, L.I., Fleuriot, J.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 1–18. Springer, Heidelberg (2006)
Melquiond, G., Pion, S.: Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates. Theoretical Informatics and Applications, EDP Science 41(1), 57–69 (2007)
Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Annals of Mathematics and Artificial Intelligence 56(3-4), 245–272 (2009)
Pichardie, D., Bertot, Y.: Formalizing Convex Hulls Algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346–361. Springer, Heidelberg (2001)
Priest, D.: Algorithms for Arbitrary Precision Floating Point Arithmetic. In: Tenth Symposium on Computer Arithmetic, pp. 132–143. IEEE, Los Alamitos (1991)
Puitg, F., Dufourd, J.-F.: Formal specifications and theorem proving breakthroughs in geometric modelling. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 401–427. Springer, Heidelberg (1998)
Tutte, W.E.: Graph Theory. Encyclopedia of Mathematics and its Applications. Addison Wesley, Reading (1984)
Yap, C.-K., Pion, S.: Special Issue on Robust Geometric Algorithms and their Implementations. Computational Geometry - Theory and Applications 33(1-2) (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dufourd, JF., Bertot, Y. (2010). Formal Study of Plane Delaunay Triangulation. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)