Computer Science ›› 2019, Vol. 46 ›› Issue (7): 139-145.doi: 10.11896/j.issn.1002-137X.2019.07.022

• Software & Database Technology • Previous Articles     Next Articles

Matrix Formalization Based on Coq Record

MA Zhen-wei1,CHEN Gang1,2   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210000,China)1
    (Beijing Jinghang Research Institute of Computing and Communication,Beijing 100074,China)2
  • Received:2018-06-01 Online:2019-07-15 Published:2019-07-15

Abstract: 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.

Key words: Coq, Matrix, Formal verification, Theorem proving, Record type

CLC Number: 

  • TP311
[1] 吴森堂.飞行控制系统[M].北京:北京航空航天大学出版社,2013.
[2] Cook M V.Flight Dynamic Principles[M].British:Butterworth-Heinemann,2007:20-33.
[3] CHLIPALA A.Certified Programming with Dependent Types:A Pragmatic Introduction to the Coq Proof Assistant[M].The MIT Press,2011.
[4] TEAM T C D.The Coq Proof Assistant Reference Manual -- Version V8.7.1[C]∥INRIA.2016.
[5] NIPKOW T,WENZEL M,PAULSON L C.Isabelle/HOL:a proof assistant for higher-order logic[C]∥Springer-Verlag,2002:xiii-xiv.
[6] SHI Z,SONG X,ZHANG J,et al.Formalization of Matrix Theo- ry in HOL4[J].Advances in Mechanical Engineering,2014,56(5):1-14.
[7] HARRISON J.A HOL theory of euclidean space[C]∥International Conference on Theorem Proving in Higher Order Logics.Springer-Verlag,2005:114-129.
[8] MCBRIDE C.Epigram:Practical Programming with Dependent Types[M]∥Advanced Functional Programming.Springer Berlin Heidelberg,2005:130-170.
[9] MAGAUD N.Programming with Dependent Types in Coq:a Study of Square Matrices[C]∥Unpublished.2005.
[10] WILSON S,FLEURIOT J,SMAILL A.Inductive Proof Automation for Coq[R].England:The University of Edinburgh,2010:3-9.
[11] DENES M,BERTOT Y.Experiments with computable matrices in the Coq system[R].France:INRIA,2011:2-27.
[12] MULLEN E,PERNSTEINER S,WILCOX J R,et al.Euf:minimizing the Coq extraction TCB[C]∥The ACM Sigplan International Conference.ACM,2018:172-185.
[13] SOZEAU M,TABAREAU N.Universe Polymorphism in Coq[M]∥Interactive Theorem Proving.Cham:Springer,2014:499-514.
[14] ZILIANI B,SOZEAU M.A unification algorithm for Coq featuring universe polymorphism and overloading[C]∥ACM Sigplan International Conference on Functional Programming.ACM,2015:179-191.
[15] KREBBERS R,SPITTERS B.Type classes for efficient exact real arithmetic in Coq[J].Logical Methods in Computer Science,2013,9(1):51-59.
[16] BOLDO S,LELAY C,MELQUIOND G.Coquelicot:A User- Friendly Library of Real Analysis for Coq[J].Mathematics in Computer Science,2015,9(1):41-62.
[1] WANG Xia, PENG Zhi-hua, LI Jun-yu, WU Wei-zhi. Method of Concept Reduction Based on Concept Discernibility Matrix [J]. Computer Science, 2021, 48(1): 125-130.
[2] SUN Xiao-xiang, CHEN Zhe. Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving [J]. Computer Science, 2021, 48(1): 268-272.
[3] HAN Xiao-dong, GAO Fei, ZHANG Li-wei. Novel Real-time Algorithm for Critical Path of Linear Network Coding [J]. Computer Science, 2020, 47(9): 232-237.
[4] LI Yu-rong, LIU Jie, LIU Ya-lin, GONG Chun-ye, WANG Yong. Parallel Algorithm of Deep Transductive Non-negative Matrix Factorization for Speech Separation [J]. Computer Science, 2020, 47(8): 49-55.
[5] SANG Bin-bin, YANG Liu-zhong, CHEN Hong-mei, WANG Sheng-wu. Incremental Attribute Reduction Algorithm in Dominance-based Rough Set [J]. Computer Science, 2020, 47(8): 137-143.
[6] LIU Jun-liang, LI Xiao-guang. Techniques for Recommendation System:A Survey [J]. Computer Science, 2020, 47(7): 47-55.
[7] LI Xiang-li, JIA Meng-xue. Nonnegative Matrix Factorization Algorithm with Hypergraph Based on Per-treatments [J]. Computer Science, 2020, 47(7): 71-77.
[8] LIU Zi-qi, GUO Bing-hui, CHENG Zhen, YANG Xiao-bo and YIN Zi-qiao. Science and Technology Strategy Evaluation Based on Entropy Fuzzy AHP [J]. Computer Science, 2020, 47(6A): 1-5.
[9] WU Chong-ming, WANG Xiao-dan, XUE Ai-Jun and LAI Jie. Multiclass Cost-sensitive Classification Based on Error Correcting Output Codes [J]. Computer Science, 2020, 47(6A): 89-94.
[10] TANG Jia-lin, ZHANG Chong, GUO Yan-feng, SU Bing-hua and SU Qing-lang. Color Difference Correction Algorithm Based on Multi Colors Space Information [J]. Computer Science, 2020, 47(6A): 157-160.
[11] MA Hai-Jiang. Recommendation Algorithm Based on Convolutional Neural Network and Constrained Probability Matrix Factorization [J]. Computer Science, 2020, 47(6A): 540-545.
[12] ZHAO Xue-yuan, ZHOU Shao-lei, WANG Shuai-lei and YAN Shi. Formation Containment Control of Multi-UAV System Under Switching Topology [J]. Computer Science, 2020, 47(6A): 577-582.
[13] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[14] CUI Kai, ZHAO Guo-liang, ZHOU Kuan-jiu, LI Ming-chu. Model of Embedded Software for Solving Concurrent Defects [J]. Computer Science, 2020, 47(6): 24-31.
[15] LIU Shu-jun, WEI Lai. Block Integration Based Image Clustering Algorithm [J]. Computer Science, 2020, 47(6): 170-175.
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[2] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[3] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[4] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[5] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[6] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[7] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[8] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[9] CUI Qiong, LI Jian-hua, WANG Hong and NAN Ming-li. Resilience Analysis Model of Networked Command Information System Based on Node Repairability[J]. Computer Science, 2018, 45(4): 117 -121 .
[10] WANG Zhen-chao, HOU Huan-huan and LIAN Rui. Path Optimization Scheme for Restraining Degree of Disorder in CMT[J]. Computer Science, 2018, 45(4): 122 -125 .