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

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

引理为例具体说明.
对于需要证明的单位矩阵左乘性质引理如下:
_
:
Lemma matrix mul unit l : forall {m n nat } (ma Mat A m n ),
:
(1)
_
matrix mul (MI ) m ma == ma .
其中,matrix_mul 为矩阵乘法函数,MI 为单位矩阵生成函数(MI m 代表 m 阶单位矩阵),ma 代表 m×n 的矩阵.该
引理所表示的性质为:单位矩阵与矩阵相乘结果等于矩阵本身.
在证明 matrix_mul_unit_l 引理时,首先对已封装的处理矩阵的函数(matrix_mul,MI)以及矩阵相等判断函数
(M_eq)展开,并进行一些变换操作化简成有关于二维表类型的引理,引理整理后如下:
:
_
Lemma dlist mul unit _ :l′ forall m n (ma list (list A )), height ma = m → width ma n →
_
(2)
′
_
_dl mul dl A Zero add mul (rev (dlist _ i A Zero One )) (m m gettrans A Zero ma )n = ma .
其中,gettrans 是对二维表的转置函数,其带有 4 个参数,分别为二维表内元素类型 A、A 类型中零的表示、二维
表以及二维表的宽度.引理(2)等号左侧的结构看起来非常复杂,为了简化引理,我们证明了 dl_mul_dl 函数与 rev
函数的关系,具体如图 24 所示.

Fig.24 Relationship between dl_mul_dl function and rev function
图 24 dl_mul_dl 函数与 rev 函数的关系
接着,使用该引理对引理(2)进行化简并为新的证明目标,如下:
_
_
:
Lemma dlist mul unit _ :l′ forall m n (ma list (list A )), height ma = m → width ma n →
(3)
_ ′
rev ( _dl mul dl A Zero add mul (dlist i A Zero One m m ) (gettrans A Zero ma n = ma .
_
))
由于 rev 函数对一个参数使用两次后的结果等于其本身,我们将等式两边都使用 rev 函数以消除左侧的 rev
函数,并对等式左侧 ma 的转置项(gettrans A Zero ma n)替换为普通二维表.该化简的目的是为了减少引理等号
左侧的复杂性,并将其转移至引理等号右侧.最终需要进行归纳证明的引理如下:
Lemma dlist mul unit l′ forall m n (ma list (list A )), height ma = m → width ma n →
_
_ :
_
:
(4)
_ ′
dl _ mul dl A Zero add mul (dlist i A Zero One n n ma = rev (gettrans A Zero ma n ).
_
)
在该引理的归纳证明中,我们需要对 n 和 ma 两个变量进行归纳,在 n=S n 和 ma=a::ma 时,化简后得到如下
形式子目标:
( )( )) ( :: ma
_ Zero
_
l _ mul dl A add mul (list i A One S n S n a )
Zero
′
( ) ) ( :: ma =
_
Zero
:: dl mul dl A add mul (dlist i A One S n n a ) (5)
_
_ Zero
)
rev (gettrans A Zero (tl a tailcolumn A ma n ++ (hd Zero a headcolumn A Zero ma ):: nil
)
::
::
该子目标看起来较为复杂,但其整体形式为 a::A=B++(b::nil),如图 25 所示.

Fig.25 Proof problem caused by rev function
图 25 rev 函数引起的证明问题
该问题产生的原因在于 rev 函数,rev 函数将 a::ma 形式的参数转变为 ma++(a::nil)形式,其中,++为 app 函数
用于连接两个表.而我们通常对该类问题进行证明时,采用一定方法将子目标化简为 a::A=b::B 形式,再利用 f_