This library contains definitions and theorems about real closed fields, with a construction of the real closure and the algebraic closure (including a proof of the fundamental theorem of algebra). It also contains a proof of decidability of the first order theory of real closed field, through quantifier elimination.
- Author(s):
- Cyril Cohen (initial)
- Assia Mahboubi (initial)
- License: CeCILL-B
- Compatible Coq versions: Coq 8.17 or later
- Additional dependencies:
- Coq namespace:
mathcomp.real_closed
- Related publication(s):
The easiest way to install the latest released version of Real closed fields is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-real-closed
To instead build and install manually, do:
git clone https://github.com/math-comp/real-closed.git
cd real-closed
make # or make -j <number-of-cores-on-your-machine>
make install
The repository contains
- the decision procedure
rcf_sat
and its corectness lemmarcf_satP
for the first order theory of real closed fields through certified quantifier elimination - the definition
{realclosure F}
, a construction of the real closure of an archimedean field, which is canonically arcfType
whenF
is an archimedean field, and the characteristic theorems of sectionRealClosureTheory
. - the definition
complex R
, a construction of the algebraic closure of a real closed field, which is canonically anumClosedFieldType
that additionally satisfiescomplexalg_algebraic
.
Except for the end-results listed above, one should not rely on anything.
The formalization is based on the Mathematical Components library for the Coq proof assistant.
- Install nix:
-
To install it on a single-user unix system where you have admin rights, just type:
sh <(curl https://nixos.org/nix/install)
You should run this under your usual user account, not as root. The script will invoke
sudo
as needed.For other configurations (in particular if multiple users share the machine) or for nix uninstallation, go to the appropriate section of the nix manual.
-
You need to log out of your desktop session and log in again before you proceed to step 2.
-
Step 1. only need to be done once on a same machine.
-
Open a new terminal. Navigate to the root of the Abel repository. Then type:
nix-shell
- This will download and build the required packages, wait until you get a shell.
- You need to type this command every time you open a new terminal.
- You can call
nixEnv
after you start the nix shell to see your work environemnet (or callnix-shell
with option--arg print-env true
).
-
You are now in the correct work environment. You can do
make
and do whatever you are accustomed to do with Coq.
-
In particular, you can edit files using
emacs
orcoqide
.-
If you were already using emacs with proof general, make sure you empty your
coq-prog-name
variables and any other proof general options that used to be tied to a previous local installation of Coq. -
If you do not have emacs installed, but want to use it, you can go back to step 2. and call
nix-shell
with the following optionnix-shell --arg withEmacs true
in order to get a temporary installation of emacs and proof-general. Make sure you add
(require 'proof-site)
to your$HOME/.emacs
.
-