14

我在从 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并尝试将其加载到另一个模块中,例如FinSetListor 。当我尝试导入模块时,Coq(通过 Proof General)发出警告:FinSetRBTRequire Import FinSet

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

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

4

2 回答 2

6

我认为你的困惑是因为在 Coq 中,“模块”可能意味着两个不同的东西——源文件 (Foo.v) 和源文件中的模块 ( Module Bar.) 尝试以与源文件中的模块不同的方式命名源文件文件。然后用于Require Import将一个源文件导入另一个(因此,指定源文件的名称,而不是源文件中模块的名称)。

另外,我对Coq 中Module的 s 和Module Types 不是很熟悉,但你不需要Module Type那里,不是Module吗?

于 2011-10-29T14:27:26.067 回答
2

尝试将.emacs一些明确的包含路径添加到您的文件中:

 '(coq-prog-args (quote ("-I" "/home/tommd/path/to/some/stuff/lib" "-I" "/home/tommd/path/to/more/stuff/common")))
于 2011-10-26T23:22:26.247 回答