Specifying Paths for exporting files in Coq?

0
votes

I am writing my first own Coq file but I am experiencing trouble in exporting another user defined file (defined by the book Software Foundations).

The issue is my current Coq file has path Coq/NWA.v and the file I want to import has path Coq/SoftwareFoundations/lf/Rel.v. I tried the following syntaxes:

From Coq/SoftwareFoundations/lf Require Import Rel.v

&

From Coq.SoftwareFoundations.lf Require Import Rel.v

&

From ./../SoftwareFoundations/lf Require Import Rel.v

all of which give a syntax error. How can I import the Rel.v file?

1
coq
It might be relevant to read the first section of softwarefoundations.cis.upenn.edu/lf-current/Induction.html – Li-yao Xia
I followed the steps: (1) I made a _CoqProject file with content '-Q ./../SoftwareFoundations/lf/ LF' . (2) I added the line From 'LF Require Export Rel' in my file NWA.v. (3) From command line I run the cmd: "coq_makefile -f _CoqProject *.v -o Makefile" (4) I recompiled the file Rel.v I still got a syntax error. – Kaind

1 Answers

1
votes

tl;dr: The correct syntax is

From LF Require Import Rel.

To manage Coq files, there are two kinds of paths to be aware of:

  • Physical paths: the usual file paths you're used to, like Coq/SoftwareFoundations/lf.

  • Logical paths: fully qualified module names, that are mapped to files by the Coq compiler.

What the -Q my/path/to/lf LF option (that ultimately needs to be passed to coqc) does is map logical paths (LF) to physical paths (my/path/to/lf).

In a Coq file, the Require Import command (including the From _ Require Import _) works with logical paths. The rule of thumb is that the contents of a .v file only talks about logical paths, although there are a couple of exceptions (e.g., Add LoadPath and extraction).

The Logical Foundations volume is built using logical path LF.ModuleName, that's what you need to use in Coq/NWA.v to import Rel:

From LF Require Import Rel.

(* or *)

Require Import LF.Rel.