English version of this page at the bottom

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

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

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.

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.

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.

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.

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.

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.

- 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)

- 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.

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.

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.

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.

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

- 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`is true then*l*`sorted (insert`is also true. Then use this lemma to prove that for any*a**l*)*l*,`sorted (sort`is true. Also, prove that the length of a list is preserved when sorting it.*l*) - 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.

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

- define a function mapping any list of digits to the natural number it represents.
- 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).
- Prove that your implementation of addition returnts a legitimate output.
- product
- comparison
- subtraction
- 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. - 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.

Last modified: Wed Nov 28 13:38:05 CET 2012