Stream: Coq devs & plugin devs

Topic: Keyword Define as synonym to Proof

Karl Palmskog (Sep 29 2020 at 13:14):

Something that I find reduces code readability, and hinders proper documentation generation, is that people often omit the Proof keyword whenever they define a non-Prop body with tactics (e.g., with refine). I believe one important reason for this is that people feel Proof should be reserved for actual proofs, and not "definitions".

One way to get around this would be to introduce a new keyword, say, Define, which acts as a synonym to Proof. Has this been thought of before, and is there any way it might be accepted as a Coq PR? Who would I have to persuade it's a good idea? I'm not super-attached to Define itself, but more to the general idea of a synonym.

Théo Zimmermann (Sep 29 2020 at 16:43):

I think everybody would be in favor of such an idea.

Théo Zimmermann (Sep 29 2020 at 16:44):

Incidentally, this seems like an important step toward making Proof and variants mandatory.

Karl Palmskog (Sep 29 2020 at 17:54):

another possibility instead of Define might be the more neutral Body

Gaëtan Gilbert (Sep 30 2020 at 08:00):

I believe one important reason for this is that people feel Proof should be reserved for actual proofs, and not "definitions".

is that really enough reason to add a synonym?

Théo Zimmermann (Sep 30 2020 at 10:06):

Coq has always been fond of command variants / synonyms. We even have singular and plural variants. So yes, it seems to me reason enough.

Maxime Dénès (Sep 30 2020 at 10:34):

Is this a good thing, though? For example, it is also what prevents us from turning structuring commands into keywords (since there are too many, it would be too invasive)

Théo Zimmermann (Sep 30 2020 at 10:51):

I do not have an opinion on this but it is a defining characteristic of the Coq language and not something that we would move away from without reinventing a completely new language.

Karl Palmskog (Sep 30 2020 at 11:14):

another benefit from a synonym: it could be treated differently than Proof by document generators. So for example, you might have an option to completely omit all Proof. ... Qed. while displaying fully all Body.... Defined.

This is in line with what we discussed in coq-community, where Theorem could be used to indicate that a lemma's underlying assumptions should be inspected by an external tool (so it doesn't use disallowed axioms, etc.), while Lemma is ignored by the tool.

Maxime Dénès (Sep 30 2020 at 12:16):

Wouldn't it make more sense to correlate it with opacity? I.e. omit Proof. ... Qed., but display Proof. ... Defined?

Maxime Dénès (Sep 30 2020 at 12:16):

after all that's exactly where the content is relevant

Karl Palmskog (Sep 30 2020 at 12:37):

there are quite a few developments where they make all proofs transparent these days.

Karl Palmskog (Sep 30 2020 at 12:39):

also, documentation generators would not need lookahead with Proof/Body as indicators

Karl Palmskog (Sep 30 2020 at 12:43):

anyway, since this didn't get shot down hard here (which is somehow contrary to what I expected), I will probably go ahead and submit a PR, and we can do all the bikeshedding stuff there

Théo Zimmermann (Sep 30 2020 at 13:23):

Remember that coq/ceps#42 now includes a proposal to eventually make Qed not represent opacity but only the fact that a proof is terminated (following a suggestion of @Enrico Tassi).

Last updated: Jun 09 2023 at 07:01 UTC