Page 327 - 《软件学报》2021年第6期

麻莹莹 等:基于 Coq 的分块矩阵运算的形式化 1901

从该例子的证明中我们可以明显发现证明的简化,并且该简化对于难度更大的引理证明仍然适用.因此,我
们在证明分块矩阵函数与矩阵函数等价性,不仅能够保证分块矩阵运算函数的正确性,还能够在很大程度上简
化分块矩阵函数性质证明过程,减少重复证明工作.
目前已成功证明的分块矩阵函数性质引理见表 4.
Table 4 Lemma of the properties of the block matrix function
表 4 分块矩阵函数性质引理
引理 引理名字
加法交换律 mmatrix_add_comm
加法结合律 mmatrix_add_assoc
左加零矩阵性质 mmatrix_add_zero_l
右加零矩阵性质 mmatrix_add_zero_r
减法交换律 mmatrix_sub_opp
减法结合律 mmatrix_sub_assoc
左减零矩阵性质 mmatrix_sub_zero_l
右减零矩阵性质 mmatrix_sub_zero_r
自身相减矩阵性质 mmatrix_sub_self
乘法左分配律 mmatrix_mul_distr_l
乘法右分配律 mmatrix_mul_distr_r
乘法结合律 mmatrix_mul_assoc
左乘零分块矩阵性质 mmatrix_mul_zero_l
右乘零分块矩阵性质 mmatrix_mul_zero_r
两次转置性质 mmtrans_same
转置加减性质 mmteq_f
转置乘性质 mmtrans_mul

4 矩阵与分块矩阵形式化证明总结与分析

本节主要对本次研究工作中的证明部分的经验进行总结,并利用具体例子对几个难点进行了详细的分析.
4.1 证明总结

本次有关矩阵函数性质证明的研究工作是在文献[3]的基础上进行的,对其缺少的引理进行了补充证明,在
数量上增加了 10 余条矩阵函数性质,并且部分性质证明难度较高.函数性质证明难度的高低取决于其涉及到的
函数的定义的复杂性,例如矩阵乘法结合律以及矩阵与单位矩阵相乘性质.由于引理证明难度的增加,导致其需
要的辅助引理的数量也大大增加.文献[3]中提供的代码量在 2 000 行左右,本次矩阵与分块矩阵形式化研究工
作在其基础上进行扩充,最后统计有关于矩阵与分块矩阵形式化的代码部分在 10 000 行左右.
无论是在矩阵形式化还是在分块矩阵形式化的研究工作中,都有大量有关函数性质的证明,我们在进行对
函数性质的证明时,主要采用归纳证明的方式进行证明.引理的证明与个人的证明经验挂钩,在证明中有许多的
策略,证明经验能够帮助我们针对不同情况选择不同的证明策略.在对函数性质的证明过程中,我们可以发现一
些函数的潜在问题,然后根据这些问题对函数进行一定调整与修改,并重新对该函数性质进行证明.因此,函数
的构造与函数性质的证明并不是一蹴而就的,而是一个反复的过程.在函数性质证明中发现的函数定义存在问
题,则需要在函数中进行相应调整,在调整后需要对调整后的函数的性质进行重新证明.采用这种方法所产生的
函数能够在很大程度上修正函数定义中存在的问题.当函数定义存在一些难以察觉的问题时,即产生结果正确
却在证明时与引理产生一定冲突和矛盾,此时我们需要重新修改函数的定义.对于部分引理利用当前已有函数
和引理无法完成证明的情况,我们需要构造新的辅助函数并且提出新的辅助引理,辅助函数构造方式的选择也
成为证明途中一个阻碍.在引理的归纳证明中,需要对引理中的变量进行归纳.如何选择归纳变量以及确定变量
归纳的顺序,对于引理的证明来说非常重要,正确的选择能够使得引理更快地得到证明.
下面是我们对本次研究工作中归纳证明时的经验的总结.
• 对必要的变量进行归纳证明.每条引理中存在多个变量,当引理较为复杂时,其中变量的数量也较多,若