The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

TL;DR

Tactician is an interactive tactic learning and automation tool for Coq that learns from user scripts to suggest or automate tactics, enhancing proof development with seamless integration and adaptive automation.

Contribution

The paper introduces Tactician, a novel Coq plugin that combines tactic learning with user control, enabling seamless, interactive proof automation based on machine learning from existing scripts.

Findings

Provides tactic suggestions based on learned patterns

Allows users to delegate proof steps to automation

Addresses package dependency issues in large-scale learning

Abstract

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.