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

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

的向量和矩阵.在基于依赖类型的定理证明器中,可通过依赖类型定义出可设定长度的表. Magaud 基于依赖类
型定义了带有长度的向量类型,其定义如下:
Inductive vect (A:Set):nat→Set:=
|vnil: vect A 0
|vcons: forall n:nat,A→vect A n→vect A(S n).
该定义与表类型 list 相似,不同在于其增加了一个表示列表长度的参数(类型为自然数).然而,这一技术在操
作和证明上都十分繁琐,不仅无法利用表结构上的各种已知函数,而且当处理更为复杂的二维矩阵问题时,将面
临较大的困难.
在 Coq 的 Coquelicot 库中也有一种矩阵形式化方法 [16] ,该方法与上述方法都基于依赖类型实现了定长向
量,其利用对 pair 函数的递归实现向量,矩阵由向量的嵌套实现.该方法的相比于上述方法构造更加巧妙、易于
理解、矩阵函数的实现简单,但后续函数性质的证明较少.
[3]
马振威提出一种基于 Coq 记录类型的方法来实现矩阵的形式化 ,该方法用包含 3 个分量的记录来表示二
维矩阵,其中一个分量是实现矩阵的二维表,另外两个分量分别是对矩阵的长度和宽度满足指定长宽的两个证
明.这种方式易于理解,能够让我们定义出具有指定长宽的矩阵类型,并且我们能够在向量类型和矩阵类型上定
义基本的矩阵操作函数(矩阵加法、转置、乘法等).文献[3]证明了一组矩阵操作的基本性质.这种实现矩阵形式
化方法的好处在于易于理解并且方便使用,利用该方法构建的函数可直接通过程序抽取得到可执行的 OCaml
代码.但是,在文献[3]中有一个问题没有得到很好的解决,它就是矩阵的相等性问题.对于两个基于记录的矩阵,
传统等号并不能准确表达它们的相等性,因为两个记录相等当且仅当这两个记录的所有分量相等.但对于两个
列表相同的矩阵记录,它们所包含的关于长度和宽度的证明是不必要求相等的.
目前,我们还未看到有关于分块矩阵运算的形式化研究工作.
本文期望在解决基于 Coq 记录类型的方法存在问题的基础上,对更多矩阵函数性质进行补充证明,并且利
用该技术对分块矩阵及其运算形式化,最后不仅能够构建多个不同类型的矩阵形式化的基础库供后续研究人
员使用,还能为从事该研究方向的人员提供一些经验上的参考.

2 矩阵形式化

本次工作所采用的矩阵形式化方法是对文献[3]中的矩阵形式化方法的完善,其中包括矩阵等价定义、部分
矩阵函数修改以及矩阵函数性质的补充证明.本节介绍基于 Coq 记录的矩阵形式化方法,其中矩阵类型定义、
矩阵函数定义方法以及矩阵函数性质证明思路.
2.1 矩阵类型定义

Record 类型是一个允许定义记录的宏,使用 Record 可以定义出一种数据结构.该数据结构中具有一些数据,
而这些数据满足某种性质,如下即为利用 Record 定义的矩阵类型.
Record Mat (A:Set)(m n:nat): Set:=mkMat
{
mat: list (list A);
mat_height: height mat=m;
mat_width: width mat n
}.
其中,A 表示矩阵内部元素类型,m 表示矩阵行数,n 表示矩阵列数,height 函数用于返回二维表的高度,width
函数用于判别输入二维表的宽度是否等于输入参数,mat 用于存储矩阵内部数据即二维表,mat_height 为二维表
的高度的等价证明,mat_width 为二维表的宽度的等价证明.因此,在创建一个大小为 m×n 的矩阵时,需要提供一
个二维表、该二维表的高度性质证明以及该二维表的宽度性质证明.以下是构建一个 3×3 的矩阵 Tm1 的例子.
Definition tm1:=[[1;2;3];[2;3;4];[3;4;5]].