img-logoInria img-logoProveandRun


Conférence ITP 2013 (Interactive Theorem Proving)

Tutorial 2: The Mathematical Components library - principles and design choices

img-ITP2013AssiaMahboubi-EnricoTassi Assia Mahboubi & Enrico Tassi

Mathematical Components project at the Microsoft Research-Inria Joint Center


1. Contents of the library, by Assia Mahboubi

2. Live demo, by Enrico Tassi at 25:24

3. There are tricks in every trade, by Enrico Tassi at 52:45

4. Conclusions, by Assia Mahboubi at 60:07

5. Questions, at 83:00

Companion material:  Slides, demo files and and other resources

Wednesday, July 24th (duration: 91:23)


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.