[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 could now be loaded in the Prelude (in a further PR, c.f. #21776 ). 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 of T & ... & T notation for anonymous binders (c.f., Add "& T" syntax for anonymous binder "(_ : T)" and "of _ & _ & _" syntax for constructors #21611 ) (merged)
  • the if <term> is <pattern> then <term> else <term> and if <term> isn't <pattern> then <term> else <term> notations (c.f., Add "if <term> is <pattern> then _ else _" syntax #21609 )
  • 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)

• Added / updated test-suite.

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

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

[proux01]

To be discussed in a future Call: https://github.com/rocq-prover/rocq/wiki/Rocq-Call-2026-03-17

[SkySkimmer]

not convinced we should be adding this stuff to the prelude
also even if we decide we should, it doesn't match the PR title "[ssreflect] use rw instead of rewrite"

[SkySkimmer]

why?

[proux01]

Ssreflect was using _foo_ for reserved identifiers (the ones introduced by move=> ?) which forbids explicitly using any such identifier. To avoid conflicts this changes it to ‗foo‗.

[SkySkimmer]

???

[proux01]

case E: foo is valid ssreflect syntax (c.f., https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html#generation-of-equations ), the parenthesis fixes the conflict.

[proux01]

Following last Rocq call, this is now split in two:

• ssreflect related changes remain here
• addition of ssreflect to prelude is moved to Add ssreflect to the prelude #21776

@gares CI green this now seems in a mergeable state

[gares]

I think that the PR now only contains what was discussed at the rocq-call, @SkySkimmer @andres-erbsen please amend your requests for changes.

I'm a little worried about the warning. I don't think it is urgent, since the use case this PR makes possible is to load SSR/MC inside non SSR/MC context. You don't really care if the the MC code uses rewrite instead of rw. The warning is there, correct me if I'm wrong, to push MC users to port their scripts. IMO this can wait. Also, the warning should really come with a quickfix, so that the porting can be done automatically.

[proux01]

It's the common policy here to emit deprecation warning as soon as the replacement is available, since warnings can easily be silenced. No strong opinion but it would be strange to make an exception here.
I'll add the quickfix.

[SkySkimmer]

remove the test suite makefile change

I'm also not very convinced about allowing DOUBLE LOW LINE in idents

[proux01]

The warning is there, correct me if I'm wrong, to push MC users to port their scripts.

More generally, all ssreflect users.

IMO this can wait.

No strong opinion, but we usually introduce warnings with the replacement to let user know, they can then silence it until they can handle it. Doing it later means we have to remember introducing it latter, users may discover the change it later (probably not an issue here), the difference between the versions the replacement was introduced and the version the deprecation warning was introduced may make it harder to track/handle for users (particularly if this one differs whereas others usually don't).

Also, the warning should really come with a quickfix, so that the porting can be done automatically.

done

remove the test suite makefile change

@SkySkimmer done

[proux01]

I'm also not very convinced about allowing DOUBLE LOW LINE in idents

Note that this is for ssreflect reserved identifiers (typically the ones introduced by move=> ?), users are not allowed to manually input such identifiers.

[proux01]

@gares CI green

[gares]

@andres-erbsen please check the updated PR. If I hear nothing I'll merge tomorrow.

[gares]

@coqbot merge now