Using the following Coq code:
Search "prod_uncurry_subdef".
Require Import Arith.
Search "prod_uncurry_subdef".
prints out the following:
prod_uncurry_subdef: forall [A B C : Type], (A * B -> C) -> A -> B -> C
prod_uncurry_subdef: forall {A B C : Type}, (A * B -> C) -> A -> B -> C
Is this by intention that an (unrelated) import changes already existing definitions?
The Arith import changes about ten definitions, like:
le_pred, pred_Sn, f_equal_pred, max_l, ...
Even if some of them are deprecated I find this behaviour irritating. This means that adding an import might invalidate parts of a Coq file.
Is this by intention? If so why? What is the reason?
[For the files: I'm using version 8.17.1.]
It is a feature of Require Import that loading a new development may break an existing development (that was not using the newly imported module). This is already apparent in proof search, but in this case what is affected is the declaration of implicit arguments for existing constants.
In the case of modifying the declaration of implicit arguments for existing constants, this should be avoided, and the developers of Coq made this mistake in older version of Coq. It seems Arith loads Program which, contains a command to change the implicit arguments of prod_uncurry_subdef. It probably seemed a minor nuisance at the time, because a change from []-kind to {}-kind of implicit argument will not break many developments, and users are not suppose to use the _subdef objects, only the curry or uncurry objects.
But the problem is corrected in the new version of Coq (8.19), because the constant prod_uncurry_subdef no longer exists.
There are reflections in the design of the system to avoid this kind of nuisance in the future, in particular by making each library live in its own naming space.