# 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).
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).
4. 4.
Devillers, O., Pion, S., Teillaud, M.: Walking in a triangulation. Int. J. Found. Comput. Sci. 13(2), 181–199 (2002).
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).
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).
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).
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).
9. 9.
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Form. Reason. 3(2), 95–152 (2010).
10. 10.
Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, 1–29 (2017).
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/27642361
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).
13. 13.
Knuth, D.E. (ed.): Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992).
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).
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).