Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Proof assistants (24h, 3 ECTS)

In charge: Théo Winterhalter

Practical information for 2023-2024

The class takes place in the first period (08:45-11:45) in room 1002 in Bâtiment Sophie Germain. The first lecture is on September 18th.

Students must bring their own laptop with Coq installed prior to the first lecture (⚠️): we require version 8.16 together with Equations and MetaCoq installed. To that end we assume students have installed the corresponding Coq Platform. Please don't hesitate to send us an email if you have trouble installing anything before the first lecture.

⬇️ See below for precise information on how to install Coq or for which editor to use. ⬇️

Please check your installation is correct by trying to run the test file we provide (make sure to save it with a .v extension without dashes (-)). Once again, contact us if you have any trouble.

A background in functional programming, logic, or basic usage of Coq is preferable, but not mandatory or necessary to pass the lecture.

Teachers for 2023-2024

Goals

The goal of this course it to teach about proof assistants through practice in the Coq proof assistant. Students will also learn about the underlying dependent type theory it implements.

Proof assistants have a wide range of applications from mathematical theorems (including some, like the four colour theorem, that have no proof without the use of a computer) to program verification (which can be crucial for critical software, sometimes used in life-or-death situations). We will give an overview of proof assistants as well as motivations and applications during the lectures.

Outline of the course

The course is divided over 8 weeks with the tentative following schedule. For each lecture we plan to provide optional advanced exercises. Doing them is not mandatory to pass the course, but we encourage you to try them.

  1. 18 Sept. Overview of the course. Presentation of proof assistants. Getting acquainted with Coq. Slides Live coding (with comments) Exercise sheet Solutions
  2. 2 Oct. Proof terms and meta-theory. Overview of other proof assistants. Exercise sheet Slides Slides on meta-theory and other proof assistants Live coding Overview on reduction rules Solutions
  3. 16 Oct. Mathematical modelling. Automation. Live coding Exercises Solutions
  4. 30 Oct. Advanced elimination / induction. Live coding Exercises Solutions
  5. 6 Nov. Dependent functional programming. Conclusion. Exercises Awesome Coq (list of tools, libraries and resources for Coq)

Evaluation

There will be an exam and a project, each counting for half of the final grade.

The pdf for the project can be found here. The deadline for the project is November 20th at 21:00. The solutions will be checked with Coq 8.16.1.

The exam will happen on November 27th in Salle 1002 (the usual room where we have the lecture) at 08:45 and will be 3 hours long. No machine is allowed. No material is allowed, apart from one hand-written A4 page (both sides).

Language

The course will be taught in English by default. You can still ask us questions in French.

Related courses

Related internships

Do not hesitate to contact us about internships. You may contact people even if they did not add an internship to the MPRI page. We know a lot of people in the domain so we can help you.

- Various topics in formal logic and proof assistants with Yannick Forster

- Ghost dependent types with Théo Winterhalter

- Semantics of inductive types / A diagram editor to help mechanise categorical proofs in Coq with Ambroise Lafont

- A Generalized Search Command for Coq-Actema / Outputting Actema Proofs with Benjamin Werner

- Implementation of hierarchies of algebraic structures in type theory with Assia Mahboubi

Installing Coq

We require the students to come with laptop on which Coq 8.16.1 is already installed. We additionally require MetaCoq 1.1 and Equations 1.3. The easiest way to install all of them at once, together with CoqIDE is to install the Coq Platform 2022.09.1 at the extended level.

You have several options: installing the Coq Platform from binaries, or installing the packages separately using opam. If you elect other ways to install Coq (eg. using Nix) then we may not be able to help you. In any case, check that everything works as expected on the test file we provide (make sure to save it with a .v extension without dashes (-)).

Please contact us ahead of time if you have trouble installing Coq or checking that the test file works.

Installing the platform from binaries

Installation should be as simple as downloading the binaries corresponding to your OS Coq Platform release and installing them. You may further read instructions corresponding to your OS: macOS, Windows or Linux.

You can also follow instructions in there to find alternative ways to install the extended level of the platform.

If you are on macOS make sure to read the notes towards the end of the file: macOS will probably refuse to launch CoqIDE unless you open your system settings and explicitly allow it to run.

Installing directly from opam

In case you want to use the ocaml package manager opam, first make sure you have opam 2 installed. Then run the following commands:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq.8.16.1 coq-metacoq-template.1.1.1+8.16 coq-equations.1.3+8.16

If you plan to use multiple versions of Coq, then you can create an opam switch for each Coq version. You can also use pinning to make sure you do not inadvertently change the Coq version by running `opam upgrade`.

opam switch create coq.8.16
opam pin add coq 8.16.1
opam install coq-metacoq-template.1.1.1+8.16 coq-equations.1.3+8.16

Which editor to use?

We recommend you use either CoqIDE or Visual studio code (VSCode)/VSCodium with the VSCoq extension. The Coq website has a page listing most available options in case you really want to use a different editor.

If you installed the Coq Platform, then you should have CoqIDE ready to go with the correct version. It should be the simplest tool to use as the interface is built exactly for Coq. You can press button to evaluate a file etc.

VSCoq will let you use a more modern approach. Install version v0.3.9 (and not the preview version that is only beta and will only work with Coq 8.18 and onwards, click on the arrow next to uninstall and select another version if it forced the update to 2.0.0): for VSCode or VSCodium. If you have installed Coq via opam, then it should be in your PATH and VSCoq should pick it up (if you open a .v file, such as the test file we provide, it will complain if it did not find a Coq installation). In case it doesn't find it automatically—eg. if you installed the Coq Platform—then you can try to launch VSCode from a terminal that find Coq by running

code .

If it doesn't work, you can open the settings for VSCode and search for “Coq Bin Path”, this will let you add the path to the folder containing the Coq binary. It depends on where you installed it. If you have a terminal which finds coq then you can run

dirname $(which coqtop)

to find the corresponding path.

References

The most important resources for you are:

Books to learn Coq:

Other related documents:

Lecture notes from an older course: “Assistants de Preuves” (PDF, HTML).

Previous exams

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA