Как импортировать модули в Coq?

У меня возникли проблемы с импортом определений из модулей в Coq. Я новичок в Coq, но не смог решить проблему, используя справочное руководство по языку или онлайн-учебник. У меня есть модуль, который определяет сигнатуру и аксиомы для конечных множеств, которые я намерен реализовать в другом модуле. Это еще не все, но выглядит примерно так (Для справки, я внимательно слежу за работой Филлиатра о конечных автоматах): 

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. Как импортировать определения (в данном случае аксиомы) из одного модуля в другой? Я в основном следовал шагам, изложенным в лекциях Пирса "основы программного обеспечения". Однако они не работают на меня.
2 13
import module coq

2 ответа:

Я думаю, что ваша путаница возникает из - за того, что в Coq "модуль" может означать две разные вещи-исходный файл (Foo.v) и модуль в исходном файле (Module Bar.) попробуйте назвать исходный файл иначе, чем модуль в исходном файле. Затем используйте Require Import для импорта одного исходного файла в другой (таким образом, Укажите имя исходного файла, а не имя модуля в исходном файле).

Кроме того, я не очень хорошо знаком с Modules и Module Types в Coq, но разве вам не нужно иметь Module Type там, а не Module?

5

Попробуйте добавить в ваш файл .emacs некоторые явные пути включения: 

 '(coq-prog-args (quote ("-I" "/home/tommd/path/to/some/stuff/lib" "-I" "/home/tommd/path/to/more/stuff/common")))
1