基于Coq的分块矩阵运算的形式化

矩阵是工程领域中常用的一种数据结构，在深度学习领域，矩阵乘法是神经网络训练中的核心技术之一，面对大型矩阵的运算问题，分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算，并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.本文首先对目前学术界的矩阵形式化工作进行了系统总结并且分析了矩阵形式化的主要几种方法；其次介绍并完善了基于Coq记录类型的矩阵形式化方法，其中包括提出新的矩阵等价定义、对之前的形式化工作进行了整理和完善，并证明了一组新的引理；在此基础上进一步实现了分块矩阵运算的形式化，讨论了该类型的归纳证明的难点和解决方法；最终实现了矩阵与分块矩阵形式化的不同类型的基础库.

Formalization of Operations of Block Matrix Based on Coq

Matrix is a commonly used data structure in the field of engineering. In the field of deep learning, matrix multiplication is one of the key technologies in neural network training. Faced with the problem of operations of large matrices, the block matrix technology can be used to convert large matrix operations into small matrix operations to realize parallel computation, which can greatly reduce matrix operation steps and improve the efficiency of matrix operation. Firstly, this paper systematically summarizes the current matrix formalization work in academia and analyzes the main methods of matrix formalization. Secondly, it introduces and improves the matrix formalization method based on Coq record type, which includes putting forward a new definition of matrix equivalence, sorting out and perfecting the previous formalization work and proving a new set of lemmas; then on this basis, the formalization of block matrix operations is further realized, and the difficulties and solutions of this type of inductive proof are discussed. Finally, basic libraries with different types for matrix and block matrix formalization are realized.