Introduction à Coq: Expressions arithmétiques et évaluateurs

Cette séance de cours présente les bases de Coq, en se concentrant sur la définition d'expressions arithmétiques à l'aide de types inductifs. L'instructeur commence par expliquer comment créer un type arithmétique simple avec des constantes, des additions et des multiplications. Des exemples sont fournis pour illustrer comment construire des expressions et les évaluer. Les concepts de taille et de profondeur des expressions sont introduits, ainsi que les fonctions récursives pour calculer ces propriétés. L'instructeur démontre comment prouver des théorèmes sur la relation entre la profondeur et la taille en utilisant l'induction. La séance de cours progresse pour inclure des variables dans les expressions arithmétiques, montrant comment modifier la fonction d'évaluation pour tenir compte de ce changement. L'instructeur souligne l'importance de l'automatisation de la preuve dans Coq, démontrant diverses tactiques pour simplifier les preuves. La séance de cours se termine par une discussion sur les optimisations pour les expressions et l'exactitude de la fonction d'évaluation, renforçant le lien entre la théorie et la mise en œuvre pratique dans Coq.