An Implementation of the Heine-Borel Covering Theorem in Type Theory
Jan Cederquist, Giménez, E., Paulin-Mohring, C. · University of Twente Research Information · 1996
. We describe an implementation, in type theory, of a proof of a pointfree formulation of the Heine-Borel covering theorem for intervals with rational endpoints. 1 Introduction The proof presented here is a complete formalisation of the proof presented in "A constructive proof of the Heine-Borel covering theorem for formal reals" [CN]. We describe an implementation, in type theory, of a proof of a pointfree formulation of the Heine-Borel covering theorem for intervals with rational endpoints. The implementations also contain a definition of formal spaces as a type, and definitions of the continuum and the closed rational interval as instances of that type. The paper is organised as follows: in section 2 we describe the proof-checker Half, in which the implementation has been done, and the type theory it is based on. The rest of the paper is devoted to formal definitions and the proof of the Heine-Borel covering theorem. In section 3 some general definitions are given. In section 4 we ...