如何在Coq中导入模块？

Question

我在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,与命令Require Import FinSet.当我尝试导入模块时,Coq(通过Proof General)发出警告:

Warning: trying to mask the absolute name "FinSet"!

此外,我看不到任何定义FinSet.如何将定义(在本例中为公理)从一个模块导入另一个模块？我基本上遵循了Pierce的"软件基础"讲座中概述的步骤.但是,他们不适合我.

Answer 1

我认为你的混淆源于Coq中的"模块"可能意味着两个不同的东西 - 源文件(Foo.v)和源文件中的模块(Module Bar.)尝试命名源文件与源文件中的模块不同文件.然后使用Require Import将一个源文件导入另一个源文件(因此,指定源文件的名称,而不是源文件中的模块名称).

另外,我对Coq中的Modules和Module Types 不太熟悉,但你不需要在Module Type那里,不是Module吗？