Translating a Fragment of Weak Type Theory into Type Theory with Open Terms

摘要

One of the main application areas of interactive proof assistants is the formal-ization of mathematical texts. This formalization not only allows mathematical texts to be handled electronically, but also to be checked for correctness. Due to the level of detail required in the formalization, formalized texts eliminate ambiguities that may be present in an informally presented mathematical texts. The process of formalization begins with such an informal text given either on paper or kept in the author's mind. Then this text needs to be written down in a computer-processable formal language and fed into a theorem prover. In this theorem prover all the details of the proofs in the text need to be fully worked out. Once this is done, we have a completely formalized version of the original mathematical text. The main problem when formalizing is how to manage the complexity of the details needed for a completely formal proof while at the same time ensuring maximum reliability of the whole formalization process. This paper is a part of an ongoing effort to study the whole process of formalization starting from the informal document and ending with the full formalization. Our approach to formalization is to use several intermediate steps designed to reduce the possibility of introducing errors during formalization and at the same time to explore the opportunities for computer assistance. The contribution of this paper is the description of a set of formal rules that allow us to automatically make one of these steps - namely the step from our vernacular language Weak Type Theory (WTT) to the language of a theorem prover (Type Theory). We also present an implementation of these rules and report some early results from experiments with it.