Stream: Coq devs & plugin devs

Topic: Keyword Define as synonym to Proof


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

view this post on Zulip Théo Zimmermann (Sep 29 2020 at 16:43):

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

view this post on Zulip Théo Zimmermann (Sep 29 2020 at 16:44):

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

view this post on Zulip Karl Palmskog (Sep 29 2020 at 17:54):

another possibility instead of Define might be the more neutral Body

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

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

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

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

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

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

view this post on Zulip Maxime Dénès (Sep 30 2020 at 12:16):

after all that's exactly where the content is relevant

view this post on Zulip Karl Palmskog (Sep 30 2020 at 12:37):

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

view this post on Zulip Karl Palmskog (Sep 30 2020 at 12:39):

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

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

view this post on Zulip 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: Oct 16 2021 at 01:03 UTC