Coqito ergo sum

Ou chercher la vérité dans le formalisme...

Piste rouge 8 décembre 2014  - Ecrit par  Aurélien Alvarez Voir les commentaires (4)

On se souvient de la célèbre formule de Descartes, Cogito ergo sum, première certitude résistant à un doute méthodique, et donc point de départ de fondements indiscutables dans le but de reconstruire entièrement la connaissance [1]. La philosophie de cet article sera quant à elle celle du Coqito ergo sum :-).

On lira ou relira avec plaisir le célèbre Discours de la méthode (Pour bien conduire sa raison, et chercher la vérité dans les sciences) qui s’ouvre avec cette très belle première phrase :

Le bon sens est la chose du monde la mieux partagée ; car chacun pense en être si bien pourvu, que ceux même qui sont les plus difficiles à contenter en toute autre chose n’ont point coutume d’en désirer plus qu’ils en ont.

Il y a un an et demi de cela, Le Monde.fr a proposé une série d’énigmes mathématiques dans ses colonnes. C’était à l’occasion du lancement de la collection Le monde est mathématique, d’ailleurs parrainée par Images des maths. À l’époque j’avais proposé l’énigme suivante qui, d’une certaine façon, se résout par le seul bon sens... Juste après la vidéo une version écrite de l’énigme : il n’est donc pas obligatoire de regarder la vidéo pour lire la suite de ce texte ;-).

L’énigme des chapeaux

Une urne contient cinq chapeaux : trois noirs et deux blancs. Par ailleurs, trois personnages, Albert, Marie et Sophie tirent chacun et chacune un chapeau et se le mettent sur la tête. Le hasard a fait qu’ils ont tiré les trois chapeaux noirs ; il ne reste donc dans l’urne que les chapeaux blancs, mais ça, nos personnages ne le savent pas. On leur demande de deviner la couleur de leur chapeau.

  • Après réflexion, Albert dit : « Je ne sais pas ».
  • Marie réfléchit à son tour et dit : « Je ne sais pas non plus ».
  • Sophie s’exclame alors : « Je sais, j’ai un chapeau noir sur la tête ».
    Pourquoi ? Comment Sophie fait-elle pour être si sûre d’elle ? Peut-on comprendre son raisonnement ? [2]

La semaine suivante, était publiée en ligne une solution à l’énigme que vous pouvez retrouver sur la vidéo suivante. Mais pas si vite ! Il faut bien sûr que vous preniez le temps de réfléchir tranquillement à l’énigme. Revenez lire la suite de cet article demain si besoin. Entre temps, n’hésitez pas à vous plonger dans Une petite histoire pas très sérieuse de deux très sérieuses logiques de Guillaume Cano : peu probable que ça vous aide mais c’est l’occasion d’apprendre que différentes logiques sont possibles et utilisées par les mathématiciens. Et que du coup certains énoncés sont des théorèmes pour les uns mais pas forcément pour tous. Eh oui !

L’histoire aurait pu s’arrêter là. Mais quelques semaines plus tard, je recevais un email inattendu.

Bonjour,

Par ce petit email, je tiens à vous féliciter pour votre série sur les énigmes mathématiques. C’est vraiment super !

Je vous suis chaque semaine avec très grand plaisir en essayant d’entrer (pour l’instant avec succès ;-)) vos différents problèmes dans l’assistant de preuve Coq (celui de Feit-Thompson) :

http://www-sop.inria.fr/marelle/Laurent.Thery/LeMonde/

Encore bravo !

Laurent Théry - INRIA Sophia Antipolis

Un collègue de l’INRIA venait donc de formaliser l’énigme des chapeaux et d’en certifier une démonstration grâce à l’assistant de preuves Coq. Les lecteurs d’Images des maths ont déjà entendu parler à plusieurs reprises de démonstrations formelles et de Coq dans les articles suivants notamment :

Si le sujet vous passionne, pensez également à aller faire un tour sur Interstices, l’analogue d’Images des maths pour l’informatique en quelque sorte. En particulier, je peux recommander l’article Du rêve à la réalité des preuves de Jean-Paul Delahaye.

Récemment a même eu lieu un trimestre IHP sur la thématique Sémantique des preuves et des programmes et mathématiques certifiées, comme nous le rappelle Pierre Pansu dans son article La sémantique, c’est romantique. Certains exposés du trimestre sont disponibles en ligne sur la chaîne YouTube de l’IHP. Attention, c’est pour les experts. Pour une vidéo très très légèrement plus accessible (mais ça reste pour les personnes très très très très motivées !), il y a également l’exposé de Thierry Coquand au séminaire Bourbaki de juin dernier.

Une démonstration formelle de l’énigme

Piqué par la curiosité, j’installais donc Coq sur mon ordinateur. Le problème auquel on se confronte rapidement, c’est qu’il ne suffit pas d’avoir le permis de conduire pour pouvoir se mettre au volant d’une formule 1 ! En particulier, ne serait-ce que faire ses premiers pas est hautement non trivial :-(. Dans la suite de cet article, je propose un raisonnement pour résoudre l’énigme, ainsi qu’une formalisation et une certification par Coq de ce dernier. Chaque étape du raisonnement sera donc suivie de sa version formalisée : les plus curieux pourront lire les preuves des énoncés en dépliant les blocs Proof. Bien sûr, ce qui suit n’est pas un tutoriel d’introduction à Coq, loin de là… de toute façon je sais tout juste passer la première vitesse de ce type de formule 1... et encore bien souvent je cale et suis obligé de m’y prendre à deux fois ;-).

D’une certaine façon, ce que j’aimerais faire ici sur cet exemple très très simple de l’énigme des chapeaux (et donc à des années-lumières du travail qui vient d’être accompli pour certifier la démonstration du théorème de Feit-Thompson), c’est essayer de faire ce qu’écrivent dans leur introduction les auteurs du livre Homotopy type theory dont il est question dans l’article À la croisée des fondements des mathématiques, de l’informatique et de la topologie que je mentionnais ci-dessus :

One can imagine a not-too-distant future when it will be possible for mathematicians to verify the correctness of their own papers by working within the system of univalent foundations, formalized in a proof assistant, and that doing so will become as natural as typesetting their own papers in TEX. In principle, this could be equally true for any other foundational system, but we believe it to be more practically attainable using univalent foundations, as witnessed by the present work and its formal counterpart. [3]

Quelques mots sur l’assistant de preuve Coq

PNG - 78.2 ko

La langue vernaculaire de Coq est le langage Gallina. C’est donc via ce langage que nous pouvons interagir avec l’assistant de preuve. Ce dernier se fonde sur le calcul des constructions, une théorie des types d’ordre supérieur, et son langage de spécification est donc une forme de lambda-calcul typé. À ce propos, un très bel article à propos du calcul est celui de Jean-Louis Giavitto sur Interstices : Le calcul, une notion difficile à attraper. Mais revenons à ce qu’il est possible de faire avec Coq, à savoir :

  • manipuler des assertions du calcul ;
  • vérifier mécaniquement des preuves de ces assertions ;
  • aider à la recherche de preuves formelles ;
  • synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.

Si vous avez ouvert le bloc précédent, vous avez pu être effrayé par tout ce charabia. C’est normal, il y a de quoi ! Mais la bonne nouvelle, c’est qu’il est inutile de comprendre tout cela pour lire la suite de cet article, bien au contraire. Nous allons faire connaissance avec le langage Gallina en douceur, d’autant que la plupart des mots de ce langage sont assez transparents : Goal, Lemma, Theorem, Proof, Hypothesis, Set, forall.... Les symboles utilisés \/, /\, ->, <-> sont également suffisamment transparents pour qu’on puisse reconnaître ou, et, implique, équivalent. Bref, ne partez pas trop vite, il y a certes un petit effort à faire mais ça en vaut vraiment la peine. Pour celles et ceux qui souhaiteraient suivre le détail des preuves et donc en savoir plus sur les tactiques utilisées, voici déjà un petit guide de survie en Coq par Alexandre Miquel, l’étape suivante étant de se plonger dans le manuel de référence...

Quelques définitions pour commencer

Nous définissons d’abord un ensemble pour que nos chapeaux puissent avoir une couleur noire ou blanche, ainsi qu’une configuration correspondant à un tirage de chapeaux.

Inductive couleurChapeau : Set := blanc | noir.

Inductive configuration : Set := config : couleurChapeau -> couleurChapeau -> couleurChapeau -> configuration.

Puis trois fonctions qui chacune, à une configuration donnée, renvoie la couleur du chapeau du personnage correspondant.

Definition chapeauAlbert : configuration -> couleurChapeau := fun c => match c with config couleur _ _ => couleur end.

Definition chapeauMarie : configuration -> couleurChapeau := fun c => match c with config _ couleur _ => couleur end.

Definition chapeauSophie : configuration -> couleurChapeau := fun c => match c with config _ _ couleur => couleur end.

Pour tout tirage, l’un des chapeaux tirés est forcément noir puisqu’il n’y a que deux chapeaux blancs et que nous avons trois personnages. D’où l’hypothèse générale que nous faisons pour toute configuration de chapeaux. [4]

Hypothesis configurationValide : forall c : configuration, chapeauAlbert c = noir \/ chapeauMarie c = noir \/ chapeauSophie c = noir.

Nous sommes désormais prêts à attaquer notre problème.

Quelques lemmes pour s’échauffer

Rappel aux malheureux qui projettent d’ouvrir les blocs dépliants des preuves ci-dessous et qui souhaitent malgré tout survivre : petit guide de survie en Coq par Alexandre Miquel.

Un chapeau a forcément une couleur, en l’occurrence noire ou blanche.

Goal forall couleur : couleurChapeau, (couleur = noir) \/ (couleur = blanc).

Proof.

intro c. destruct c. right. reflexivity. left. reflexivity.

Qed.

Si un chapeau n’est pas de couleur blanche, c’est qu’il est de couleur noire. Et réciproquement : s’il est de couleur noire, c’est qu’il n’est pas de couleur blanche !

Lemma nonBlancEstNoir : forall couleur : couleurChapeau, (couleur <> blanc) <-> (couleur = noir).

Proof.

intro c. split.

  • intro H. destruct c. destruct H. reflexivity. reflexivity.
  • intro H. destruct c. discriminate H. discriminate.

Qed.

Nous en déduisons qu’un chapeau ne pourra donc jamais être noir et blanc en même temps...

Lemma noirOUblanc : forall c : couleurChapeau, c = noir /\ c = blanc -> False.

Proof.

intros c H. destruct H as [H1 H2]. apply (nonBlancEstNoir c). exact H1. exact H2.

Qed.

À ce stade, nous avons démontré que tout chapeau a une couleur, que cette couleur est noire ou blanche, et qu’elle ne peut pas être noire et blanche en même temps.

Essayons de comprendre comment Sophie a réussi à deviner la couleur de son chapeau

Puisque les chapeaux de Marie et Sophie ont forcément une couleur qui peut-être noire ou blanche d’après ce que nous venons de voir, Albert se retrouve donc face à l’une des quatre éventualités suivantes :

  • cas 1 : Marie a un chapeau blanc et Sophie a un chapeau blanc
  • cas 2 : Marie a un chapeau noir et Sophie a un chapeau blanc
  • cas 3 : Marie a un chapeau blanc et Sophie a un chapeau noir
  • cas 4 : Marie a un chapeau noir et Sophie a un chapeau noir

Nous allons voir maintenant que le cas 1 est exclu. Pour cela, montrons que si le chapeau de Marie est blanc, en même temps que celui de Sophie est blanc également, alors celui d’Albert ne peut être que noir.

Lemma AlbertSait : forall c : configuration, chapeauMarie c = blanc /\ chapeauSophie c = blanc -> chapeauAlbert c = noir.

Proof.

intros c H. destruct H as [H1, H2]. destruct (configurationValide c). exact H. destruct H. destruct (noirOUblanc (chapeauMarie c)). apply (conj H H1). destruct (noirOUblanc (chapeauSophie c)). apply (conj H H2).

Qed.

Puisqu’Albert est indécis, c’est qu’il n’est pas en mesure d’appliquer le lemme précédent. Autrement dit, Albert (qui a une très bonne vue !) ne dispose pas d’une preuve que le chapeau de Marie est blanc en même temps que celui de Sophie est blanc également. Sinon, en posant

  • P = chapeauMarie c = blanc /\ chapeauSophie c = blanc
  • Q = chapeauAlbert c = noir
    Albert aurait appliqué le célèbre modus ponens pour en déduire que son chapeau était noir :

Lemma modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.

Proof.

intros P Q p pq. apply pq. exact p.

Qed.

Le cas 1 « Marie a un chapeau blanc et Sophie a un chapeau blanc » est donc exclu. Dans les trois autres cas, l’un des deux personnages féminins au moins a un chapeau noir. Nous dirons donc qu’Albert est indécis dès que Marie ou Sophie (ou les deux) porte un chapeau noir.

Definition AlbertIndecis (c : configuration) : Prop := chapeauMarie c = noir \/ chapeauSophie c = noir.

Montrons désormais que si Albert est indécis et que le chapeau de Sophie est blanc, alors le chapeau de Marie est forcément noir.

Lemma MarieSait : forall c : configuration, (AlbertIndecis c) /\ (chapeauSophie c = blanc) -> chapeauMarie c = noir.

Proof.

intros c H. destruct H as [H1, H2]. destruct H1. exact H. destruct (noirOUblanc (chapeauSophie c)). apply (conj H H2).

Qed.

Même raisonnement que pour Albert, si Marie n’est pas en mesure d’appliquer le lemme précédent et donc de deviner la couleur de son propre chapeau, c’est qu’elle ne dispose pas à la fois d’une preuve qu’Albert est indécis et d’une preuve que Sophie a un chapeau blanc. Or Marie (qui n’est pas sourde !) sait qu’Albert est indécis puisque ce dernier l’a dit haut et fort. C’est donc que Marie ne sait pas que le chapeau de Sophie est blanc. Mais Marie a elle aussi une très bonne vue et voit bien la couleur du chapeau de Sophie : puisque cette couleur est ou bien noire, ou bien blanche comme nous l’avons vu dans nos lemmes d’échauffement, c’est donc que le chapeau de Sophie est noir.

Definition MarieIndecise (c : configuration) : Prop := chapeauSophie c = noir.

La conclusion est très facile. Dès lors que Marie est indécise, Sophie est capable d’en déduire la couleur noire de son chapeau et n’a d’ailleurs nul besoin de voir ses deux camarades.

Theorem SophieTrouve : forall c : configuration, MarieIndecise c -> chapeauSophie c = noir.

Proof.

trivial.

Qed.

Et voilà, le tour est joué ! J’espère que les lecteurs d’Images des maths qui sont arrivés jusqu’ici et que je n’ai pas réussi à faire fuir relèveront le défi d’essayer de formaliser et certifier à leur tour les démonstrations de leurs théorèmes préférés :-).

Post-scriptum :

Merci aux relecteurs, en particulier à Sylvain Courte et surtout à Guillaume Pontier qui a pris soin de vérifier qu’il ne trainait pas de coquilles dans les preuves proposées en Coq.

Article édité par Patrick Popescu-Pampu

Notes

[1Je renvoie vers les spécialistes de Descartes pour une bonne compréhension de la formule latine Cogito ergo sum, en particulier l’interprétation du donc qui est plus subtile qu’il n’y paraît et ne témoigne pas d’un lien de cause à conséquence.

[2C’est une remarque mais on pourrait même supposer que Sophie est aveugle ! Il lui suffit de savoir qu’Albert puis Marie sont indécis pour en conclure que son chapeau est noir.

[3« On peut imaginer que dans un avenir relativement proche, il deviendra possible pour les mathématiciens de formaliser et de certifier leurs propres démonstrations en s’appuyant sur les fondements univalents, et en utilisant un assistant de preuves de manière tout aussi naturelle qu’ils utilisent TeX pour écrire leurs articles aujourd’hui. En principe, ce devrait être possible pour tout système de formalisation des mathématiques mais nous pensons que les fondements univalents se prêtent mieux à cette approche, comme nous tâchons de le montrer tout au long de ce livre. »

[4Ceux qui pratiquent le doute hyperbolique pourront toujours s’amuser à démontrer que

2 < 3 !

Pour cela, nous proposons d’utiliser la bibliothèque d’arithmétique, le petit guide de survie en Coq ne nous suffisant plus pour l’occasion...

Require Import Arith.

Goal 2 < 3.

Proof.

apply le_lt_n_Sm. apply le_n.

Qed.

Partager cet article

Pour citer cet article :

Aurélien Alvarez — «Coqito ergo sum» — Images des Mathématiques, CNRS, 2014

Commentaire sur l'article

  • Coqito ergo sum

    le 8 décembre 2014 à 20:37, par Creux

    N’ayant pas les connaissances suffisantes pour apprécier à sa juste valeur votre article, je me contenterai de signaler que les « crédits images » sont actuellement vides mais que le dessin du coq me fait fortement penser au style d’Albert Uderzo.

    Répondre à ce message
    • Coqito ergo sum

      le 9 décembre 2014 à 00:51, par Aurélien Alvarez

      L’image du Coq est l’une des toutes premières proposées par Google Images. Elle provient de ce blog mais je ne saurai en dire plus...

      http://www.blogaf.org/2011/04/l´embleme-de-la-france-le-coq-pourquoi/

      Cordialement, Aurélien Alvarez.

      Répondre à ce message
      • Coqito ergo sum

        le 9 décembre 2014 à 21:22, par Jean-Paul Allouche

        Bonsoir

        Si on insère le dessin de ce coq dans la fenêtre de recherche d’images de Google, on trouve énormément de sites qui le reprennent. Mais il semble bien en effet que l’original soit Chanteclairix (le coq gaulois dans Astérix), voir par exemple ici.

        Répondre à ce message
        • Coqito ergo sum

          le 9 décembre 2014 à 21:59, par Aurélien Alvarez

          D’accord et merci pour cet éclairage. Si en plus c’est un coq gaulois, ça nous fait une raison de plus de chanter cocorico :-).

          Répondre à ce message

Laisser un commentaire

Forum sur abonnement

Pour participer à ce forum, vous devez vous enregistrer au préalable. Merci d’indiquer ci-dessous l’identifiant personnel qui vous a été fourni. Si vous n’êtes pas enregistré, vous devez vous inscrire.

Connexions’inscriremot de passe oublié ?

Suivre IDM