Formalized linear algebra over Elementary Divisor Rings in Coq

TL;DR

This paper formalizes linear algebra over elementary divisor rings in Coq, proving key theorems, and developing verified algorithms for Smith normal form computation across various coefficient structures.

Contribution

It introduces a Coq formalization supporting linear algebra over elementary divisor rings, including classification theorems and verified algorithms for Smith normal form.

Findings

Formal proof of classification theorem for finitely presented modules.

Verified algorithms for Smith normal form over multiple coefficient structures.

Extensions of Bézout domains enabling Smith normal form computation.

Abstract

This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend B\'ezout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension $\leq 1$ and well-founded strict divisibility.