Computer-assisted proofs (preuves sur ordinateur)

This is the webpage for the tutorials of the course computer-assisted proofs by Colin Riba.

TDs

Each file for the tutorials will appear here when needed.

td1.pdf: λ-calculus and encodings of data types (french: td1fr.pdf, solutions: td1frsol.pdf)
td2.pdf: Propositional Curry-Howard (solution of 1: td2-ex1-cor.v)
tp3.v or tp3.html: Curry-Howard and induction in Heyting arithmetic
tp4.v or tp4.html: Automatic tactics and integer division (solution: tp4cor.v)
tp5.v or tp5.html: Dependent pattern matching and accessibility
tp6.v or tp6.html: Accessibility, induction in HA again, pigeons
tp7.v or tp7.html: Proofs by reflection
td8.pdf: Codage des types de données dans système F (correction : td8cor.pdf)
td9.pdf: Calcul des séquents (correction : td9cor.pdf)
td10.pdf: Réversibilités dans LK₀

DM1

Le DM1 est à rendre pour le 8 octobre. Vous pouvez choisir l'un des deux sujets et vous mettre en binôme.

Sujet 1 : preuve de réduction du sujet
Exercice 3 du TD 2, à rédiger sur papier en détaillant toutes les étapes.
Sujet 2 : théorème de Glivenko en coq
Formalisez toutes les règles de NJ et NK, et prouvez le théorème de Glivenko (cf TD 2). Suivez le schéma du fichier td2-dm.v.

DM2

Sujet : dm2.pdf. Il est à faire sur papier en binôme et à rendre à Colin le 23 octobre. Les définitions sont sur sa page.

DM3

Le DM3 est à rendre pour le 12 novembre avant le TP. C'est principalement la suite du TP 6, donc vous pouvez reprendre ce que vous avez déjà fait. Il y a une partie sur la division entière qui est en bonus qui n'était pas dans le TP 6. J'ai laissé la correction de certaines preuves déjà faites. Les fichiers : dm3.v (et pour lire : dm3.html).

DM4

Le DM4 est à rendre pour le 20 décembre 2013 à 23h45, il est à faire par binôme, avec un sujet au choix parmi les deux ci-dessous :

Théorème de Ramsey infini : preuve usuelle et preuve formalisée en Coq. Énoncé : ramsey.pdf, fichier Coq : ramsey.v.
Paradoxe de Girard/Hurkens. Énoncé et fichier Coq : hurkens.v.