Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective

Nicolas Magaud 1 Agathe Chollet 2 Laurent Fuchs 3
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
2 Laboratoire MIA
MIA - Mathématiques, Image et Applications
Abstract : This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on previous work by Chollet, Fuchs et al. where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. Laugwitz-Schmieden numbers are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated. In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.
Type de document :
Article dans une revue
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2015, 〈10.1007/s10472-014-9434-6〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01066671
Contributeur : Nicolas Magaud <>
Soumis le : lundi 22 septembre 2014 - 18:59:14
Dernière modification le : jeudi 11 janvier 2018 - 06:24:11
Document(s) archivé(s) le : mardi 23 décembre 2014 - 10:45:31

Fichier

magaud-chollet-fuchs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nicolas Magaud, Agathe Chollet, Laurent Fuchs. Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2015, 〈10.1007/s10472-014-9434-6〉. 〈hal-01066671〉

Partager

Métriques

Consultations de la notice

245

Téléchargements de fichiers

235