Adding "Body", synonymous of "Proof", for interactively-defined definitions

[herbelin]

See discussion at rocq-prover/rfcs#42.

We introduce Body as a synonymous of Proof to delimit the beginning of a definition by tactics. When used in the form Body c, it indicates an Opaque declaration (independently of the question of whether the forms Proof c and Body c, that add little, are worth to be kept). This is useful in particular for UIs that rely on Proof .. Qed-like blocks for highlighting, while Proof sounds odd for a Definition.

• Added changelog.
• Added / updated documentation.
• Inform UIs about the alternative

If wanted, this may help to introduce a warning on proofs not started with Proof.

[ejgallego]

IMHO I'd instead remove the VernacExactProof construction at all.

[herbelin]

IMHO I'd instead remove the VernacExactProof construction at all.

That's a different question than what the PR is doing. The motivation of the PR is to support scripts of the form:

Definition f (n:nat) : nat.
Body.
blabla.
Defined.

so that we don't have to write neither the non-bracketed:

Definition f (n:nat) : nat.
blabla.
Defined.

nor the misleading:

Definition f (n:nat) : nat.
Proof.
blabla.
Defined.

If the PR introduces Body t it is because there is already Proof t. Would Proof t be removed, then the PR would not have to add Body t.

Would you like me to make a PR deprecating Proof t?

[ejgallego]

@herbelin based on your examples I'm not sure the PR is doing what you want?

(Do examples compile at all?)

I think you've modified the Proof term command

[SkySkimmer]

I'm not convinced that we want more aliases.

Also CI indicates that the Show Proof change is broken.

[herbelin]

I'm not convinced that we want more aliases.

Would you rather go in the direction of removing Defined and have only Proof/Qed brackets for tactic scripts?

[herbelin]

Excerpts from rocq-prover/rfcs#42:

"The motivation for the second part of the CEP (separating the transparency status from the Defined / Qed commands) is that Defined is naturally associated with the notion of definition and Qed with the notion of proof. The use case that it has taken (defined theorems to mean non-opaque ones) was not anticipated and now we would have other ways of specifying it (the attribute). Furthermore, having the transparency status of an object always be determined at declaration time would remove an inconsistency between the case where a body is provided and the case where the body is built in interactive proof mode."

"The end goal is that the transparency status is only determined by the attributes and that Qed and Defined become synonyms of each other (Qed being encouraged in combination with Theorem and Defined being encouraged in combination with Definition)."

[proux01]

Doesn't seem ready for 8.20, removing the milestone.

[herbelin]

This is a design question somehow related to the rocq-prover/rfcs#42. No urgency.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.