基于Coq记录的矩阵形式化方法

Matrix Formalization Based on Coq Record

矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制。Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂。针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质。基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证。同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便。

Matrix has a wide range of applications in engineering systems,and the correctness of matrix operations has an important impact on the reliability of engineering systems.Coq is a powerful higher-order theorem prover based on the typeλcalculus.Although the Coq type system can describe variable-sized dynamic data types well,there is a lack of satisfactory description mechanisms for data types such as fixed-size vectors and matrices.At present,there is no vector library or matrix library in the Coq library,so it is more difficult to use Coq to formally verify the theorem or algorithm involving the matrix.In order to solve these problems,this paper proposed a matrix implementation method based on Record type,defined a set of basic matrix functions and proved their basic properties.The verification of the flight control transformation matrix can be done easily by using the matrix types and related lemmas provided in this paper.Compared with other matrix implementation methods,this method is not only relatively simple to implement,but also simpler and more convenient to use.