Regression: Importing ZArith leads to setoid_rewrite performance degradation

[Janno]

In the following proof, setoid_rewrite works fine on older versions of the stdlib (sometime between 8.20 and 9.0, I think) but it takes over 30 seconds on more recent versions of the standard library. I don't think the rocq version matters but I have tested with master and a snapshot of master from late February.

From Corelib Require Import PrimInt63 Uint63Axioms.
Require Import Corelib.Strings.PrimString.
Require Import Corelib.BinNums.IntDef.
Require Import Corelib.Numbers.BinNums.
From Corelib Require Import Setoid.
From Stdlib Require Import ZArith.

Axiom N_to_nat : N -> nat.
Axiom N_modulo : N -> N -> N.
Axiom N_mod_0_r : forall x, N_modulo x N0 = N0.

Goal forall x,
  Init.Nat.min 
    (IntDef.Z.to_nat (to_Z PrimString.max_length))
    (N_to_nat (N_modulo x N0))
  = 0%nat.
Proof.
  Timeout 1 setoid_rewrite N_mod_0_r.
Abort.

AFAICT the change is related to Znumtheory pulling in libraries like Ncring but I am not 100% sure. A similar slowdown can be seen when importing just Ncring instead of ZArith in the example above. In that case, the slowdown can be fixed by disabling these typeclass instances:

Remove Hints  ring_setoid : typeclass_instances.
Remove Hints  ring_plus_comp : typeclass_instances.
Remove Hints  ring_mult_comp : typeclass_instances.
Remove Hints  ring_sub_comp : typeclass_instances.

But this does not suffice to fix the slowdown when importing all of ZArith.

[Janno]

Bisecting isn't exactly easy with the core/stdlib split and also the 8 -> 9 version bump and all that. I am not 100% sure that this is the commit responsible but it's the closest I will get:

8fbb9f33f4490f09e83280f8bce019b243ab3704 is the first bad commit
commit 8fbb9f33f4490f09e83280f8bce019b243ab3704
Author: Andres Erbsen <andres@andres.systems>
Date:   Sat May 10 07:44:20 2025 -0400

    add a compat require :/

 theories/ZArith/ZArith.v | 3 +++
 1 file changed, 3 insertions(+)

/cc @andres-erbsen

[andres-erbsen]

Ack. If this commit is really the issue, we should be able to get rid of it by sprinkling Require statements throughout Rocq CI. I did not consider TC performance when adding that Require.