如何在Coq中重载"+"符号？解决重载定义报错问题

报错原因分析 #

1. 第一个报错：原有+符号的参数优先级是左操作数level 50，右操作数next level，你第一次定义Notation时，左操作数x未指定level，默认是next level，和原有符号的参数优先级不匹配，导致冲突。
2. 第二个报错：Coq的语法规则规定，中缀符号的左操作数优先级必须和符号本身的level一致（用于处理左递归表达式），因此你不能手动修改已有符号左操作数的level，否则会触发The level of the leftmost non-terminal cannot be changed错误。

正确的重载方式 #

如果你想把自定义的my_add关联到已有的+符号，直接用Global Existing Infix命令即可，无需重新声明Notation的优先级：

Definition my_add (n m : nat) := n + m.

Global Existing Infix "+" (my_add).

如果是为新类型定义+符号，需要先保留符号再绑定：

(* 先保留符号，指定优先级和结合性 *)
Reserved Notation "x + y" (at level 50, left associativity).

(* 自定义新类型的加法函数 *)
Definition my_add (a b : your_new_type) : your_new_type := ...

(* 绑定符号到函数 *)
Infix "+" := my_add (at level 50, left associativity).

关于旧版本成功的可能原因 #

旧版Coq对符号优先级的检查规则更宽松，允许部分不匹配的情况；或者你之前是为全新类型定义+，而非重载nat类型已有的+符号，因此没有触发优先级冲突。

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