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

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

⎛ cosα 0 − sinα ⎛ cosβ ⎞ − sin β 0⎞ cos *cosα β − ⎛ cos *sinα β − sin β ⎞
⎜ ⎟ ⎜ ⎟ ⎜ ⎟
⎜ 0 1 0 ⎟ ⎜ sin β × cosβ 0 = ⎟ ⎜ sin β cosβ 0 ⎟
⎜ sinα cosα ⎟ ⎜ ⎟ ⎜ sin *cosβ α − sin *sin β α cosα ⎟
⎝ 0 ⎠ ⎝ 0 0 1 ⎠ ⎝ ⎠
图 12 为对该转换矩阵验证的代码部分.

Fig.12 Verification of rotation matrix of airflow coordinate system and stable coordinate system
图 12 气流坐标系与稳定坐标系的旋转矩阵的验证

3 分块矩阵形式化

本节将介绍利用第 2 节中的矩阵形式化方法所构建的分块矩阵形式化方法.由于在第 2 节中的矩阵形式化
方法中所定义的类型、函数以及证明的函数性质都是带多态参数的,因此我们可以利用该多态性构造同样具有
多态性的分块矩阵类型、分块矩阵函数以及证明分块矩阵函数所满足的性质.但我们无法通过函子将矩阵作为
元素类型输入到矩阵模块之中,原因在于:矩阵使用的等价判断函数 M_eq 不适用于分块矩阵;矩阵乘法不具有
乘法交换律,其无法形成一个满足矩阵模块要求的输入元素模块.因此在本节中,我们提出新的分块矩阵的等价
性判别函数、分块矩阵运算函数,并且对分块矩阵函数的性质采用了一种新的方式进行证明.

3.1 分块矩阵类型定义
在分块矩阵类型定义中,我们使用矩阵类型定义的双层嵌套来表示分块矩阵类型定义.根据第 2.1 节中矩
阵类型的定义,当矩阵元素类型为 A 且其高度和宽度分别为 m 和 n 时,其类型表示为 Mat A m n,以该矩阵的类
型作为矩阵内部元素的类型即可构造出一个内部分块大小为 m×n 分块矩阵.图 13 为高度和宽度分别为 m2 和
n2、内部元素为 m×n 矩阵的分块矩阵的内部结构.