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

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

Fig.32 Problems caused by mlink constructed using link function
图 32 使用 link 函数构造的 mlink 所产生的问题
其原因在于,mlink 利用第 1 个二维表的宽度作为递归参数,利用 headcolumn 以及 tailcolumn 函数将二维表
按列分割,跟二维表的归纳方式不同(按行分割),因此不利于后续归纳证明.在该情况下,即使对所有涉及到的变
量进行多次归纳仍难以化简,并且给证明制造了更多的困难.因此,虽然该函数的定义所产生的结果满足我们的
需求,但由于无法证明后续引理,我们选择了第 2 种定义.
第 2 种定义主要使用辅助函数 app 来辅助 mlink 的构造,该定义较第 1 种定义更为简单,无需提供输入参数
中第 1 个二维表的宽度,并且后续的一系列有关于该函数的引理都可以顺利证明.
在后续的证明中,仍需要构造新的辅助函数以及大量辅助引理以支撑证明.在分块矩阵函数等价性证明中,
还需要构造两个辅助函数,分别是 headcolumn_n 以及 tailcolumn_n.这两个函数的作用分别是取二维表前 n 列、
取二维表除前 n 列以外剩余的列数,这两个函数主要起过渡作用,用于建立部分函数之间的关系.
在矩阵和分块矩阵形式化研究工作中,通常函数定义无法一步到位,一个函数的实现有多种方式,一开始定
义的函数看起来正确,但是具有一些潜在问题难以发现,在后期性质证明时产生冲突或无法证明,则要思考是否
需要修改函数定义;性质证明无法一步到位,在证明一个引理时往往需要多个引理以支撑.这些性质可以分为辅
助引理与关键引理,当目前无引理可帮助化简证明时,需要构造过渡函数以创建新的引理进行进一步化简证明,
如 link1 函数、headcolumn_n 函数以及 tailcolumn_n 函数.此时,辅助引理的构造方式也需要在后续证明中选择;
定义与证明同时进行时,遇到证明失败时难以确定是函数定义问题还是证明策略问题,需要在不断的尝试中进
一步理解问题所在.

5 总 结

利用 Coq 定理证明器中的 Record 类型所实现的矩阵形式化方法与其他矩阵实现方法相比,其实现更加简
洁且更容易理解,使用起来也更加方便,并且可以使用代码抽取机制将经过验证的函数抽取为可执行的 OCaml
代码.我们在完善了矩阵形式化方法的基础上,为矩阵函数的引理进行了补充证明,并且建立了基于不同类型的
矩阵基础库,具体包括实数矩阵库、整数矩阵库、复数矩阵库以及函数矩阵库.后续在矩阵形式化方法的基础
上实现分块矩阵形式化方法,其能够实现将高阶矩阵运算转换为多个低阶矩阵运算.在后续有关于分块矩阵形