How to make ad hoc proof automation less ad hoc by Aleksandar Nanevski

To overcome the burden involved in interactively mechanizing mathematical proofs on a computer, most theorem-proving systems such as Coq and Isabelle, support user-customizable proof automation by means of tactics. 

Tactics, introduced by Milner in Edinburgh LCF, are programs that can inspect and algorithmically manipulate assertions in the prover's base logic, with the goal of simplifying or discharging them. 

While tactics are clearly useful in practice, they are beset by a number of fundamental limitations. They are written in a domain-specific scripting language, which by necessity resides outside of the prover's base logic, and lacks the base logic's precise typing. This in turn makes tactics famously difficult to maintain, and impossible to precisely specify and verify. 

In this talk I will present an alternative architecture for user-customizable proof automation, specifically in Coq, which overcomes the above limitation. The starting point is the observation, well known as Curry-Howard isomorphism, that proofs and programs in Coq are equivalent entities. Thus, concepts and ideas developed in the world of programming, can be applied to mathematics as well. 

In particular, I will show how the idea of overloading a method name in programming (a.k.a. ad hoc polymorphism, static dispatch), can be applied to mathematical theorems. 

Such an 'overloaded theorem' realizes a method for an automated discharge of a class of proof obligations, which, unlike a tactic, can itself be verified in the base logic of Coq, and flexibly composed with other Coq programs, theorems and proofs.