Journal of Automated Reasoning

, Volume 43, Issue 1, pp 19–51 | Cite as

An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps

  • Jean-François Dufourd


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.


Formal specifications Computer-aided proofs Coq system Computational topology Planar subdivisions Combinatorial hypermaps Discrete Jordan Curve Theorem 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graph. Models Image Process. 56, 1 29–60 (1994)CrossRefGoogle Scholar
  4. 4.
    Chen, L.: Note on the discrete Jordan Curve Theorem. In: SPIE Conf. on Vision Geometry VIII, vol. 3811, pp. 82–94. SPIE, Bellingham (1999)Google Scholar
  5. 5.
    The Coq Team Development-TypiCal Project: The Coq proof assistant reference manual—version 8.1. INRIA, Le Chesnay (2007)
  6. 6.
    Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. In: EUROCAL. LNCS, vol. 203. Springer, New York (1985)Google Scholar
  7. 7.
    Cori, R.: Un code pour les graphes planaires et ses applications. Astérisque 27 (1970) (Société Math. de France)Google Scholar
  8. 8.
    Dehlinger, C., Dufourd, J.-F.: Formalizing the trading theorem in Coq. Theor. Comp. Sci. 323, 399–442 (2004)MATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial oriented maps. Comput. Geom. Theory Appl. 16, 129–156 (2000)MATHMathSciNetGoogle Scholar
  10. 10.
    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 MATHCrossRefGoogle Scholar
  11. 11.
    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 MATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    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:
  13. 13.
    Filliâtre, J.C.: Formal proof of a program: FIND. Sci. Comput. Program. 24(3), 332–340 (2006)Google Scholar
  14. 14.
    Françon, J.: Discrete combinatorial surfaces. CVGIP, Graph. Models Image Process. 57(1), 20–26 (1995)CrossRefGoogle Scholar
  15. 15.
    Gonthier, G.: A computer-checked proof of the four colour theorem, 57 pp. Microsoft Research, Cambridge. (2005)
  16. 16.
    Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system, 75 pp. RR 6455, Microsoft Research-INRIA. (2007)
  17. 17.
    Gonthier, G.: Formal proof - the four-Colour theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)MATHMathSciNetGoogle Scholar
  18. 18.
    Griffiths, H.: Surfaces. Cambridge University Press, Cambridge (1981)MATHGoogle Scholar
  19. 19.
    Hales, T.: Formalizing the proof of the Kepler conjecture. In: Theorem Proving in HOL Conf. LNCS, vol. 3223, p. 117. Springer, New York (2004)Google Scholar
  20. 20.
    Hales, T.: A verified proof of the Jordan Curve Theorem. Seminar talk. Dep. of Math., University of Toronto (2005)
  21. 21.
    Hales, T.: The Jordan Curve Theorem, formally and informally. Am. Math. Mon. 114(10), 882–893 (2007)MATHMathSciNetGoogle Scholar
  22. 22.
    Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant—a tutorial—version 8.0. Tech. report, INRIA, France (2004)
  23. 23.
    Khachan, M., Chenin, P., Deddi, H.: Digital pseudomanifolds, digital weakmanifolds and Jordan-Brower separation theorem. Discrete Appl. Math. 125(1), 45–57 (2003)MATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Kornilowicz, A.: Jordan Curve Theorem. Formaliz. Math. 13(4), 481–491 (2005) (Univ. of Bialystock)Google Scholar
  25. 25.
    Kong, T.Y., Rosenfeld, A.: Digital topology: introduction and survey. Comput. Vis. Image Process. 48, 357–393 (1989)CrossRefGoogle Scholar
  26. 26.
    Malgouyres, R.: A definition of surfaces of Z3—a new 3D discrete Jordan theorem. Theor. Comp. Sci. 186, 1–41 (1997)MATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
    Simpson, C.: Explaining Gabriel-Zisman localization to the computer. J. Autom. Reason. 36 (2006). doi: 10.1007/s10817-006-9038-x,259–285 MATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Slapal, J.: A digital analog of the Jordan Curve Theorem. Discrete Appl. Math. 139(1–3), 231–251 (2004)MATHMathSciNetGoogle Scholar
  30. 30.
    Stahl, S.: A combinatorial analog of the Jordan Curve Theorem. J. Comb. Theory B 26, 28–38 (1983)MathSciNetGoogle Scholar
  31. 31.
    Tutte, W.T.: Combinatorial oriented maps. Can. J. Math. XXXI(5), 986–1004 (1979)MathSciNetGoogle Scholar
  32. 32.
    Tutte, W.T.: Graph theory. In: Encyclopedia of Mathematics and its Applications. Addison Wesley, Reading (1984)Google Scholar
  33. 33.
    Veblen, O.: Theory on plane curves in non-metrical analysis situs. Trans. Am. Math. Soc. 6, 83–98 (1905)MATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    Vince, A., Little, C.H.C.: Discrete Jordan Curve Theorems. J. Comb. Theory B 47, 251–261 (1989)MathSciNetGoogle Scholar
  35. 35.
    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)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.UFR de Mathématique et d’Informatique, Laboratoire des Sciences de l’Image, de l’Informatique et de la Télédétection (UMR CNRS-ULP 7005)Université de StrasbourgIllkirchFrance

Personalised recommendations