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
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
Qed. while displaying fully all
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
Qed., but display
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
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: Dec 07 2023 at 09:01 UTC