Hello,
I am glad to announce the first release of Trakt, a generic goal preprocessing tool for proof automation tactics in Coq.
Automation tactics in Coq are usually tailored for specific subsets of goals. Yet, when designing their proof statements, Coq users can choose from a range of different inductive types with advantages and drawbacks (computational efficiency, ease of proof, etc). This variability can lead to a situation where the tactic the user would like to use to prove a goal cannot understand this goal, because the types at use are not recognised by this tactic. However, if the goal falls into the scope of this tactic, the goal can be proven equivalent to a converged one (i.e. expressing values in the types that are said to be recognised in the input specification of the tactic). This also applies to logic, as some tactics may prefer an input in
Propand others inbool. Trakt is a plugin made to solve this problem by automatically preprocessing goals into their converged version, before the user hands them to an automation tactic.
Please head to the home page or the GitHub repository for further information. The tool is written in Coq-Elpi and has been tested with Coq 8.13. It can be installed through opam pin. Keep in mind that this is a research project that can be subject to bug fixes and still has a lot of room for improvement.
Special thanks to my supervisors, Assia Mahboubi and Denis Cousineau, for their guidance since the birth of the project, Enrico Tassi for his precious help about Coq-Elpi during the development, and the SMTCoq team for testing the tool and bringing its first use case.
If you have any question about the tool, feel free to contact me on the Zulip server or by e-mail.
Best regards,
Enzo Crance