nsatz no longer unfolds TwoF

[Boutry]

Description of the problem

I recently had to change our script to get our library to compile with Coq 8.19.0.

Small Coq file to reproduce the bug

Require Import Nsatz.

Require Import Rbase.

Definition TwoF : R := 1 + 1.

Goal forall x y:R,  x = y -> (x+1+1)%R = (y+TwoF)%R.
nsatz.
Qed.

Version of Coq where this bug occurs

8.19.0

Last version of Coq where the bug did not occur

8.18.0

[Boutry]

Thank you @thery for spotting the problem :)

[andres-erbsen]

I'd guess it's #18325 -- previously nsatz interpreted goals using typeclass search, which I believe would have unfolded TwoF.

IMO the nsatz change itself here is likely desirable as it makes it easier to predict whether nsatz will solve a goal and makes nsatz less slow on pathological cases, but breaking scripts that relied on the heuristic unfolding is unfortunately direct consequence. Currently, the main way we offer for handling changes of this kind is to participate in the Coq CI. There have been a number discussions about how strict and conservative we should be about avoiding coq changes that require backwards-compatible changes to downstream code, and input is welcome in that regard.

[Boutry]

So is 2 a notation instead of a definition then? I am asking as the following does not present the problem.

Goal forall x y:R,  x = y -> (x+1+1)%R = (y+2)%R.
nsatz.
Qed.

[andres-erbsen]

Yes, 2 is a Number Notation for IZR as defined in theories/Reals/Rdefinitions.v, and nsatz understands IZR. Set Printing All is helpful for figuring out these differences.

[thery]

maybe something should be added in the change log if it is not already done explaining this issue and the possible change of behavior of nsatz