Real closed fields

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.

Meta

• Author(s):
  • Cyril Cohen (initial)
  • Assia Mahboubi (initial)
• License: CeCILL-B
• Compatible Coq versions: Coq 8.17 or later
• Additional dependencies:
  • MathComp ssreflect 2.1 or later
  • MathComp algebra
  • MathComp field
  • MathComp bigenough 1.0.0 or later
• Coq namespace: mathcomp.real_closed
• Related publication(s):
  • Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination doi:10.2168/LMCS-8(1:2)2012
  • Construction of real algebraic numbers in Coq doi:10.1007/978-3-642-32347-8_6

Building and installation instructions

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

Documentation

The repository contains

• the decision procedure rcf_sat and its corectness lemma rcf_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 a rcfType when F is an archimedean field, and the characteristic theorems of section RealClosureTheory.
• the definition complex R, a construction of the algebraic closure of a real closed field, which is canonically a numClosedFieldType that additionally satisfies complexalg_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.

Development instructions

With nix.

1. 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.

2. 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 call nix-shell with option --arg print-env true).

3. You are now in the correct work environment. You can do

   make

   and do whatever you are accustomed to do with Coq.

4. In particular, you can edit files using emacs or coqide.

   • 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 option

     nix-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.