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

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 thery/coqprime#93 (edit 8 lines, renaming some tactic rw -> rew)
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/coqutil#149 (edit 2 lines, adding parentheses)
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat#127 (edit 4 lines, adding parentheses)
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/kami#46 (edit 1 line, adding parentheses)
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 damien-pous/relation-algebra#53 (edit 5 lines, adding parentheses)
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 stdlib#228 (edit 1 line, adding a space // -> / /)

[andres-erbsen]

Based on the overlays, this change is doing more than renaming ssreflect rewrite, and seems more like a language change. What is the goal here?

[proux01]

Being able to use ssreflect without conflicts. The major source of conflict was the rewrite tactic, which is handled by renaming the ssreflect one to rw. Overlays are just handling minor other conflicts (they are mostly editing a couple lines), as detailed in the changelog entries.

[thomas-lamiaux]

While, on the long run, I strongly believe tactics should be indexed through Ltac2, it is far away, and in the meantime it would be indeed great if ssreflect could be loaded by default.

A few questions after a quick review of the code and docs:

• This PR is not only doing the name change, not actually importing it by default, right ?
• What about the if that differs between both languages ? (I don't get the solution from the intro message)
• Perennial is remove from the CI in this PR ? should it be done in a seperate PR ?

[SkySkimmer]

This PR seems to be doing multiple separate things (as indicated by having 3 changelogs) and should probably be split.
also whatever made the stdlib overlay needed is not described in the changelog and doesn't even seem to be desired, the overlay should be reverted and the change fixed.

[proux01]

* This PR is not only doing the name change, not actually importing it by default, right ?

Not sure I understand the question(s)?

* What about the `if` that differs between both languages ? (I don't get the solution from the intro message)

C.f. the related changelog entry and top message comment about what could be done in the future. So currently, this is only adding the if ... is ... then ... else ... syntax whereas the if <guard> then ... else ... forcing <guard> : bool remains in the compat layer.

* Perennial is remove from the CI in this PR ? should it be done in a seperate PR ?

According to #21425 (comment) it should be done "the next time it breaks", so either in the current PR or any other that get merged before it.

This PR seems to be doing multiple separate things (as indicated by having 3 changelogs) and should probably be split.

It could relatively easily be split in three nonindependent PRs (one per changelog entry), but not sure it's worth it (no strong opinion, I'd rather let the assignee decide).

also whatever made the stdlib overlay needed is not described in the changelog and doesn't even seem to be desired, the overlay should be reverted and the change fixed.

In some earlier development stage of the current PR, I considered forbidding the use of *) outside comments (which seems a relatively reasonable thing to expect). This is no longer needed in the current state of the PR (hence the absence of changelog/refman change about that), but I didn't revert that change in the overlays.

[andres-erbsen]

Please do remove the unneeded changes from overlays (or at least a few representative ones) so that we can have illustrative examples of what the actually necessary downstream changes are.

I don't have opinions on what ssreflect rewrite is called, but making is a keyword(?) sure seems undesirable on top of the already several short-word keywords rocq has. Why is that notation bundled with using ssreflect tactics?

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

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