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

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

(add (mul a a2) (product′ A Zero add mul a0 c))

Fig.10 Right distributive law of inner product function and addition
图 10 product 函数与加法的右分配律
这提示表内积函数与加法的右分配律定理的证明需要一个新定理的证明支持,即乘法 mul 与加法 add 的右
分配律:a*(b+c)=a*b+a*c,其表示如图 11 所示.

Fig.11 Right distributive law of multiplication and addition
图 11 乘法与加法的右分配律
大部分的乘法与加法都具有右分配律性质,因此,只要在证明中添加该定理作为前提,即可通过反向推导证
明矩阵乘法与矩阵加法具有右分配性质.
上述依次需要证明的定理整理见表 1.
Table 1 Lemmas needed to prove the right distributive law of matrix multiplication
表 1 矩阵乘法右分配律证明所需引理
序号 引理内容 引理名称
1 乘法与加法的右分配律 mul_distr_r
2 表内积函数与加法的右分配律 product_distr_r
3 表与二维表乘法和二维表加法的右分配律 l_mul_dl_distr_r
4 二维表乘法与二维表加法的右分配律 dl_mul_dl_distr_r
5 矩阵乘法与矩阵加法右分配律 matrix_mul_distr_r

在利用数学归纳法进行归纳证明,尤其当证明的性质中含有多个变量时,不建议在证明开始时盲目地对所
有变量进行统一归纳展开.
• 一是因为在有些变量展开后证明中的前提条件产生假命题.在这种情况下,可以直接跳过该目标证明.
若在该情况下继续进行对其他变量进行归纳展开,会增加许多重复代码与不必要的证明工作;
• 二是对于变量是否进行归纳展开主要依据在于证明思路,如在图 8 中含有 3 个变量:a,b 和 c,选择 a 作
为主要归纳对象的原因在于 dl_mul_dl 函数在运算过程中首先对左侧变量进行模式匹配,当 a 归纳为
不同结构时,可进行化简并且能够进一步产生与 l_mul_dl 函数相关引理的形式.若先对 b 或 c 进行归纳,
不仅不能进一步化简,还会使得证明目标变得更加繁琐.
但对于一些更为复杂的引理,如乘法结合律以及单位矩阵乘矩阵性质,没有明确的证明思路时,需要构造特
殊的函数以及引理来支持其每一个归纳证明目标的证明,这使得这些引理的证明更加复杂并且难以理解,具体
的部分我们将在第 4 节详细讨论.