I have been working with Coq for a few months now, mainly focusing on formal proofs in logic and set theory. I am interested in extending Coqs functionality for a specific project & want advice on how to approach this.
The goal of my project is to create a custom tactic for automating certain repetitive proof patterns that arise frequently in my work; I have been reading about Coqs Ltac language & the various tactics available but I am unsure about the best practices for defining my own tactic or modifying existing ones.
What are the key steps to start developing custom tactics in Coq?
Are there any examples or existing projects that provide a good starting point for learning how to extend Coqs proof automation capabilities??
What are the challenges or pitfalls I should be aware of when extending the tactic framework?
There is some guidance, indeed the problem of “good proof automation” is an area of research in itself, at the boundary between formal systems and software engineering.
But let me ask you a preliminary question, for clarification, since you have posted in “Developing the Coq system”, not in “Using Coq”:
Coq already ships with tactic languages with which to create custom tactics, as well as the tactic auto that supports the notion of programmable proof automation.
Are you sure that is not enough and that you are really asking about extending Coq, which typically means writing plugins to create (vernacular and commands and) tactics from scratch?
I suggest trying to work with Ltac or, probably better, Ltac2. Much harder: creating new tactics using Coq’s implementation language, OCaml, which would require learning Coq internals (for which there is little documentation).
Do you plan to make your new tactics available to others?
Usually you can put new OCaml tactics into plugins; they don’t have to be become part of the Coq repository, they can be in their own repository. Putting your additions into Coq will require review and approval from Coq maintainers.
Enhancing existing tactics generally means making changes in the Coq repository. Changing the existing behavior could break existing proofs. We try to avoid that.
Also, you’re more likely to get useful feedback if you describe in detail what you want your tactic(s) to do. There may be existing libraries that may be helpful, but no one will know to suggest them without knowing specifics.
