Metric Spaces

Description: This library provides a model of the real numbers, CR, that is suitable for computing with inside Coq. Also included is a rasterization library for computing plots of uniformly continuous functions.
    The formalization includes:

• field operations, abs, sin, cos, exp, square root, ln, arctan for CR.
• integration of uniformly continuous functions on [0,1]
• proofs that these operations are equivalent to the ones on IR.
• a tactic, IR_solve_ineq, for automatically strict inequalities over IR that are closed expressions.
• a function, PlotQ for creating plots of uniformly continuous functions

References:  

• Russell O’Connor. "A monadic, functional implementation of real numbers", Mathematical. Structures in Comp. Sci., 17(1):129–159, 2007.
• Russell O’Connor. "Certified exact transcendental real number computation in Coq". In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, LNCS. Springer-Verlag, 2008. to appear.
• Russell O’Connor. "A Computer Verified Theory of Compact Sets". to appear.

Maintainer: Russell O’Connor

Developers: Russell O’Connor

Documentation

Download