Real Calculus

Description: This library includes a formalization of Real Analysis following Bishop (see references). Starting with the real numbers and partial functions axiomatized in the algebraic hierarchy, we define notions of continuity, differentiability and integral in compact intervals and in more general subsets of IR.
    The formalization includes:

• results about preservation of continuity through algebraic operations;
• the usual rules for derivation; - formalization of power series and Taylor series;
• several formulations of Rolle's Theorem, the Mean Law, convergence theorems and error estimates for Taylor series;
• the fundamental theorem of calculus;
• definition of the usual elementary transcendental functions (exp, sin, cos, tan) and their inverses (log, arcsin, arccos, arctan), along with their usual algebraic properties;
• tactics for automatically proving usual properties about continuity and derivatives of these functions.

References:  

• For the mathematical content:
• Bishop, E., "Foundations of Constructive Analysis", McGraw-Hill Book Company, 1967
•  About the formalization itself:
• Cruz-Filipe, L., "Formalizing Real Calculus in Coq", in  Theorem Proving in Higher Order Logics , Carreño, V., Muñoz, C. and Tahar, S. (eds.), NASA Conference Proceedings, Hampton VA, 2002 (ps, pdf)
• ``A Constructive Formalization of the Fundamental Theorem of Calculus'', © Springer-Verlag, in Types 2002, Proceedings of the workshop Types for Proof and Programs, Geuvers, H. and Wiedijk, F. (eds.), LNCS, Springer-Verlag 2003; ps,pdf

Maintainer: Luís Cruz-Filipe

Developers: Luís Cruz-Filipe

Documentation

Download