导入不仅导入还更改现有定义吗？

Question

使用以下 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 文件的部分内容无效。

这是故意的吗？如果是这样为什么？原因是什么？

Answer 1

加载新开发可能会破坏现有开发（未使用新导入的模块），这是

Require Import

的一个功能。这在证明搜索中已经很明显，但在这种情况下，受影响的是现有常量的隐式参数声明。

在修改现有常量的隐式参数声明的情况下，应该避免这种情况，Coq 的开发人员在旧版本的 Coq 中犯了这个错误。似乎

Arith

加载了

Program

，其中包含更改

prod_uncurry_subdef

隐式参数的命令。当时这似乎是一个小麻烦，因为从 [] 类型到 {} 类型隐式参数的更改不会破坏许多开发，并且用户不应该使用

_subdef

对象，而只能使用

curry

或

uncurry

物体。

但是这个问题在新版本的 Coq (8.19) 中得到了纠正，因为常量

prod_uncurry_subdef

不再存在。

在系统设计中进行了反思，以避免将来出现这种麻烦，特别是让每个库都存在于自己的命名空间中。