Как импортировать модули в Coq? - PullRequest
Новая
       16

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

13 голосов
/ 26 октября 2011

У меня проблемы с импортом определений из модулей в 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 ]

6 голосов
/ 29 октября 2011

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

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

2 голосов
/ 27 октября 2011

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

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