The design of modern proof assistants is faced with several sometimes conflicting goals, including scalability, extensibility, and soundness of proof checking. In this paper, we propose a new design for proof assistants, in an attempt to address some of these difficulties. The new design is characterized by a pervasive use of macros in representing and checking proofs, and a foundational format for theory files based on JSON. We realize these ideas in a prototype proof assistant called holpy, implemented in Python. We also demonstrate how proof automation can be extended using Python under this framework. Finally, we present a case study about a simple imperative language.
Lean @cite_10 already proposed the use of macros to shorten proof terms. However, this functionality does not appear to be widely used in user-defined theories. The virtual machine for Lean evaluates operations on natural numbers, integers, and arrays directly using C++ functions, rather than within the logic, resulting in a large speedup in many applications @cite_3 . The main difference in our work is that definition of macros is easily accessible and widely applied at the user level. We also demonstrate the use of macros in logical foundations without explicit Curry-Howard correspondence.
@cite_10 @cite_3
2753707546 1464569014
We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the met alanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation. Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.