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, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on a previous work by some of the authors where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. A formalization of a first attempt for a model of the Hartong-Reeb line based on the work of Laugwitz and Schmieden is also presented and analyzed. We hope that this work could help reasoning and implementation of numeric computations in geometric systems.

N. Magaud , A. Chollet , L. Fuchs

Automated Deduction in Geometry - 2010

@Inproceedings{7-MCF10,
 author = {Magaud, N. and Chollet, A. and Fuchs, L.},
 title = {Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective},
 booktitle  = {Automated Deduction in Geometry},
 month = {Jul},
 year = {2010},
 editor = {J\"urgen Richter-Gebert },
 publisher = {Pascal Schreck},
 x-international-audience = {Yes},
 x-language = {EN},
 url = {http://publis.icube.unistra.fr/7-MCF10}
}