Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb [16], the HarthongReeb line. This model was at the origin of important developments in the Discrete Geometry field [31]. The formalization is based on the work presented in [8,7] where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges [4]. Laugwitz-Schmieden numbers [20] are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated [7]. 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: Journal
• Year: 2015
• Where: AMAI
• Authors: Nicolas Magaud, Agathe Chollet, Laurent Fuchs
• Keywords: AMAI 2015, Artificial Intelligence