[ssreflect] Use rw instead of rewrite to avoid conflicts with legacy tactic

[proux01]

Since this was the major cause of conflict with legacy tactics, ssreflect can now be loaded in the Prelude. For backward compatibility

From Corelib Require Import ssreflect.

still loads a rewrite wrapper to rw.

The theories/Corelib/ssr dir still contains:

• ssrfun.v and ssrbool.v that should go back in mathcomp (in a further PR)
• ssreflect.v with
  • the compat rewrite tactic as alias to rw (to be removed in a few releases)
  • the boolean if ... then ... else notations: in the long run we should maybe deprecate the specific if ... then ... else for inductives with two constructors (that is error prone, since it depends from the order of the constructors) with a quickfix toward the new if g is first_constructor then ... else variant and restrict if ... then ... else to booleans (or anything coercible to bool)

Depends on: #21609 , #21611

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

Most overlays are handling the new of and is keywords and are only a couple lines long.

• Adapt to https://github.com/rocq-prover/rocq/pull/21478 fblanqui/color#60
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 AbsInt/CompCert#570
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 thery/coqprime#93
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/coqutil#149
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat-crypto#2246
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat-crypto#2247
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat#127
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/kami#46
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 Mtac2/Mtac2#423
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 damien-pous/relation-algebra#53
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 stdlib#228
• https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/685
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 uwplse/verdi#149

[andres-erbsen]

Finally realizing the true extent of the change here, I am deeply skeptical of where this is going. Over years, ssreflect code has earned a reputation of being dense and essentially incomprehensible to outsiders and brittle outside the narrow niche of coding style used in mathcomp. While there are certainly valuable bits to be adopted from there, the way towards it would be targeted feature-by-feature design review with user-experience considerations under special focus.

Even adding a global 2-letter shorthand for ssreflect's rewrite seems premature given that unifall did not land, and I ran into serious issues within the first hour of trying ssr rewrite out in a relatively undemanding proof. I am still in favor of resolving the naming collision, but ssrewrite or something similarly evocative of the use case of the tactic would be more appropriate.

[andres-erbsen]

The referenced file defines a number of global notations, Ltacs, definitions, lemmas, and hints, not just ssreflect rewrite. We should not force these upon all corelib users without much more extensive review, even if we can get CI to pass with them.

[CohenCyril]

I guess the point here is to provide the ability to load at the same time ssreflect and libraries which did not load it, and in order to do that, at least the grammar from ssreflect must be taken into account in order not to create conflicts during a late Require. Indeed no one forces anyone to use ssreflect, actually quite on the contrary: the purpose here is to make ssreflect features available to all without paying the additional cost of forcing one to refactor their development to ssreflect 🤷

[CohenCyril]

Let me take a step back: I think indeed this is not a regular PR but a strategic one. Let's start with some facts.

• a decision was taken (in 2020?) to integrate the ssr tactic language in Rocq
• according to 2022 Rocq community survey 29% of respondents (out of 466) use ssreflect (whether one likes it or not)
• the integration to Rocq is not full because of the problem I mention: ssreflect may be "Require-incompatible" with some other libraries, because these libraries cannot be aware of stuff without requiring ssreflect as a starting point.
• (one of?) the largest corpus of mathematics in Rocq to this day is mathcomp-based and using ssreflect
• whatever happens, no one will be forced to use ssreflect's syntax.

Stuff that have been tried before and are not a good thing IMO.

• changing the syntax (or semantics) of ssreflect without porting the whole of mathcomp (and user dev in the CI) with it, because some oddities do actually have a justification and they may bite you very hard way later. (So one has to test them in places they do bite.)
• taking in ssreflect-like features but with a slightly different semantics (and syntax) in other tactics (e.g. intros [=stuff] %bla [x | y]) because it is so confusing (and does not bring more readability).
• ignoring the issue altogether, because it a source of frustration and inconsistencies.

In my opinion, we should integrate ssreflect as such to resolve compatibility issues right now, with minimal impact to users: I do not think here is the time and place to change its syntax or semantics as an answer to tastes and distastes of the participants to this discussion (this is a more general and valid question, but solves a distinct issue).

The fact that this PR does not pass CI and calls for overlay reflects the Require time conflicts, so that we can solve them here once and for all, for everyone wanting to mix mathcomp or other ssreflect based developments with almost anything.

[andres-erbsen]

I agree that the split of the ecosystem is not ideal and we ought to do something about it. I would be happy to discuss strategy if one was proposed.

I am not sure what you mean by Require-time conflicts -- are there any? I've been able to Require and wrap ssreflect in coqutil, for example, without needing the overlays here. The change I highlighted above adds controversial ssreflect constructs to by-default-Imported prelude. This does not seem necessary for fixing the compatibility issues, but is interesting as an experiment for investigating what the incompatibilities are -- or is that what you meant by "strategic PR"?

I would like to improve compatibility, but the path towards that must take into account desires and constraints of all users, mathcomp and otherwise. Obviously porting large swaths of code is costly, and shipping barely-tested constructs is not right. But I don't think we'd make any friends by forcing ssreflect as-is upon the supermajority of users who have not chosen it -- at the very least we should leave them the option whether to Import it or not.

At a higher level, my preferred path would be to

1. Resolve Require-time issues, if any. Much less invasively than this PR.
2. Factor out mechanisms from syntax, and make the (less controversial) mechanisms available through Require or qualified Import without the (more controversial) syntax.
3. Evaluate individual ssreflect features (either syntax or mechanisms). For each one, either document it and adopt it or stdlib (and so on) or change/remove it in mathcomp. (And ssreflect rewrite was actually first on my list in terms of interest, I just didn't have a good experience with it.)

[CohenCyril]

I globally agree with you @andres-erbsen.

By the way I think I got mistaken when I said Require-time, I was more thinking about my experience wanting to use ssreflect in a development that did not use it and being forced to refactor all the code to be ssreflect compliant. I think this is very bad because: 1. it imposes ssreflect on potentially large code base 2. it forces a refactor before anything can be done. That's why the priority for me is to make this integration, without making other users pay the price for a language they do not (yet 😉) use, but let them use some features when they like their behaviour.

As for ssreflect evaluation, I fully agree that it should be tested on non ssr contexts to see what might be missing and improved in a backward compatible way. I'm sorry to see your issues with ssr rewrite taking an awful amount of time (I usually have the exact opposite experience so I was surprised) and I am eager to know where this slowdown comes from.

However I do think ssreflect syntax should not be "evaluated" but that there should be a second one, less perl-ish available to all, and that ideally it should resemble current syntax e.g. elim: x => [|y z] in H1 H2 * could be written induction x as [|y z] generalizing H1 H2] (with => written as, and in ... * written generalizing ..., etc) but as
compositional as ssreflect is, because I think the key feature of ssr is not its syntax, but its compositional semantics and uniformity (everything on the stack (however you call it), not modifying hypotheses implicitly, allowing on the fly generalization as part of a general "tacticial pattern", as being general, generalizing too, and not attached to each tactic with a different implementation). The syntax just happens to be short to do be able to do "obvious stuff" quickly when you are an expert, and could be opt-in.

[CohenCyril]

PS:

at the very least we should leave them the option whether to Import it or not.

What I would like to reach is the point where Importing should be fully backward compatible for users (except the possibility to use ssreflect tactic if they want). And the price to pay for that is to change a small amount of things that are incompatible with current ssreflect, without being too much of a change (both for impacted library, and also for mathcomp if we need to change somehting).