Add `Proof using` directives

[JasonGross]

Done by setting '(coq-accept-proof-using-suggestion 'always) in emacs custom variables and evaluating to the end of the file in every file.

[samuelgruetter]

What's this good for? Is it to speed up parallel builds?

[JasonGross]

Proof using directives allow theorems in sections with section variables to be skipped over in async mode, which should speed up parallel builds. It also makes the proofs more robust to and easier to maintain in the face of, e.g., changes in lia that change which section variables get used. (This was the Qed errors rather than having a downstream use of the theorem complain that the arguments are wrong.) But my actual motivation for submitting this PR is that I set up my emacs/PG to insert them automatically so I could speed up parallel builds in the files in other projects where it matters more, and I'd rather not have my other PRs cluttered with Proof using changes, and it's a bit annoying to change them all back.

[samuelgruetter]

But my actual motivation for submitting this PR is that I set up my emacs/PG to insert them automatically

Haha thanks for being honest about your motivation :sweat_smile: So how about you add a .dir-locals.el to your coqutil clone that disables this setting?

[JasonGross]

So how about you add a .dir-locals.el to your coqutil clone that disables this setting?

I could do that, but given that Proof using improves both robustness and parallel build and makes it more obvious / self-documenting what variables are used by a given lemma, it seems to me like this PR is a win?

[andres-erbsen]

Reading through Word.Properties, most annotations look like they are just spelling out the concrete choices the default behavior would already make. Is that true or am I missing something here?

[JasonGross]

Yes, that's correct. All of these annotations are just spelling out the default behavior. They allow proofs to be processed in parallel in vio mode and CoqIDE, though, and are also for robustness when default behavior changes

[andres-erbsen]

Are you saying that the default behavior is to use the same hypotheses as listed but still not run the proofs in parallel? Edit: to put it differently, is there a mode where everything in section context is assumed to be used in every lemma unless we explicitly annotate otherwise? In that case parallelization would be limited but unambiguous.

[JasonGross]

Yes, that's correct. The proofs cannot be run in parallel because the variables that get used are not known until after the proof is run. And also, yes, there is such a mode, that mode is called Set Default Proof Using "All". There is also Set Default Proof Using "Type". https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Default-Proof-Using

[JasonGross]

Note that the All mode will change the arguments of the theorem even in serial mode (because serial mode and parallel mode must match), and Type mode will result in errors at Qed-time if you use some other section variable.

[andres-erbsen]

Would setting All mode by default in coqutil and manually annotating lemmas where this is not desired be a satisfying solution to everyone? I think it is a very common case and only annotating everything that doesn't do that would have much less clutter.

[JasonGross]

You could do that, and I have no objection (but please don't let the setting leak to dependencies of coqutil), but note that you'll get no help from Coq in that case (Coq won't let you know when you have unused variables, it'll just silently add them)

[andres-erbsen]

but please don't let the setting leak to dependencies of coqutil

Do you have suggestions for how to achieve that?

[JasonGross]

Do you have suggestions for how to achieve that?

Use the syntax for setting the option from the command-line / _CoqProject. You might have to add a coq-prog-args comment at the top of each file as well, if PG doesn't parse option-setting from _CoqProject

[andres-erbsen]