Table of Contents
## 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
Students must bring their own laptop with Coq installed ⬇️ 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- Yannick Forster, Chargé de Recherche Inria Paris
- Théo Winterhalter, Chargé de Recherche Inria Saclay
## GoalsThe 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 courseThe 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. - 18 Sept. Overview of the course. Presentation of proof assistants. Getting acquainted with Coq. Slides Live coding (with comments) Exercise sheet Solutions
- 25 Sept. Inductive types.
- 2 Oct. Proof terms and meta-theory. Overview of other proof assistants.
- 9 Oct. Mathematical modelling. Automation.
- 16 Oct. Equality.
- 23 Oct. Advanced elimination / induction.
- 30 Oct. Meta-programming.
- 6 Nov. Dependent functional programming. Conclusion.
## EvaluationThere will be an exam and a project, each counting for half of the final grade.
The exam will (tentatively) happen on November 27th at 08:45 and will be 3 hours long. No machine is allowed. No material is allowed, apart from More information to come on the project. I will consist in solving exercises in the Coq proof assistant. They will be checked with Coq 8.16.1. ## Material (slides, exercises, project)We will update this section after every class. ## LanguageThe course will be taught in English by default. You can still ask us questions in French. ## Related courses## Related internships## 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 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 binariesInstallation 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 opamIn 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— 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. ## ReferencesThe most important resources for you are: - Coq Zulip chat which is the most active platform for asking questions about Coq. A (not so easy to read) archive is publicly available.
Books to learn Coq: - B. C. Pierce, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hriţcu, V. Sjöberg, B. Yorgey. Software Foundations (Volume 1).
- A. Chlipala. Certified Programming with Dependent Types
- Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS Series (2004), Springer. (Version française).
Other related documents: - The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory.
- E. Rijke. Introduction to homotopy type theory. arXiv preprint arXiv:2212.11082 (2022).
- A. Mahboubi, E. Tassi. Mathematical Components book.
- I. Sergey. Programs and Proofs: Mechanizing Mathematics with Dependent Types. Lecture Notes.
- G. Smolka. Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant. Lecture Notes.
Lecture notes from an older course: “Assistants de Preuves” (PDF, HTML). ## Previous exams |