Theorems for real closed fields

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.

Installation

If you already have OPAM installed:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-real_closed