Импорт переменных Coq из другого файла - PullRequest
Новая
       15

Импорт переменных Coq из другого файла

1 голос
/ 18 мая 2019

Я доказал некоторые базовые свойства полей, основанные на аксиомах здесь , и теперь я продолжил определять аксиомы векторных пространств. В частности, Field.v содержит следующие строки: 

(***********)
(* IMPORTS *)
(***********)
Require Import Setoid Morphisms.

Variable (F:Type).
Variable (zero:F).
Variable (one :F).  
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (eq: F -> F -> Prop).

Я импортировал его в файл с именем VectorSpace.v, но Coq жалуется, что не знает F: 

(*******************)
(* GENERAL IMPORTS *)
(*******************)
Require Import Setoid Morphisms.

(*******************)
(* PROJECT IMPORTS *)
(*******************)
Require Import Field.

(****************)
(* Vector Space *)
(****************)
Variable (V:Type).
Variable (zerov:V).
Variable (onev :V).
Variable (addv: V -> V -> V).
Variable (mulv: F -> V -> V).

Вот сообщение об ошибке: 

The reference F was not found in the current environment.

Ответы [ 2 ]

2 голосов
/ 18 мая 2019

Если вы действительно хотите аксиоматизировать одно поле для всей разработки, используйте вместо него Parameter (или Axiom, то же значение).

Напротив, Variable предназначен для использования в Section и объявляет привязки, которые будут превращены в аргументы, так что разработка может быть реализована с различными полями внизу строки.

Variable вне разделов имеет совершенно другое значение, поэтому во избежание путаницы я бы рекомендовал не использовать эту команду таким образом.

Variable ...
(...) Использование команды Variable из любого раздела эквивалентно использованию Local Parameter.

Local Parameter ...
Такие параметры никогда не будут доступны через их неполное имя при импорте и его вариантах. Вы должны явно указать их полное имя, чтобы ссылаться на них.

--- Справочное руководство Coq

2 голосов
/ 18 мая 2019

  1. Заменить Variable объявлениями Axiom везде.

  2. Создайте файл _CoqProject в корне вашего проекта со структурой вашего проекта. Например: 

    -Q . MyProject
Field.v
VectorSpace.v

    Теперь вы можете использовать MyProject.Field для ссылки на Field.v в VectorSpace.v (я полагаю, вы импортировали модуль Field из стандартной библиотеки ранее).

  3. Сгенерируйте make-файл и скомпилируйте проект: 

    coq_makefile -f _CoqProject -o Makefile
make

Если вы используете Proma General в Emacs, должна быть возможность проходить через VectorSpace.v в интерактивном режиме. Я считаю, что CoqIDE имеет некоторую поддержку для автоматизации шагов (2) и (3), но я не уверен.

...