A formalization of the Smith normal form in higher-order logic (Q2102950)

In the paper under review the authors offer a detailed description of their work on formalising in Isabelle/HOL the Smith normal form for matrices over certain classes of rings, although the main focus is on matrices over principal domains and over Bézout rings. Let us start by recalling that for a natural number \(n\in\mathbb{N}\) and a commutative, unitary ring \(R\), a square matrix \(A=(a_{i,j})\in\mathscr{M}_{n,n}(R)\) is in \textit{Smith normal form} (SNF) if it is diagonal and the diagonal entries are ordered by divisibility: in formulæ, \[ \forall\;0\leq i,j\leq n-1,\,i \ne j \Longrightarrow a_{i,j}=0\quad\land\quad \forall\;0\leq i\leq n-2,\,a_{i,i}\mid a_{i+1,i+1}. \] From the formalisation viewpoint, the above definition presents several difficulties, some that are intrinsically related to defining matrices and divisibility in a proof assistant, and some that are somewhat peculiar to the underlying logic of Isabelle/HOL, in particular to the lack of dependent types. The paper details these difficulties and gives a pleasant description of the authors' strategy to tackle them. It also contains some abstract mathematical results, like the nice Theorem 2 of \S 4.2 showing that a ring is Bézout if and only if all diagonal matrices admit a SNF. The general overarching theme is the connection between two different libraries: the HOL Analysis (or HA, for short) and the JNF library, initially developed in [\textit{R. Thiemann} and \textit{A. Yamada}, ``Formalizing Jordan normal forms in Isabelle/HOL'', in: Proceedings of the 5th ACM SIGPLAN international conference on certified programs and proofs, CPP'16. New York, NY: Association for Computing Machinery (ACM). 88--99 (2016; \url{doi:10.1145/2854065.2854073})] in order to formalise the Jordan normal form. Both libraries contain definitions and results allowing to work with matrices, but each comes with advantages and drawbacks. The approach taken by the authors is to develop a bridge between the two libraries: each result is proven in the most suited library, and the bridge allows to port the result to the other one. Independently of their final application to SNF, which is certainly much valuable on its own, the description of the bridge and the analysis of the approach makes the paper of the utmost interest. In the HA library, matrices with coefficients in an arbitrary type \(\alpha\) are defined as functions from a product type \(\texttt{m}\times\texttt{n}\) to \(\alpha\), where \(\texttt{m}\) and \(\texttt{n}\) are finite types representing the indexing sets of rows and columns, respectively. If one wants to discuss SNF for such objects, a notion of ``first row'' (or ``first column'') is needed, as well as the notion of ``successive diagonal term'' with the convention that once the last row, or column, is attained, the subsequent one must be the first. All this is encoded in the notion of a \textit{mod\_type}, whose description is detailed in \S 2.5. Here, the lack of dependent types in HOL shows its limitation: it is difficult to represent a matrix \(A\colon \texttt{m}\Rightarrow\texttt{n}\Rightarrow R\) as a matrix of ``larger size'', say \(\texttt{m}'\Rightarrow\texttt{n}'\Rightarrow R\), or to speak about submatrices of \(A\). More generally, quantifying over the size of matrices, for instance in order to perform some inductive argument, is impossible in the context of simple type theory as long as matrices are implemented as types of the form \(\texttt{m}\Rightarrow\texttt{n}\Rightarrow R\). In the JNF library, on the other hand, a matrix \(A\in\mathscr{M}_{n,m}(R)\) is simply represented by a triple \((n,m,f)\) where \(n,m \colon \mathbb{N}\) are natural numbers (representing the size of \(A\)), and \(f\colon \mathbb{N}\Rightarrow\mathbb{N}\Rightarrow R\) is a function accessing the coefficients of \(A\), so that \(f\,i\,j =a_{i,j}\). Expressed in this way, a submatrix of \((m,n,f)\) is simply a triple \((m_1,n_1,f)\) for suitable \(m_1\leq m\) and \(n_1 \leq n\), and arguing by induction or quantifying over matrix sizes becomes quite smooth. The drawback of the JNF library is that it still lacks many results and notions that are already available in the HA library, like the full treatment of Bézout rings, leading to the necessity of a bridge between the two. This bridge is nicely described in \S 3, while \S 4 and \S 5 contain the algorithms to compute SNF first for diagonal matrices, and then for arbitrary ones. We also call attention to the short, yet interesting, \S 6 where a certifier for SNF is described: this is a tool that \textit{verifies} that a matrix \(\tilde{A}\in\mathscr{M}_{n,m}(R)\), produced by some external oracle, is a SNF of a given matrix \(A\in\mathscr{M}_{n,m}(R)\) through conjugation by two invertible matrices \(P,Q\): this verification is much faster than the computation of \(\tilde{A}\) directly in Isabelle/HOL, and very useful in certain practical applications. Then, \S7 contains a brief description of the uniqueness of the SNF, which clearly only holds up to units: to prove this result, an inductive argument over the size of matrices is performed, an argument for which the JNF library is better suited than HA. The paper closes with a discussion of related works (especially in Coq) in \S8, and with a program for future developments in \S9.