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

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

equal 策略使该目标转化为两部分各自相等的子目标.若对其内部继续进行归纳化简,证明会变得更加复杂繁
琐.因此面对该问题时,我们分析了问题出现的原因并且发现重新思考与 rev 函数相关的函数定义,在该例子中
即为单位矩阵生成函数的定义.
因此,我们不采用文献[3]中所定义的单位矩阵生成函数.虽然该函数产生结果满足我们的要求,但其内部构
造不利于有关单位矩阵的性质证明.因此,我们对其单位矩阵生成函数进行了修改.对于 list_i 函数,我们不决定
修改,原因在于该函数满足我们的要求,并且没有在证明过程中产生阻碍.我们对单位矩阵的二维表的生成函数
做了以下修改.
Fixpoint dlist_i′ m n i:=
match m with
|O⇒List.nil
|S m′⇒List.cons (list_i n (S i)) (dlist_i′ m′ n (S i))
end.
dlist_i′函数的作用是产生一个行数为 m、每行长度为 n 的二维表,dlist_i′ n n 0 即为 n 阶单位矩阵(二维表
类型).在完成函数的构造后,对该函数输出结果(二维表)的高度以及宽度进行等价性证明.下面是对该函数进行
的测试部分,如图 26 所示.
Compute (dlist_i′ nat 0 1 3 3 0) (构建 3 阶单位矩阵):
= [ [1; 0; 0]; [0; 1; 0]; [0; 0; 1] ]
:list (list nat )
Fig.26 Test result of dlist_i′ fucntion
图 26 dlist_i′函数测试结果
经过测试,我们可以看到,该函数所产生的二维表满足单位矩阵的特性.利用上述函数以及性质,将 dlist_i′封
装成单位矩阵生成函数 MI,如下:
Definition MI n:=let ma:=dlist_i′ n n 0 in mkMat A n n ma (height_dlist_i′ n n 0) (width_dlist_i′ n n 0).
在上述无 rev 函数定义的单位矩阵生成函数定义下,对引理(1)进行展开化简,得到如下引理:
Lemma dlist mul unit _ :l′ forall m n (ma list (list A )), height ma = m → width ma n →
_
_
:
(6)
′
_
_dl mul dl A Zero add mul (dlist _ i A Zero One 0) m m gettrans A Zero ma n = ma .
为了使证明更加简单,我们利用转置函数的特性对该引理进行化简,如下:
_
_
Lemma dlist mul unit _ :l′ forall m n (ma list (list A )), height ma = m → width ma n →
:
(7)
′
_dl mul dl A Zero add mul (dlist _ i A Zero One 0) n n ma = gettrans A Zero ma .n
_
下面对该引理进行归纳证明.对变量 n 进行归纳证明时,得到一个子目标如下:
_ ′
_
dl _ mul dl A Zero add mul (dlist i A Zero One n (S n ) 1) ma =
(8)
′
dl _ mul dl A Zero add mul (dlist _ i A Zero One 0) (n n tailcolumn A ma )
_
观察该子目标发现,需要将 dlist_i′ A Zero One n (S n)进行化简.但利用已有函数无法进行化简,因此需要构
造新的函数 link1 来辅助该化简证明.该函数的作用是将一个表左接于一个二维表,其实现原理如图 27 所示.

Fig.27 Implementation principle of link1 function
图 27 link1 函数实现原理