Réunion en visio sur https://rendez-vous.renater.fr/liberabaci.
Planning prévisionnel :
Un moyen de faciliter l’entrée des débutants dans un système de preuve sur ordinateur est de fournir un ensemble de contenus pensés pour une prise en main facile, et en évitant les choix multiples. Il faudrait ainsi disposer d’une collection de bibliothèques thématiques motivée par le besoin d’enseignement. Pour chaque bibliothèque, nous proposons de réunir des spécialistes de formalisation, un ou des enseignants de mathématiques, et des jeunes chercheurs qui seront ainsi formés à l’utilisation de Coq et au travail à l’interface avec les enseignants. Le travail effectué jusqu’à maintenant a permis l’exploration de chemins divers, mais il manque un parcours balisé pour l’enseignement, où les différents aspects d’une bibliothèque (progression des concepts, uniformité des nommages, complétude des théories pour chaque niveau d’abstraction) sont organisés. Le développement de ces bibliothèques thématiques est un travail d’envergure et représente un risque assez fort si la complétude et l’uniformité ne sont pas obtenues de manière satisfaisante. Un domaine important des mathématiques concerne l’analyse réelle, et c’est d’ailleurs pour cette raison que Coq dispose déjà de bibliothèques anciennes sur ce sujet. Toutefois, ces bibliothèques souffrent de défauts hérités de choix initiaux dont les conséquences sont apparues avec le temps. Nous proposons de reprendre ce travail et de l’utiliser comme étude de cas. Sur la base des expériences précédentes, certains choix pour la prochaine bibliothèque sont clairs, alors que d’autres aspects font encore l’objet de réflexions. Ainsi, il est certain que cette bibliothèque d’analyse pour l’enseignement doit reposer sur des principes de logique classique : il faut partir des axiomes connus, axiome du tiers-exclu, axiome du choix, principe d’extensionnalité pour les fonctions. Il faut également exploiter ces axiomes au maximum dans les outils de preuve automatique.
Il serait tentant de décider maintenant le contenu des bibliothèques à formaliser, mais il est important de synchroniser cet partie du travail avec les enseignants. Un point qui pourra demander plus d’expérimentation concerne le niveau d’abstraction vis-à-vis des espaces à une ou plusieurs dimensions. Considérer les théorèmes sur ℝ comme des cas particuliers de théorèmes plus généraux sur ℝn permet de faire certaines preuves une seule fois. En revanche, une telle économie présente une difficulté supplémentaire pour le public étudiant, qui doit être capable d’absorber simultanément les concepts spécifiques au théorème et le raisonnement en plusieurs dimensions. Il faudrait aussi que cette nouvelle bibliothèque puisse être reliée aux autres développements existants, pour permettre à la fois une transition confortable vers des développe- ments plus évolués (tels que Coquelicot, MILC, ou mathcomp-analysis) et une réutilisation efficace de matériel déjà formalisé. Il faut noter que des expériences d’utilisation en milieu universitaire ont déjà commencé.
Il y a eu trois exposés LiberAbaci à ThEdu le 2 juillet 2024 à Nancy.
David Hamelin: Teaching Divisibility and Binomials with Coq (avec Sylvie Boldo, Francois Clement, Micaela Mayero et Pierre Rousselin). Cet exposé s'accompagnent de démonstrations utilisables dans le navigateur, pour la divisibilité et pour les nombres binomiaux.
Pierre Rousselin: Maths with Coq in L1 (avec avec Marie Kerjean et Micaela Mayero).
Julien Puydt: Framed Typing