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.
I think everybody would be in favor of such an idea.
Incidentally, this seems like an important step toward making Proof
and variants mandatory.
another possibility instead of Define
might be the more neutral Body
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?
Coq has always been fond of command variants / synonyms. We even have singular and plural variants. So yes, it seems to me reason enough.
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)
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.
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.
Wouldn't it make more sense to correlate it with opacity? I.e. omit Proof.
... Qed.
, but display Proof.
... Defined
?
after all that's exactly where the content is relevant
there are quite a few developments where they make all proofs transparent these days.
also, documentation generators would not need lookahead with Proof
/Body
as indicators
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
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