Coq中导入含重复符号的外部模块冲突问题及解决咨询

这种符号冲突的问题在Coq里确实挺常见的，尤其是依赖外部库又不想修改源码的时候，我给你整理了几个可行的解决办法：

• 选择性导入，排除冲突符号
  Coq支持在导入模块时排除特定的符号/记号，这样既能用到模块里的其他内容，又能避开冲突的部分。比如假设冲突的记号是_ ~ _，两个模块分别是ModA和ModB，你可以这样写：

  (* 先完整导入第一个模块 *)
  Import ModA.
  (* 导入第二个模块，但排除冲突的记号 *)
  Import ModB.(- Notation "_ ~ _").
  

  这样ModB里除了_ ~ _之外的其他符号都能正常使用，不会和ModA的记号冲突。

• 重命名冲突记号，区分使用
  如果两个模块的_ ~ _你都需要用到，可以给其中一个重新绑定一个新的记号。比如先导入其中一个模块，然后把另一个模块的冲突记号映射成新的语法：

  Import ModA.
  (* 把ModB的_ ~ _重命名为x ≈ y，指定层级和关联性 *)
  Notation "x ≈ y" := ModB.(_ ~ _) (at level 50, left associativity).
  

  之后你用a ~ b就是调用ModA的记号，用a ≈ b就是调用ModB的记号，完美区分。

• 使用模块限定名直接访问
  不直接导入模块，每次使用符号时加上模块的限定名，这样明确指定符号的来源，从根源上避免冲突。比如：

  (* 不导入任何模块，或者只导入无冲突的部分 *)
  Check ModA.(a ~ b). (* 使用ModA的_ ~ _ *)
  Check ModB.(a ~ b). (* 使用ModB的_ ~ _ *)
  

  这种方法适合冲突符号使用频率不高的场景，代码虽然长一点，但逻辑最清晰。

• 局部导入（Section范围内导入）
  如果两个模块的符号只在某一段代码里需要，可以把其中一个模块的导入放在Section中，Section结束后导入就会失效，不会影响全局环境的符号。示例：

  (* 全局导入第一个模块 *)
  Import ModA.
  
  Section WorkWithModB.
    (* 只在这个Section里导入ModB *)
    Import ModB.
    (* 这里可以自由使用ModB的所有符号，包括_ ~ _ *)
    Lemma example : a ~ b -> True.
    Proof. trivial. Qed.
  End WorkWithModB.
  
  (* 离开Section后，全局环境里还是只有ModA的_ ~ _，不会冲突 *)
  Check a ~ b. (* 调用的是ModA的记号 *)
  

你遇到的错误提示是因为两个模块给同一个记号_ ~ _设置了不同的优先级层级（一个是27，一个是50），Coq无法自动合并这些定义，上面的几种方法都能绕过这个问题，根据你的使用场景选一个最合适的就行。

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