===== M2 LMFI: Functional programming and formal proofs in Coq ===== ===== M2 LMFI: Programmation fonctionnelle et preuves formelles en Coq (PF2) ===== ==== Introduction ==== The 2024-2025 PF2 course is taught by Alexis Saurin. It was previously taught by [[https://www.irif.fr/users/letouzey/index|Pierre Letouzey]] and **an important part of the course material is adapted / expanded** from his previous material and by (older) material from Alexandre Miquel. The rooms for the class and lab sessions is 2006. [[https://edt.math.univ-paris-diderot.fr/#/parcours/math/m2/4670|Look at the schedule of LMFI]] to get the proper information and in case of doubt, check the course discord on which I will post changes in classroom assignment. == Coming lectures planning: == * No lecture on october 16th * 21st October, 15h15-17h15 in room 1020 then 17h15-19h15 in computer lab 2005 * 22nd October, 13h45-18h in room 2006 * No lecture on October 30th * 6th November, 13h45-18h in room 2006 * 13th November, 13h45-18h in room 2006 * 20th November, 15h30-18h in room 2006 * 27nd November, 13h45-18h in room 2006 * 11th December, 13h45-18h in room 2006 * **18th** December, 13h45-18h in room 2006 -- Lecture by Marie Kerjean ==== Aim of the course and organization ==== === Goals of the course === The course has four main goals: * to serve as an introduction to (functional) programming (in Coq); * to serve as an introduction to the mechanization of proofs in Coq, and more generally to proof assistants; * to investigate the basic properties of the logical framework on which Coq is designed, the Calculus of Inductive Construction (CIC), a extension of Martin-Löf dependent type theory; * to give you enough familiarity with Coq proof assistant so that you can use it during your research internship. The course will start with a first period focusing on programming using Coq, for approximately 4 or 5 weeks. Then, we will shift to using Coq as a proof assistant. Globally, I plan that 5 weeks are dedicated to **programming with Coq** (TP0 non included) and 7 weeks are dedicated to **proving with Coq**. === Weekly organization === /*Every week, students will have: * 2H of lectures; * 2H of lab sessions; * some additional exercises to work on and details to work out in the course material published online. */ === Regarding homework === I consider that you should spend "about" the same amount of time studying in class than outside class. More precisely, for PF2, students are expected to spend **3H to 5H a week** of extra working time (studying course material, doing some of the additional exercise of the TP, doing some additional reading given in class or completing some proof / example that has been only partially treated in class. This is of course **purely indicative**: some of the student will need less, some might need more and you may decide focusing some week more on this class and some other week more on another class. The thing to keep in mind is that if for two consecutive weeks you provide no additional work in this course, there are good chances that you end up being lost. The course exam will consist in a formalization project to be handed early in the second semester (details to come around Halloween / Toussaint). ==== Activating your accounts in the computer labs ==== In order to log in the computers: * the login to be used is not directly your university credentials (@u-paris.fr), you need to use your UPC student account to activate your access to the computer labs, * in order to do so, first visit https://stp.math.univ-paris-diderot.fr/ to get a login specific to these lab rooms. * in case of trouble, the guest account allows you to use the computer anyway: bring a usb key in that case so that you can store the files you work on. ==== Course material ==== The Coq files corresponding to the course as well as addition material will be gathered on [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024|this git repository]] from which you can download them. * Lecture 1: First encounter with Coq proof assistant, as a programming language. * Lecture notes * TP0: First steps... Open the webpage for TP0, download the file TP0.v and follow the instructions! [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP0.v|(visit this page to download TP0.v)]] * source for first lecture: Coq functional core, lambda-calculus basics, first data types in Coq: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course1.v|(visit this page to download Course1.v)]] * TP1: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP1.v|(visit this page to download TP1.v)]] * Here is your homework for next wednesday, september 25th: * 0) finish TP0 if you were not one during the first part of the lecture; * 1) please read carefully Course1.v and re-run it with Coq, skipping the paragraph "Some more details on Coq types" and stopping at the end of paragraph "First data types : Boolean and natural numbers" * 2) continue working on the exercises of TP1: try to solve them till exercise 6 (do not spend too much time on ex 2 and 3 if you are stuck on them) * Lecture 2: Fixpoints and Inductive types in Coq * source for second lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course2.v|(visit this page to download Course2.v)]] * TP2: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP2.v|(visit this page to download TP2.v)]] * Lecture 3: Advanced Fixpoints and Inductive types in Coq * source for third lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course3.v|(visit this page to download Course3.v)]] * TP3: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP3.v|(visit this page to download TP3.v)]] * Lecture 4: Introducing dependent types in Coq * source for fourth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course4.v|(visit this page to download Course4.v)]] * TP4: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP4.v|(visit this page to download TP4.v)]] * Lecture 5: Proofs as Programs, Types as Propositions (+ Some complements on dependent types in Coq) * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2024/lecture5|lecture notes]] * source for fifth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course5.v|(visit this page to download Course5.v)]] * TP5: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP5.v|(visit this page to download TP5.v)]] * Lecture 6: Equality Proofs and Proofs by Induction in Coq /* * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2024/lecture6|lecture notes]] */ * source for sixth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course6.v|(visit this page to download Course6.v)]] * TP6: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP6.v|(visit this page to download TP6.v)]] * Lecture 7: Understanding how the tactics for inductive types actually work * source for seventh lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course7.v|(visit this page to download Course7.v)]] * TP7: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP7.v|(visit this page to download TP7.v)]] * Lecture 8: Inversion and automation * source for eighth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course8.v|(visit this page to download Course8.v)]] * TP8: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP8.v|(visit this page to download TP8.v)]] * Lecture 9: The Module system * source for ninth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course9.v|(visit this page to download Course9.v)]] * TP9: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP9.v|(visit this page to download TP9.v)]] * Lecture 10: Proofs by reflection (+ introduction to record types) * source for tenth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course10.v|(visit this page to download Course10.v)]] * TP10: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP10.v|(visit this page to download TP10.v)]] * Lecture 11: Typeclasses * source for eleventh lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course11bis.v|(visit this page to download Course11bis.v)]] * TP11: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP11bis.v|(visit this page to download TP11bis.v)]] * Lecture 12: Mathematical libraries (Marie Kerjean) * source for twelfth lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/Lectures/Course12.v|(visit this page to download Course12.v)]] * TP12: exercises for the practical sessions following the lecture: [[https://gitlab.math.univ-paris-diderot.fr/saurin/pf2-lmfi-2024/-/blob/main/TP/TP12.v|(visit this page to download TP12.v)]] /* * Lecture 1: Introduction to functional programming in Coq //(types and terms; the pure and simply typed lambda-calculus and the arrow type; first steps into CIC, the type theory of Coq: the sorts Type, Set and Prop & dependent product; global and local definitions; sections; global and local declarations; recursive functions definitions; introduction to inductive types.)// * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture1|Material for Lecture 1.]] (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course1.v|.v file]]) * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP1.v|visit this page to download TP1.v.]] ([[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/solution-TP-prog.v|solutions or indications]]) * Notice that TP 1 contained far too many exercises for 2H and I will include all exercise from exercise 6 in next week TP sheet. Please try working out the TP1.v exercise sheet on your own till exercise 5 included. I will post soon the solutions to exercises 1 to 3. * Lecture 2: Introducing inductive types * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture2|Material for Lecture 2.]] (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course2.v|.v file]]) * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP2.v|visit this page to download TP2.v.]] ([[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/solution-TP-prog.v|solutions or indications]]) * Lecture 3: Advanced inductive types and introducing dependent types * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture3|Material for Lecture 3.]] (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course3.v|.v file]]) * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP3.v|visit this page to download TP3.v.]] ([[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/solution-TP-prog.v|solutions or indications]]) * Lecture 4: Advances dependent types * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture4|Material for Lecture 4.]] (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course4.v|.v file]]) * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP4.v|visit this page to download TP4.v.]] ([[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/solution-TP-prog.v|solutions or indications]]) * Lecture 5: More dependent types and ointroducing the proof environment //((o) dependent sum, (i) proofs as programs, (ii) encounter with the third kind: Prop and specific dependent formation rules of CC (iii) Coq proof environment and elementary tactics)// * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture5|Material for Lecture 5.]] /* (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course4.v|.v file]]) */ * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP5.v|visit this page to download TP5.v.]] * Assignement: Finish the exercises in TP5 by the 4th of november! * Lecture 6: Equality proofs & proofs by induction * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture6|Material for Lecture 6.]] /* (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course4.v|.v file]]) */ * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP6.v|visit this page to download TP6.v.]] * Lecture 7: Module sysytem + understanding inductive types * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/lecture7|Material for Lecture 7.]] (+ Corresponding [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course7.v|.v file]]) * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP7.v|visit this page to download TP7.v.]] * Lecture 8: Inversion and automation * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course8.v|Inversion and Automation .v file]] * Lecture 9: Records and reflection * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course9.v|On records and reflection .v file]] * Lecture 10: Mathematical libraries * Marie Kerjean Seminar / Lecture * Lecture 11: Typeclasses * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/Lectures/Course11.v|Typeclasses in Coq .v file]] */ ==== Coq-Related Bibliography ==== * [[https://coq.inria.fr/|The website of the Coq proof assistant]] * [[https://coq.inria.fr/distrib/current/refman/| Coq reference manual]] * [[https://coq.inria.fr/distrib/current/stdlib/|Description of Coq standard library]] and the [[https://coq.inria.fr/doc/V8.20.0/refman/language/coq-library.html#|corresponding section of the reference manual]] * [[https://github.com/coq/coq/wiki/The-Coq-FAQ|Coq FAQ]] * [[https://www.labri.fr/perso/casteran/CoqArt/|Coq'Art]], by Yvers Bertot and Pierre Castéran (resources available in french and english) * [[https://softwarefoundations.cis.upenn.edu/|Software foundations]], Pierce et al. ==== General Bibliography ==== * Basic Proof-Theory, by Schwichtenberg and Troelstra * Domains and Lambda-calculi, by Roberto Amadio and Pierre-Louis Currie * Lambda-calculus, types and models, by Jean-Louis Krivine * Practical Foundations for Programming Languages, by Bob Harper * Proof-Theory and Logical Complexity, by Jean-Yves Girard