TR-2004004: Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant

No proof assistant can be considered complete unless it pro- vides facilities for basic arithmetical reasoning. Indeed, integer theory is a part of the necessary foundation for most of mathematics, logic and computer science. In this paper we present our approach to implement- ing arithmetic in the intuitionistic type theory of the MetaPRL proof assistant. We focus on creating an axiomatization that would take ad- vantage of the computational features of MetaPRL type theory. Also, we implement the Arith decision procedure as a tactic that constructs proofs based on existing axiomatization, instead of being a part of the "trusted" code base.