Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms

TL;DR

This paper formalizes key algebraic concepts and theorems related to Euclidean domains within the PVS proof assistant, including division algorithms, prime elements, and unique factorization, with verified algorithms for gcd computation.

Contribution

It extends the PVS algebra theory with formal proofs of fundamental properties of Euclidean and related domains, including a verified Euclidean gcd algorithm.

Findings

Formalization of divisibility, prime, and irreducible elements in rings.

Proof that principal ideal domains are unique factorization domains.

Verification of Euclidean gcd algorithm and its inheritance in specific domains.

Abstract

This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm for Euclidean rings and Unique Factorization Domains that are general structures where an analog of the Fundamental Theorem of Arithmetic holds. First, we formalize the general abstract notions of divisibility, prime, and irreducible elements in commutative rings, essential to deal with unique factorization domains. Then, we formalize the landmark theorem, establishing that every principal ideal domain is a unique factorization domain. Finally, we specify the theory of Euclidean domains and formally verify that the rings of integers, the Gaussian integers, and arbitrary fields are Euclidean domains. To highlight the benefits of such a general abstract discipline of formalization, we specify a Euclidean gcd algorithm for Euclidean domains and formalize its correctness. Also, we show how this correctness is inherited under adequate parameterizations for the structures of integers and Gaussian integers.