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.
Many of the ideas in the current work arose from the author's previous work on the auto2 prover @cite_21 . In particular, the definition of macros is similar to that of proof steps in the earlier work. The style of programming proof automation based on building proof terms is also already present there.
@cite_21
2403724605
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle HOL, and applied it to several formalization projects in mathematics and computer science, demonstrating the high level of automation it can provide in a variety of possible proof tasks.