Advertisement

Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs

  • Yves Bertot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm, questions of symmetry appear and this exposition attempts to give an account of how these symmetries can be handled. All this work relies on formal developments made with Coq and the mathematical components library.

References

  1. 1.
    Brun, C., Dufourd, J.-F., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8), 436–457 (2012).  https://doi.org/10.1016/j.comgeo.2010.06.006MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.8 (2018)Google Scholar
  3. 3.
    Dehlinger, C., Dufourd, J.-F.: Formalizing generalized maps in Coq. Theor. Comput. Sci. 323(1–3), 351–397 (2004).  https://doi.org/10.1016/j.tcs.2004.05.003MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Devillers, O., Pion, S., Teillaud, M.: Walking in a triangulation. Int. J. Found. Comput. Sci. 13(2), 181–199 (2002).  https://doi.org/10.1142/s0129054102001047MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Dufourd, J.-F.: An intuitionistic proof of a discrete form of the Jordan Curve theorem formalized in Coq with combinatorial hypermaps. J. Autom. Reason. 43(1), 19–51 (2009).  https://doi.org/10.1007/s10817-009-9117-xMathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Dufourd, J.-F., Bertot, Y.: Formal study of plane delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 211–226. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14052-5_16CrossRefGoogle Scholar
  7. 7.
    Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333–333. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-87827-8_28CrossRefGoogle Scholar
  8. 8.
    Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39634-2_14CrossRefGoogle Scholar
  9. 9.
    Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Form. Reason. 3(2), 95–152 (2010).  https://doi.org/10.6092/issn.1972-5787/1979MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, 1–29 (2017).  https://doi.org/10.1017/fmp.2017.1MathSciNetCrossRefGoogle Scholar
  11. 11.
    Hales, T.C.: The Jordan Curve theorem, formally and informally. Am. Math. Mon. 114(10), 882–894 (2007). http://www.jstor.org/stable/27642361MathSciNetCrossRefGoogle Scholar
  12. 12.
    Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of 2015 Conference on Certified Programs and Proofs, CPP 2015 (Mumbai, January 2015), pp. 129–136. ACM Press, New York (2015).  https://doi.org/10.1145/2676724.2693164
  13. 13.
    Knuth, D.E. (ed.): Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55611-7CrossRefzbMATHGoogle Scholar
  14. 14.
    Lawson, C.L.: Software for \(c^{1}\) surface interpolation. JPL Publication 77–30, NASA Jet Propulsion Laboratory (1977). https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/19770025881.pdf
  15. 15.
    Mahboubi, A., Tassi, E.: Mathematical components (2018). https://math-comp.github.io/mcb
  16. 16.
    Meikle, L.I., Fleuriot, J.D.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 1–18. Springer, Heidelberg (2006).  https://doi.org/10.1007/11615798_1CrossRefzbMATHGoogle Scholar
  17. 17.
    Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346–361. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44755-5_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Inria Sophia Antipolis – Méditerranée and Université Côte d’AzurSophia Antipolis CedexFrance

Personalised recommendations