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

DOI10.2168/LMCS-12(2:7)2016MaRDI QIDQ5739892zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cited in

(6)

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

Describes a project that uses

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)