在Coq中指定导出文件的路径？

Question

我正在编写我自己的第一个Coq文件，但在导出另一个用户定义的文件（由《软件基础》一书定义）时遇到了麻烦。

问题是我当前的Coq文件的路径是 Coq/NWA.v 而我要导入的文件的路径是 Coq/SoftwareFoundations/lf/Rel.v. 我尝试了以下语法。

From Coq/SoftwareFoundations/lf Require Import Rel.v

&

From Coq.SoftwareFoundations.lf Require Import Rel.v

&

From ./../SoftwareFoundations/lf Require Import Rel.v

都出现了语法错误。如何导入Rel.v文件？

Answer 1

tl;dr: 正确的语法是

From LF Require Import Rel.

---

要管理Coq文件，需要注意两种路径。

• 物理路径： 通常的文件路径，你已经习惯了，像... Coq/SoftwareFoundations/lf.

• 逻辑路径：完全限定的模块名称，被Coq编译器映射到文件中。

什么是 -Q my/path/to/lf LF 选项（最终需要传递给 coqc)的作用是映射逻辑路径(LF)到物理路径(my/path/to/lf).

在Coq文件中， Require Import 命令（包括 From _ Require Import _)的工作原理是逻辑路径。经验法则是在 .v 文件只谈逻辑路径，尽管有几个例外（例如......和提取）。Add LoadPath 和提取）。)

逻辑基础卷是使用逻辑路径建立的。LF.ModuleName，这就是你需要在 Coq/NWA.v 导入 Rel:

From LF Require Import Rel.

(* or *)

Require Import LF.Rel.