Stream: Coq users

Topic: ✔ (Newbie) Tips for Systematic Organisation of Theorems


view this post on Zulip Jiahong Lee (Jul 10 2022 at 14:33):

Hi, I've progressed through Software Foundation Vol 0 and half-way through Vol 1.

Problems:

  1. I've hard time looking up previously proven theorem. Most of them are trivial to people, but needed for proceeding mechanical proofs. Looking them up are a chore. While I can use the Search command, if I couldn't remember the theorem name, I'll need to Search for it everytime I want to use the theorem.
  2. Sometimes, I've proven the same theorems twice, under two different names. I think this is bad, cause it's a waste of effort.

Do you face the same problems? How do you solve/workaround them?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jiahong Lee (Jul 11 2022 at 00:59):

@Gaëtan Gilbert Thanks, good to know how theorems are organised in other projects

view this post on Zulip 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.."

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Jul 11 2022 at 11:15):

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.

view this post on Zulip Jiahong Lee (Jul 11 2022 at 13:30):

@Ana de Almeida Borges I see, thanks!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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:

  1. Robust naming scheme.
  2. Search whenever you're stuck.
    Compatible with any naming scheme (e.g. ad hoc, semi-consistent, robust naming scheme).

  3. 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.

view this post on Zulip Notification Bot (Jul 14 2022 at 02:06):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip 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: Jun 17 2024 at 22:01 UTC