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

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

Fig.6 Structure of the definition of matrix multiplication
图 6 矩阵乘法函数定义结构
由于 matrix_mul 为非递归函数,其与矩阵加法函数的右分配律性质展开后形成的证明目标将作为一条新
待证引理(mat_mul_mat 函数同理),完成该待证引理的证明即可完成该性质的证明.图 7 为 matrix_mul 函数展开
后需要证明的子目标,即 mat_mul_mat 函数与二维表加法函数的右分配律.

Fig.7 Right distributive law of mat_mul_mat function and two-dimensional list addition function
图 7 mat_mul_mat 函数与二维表加法函数的右分配律
由于 mat_mul_mat 是一个非递归函数,其是在 dl_mul_dl 函数的基础之上定义的,主要功能是分别取出两个
输入矩阵中的二维表,并对第 2 个二维表进行转置,再利用 dl_mul_dl 函数对两个二维表进行乘法函数操作,将
T
mat_mul_mat 函数展开化简后得到需要证明的两个子目标,分别是二维表转置函数与二维表加法性质((A+B) =
T
T
A +B )和 dl_mul_dl 函数与二维表加法右分配律性质.
二维表转置函数与二维表加法性质的证明在这部分不详细介绍,dl_mul_dl 函数与二维表加法右分配律如
下,此处以及下文代码部分采用 Section 机制 A,m 和 n 为局部变量(A:Set; m n:nat).
Lemma dl_mul_dl_distr_r: forall m n (a b c:list(list A)),
width a n→width b n→width c n→height b=m→height c=m→
dl_mul_dl a (mat_each′ A add b c)=mat_each′ A add (dl_mul_dl a b)(dl_mul_dl a c).
由于 dl_mul_dl 函数定义在 l_mul_dl 函数之上,利用数学归纳法对二维表变量 a(图 8)进行归纳展开时,当 a
的形式为 a::a0 时,会取出其二维表中的第 1 个子表,并拆分成含有 l_mul_dl 的形式,如下所示.
l_mul_dl a (mat_each′ A add b c):: dl_mul_dl a0 (mat_each′ A add b c)=
list_each A add (l_mul_dl a b) (l_mul_dl a c)
:: mat_each′ A add (dl_mul_dl a0 b) (dl_mul_dl a0 c)
这提示二维表乘法与二维表加法的右分配律定理的证明需要一个新定理的证明支持,即表与二维表乘法
函数 l_mul_dl 与二维表加法的右分配律.
Lemma l_mul_dl_distr_r: forall m n (a:list A) (b c:list(list A)),
length a=n→width b n→width c n→height b=m→height c=m→
l_mul_dl a (mat_each′ A add b c)
=list_each A add (l_mul_dl a b) (l_mul_dl a c).