| A case study in machine-assisted proofs: The Integers form an Integral Domain (1993) | |||||||||||||||||
Abstract | |||||||||||||||||
| We present a formalization of the set Z of integers using Martin-Lof's type theory. In particular we focus on the task of proving that this set with the operations + and form an Integral Domain. The proofs are developed for an inductive definition of Z, but we also discuss what kind of proofs could be obtained for a formulation where the set is defined as a quotient. The differences between both approaches when one is interested in regarding the computational meaning of proofs are pointed out. In order to better reason about the proofs of the properties following from the postulates of an integral domain, an abstract formalization of this algebraic system is also proposed. With this, we aimed at not just being able to formally reflect the derivation of the properties independently of the concrete representation we were interested in, but also to translate these results to every algebraic structure satisfying those postulates. Keywords and phrases: integers, type theory, integral dom... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||