Abstract:

The Mathematical Components project has organized a six year collaborative effort which culminated with a formalization of a proof of the Odd Order Theorem using the Coq system.

The wide and complex variety of algebraic theories at stake in this proof motivated the choice of this famous result of finite group theory. Its formalization requires a description of this edifice of mathematical theories in the type theory implemented by Coq, and a faithful account for the numerous proof methodologies encountered throughout these areas. The code describing the very proof of the Odd Order Theorem actually counts only for one third of the total and should be considered as a large scale validation of the prerequisite components.

In the present tutorial we discuss a panel of methodologies that emerged from this experience. In particular we comment on the features of the Calculus of Inductive Constructions we use in order to represent mathematical objects. We also describe how we take benefit from the facilities provided by Coq like user notations or programmable type inference. Finally we comment on some policies we enforced while developing this code in order to preserve the robustness of proof scripts and the modularity of the components.