如何在Coq中查找定义所在文件？以list_norepet为例

我平时做Coq证明时也经常碰到这个问题，分享几个实用的方法帮你定位list_norepet这类定义的源文件：

• 用Locate命令直接查询：这是最省心的方式，在Coq交互环境里输入：

  Locate list_norepet.
  

  它会输出该常量的定义位置，通常包含对应的模块和完整源文件路径。比如输出可能是这样的：

  Constant List.list_norepet
  located in file /usr/local/lib/coq/theories/Lists/List.v

• 通过模块反向定位文件：如果Locate只返回了模块名（比如List.list_norepet），你可以进一步查询模块对应的文件：

  Locate Module List.
  

  这条命令会输出该模块所在的源文件路径。

• 交互式IDE直接跳转：如果你用CoqIDE、VsCoq或者ProofGeneral这类工具，直接右键点击目标标识符（比如list_norepet），选择「跳转到定义」（Go to definition），就能直接打开对应的源文件并定位到定义位置，效率很高。

另外提一句，有些旧版本的Coq里Print命令确实不会显示文件名，但Locate命令在几乎所有版本中都能提供这个关键信息，优先用它准没错。

内容的提问来源于stack exchange，提问作者Vilhelm Sjöberg