Programs and Proofs: Mechanizing Mathematics with Dependent Types

Installation and Set-up

In order to follow the course, execute the examples and complete the exercises, you are expected to have the Coq Proof Assistant with Ssreflect extension installed at your machine. This page contains some general instructions on the installation and set-up.

There is also an option to use a virtual machine image instead of installing all the software natively (the instruction on obtaining the VM are below).

For further information or assistance on set-up, please, contact .

Installing Coq and Ssreflect natively

The sources of the course files are checked to compile and tested with Coq version 8.6 and Ssreflect/Mathematical Components version 1.6.1. It is not guaranteed that the same examples will work seamlessly with different versions. Therefore, several recipes on how to build install the necessary software are provided below.

Linux, Cygwin and macOS

Linux and macOS users are recommended to compile Coq 8.6 and Ssreflect/Mathematical Components 1.6 from sources, which would take around an hour (getting Coq using a system-specific package manager, such as aptitude or MacPorts is another option, although the Coq version acquired this way is not guaranteed to work with Ssreflect 1.6). In order to be compiled, Coq 8.6 requires OCaml version 4.02.2 or later, Camlp5 version >=6.13, GNU Make version 3.81 or later (see the INSTALL file from the archive with sources for the full list of requirements on configuration and installation). Once compiled, the following environment variables should be set (e.g., in ~/.bashrc or ~/.profile configuration files) to build Ssreflect (with the respective paths chosen during the Coq's installation): 
    export COQBIN="/usr/local/bin/"
    export COQ_MK="/usr/local/bin/coq_makefile"
It is also recommended to keep sources of Ssreflect and Mathematical Components easily accessible as reading them might be helpful when working with libraries (for instance, in the folder ~/misc/mathcomp-1.6/mathcomp). Upon installing Ssreflect via make install, the following environment variable should be also set up: 
    export SSRCOQ_LIB="/usr/local/lib/coq/user-contrib/mathcomp/ssreflect"
Alternatively, instead of running make install, one can set up the environment variable SSRCOQ_LIB to point to the folder ssreflect-location/theories, which contains all Ssreflect modules compiled (and ssreflect-location denotes the location of the directory where Ssreflect has been unpacked to).

Emacs and Proof General set-up

Emacs (or Aquamacs for macOS users) text editor provides a convenient environment for Coq development, thanks to the Proof General mode.

On Unix-like systems, clone Proof General from its GitHub repository, following the instructions below. Upon downloading and unpacking, add the following lines into the .emacs configuration file located in the home directory (~/) in Unix and in C:\ root in Windows (possibly replacing the ~/misc/ part with the path where Proof General and Ssreflect sources were unpacked/cloned). 

    ;; Proof General support
    (load-file "~/misc/PG/generic/proof-site.el") 

    ;; Ssreflect support 
    (load-file "~/misc/mathcomp-1.6/mathcomp/ssreflect/pg-ssr.el")
Linux users, more used to the Windows-style Copy/Paste/Undo keystrokes can also find it convenient to enable the Cua mode in Emacs, which can be done by adding the following lines into the .emacs file: 
    (cua-mode t)
    (setq cua-auto-tabify-rectangles nil)
    (transient-mark-mode 1)
    (setq cua-keep-region-after-copy t)
Every Coq file has the extension .v. Opening any .v file will automatically trigger the Proof General mode.

Using a virtual machine image

WARNING: The virtual machine image hasn't yet been updated for Coq 8.5 and Ssreflect 1.6 and contains an older version of the course.

If compiling and installing Coq and Ssreflect from scratch looks like too much hassle, there is also a possibility to use a virtual machine image with all necessary libraries preinstalled and Emacs set up to work with Ssreflect. The image requires Oracle VirtualBox to be used; it is about 1.8 GB size and can be obtained by the following link. It runs Ubuntu 14.04 and automatically logs in when started with the user coquser (use the password coquser whenever it is required). The folder ~/misc contains the sources of Ssreflect and Proof General.

Checking your set-up

To check that your setup is correct, create in Emacs a file with an extension .v and the following text in it: 

From mathcomp
Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Test.

Variable A : Type.

Theorem counterexample P : (exists x : A, ~P x) -> ~(forall x, P x).
Proof.
by case=>x H1 H2; apply: H1 (H2 x).
Qed.

Print counterexample.

End Test.
After that, set the text caret to the very last position of the file and press Ctrl-c Ctrl-Enter. This will activate the Proof General interactive checking mode and will interpret the file. As the result, the buffer *goals* should display the following message: 
Module Test is defined
which would mean that your set-up is correct and you are ready for hacking in Coq/Ssreflect.

[Back to the course page]

Last modified: Thu Jan 3 18:33:17 +08 2019