Stream: Coq users

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

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: Feb 06 2023 at 13:03 UTC