A Formalization of the Smith Normal Form in Higher-Order Logic

The Smith normal form (SNF) is a well-known canonical form of matrices [51]. It is commonly defined for matrices whose coefficients belong to a principal ideal domain (from here on, PID). A matrix is in SNF if its diagonal elements \(\alpha _i\) satisfy \(\alpha _i\ |\ \alpha _{i+1}\) (note that every number divides 0 and 0 only divides itself) and the rest of the elements of the matrix are zeros. Over a PID, there exists an algorithm to transform a matrix A into its corresponding Smith normal form S by means of invertible matrices, i.e., there exist invertible matrices P and Q such that \(S = P\!AQ\). The Smith normal form plays an important role in different fields, such as control theory [42], combinatorics [50] and structure of lattice rules [41]. Another important application arises in algebraic topology, since it can be used to compute the homology of a chain complex. More generally, it is useful to compute persistent homology, which can be applied to process big volume of data [48] and to the analysis of digital images [8].

In this work, we present a formalization of several facts related to the SNF of a matrix in Isabelle/HOL. We present two algorithms (one is specific to transform a diagonal matrix into Smith normal form, the other one works for arbitrary matrices), together with some theorems on the underlying structures and uniqueness of the transformation. A very important part of this contribution is how it has been obtained in a context where submatrices play an important role and the underlying logic (HOL) does not feature dependent types. Throughout the paper we present the work that we have carried out involving two matrix representations, the one presented in the HOL Analysis library (where matrices are encoded as functions over finite types) and another one by Thiemann and Yamada [53], where a matrix is modeled by a function that maps natural numbers (the indices) to elements, together with two natural numbers that correspond to its dimensions. Depending on the algorithm that we want to verify or the theorem that we wish to prove, we carry out the formal proof in one of the representations (either because it is easier or simply impossible in the other representation), and later we move the results (maybe including intermediate steps or sometimes just the final result) to the other one. To this end, we crucially rely on the lifting and transfer package [33] and above all on local type definitions, a sound extension of HOL [39]. Thus, our work provides an interesting case study of how to use these novel Isabelle/HOL tools to overcome the expressivity problem that HOL has no dependent types. This approach was already carried out in a similar context [22], but the new connection goes one step further and permits reusing more results and combining algorithms of different libraries, which were not possible before.

The outline of the paper is as follows. In Sect. 2, we introduce the ring structures that we formalized and also present a brief introduction to Isabelle. The Isabelle matrix libraries and the required infrastructure are also explained there. In the following sections we show the main contributions of this paper:We then present an overview of related work in Sect. 8. Finally, Sect. 9 shows the conclusions. The formalization is publicly available in the Archive of Formal Proofs [17] and comprises over 14,000 lines of code.

In a work on the Perron–Frobenius theorem [22], there has been a collaboration on the connection between the basics of the HA and the JNF libraries by means of the lifting and transfer package, whenever the indices in the HA library are modeled by finite types (class ). More concretely, that work defines functions to convert, among others, indices and matrices between both representations. For instance, a function is defined for the indices, which is an arbitrary bijection between and the set of all elements of the finite type . Analogously, its inverse function is defined as .¹ Note that both functions have nothing to do with the morphisms and presented previously: the latter ones belong to the class and they are strictly monotonic functions. Then, indices in both representations are related as follows:

In a similar way, matrices in the JNF and the HA libraries are related:

In the definition, is the function that converts a matrix in HA to its corresponding one in JNF, is the access operator for matrices and vectors in HA.

Then, transfer rules like the following one are proved:

This rule means that given two matrices \(A_1\) and \(A_2\) in the JNF library related to the HA matrices \(B_1\) and \(B_2\), respectively (via ), then if matrix addition is invoked in JNF ( \(A_1\) \(A_2\)) the result is related to the matrix addition in HA ( \(B_1\) \(B_2\)). Transfer rules permit one to partly automate the process of sharing statements between both libraries. Putting that work together with the use of local type definitions, we can move results from one library to the other one (in a bidirectional way) if the matrix dimensions are of type [22,  Sect. 4]. Local type definitions are the key, since they allow us to define types dynamically in proof contexts, which are mainly necessary to convert the numerical matrix dimensions in JNF into finite types in HA. More concretely, they permit one to get rid of some type class restrictions and type variables in the theorems that appear while transferring results from HA to JNF. For instance, they are used to transform statements with conditions about the type class (such as ) to simply \(i<n\) where n is a free variable.

However, the class plays an important role in this work about the SNF when working with the HA library, since, similarly as in our previous works, many times the matrix dimensions cannot be modeled by (only) a finite type, but they also must satisfy additional properties. For instance, in this work we need to introduce the definition of the SNF in HA:

The predicate is used to impose the matrix A to be diagonal. The functions and obtain the number of rows and columns of a matrix in HA. The input matrix A has type . In the definition, the quantified variables a and b are used for referring to the indices of the rows (of type with the restriction) and columns (of type and with the restriction too), respectively. Let us remark that a and b do not have the same type. This means that we cannot write when referring to the diagonal elements. Neither we can assume \(a=b\). On the contrary, we have to work with and thus, the restriction is added as a premise in the first condition. Let us also note that, given an index a, we refer to the next position as \(a+1\). This is possible since the class assumes the existence of a sum operation (class ) and some basic arithmetical properties. In addition, demands the morphisms and to be strictly monotonic increasing functions. This property does not hold with , and in our case is very convenient since we can deduce useful properties, such as . Thanks to properties like this one, the class is very useful in our previous works and, as seen above, also required in this particular development since it allows one to impose easily the divisibility condition of diagonal elements when defining the Smith normal form predicate in HA.

Thus, it is desirable to be able to move statements between both libraries, even if the matrix dimensions require the restriction in HA. With the previously existing connection [22], this is not possible (if one tries it, one would get proof obligations like when proving the required transfer rules for some definitions, which do not necessarily hold). To circumvent this problem, we developed a new bridge which connects the HA library with JNF, but using the morphisms and from the class , so that we can relate theorems and algorithms that possess such a class restriction over the indices of the matrices, and, concretely, we will be able to transfer our algorithms and results about the SNF between both representations.

We define the new relations between indices, vectors and matrices (involving ) in HA and JNF ( , , and , respectively) and prove new transfer rules for the basic operations such as matrix addition, determinants and so on.

Let us show the process to transfer statements from HA to JNF by means of a guided example. The following statement is proved in HA with the restriction. It simply states that the first element of a square matrix in SNF divides any other element of the matrix.²

Note that we use 0 (which is of type ) to represent the first element of the type and then, is used to access to the first element of the matrix. However, if one only requires instead of for the type , we would not know if 0 is the first element of the type ; indeed, we would not know if the type has a 0 as one of its elements.

The first step is to define the notion of SNF in the JNF library:

The definition is very similar to the one in HA. Here, the symbol is used to represent the access operator for matrices in JNF and is the predicate in JNF that requires the input matrix A to be a diagonal matrix.

Now, we prove transfer rules to relate the definitions involved in the statement, in this case we relate the definitions and .

Let us recall that this lemma states that whenever a matrix A in JNF and a matrix B in HA are related (via ), then A and B are equal (related by the equality relation). The difficulty of a transfer rule depends on the number of definitions and operations that are involved as well as the similarity between the definitions in HA and JNF. In this case, the SNF definition relies on several operations and facts that also need to be related ( with , with , with , etc.). It is worth noting that and can be defined and related without using the restriction, but then the corresponding transfer rule can only be proved for square matrices. Applying transfer rules to every constant presented in Lemma  we want to move from HA, we get the following statement in JNF:

The statement assumes two new premises, namely and where A has type . Here, is the set of all matrices (JNF requires explicit dimensions). We would like to transform the new assumptions into n n and \(i<n\), respectively, where n is a free variable. This can be done by means of local type definitions, since the local typedef rule [39] provides exactly what is needed: types defined dynamically in local proof contexts. However, we still would have to internalize the type class and then abstract over its operations via dictionary construction [38]. This step is almost immediate when using the type class , because there are no operations associated with it, just the assumption , and at the end everything is reduced to assume that there exists a type (with no type class restrictions) for which there exists an isomorphism between the set of all elements of the type and \(\{0,\dots ,n-1\}\), then proving that fulfills the condition of the type class , which holds trivially, and finally, is instantiated by .

However, as explained before, introduces more type classes ( , , etc.) as well as associated operations and constants ( \(+\), \(*\), 1, etc.). Hence, the approach is more arduous, since we would have to define a predicate S \(f'\) \(g'\) ...where S is the carrier set and \(f'\), \(g'\), etc. the abstraction of all the operations and constants. This is the common approach and has been applied successfully, for instance, by Immler to connect theorems and structures of linear algebra and rings involving different representations [34]. It is feasible, but laborious. This approach would require the use of another sound extension of Isabelle’s logic by Kunĉar and Popescu: the unoverloading rule [39,  Sect. 6.2].

In our case, we take a shortcut: we use the type , which was presented in Sect. 2.5. We prove that is an instance of the type class , that is, it satisfies all the conditions imposed by the type class: it defines a well ordering, there exists a strictly monotonic increasing function from elements of the to the naturals, etc. Once such an instance is completed, any statement that involves a matrix of type \(\alpha \)        can be rewritten as \(\alpha \)        , where just imposes the type to have more than one element. Fortunately, it is easy to apply local type definitions to a type , since we can rewrite to . Then, the previous theorem can be easily transformed to:

Now it is almost straightforward to substitute by a new variable n using local type definitions, since it is very easy to internalize the type class and prove that the new fresh type variable satisfies its properties (it has no associated operations or constants, so is similar to the class ). To do this, we apply the local type definition rule by creating a local type with n elements and then instantiate the previous statement where . The only peculiarity which remains is that the resulting theorem restricts the new variable n to be greater than 1, since demands the type to have more than one element. This imposes the local type definition rule to be applied within a context that assumes \(n>1\). Cases \(n=0\) and \(n=1\) have to be treated separately. They correspond to the case of matrices with no elements and with one element, respectively. In both cases, the result is trivial. Finally, we get the statement in JNF:

Note that, once the transfer rules are proved the rest of the process is almost immediate. As expected, the transfer rules are proved only once to relate concepts between HA and JNF, and then they are reused when moving results. The fact of being able to transfer results between both libraries by means of the connection bridges is essential and it saves much work in our development. Throughout the paper, we use both bridges continuously, not only the new connection. For instance, the following lemma was available in HA (for finite types), but not in JNF.

This result is very important, since it permits us to characterize the invertible matrices of any ring. We need it in the JNF library. Instead of replicating the proof, which would demand some work since it is based on several previous lemmas that are not available in JNF, we directly converted it using transfer rules and local type definitions. Once the lemma is available in JNF, we use it throughout the whole development to make the proofs easier, concretely more than 20 times. Let us remark that the connection is bidirectional and the way back from JNF to HA is easier (no local type definitions are required) once the transfer rules are provided.

As a summary of the methodology, we show here the necessary steps to move theorems back and forth between HA and JNF:

In the previous section, we have presented a general verified algorithm to transform arbitrary matrices into their SNFs. If one is simply interested in the result of computing a Smith normal form over a concrete structure, such as integer matrices, a result certification approach is a valid alternative. The approach is well known: compute externally and check the output in a theorem prover. In our case, the external algorithm (efficient oracle) must provide five matrices: P, S, Q and also the inverses \(P^{-1}\) and \(Q^{-1}\). We could really work with only the matrices P, S and Q, but then we would have to check whether P and Q are indeed invertible matrices within Isabelle/HOL, which would affect the performance. This way, given \(P^{-1}\) and \(Q^{-1}\), only a matrix multiplication is required to check each one. Since the main reason to use the certified approach is the performance, the checker is implemented in JNF to make use of the Strassen matrix multiplication algorithm (which requires block matrices). The final soundness statement follows:

This approach permits us to solve the problems with the performance of our verified version. Moreover, both approaches are compatible: the verified approach provides a formal proof of an algorithm over general structures, whereas the certified approach provides a connection to external efficient algorithms, whose output is verified within Isabelle/HOL. The performance of the certified approach strongly depends on the performance of the external algorithm: since the properties validated by the checker are inexpensive, the checker does not cause a huge overhead. However, the need of the \(P^{-1}\) and \(Q^{-1}\) matrices slows down the external algorithm, but in any case it is faster than checking invertibility within Isabelle/HOL.

The SNF is unique up to multiplication by units. This statement can be expressed in both the HA and JNF libraries. However, the proof requires an intensive use of submatrices and minors (determinants of submatrices). Since submatrices are a delicate issue in the HA library, the appropriate approach is to state the theorem in HA, but prove it in the JNF library. Indeed, a formal proof in the HA library is not directly possible, since induction on the dimension of submatrices is required. We first show the definition of submatrix in JNF, which was introduced by Bentkamp.

Here, I and J are the subsets of \({\mathbb {N}}\) which restrict the indices of A that define the elements of the submatrix. The function is used to relate the indices of the input matrix to the ones of the submatrix, i.e., I i is the ith largest element of I. This way, the element ( A I J) (i, j) is the one in the position ( I i, J j) of the input matrix A. Note that if \(I=\mathsf {UNIV}\) (where \(\mathsf {UNIV}\) represents the set of all elements of type ), then I \(i = i\), i.e., we choose all rows (analogous with respect to J and the columns).

Now, we sketch our proof of the uniqueness of the SNF of a matrix, which is an adaptation of the one presented in [32,  p. 76]. The first step consists in showing that any minor of order k (the determinant of a submatrix with k rows and k columns) of a diagonal matrix is either 0 or the product of k elements of the diagonal (up to sign). The proof is carried out by induction on k. Although our proof in Isabelle/HOL required some work due to some missing properties about submatrices, the JNF library and its submatrix representation were very useful and allowed us to formalize the result.

Then, the following equivalences are the key to prove the uniqueness:In the formula, \(d_i\) is the ith element of the matrix S, which is a Smith normal form of a matrix A. \(\bar{A}_{k}\) represents the set of all minors of order k of A (analogous for \(\bar{S}_{k}\)). Thus, we are stating that the product of the k first elements of S is associated, i.e., equal up to multiplication by units, to the \(\gcd \) of all minors of order k of S and also to the \(\gcd \) of all minors of order k of the original matrix A.

In order to prove (1), we proceed as follows. First, we show that the left-hand side divides the right-hand side. Let b be a nonzero minor of order k of S (if the minor is 0, we are done). Since S is in SNF, then it is diagonal and thus b can be written as the product of k elements of the diagonal of S. Let J be the (ordered) list of those k elements, then each \(d_i\) divides the ith element of J, and this implies the result. The other direction is actually quite easy, indeed \(\prod _{i=1}^k d_i\) is a minor of order k of S and then the \(\gcd \) of all minors must divide it.

Before proving (2), we need an essential result: the Cauchy–Binet formula. This formula relates the determinant of the product of rectangular matrices to a summation of determinants of submatrices.

Our proof in Isabelle/HOL of this fact follows the argument presented in [54]. Nevertheless, we substantially modified some parts of it [concretely, while proving Eq. (11) of that article] to base the reasoning on properties of determinants that were already proved in JNF. The final statement in Isabelle/HOL follows:

Once the Cauchy–Binet formula is formalized, we can tackle the proof of (2). The key is to prove the following rewrite rule for all matrices P, A and Q, sets of indices I and J of cardinality k, and sets \({\mathcal {I}} = \{I'.\, I'\subseteq \{0..<n\} \wedge \mathsf {card}\, I'=k\}\) and \({\mathcal {J}} = \{J'.\, J'\subseteq \{0..<m\} \wedge \mathsf {card}\ J'=k\}\).The proof of this fact is performed using the Cauchy–Binet formula and properties of multiplication and composition of submatrices. In (2), to prove that the right-hand side divides the left-hand side, one just has to note that \(\gcd (\bar{A}_{k})\) divides each element of such a summation (concretely, each \(\mathsf {det(submatrix}\ A\ J'\ I')\)), and then we get the result. The reasoning for proving the other way consists of applying the same rewrite rule again, but taking into account that P and Q are indeed invertible matrices.

Putting everything together, we get the statement for the uniqueness, since given two matrices S and \(S'\) which are Smith normal forms of a matrix A, then \(S_{ii}\) and \(S'_{ii}\) are associated. The final statement (in JNF) is as follows:

Nevertheless, our algorithm was defined in the HA library where also its soundness theorem is proved, so we transfer the result from JNF to HA following the approach presented in Sect. 3. Let us note that the uniqueness is proved on a GCD domain (a more general structure than Bézout domain). We also get the equality of the matrices S and \(S'\) (in both HA and JNF) once the definition of the SNF is parametrized by a complete set of non-associates, i.e., a set of elements of \({\mathcal {R}}\), one from each equivalence class defined by the equivalence relation of being associate elements [51].

In this concrete case we can also transfer an intermediate result to HA: the Cauchy–Binet formula. Although this formula involves submatrices, in this concrete case something special happens: we do know the type of each submatrix involved in the formula in the corresponding HA statement. If the original matrices are of type and , respectively, then the submatrices will have type . Thus, in this case we can define submatrices in HA.

Here, \(\chi \) defines a lambda-expression when working with the vector and matrix representation presented in HA.

By means of transfer rules we can relate submatrices in HA to submatrices in JNF, but in a context assuming that the cardinality of the sets I and J that define the submatrices are equal to the cardinality of the new types of the submatrices.

Now, using this new transfer rule outside the context properly, we can move the result from JNF to HA. Then, we obtain the following statement:

Note that the type of the submatrices must be explicitly provided, and this is possible thanks to the fact that the type variable is already fixed.

There are linear algebra developments in most theorem provers [15, 16, 25, 44, 47], above all focused on vector spaces properties. However, only Coq provides a formal correctness proof of the SNF thanks to a development by Cano et al. [13], which is the closest work to ours. Such a development consists of approximately 9000 lines of code⁴ and uses the SSReflect proof language. This work differs in the sense that the authors provide formal proofs of facts that are not covered in our work, for instance, the classification theorem for finitely presented modules. They provide three formalizations of the Smith normal form algorithm: over a Euclidean domain, over a structure that they call constructive principal ideal domain (a Bézout domain with a well-founded divisibility relation) and over an integral domain with a division operator and a \(2 \times 2\) Smith operation, which is actually the closest to what is presented in this paper.

The Coq development makes strong use of dependent types; indeed, matrices are implemented as finite functions over finite sets of indices where dependent types are used to ensure well formedness. This makes it easier to work with submatrices and permits induction over the dimension, which are problematic issues in the HA library. Since Isabelle/HOL lacks dependent types, we had to switch conveniently between two representations (the HA and JNF libraries) using the lifting and transfer package and local types definitions to get the results. Dependent types also facilitate some definitions and proofs, for example, the authors of [13] also use dependent types for defining the set \({\mathcal {Z}}_{nm}\) of functions from \(\{0,\dots ,n-1\}\) to \(\{0,\dots ,m-1\}\) where n and m are parameters. This set is necessary at some point for proving the Cauchy–Binet formula. As a definition like that one cannot be precisely cast in the HOL type system and in fact functions in HOL are total, we usually have to somehow complete the functions of such a set for values outside the domain. Such functions must have type in Isabelle/HOL; whereas in Coq they can write \( \{\texttt {ffun}\,\texttt {'I}\_\texttt {n}\,\rightarrow \,\texttt {'I}\_\texttt {m}\}\) in order to implement the type of functions with a finite domain (’I_n and ’I_m represent the types with n and m elements, respectively). In this concrete example, we model the set \({\mathcal {Z}}_{nm}\) as a function in Isabelle/HOL that receives two parameters (n and m) and returns the set of functions which map values in \(\{0,\dots ,n-1\}\) to \(\{0,\dots ,m-1\}\), with the extra condition that each \(f \in {\mathcal {Z}}_{nm}\) satisfies \(\forall i.\ i \notin \{0,\dots ,n-1\} \longrightarrow f\ i = i\). With this trick, we can ensure the injectivity of each \(f \in {\mathcal {Z}}_{nm}\) provided that f is injective over the set \(\{0,\dots ,n-1\}\), i.e., we usually have to complete the functions outside the desired domain to preserve useful properties in each case. Otherwise, too many cases would arise in the proofs and this could even break them, for example, when two functions of \({\mathcal {Z}}_{nm}\) must be composed. This approach clearly introduces an overhead in the formalization process in Isabelle/HOL, where functions must be total, compared to the same proofs with dependent types; but it is a workable solution (and it seems there is no better alternative). Another example where the use of dependent types makes this kind of formalization easier is in the termination proof of the algorithm presented in Sect. 5.1. As explained there, since our matrices must be accompanied with their explicit dimensions (modeled with natural numbers), we have to prove that the involved matrices possess the correct dimensions, which required a partial induction. However, in a setting with dependent types, one would have this almost for free.

One difference with respect to the development in Coq is that we allow zero divisors (we do not assume that the ring is a domain). The correctness proofs of the algorithms essentially follow the same reasoning as in a domain and indeed the difficulty is similar, but the proofs become longer (we estimate a 10%) since we need to treat more cases. The Coq development includes a characterization of elementary divisor domains⁵ based on the Kaplansky condition presented in [37,  Theorem 5.2]. In our case, we provided a characterization of elementary divisor rings (not restricted to domains) in Theorem 4. To this end, we had to formalize most of the results presented in an article by Gillman and Henriksen [26], which requires more effort but generalizes the statement of the Coq development. The main contribution compared to the Coq development is that ours has been carried out in HOL, a context without dependent types, making use of local type definitions and a new bridge to switch between two representations. We sketched this idea at a workshop [21].

Local type definitions are still considered as an experimental extension of higher-order logic and there are very few developments that have used it. As far as we know, apart from the basic examples provided by the implementation of the rule and the work presented in this paper, there only exist four developments that have used local type definitions. The first one is the library about the Perron–Frobenius theorem [22], which has already been mentioned in Sect. 3. The second one presents a formal correctness proof of the Berlekamp–Zassenhaus algorithm [23], an algorithm to factor polynomials. There, local type definitions are used to connect three different representations of finite rings. This library has also been mentioned in Sect. 3 since we make use of the type implemented in it. The authors of this paper collaborated in both the Perron–Frobenius and the Berlekamp–Zassenhaus development. The last development is a work that defines and proves basic properties of smooth manifolds [35], where the authors transform an existing (type based) library of linear algebra (which includes definitions and results on groups, rings, vector spaces...) into one with explicit carrier sets. There also exists an interesting example on how to use local type definitions to move Cramer’s lemma to the JNF library [10,  Sect. 6].

Theorem 2 relates the existence of a Smith normal form to the properties of the underlying structure. It is also known that, if all matrices over a commutative ring with unit \({\mathcal {R}}\) have a SNF, then it does not follow that \({\mathcal {R}}\) is a principal ideal domain [40]. Moreover, there are examples of Bézout rings that are not Hermite rings and also examples of Hermite rings that are not elementary divisor rings [31]. However, it is a well-known open problem to decide whether a Bézout domain is always an elementary divisor domain [30].

In this work, we have formalized several facts related to the Smith normal form of a matrix. An important contribution of this work is its methodology of formalization: since many results and algorithms about the SNF require the manipulation of submatrices, we had to switch between two existing libraries (HA and JNF). Indeed, there are proofs that cannot be performed in the HA library and even theorems that cannot be stated there, since quantification over type variables is not possible in Isabelle/HOL. Sometimes one prefers proving a theorem in one of the libraries because its proof is easier. It also happens that some of the required results exist in the HA library but not in the JNF one. To easily switch between both libraries, we use bridges to connect them and move results bidirectionally using the lifting and transfer package and local type definitions. This way, both libraries are combined to provide the advantages of a type based formalization (in which sometimes proofs are more concise and direct since the dimensions are ensured via type checking) with the flexibility of explicit dimensions as natural numbers, all of this in Isabelle/HOL with its powerful proof automation tools. This permits working with simple type theory in a context (matrices, submatrices, blocks, etc.) that is usually considered more adequate for dependent type theory. Following this methodology, we have formalized an algorithm that transforms a diagonal matrix into Smith normal form, which is sometimes the second step to obtain a general algorithm that works for any matrix. This verified algorithm accomplishes the task in a general setting: it works for any matrix, including non-square and singular ones, and it is defined for matrices with coefficients in Bézout rings. Indeed, we have presented a proof of Theorem 2, which shows that there is no more abstract structure where the desired transformation can be carried out for all matrices. A complete Smith normal form algorithm which works for any matrix over elementary divisor rings is also provided, also in a general setting via parametrization by functions. To provide an efficient alternative to the verified algorithm, we also formalized a result certification approach. In addition, we have formalized characterizations of Hermite rings and elementary divisor rings, following the generalizations presented in [26] and a formal proof on the uniqueness of the SNF.

Some parts of the development were quick to develop and are very readable, since the code includes comments and examples. On the other hand, the development of the infrastructure to connect both libraries (HA and JNF) and sometimes the use of it together with local type definitions are more technical. But once the basics of the bridge are developed, one just has to connect the definitions of the different representations, which is usually an easy transfer lemma. The proof engineering methodology presented in this paper is scalable and replicable in other developments. It extends the previous connection by allowing statements with the restriction, i.e., it permits easily transferring a lemma that requires HA and to JNF and vice versa, and one can also combine algorithms in different representations. This shows that the combination of the lifting and transfer package with local type definitions is a workable strategy to share theorems between different representations, and it even makes it easier to work in a setting with no dependent types. In fact, the new bridge has already been successfully used in a development about modular algorithms for computing reduced lattice bases and Hermite normal forms [9]. Such a development required to move almost all final theorems of the echelon form and Hermite normal form AFP entries [18, 19] (which are large developments; around 8000 and 2300 lines of code, respectively), from HA to JNF. The JNF library is growing and is a nice candidate to substitute the HA representation in the long term due to the troubles when reasoning with matrix dimensions. Indeed, according to the AFP statistics, it is one of the most used entries. However, it is usual that some entries that use the JNF library again prove theorems that are already part of HA. For instance, the Gröbner basis entry [43] proves from scratch theorems about row spaces (such as the row space of \(P\cdot A\) is equal to the row space of A if P is an invertible matrix) that were already proved in HA with the restriction. The use of the new bridge would benefit the works that rely on JNF.