Mathematical Components est un ensemble de bibliothèques de mathématiques formalisées développées avec l’assistant de preuve Coq. Ces bibliothèques ont été utilisées pour des projets de formalisation à grande échelle, tels que celle du théorème des quatre couleurs et du théorème de l’ordre impair (Feit-Thompson).
Dans ce cours en deux parties, nous explorerons les bibliothèques Mathematical Components disponibles et je fournirai des éléments pour en lire le contenu, les utiliser et y contribuer.
La première partie du cours donnera des clés de lecture de la bibliothèque, et en particulier comment y trouver et utiliser les résultats recherchés. Pour cela nous passerons en revue les conventions de nommage et d’usage en vigueur, afin de faire des recherches pertinentes dans le contenu des bibliothèques. Nous verrons également comment lire les scripts de preuve écrits avec le langage de tactique SSReflect, ainsi que les quelques tactiques indispensables pour utiliser des résultats de la bibliothèque. Cela sera illustré avec quelques exemples lors de session d’exercices encadrés.
Mercredi 14:00 - 15:30
La deuxième partie du cours sera consacrée aux hiérarchies de structures présentes dans les bibliothèques Mathematical Components et à la manière dont elles sont générées avec Hierarchy Builder à partir de la version 2.0+alpha1 de Mathematical Components. Je présenterai les motivations pour l’utilisation de Hierarchy Builder par rapport à une gestion manuelle avec des records, des classes ou des modules. Ensuite nous examinerons les différentes façons d’instancier des structures, puis comment ajouter des nouvelles structures en utilisant Hierarchy Builder, et enfin comment modifier du code tout en préservant la compatibilité arrière.
Jeudi 17:00 - 18:30
https://www-sop.inria.fr/teams/marelle/JFLA-23-installers/
Suivez les instructions
d’installation de Coq (si vous créez un nouveau switch opam
n’oubliez pas de rajouter le repository de Coq avec
$ opam repo add coq-released https://coq.inria.fr/opam/released)
Ajouter le repository de mathcomp 2
opam repo add mathcomp2 https://www-sop.inria.fr/teams/marelle/JFLA-23-installers/opam/Attention! Si vous avez ajouté le repo hier, il y avait un bug et ce
n’est plus le même aujourd’hui, il faut retirer le précédent
(opam repo remove mathcomp2) avant de recommencer.
Installez les paquets suivants (dans l’ordre indiqué !):
opam pin coq-mathcomp-field -k version 2.0.0+alpha1
opam pin coq-mathcomp-zify -k version hierarchy-builder
opam pin coq-mathcomp-algebra-tactics -k version hierarchy-buildercachix use coq coq-community math-comp # install cachix if not working)
nix-shell https://github.com/gares/math-comp-school-2022/tarball/master