Skip to content

Latest commit

 

History

History
68 lines (52 loc) · 2.57 KB

README.md

File metadata and controls

68 lines (52 loc) · 2.57 KB
Raw

Dedekind Reals

Docker CI Contributing Code of Conduct Zulip

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):
  • 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