Hopster: Automated discovery of mathematical properties in HOL

Abstract

A new tactic for HOL is proposed that is suitable for proving equational properties of functional programs. HOL has numerous tactics that automate the process of proving a logical statement. Yet none incorporate the discovery of useful lemmas in their process, an essential activity when performing a manual proof. The Hopster tactic is able to discover new lemmas via a technique known as theory exploration, implemented in a tool called QuickSpec. So far, theory exploration has been applied with increasing success for generating many useful properties when given a theory of considerable size. A dual to this scenario occurs when the theory is fairly well-developed and the user is interested in proving a specific new property. This work pays particular attention to the second scenario, when the user wishes to prove a specific goal using theory exploration. The tactic has been designed to support this case by automating the selection of which functions to explore. The design and testing of this selection process are the principal contributions of this work. The effectiveness and efficiency of the implementation are measured on a set of test cases to identify where the tactic performs well and where further improvements remain. It is hoped that Hopster serves as a useful tool that supports the development of verified functional programs.