Packaging Mathematical Structures

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference; inside the COQ system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm; and a matrix decomposition problem.