Formalization Of Matrices Using Record Type

Matrices are widely used in theoretical mathematics,engineering mathematics and computer sciences.For example,in flight control systems,matrices are used to describe the forces acting on an aircraft,to derive the aerodynamics equations and to design flight control algorithms.Therefore,the correctness of matrix processing algorithms and matrix mathematical derivation have great impact on the reliability of computer systems.Formal methods play an important role in ensuring security and reliability of computer systems.Theorem proving is the most rigorous and powerful formal verification method and it is capable for the verification of mathematical formulas and computer algorithms.Coq is such an interactive high-order theorem prover.It is based on the theory of the Calculus of Inductive Constructions.It is very expressive and has a powerful logic system.It can be used to write specifications and to develop programs that meet the specifications.Coq is suitable for formal verification of programs in systems that require high reliability.Although the standard library of Coq contains a rich set of formalized theories,but it does not have a theory of matrix yet.The expression ability of the scheme based on List is limited,the scheme based on the dependent type List is complex and difficult to verify,and the scheme based on function only verifies the matrix theory,and can not construct the matrix with specific data,nor can they be used for the derivation,verification of the actual matrix and program extraction.This thesis proposes a matrix formalization method based on Record type,which is concise in description,convenient for proof development,easy to use,and feasible for program extraction.The main contribution of this thesis are as follows:Firstly,a vector definition based on Record type is proposed,which contains two fields,one is of the List type and is used to store the data of the vector;another field contains a proof of the property that the length of the list is the same as what is specified.An implementation of matrix is based on this formalism of vectors.Both the design of the matrix manipulation functions and the complexity of the matrix property proofs are simpler than the methods used in other matrix verification work in Coq.Secondly,with the help of functors,we studied a generic method of vector and matrix formalization,which is independent of the types of their elements.Functors can be viewed as parameterised modules,or functions from modules to modules.The input type of a functor is called a signature,which describes the data type of the input module as well as properties proved in themodule.The functor based matrix formalization can utilize properties of its input element module to prove the properties of the matrix.Traditional matrix formalization needs to work on each type of matrix,one by one.With the help of functor,it is possible to give a generic definition for matrices with different element types,and prove matrix properties in a uniform way.Thirdly,on the basis of functor vector and matrix,the formalization of real number matrix and complex number matrix is completed.At the same time,the function domain is formalized,and the function definite integral of binary and ternary is formalized based on Coquelicot library.At last,on the basis of the previous work,the formalized description of function matrix and function matrix calculus and the verification of some properties are given.Finally,we demonstrate the use of this matrix library by the verification of coordinate transformation matrices,and the development of aerodynamic equations for flight control systems.It can be seen from these examples that the matrix based on the Record type is simple to use and it can support the task of formal matrix property verification.