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

#import #module #coq

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

Ответ №1:

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

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

1. Да, это кажется правильным. Очевидно, я неправильно импортировал модули.

2. Исходный файл должен быть скомпилирован coqc name_of_the_source.v перед импортом Require Import name_of_the_source . Вы также можете, если задействованы разные пути, использовать Add LoadPath "../mypath/" в начале вашего .v файла.

Ответ №2:

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

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

1. Да, я пробовал это. Комбинация Add LoadPath "/home/pordan30/test" in a .v file и '(coq-prog-args (quote ("-I" "/home/pordan30/test"))) in my .emacs file приводит к той же проблеме при импорте скомпилированных модулей в ~/test (т. Е. В тот .v файл, в который добавлен путь загрузки). Спасибо, что предложили некоторую помощь.