|
Table of Contents
Proof assistants (24h, 3 ECTS)In charge: Théo Winterhalter Practical information for 2023-2024The 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
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.
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 one hand-written A4 page (both sides). 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 coursesRelated internshipsInstalling CoqWe 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 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—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. ReferencesThe 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 |