ABSTRACT. In this talk we present an ongoing effort to develop a Coq formal library about elementary real analysis, in a firmly classical setting. Almost all existing proof assistants on the market have been used to define real numbers, and to investigate the formalization of real, and sometimes also complex, analysis. A survey by Boldo et al. reviews the different approaches and the breadth of the existing developments. In particular, the Coq standard library provides an axiomatization of real numbers, with a classical flavor and the Coquelicot external library is a conservative extension thereof. At the time of writing, these libraries however cover far less material that their analogues in the HOL ecosystem, including Harrison’s HOL Light library and its translation to Isabelle/HOL.

The present work is yet another attempt at providing a library for classical analysis in Coq. The motivation is twofold. First, the library relies on stronger classical axioms, so as to get closer to the logical formalism used in classical mathematics. In particular, this impacts the formalization of compactness-related facts. Second, the library is designed along the formalization methodology put into practice in the Mathematical Components libraries. The latter libraries are essentially geared towards algebra and this work aims at providing an extension for topics in analysis. However, we incorporated a significant subset of the Coquelicot library. The main original contributions lie in the effort put in the infrastructure of the library: automation, notations, etc. The library is still rather incomplete, but it proved already useful enough for a few applications.