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

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

MM_to_M (matrix_map (Mat A m n) (matrix_map A f1) me)===matrix_map A f1 (MM_to_M me).
3) 分块矩阵转置函数等价引理.
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).
4) 分块矩阵乘法函数等价引理.
Lemma MMmul_eq_Mmul: forall (me:Mat (Mat A m n) m2 n2) (mf:Mat (Mat A n p) n2 p2)
MM_to_M (mmatrix_mul A Zero add mul m n p me mf)
===matrix_mul A Zero add mul(MM_to_M me)(MM_to_M mf).
利用以上引理,可直接将普通矩阵函数所具有的性质移植到分块矩阵的函数之上,无需对分块矩阵函数所
满足的性质一一证明,加快了证明效率.对于证明较为简单的分块矩阵加法交换律,利用归纳证明其证明步骤如
图 22 所示.

Fig.22 Ordinary inductive proof process of addition distributive law of block matrix
图 22 分块矩阵加法分配律的普通归纳证明过程
对于使用分块矩阵函数与普通矩阵函数的等价性的分块矩阵加法交换律证明如图 23 所示.

Fig.23 Proof process of addition distributive law of block matrix using the above equivalence
图 23 分块矩阵加法分配律利用等价性的证明过程