A Mechanical Proof of the Chinese Remainder Theorem

David M. Russinoff

This paper (ps, pdf), which was presented at ACL2 Workshop 2000 (see slides: ps, pdf), describes an ACL2 proof of the Chinese Remainder Theorem:

If m₁, ..., m_k are pairwise relatively prime moduli and a₁, ..., a_k are natural numbers, then there exists a natural number x that simultaneously satisfies x = a_i (mod m_i), i=1, ..., k.

The entire proof is contained in the single event file crt.lisp, except that it depends on some lemmas from the author's library of floating-point arithmetic. In order to certify this file (after obtaining and certifying the library), first replace each of the two occurrences of "/u/druss/" with the path to the directory under which your copy of the library resides. A second event file, summary.lisp, which contains the definitions and main lemmas involved in the proof, may then be certified.