如何在 Coq 中导入模块？
我在从 Coq 中的模块导入定义时遇到问题。我是 Coq 新手，但无法使用该语言的参考手册或在线教程解决问题。我有一个定义有限集签名和公理的模块，我打算在另一个模块中实现它。还有更多内容，但它看起来像这样（作为参考，我密切关注 Filliatre 关于有限自动机的论文）：
Module FinSet.
...
Parameter fset : Set -> Set.
Parameter member : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union :
forall A : Set, forall a b : fset A, forall x : A, i
member x (union a b) <-> (member x a) \/ (member x b).
...
End FinSet.
我使用 coqc 编译模块并尝试将其加载到另一个模块中，例如FinSetList 或 FinSetRBT，使用命令需要导入 FinSet。当我尝试导入模块时，Coq（通过 Proof General）发出警告：
Warning: trying to mask the absolute name "FinSet"!
此外，我看不到 FinSet 中定义的任何内容。如何将定义（在本例中为公理）从一个模块导入另一个模块？我基本上遵循了皮尔斯的“软件基础”讲座中概述的步骤。然而，他们不为我工作。
I'm having trouble importing definitions from modules in Coq. I'm new to Coq, but couldn't solve the problem using the language's reference manual or online tutorial. I have a module that defines a signature and axioms for finite sets, which I intend to implement in another module. There's more to it, but it looks something like this (for reference, I'm closely following Filliatre's paper on finite automata):
Module FinSet.
...
Parameter fset : Set -> Set.
Parameter member : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union :
forall A : Set, forall a b : fset A, forall x : A, i
member x (union a b) <-> (member x a) \/ (member x b).
...
End FinSet.
I compile the module using coqc and attempt to load it into another module, say FinSetList or FinSetRBT, with the command Require Import FinSet. When I attempt to import the module, Coq (via Proof General) issues the warning:
Warning: trying to mask the absolute name "FinSet"!
Furthermore, I can't see anything defined in FinSet. How do I import the definitions (in this case, axioms) from one module into another? I essentially followed the steps outlined in Pierce's "Software Foundations" lectures. However, they aren't working for me.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
我认为您的困惑源于这样一个事实：在 Coq 中，“模块”可以表示两个不同的东西 - 源文件 (Foo.v) 和源文件中的模块 (
Module Bar.) 尝试命名您的源文件与该源文件中的模块不同。然后使用Require Import将一个源文件导入到另一个源文件中（因此，请指定源文件的名称，而不是源文件中模块的名称）。另外，我对 Coq 中的
Module和Module Type不是很熟悉，但是你不需要在那里有Module Type吗？不是模块？I think your confusion arises from the fact that in Coq, "module" can mean two different things - a source file (Foo.v) and a module within a source file (
Module Bar.) Try naming your source file differently from your module in that source file. Then useRequire Importto import one source file into another (so, specify the name of the source file, not the name of the module in the source file).Also, I am not very familiar with
Modules andModule Types in Coq, but don't you need to haveModule Typethere, notModule?尝试向您的 .emacs 文件添加一些显式包含路径：
Try adding to your
.emacsfile some explicit include paths: