Patrick Nicodemus (Apr 12 2023 at 17:39): Patrick Nicodemus (Apr 12 2023 at 17:39):This page of the wiki has a section called "Some Useful Custom Tactics and Notation"
https://github.com/coq/coq/wiki/OtherContents
where a bunch of Ltac tactics (mostly/all written by Pierre Letouzey?) are showcased.
I think this is great and I would like to suggest that this be expanded to a page in the wiki dedicated to showing users how they can write good automation in Ltac. What I imagine is a kind of showcase where long time users who have experience writing sophisticated automation give links to their git repos or blog posts where they discuss tactics they have come up with which are themselves of more general use or illustrate general design principles. My impression is that the distribution of Ltac quality is mostly users doing pretty simple rote stuff, Adam Chlipala's book has a lot of good Ltac in it but from going through that book I mostly just learned how to write "repeat match goal with (dozen cases) end." I would like to see something beyond that.
Paolo Giarrusso (Apr 12 2023 at 19:38):I agree CPDT lacks design principles. A relevant paper is "How to make ad hoc proof automation less ad hoc", and "Interactive Proofs in Higher-Order
Concurrent Separation Logic" is probably a modern brain-child. Of note, the latter does not use canonical structures to encode proof search with backtracking, but simply typeclasses; nevertheless, the design goal is similar
Last updated: Oct 04 2023 at 22:01 UTC