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

1888 Journal of Software 软件学报 Vol.32, No.6, June 2021

Fig.4 Implementation principle of mat_mul_mat function
图 4 mat_mul_mat 函数实现原理

根据以上函数以及有关函数输出结果高度与宽度证明性质构造矩阵乘法函数 matrix_mul,其定义如下.
Definition matrix_mul {m n p:nat}(left:Mat A m n)(rightMat A n p):=
let ll:=mat_mul_mat left right in
mkMat A m p ll(height_mat_mul_mat left right)(width_mat_mul_mat left right).
该函数是将 mat_mul_mat 函数以及该函数输出结果的高度与宽度等价性质这 3 部分封装成一个输入为矩
阵类型、输出为矩阵类型函数.
2.4 矩阵函数性质证明
Coq 采用反向推理的方法构造证明,即:在证明一条引理时会产生一个证明目标,需要通过使用一组引理以
及证明命令来产生保证该目标的成立的子目标.当所有子目标已知或为公理时,则完成证明;反之,则需要继续
对子目标进行证明,直到所有的目标都得到证明.对于矩阵函数性质的证明,需要根据矩阵函数内部定义来选择
归纳目标,从而产生符合预期的子目标.此类有关于矩阵的性质证明难点之一在于证明思路的构建,证明思路决
定了变量是否需要归纳以及变量归纳证明的顺序.证明思路需要根据函数内部定义而建立,下面以矩阵乘法右
分配律为例.
矩阵乘法右分配律形式为 A×(B+C)=A×B+A×C,如图 5 所示.

Fig.5 Right distributive law of matrix multiplication function and matrix addition function
图 5 矩阵乘法函数与矩阵加法函数的右分配律

在证明该定理时,需要将变量进行归纳,该定理中的变量有 m,n,A,B,C,在第 2.3 节中介绍矩阵乘法函数
(matrix_mul)定义的实现是由表与表之间的内积函数、表与二维表的乘法函数、二维表与二维表的乘法函数到
矩阵以及矩阵乘法函数(返回二维表)的顺序实现的,如图 6 所示.