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

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

对于子目标(8)中的 dlist_i′ A Zero One n (S n) 1 部分,我们需要利用 link1 函数进行化简,其化简引理如下:
Lemma dlist i′ 1: forall m n i ,
_ _link
(9)
′
′
dlist _ i A Zero One ( ) ( )m S n S i = link 1 (list _ o A Zero ) (m dlist _ i A Zero One ).m n i
利用该性质将子目标(8)进行化简,得到:
′
0)) ma =
_
dl _ mul dl A Zero add mul (link 1 (list _ o A Zero ) (n dlist _ i A Zero One n n
(10)
′
_ Zero
dl _ mul dl A add mul (dlist i A One n n ma )
_
Zero
0) (tailcolumn A
观察该子目标,需要证明 dl_mul_dl 函数与 link1(list_o A Zero n)函数之间的关系,其原理如图 28 所示.

Fig.28 Relationship between dl_mul_dl function and link1 function
图 28 dl_mul_dl 函数与 link1 函数的关系
为了使该引理更易证明,将其泛化成以下形式:
_
_
)
,
_ :
Lemma dlist mul unit l forall m n i ma width ma (S n →
′
dl
_ Zero m
)) ma
_ mul dl A add mul (link 1 (list o A ) (dlist i A One m n i (11)
_ Zero
Zero
_
_ ′
= dl _ mul dl A Zero add mul (dlist i A Zero One m n i ) (tailcolumn A ma )
_
完成该引理的证明后,加上一些辅助引理的证明即可完成单位矩阵左乘性质的证明.
整体的证明框架如图 29 所示.

Fig.29 A proof framework for the property of left multiplication of identity matrix
图 29 单位矩阵左乘性质证明框架
由图 29 可知:该单位矩阵左乘性质的证明依赖于 17 个引理的证明,并且每个引理都需要有策略地对多个
变量按一定顺序进行归纳证明,部分引理依赖于其他引理.一个矩阵函数性质的证明过程较为复杂以及繁琐,对
如第 2.4 节中分析的乘法右分配律性质,可以在证明过程中产生较为清晰的证明思路;但对于一些证明思路并
不明显的性质,如本节例子的单位矩阵左乘性质,证明过程中产生的一些引理主要是根据其归纳证明过程中子