The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
This tool addresses the problem of proof automation and user assistance for developers and researchers using Coq, though it appears incremental as it builds on existing learning-based methods for proof assistants.
The paper introduces Tactician, a tool that assists users in making tactical proof decisions in the Coq Proof Assistant by learning from existing tactic scripts, offering suggestions or automating proof synthesis to enhance interactive and adaptive proof automation.
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously written tactic scripts and gives users either suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide users with a seamless, interactive, and intuitive experience together with robust and adaptive proof automation. In this paper, we give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management while learning in the large. Finally, we give a peek into Tactician's implementation as a Coq plugin and machine learning platform.