Coq中导入模块修改已有定义是否为预期行为？

复现代码与输出 #

执行的Coq代码 #

Search "prod_uncurry_subdef".
Require Import Arith.
Search "prod_uncurry_subdef".

输出结果 #

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

问题描述 #

导入无关模块会修改已有定义是否为预期设计？导入Arith模块后，le_pred、pred_Sn、f_equal_pred、max_l等约十个定义被修改。即便部分定义已废弃，该行为仍易引发困扰，可能导致添加导入操作后Coq文件失效。请问该行为是否为预期？若为预期，原因是什么？（使用版本：8.17.1）

解答 #

这种行为是预期设计，核心原因如下：

• Coq的全局命名空间是共享的，Require Import会将目标模块的全局标识符导入当前环境，若存在同名定义，后导入的版本会覆盖先存在的，这是Coq模块系统的固有特性。
• 你提到的被修改的定义大多是标记为废弃（deprecated）的旧实现，Arith模块作为基础算术库，引入了符合当前Coq库设计规范、逻辑更严谨的替代版本，以此推进库的演进。
• 这种设计兼顾了兼容性与迭代：旧代码可以继续依赖未导入新模块时的旧定义，而新代码通过导入Arith能使用优化后的版本；同时允许库维护者逐步淘汰有缺陷或不符合规范的旧定义。

规避建议 #

• 优先使用Require而非Require Import，仅引入模块而不导入全局命名空间，通过Arith.le_pred这类带模块前缀的方式访问定义。
• 对自定义代码使用局部命名空间或模块封装，减少全局命名冲突的概率。

内容的提问来源于stack exchange，提问作者Andreas Florath