Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

Formalizing real analysis for polynomials

Cyril Cohen 1, 2, 3 
Abstract : When reasoning formally with polynomials over real numbers, or more generally real closed fields, we need to be able to manipulate easily statements featuring an order relation, either in their conditions or in their conclusion. For instance, we need to state the intermediate value theorem and the mean value theorem and we need tools to ease both their proof and their further use. For that purpose we propose a Coq library for ordered integral domains and ordered fields with decidable comparison. In this paper we present the design choices of this libraries, and show how it has been used as a basis for developing a fare amount of basic real algebraic geometry.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Sunday, December 12, 2010 - 5:27:44 PM
Last modification on : Friday, November 18, 2022 - 9:24:27 AM
Long-term archiving on: : Friday, December 2, 2016 - 6:17:39 PM


Files produced by the author(s)


  • HAL Id : inria-00545778, version 1



Cyril Cohen. Formalizing real analysis for polynomials. {date}. ⟨inria-00545778⟩



Record views


Files downloads