Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. (English) Zbl 1348.68213

Summary: In this contribution we present a formalised algorithm in the Isabelle/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over Bézout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the Bézout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
15A21 Canonical forms, reductions, classification
68W30 Symbolic computation and algebraic computation
Full Text: DOI


[1] Aransay J, Divasón J (2014) Formalization and execution of Linear Algebra: from theorems to algorithms. In: Gupta G, Peña R (ed) Post Proceedings of the international symposium on logic-based program synthesis and transformation: LOPSTR 2013, LNCS, vol 8901. Springer, pp 01-19 · Zbl 1453.68210
[2] Aransay J, Divasón J (2015) Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. J Funct Program 25(e9):21. doi:10.1017/S0956796815000155 · Zbl 1420.68185
[3] Aransay J, Divasón J (2015) Generalizing a Mathematical Analysis library in Isabelle/HOL. In: Havelund K, Holzmann G, Joshi R (eds) Proceedings of the seventh NASA formal methods symposium: NFM 2015 · Zbl 1348.68213
[4] Adelsberger S, Hetzl S, Pollak F (2014) The Cayley-Hamilton theorem. Archive of formal proofs. Formal proof development. http://isa-afp.org/entries/Cayley_Hamilton.shtml. Accessed 30 Apr 2016
[5] Bathe KJ (2003) Computational fluid and solid mechanics. Elsevier Science, Amsterdam · Zbl 1068.76002
[6] Borodin, A; Gathen, J; Hopcroft, JE, Fast parallel matrix and gcd computations, Inf Control, 52, 241-256, (1982) · Zbl 0507.68020
[7] Beineke LW, Wilson RJ (2004) Topics in algebraic graph theory. Encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge
[8] Cano G, Cohen C, Dénès M, Mörtberg A, Siles V (2016) Formalized linear algebra over elementary divisor rings in Coq. Logical methods in computer science (Submitted) · Zbl 1448.68461
[9] Cohen C, Dénès M, Mörtberg A (2013) Refinements for Free! In: Gonthier G, Norrish M (eds) Certified programs and proofs: CPP 2013, of lecture notes in computer science, vol 8307. Springer, pp 147-162
[10] Child D (2006) The essentials of factor analysis. Bloomsbury Academic, New York
[11] Divasón J, Aransay J (2014) Gauss-Jordan algorithm and Its applications. Archive of formal proofs. Formal proof development. http://isa-afp.org/entries/Gauss_Jordan.shtml. Accessed 30 Apr 2016 · Zbl 1453.68210
[12] Divasón J, Aransay J (2015) Echelon form. Archive of formal proofs. http://isa-afp.org/entries/Echelon_Form.shtml, Formal proof development. Updated version available from the AFP repository version: http://www.isa-afp.org/devel-entries/Echelon_Form.shtml. Accessed 30 Apr 2016
[13] Divasón J, Aransay J (2015) QR Decomposition. Archive of formal proofs. Formal proof development. http://isa-afp.org/entries/QR_Decomposition.shtml. Accessed 30 Apr 2016 · Zbl 1420.68185
[14] Dénès M (2013) Formal study of efficient algorithms in linear algebra. Ph.D. thesis, Université Nice Sophia Antipolis
[15] Dénès M, Mörtberg A, Siles V (2012) A refinement-based approach to Computational Algebra in COQ. In: Beringer L, Felty A (eds) Interactive theorem proving: ITP 2012, lecture notes in computer science, vol 7406. Springer, pp 83-98 · Zbl 1360.68745
[16] Eberl M (2015) A decision procedure for univariate real polynomials in Isabelle/HOL. In: Proceedings of the 2015 conference on certified programs and proofs, CPP ’15, New York, NY, USA, pp 75-83 · Zbl 0507.68020
[17] Fuchs L, Salce L (2001) Modules over non-Noetherian domains. Mathematical surveys and monographs. American Mathematical Society, Providence · Zbl 0973.13001
[18] Fukunaga K (2013) Introduction to statistical pattern recognition. Computer science and scientific computing. Elsevier Science, Amsterdam · Zbl 1074.68081
[19] Gamboa R, Cowles J, Van Baalen J (2003) Using ACL2 arrays to formalise matrix algebra. In: Fourth international workshop on the ACL2 theorem prover and its applications
[20] Hales T, Adams M, Bauer G, Tat Dang D, Harrison J, Le Hoang T, Kaliszyk C, Magron V, McLaughlin S, Tat Nguyen T, Quang Nguyen T, Nipkow T, Obua S, Pleso J, Rute J, Solovyev A, Hoai Thi Ta A, Tran TN, Thi Trieu D, Urban J, Khac Vu K, Zumkeller R (2015) Formal proof of the Kepler conjecture CoRR. abs/1501.02155. Accessed 30 Apr 2016
[21] Haftmann F (2016) Code generation from Isabelle/HOL theories. Tutorial documentation. http://isabelle.in.tum.de/dist/Isabelle2016/doc/codegen.pdf. Accessed 30 Apr 2016
[22] Haftmann F (2016) Haskell-style type classes with Isabelle/Isar. Tutorial documentation. http://isabelle.in.tum.de/dist/Isabelle2016/doc/classes.pdf. Accessed 30 Apr 2016
[23] Harrison, J, The HOL light theory of Euclidean space, J Autom Reason, 50, 173-190, (2013) · Zbl 1260.68373
[24] Huffman B, Kunčar O (2013) Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In: Gonthier G, Norrish M (eds) Certified programs and proofs: CPP 2013, lecture notes in computer science, vol 8307. Springer, pp 131-146
[25] Hogben J (2006) Handbook of linear algebra (discrete mathematics and its applications), 1st edn. Chapman & Hall/CRC, Boca Ratón
[26] Jacobson N (2012) Basic algebra I, 2nd edn. Dover Books on Mathematics, Dover Publications, New York · Zbl 0284.16001
[27] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22Nd symposium on operating systems principles, SOSP ’09. ACM, New York, pp 207-220
[28] Lochbihler A, Bulwahn L (2011) Animating the formalised semantics of a Java-like Language. In: van Eekelen M, Geuvers H, Schmalz J, Wiedijk F (eds) Interactive theorem proving (ITP 2011), lecture notes in computer science, vol 6898. Springer, pp 216 - 232 · Zbl 1342.68294
[29] Leon SJ (2014) Linear algebra with applications. Featured titles for linear algebra (introductory) Series. Pearson Education, New Jersey
[30] Liu B, Lai HJ (2000) Matrices in combinatorics and graph theory. Network theory and applications. Springer, Berlin · Zbl 1074.68081
[31] Langville AN, Meyer CD (2011) Google’s Pagerank and beyond: the science of search engine rankings. Princeton University Press, Princeton · Zbl 1270.68005
[32] The MLton website. MLton. a whole program optimizing complier for Standard ML. http://mlton.org/. Accessed 30 Apr 2016
[33] Newman M (1972) Integral matrices. Pure and applied mathematics. Elsevier Science, New York
[34] Narkawicz, A; Muñoz, C; Dutle, A, Formally-verified decision procedures for univariate polynomial computation based on sturm’s and tarski’s theorems, J Autom Reason, 54, 285-326, (2015) · Zbl 1356.68196
[35] Ould Biha S (2010) Mathematical components for groups theory. Ph.D. thesis, Université Nice Sophia Antipolis · Zbl 1005.12004
[36] Pan, VY, Computation of approximate polynomial gcds and an extension, Inf Comput, 167, 71-85, (2001) · Zbl 1005.12004
[37] The Poly/ML website. http://www.polyml.org/. Accessed 30 Apr 2016
[38] Roman S (2007) Advanced linear algebra. Graduate texts in mathematics. Springer, Berlin
[39] Rudnicki, P; Schwarzweller, C; Trybulec, A, Commutative algebra in the mizar system, J Symbolic Comput, 32, 143-169, (2001) · Zbl 1074.68081
[40] Storjohann A (2000) Algorithms for matrix canonical forms. Ph.D. thesis, Swiss Federal Institute of Technology Zurich
[41] Coquand, T; Mörtberg, A; Siles, V, A formal proof of Sasaki-murao algorithm, J Formaliz Reason, 5, 27-36, (2012)
[42] Thiemann R, Yamada A (2015) Matrices, Jordan normal forms, and spectral radius theory. Archive of formal proofs, August. Formal proof development. http://isa-afp.org/entries/Jordan_Normal_Form.shtml. Accessed 30 Apr 2016
[43] Von Neumann J (1955) Mathematical foundations of quantum mechanics. Investigations in physics. Princeton University Press, Princeton
[44] Zill D (2012) A first course in differential equations with modeling applications. Cengage Learning, Boston · Zbl 1330.34007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.