Aperçu d'un assistant de preuve

Publié le vendredi 3 août 2018

Pour illustrer un aspect de la recherche en "méthodes formelles", voici un petit aperçu de mon outil de travail actuel : l'assistant de preuve Coq.

L'idée est d'écrire et de démontrer des théorèmes (comme le théorème de Pythagore ou le théorème d'Euclide sur les nombres premiers) dans un langage dédié, qui peuvent être ensuite vérifiés automatiquement.

Cette technologie n’est pas toute jeune : Coq est né en 1984 d’après Wikipedia, et il existe d’autres assistants de preuve et logiciels d’espèces similaires tels que Isabelle et Lean, pour en citer deux.

Le développement et le bon usage de ces outils sont néanmoins toujours des sujets de recherche actifs.1 Dans un futur lointain un assistant de preuve pourrait servir dans l’apprentissage des mathématiquess et peut-être même des autres matières scientifiques.

Coq est un langage

On utilise le nom “Coq” pour désigner à la fois:

  • l’assistant de preuve, un logiciel qui sert non seulement à vérifier automatiquement des preuves, mais contient aussi un environnement interactif pour faciliter leur rédaction (ce qui en fait bien un “assistant”) ;

  • le langage compris par cet outil.

Tout comme au collège ou au lycée on rédige des démonstrations en français, ici on les rédige “en Coq”. C’est un langage spécialisé pour les démonstrations, un moyen efficace d’échanger des preuves avec d’autres utilisateurs, et de vérifier ces preuves automatiquement grâce aux règles extrêmement précises suivies par le langage.

Exemple de théorème

Commençons directement avec un exemple de théorème en Coq. Dans ce billet, nous ne nous concentrerons pas sur le sens de ce théorème en particulier, mais il y a déjà pas mal de choses à dire en général sur le principe de l’écrire en Coq.

Theorem l'addition_est_associative :
  forall a b c, (a + b) + c = a + (b + c).
Proof.
  induction a.
  - reflexivity.
  - intros b c. simpl. rewrite IHa. reflexivity.
Qed.

Expliquons progressivement ce que vous voyez là. Voici à nouveau la première ligne.

Theorem l'addition_est_associative :

Elle déclare un théorème, et lui donne un nom, l'addition_est_associative, afin de pouvoir s’y référer plus tard. Le nom lui-même n’a pas d’importance, le théorème pourrait très bien s’appeller Bob, mais en pratique on préférera des noms plus descriptifs, abrégés et en anglais pour faire pro.

Un théorème, c’est un énoncé ayant une démonstration, ou preuve. Dans ce morceau, l’énoncé est donné après les deux points, sur la deuxième ligne.

  forall a b c, (a + b) + c = a + (b + c).

En anglais, “for all” (en deux mots) signifie “pour tout”. Le langage Coq emprunte cette expression de l’anglais et l’abrège en un seul mot forall, car c’est plus court.

Nous pouvons traduire ces deux premières lignes en français directement, en une phrase qui aurait l’air tout à fait anodin dans un cours d’algèbre ou de logique :

Théorème. L’addition est associative : pour tous entiers naturels a, b et c, la somme (a + b) + c est égale à la somme a + (b + c).

Ensuite vient la preuve, trois lignes encadrées par les mots Proof (“Preuve” en anglais) et Qed (“CQFD” en latin).

Proof.
  induction a.
  - reflexivity.
  - intros b c. simpl. rewrite IHa. reflexivity.
Qed.

C’est une preuve de trois lignes, mais paradoxalement son explication prendrait des pages2, alors nous ne la ferons pas ici.

Vérification automatique

De votre point de vue, le théorème l'addition_est_associative est plutôt un postulat, car vous me croyez sur parole que ma preuve est correcte.

Si elle était écrite en français, le seul moyen de la vérifier serait de la lire ou faire lire à quelqu’un de confiance et d’espérer que nous n’allons pas rater une erreur s’il y en a. Mais comme elle est écrite en Coq, il n’est pas nécessaire d’avoir l’expertise et le temps pour cela, ni d’accorder aveuglément confiance à ma parole. Nous pouvons demander à notre fidèle assistant Coq de la vérifier, ce qu’il fait automatiquement en appliquant des règles logiques simples sans broncher.

Le processus est hautement plus rapide que de faire lire la preuve à quelqu’un. En fait, il n’est même pas nécessaire pour quiconque de comprendre la preuve (seulement l’énoncé du théorème, puisqu’il faut a priori savoir ce que nous cherchons à prouver). Vous misez sur l’absence d’erreur dans Coq, qui est un système plutôt bien testé avec quelques milliers d’utilisateurs. Bien sûr, des erreurs peuvent exister en pratique, mais puisque Coq est un programme, elles peuvent être corrigées une fois pour toutes et n’apparaissent que dans des cas très particuliers (sinon on les aurait trouvées et corrigées avant).

Voici ce à quoi ça ressemble. On communique avec Coq via trois fenêtres dans l’image ci-dessous. Dans la fenêtre de gauche on écrit du code, c’est-à-dire théorèmes, preuves, ainsi que toutes sortes de commandes dans le langage Coq. Dans les deux fenêtres de droite on lit les réponses de Coq.

Cliquez sur l'image pour l'agrandir.

Nous pouvons donc copier le bout de code ci-dessus dans la fenêtre de gauche, et le soumettre à Coq avec une commande.

Cliquez sur l'image pour l'agrandir.

Notre code se surligne en bleu et Coq répond l'addition_est_associative is defined, qui est sa manière de nous annoncer que notre preuve est correcte.

Que se passe-t-il si la preuve n’est pas correcte? Voici un faux théorème: 1 = 0, avec une preuve quelconque (auto.) qui ne peut qu’être mauvaise.

Cliquez sur l'image pour l'agrandir.

Demandons à Coq de la vérifier…

Cliquez sur l'image pour l'agrandir.

Le surlignage ne va pas tout en bas (il s’arrête avant Qed) et nous recevons un message d’erreur à droite. Coq a rejeté notre preuve, à raison.

Programmer en Coq

Le langage Coq n’est pas seulement un langage pour faire des mathématiques. C’est aussi un langage de programmation, avec lequel on peut construire des logiciels, comme le navigateur dans lequel vous lisez ce billet. Votre navigateur est très certainement écrit dans des langages de programmation différents (et plus adaptés), peut-être C++ ou Java. Mais si vous utilisez Google Chrome, il contient depuis peu un morceau écrit en Coq!3 Il fait partie du mécanisme derrière le cadenas vert dans votre barre d’adresse, qui garantit que la page que vous lisez provient bien du site indiqué.4

L’intérêt de programmer en Coq, c’est qu’on peut ensuite prouver des théorèmes à propos de nos programmes, et s’assurer mathématiquement qu’ils ne contiennent pas d’erreurs : ils ne se plantent pas et donnent les résultats attendus. C’est la raison principale pour laquelle je travaille avec Coq dans ma recherche.

Dans un futur billet, nous étudierons de plus près le théorème présenté ici et nous nous en servirons dans une autre preuve suffisament simple à expliquer.


Commentaires et questions

Question d’Adrien Fabre:

Comment un théorème est uploadé, et est-ce qu’on peut utiliser n’importe quel théorème uploadé ou ça fonctionne par bibliothèques ?

Lorsqu’on a démontré des théorèmes qui peuvent s’avérer utiles à d’autres, on souhaiterait les partager. Il suffit pour cela de mettre en ligne nos travaux écrits en Coq (qui sont de simples fichiers), que d’autres utilisateurs peuvent télécharger et inclure dans leurs projets. Les moyens de distribution possibles sont variés. Dans l’absolu rien n’empêche d’utiliser Google Drive, DropBox, ou de s’envoyer des pièces jointes par courriel, mais en pratique on préférera des dépôts spécialisés permettant de mieux garder trace des mises à jour, comme Github ou Gitlab. Ensuite, on peut se faire connaître sur les réseaux sociaux, les listes de diffusion, les journaux et conférences scientifiques.

Par exemple, le code de l’assistant de preuve Coq lui-même se trouve sur Github, et inclut d’ailleurs le théorème de ce billet, avec une preuve différente.

À propos du mot “bibliothèque”

Plutôt que des théorèmes individuels, il est plus utile de construire des théories, des ensembles de définitions et théorèmes, et plus simplement d’idées, permettant de raisonner et de travailler avec une classe particulière d’objets. Par exemple : théorie des nombres, théorie des ensembles. C’est par ailleurs un principe commun à toutes les sciences. De manière similaire, les projets logiciels s’organisent en unités appelées bibliothèques (“libraries” en anglais).

Quand on parle de Coq, qui a trait en même temps aux mathématiques et au dévelopement logiciel, les deux termes “théorie” et “bibliothèque” ont du sens. Ils ne sont pas tout à fait équivalents : une bibliothèque est définie par son code source, mais une théorie n’est pas une chose qu’on délimite par un critère objectif. Si dans beaucoup de cas une théorie correspond plus ou moins à une bibliothèque, une théorie de grande envergure peut aussi occuper plusieurs bibliothèques, et une bibliothèque peut rassembler plusieurs théories plus ou moins liées.


  1. Sur ce blog, je passe plein de détails sous le tapis (puisque c’est de la vulgarisation). Il y a beaucoup de choses à apprendre avant de pouvoir essayer ces outils vous-mêmes. Mais le but ici est de montrer que l’informatique n’est pas de la magie noire, car derrière ces obstacles se cachent des concepts au final tout à fait simples.

  2. Il faudrait définir les entiers naturels à partir de principes fondamentaux, sur lesquels des livres entiers ont été écrits (par exemple, Principia Mathematica).

  3. Par des chercheurs du MIT, dont voici leur article scientifique à ce sujet : Simple High-Level Code For Cryptographic Arithmetic – With Proofs, Without Compromises, A. Erbsen et al., 2019. Notez que la conférence est dans le futur. Nous avons effectivement affaire à de la technologie de pointe.

  4. Faites quand même attention que le site que vous voyez dans la barre d’adresse est bien celui sur lequel vous pensez être: de nombreuses arnaques essaient de vous avoir sur un site mal épelé intentionellement. Évitez de faire vos achats sur nanazon.fr ou d’accéder à votre boite à courriel sur gmeil.fr. Fin de la minute cybersécurité.