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

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

Lemma tm1_cond1:height tm1=3.
Lemma tm1_cond2:width tm1 3.
Definition Tm1:=mkMat nat 3 3 tm1 tm1_cond1 tm1_cond2.
由于构建一个矩阵所需要写的代码过多,因此我们可以将固定尺寸的矩阵构造封装成函数,后期构造时只
需输入矩阵内部元素即可得到所构造的矩阵,如构建 3×3 矩阵函数 mkMat_3_3.
Definition mkMat_3_3′ (a11 a12 a13 a21 a22 a23 a31 a32 a33: A):=
[[a11;a12;a13]; [a21;a22;a23]; [a31;a32;a33]].
Definition cond2_mkMat_3_3′:forall a11 a12 a13 a21 a22 a23 a31 a32 a33,
width(mkMat_3_3′ a11 a12 a13 a21 a22 a23 a31 a32 a33) 3%nat.
Definition mkMat_3_3 (a11 a12 a13 a21 a22 a23 a31 a32 a33:A):=
mkMat A 3 3 (mkMat_3_3′ a11 a12 a13 a21 a22 a23 a31 a32 a33)
eq_refl(cond2_mkMat_3_3′ a11 a12 a13 a21 a22 a23 a31 a32 a33).
其中,eq_refl 是自定义的一个证明目标,其能够自动证明二维表的高度.在此基础上,Tm1 的构建代码大大减
少,如下.
Definition Tm1:=mkMat_3_3 1 2 3 2 3 4 3 4 5.
2.2 矩阵类型等价性质
在文献[3]中,对矩阵类型的等价判断是采用 Coq 中的 eq 函数表示,其采用公理 Meq 作为二维表(即矩阵内
部数据)相等与矩阵相等的转换理论,如下:
Axiom Meq: forall (A:Set) (m n:nat) (m1 m2:Mat A m n), mat A m n m1=mat A m n m2↔m1=m2.
其中:A 为矩阵元素类型;m 和 n 分别为矩阵的高度以及宽度;m1 和 m2 为元素类型为 A、大小为 m×n 的矩阵;mat
是获取矩阵内部二维表的函数,其参数分别为元素类型、矩阵高度、矩阵宽度以及矩阵.由于 eq 函数对于 Record
类型相等要求的特性,即要求 Record 类型中每一条记录相等,而当两个矩阵相等时(即内部数据相等),不要求其
关于该数据的高度以及宽度证明相等,因此该公理存在部分错误,即,由二维表相等无法推导出矩阵相等.
为了解决该公理存在的问题,我们提出了新的矩阵等价判断函数 M_eq,定义如下:
Definition M_eq{A:Set} {m n:nat} (m1 m2:Mat A m n):=mat A m n m1=mat A m n m2.
其实现原理如图 1 所示.

Fig.1 Implementation principle of M_eq function
图 1 M_eq 函数实现原理

该函数用于判断两个矩阵类型中的二维表(即矩阵内部数据)是否相等.该判断方法有效避免了关于 Record
类型使用 eq 函数进行等价判断所存在的问题,也消除其使用错误公理而产生的漏洞.该函数具有自反性、对称
性以及传递性,因此,我们借助 Coq 中的重写扩张机制构建重写性质,使其成为一个重写可用的二元关系.下面使
用“===”标记表示 M_eq 函数.下面是 M_eq 的自反性、对称性和传递性的引理表示.