Hi, I've progressed through Software Foundation Vol 0 and half-way through Vol 1.
Problems:
Search
command, if I couldn't remember the theorem name, I'll need to Search
for it everytime I want to use the theorem. Do you face the same problems? How do you solve/workaround them?
The method I have in mind is to come up with a mnemonic (or systematic naming scheme) for theorems.
The goal is to give unique name to simple theorems, and similar names to complex theorems. So that the same theorem wouldn't be proven twice. I assume that there exists a unique name for every simple theorem/goal, e.g. 0 <= n
, n <= S n
, ~ (S n <= n)
, n <= m -> S n <= S m
). As for complex theorems, perhaps similar names are enough to help discovery of duplicate efforts.
Thus, I'm asking for comments before coming up with my own system
https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#naming-conventions-for-lemmas-non-exhaustive
other projects will have their own naming styles, with varying degrees of strictness
I like mathcomp's system (linked by Gaëtan), although it has a bit of a learning curve. But I wonder: do you feel like each use of Search
is annoying, or that overall you need to use Search
a lot even though each individual use is easy/fast? If the former, it's possible that learning some more Search
features might be helpful. If the latter, some IDEs include shortcuts for searching, without needing to actually type "Search
" in the middle of your file, which might make it a bit better.
Regardless, Search
itself is not perfect and the situation could definitely be improved. I think there is a group of people looking into it.
@Gaëtan Gilbert Thanks, good to know how theorems are organised in other projects
@Ana de Almeida Borges I'm annoyed by the need to use Search
in the middle of proof. It's quite disruptive to my mental flow. Right now, it's like "Oh, I know there is a theorem to resolve this goal. What is its name already? Hmmm, nvm, let's Search
for it".
Instead, I want to reach the state "Oh, I know there is a theorem to resolve this goal. What is its name already? Hmm, from its goal and hypothesis H1, I guess it's called A_if_B
. Bingo! Let's proceed.."
Search
is indeed a very powerful tool. I like it and I'm not intended to replace it either. I believe I only barely scratch the surface of its functionality. But what I have in mind is something orthogonal(?) or complementary to it?
@Ana de Almeida Borges Who is looking into improving the situation? I'm interested both in seeing what they have and help if I like it...
@Julien Puydt, see this thread: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Towards.20a.20CEP.20for.20improving.20Search
Jiahong Lee said:
Search
is indeed a very powerful tool. I like it and I'm not intended to replace it either. I believe I only barely scratch the surface of its functionality. But what I have in mind is something orthogonal(?) or complementary to it?
I see. In that case I think coming up with a robust naming scheme is your best bet.
@Ana de Almeida Borges I see, thanks!
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.
That raises the question of composing those tactics, but sometimes the lemmas can be turned into canonical structures ("how to make proof automation less ad-hoc") or typeclass instances (same basic idea as in the previous paper's introduction; this strategy is used e.g. in iris, but also many other places)
Thanks! Good to know that, but it's way too advance for me to understand right now.
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: Jun 17 2024 at 22:01 UTC