Sciweavers

Share
AMAI
2015
Springer

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

4 years 10 months ago
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.
Nicolas Magaud, Agathe Chollet, Laurent Fuchs
Added 15 Apr 2016
Updated 15 Apr 2016
Type Journal
Year 2015
Where AMAI
Authors Nicolas Magaud, Agathe Chollet, Laurent Fuchs
Comments (0)
books