Generic Proof Tools and Finite Group Theory
Outils génériques de preuve et théorie des groupes finis
Résumé
This thesis presents advances in the use of Canonical Structures, a programming language construct of the Coq proof assistant equivalent to the notion of type classes. It provides a new model for developping hierarchies of mathematical structures using dependent records, and, as an illustration, reformulates the common formal proof of the correctness of the RSA cryptosystem, providing facilities for algebraic reasoning along with a formalization in type theory of the necessary mathematical notions (including cyclic groups, automorphism groups, group isomorphisms). We provide an extension of the Canonical Structure inference mechanism using phantom types, and apply it to treating the notion of partial functions. Next, we consider a generic treatment of several forms of subgroup definitions occurring in the formalization of the Feit-Thompson theorem, a large library of fomalized algebra developed in the Mathematical Components team at the MSR-INRIA joint laboratory. We show that a unified treatment of those 16 subgroups allows us to shorten menial proofs and obtain more composable definitions. We formalize a correspondence between the study of those group functorials, and some common and useful group-theoretic properties represented as the class of groups verifying them. We conclude in exploring the possibilities for analyzing the functoriality of those definitions by inspecting their type, and suggest a path towards obtaining instances of a parametricity result in Coq.
Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.
Loading...