Nevertheless, I'll try summarise this thread for my own future reference. Three (possibly complementary) approaches to solve the problem:
Search
whenever you're stuck.
Compatible with any naming scheme (e.g. ad hoc, semi-consistent, robust naming scheme).
Simply avoid depending on the theorem names!
This will solve the entire class of problem. Methods: (a) Integrating each lemma in powerful tactic (proof automation?). (b) Fold lemmas into canonical structures/typeclass instances.
Jiahong Lee has marked this topic as resolved.
Pierre Courtieu said:
Another solution is Chlipala’s style: each lemma is integrated in powerful tactics and you never have to type the name of that lemma again. I personally am not able to comply with such strong discipline but it almost nullifies the problem of naming theorems.
IMHO one has to distinguish between routine work and proving more fundamental lemmas for preparing the ground for routine work. Routine work can and should be automated as much as possible. For fundamental lemmas were one does not regularly prove similar lemmas, it doesn't make much sense to spend much time on automation - what can be achieved there is anyway quite limited. Of course one should have a look at maintainability of fundamental proofs as well, but this does not necessarily mean automation.
Last updated: Feb 06 2023 at 13:03 UTC