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:

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:

Require Import Setoid Morphisms.

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.

2 Answers

Arthur Azevedo De Amorim On Best Solutions
  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

    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

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.

Li-yao Xia On

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