## Formalizing Refinements and Constructive Algebra in Type Theory

##### Abstract

The extensive use of computers in mathematics and engineering has led to an increased demand for reliability in the implementation of algorithms in computer algebra systems. One way to increase the reliability is to formally verify that the implementations satisfy the mathematical theorems stating their specification. By implementing and specifying algorithms from computer algebra inside a proof assistant both the reliability of the implementation and the computational capabilities of the proof assistant can be increased. The extensive use of computers in mathematics and engineering has led to an
increased demand for reliability in the implementation of algorithms in com-
puter algebra systems. One way to increase the reliability is to formally verify
that the implementations satisfy the mathematical theorems stating their spe-
cification. By implementing and specifying algorithms from computer algebra
inside a proof assistant both the reliability of the implementation and the com-
putational capabilities of the proof assistant can be increased.The extensive use of computers in mathematics and engineering has led to an
increased demand for reliability in the implementation of algorithms in com-
puter algebra systems. One way to increase the reliability is to formally verify
that the implementations satisfy the mathematical theorems stating their spe-
cification. By implementing and specifying algorithms from computer algebra
inside a proof assistant both the reliability of the implementation and the com-
putational capabilities of the proof assistant can be increased.
This first part of the thesis presents a framework, developed in the interact-
ive theorem prover C OQ , for conveniently implementing and reasoning about
program and data refinements. In this framework programs defined on rich
dependent types suitable for proofs are linked to optimized implementations
on simple types suitable for computation. The correctness of the optimized
algorithms is established on the proof-oriented types and then automatically
transported to the computation-oriented types. This method has been ap-
plied to develop a library containing multiple algorithms from computational
algebra, including: Karatsuba’s polynomial multiplication, Strassen’s matrix
multiplication and the Sasaki-Murao algorithm for computing the character-
istic polynomial of matrices over commutative rings.
The second part of the thesis presents the formalization of notions from
constructive algebra. Focus is on the theory of coherent and strongly discrete
rings, which provides a general setting for developing linear algebra over rings
instead of fields. Examples of such rings include Bézout domains, Prüfer do-
mains and elementary divisor rings. Finitely presented modules over these
rings are implemented using an abstraction layer on top of matrices. This
enables us to constructively prove that the category of these modules form a
suitable setting for developing homological algebra. We further show that any
finitely presented module over an elementary divisor ring can be decomposed
to a direct sum of a free module and cyclic modules in a unique way.
This first part of the thesis presents a framework, developed in the interactive theorem prover Coq, for conveniently implementing and reasoning about program and data refinements. In this framework programs defined on rich dependent types suitable for proofs are linked to optimized implementations on simple types suitable for computation. The correctness of the optimized algorithms is established on the proof-oriented types and then automatically transported to the computation-oriented types. This method has been applied to develop a library containing multiple algorithms from computational algebra, including: Karatsuba’s polynomial multiplication, Strassen’s matrix multiplication and the Sasaki-Murao algorithm for computing the characteristic polynomial of matrices over commutative rings.
The second part of the thesis presents the formalization of notions from constructive algebra. Focus is on the theory of coherent and strongly discrete rings, which provides a general setting for developing linear algebra over rings instead of fields. Examples of such rings include Bézout domains, Prüfer domains and elementary divisor rings. Finitely presented modules over these rings are implemented using an abstraction layer on top of matrices. This enables us to constructively prove that the category of these modules form a suitable setting for developing homological algebra. We further show that any finitely presented module over an elementary divisor ring can be decomposed to a direct sum of a free module and cyclic modules in a unique way. This decomposition gives a decision procedure for testing if two finitely presented modules are isomorphic.

##### Parts of work

A Refinement-Based Approach to Computational Algebra in Coq. Maxime Dénès, Anders Mörtberg and Vincent Siles. In Interactive Theorem Proving, volume 7406 of Lectures Notes in Computer Science, pages 83–98. Springer, 2012. Refinements for free!. Cyril Cohen, Maxime Dénès and Anders Mörtberg. In Certified Programs and Proofs, volume 8307 of Lecture Notes in Computer Science, pages 147–162. Springer, 2013. A Formal Proof of Sasaki-Murao Algorithm. Thierry Coquand, Anders Mörtberg and Vincent Siles. Journal of Formalized Reasoning, 5(1):27–36, 2012. Coherent and Strongly Discrete Rings in Type Theory. Thierry Coquand, Anders Mörtberg and Vincent Siles. In Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 273–288. Springer, 2012. A Coq Formalization of Finitely Presented Modules. Cyril Cohen and Anders Mörtberg. In Interactive Theorem Proving, volume 8558 of Lecture Notes in Computer Science, pages 193–208. Springer, 2014. Formalized Linear Algebra over Elementary Divisor Rings in Coq. Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg and Vincent Siles. Preprint, 2014.

##### Degree

Doctor of Philosophy

##### University

Göteborgs universitet. IT-fakulteten

##### Institution

Department of Computer Science and Engineering ; Institutionen för data- och informationsteknik

##### Disputation

Fredagen den 12 december 2014, kl. 10:00, rum ED, EDIT byggnaden, Rännvägen 6B, Chalmers Tekniska Högskola

##### Date of defence

2014-12-12

anders.mortberg@cse.gu.se

##### Date

2014-11-21##### Author

Mörtberg, Anders

##### Keywords

Formalization of mathematics

Refinements

Constructive algebra

Type theory

Coq

SSReflect

##### Publication type

Doctoral thesis

##### ISBN

978-91-982237-0-5

##### Series/Report no.

115D96

##### Language

eng