Abstract
This paper presents a completely formalized proof of a discrete form of the Jordan Curve Theorem. It is based on a hypermap model of planar subdivisions, formal specifications and proofs assisted by the Coq system. Fundamental properties are proven by structural or noetherian induction: Genus Theorem, Euler Formula, constructive planarity criteria. A notion of ring of faces is inductively defined and a Jordan Curve Theorem is stated and proven for any planar hypermap.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Bauer, G., Nipkow, T.: The 5 colour theorem in Isabelle/Isar. In: Theorem Proving in HOL Conf. LNCS, vol. 2410, pp. 67–82. Springer, New York (2002)
Bertot, Y., Castéran, P.: Interactive theorem proving and program development—Coq’art: the calculus of inductive construction. In: Text in Theoretical Computer Science, An EATCS Series. Springer, New York (2004)
Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graph. Models Image Process. 56, 1 29–60 (1994)
Chen, L.: Note on the discrete Jordan Curve Theorem. In: SPIE Conf. on Vision Geometry VIII, vol. 3811, pp. 82–94. SPIE, Bellingham (1999)
The Coq Team Development-TypiCal Project: The Coq proof assistant reference manual—version 8.1. INRIA, Le Chesnay http://coq.inria.fr/doc-fra.html (2007)
Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. In: EUROCAL. LNCS, vol. 203. Springer, New York (1985)
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. Theor. Comp. Sci. 323, 399–442 (2004)
Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial oriented maps. Comput. Geom. Theory Appl. 16, 129–156 (2000)
Dufourd, J.-F.: Design and certification of a new optimal segmentation program with hypermaps. Pattern Recogn. 40, 2974–2993 (2007). doi:10.101b/j.patcog.2007.02.013
Dufourd, J.-F.: Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof. Theor. Comp. Sci. 403, 133–159 (2008). doi:10.101b/j.tcs.2008.02.012
Dufourd, J.-F.: Discrete Jordan Curve Theorem: a proof formalized in Coq with hypermaps. In: Weil, P. (ed.) Symp. on Theoretical Aspects on Computer Science, 12 pp (2008). doi:hal-archives-ouvertes.fr/hal-002211501~v1
Filliâtre, J.C.: Formal proof of a program: FIND. Sci. Comput. Program. 24(3), 332–340 (2006)
Françon, J.: Discrete combinatorial surfaces. CVGIP, Graph. Models Image Process. 57(1), 20–26 (1995)
Gonthier, G.: A computer-checked proof of the four colour theorem, 57 pp. Microsoft Research, Cambridge. http://research.microsoft.com/~gonthier (2005)
Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system, 75 pp. RR 6455, Microsoft Research-INRIA. http://hal.inria.fr/inria-00258384/ (2007)
Gonthier, G.: Formal proof - the four-Colour theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)
Griffiths, H.: Surfaces. Cambridge University Press, Cambridge (1981)
Hales, T.: Formalizing the proof of the Kepler conjecture. In: Theorem Proving in HOL Conf. LNCS, vol. 3223, p. 117. Springer, New York (2004)
Hales, T.: A verified proof of the Jordan Curve Theorem. Seminar talk. Dep. of Math., University of Toronto http://www.math.pitt.edu/~thales (2005)
Hales, T.: The Jordan Curve Theorem, formally and informally. Am. Math. Mon. 114(10), 882–893 (2007)
Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant—a tutorial—version 8.0. Tech. report, INRIA, France http://coq.inria.fr/doc-fra.html (2004)
Khachan, M., Chenin, P., Deddi, H.: Digital pseudomanifolds, digital weakmanifolds and Jordan-Brower separation theorem. Discrete Appl. Math. 125(1), 45–57 (2003)
Kornilowicz, A.: Jordan Curve Theorem. Formaliz. Math. 13(4), 481–491 (2005) (Univ. of Bialystock)
Kong, T.Y., Rosenfeld, A.: Digital topology: introduction and survey. Comput. Vis. Image Process. 48, 357–393 (1989)
Malgouyres, R.: A definition of surfaces of Z3—a new 3D discrete Jordan theorem. Theor. Comp. Sci. 186, 1–41 (1997)
Paulin-Mohring, C.: Inductive definition in the system Coq—rules and properties. In: Typed Lambda-Calculi and Applications. LNCS, vol. 664, pp. 328–345. Springer, New York (1993)
Simpson, C.: Explaining Gabriel-Zisman localization to the computer. J. Autom. Reason. 36 (2006). doi:10.1007/s10817-006-9038-x,259–285
Slapal, J.: A digital analog of the Jordan Curve Theorem. Discrete Appl. Math. 139(1–3), 231–251 (2004)
Stahl, S.: A combinatorial analog of the Jordan Curve Theorem. J. Comb. Theory B 26, 28–38 (1983)
Tutte, W.T.: Combinatorial oriented maps. Can. J. Math. XXXI(5), 986–1004 (1979)
Tutte, W.T.: Graph theory. In: Encyclopedia of Mathematics and its Applications. Addison Wesley, Reading (1984)
Veblen, O.: Theory on plane curves in non-metrical analysis situs. Trans. Am. Math. Soc. 6, 83–98 (1905)
Vince, A., Little, C.H.C.: Discrete Jordan Curve Theorems. J. Comb. Theory B 47, 251–261 (1989)
Yamamoto, M., Nishizaki, S., Hagiya, M., Tamai, T.: Formalization of planar graphs. In: Theorem Proving in HOL Conf. LNCS, vol. 971, pp. 369–384. Springer, New York (1995)
Author information
Authors and Affiliations
Corresponding author
Additional information
This research is supported by the “white” project GALAPAGOS, French ANR, 2007.
Rights and permissions
About this article
Cite this article
Dufourd, JF. An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. J Autom Reasoning 43, 19–51 (2009). https://doi.org/10.1007/s10817-009-9117-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9117-x