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の別のモジュールにロードしようとします。モジュールをインポートしようとすると、Coq（Proof General経由）が警告を発行します。FinSetListFinSetRBTRequire Import FinSet

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

さらに、で定義されているものが表示されませんFinSet。あるモジュールから別のモジュールに定義（この場合は公理）をインポートするにはどうすればよいですか？私は基本的に、Pierceの「SoftwareFoundations」講義で概説されている手順に従いました。しかし、彼らは私のために働いていません。

4

2 に答える 2

6

Coqでは、「モジュール」は2つの異なる意味を持つ可能性があるという事実から混乱が生じると思います。ソースファイル（Foo.v）とソースファイル内のモジュール（Module Bar.）ソースファイルの名前をそのソース内のモジュールとは異なるものにしてみてくださいファイル。次に、を使用Require Importして1つのソースファイルを別のソースファイルにインポートします（したがって、ソースファイル内のモジュールの名前ではなく、ソースファイルの名前を指定します）。

また、私はCoqModuleのsとsにあまり精通していませんが、そこにModule Typeいる必要はありませんか？Module TypeModule

于 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 に答える