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

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