Remove uses of "Proof with" from library

[jfehrle]

NEW DESCRIPTION:
Remove uses of "Proof with" from the library because it's not a great feature (see #12059) and I think not a best practice. The library should try to follow best practices since users may emulate thing they see in there.

ORIGINAL:
Experiment with removing "Proof with" and see what breaks

[Zimmi48]

It's amazing how much it breaks! Even Software Foundations, wow!

[jfehrle]

Funny, I was pleased that about half the libraries and plugins still compiled.

You think it's worth committing the .v changes now?

[Zimmi48]

Well, it's pretty rare that we commit changes with this level of breakage. This would have to be discussed with the users of the feature, but given that it is not a super problematic feature, I wouldn't push for this too hard.

Regarding the clean-up of the standard library, yes it would be interesting to commit this but it would be better to clean the diff as much as possible, i.e., remove the trailing tactics every time they do nothing.

[jfehrle]

yes it would be interesting to commit this but it would be better to clean the diff as much as possible, i.e., remove the trailing tactics every time they do nothing.

I already did that for the 2 files in theories/Reals where it looked like it was overused. In the other files it was used far less and didn't look overused. Verifying whether each one is necessary is too tedious, not something I plan to do.

[jfehrle]

We could add language to the doc for "Print with" recommending the use of alternative constructs. Could be in this PR or elsewhere.

[anton-trunov]

If we stick to changing only Qeded proofs it should not break things, right?

[jfehrle]

If we stick to changing only Qeded proofs it should not break things, right?

@Zimmi48's comments about breakage refer to an initial experiment in which I made Proof with unavailable. All the jobs in GitLab are green now.

[anton-trunov]

Thanks. I just remember several years ago Software Foundation had a bunch of Proof with, so I naturally thought CI was not green because of Defined.

[ejgallego]

Thanks. I just remember several years ago Software Foundation had a bunch of Proof with, so I naturally thought CI was not green because of Defined.

Indeed the use of Proof with in SF explains why is so pervasive among other developments.

[Zimmi48]

Verifying whether each one is necessary is too tedious, not something I plan to do.

Yeah, I was wondering if some automated strategy (based on proof diffs) could help here, but I have nothing concrete to propose.

[Zimmi48]

We could add language to the doc for "Print with" recommending the use of alternative constructs. Could be in this PR or elsewhere.

Before discouraging the use of the feature, we should ask the opinion of @bcpierce00. It makes little sense to discourage a feature in the reference manual, if in the same time it is presented in the most read tutorial about Coq.

But we can already remove it from the standard library if we want.

[Zimmi48]

Since I'm still reluctant to introduce a change that puts a lot of ; foo in the code even though most of them might be useless, I thought of a new idea. What about introducing a new warning (off by default) that a user can use to detect useless ..., i.e., Coq would warn if the goal after applying the "Proof with tactic" is in the same state as before. Users could activate this warning and a script could use them to remove all useless ..., then the script could further transform the remaining ... into ; foo.

[bcpierce00]

I like this last option a lot. I'd be happy to get rid of all these Proof...with...'s, but would like not to make the proofs a lot uglier in the process.

[ejgallego]

I think that in general the idea of ... is a useful one and built-in in other development styles, for example ssr's // which is rebindable and was recently extended.

I have indeed trouble agreeing on the original premise of this PR which qualifies ... as not a great feature and not best practice, as in practice alternatives such as // are essential for some proof styles, and also implemented in advanced ltac setups such as the ones by MIT.

[Zimmi48]

I think that in general the idea of ... is a useful one and built-in in other development styles, for example ssr's // which is rebindable and was recently extended.

I have indeed trouble agreeing on the original premise of this PR which qualifies ... as not a great feature and not best practice, as in practice alternatives such as // are essential for some proof styles, and also implemented in advanced ltac setups such as the ones by MIT.

There's a major difference between // and ... which is that the former does not require built in support in Proof and, more importantly, in terminators.

It would be pretty reasonable to replace this feature with a //. that is locally defined.

[jfehrle]

IIUC // doesn't do anything that can't be done by replacing Proof with <tactic> with Proof. Ltac f := <tactic>. and ... with . f. f is certainly rebindable. Setting aside SSR, we don't use punctuation by itself to represent tactics--those are named with identifiers. It makes sense to clean up some of the odder features of Coq syntax that duplicate the functionality of other, more consistent features--there's no loss of functionality, it's easier to document, fewer constructs to learn and perhaps enables other code cleanup.

@Zimmi48

What about introducing a new warning (off by default) that a user can use to detect useless ..., i.e., Coq would warn if the goal after applying the "Proof with tactic" is in the same state as before. Users could activate this warning and a script could use them to remove all useless ..., then the script could further transform the remaining ... into ; foo.

Something along these lines would make it painless for users to update their proofs, though instead of printing a warning, coqc could just remember where the ... should be removed. After compilation is complete, that info could be used to update the file, the code for which could be entirely OCaml or a python script started by coqc.

[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.

[Zimmi48]

I suggest closing this PR until a tool is made available that would help replace ... by ; tac only where it is useful (based on a warning or something else).

[coqbot-app]

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

[coqbot-app]

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