Tactician is a tactic learner and prover for the Coq Proof Assistant. The system will help users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician will learn from previously written tactic scripts, and either gives the user suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician’s goal is to provide the user with a seamless, interactive, and intuitive experience together with strong, adaptive proof automation.
Yes, the system has first-class support for Opam, Coq’s package manager. When
you install dependencies, Tactician can automatically instrument those
developments and learn from them. When you work on your project, Tactician
will have background knowledge on all modules you
On the flip side, using Tactician in your project does not mean you now have a hard
dependency on Tactician. When the system finds a proof, it presents you with
a caching witness that you can copy into your source file. As long as this witness
remains valid, you can compile your project without having the main Tactician code-base
installed. You only need 10 lines of helper tactics, which you can install
coq-tactician-dummy package, or simply copy them into your development.
We have not yet performed a large-scale test on students, but we believe that the system may indeed be used in this capacity. Installation is straightforward and the system functions on Linux, macOS and Windows. The automation is push-button style without needing any configuration, and when a proof cannot be found, Tactician can still suggest tactics that may be useful.
Yes! Tactician is an extensible platform that can incorporate multiple machine learning models and search procedures. If you want to contribute your ideas, you can either work on the Tactician code-base directly, or you can create a plugin for Tactician in a separate repository. We are always searching for people that want to develop new ideas, either independently or in collaboration with us. If you’d like more information, please reach out to us!