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

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

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 "Software Foundations". Однако они не работают для меня.

Ответы

Ответ 1

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

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

Ответ 2

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

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