Canonical Big Operators
The bigops library contains an approach to describe uniformly iterated "big" operations and to provide lemmas that encapsulate all the commonly used reasoning steps on these constructs.
This is one of the libraries developed within the Mathematical Components project and it is based on the SSReflect extension of the Coq proof system.
A paper describing this work has been submitted at TPHOLs [ pdf ].
Some applications based on the library are:
- formalization of determinants and the Leibnitz formula [source];
- proof of the Cayley-Hamilton theorem [source, pdf (in french)];
- formalization of multivariate analysis for Kantorovitch's theorem [source, pdf].