Jiahong Lee (Jul 10 2022 at 14:33): Jiahong Lee (Jul 10 2022 at 14:33):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?
Jiahong Lee (Jul 10 2022 at 14:39):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
Gaëtan Gilbert (Jul 10 2022 at 14:44):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
Ana de Almeida Borges (Jul 10 2022 at 15:43):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.
Ana de Almeida Borges (Jul 10 2022 at 15:47):Regardless, Search itself is not perfect and the situation could definitely be improved. I think there is a group of people looking into it.
Jiahong Lee (Jul 11 2022 at 00:59):@Gaëtan Gilbert Thanks, good to know how theorems are organised in other projects
Jiahong Lee (Jul 11 2022 at 01:10):@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.."
Jiahong Lee (Jul 11 2022 at 01:12):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?
Julien Puydt (Jul 11 2022 at 06:03):@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...
Ana de Almeida Borges (Jul 11 2022 at 11:12):@Julien Puydt, see this thread: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Towards.20a.20CEP.20for.20improving.20Search
Ana de Almeida Borges (Jul 11 2022 at 11:15):Jiahong Lee said:
Searchis 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.
Jiahong Lee (Jul 11 2022 at 13:30):@Ana de Almeida Borges I see, thanks!
Pierre Courtieu (Jul 13 2022 at 15:32):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.
Paolo Giarrusso (Jul 13 2022 at 16:41):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)
Jiahong Lee (Jul 14 2022 at 01:52):Thanks! Good to know that, but it's way too advance for me to understand right now.
Jiahong Lee (Jul 14 2022 at 02:05):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.
Notification Bot (Jul 14 2022 at 02:06):Jiahong Lee has marked this topic as resolved.
Michael Soegtrop (Jul 14 2022 at 07:36):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: Oct 13 2024 at 01:02 UTC