Coq FAQ

Does Coq support unicode?

Yes it does. In fact you don’t need to do anything and you will be able to use unicode in notations.

Caution

Certain unicode characters are seen as letters, and only can be used inside identifiers. For Coq Notations however you are free to use them however you want.

You can actually even use ∀ (x : A), B instead of forall (x : A), B, A ∧ B instead of A /\ B, A → B instead of A -> B and so on… as soon as you import the Utf8 module:

From Coq Require Import Utf8.

Tip

You can use the latex-input VSCode extension (or presumably others of your liking) to enter unicode characters easily.

Do I really have to manually evaluate each line when navigating a Coq file?

Assuming you use VSCoq Legacy or CoqIDE, then the answer is mostly yes. However, you can also tell Coq to evaluate up to the point where your cursor is. In VSCoq you do it with Ctrl + Alt + → or “Interpret to point” from the commande palette (Ctrl + Shift + P).

If you use VSCoq 2 instead, then you have access to “Continuous mode” which displays the goal where your cursor is, and otherwise evaluates everything in the background. See our section on editors for more.

Why can’t I use a dash (-) in the filename?

Coq doesn’t let you use dashes in the filename (for instance if you call it my-file.v then VSCoq will not work) because implicitly, a filename becomes a Coq module (a bit like OCaml files become OCaml modules). So myFile.v will become the myFile module, and those don’t allow for dashes in them. In fact, it’s better to stick to letters and underscores (_).

Note

There’s no need to understand all this, just know that if Coq won’t even start then it’s a good idea to try for a simpler name, just in case.

I’m testing my own tactic and I would like to know how long it takes, how can I do that?

If you want to know how long a tactic or a command takes, you can use the Time command for instance as follows:

Time my_tactic.

I don’t like the name Coq, isn’t going to change?

Yes, possibly before the end of the course, Coq should be renamed to Rocq. Officially it’s still called Coq, but people have already starting using the new name.

Can I use Nix to install Coq and MetaCoq?

Nix can be used to install Coq and Equations, as well as many other packages, but it seems to be currently broken when it comes to MetaCoq so unless you want to spend hours debugging things, we recommend you use opam or the binary installers as advised in the installation page.

Is it possible to simplify only parts of an expression?

If simpl simplifies too much, you can also use eg. simpl add to only simplify addition. So for instance (0 + S n) - m will become S n - m without Coq unfolding also -.

You will see in lesson 3 a bit more about computation and how to control it.

How do I use multiple files in a project?

If you want to have a multi-file project, you need to create a _CoqProject at the root of your directory (the one you open eg. with VSCoq) of the following shape.

-Q . Project

ex1.v
ex2.v
ex3.v

It lists all the files (or path to files if not in the same directory) and gives a name to the project (here: Project).

Note

You don’t need to put then in any particular order, but it’s usually nicer to have them in dependency order.

Then in one of the files you can import, eg, the definitions from ex1.v by writing

From Project Require Import ex1.

Note

The .v is removed from the name here.

You can then build your project by using the following Makefile.

all: Makefile.coq
    $(MAKE) -f Makefile.coq

clean: Makefile.coq
    $(MAKE) -f Makefile.coq clean

Makefile.coq:
    coq_makefile -f _CoqProject -o Makefile.coq

.PHONY: all clean

Running make is then going to build all your project. And you might need to run make again after an update to see it happen in CoqIDE or VSCoq.

Important

Make sure that the Makefile uses tabs and not spaces, otherwise it may not work.