X-UPS Days 2026: "Formal Verification of Proofs" – Micaela Mayero 1

bien de rejoindre l'équipe parce que je vais dû passer la main dans peu de temps mais bon je pense que je serai encore là l'année prochaine. Voilà. Et la première ce matin est Mikael Maero de l'université alors perdu moi Sorbon Paris Nord et qui va nous parler des assistants de preuve pour l'analyse réelle et numérique un focus sur rock et de la recherche à l'enseignement. Voilà, je laisse la parole à Mika. Bonjour, ça va? assez je parle assez fort, c'est bon, le micro fonctionne. D'accord. Euh donc aujourd'hui, je vais pas forcément parler, je vais pas du tout parler de réel d'ailleurs ni d'analyse. Ce sera pour demain. Aujourd'hui, je vais faire une présentation à une introduction à tout ce qui est preuve formelle euh avec un petit panel historique parce que d'après ce que j'ai compris, vous êtes Mattheux. Voilà. Euh donc euh la logique, je sais pas à quel point euh vous êtes familier avec la logique. Euh avec l'informatique peut-être encore moins. Enfin pas la pas l'informatique de tous les jours hein, je parle euh l'informatique fondamentale. Donc je vais faire un petit un petit panel d'introduction pour arriver jusqu'aux assistants de preuve euh en partant de la logique d'emprera plus dans le vif du sujet qui est l'analyse réelle. euh et l'analyse numérique qui est une partie compliquée, un peu particulière des assistants de preuve. Euh donc on va faire un petit peu d'histoire de la logique à l'informatique en passant par les maths. Après on on focusera sur rock. Alors des assistants de preuve, je sais pas si vous connaissez un peu les mots clés des assistants de preuve. Il y en a plein. Euh je vais en citer quelques-uns. On va voir aussi à quoi ça sert, comment on peut les utiliser. Euh et à la fin, il y aura une démo et puis je vous demanderai vers le vers le milieu, je vous demanderai un peu votre avis euh ce que vous préférez qu'on fasse euh ou pas. Euh donc alors la logique euh alors ça c'est des c'est des c'est une présentation que je fais un peu dans les lycée parce que souvent les élèves ou même les étudiants, ils n'ont pas la notion pour eux quand on est quand on est né en avant 2000, on on date déjà beaucoup, on est déjà très vieux. Donc ils ont du mal à ils ont du mal à se placer euh dans le dans le temps. Et donc les au niveau puisqu'on parle de logique, la logique bah le les premiers questionnements sur comment est-ce qu'on raisonne, comment est-ce qu'on réfléchit, bah ça date quand même euh d' a y un certain temps, hein. Donc le premier qu'on peut citer, c'est Aristote - 300. Et puis dans les civilisations un petit peu indo-pakistanaises euh il y a les coutumes du niaya. Euh là on est à + 500 où les gens ont commencé à se dire "Mais on réfléchit? Mais qu'est-ce que ça veut dire que de réfléchir? Comment on peut alors? J'irais pas utiliser jusqu'à le mot formaliser mais pourquoi pas. Donc Aristote euh Aristote il a quand même il s'est quand même posé des questions sur euh tous les sa fameuse phrase très connue "Tous les hommes sont mortels, je suis un homme donc je suis mortel et cetera". Donc c'est voilà. Ensuite bah ensuite alors les alors c'est pas ensuite c'est avant avant de commencer à essayer de raisonner sur qu'est-ce que ça veut dire raisonner? Bah, il y avait les maths. Alors, les maths, bah on remonte en Mésopotamie ou dans à peu près toutes les civilisations à moins 3000. Et alors les maths, pourquoi? Ben les maths pour calculer surtout pour construire des choses ou pour faire du commerce sur des tablettes en argile, des choses comme ça. Donc ça c'était déjà euh c'était déjà des maths. Euh formaliser. Alors, après, on parle de formaliser la réflexion. Donc après la après le calcul viennent les théorèmes. Donc là euh ça ça vous parle aussi euh c'est-à-dire essayer de de voir ce qu'on un peu généraliser les calculs qu'on fait pour les pyramides. Donc souvent aux élèves de de 3e ou de seconde, je leur cite Pythagore est à lè parce que c'est ce qu'ils connaissent c'est ce qu'ils connaissent le mieux avec Hippathi Sophie Germain au 19e siècle. Donc je sais je et tout ça tout ça pour dire que il y a pas il y a pas de de genre il y a aussi des hommes, des femmes dans toutes ces réflexions là. Euh alors on reste alors là vous voyez euh on est à - 500 un peu le 19e siècle mais 400 et les maths ont commencé à s'intéresser à la logique mais vraiment il y a il y a 1000 ans d'écart. J'ai je vous montrerai une frise tout à l'heure il y a vraiment 1000 ans d'écart entre les débuts de qu'est-ce que ça veut dire réfléchir? Qu'est-ce que ça veut dire raisonner et puis comment on peut formaliser la réflexion? Et donc là, c'est vraiment c'est la logique qui apparaît avec ça. Oui, avec au 17e siècle l'imnitz, on en on reparlera puisque en fait tous ces tous ces personnages là ont vraiment contribué à l'avènement des outils de preuv formell. On va retrouver tous ces noms quand on va parler de preuv formell euh avec Hilbert. Alors, Brouer. Alors là, j'ai mis euh des petites épées parce qu'il y a comment dire, ils se sont fightés, enfin ils se sont bagarrés. Alors, je vais revenir dessus parce que justement euh on va parler de logique classique, de logique intuitionniste et donc logique classique côté Hilbert, logique intuitionniste côté brouer. Et avant avant qu'il ne qu'il ou qu'on ne s'aperçoiv qu'en fait c'était deux logiques différentes et qu'il y en avait pas une meilleure que l'autre, qu'il y en avait pas une qui était fausse et une qui était vraie. Euh bah du coup, ça a fait une sorte de querelle entre entre ces grands personnages euh avec le on parle aussi de je alors j'ai pas mis tout le monde mais il y a le paradoxe de avec Godel. Il y a Colmogorov qui en même temps à peu près en même temps que Brouer a commencé les prémisses de la logique intuitionniste aussi. Et puis Alonso Church bien sûr on va en reparler. Tout ça c'est des noms qui vont revenir dans dans la théorie côté alors là on était toujours dans les maths hein. Donc on a fait la logique les maths et puis bah il y a quand même l'informatique. Alors l'informatique on le situe souvent vers les années 36 avec la machine de Turing. Mais si on prend une partie calcul, si on s'intéresse au calcul et ça Benjamin tout à l'heure, il va il va vous parler un peu côté calcul et ben on peut remonter à la Pascaline de Pascal. Donc ça c'est pour calculer. En gros, la Pascaline c'est la première calculatrice. Donc donc là on est déjà dans la dans l'informatique en quelque sorte puisqu'il s'agit d'automatiser le calcul. euh la machine de Charles Babage qui qui avait pour but de faire des programmes euh et puis la machine de Turing en 36. Donc là, on est dans l'informatique avec Ada Lovelace qui était une étudiante de Babge. Et alors Ada c'est la première implémentation d'un algo. Donc un algorithme, c'est on peut voir ça un peu côté un algorithme pour moi c'est un peu des maths, c'est-à-dire c'est comment c'est une recette pour pour faire des choses et puis euh l'implémentation de cet algo en tant que programme pour la machine de babege. Donc le le donc là on est on est en 1843. Donc tout ça pour dire que il y a deux il y a vraiment deux millénaires d'évolution. Alors, j'étais obligé de mettre des pointiller parce que bien sûr de millénair ça passe pas. Mais euh tout ça, vous voyez que là entre 300 et 1600 au niveau logique, alors je parle pas des maths, mais au niveau logique c'est assez il se passe pas grand-chose. C'est et surtout c'est au niveau au vers le 19e euh que ça commence à à bouillonner euh surtout au niveau math la logique mathématique. Alors là, les mathématiciens se sont emparés de la logique vraiment énormément jusqu'à l'avènement de ce qu'on peut nous appeler l'informatique maintenant qui est l'automatisation de cette logique. Euh et ce qui est alors ce qui est amusant c'est que en France par exemple la logique elle est plutôt classée dans l'informatique. Alors ça, je sais pas pourquoi pour le coup, mais elle est plutôt classée dans l'informatique mais il y a pas mal de pays en Espagne par exemple. En Espagne, la logique fait partie des maths. Ça il y a pas ça. C'est donc les départements de math bah ils font la logique. En il y a d'autres pays où j'ai vu un candidat une fois il il avait fait de la chimie et en fait alors je me souviens plus de pays, c'est dommage, faudrait que je recherche et ce candidat ce candidat là nous expliquait que en dans ce pays-là la logique était était associée à la chimie. Donc c'est les chimistes qui faisaient de la logique. Donc c'était voilà. Donc alors nous on va en venir ici dans les années 70 aux assistants de preuve. Alors on a parlé de calcul, on a parlé mais on a aussi parlé de théorèmes. Et donc les théorèmes, c'est quoi? C'est prouver la formalisation. Donc c'est les preuves formelles. Donc on ne peut pas citer les assistants de preuve sans citer la théorie des types de Martinelof. Donc je reviendrai sur la théorie des types de Martinov. Alors vous voyez que tous ces tous ces gens-là là c'est vraiment très très récent. Ça fait 50 ans hein. C'est c'est donc quand je quand je dis ça aux élèves 50 ans c'est vieux mais non par rapport à mo- 3000 50 ans c'est vraiment très très jeune. Et et d'ailleurs euh bah Martinov euh il est contemporain hein, on on le rencontre encore euh de brun ça fait pas longtemps qu'il est décédé et personnellement j'ai mangé à sa table. Donc tout ça pour dire que c'est des gens on est contemporain de de ces gens-là. Euh Thierry Cocan, bah pareil et encore un exercice, même pas à la retraite. Christine Paulin non plus. Enfin non, j'aurais pu mettre Benjamin ici comme photo parce que voilà, c'est je voilà. Euh donc c'est c'est vraiment une science qui est qui est qui est toute neuve. C'est et il s'agit de d'utiliser euh la les ordinateurs pour pouvoir vérifier des démonstrations. Alors si je refais un petit schéma récapitulatif des à partir des années 70, du coup je commence ici, c'est la petite boîte orange qui est là. Je commence ici. Donc le premier donc c'est l'automate. C'est le système automate de deux brins. Ensuite il y a un autre. Donc on verra tout à l'heure que tous ces systèmes sont basés sur plusieurs théories mathématiques et sur plusieurs logiques. Donc il y a des prouveurs ensemblistes, il y a des théories qui sont plutôt intuitionnistes, il y a des prouveurs plutôt classiques. Euh et nous on va se focaliser sur coque. Alors euh comment dire coque? Je vais parler de deux choses. Je vais parler de coq et de rock. Et souvent je vais mélanger les deux parce que jusque en 2023 ou enfin là il y a il y a il y a un an ou deux, le coque s'appelait Coc. D'accord. C'était le nom de Coque en référence au calcul des constructions, en référence à Tierry Cocan, en référence à Coc, c'est un outil français, Cocorico et cetera. Donc c'était c'est un voilà, c'est un joli nom que moi j'appréciais. Moi j'aimais beaucoup. Mais en 2023 je crois 2023 ou 2024 2023 je pense le nom a changé et ça et maintenant il s'appelle Rock mais en fait c'est exactement le même outil. Il y a juste le nom qui a changé et voilà comme je vais je vais mélanger les deux donc vous vous perdez pas si je dis rock ou coque. C'est pareil c'est voilà. Euh donc dans les années donc il y a plusieurs outils qui sont nés avec plusieurs influences. Donc ces théories là, la théorie des types de Martinov, le calcul des constructions de coquan Uette, le calcul des constructions inductives de Paulin, Morin, Verner, enfin voilà, ça ont influencé tous ces outils. H Et donc ça c'est juste pour voilà un panel un panel de ce dont de ce dont on va parler. On rentre un peu dans le vif maintenant, un peu plus le la partie historique un peu un peu finie. Euh alors c'est quoi pourquoi alors en 2026, on est en 2026, ces outils sont utilisés principalement dans deux directions. La correction de programme et de problèmes critiques. Alors, ça c'est un exemple. Pourquoi j'ai mis cet exemple là? C'est parce que je vais en parler demain. Euh demain, je vais vous parler d'éléments finis. Les éléments finis pour le coup, ça c'est des maths, c'est l'analyse numérique. Donc ça c'est des mots que qui sont familialise but c'est de prouver la correcte les programmes qui qui font des calculs sur les éléments finis. Et donc ici, on voit une plateforme pétrolière et cette plateforme pétrolière s'est totalement écroulée justement parce que le programme qui calculait les éléments finis qui sont sur sa plateforme a eu un bug. Et donc le but c'est de prouver la correction de ces programmes. Alors vous allez me dire "Ah oui mais il suffit de faire des tests, il suffit de faire du modèle checking, il suffit". Non, là on n'est pas du tout dans la vérification ni dans les tests. On est dans la preuve de programme. Et la preuve de programme, ça présente l'avantage que bah c'est on obtient des programmes qui sont vraiment prouvés par des propriétés mathématiques que l'on a démontré. On peut même en extraire un programme, je vais en parler après. Et euh donc on est sûr, on appelle ça des programmes zéro défauts. On est sûr que vraiment le programme, il est sûr puisqu'on l'a montré mathématiquement, il a été vérifié, les propriétés ont été vérifiées mathématiquement euh par nos théorèmes. Et puis l'autre direction, alors en ce moment ça bouillonne, ça bouillonne, ça bouillonne. C'est je sais pas quoi dire d'autre. C'est la formalisation des mathématiques. Alors ça le mot clé bah il y a IA dedans, intelligence artificielle. On veut utiliser l'intelligence artificielle pour prouver des théorèmes mathématiques qui sont encore ouverts, qui ont jamais été démontrés. On veut utiliser l'intelligence artificielle pour formaliser les maths dans les théorème prouver, mais on veut utiliser les théorème proover pour démontrer la correction de ce que fournit l'intelligence artificielle. Donc ça là, j'en ai mis euh 1 2 3 4 5 6 7 8 9 10 gros grosso modo une dizaine de confes qui datent il y a 2 mois hein. Voilà, elles sont toutes hyper récentes sur ce sujet-là. Euh alors après, je je vais pas parler des conséquences environnementales. Euh je vais pas parler des conséquences potentiellement sur euh bah le fait que il y a des grandes sociétés qui s'emparent de ça comme Microsoft, Google et que on craint un peu que certains théorèmes ne soient ne soient breuveté. Enfin, on brevette pas les maths, hein. Je suis pas là pour enfin vous allez pas me contredire, je pense. Les maths, c'est pas quelque chose qui doit être breveté. Donc voilà. Donc il y a Mais ça, en tout cas en ce moment ce sujet est bouillonnant. Et alors moi je vais pas en parler pour le coup, c'est voilà. Euh peut-être que Patrick Masso demain euh vous en parlera un peu, on verra. H Alors, du coup, si je reviens aux familles de prouveur, alors pour quoi faire? Et ben comme j'ai dit tout à l'heure, pour prouver euh des propriétés mathématiques, pour faire de la preuve de programme, des spécifications et alors dans la dans la vraie vie euh c'est utile aussi. On a pas mal d'exemples que vous utilisez d'ailleurs tous les jours qui ont été euh dont le les programmes ont été prouvé formellement. En particulier, on peut citer la ligne 14. La ligne 14, le métro qui conduit tout seul. Donc lui, il a été euh donc c'est Matra qui était à l'œuvre il y a c'était quand? Dans les années 80 97 98, un petit peu avant les années 2000. Et donc avec la avec la méthode B, euh la NASA utilise un autre prouveur qui s'appelle PVS pour prouver des choses sur les systèmes d'avion. Euh il y a euh la Java, le compilateur du langage C euh qui a été certifié aussi. Il y a comme je disais des exemples aussi très significatifs de développement bibliothèque. Alors Benjamin, il vous parlera du théorème des quatre couleurs. Il y a le théorème de Fight Thompson. Il y a la conjecture de Kepler qui a été prouvée en Isabelle à Choel. Euh voilà. Et donc comme je disais tout à l'heure, les preuves, on n'est pas dans la vérification, on est c'est pour ça qu'on utilise le mot clé preuve. On est dans ce qu'on appelle des démonstrations. Alors, c'est preuves mais c'est des démonstrations, des vraies démonstrations mathématiques. Alors, la logique, alors tout ça, tous ces tous ces outils, bah forcément, ils sont pas basés sur rien. Je vous je vous disais tout à l'heure, on peut pas parler de d'outils de preuve formelle dans sans parler bah sans parler de Brouer, sans parler de Martinov, sans parler de Debrin, sans parler voilà. Donc là, on y arrive. Donc il y a plusieurs logiques sous-jacentes sur lesquelles sont basés ces prouveurs. Il y a la théorie des ensemble. Donc ce que je vous le la méthode B dont je vous parlais tout à l'heure pour le météor pour la ligne 14, elle est basée sur la théorie des ensemble. Il y a le calcul des constructions inductives. Donc ça euh je vais je vous reparler de Martin Lof et Thierry Cocan et de Christine Paulin sur ça. Il y a les logiques d'ordre supérieur, il y a la logique du premier ordre, il y a tout ce qu'on appelle la théorie des types versus la théorie des ensembles, la logique classique versus la logique intuitionniste, l'isomorphisme. Donc là, on retrouve alors j'ai pas cité Cury ni Howard mais on retrouve l'isomorphisme de Cury Howard. Alors, souvent on dit l'isomorphisme de Curry Howard, mais mon directeur de thèse m'avait dit, il m'avait appris, nous avait appris que Debrin avait beaucoup participé et donc lui, il disait isomorphisme de curry de brun au ward. Donc du coup, j'ai j'ai pris son cette habitude et euh et tout ça, je l'ai dit très rapidement tout à l'heure, ça fait que grâce à cet isomorphisme, on peut extraire de nos preuves un programme. C'est comme si vous quand vous faites une preuve au tableau papier crayon ou mathématique et ben une fois que vous avez fait votre démonstration et ben hop automquement vous avez un programme qui fait qui qui qui provient de ce que vous avez démontré. On reviendra dessus un petit peu tout à l'heure sur l'isomorphisme de Curward. Alors, exemple de prouveurs. Donc du coup, les prouveurs, je vous avais dit, vous allez avoir une liste de prouveurs et on peut les classer suivant différentes méthodes. On peut les classer soit suivant la logique ou soit suivant d'autres critères qui est le transparent juste après. Donc le premier prouveur qui était automate de brins, c'est plus une logique propositionnelle. Alors, je vais revenir sur cette notion hein, mais si logique propositionnelle, je pense que ça ça vous ça vous parle. Logique du premier ordre aussi. Donc, premier ordre, c'est qu'on commence à quantifier sur les variables. Donc, c'est une logique propositionnelle où on ajoute des variables, on peut quantifier dessus. Euh la logique d'ordre supérieur. Donc là, je vais revenir dessus aussi. C'est la logique où non seulement on quantifie sur les variables, mais aussi on peut aussi quantifier sur les propositions, sur les fonctions. Donc, on passe à un ordre supérieur. Euh hm, qu'est-ce que la théorie des ensembles comme je disais tout à l'heure et le calcul des constructions inductives. Donc aujourd'hui, entre aujourd'hui et demain, vous allez principalement entendre parler de deux prouveurs, Rock et Lin. Lin, Lin, c'est le tout dernier né, c'est le dernier petit bébé, il est il est ados, on va dire. Donc ça c'est ce sera en fin de journée, je crois. Et puis et puis demain aussi. Et puis vous aurez un TP avec euh avec Patrick Masso sur sur Lin. Hm. Donc vous voyez que c'est c'est un peu comme les langages de programmation. Il y a il y a pas il y en a pas un qui est mieux que l'autre. Ça dépend ce que vous voulez faire, ça dépend ce que vous voulez prouver avec. Ça dépend si vous voulez en extraire un programme, ça dépend si vous voulez faire des maths constructives ou des maths classiques. Alors vous, je pense que vous faites que des maths classiques dans vos cours. Euh voilà, on va parler un petit peu de math constructive mais à peine. Euh donc voilà, ça dépend ce que vous voulez en faire. l'autre une autre manière de classer et ça pourquoi je vous le présente c'est parce que demain justement je vais vous parler d'analyse réelle et d'analyse numérique c'est via les nombres. Donc les nombres vous avez les entiers euh juste les entiers les entiers de piano. Donc 0 0 successeur donc c'est les nombres. Vous avez un petit peu plus d'arithmétique donc de l'arithmétique entière. Alors ça veut pas dire que dans ces prouveurs, vous avez que de l'arithmétique parce que par exemple Hol ou Isabelle ou dans COC ou dans PVS, il y a il y a aussi des réels. Mais je veux dire au niveau un peu historique, c'est les premiers nombres qui sont apparus. Vous avez des nombres réels. Alors les nombres réels, comme je vais vous en parler demain, ça pose ça pose un vrai ça pose un vrai souci. Et pourquoi? Vous voyez que là on est dans les années 80 7080 alors saufda qui est un peu particulier mais 70 80 les nombres réels, on est plutôt dans les années 90 voire la fin des années 90. Donc là c'est pareil c'est pourquoi est-ce qu'il y a autant d'années entre chaque développement? c'est parce que ça c'est pas si simple que ça. Euh et puis alors les nombres flottants, alors les nombres flottant alors oui, demain je vous en parlerai aussi. C'est quoi la différence entre les nombres flottants et les réels? Bah les nombres flottants c'est pas des enfin c'est pas des maths, faut pas que je dise ça, c'est un peu exagéré quand même. Euh mais vous en tout cas, quand vous faites vos démonstrations en tant que mat, vous faites des démonstrations avec des réels. D'accord? les réels qui ont les bonnes propriétés, les réels sont des nombres, l'addition est associative dans les réels et cetera et cetera. Les nombres flottants euh sauf que les réels c'est la c'est comme on dit la droite du continu. Donc on peut pas représenter ça en machine. Donc les vrais réels en machine bah enfin c'est c'est un peu il y en a pas. Enfin c'est je modulerai mon propos demain mais voilà. Mais donc les flottants, c'est une approximation des nombres réels pour les machines. Donc il y a des normes qui disent bah ce réel là on peut l'approximer, l'approcher par tel nombre avec une borne d'erreur qui est comme si comme ça. Donc c'est la norme i3 754 et cetera. Donc là, on est vraiment dans l'informatique, les nombres flottants, mais forcément hein, comme on est dans des outils informatiques, et ben il faut qu'on ait des nombres flottants. Alors, c'est là où je vais vous demander euh un petit peu quelle heure il est. Ah, j'ai peut-être un peu le temps. C'est là où je vais vous demander un petit peu votre avis. Euh là, on focus sur rock. On va focusser sur rock parce qu'il faut bien prendre un exemple. Et donc Rock c'est un outil qui a une trentaine d'années, non je vais pas compter 40 peut-être voilà euh qui où les choses ont été pensées depuis longtemps et et que j'utilise en particulier. Donc c'est celui que je connais le mieux. Donc c'est aussi pour ça que je préfère m'orienter sur rock. Euh là, on a le choix entre vraiment détailler toute la logique et toute la théorie qui se trouve derrière ces outils que probablement vous connaissez pas tellement ou soit faire euh passer relativement rapidement pour aller après faire une démo ou alors faire une démo d'abord pour que vous soyez pour que vous sachiez vraiment à à quoi ça ressemble et revenir sur la théorie derrière. Donc c'est un peu modulable, je sais pas ce que vous préférez. Je veux juste quand même parler de ce de cette présentation. Donc le calcul des constructions inductives, c'est vraiment la base de rock, c'est aussi la base de l C'est basé sur la théorie des types de Martin Lof avec égalité et univers. Donc ça je vais je vais passer. Donc ça c'est des évolutions. Au au départ la théorie des types de Martin Love était inconsistente et il s'avère que Jean-Irve Girard a montré cette inconsistance et donc du coup les univers ont été introduits dans la théorie des types de Martin Lov justement pour remédier à cette inconsistance. Donc du coup, c'est tout ça pour dire que rock n'est pas inconsistant puisque c'est une théorie des types avec univers. H et donc ça a donné le calcul des constructions de coconette en 85. Il y avait pas de type inductif au début. Donc les types inductifs, c'est une manière de définir et d'utiliser la récurrence. Donc ça inductif, vous connaissez ce mot en fait, c'est la récurrence he c'est tout ce qui est preuve par récurrence. Et donc Christine Paulin avec avec Benjamin aussi. ont ajouté les types inductifs. Et donc le calcul des constructions, bah ça englobe ça englobe tout ça. Le lambda calcul simplement typé, la logique d'ordre supérieur, la déduction naturelle, la logique, c'est une logique intuitionniste, il y a des types inductifs, des types dépendants. des types dépendants, il y a il y a très peu de d'outils ou de langages de programmation qui ont des types dépendants et l'isomorphisme de Cury Howard. Euh quoi qu'il en soit, j'ai quand même besoin de vous parler de déduction naturelle rien que pour faire la démo. Alors, vous avez toutes les toutes les règles. Là, il y en a que six, hein. Euh, vous avez toutes les règles. Page on quoi? Oui, oui, je vais les expliquer. Je je vais les expliquer. Je vais les expliquer comment elles se lisent. Justement alors page 18, vous avez toutes les justement j'y allais, j'y venais. Alors, comment ça se lit? Déjà, ça se lit de base en haut. Chaque règle se lit de base en haut. Par exemple, si je prends celle-ci, qu'est-ce qui se passe? Donc là, vous êtes dans un environnement donné qui s'appelle gamma et je veux montrer la propriété A. Et ben je peux montrer cette propriété A à condition que A soit dans gamma. Donc ça c'est une règle un peu évidente. C'est-à-dire si j'ai A en gros c'est si j'ai A alors j'ai A. Donc c'est Oui. On m'applaudit hein papa. On applaudit la règle hein. C'est si j'ai a. Ça c'est la règle axiomatique. C'est pour ça que axe c'est la règle axiomatique de base. Donc on va remonter comme ça à chaque fois dans l'épreuve pour avoir pour obtenir la règle axiomatique. Maintenant la règle de la flèche intro. I comme intro E comme élimination. La règle de la flèche intro ça veut dire je suis toujours dans un environnement gamma. Si je veux montrer que A flèche B, A flèche B en gros ça veut dire bah si j'ai A bah je vais pouvoir montrer B. Pour montrer que A flèche B et ben il suffit enfin il suffit une une des premières choses à faire c'est de dire bah je il faut que A vienne augmenter mon environnement gamma. Donc a vient augmenter mon environnement gamma et dans ce cas-là, je pourrais prouver B et puis après je pourrais continuer. Autre exemple maintenant si je veux prouver juste une question sur gamma. Donc gamma c'est un environnement où typiquement ça contient des axiomes. Ça contient autre chose ou c'est juste une liste d'axium? Non non ça alors gamma il peut être vide déjà au départ. Au départ il peut être vide. Après, au fur et à mesure, on l'augmente. Alors, ça peut contenir les axiomes s'il y en a, mais souvent on préfère ne pas axiomatiser les choses. Alors, je dis ça, mais demain, je vais dire le contraire, mais euh c'est pas grave. Mais les axiomes, c'est dangereux quand même parce que les axiomes, ils peuvent être faux. Un axium, c'est quelque chose qui n'est pas démontré. Donc, souvent, on essaie d'éviter de d'avoir des axiumes dans notre environnement. Euh mais ça peut aussi contenir les lèes ou les théorèmes qu'on a démontré avant. D'accord. Oui. Oui. Donc en fait ça contient ce qui est nécessaire à ce qu'on veut prouver voir plus. En tout cas, c'est une liste dénoncée. C'est une liste dénoncée. C'est une liste de théorèmes. C'est une liste de définitions. C'est voilà. Il faut pas dire que c'est un ensemble. On peut pas dire que c'est un ensemble dénoncé ou ça revient au même ça c'est un abus de langage mais c'est mais c'est pas c'est alors tu peux très bien dire tu tu le codes enfin tu le codes comme une liste ou tu le codes comme un ensemble mais c'est une succession de et fini après. Ah oui fini ou toujours fini de toute façon ou c'est alors comment si on veut montrer A et B là c'est c'est facile hein. Si on veut montrer A et B, il faut montrer donc là l'arbre il va avoir deux branches. Il faut montrer à la fois A et puis à la fois B sur le même le même environnement. Maintenant, si on veut montrer A et que on a on peut très bien avoir à montrer A et du coup euh augmenter en quelque sorte les hypothèses, mais pour dire tant qu'on a A et B, on pourra montrer A. Pareil pour B. Alors, celle-là est intéressante et elle est elle est utilisée assez souvent, il faut la l'utiliser à boncient. C'est l'unique façon de montrer le false. Donc ça c'est false. Ah oui, pardon. Ça c'est faux. C'est le bottom. C'est faux. Celui-là. L'unique façon de montrer le faux, bah c'est que on a à la fois A et puis non A. Donc là, on est dans un dans on a des hypothèses incohérentes A et non A. Et du coup, on va pouvoir montrer faux. Donc grâce à toutes ces règles, alors il y a il y a plusieurs systèmes de déduction. Grâce à toutes ces règles de déduction naturelle, on va pouvoir faire des équivalences dans notre système. Alors, notre système rock, il est basé sur ce qu'on appelle un langage de tactique. Les tactiques, c'est des ordres qu'on va donner à notre prouveur pour lui dire bah applique telle ou telle règle. Donc par exemple, si je lui dis assumption, bah il va appliquer la règle axiomatique. Si je lui dis intro, il va appliquer la règle flèche intro. Si je lui dis apply et cetera, il va appliquer un certain nombre de règles qu'on a vu tout à l'heure. Et donc du coup, il va faire petit à petit la preuve. Ça, je vais passer dans un premier temps parce que là, c'est vrai que c'est totalement nouveau. Je vous sens un petit peu perdu. Alors, exemple exemple, après on va faire la démo. On veut montrer on veut montrer que n que pour tout n + 0 = n. Ouis, vous allez me dire c'est complètement stupide comme mais il faut bien commencer quelque part. D'accord? Alors, comment est-ce que on montre ça? Alors, ce qu'il faut ce qui est intéressant dans les systèmes de preuve, alors c'est à la fois intéressant et à la fois pénible. C'est-à-dire que il faut vraiment la machine, on parle, on narrête pas de parler d'intelligence artificielle et cetera. La machine est bête en faitin, on est bien d'accord. Elle est elle est pas l'intelligence, c'est que l'apprentissage de toute façon. Elle a des capacités d'apprentissage parce que c'est des calculs monumentaux énormes mais la machine elle ne elle est bête, elle ne réfléchit pas et donc du coup il faut aller vraiment jusqu'à la base de ce qu'elle peut de ce qu'elle peut faire. Et la base de ce qu'elle peut faire, c'est la règle axiomatique dont on parlait tout à l'heure. C'est-à-dire si j'ai a. Mais mais elle va pas arriver, elle va pas arriver. Comment ça se fait ça? Elle va pas arriver à démontrer ça comme ça par miracle. Et donc euh je sais pas si vous avez déjà eu à démontrer ce genre de choses. Ah non, pas en prépa, en prépa, ils savent que n + 0 = n. Mais euh mais peut-être que euh c'est un exercice intéressant. Nous, on le fait alors je vais parler enseignement après, mais nous on le fait avec des étudiants justement. Comment on démontre que n + 0 = n? Bah, on fait on fait une preuve par récurrence. et une preuve par récurrence et ben on lui dit induction. Donc tu fais une récurrence sur n après tu simplifies. On va faire la démo tout à l'heure parce que là c'est pas une démo, c'est juste après tu simplifies donc tu auras le cas de base tu auras 0 + 0 bah é= 0. Donc ça il va il va savoir simplifier ses réflexivity donc il va obtenir 0 = 0. Donc 0 = 0, c'est la règle de c'est de la réflex c'est de la réflexion enfin réflexivité. Ensuite la IHN c'est l'hypothèse d'induction. Donc l'hyp donc ça pour les étudiants c'est quand même quelque chose d'intéressant parce que ça leur montre vraiment quel est le schéma et le principe de récurrence et puis après réflexivité à nouveau. Alors je vous rassure tout de suite he dans un outil tel que rock on n'est pas obligé à chaque fois qu'on l'on tombe sur n + 0 é= n de reprouver hein. On a des tactiques automatiques. Easy fait ça très bien. Enfin voilà il a des non c'est c'est juste pour rassurer parce que voilà. Alors qu'est-ce qui se passe quand on a fait ça? Bah les entiers naturels, comment ils sont définis? Là, on va parler de alors l'ambda à calcul. L'amb calcul euh j'ai j'ai écrit dans le dans le support que là c'est pareil, Gill que j'avais en cours à l'époque nous avait dit, c'est quelque chose qui m'avait frappé, il nous a dit le lambda calcul, on aurait très bien pu l'appeler flèche calcul. D'accord? Le lambda calcul, c'est un nom savant. Alors, d'ailleurs, je sais pas pourquoi. Peut-être que Benjamin, il sait pourquoi ça s'appelle lambda. Non, j'ai oublié. Tu as oublié? Oui, je moi aussi. Donc, je sais pas pourquoi lambda, mais en tout cas, c'est juste une manière de représenter les fonctions. Alors, le lambda calcul par exemple, si vous écrivez lambda x, alors je vais parler du lambda calcul typé. Moi, Benjamin vous parlera vous vous dira pourquoi quels sont les inconvénients de pas typer. Mais moi je vous je vais vous parler de l'OM calcul typé. C'est-à-dire si on écrit ça, d'accord? Lambda x nat x + 1. D'accord? Ça c'est exactement la même chose. Alors, je vais je vais je vais l'écrire f par exemple que d'écrire f de type n. et puis à x asso on associe la fonction x + 1. D'accord? Donc ça c'est la exactement pareil sauf que ça a un formalisme qui est qui est beaucoup plus puissant. C'est quoi le symbole entre mat et x + 1? Ouais, c'est un point. Donc ça c'est un formalisme où on peut en plus faire des fonctions de fonction euh faire des avec on peut aussi définir des fonctions à plusieurs variables ou alors la c'est vraiment un formalisme qui est qui est très très puissant. Donc ça c'est Alonso Church qui est à l'origine en 36 du lampe d'un calcul. Et ce qu'il faut savoir, c'est que Alonso Church, il a il a inventé ça et puis c'est resté un peu inutilisé pendant 22 ans jusqu'en 58. 58 c'est en fait le premier langage de programmation fonctionnelle, c'est l'ISP. Donc l'ISP qui est un langage de programmation fonctionnel. Alors ça s'appelle fonctionnel fonctionnel parce que parce que fonction hein. Et donc l'ISP est vraiment basé sur le lambda calcul inventé 22 ans plus tôt par Alonso Church. Donc le lambda calcul c'est ça. Et puis alors comment on fait par exemple pour faire f3? D'accord? Bah f3 c'est lambda x de type nat x + 1. Oui. Appliqué à 3. D'accord? Et donc bah qu'est-ce qui se passe là? Je remplace je fais x + 1 ou x est égal à 3. Alors il y a plusieurs notations. Donc on appelle ça la c'est une réduction. On appelle ça une réduction. Et en l'occurrence, on appelle ça la beta réduction. Donc x + 1 appliqué à 3 et donc ça ce betta réduit. Bah x + 1 appliqué à 3, bah 3 + 1 qui est égal à 4. D'accord? Donc il y a des tas de réduction. On Ah pardon. Oui vraiment c'est juste donc l'avantage de ça c'est vraiment juste au niveau de la notation. C'est qu'en fait si je voulais écrire au lieu de lambda x + 1, juste écrire f(x) = x + 1 mais garder ça entre braquette et puis faire une betta réduction à partir de ça, ça pourrait marcher pareil. C'est juste c'est juste une suite de symbole qui on sait qu'il faut l'identifier après. Oui. OK. On peut dire on peut dire ça comme ça. OK. Sauf que quand même quand on si tu veux écrire lambda x euh lambda y par exemple, je sais pas x x x y euh c'est quand même plus facile de l'écrire comme ça. Enfin c'est parce que ça ça connaît f de x et y. Ouais. Ça ça en fait c'est une fonction qui prend deux arguments x y en math. Alors en math ça c'est un peu compliqué parce que ce serait n2 flèche. Alors ça dépend ce que ce que je mets après hein. Si je mets x + y n flèche n. D'accord. Et donc ça ferait euh xy x + y. H donc là le n en fait alors il y a il y a ce qu'on appelle la purification mais ça je voulais pas trop en parler. Ça ça c'est un couple X Y. D'accord? Et ça c'est la même chose que de dire j'ai X et Y. Enfin X flèche Y enfin flèche. Oui. Non mais de même que de noter fx y on peut noter fx de Y. Voilà ça factoriser comme ça. C'est ça. Donc ça c'est un peu la même chose parce que il y a pas il y a pas de vraie notation mathématique pour faire cette ce qu'on appelle cette purification. Donc tandis que là c'est ça vient tout seul. Là c'est tout seul. Mais sinon c'est pareil. Alors quand on Non question ça va compliqué que non au contraire on on on va pratiquer un petit peu après. C'est oui, c'est une question d'habitude et une question de pratique mais il y a il y a beaucoup plus de choses. On peut faire beaucoup plus de choses simplement et en particulier automatiser les choses dans un Ouais. Je Est-ce que je peux juste kidnapper votre attention 5 secondes parce que comme je sais qu'il y en a quand même il y a pas mal de de camel en prépar. Combien parmi vous connaissent sont relativement familiers avec le haut camel? OK. Alors dans dans le support de cours, j'ai fait des exemples en partant d'OKAM justement parce queamel c'est un langage fonctionnel et donc quand vous écrivez en camel lettre f(x) é= x + 1, bah c'est exactement c'est exactement la même chose. Donc sauf qu'en nos camel, on n'utilise pas lambda mais c'est exactement pareil. Et donc au niveau quand on définit un type un type inductif, alors quand on fait des preuves en coque, tout à l'heure on en est là, on a fini la preuve. QED, ça veut dire la preuve est terminée. L'outil va vérifier le type, type checker va vérifier le type du lambda terme obtenu. C'est pour ça que je parle de lambda calcul et de lambda terme. C'est parce que cette preuve- làà va nous fournir un lambda terme. Le lambda terme, il est ici. Alors, je je vous le fais pas lire, mais on on va quand même le lire un petit peu ensemble après. Alors, on va commencer par le schéma d'induction quand on définit le type inductif des entiers de péano. Donc là, on est dans les entiers de péano. Les entiers de péano, on a dit tout à l'heure, c'est zéro et successeur. D'accord? Alors, les entiers de péano, on appelle ça aussi les entiers bâtons. C'est-à-dire que 3 c'est égal à successeur de successeur de zéro. D'accord? Si vous remplacez le successeur par un bâton, ça vous fait trois bâtons. Donc c'est les entiers de péano, c'est les entiers bâtons. Donc les entiers d'roc. Alors il y a pas que ces entiers là mais nous on va parler de ces entiers là. C'est les entiers de base de rock et c'est des entiers qui sont vraiment hyper simples à utiliser parce que justement on peut faire de la récurrence dessus très facilement. Et dans rock. Alors moi je dis ça, rock, on ne calcule pas. Benjamin va vous dire le contraire parce qu'on peut quand même calculer dans rock. Mais disons que quand on fait des preuves comme ça mathématiques, souvent on n pas besoin de faire du calcul. Parfois oui, en l'occurrence pour le théorème des quatre couleurs, il va vous montrer que il y a du calcul à faire, mais souvent on ne calcule pas. Et donc par contre, vous avez un schéma d'induction. Ce schéma d'induction, vous le connaissez hein, vous le connaissez depuis la classe de quoi de seconde ou je sais pas quoi quand on fait la récurrence. Non, seconde. Oui, seconde. Voilà. Donc qu'est-ce que qu'est-ce qui se passe là? D'abord, on vérifie pour le cas zéro. D'accord? Ensuite, on dit bah si pour tout n à partir de p de N, on peut montrer que c'est vrai pour P. Alors ça c'est successeur de N. Donc est-ce que c'est vrai pour p de n + 1? Alors c'est vrai pour toutes les propriétés. Donc ce schéma d'induction là, il est généré automatiquement par le système dès qu'on déclare un type inductif. Et c'est ce schéma qui est utilisé quand on applique la tactique induction. Et ben c'est ce schéma qui est utilisé. Vous voyez ici, on a le cas de base 0 + 0 = 0 qui est prouvé par la tactique de réflexivité. On a ici la l'hypothèse de récurrence. Si c'est vrai pour n, alors on le prouve pour n + 1 et c'est vrai en appliquant la la l'hypothèse de récurrence. Et finalement, on a que c'est vrai pour tout n. Alors ça c'est lisible hein. Alors on peut dans le système l'écrire directement. Il y a une tactique qui s'appelle exacte où vous pouvez directement donner le lambda à terme, c'est-à-dire ça. Mais personne enfin pas grand monde ne fait ça. Voilà. H alors ça c'est un peu ce que j'ai écrit au tableau, c'est-à-dire en rock, on a ce genre de choses, le lambda calcul et en math on a ça. Et la betta réduction, c'est ce que j'ai écrit au tableau là-bas. Alors, je vais vous faire un peu de démo peut-être pour que vous voyez plus à quoi ça ressemble et puis si vous voulez, on pourra revenir sur Non, mais c'est bon. Alors euh par exemple, voilà euh ici. Alors on va se mettre ici par exemple. Voilà. Donc vous vous souvenez où je vous disais les en déduction naturelle, on part du bas. Les règles de la déduction naturelle, on part du bas pour remonter. Et ben dans le logiciel d'enco ce qu'on veut prouver. D'accord? Et puis on va appliquer des choses, des tactiques pour lui dire bah applique telle ou telle règle. Cet exemple-là euh il est tiré, il est issu d'un cours qu'on fait en double licence Matinfo à Sorbon Paris Nord. Euh où on leur fait au des étudiants, on leur fait du rock. Donc dès le mois de septembre, ils arrivent, ils sortent du lycée, ils sortent de la terminale, on leur fait du rock. Et euh alors et donc et donc on leur on leur explique alors il y a plein de choses avant hein, mais on leur explique que euh comment faire les preuves dans donc je je vous montrerai si j'ai le temps, moi j'aimerais bien avoir le temps, un fichier un peu plus fourni de des preuves qui peuvent qu'il peuvent faire avec. Et donc il les ça fait ça fait combien de temps? Ça fait 3 ans au moins qu'on fait ce cours. Ça fait 3 ou 4 ans qu'on fait ce cours. Et il s'avère que nos collègues enseignants de math trouvent que depuis qu'on fait ce cours, les étudiants sont beaucoup plus rigoureux dans leur manière de rédiger leur preuv mathématiques. Et donc notre but à nous, c'est pas de leur apprendre rock ni de leur apprendre la logique sous-jacente. Là, je vous en ai parlé parce que parce que je trouve que pour vous, c'est intéressant de savoir ce qui se passe derrière, toutes les toute l'évolution qu'il y a eu pour arriver à ces outils. Mais eux non, eux eux c'est vraiment côté utilisateur. On leur parle pas de calcul des constructions inductives, on leur parle pas de lambda à calcul, on leur parle pas on leur parle pas de déduction naturelle, on leur parle pas de tout ça. Mais par contre euh on leur explique comment sont définies les entiers de péano. On leur explique par exemple le schéma inductif qui est issu des entiers de péan et du coup cette preuve par exemple sur l'associativité parce que n + m + p là c'est un parenthèsage. Alors c'est alors c'est oui c'est c'est ce qui est dit en commentaire ici c'est-à-dire que par défaut l'associativité est parenthèsée à gauche. Donc là en fait entre le n + m c'est parenthès à gauche. Donc c'est pas c'est pas indiqué, c'est pas affiché par le pret printer de rock. Alors ça c'est des c'est des choses à savoir. Voilà. Mais par contre quand on inverse le parenthèsage par défaut, bah forcément c'est c'est logique. Alors h alors là, qu'est-ce que qu'est-ce qu'on a fait? On a fait une induction sur n. On a fait une induction sur N. C'est pas ce que j'aurais voulu qu' qui vous montre. Alors attendez, je vais modifier un petit peu ça parce que là c'est un peu trop automatisé. Et puis voilà. Donc j'ai fait une induction donc une une récurrence sur les entiers et j'ai mis les variables, je les ai mis en dans le contexte. Donc elles sont passées au-dessus du trait. D'accord? Et donc je dois montrer le cas 0. L'induction, elle est que sur n. Donc le cas de base c'est je remplace n par 0. D'accord? Et là bah comment ça se passe? Bah la réflexivity la réflexivité va le montrer va le montrer tout seul. Et ce qui m'intéresse, c'est le cas inductif. Le cas inductif, je vais appeler la tactique simple. Regardez bien ce qui se passe ici. Vous voyez la différence? Donc qu'est-ce qui se passe? Regardez comment est définie l'addition. L'addition, elle est définie si donc j'ai l'addition entre là-bas l'addition entre n et m. D'accord? Ça, ceux qui font du camel, vous arrivez à lire parce que c'est exactement la même chose, hein. Vous voyez que c'est une syntaxe très proche de camel. Donc je fais un match si j'ai 0, si n est égal à 0, ben j'obtiens m. D'accord? Et si n est égal à successeur de p et ben j'obtiens successeur et je me rappelle récursivement sur P et M. Donc ça c'est l'addition de n de n et de m. OK? Et donc qu'est-ce qui va se passer quand je vais appliquer? Je vais remonter d'un cran ici. Donc ici, c'est pour ça que je vous parlais de réduction tout à l'heure. Ici, j'ai S n + m + p et ça c'est égal à s n + m. Je vais mettre les parenthèses + P. OK. La tactique simple, elle fait de la réduction. Donc là, on est dans quel cas? On n'est pas dans le cas zéro, hein. On n'est pas dans le cas zéro parce que là, on est dans un cas successeur. Donc le cas successeur, il va appliquer ça et donc il va dire qu'on est dans la cas S. C'est pour ça que vous voyez la différence, on est dans le cas S finalement de N, d'accord? Plus m + P égal. Et puis là, voilà, là, on s'en fiche un peu pour l'instant. Bon, enfin non, pas tant que ça. Non. Ouais. Donc il les applique plusieurs fois. Il applique la simplification plusieurs fois. Donc vous voyez là. Et là, qu'est-ce qu'on peut faire maintenant? Il faut toujours regarder là-haut. Il faut toujours regarder là-haut parce que là-haut, on a une hypothèse de récurrence. Si on l'avait pour n, alors l'hypothèse de récurrence c'est si on l'a pour n et qu'on peut le prouver pour n + 1 et cetera. Donc là l'hypothèse de récurrence c'est on a la propriété sur n et on veut la prouver on veut sur n + 1. Sauf qu'en ayant fait simple qu'est-ce qu'on retrouve ici? On retrouve n + m + p. Et donc qu'est-ce qu'on peut faire? On peut appliquer l'hypothèse de récurrence. Donc on peut réécrire. Alors là, le intro il est il est pas nécessaire parce que je l'avais déjà fait tout à l'heure. Le intro je vais l'enlever parce que je l'avais fait tout à l'heure. Donc là on peut réécrire l'hypothèse de récurrence. Vous avez eu le temps de voir ce qui s'est passé. Vous avez vu? Là vous réécrivez et là du coup qu'est-ce que vous obtenez? Bah vous obtenez A = A. Donc là c'est fini par réflexivité. Et donc le le la tactique re la tactique revright, elle réécrit quand vous avez quelque chose en hypothèse qui est A = B. Vous avez une hypothèse H. Donc elle réécrit A en B. Elle réécrit pas B en A. Si si vous faites revivr H là, elle va réécrire B en A. Si vous alors vous la flèche par défaut, c'est celle-là, elle réécrit A en B et l'autre côté, ça réécrit B en A. Donc effectivement, vous pouvez réécrire des deux côtés et vous voyez que ça c'est encore un exemple où on doit tout lui dire parce que il est pas capable de voir tout seul de quel côté il doit réécrire. Alors oui, c'est juste pour revenir sur le cas de base avec zéro. Le cas de base ou euh en fait il y a l'idée que 0 plus quelque chose il y a le quelque chose mais en fait ça apparaît où? C'est dans le réflexivity. C'est dans réflexivity parce que parce que là on pourrait faire simple aussi. Vous voyez si je fais simple d'après la définition ici quand j'ai zéro il me réécrit en M. Donc le réflexivité il est un petit peu plus puissant que juste le réflexivity. Il regarde pas juste si c'est vraiment pareil. Il regarde pas juste si c'est vraiment pareil. Il fait du il fait du simple aussi. Ah d'accord. Merci. C'est donc il y a un ensemble d'axium qui permet de faire des récultures basiques aussi qui sont spécifi les règles de déduction naturelle que je vous ai montré, j'ai un petit peu triché parce que c'est des règles de déduction naturelle vraiment de base mais les tactiques elles une tactique peut appliquer plusieurs règles de déduction naturelle en une seule tactique. Ouais. Et le QED tu as dit que ça servait àier le type d'un d'un lamme ou quelque chose comme ça? Alors le QED du coup, est-ce qu' est-ce qu'il peut échouer le QED? Alors euh euh quand on est ici, on nous dit là-haut, tu as démontré tous les buts. Donc en principe le QED, je je crois que j'ai je suis même pas sûr de l'avoir vu échouer une seule fois, mais quand le QED échoue, euh peut-être que toi avec les quatre couleurs, tu as vu échouer le QED. Mais c'est très rare, c'est que je peux en dire, j'en diraiis peut-être un mot après. Ça vaut le coup de reposer la question à ce moment-là quand je parlerai tout à l'heure. Mais mais mais en l'occurrence alors le QED, il va type checker tout le lamp à terme qu'on a ici et tel ce qu'on peut dire, c'est que le QED fait une deuxième passe, ça vérifie que la construction a été bien faite et du point de vue architecture de sûreté, la confiance qu'on peut avoir, il suffit de faire confiance au PED. C'est un peu ça le truc puis a c'est un point important. Oui, en fait le le QED quand le QED passe et qu'on et qu'on a et qu'on affiche euh Ah non, c'est pas ça que je voulais afficher. Je voulais afficher le Lambda terme du lemme d'associativité de tout à l'heure qui était print plus associatif. Donc une fois qu'on a fait le QED, le lambda terme il est là, il a il est encore plus compliqué que celui qu'on a vu tout à l'heure. Et le QED en fait il il refait une passe de typage sur tout ce lme par rapport aux règles internes du système, aux règles logiques du système. Donc mais c'est assez rare qui enfin moi je l'ai jamais vu échouer personnellement parce que je fais pas des choses suffisamment. Je pense que là où il y a plus de problèmes ou de risque d'échec justement c'est quand il y a du calcul ou ou c'est quand il y a de l'automatisation qui utilise du calcul. C'est pour ça que je me retournais vers Benjamin parce que moi je fais vraiment des preuves quoi. Je fais pas de calcul enfin je fais c'est et donc il y a une vraie différence dans ce genre de dans ces outils entre le calcul et la preuve. Alors après on peut on peut toujours discuter est-ce que 2 + 2 = 4 est-ce que c'est une démonstration ou est-ce que c'est un calcul? Et en l'occurrence pour les entiers de péano ou pour ou même pour les réels dont je vais vous parler demain 2 + 2 c'est plus une preuve qu'un calcul. C'est voilà. Du coup, ça serait un calcul alors la alors l'arrê alors déjà on peut se demander est-ce que la est-ce que la réduction est-ce que le fait de faire ça est-ce que ça c'est un calcul? On peut se poser la question donc c'est c'est déjà un petit calcul. Euh un calcul c'est ce que font les langages de programmation. Les les flottants, c'est des calculs. Voilà. Les entiers binaires, c'est des c'est du calcul. Benjamin, demain, il va vous parler de VM Compute qui est euh une tactique qui fait du calcul. Donc lui, il va vous en parler pour le coup parce que pour le théorème des quatre couleurs, il y a vraiment du calcul. Euh alors, je voulais vous parler un voulais je voulais vous montrer un autre exemple de ce qu'on peut faire avec les étudiants. En particulier, celui-là vous aurait plus intéressé peut-être parce que c'est les coefficients binomiaux. Et donc on a tout un panel d'exercice sur les coefficients binomiaux. par exemple euh le fait que hm qu quel qu'est-ce qui est voilà que la somme des coefficients binomiaux et ben c'est 2^iss n donc et vous voyez qu'on a plusieurs pour les étudiants euh il y a plusieurs indications. Donc pour faire si on reprend cet exemple là, donc la somme ça c'est la somme de 0 à n, la somme sur k. Donc les coefficients binomiaux. Alors moi je suis habitué à dire CNK mais je sais pas comment CNK c'est voilà. Je sais pas d'ailleurs avec la notation comme ça là je sais pas comment on dit. K parmienne. Ah c'est ça le nouveau truc c'est parmienne. Non moi j'ai appris CNK pardon. Mais donc K parmi N. OK. Donc K parmi c'est long. C'est un peu long. C'est un peu long. Bref, très bien. Donc K parmi n, la somme des K par des K parmi n. Ouais, c'est ça. Oui. Oui. Ce qu'il disent, d'accord? Euh et ben c'est 2^iss N. Donc là, vous voyez, on leur dit et ben il faut commencer, ce serait bien de commencer par transformer de en une somme. Alors, de en une somme, bah on commence par trans donc 2 c'est 1 + 1. D'accord? Alors voilà. Donc donc je là je lui dis bah remplace 2 par 1 + 1 et puis prouve-moi automatiquement que 1 + 1 Ouais, c'est euh ça fait 2 donc par réflexivity. Et donc il m'a remplacé 1 + 1 là-dedans. Ensuite on leur dit utilise la formule du binôme qui est au-dessus, la formule du binôme qu'on a prouvé avant. Donc je réécris la formule du binôme. Voilà. Donc en réécrivant la formule du binôme et ben mon terme de gauche reste inchangé mais mon 1 + 1^ n et ben je peux le réécrire en la somme des i parmi n de 1^ i x 1^ n - i. Donc il m'aurait écrit la formule du minom. Ensuite, j'applique euh le j'applique un autre lem avant que je peux vous afficher ici qui est celui-là. le fait que la somme euh que si j'ai euh f1 de k = f2 de k et cetera, bah j'ai la somme, la somme enfin ça passe à la somme, c'est la même chose. Et puis après, je réécris. Alors, j'ai des tas de modifications un peu pénible sur le fait que 1^ n et ben c'est pareil que 1 et sur le fait que 1 puissance n- k et cetera. Donc il y a des tas de il y a de tas de choses un peu pénibles, mais on arrive à leur faire des choses assez compliquées avec les coefficients binomiaux euh qui sont qui sont intéressantes. Donc je vais conclure pour aujourd'hui. Donc pour aujourd'hui, c'était vraiment une introduction un peu un peu simple en principe de ce qui est les de ce qu'on peut faire avec les preuves formelles et de toute l'évolution au niveau de la recherche et qui s'applique maintenant à l'enseignement. Demain, on parlera euh on parlera de choses un petit peu plus compliquées qui sont les réels et l'analyse numérique. Et si et si vous êtes intéressé, bah il y a il y a enfin, j'aurais pu expliquer euh revenir si vous voulez qu'on fasse ça demain, que je revienne plutôt sur les notions de curry award, des choses comme ça, c'est possible aussi. Mais c'est dans le support de cours pour le coup. Voilà. Il y a-t-il des questions? Là, si j'ai bien compris la preuve du binôme. En fait, ce qu'on fait, c'est qu'on fait des on parle de ce qu'on veut montrer, on fait des tas de réaction, on arrive à avoir A = A. Exactement. C'est ce qu'on appelle une preuve backward. En fait, en pratique, quon fait, on fait pas comme ça. Non. Alors en pratique en math, en math, on fait pas comme ça. Donc en fait, est-ce que est-ce que du coup il y a toujours cette philosophie de faire une preuve un peu différente? Alors la philosophie c'est vraiment une preuve en backward mais on peut très bien faire une preuve en forward, c'estàdire en avant. En fait en math les mat, vous faites une preuve en avant. Euh, on peut le faire en mettant accerte par exemple. Vous avez un une tactique qui est accerte le machin que vous voulez euh vous voulez mettre et puis du coup ça vous fait vous prouver de manière intermédiaire des des espèces d' sous-étapes qui font que votre preuve devient en forward. En oui, en forward, en avant, une preuve en avant. Mais la philosophie, c'est plutôt la philosophie de la déduction naturelle qui est en fait comme comme vous avez dit une on part de ce qu'on veut et puis on remonte jusqu'à l'axiome qui est une preuve en arrière. Mais les deux sont possibles. Mais la philosophie naturelle c'est la preuve en arrière. Et là, il y a-t-il d'autres questions? Qu'est-ce qu'il a fait Sophie Germain en Sophie Germain? C'est c'était un exemple pour des orbes de math pas de logique. Logique. C'était juste des maths. Oui, c'est ça. Quand on parle de théorie des types, comment on se place par rapport à la logique du premier ordre ou la logique classique infionniste? Pardon, quand on est en logique du premier ordre, on peut décider de se placer en logique classique ou inclusionniste. Si on si on s'intéresse à la théorie des types, est-ce qu'on peut faire de la logique du premier ordre? Est-ce qu'on peut faire de de la logique classique, de la logique intuitionniste? Je pas je comprends pas bien le rapport. Je passe ma question. H alors la théorie des types, c'est enfin est-ce que ça remplace le la logique du premier ordre? Euh non. Enfin, c'est c'est c'est plus fort. Enfin, ça remplace non. C'est-à-dire que quand déjà il y a il y a non euh la théorie des petites c'est une théorie qui est beaucoup plus forte où on peut typiquement la quantifier sur des propositions et sur des fonctions, ça permet de prouver et de formaliser beaucoup plus de choses. La logique du premier ordre, on est quand même limité à la quantification sur les variables. Oui. Mais mais mais quand on fait de la théorie des types, on utilise pas les définitions disons de la de la logique du premier ordre? Bah si, c'est la logique du premier ordre, elle est elle est en quelque sorte inclus dans la théorie des types. D'accord? Parce que on n'est pas obligé de quantifier systématiquement sur des propositions, d'accord? On peut ne quantifier que sur des variables. D'ailleurs, là ce que j'ai fait, c'est pas tellement d'ordre supérieur. D'accord. Mais mais mais elle est inclu et et du coup quand on s'intéresse aux règles de la logique là on peut quand on est en théorie des types on peut choisir de d'utiliser les règles de la logique intuitionniste ou de ou classique. Alors là par défaut oui par défaut on est intuitionniste. Euh si on veut ajouter le tiers exclu, il faut l'ajouter à la main en disant j'ajoute l'axium du tiers exclu et dans ce cas-là je peux l'utiliser. Là, il est pas utilisable par défaut dans tout ce que j'ai montré. C'est juste si tu as envie que je rajoute un truc làdessus parce que le le effectivement comme dit Nikala la théorie type ça étend la logique du premier ordre. Euh après ce qui se passe en logique, il y a il y a des il y a des des différences de codage. C'est qu' en logique du premier ordre, on sait pas parler de fonction comme des objets. Donc ce qu'on fait, c'est qu'on les fonctions, on représente les fonctions par leur graphe. à part des relations, des ensembles de pair, des choses comme ça, ce qu'on peut faire en théorie des types, mais du coup, on peut parler des fonctions de deux manières différente et ça change des choses. Après, dans la motivation de la théorie des types, en tout cas celle de Martin L et celle qui viennent après, il y a effectivement un truc intuitionniste, c'est que ce que ce qui se passe c'est que les preuves deviennent des objets. Une preuve de A implique B, c'est une fonction qui prend une preuve de A et qui la transforme en preuve de B. Donc c'est un objet de type A flèche B ou A implique D, c'est la même chose. Alors ça c'est assez joli, il y a tout un tas de choses. Mais ce qui se passe làd quand on commence à faire ça, une preuve de A ou B, en gros, c'est soit une preuve de A, soit une preuve de B. Il y a un petit drapeau, un constructeur, ce qu'on en ML, on appelle un constructeur qui dit "Je suis la preuve de A ou je suis la preuve de B." Et donc en théorie des types, si on fait ça, naturellement on est en logique intuitionniste et si on veut rajouter le tiers exclu, là effectivement il faut supposer le tier exclu. Mais ça c'est un truc qui calcule pas parce que le tier exclu truc qui prendrait qui nous mettrait au chômage mais heureusement on sait que ça n'existe pas. Quelque chose qui prendrait une proposition en argument et qui dit bah voilà la preuve que c'est vrai ou la preuve que c'est faux parce que c'est a ou noi donc c'est un axium supplémentaire. C'est donc c'est un axium supplémentaire. Ouais. Il est alors là Benjamin, il a parlé de ça. Donc c'est-à-dire la correspondance entre type et proposition entre programme et preuve. Donc c'est c'est l'isomorphisme de Cury Award. Il a parlé de l'interprétation de Brewering Colmogorov qui fait que la preuve de A et B et ben c'est la preuve de A et la preuve de B et cetera. Et il a aussi parlé de ça qui est l'axium du tir exclu. C'est les donc ça je l'avais un peu préparé mais voilà c'est on peut pas avoir le temps de tout euh qui est ces deux principes là que Brouur donc c'est vraiment Brouur qui a réfuté ces deux ces deux principes. Euh donc ce qu'il vient de dire c'est que soit on a soit on a non a et du coup bah voilà. Alors, il y a une anecdote assez assez amusante moi que je raconte à mes à mes étudiants. C'est vous arrivez à la maternité, vous avez une dame qui vient d'avoir un qui vient d'avoir un enfant et puis vous lui demandez à cette dame "Ah, alors c'est une fille ou un garçon?" Et puis la dame classique, elle vous dit "Oui, d'accord?" Par contre, la dame intuitionniste, elle prend le bébé, elle enlève la couche et puis elle dit "Tiens, regarde, c'est bah une fille ou un garçon, enfin peu importe, mais voilà. euh et apporte la preuve que c'est une fille ou un garçon, ben elle dit pas juste oui. Donc ça c'est la vraie différence entre la logique classique et la logique instrutionniste. C'est voilà. Et donc pareil pour le pour le pour le il existe, le il existe, et ben pour montrer un existe constructif et ben il faut apporter vraiment la la preuve, il faut apporter le en quelque sorte le programme et on revoit le l'isomorphisme de Curious apparaître. Il faut apporter le programme enfin la preuve que ça calcule bien, qu'on a bien que c'est bien le témoin qui vérifie la propriété. Et donc c'est grâce à la logique intuitionniste qu'on peut extraire en extraire un programme justement. Il y a-t-il d'autres questions? On verra la suite demain? Ben, je pense qu'on peut remercier