package coq-matrix

Matrix is an important mathematical tool. Although there are at least five matrix models/libraries in Coq community, the massive verification project involving matrix are still facing some problems: (1). There havn't a full-feature formal matrix library, because the matrix theory is complex and need more time to formalize it. (2). Different libraries of these implementations cannot be easily switched at the later stage of a verification process, because the type of operations and theorems are different. But some project maybe need more matrix theories while the needed theorems only avaiable in another libraries.

Thus, we provide a unified framework for different implementations of formal matrix models, so as to decouple the difference between underlying technologies and upper-level applications.