;;;***************************************************************
;;;An ACL2 Proof of the Chinese Remainder Theorem
;;;David M. Russinoff
;;;April, 1999
;;;***************************************************************
(in-package "ACL2")
(local (include-book "crt"))
;;Recursive definition of greatest common divisor:
(defun g-c-d (x y)
(declare (xargs :measure (nfix (+ x y))))
(if (zp x)
y
(if (zp y)
x
(if (<= x y)
(g-c-d x (- y x))
(g-c-d (- x y) y)))))
;;Two naturals are relatively prime if their gcd is 1:
(defun rel-prime (x y)
(= (g-c-d x y) 1))
;;X is relatively prime to each member of L:
(defun rel-prime-all (x l)
(if (endp l)
t
(and (rel-prime x (car l))
(rel-prime-all x (cdr l)))))
;;Recognizer for lists of pairwise relatively prime moduli:
(defun rel-prime-moduli (l)
(if (endp l)
t
(and (integerp (car l))
(>= (car l) 2)
(rel-prime-all (car l) (cdr l))
(rel-prime-moduli (cdr l)))))
;;Congruence modulo M:
(defun congruent (x y m)
(= (rem x m) (rem y m)))
;;X is congruent to Ai mod Mi for i=1,...,k, where (A1 ... Ak) is a
;;list of naturals and (M1 ... Mk) is a list of moduli:
(defun congruent-all (x a m)
(if (endp m)
t
(and (congruent x (car a) (car m))
(congruent-all x (cdr a) (cdr m)))))
;;Recognizer for naturals:
(defun natp (n) (and (integerp n) (>= n 0)))
;;Recognizer for lists of naturals:
(defun natp-all (l)
(if (endp l)
t
(and (natp (car l))
(natp-all (cdr l)))))
;;The Chinese Remainder Theorem states that if M1,...,Mk are pairwise
;;relatively prime moduli and A1,...,Ak are naturals, then there exists
;;a natural X such that X is congruent to Ai mod Mi for i=1,...,k.
;;Thus, our goal is to define a function CRT that computes such an X,
;;and to prove the following:
;;(defthm chinese-remainder-theorem
;; (implies (and (natp-all a)
;; (rel-prime-moduli m)
;; (= (len a) (len m)))
;; (and (natp (crt a m))
;; (congruent-all (crt a m) a m))))
;;First, we express the gcd of X and Y as a linear combination of X and Y:
(mutual-recursion
(defun r (x y)
(declare (xargs :measure (nfix (+ x y))))
(if (zp x)
0
(if (zp y)
1
(if (<= x y)
(- (r x (- y x)) (s x (- y x)))
(r (- x y) y)))))
(defun s (x y)
(declare (xargs :measure (nfix (+ x y))))
(if (zp x)
1
(if (zp y)
0
(if (<= x y)
(s x (- y x))
(- (s (- x y) y) (r (- x y) y))))))
)
(defthm r-s-lemma
(implies (and (natp x)
(natp y))
(= (+ (* (r x y) x)
(* (s x y) y))
(g-c-d x y)))
:rule-classes ())
;;Thus, if X and Y are relatively prime, then RX+SY = 1. More generally,
;;if X is relatively prime to each member of a list L, and P is the product
;;of the members of L, then we can find naturals C and D such that CX+DP = 1.
;;The reason for this, of course, is that X and P are relatively prime,
;;which follows from the divisibility properties of the gcd and Euclid's
;;Theorem (if p|ab where p is prime, then p|a or p|b). Rather than to
;;prove all of this, however, we take a more direct route to the desired
;;result.
;;Let L = (Y . L') and let P' be the product of the members of L'. Suppose
;;we have A,B, C', and D' such that
;; RX + SY = C'X + D'P' = 1.
;;We must find C and D such that
;; CX + DP = 1,
;;where P = YP'. But since
;; (SD')P = (SY)(D'P') = (1 - RX)(1 - C'X) = 1 - (R + C' - AC'X)X,
;;we have the solution
;; C = R + C' - RC'X and D = SD'.
;;This leads to the following definitions and lemma:
(defun c (x l)
(if (endp l)
0
(- (+ (r x (car l))
(c x (cdr l)))
(* (r x (car l))
(c x (cdr l))
x))))
(defun d (x l)
(if (endp l)
1
(* (s x (car l))
(d x (cdr l)))))
(defun prod (l)
(if (endp l)
1
(* (car l) (prod (cdr l)))))
(defthm c-d-lemma
(implies (and (natp x)
(natp-all l)
(rel-prime-all x l))
(= (+ (* (c x l) x)
(* (d x l) (prod l)))
1))
:rule-classes ())
;;Now, if X and the members of L form a set of pairwise relatively
;;prime moduli, then we can construct a natural that is congrent
;;to 1 mod X and congruent to 0 mod each member of L, namely,
;; (DP)^2 = (1 - CX)^2:
(defun one-mod (x l) (* (d x l) (prod l) (d x l) (prod l)))
(defthm one-mod-nat
(implies (and (natp x)
(> x 1)
(natp-all l)
(rel-prime-all x l))
(natp (one-mod x l)))
:rule-classes ())
(defthm rem-one-mod-1
(implies (and (natp x)
(> x 1)
(natp-all l)
(rel-prime-all x l))
(= (rem (one-mod x l) x) 1))
:rule-classes ())
(defthm rem-one-mod-0
(implies (and (natp x)
(> x 1)
(rel-prime-moduli l)
(rel-prime-all x l)
(member y l))
(= (rem (one-mod x l) y) 0))
:rule-classes ())
;;The definition of CRT is now straightforward:
(defun crt1 (a m l)
(if (endp a)
0
(+ (* (car a) (one-mod (car m) (remove (car m) l)))
(crt1 (cdr a) (cdr m) l))))
(defun crt (a m) (crt1 a m m))
;;A key lemma states that if M is a sublist of a list of pairwise
;;relatively prime moduli L, and A is a list of naturals of the same
;;length as M, and X is a member of L but not of M, then (CRT1 A M L)
;;is congruent to 0 mod X:
(defun sublistp (m l)
(if (endp m)
t
(and (member (car m) l)
(sublistp (cdr m) l))))
(defthm rem-crt1
(implies (and (natp-all a)
(rel-prime-moduli m)
(= (len a) (len m))
(rel-prime-moduli l)
(sublistp m l)
(member x l)
(not (member x m)))
(and (natp (crt1 a m l))
(= (rem (crt1 a m l) x) 0)))
:rule-classes ())
;;Using the above lemma, we can prove the following generalization
;;of the Chinese Remainder Theorem:
(defun distinctp (l)
(if (endp l)
t
(and (not (member (car l) (cdr l)))
(distinctp (cdr l)))))
(defthm crt1-thm
(implies (and (natp-all a)
(rel-prime-moduli m)
(= (len a) (len m))
(rel-prime-moduli l)
(sublistp m l))
(congruent-all (crt1 a m l) a m))
:rule-classes ())
;;The desired theorem follows easily:
(defthm chinese-remainder-theorem
(implies (and (natp-all a)
(rel-prime-moduli m)
(= (len a) (len m)))
(and (natp (crt a m))
(congruent-all (crt a m) a m)))
:rule-classes ())