A Mechanical Proof of the Chinese Remainder Theorem

Since antiquity, the Chinese Remainder Theorem (CRT) has been regarded as one of the jewels of mathematics. An elegant result of considerable intrinsic mathematical interest, it has continually found new applications in a variety of disciplines, most notably in cryptology, information theory, and computing[4]. One recent example of a novel application is a veri cation system for a translator of safety-critical railroad software, implemented in ACL2 by P. Bertoli and P.Traverso [1], the correctness of which depends on CRT. That project provided an opportunity for the author to contribute to the solution of a problem of practical signi cance through an exercise that would otherwise have been a mere diversion. This note summarizes the results of this exercise: an ACL2 formalization and mechanical proof of CRT. Let m1;:::;mk be pairwise relatively prime moduli and let a1;:::;ak be arbitrary integers. The theorem guarantees the existence of an integer x that simultaneously satis es the congruences x ai (mod mi), i =1;:::;k. The usual proof of CRT proceeds as follows: For i =1;:::;k, le