Dedekind Reals

A formalization of Dedekind reals numbers that started as a student project at the University of Ljubljana under the supervision of Andrej Bauer, and was brought to the present state by Vincent Semeria.

At this point the formalization of the field of reals is finished. There are still several unfinished theorems concering the lattice-theoretic structure of the reals (search for todo in the Coq files). We would be delighted by contributions that would bring the formalization closer to completion.

Meta

• Author(s):
  • Andrej Bauer
  • Vincent Semeria
• Coq-community maintainer(s):
  • Andrej Bauer (@andrejbauer)
• License: MIT License
• Compatible Coq versions: 8.16 and later
• Additional dependencies: none
• Coq namespace: DedekindReals
• Related publication(s): none

Building instructions

To build and install, do:

git clone https://github.com/coq-community/dedekind-reals.git
cd dedekind-reals
make   # or make -j <number-of-cores-on-your-machine> 
make install

Structure of the modules

• MiscLemmas: various lemmas about rational numbers
• Cut: definition of Dedekind cuts and several other basic notions
• Additive: Additive structure of the reals
• Multiplication : Multiplicative structure of the relas
• Order : The order on the reals
• Archimedean: the proof that the reals satisfy the archimedean property
• Completeness: the reals are Dedekind-complete