English version of this page at the bottom

Preuves assistées par ordinateur à l'aide de Coq

Il est prévu que ce cours soit donné deux fois, en français puis en anglais. Les notes de cours seront fournies sur cette page dès qu'elle seront prêtes. Les élèves intéressés pourront également bénéficier d'un cours vidéo qui couvre pratiquement tout le contenu du cours.

présentation introductive du cours

1. programmation élémentaire

Il s'agit d'apprendre à écrire des programmes simples. Les notes de cours sont disponibles ici.

2. formules logiques et preuves élémentaires

Il s'agit d'apprendre à décrire les propriétés attendues des programmes et à faire des preuves simples. Les notes de cours sont disponibles ici.

3. Prouver des propriétés de programmes

Il s'agit d'apprendre à décrire les propriétés attendues des programmes et à faire des preuves simples. Les notes de cours sont disponibles ici.

4. Preuves sur les programmes arithmétiques

Il s'agit de mieux connaître les types de nombres utilisés en Coq et les outils de preuve automatique associés. Les notes de cours sont disponibles ici.

5. Types de données généraux

Il s'agit de voir d'autres types de données et de comprendre comment les techniques de preuves par récurrence s'adaptent. Les notes de cours sont disponibles ici.

Computer assisted proof

This course consists of 12 hours of lectures, 9 hours of laboratory sessions and home projects. Courses notes (with exercises) will be added to this page as soon as they become ready.

introductory presentation

1. basic programming

The aim of the first lesson is to acquire basic programming skills. Course notes for this first lesson are available here. The associated laboratory session will use the exercises given in the course notes.

Between courses, you are expected to read the course notes completely, to do all the exercises, to come up with your own examples and to write your own programs.

For the students that are excited by the subject, here are two elaborate examples that can be studied in a personal project. This kind of work will not be corrected, but I am open to discuss the subject by mail.

1. Natural numbers are badly suited to describe large numbers, but lists of digits, where digits are natural numbers smaller than 10, can be used to represent very large numbers. When working on such a representation, it is clever to have lists where the first element is the low weight digit. For instance, 239 would be represented by the list (9::3::2::nil). You should be able to write functions to compute :
   • the addition of two representations
   • the product of two representations
   • the comparison of two representations
   • the subtraction of two representations
   • whether a list of numbers is legitimate, in the sense that all numbers are digits (numbers smaller than ten)
2. matrices can be described as lists of lists (representing lists of rows). A common trick is to consider that rows that are too short actually correspond to rows that should be completed with zeros. Similarly, a matrix with too few rows corresponds to a matrix where rows containing only zeros are added. You should be able to write functions to compute
   • the addition of two matrices
   • the transposition of a matrix
   • the scalar product of two vectors
   • the product of two vectors
   • whether a list of lists really is rectangular (all rows have the same length)

For the second lesson we learn how to write logical formulas and how to make simple proofs manipulating the basic logical connectives. Course notes are available here.

Third lesson: reasoning about recursive functions

Recursive functions are the most powerful computing tools in the functional programming language of the Coq system. Reasoning about them is important. Course notes are available here.

Fourth lesson: Proofs in arithmetic

In these course notes, we see new datatypes to represent numbers, with more efficiency in the operations. More advice about proofs by induction is also provided. These course notes are available here.

Fifth lesson: General datatypes

In these course notes, we observe how new datatypes can be defined by the programmer and how one reasons about these datatypes. These course notes are available here.

Projects

Sorting

Write a function sorted that recognizes when a list is sorted, and returns a boolean value.

write functions that sorts a list and then prove that the result is sorted

1. Insertion sort: when sorting a list with more than one element, you should sort the tail of the list and insert the first element at the right position in the sorted tail. Write separately the function insert and sort following this plan. Then prove that for any l and a, if sorted l is true then sorted (insert a l) is also true. Then use this lemma to prove that for any l, sorted (sort l) is true. Also, prove that the length of a list is preserved when sorting it.
2. Use binary trees with natural numbers on the binary nodes as given by the following datatype.

      Inductive bin := N (x : nat)(t1 t2 : bin) | L.
     

   write a function that recognizes when a tree is sorted, that is, all values in t1 are smaller than x, which is smaller than all values in t2. Write a function that inserts a value in a tree, in such a way that if the input tree is sorted then the output is also sorte, write a function that takes as input a sorted tree and outputs a sorted list. Prove all of them correct.

Decimal arithmetic

Reuse the list of digits datatype given in the elaborate examples of the first session.

1. define a function mapping any list of digits to the natural number it represents.
2. Prove that your implementation of addition is correct, when the inputs are legitimate (that is when the inputs lists only contain numbers smaller than 10).
3. Prove that your implementation of addition returnts a legitimate output.
4. product
5. comparison
6. subtraction
7. division. As a remainder, here is a description of the algorithm: for a number of the form 10 * x + d divided by y first divide x by y, obtaining a quotient q and a remainder r. Find the digit u(number smaller than 10) so that u * y ≤ 10 * r + d and 10 * r + d < (u + 1) * y. The resulting quotient should be 10 * q + u and the remainder should be computed accordingly. You should develop an implementation of the algorithm along this pattern, where all variables x, y, q, and r should be legitimate lists of natural numbers. The result should be a pair of legitimate lists. Then you should be able to prove that your algorithm is correct.
8. Can you continue this exercise to defining a function that computes correctly the first n decimals of the π number? For instance, start writing a function that returns n digits of any number 1/k. The Coq libraries contains descriptions of the atan function.