Formalized linear algebra over elementary divisor rings in \textsc{Coq}

DOI10.2168/LMCS-12(2:7)2016zbMATH Open1448.68461arXiv1601.07472OpenAlexW3104555329MaRDI QIDQ5739892FDOQ5739892

Authors: Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles 

Publication date: 6 July 2016

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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 $leq1$ and well-founded strict divisibility.

Full work available at URL: https://arxiv.org/abs/1601.07472

Recommendations

• Coherent and Strongly Discrete Rings in Type Theory
• A formalization of the Smith normal form in higher-order logic
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting
• The Smith normal form
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

zbMATH Keywords

Coqformalization of mathematicsSsreflectconstructive algebra

Mathematics Subject Classification ID

Matrices over special rings (quaternions, finite fields, etc.) (15B33) Formalization of mathematics in connection with theorem provers (68V20)

Cited In (6)

• A formalization of Dedekind domains and class groups of global fields
• A formalization of the Smith normal form in higher-order logic
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
• Using abstract stobjs in ACL2 to compute matrix normal forms
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting

Uses Software

• ACL2
• Coq
• homalg
• SINGULAR
• CoqEAL
• Mizar
• Coq/SSReflect

This page was built for publication: Formalized linear algebra over elementary divisor rings in \textsc{Coq}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5739892)