Coq 中如何将记号（Notation）全局添加到指定作用域（Scope）

安全阿岳

2026-10-4

问题原因

你遇到的是Coq模块系统和记号作用域绑定的导出规则问题：

#[global]标记的作用是让记号在所在模块被导入后全局可见，而非直接穿透模块作用域自动生效。你在模块A内定义的所有记号默认都属于模块A的命名空间，关闭模块后不会自动暴露到全局。
默认不带修饰符的Notation定义在模块内时，等效于模块私有定义，即使绑定到全局声明的作用域，也不会随模块导入导出。

解决方案

方案1：导入定义记号的模块

在需要使用记号的模块里导入定义方模块即可，针对你的示例修改如下：

Declare Scope scope0.
Declare Scope scope1.
Declare Scope scope2.

Module A.
  (* 只有加了global的记号会在模块导入后暴露 *)
  Notation ". A" := (list A) (at level 100) : scope0.
  #[global]
  Notation ". A" := (list A) (at level 100) : scope1.
  #[local]
  Notation ". A" := (list A) (at level 100) : scope2.
End A.

Module B.
  (* 导入模块A，global标记的记号会生效 *)
  Import A.
  Print Scope scope1. (* 可以查到对应记号 *)
  (* scope0、scope2的记号因为没有global标记，依然不可见 *)
End B.

方案2：直接将记号定义在全局层级

如果不需要模块封装，直接在模块外定义记号，即可全局生效，不需要额外导入。

方案3：使用模块类型+导出机制批量导出记号

如果需要封装多个相关记号到模块中，可以搭配Export标记让导入链路自动传递记号：

Module A.
  #[global, export]
  Notation ". A" := (list A) (at level 100) : scope1.
End A.

(* 其他模块导入A后，再被第三方导入时，记号也会自动传递 *)
Module C.
  Export A.
End C.

Module B.
  Import C.
  Print Scope scope1. (* 记号依然可见 *)
End B.