feat: allow users to disable simpCtorEq simproc

[leodemoura]

simp only will not apply this simproc anymore. Users must now write simp only [reduceCtorEq]. See RFC #5046 for motivation.
This PR also renames simproc to reduceCtorEq.

close #5046

@semorrison A few simp only ... tactics will probably break in Mathlib. Fix: include reduceCtorEq.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5167 build failed against this PR. (2024-08-26 02:53:15) View Log
• 💥 Mathlib branch lean-pr-testing-5167 build failed against this PR. (2024-08-26 05:00:52) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b54a9ec9b986f4833278caf750ab06c6352fdf7c --onto 9305049f1ef7309842806c2a994a2020bb32a71f. (2024-08-26 13:54:37)

[leodemoura]

TODO: we must update-stage0 after merging this PR, and then remove staging workarounds.

[leodemoura]

Managed to build stage2 locally.

[leodemoura]

@semorrison I had to add a few workarounds to build stage2. I will cleanup after merging the PR, and updating stage0.

[nomeata]

About the naming of the simproc: judging from the code it only works for equalities between different constructors, but doesn't apply injectivity? The name could make users believe that it would.

Also do we have a consistent naming scheme for simprocs? reduceIte doesn't start with simp.

I think it's worth thinking about a good name for a moment here, as due to simp? this will be exposed to unsuspecting users, and if it looks too scarily internal (as simpCtorEq maybe does), it's not great for the early user experience.

Maybe to stick to existing jargon, why not noConfusion or noConstrConfusion? Or less jargony constrDontOverlap?

[nomeata]

And while we are at it: I would find it useful if, when reading code (either as a learner or as a reviewer) I could quickly grasp which simp arguments are plain theorems, and which are simprocs.

So a consistent naming convention for simprocs may be useful. I’d say it needn’t have simp, as it’s always about simp.

I was thinking about using a Proc suffix, e.g. noConfusionProc, iteProc, diteProc…

Most (all?) of the simprocs in core are called reduceFoo, so just sticking to that (reduceNoConfusion) is also an feasible option.

[leodemoura]

Also do we have a consistent naming scheme for simprocs? reduceIte doesn't start with simp.

Note that the simproc was renamed to reduceCtorEq.

[leodemoura]

I was thinking about using a Proc suffix, e.g. noConfusionProc, iteProc, diteProc…

I am not opposing this suggestion, but it should be a different PR if users see a benefit on this change. Remark: it will break many proofs in Mathlib.

[leodemoura]

About the naming of the simproc: judging from the code it only works for equalities between different constructors, but doesn't apply injectivity?

We use the injectivity theorems for that. We can add a docstring to make it clear the simproc only handles the different constructor case.