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

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

Fig.20 Implementation principle of the MM_to_M function
图 20 MM_to_M 函数的实现原理
以分块矩阵转置函数和普通矩阵转置函数为例,首先,利用定义好的分块矩阵转置函数对分块矩阵进行转
置;然后将其结果通过分块矩阵与矩阵的转换函数转换为矩阵,证明其等价于先转换为矩阵再进行矩阵转置得
到的结果.其内容如图 21 所示.

Fig.21 Proof of the equivalence of transposed function of block matrix
图 21 分块矩阵转置函数等价性证明思路
分块矩阵转置函数等价引理表示如下:
Lemma MMtrans_eq_Mtrans: forall (me:Mat (Mat A m n) m2 n2)
MM_to_M(mmtrans A Zero m n me)===trans A Zero (MM_to_M me).
该引理的证明依赖于一个重要的基础引理,即二维表的横向连接函数和二维表转置函数的关系,若完成该
引理的证明,即可完成上述分块转置函数等价引理的证明.其表示如下.
forall (A: Set) (Zero: A) (h1 h2 w: nat) (ma mb: list (list A)),
height ma=h1→height mb=h2→width ma w→width mb w→
gettrans A Zero (ma++mb) w=mlink A (gettrans A Zero ma w) (gettrans A Zero mb w).
其中,gettrans 是对二维表的转置,“++”代表 app 函数表示表的连接,mlink 表示二维表的左右连接.该引理用
⎡⎤ T
A
T
数学的方法表示为 ⎢⎥ = [A B T ].在该证明中所遇到的困难之处将在第 4.2 节详细讨论.
B
⎣⎦
在分块矩阵函数等价性证明部分,我们成功证明了以下 3 个分块矩阵函数等价性引理,具体如下.
1) 分块矩阵加减运算函数等价引理.
Lemma MMf_eq_Mf: forall (me mf:Mat (Mat A m n) m2 n2),
MM_to_M (matrix_each (Mat A m n) (matrix_each A f) me mf)
===matrix_each A f (MM_to_M me) (MM_to_M mf).
2) 分块矩阵取负运算函数等价引理.
Lemma MMm_eq_Mm: forall (me:Mat (Mat A m n) m2 n2),