;;;***************************************************************
;;;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 ())