Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
This paper presents a 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's 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
Computational topology
Computer-aided proofs
Coq
Planar subdivisions
Hypermaps
Jordan Curve Theorem
253-264
Regular Paper
Jean-Francois
Dufourd
Jean-Francois Dufourd
10.4230/LIPIcs.STACS.2008.1349
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode