Construction of real algebraic numbers in Coq

Cyril Cohen (1, 2, 3, 4)

1 SPECFUN - Symbolic Special Functions : Fast and Certified
2 MSR - INRIA - Microsoft Research - Inria Joint Centre
3 TYPICAL - Types, Logic and computing
4 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.

Mots clés: coq; real algebraic numbers; formalization of mathematics; quotient; real closure; small scale reflexion

Domaines: Autre [cs.OH]

Cyril Cohen. Construction of real algebraic numbers in Coq. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. ⟨hal-00671809v2⟩