CODEWITHSUNDEEP
importcoq
OrenIshShalom
OrenIshShalom

Reputation: 7102

Import Coq variables from another file

I proved some basic properties of fields based on the axioms here, and now I continued to define axioms of vector spaces. In particular, Field.v contains the following lines:

(***********)
(* 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).

I imported it in a file called VectorSpace.v but Coq complains it doesn't know of 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).

Here is the error message:

The reference F was not found in the current environment.

Upvotes: 1

Views: 568

Answers (2)

Li-yao Xia
Li-yao Xia

Reputation: 33409

If you really mean to axiomatize a single field for the whole development, use Parameter (or Axiom, same meaning) instead.

In contrast, Variable is meant to be used in a Section, and declares bindings which will be turned into arguments, so that the development can be instantiated with different fields down the line.

Variable outside of sections has a quite different meaning, so to avoid confusion I would recommend not using this command that way.

Variable ...
(...) Using the Variable command out of any section is equivalent to using Local Parameter.

Local Parameter ...
Such parameters are never made accessible through their unqualified name by Import and its variants. You have to explicitly give their fully qualified name to refer to them.

--- The Coq Reference Manual

Upvotes: 2

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

  1. Replace Variable by Axiom declarations everywhere.

  2. Create a _CoqProject file at the root of your project with the structure of your project. For instance:

    -Q . MyProject
Field.v
VectorSpace.v

    Now, you can use MyProject.Field to refer to Field.v in VectorSpace.v (I believe you were importing the Field module from the standard library before).

  3. Generate a makefile and compile the project:

    coq_makefile -f _CoqProject -o Makefile
make

If you are using Proof General in Emacs, it should be possible to run through VectorSpace.v interactively. I believe that CoqIDE has some support for automating steps (2) and (3), but I am not sure.

Upvotes: 3

Related Questions