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

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

对每个变量都进行归纳,会加大证明的困难程度.因此,对于一些不必要变量可以不用归纳,归纳变量的
选择由该引理中的函数定义结构决定.在对一个变量进行归纳证明时,重复同样证明操作即表示该变
量有可能存在不必要的归纳;
• 归纳变量顺序可变动(根据经验以及具体例子而定).归纳变量顺序不同,所依赖的证明思路也有所不
同.在本次工作中,主要采用由高度-宽度-二维表的归纳顺序进行归纳证明.对于一些涉及特殊函数的
引理,需要观察其函数内部定义结构,从而选择有利于进一步化简的变量进行归纳;
• 根据归纳变量所产生的归纳条件进行化简拆分,得到归纳条件中的形式,再进行重写证明.遇到无法证
明的引理,存在两种情况:1) 引理本身存在矛盾,这可能由引理本身描述错误或函数定义存在问题导致
引理中产生冲突或无法证明的情况;2) 当前函数以及引理无法满足其证明化简的要求.对于第 2)种情
况,则需要考虑构造新的函数以及引出新引理进行化简证明.在下一小节中,将详细分析这两种情况;
• 引理的等价变换和泛化,在引理的证明中起到一个重要的作用.当我们证明一个引理时,可能会产生多
个子目标,若当前子目标则需要新的化简后才可证明,则需要将该化简泛化为一个引理.同样,我们对于
一个引理的证明中也可以依据该引理涉及到的函数性质对函数做一些等价转换,以达到在一定程度
上简化证明步骤的目的.
4.2 难点分析
对于上一小节中我们所提及的引理证明存在的两种情况,将在下面以例子详细解释.
1) 由函数定义引起引理无法证明的情况
引理本身存在矛盾这种情况可能由两种原因导致:一种是引理本身描述错误,这可以通过检查发现错误的
原因并且对其进行修改;第 2 种是引理内部涉及的函数定义不合理而导致引理产生矛盾或者是无法证明的情
况,这需要对函数定义进行修改.下面以单位矩阵左乘性质为例分析第 2 种原因.
文献[3]中采用的单位矩阵生成函数 MI 由以下几个函数构成.
list_i 函数的作用是产生一个长度为 n 的表,其中,第 i 个元素为 1,其余元素为 0,如 list_i 4 3=[0;0;1;0].其定
义如下.
Fixpoint list_i n i:=
match n,i with
|O,_⇒List.nil
|S n′,O⇒List.cons Zero (list_i n′ O)
|S n′,S O⇒List.cons One (list_i n′ O)
|S n′, S i′⇒List.cons Zero (list_i n′ i′)
end.
dlist_i 函数的作用是产生一个类型为二维表的单位矩阵,其中,参数 n 表示产生单位矩阵的阶数,dlist_i 3=
[[1;0;0];[0;1;0];[0;0;1]].其定义如下.
Fixpoint dlist_i′ n i:=
match i with
|O⇒List.nil
|S i′⇒List.cons (list_i n i) (dlist_i′ n i′)
end.
Definition dlist_i n:=List.rev (dlist_i′ n n).
单位矩阵生成函数 MI 定义如下:
Definition MI n:=let m:=dlist_i n in mkMat A n n m (dlist_i_length n) (all_len_n_dlist_i n).
该定义从结果上显示是正确的,即对于任意参数 n,都可产生 n 阶单位矩阵.但其定义中所使用的 rev 函数却
在后期证明中成为证明的一大阻碍,rev 函数的作用是将一个表内元素进行逆向排放,下面以单位矩阵左乘性质