;;;*************************************************************** ;;;An ACL2 Proof of the Chinese Remainder Theorem ;;;David M. Russinoff ;;;April, 1999 ;;;*************************************************************** (in-package "ACL2") (include-book "/u/druss/fp/lib/basic") (include-book "/u/druss/fp/fp") (in-theory (disable rem)) (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))))) (defun rel-prime (x y) (= (g-c-d x y) 1)) (defun rel-prime-all (x l) (if (endp l) t (and (rel-prime x (car l)) (rel-prime-all x (cdr l))))) (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))))) (defun congruent (x y m) (= (rem x m) (rem y m))) (defun congruent-all (x a m) (declare (xargs :measure (acl2-count m))) (if (endp m) t (and (congruent x (car a) (car m)) (congruent-all x (cdr a) (cdr m))))) (defun natp (n) (and (integerp n) (>= n 0))) (defun natp-all (l) (if (endp l) t (and (natp (car l)) (natp-all (cdr l))))) #| (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)))) |# (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)))))) ) (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))))) (defun one-mod (x l) (* (d x l) (prod l) (d x l) (prod l))) (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)) (defthm g-c-d-type (implies (and (integerp x) (integerp y)) (integerp (g-c-d x y))) :rule-classes (:type-prescription)) (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 ()) (defthm hack-1 (implies (and (rationalp a) (rationalp b) (= x a) (= y b)) (= (* a b) (* x y))) :rule-classes ()) (defthm hack-2 (implies (and (rationalp a) (rationalp b) (rationalp x) (rationalp y) (rationalp c) (rationalp d) (rationalp l) (= 1 (+ (* a x) (* b y))) (= 1 (+ (* c x) (* d l)))) (= 1 (+ (* a x) (* c x) (* b d y l) (- (* x x a c))))) :rule-classes () :hints (("Goal" :use ((:instance hack-1 (x (* b y)) (y (* d l)) (a (- 1 (* a x))) (b (- 1 (* c x)))))))) (defthm c-type (implies (and (integerp x) (natp-all l)) (rationalp (c x l))) :rule-classes (:type-prescription)) (defthm prod-type (implies (natp-all l) (rationalp (prod l))) :rule-classes (:type-prescription)) (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 () :hints (("Subgoal *1/4" :use ((:instance r-s-lemma (y (car l))) (:instance hack-2 (a (r x (car l))) (b (s x (car l))) (y (car l)) (l (prod (cdr l))) (c (c x (cdr l))) (d (d x (cdr l)))))))) (defthm c-int (implies (and (integerp x) (natp-all l)) (integerp (c x l))) :rule-classes ()) (in-theory (disable rel-prime rel-prime-all rel-prime-moduli one-mod crt1 crt r s c d prod)) (defthm hack-3 (implies (= x y) (= (* x x) (* y y))) :rule-classes ()) (defthm hack-4 (implies (and (rationalp c) (rationalp d) (rationalp m) (rationalp p) (= (+ (* c m) (* d p)) 1)) (= (* d p d p) (* (1+ (* m c (- (* c m) 2)))))) :rule-classes () :hints (("Goal" :use ((:instance hack-3 (x (* d p)) (y (- 1 (* c m)))))))) (defthm one-mod-alt (implies (and (natp m) (> m 1) (natp-all l) (rel-prime-all m l)) (= (one-mod m l) (1+ (* m (c m l) (- (* (c m l) m) 2))))) :rule-classes () :hints (("Goal" :in-theory (enable one-mod) :use ((:instance c-int (x m)) (:instance c-d-lemma (x m)) (:instance hack-4 (c (c m l)) (d (d m l)) (p (prod l))))))) (defthm hack-5 (implies (and (integerp m) (integerp c) (integerp cm) (>= m 2) (>= c 1) (>= cm 0)) (natp (* m c cm))) :rule-classes ()) (defthm hack-6 (implies (and (integerp c) (>= c 1) (integerp m) (> m 1)) (natp (1+ (* m c (- (* c m) 2))))) :rule-classes () :hints (("Goal" :use ((:instance hack-5 (cm (- (* c m) 2))))))) (defthm hack-7 (implies (and (integerp m) (integerp c) (integerp cm) (>= m 2) (< c 0) (< cm 0)) (natp (* m c cm))) :rule-classes ()) (defthm hack-8 (implies (and (integerp c) (< c 1) (integerp m) (> m 1)) (natp (1+ (* m c (- (* c m) 2))))) :rule-classes () :hints (("Goal" :use ((:instance hack-7 (cm (- (* c m) 2))))))) (defthm hack-9 (implies (and (integerp c) (integerp m) (> m 1)) (natp (1+ (* m c (- (* c m) 2))))) :rule-classes () :hints (("Goal" :use (hack-6 hack-8)))) (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 () :hints (("Goal" :use ((:instance one-mod-alt (m x)) (:instance c-int) (:instance hack-9 (m x) (c (c x l))))))) (defthm hack-10 (implies (and (integerp m) (> m 1) (integerp p) (>= (1+ (* m p)) 0)) (>= p 0)) :rule-classes ()) (defthm hack-11 (implies (and (integerp m) (> m 1) (integerp c) (>= (1+ (* m c (- (* c m) 2))) 0)) (>= (* c (- (* c m) 2)) 0)) :rule-classes () :hints (("Goal" :use ((:instance hack-10 (p (* c (- (* c m) 2)))))))) (defthm rem-one-mod-m-1 (implies (and (natp m) (> m 1) (natp-all l) (rel-prime-all m l)) (>= (* (c m l) (- (* (c m l) m) 2)) 0)) :rule-classes () :hints (("Goal" :use (one-mod-alt (:instance one-mod-nat (x m)) (:instance c-int (x m)) (:instance hack-11 (c (c m l))))))) (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 () :hints (("Goal" :use (one-mod-nat (:instance one-mod-alt (m x)) (:instance rem-one-mod-m-1 (m x)) (:instance c-int) (:instance rem< (m 1) (n x)) (:instance rem+ (m 1) (n x) (a (* (c x l) (- (* (c x l) x) 2)))))))) (defun remove1 (x l) (if (endp l) l (if (eql x (car l)) (cdr l) (cons (car l) (remove1 x (cdr l)))))) (defthm prod-factor (implies (and (natp-all l) (member x l)) (= (prod l) (* x (prod (remove1 x l))))) :rule-classes () :hints (("Goal" :in-theory (enable prod)))) (defthm one-mod-factor (implies (and (integerp m) (natp-all l) (member x l)) (= (one-mod m l) (* x (d m l) (prod (remove1 x l)) (d m l) (prod l)))) :rule-classes () :hints (("Goal" :in-theory (enable one-mod) :use (prod-factor)))) (defthm prod-int (implies (natp-all l) (integerp (prod l))) :rule-classes (:type-prescription) :hints (("Goal" :in-theory (enable prod)))) (defthm natp-remove1 (implies (natp-all l) (natp-all (remove1 x l)))) (defthm hack-12 (implies (and (integerp a) (integerp b) (integerp c) (integerp d)) (integerp (* a b c d))) :rule-classes ()) (defthm rem-one-mod-x-1 (implies (and (natp m) (> m 1) (natp-all l)) (INTEGERP (* (PROD L) (D M L) (D M L) (PROD (REMOVE1 X L))))) :hints (("Goal" :in-theory (disable prod-int) :use (prod-int (:instance prod-int (l (remove1 x l))) (:instance hack-12 (a (prod l)) (b (d m l)) (c (d m l)) (d (prod (remove1 x l)))))))) (defthm rem-one-mod-x-2 (implies (and (natp m) (> m 1) (natp-all l) (rel-prime-all m l) (member x l) (integerp x) (> x 0)) (= (rem (one-mod m l) x) 0)) :rule-classes () :hints (("Goal" :use (one-mod-factor (:instance one-mod-nat (x m)) (:instance divides-rem-0 (n x) (a (* (d m l) (prod (remove1 x l)) (d m l) (prod l)))))))) (defthm modulus-pos (implies (and (rel-prime-moduli l) (member x l)) (and (integerp x) (> x 1))) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli)))) (defthm moduli-natp-all (implies (rel-prime-moduli l) (natp-all l)) :hints (("Goal" :in-theory (enable rel-prime-moduli)))) (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 () :hints (("Goal" :use ((:instance rem-one-mod-x-2 (m x) (x y)) (:instance modulus-pos (x y)))))) (defthm rem0+0 (implies (and (natp a) (natp b) (natp c) (natp n) (> n 0) (= (rem a n) 0) (= (rem c n) 0)) (= (rem (+ (* a b) c) n) 0)) :rule-classes () :hints (("Goal" :use ((:instance rem+rem (a (* a b)) (b c)) (:instance n<=fl (n 0) (x (/ a n))) (:instance divides-rem-0 (a (* (fl (/ a n)) b))) (:instance fl-rem-0 (m a)))))) (defthm rel-prime-all-remove (implies (rel-prime-all m l) (rel-prime-all m (remove x l))) :hints (("Goal" :in-theory (enable rel-prime-all)))) (defthm rel-prime-remove (implies (rel-prime-moduli l) (rel-prime-moduli (remove x l))) :hints (("Goal" :in-theory (enable rel-prime-moduli)))) (defthm member-remove (implies (and (member x l) (not (eql x y))) (member x (remove y l)))) (defun sublistp (m l) (if (endp m) t (and (member (car m) l) (sublistp (cdr m) l)))) (defthm member-sublistp (implies (and (sublistp m l) (member x m)) (member x l))) (defthm g-c-d-commutative (implies (and (natp x) (natp y)) (= (g-c-d x y) (g-c-d y x))) :rule-classes ()) (defthm rel-prime-all-rel-prime (implies (and (rel-prime-all x l) (member y l)) (rel-prime x y)) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-all)))) (defthm rel-prime-all-moduli-remove (implies (and (rel-prime-moduli l) (member x l)) (rel-prime-all x (remove x l))) :hints (("Goal" :in-theory (enable rel-prime-all rel-prime-moduli)) ("Subgoal *1/7''" :use ((:instance rel-prime-all-rel-prime (x (car l)) (l (cdr l)) (y x)) (:instance g-c-d-commutative (y (car l)))) :in-theory (enable rel-prime)) ("Subgoal *1.1/5" :use ((:instance g-c-d-commutative (y l1)))))) (defthm rel-prime-modulus-nat (implies (and (member x l) (rel-prime-moduli l)) (and (natp x) (> x 1))) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli)))) (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 () :hints (("Goal" :in-theory (enable rel-prime-moduli crt1)) ("Subgoal *1/1" :use (modulus-pos (:instance rem< (m 0) (n x)))) ("Subgoal *1/3" :use ((:instance rem0+0 (n x) (a (one-mod (car m) (remove (car m) l))) (b (car a)) (c (crt1 (cdr a) (cdr m) l))) (:instance rel-prime-modulus-nat) (:instance rem-one-mod-0 (x (car m)) (y x) (l (remove (car m) l))) (:instance one-mod-nat (x (car m)) (l (remove (car m) l))))))) (defthm rem0+1-1 (implies (and (natp a) (natp b) (natp c) (natp n) (> n 0)) (= (rem (* a (1+ (* (fl (/ b n)) n))) n) (rem a n))) :rule-classes () :hints (("Goal" :use ((:instance n<=fl (n 0) (x (/ b n))) (:instance rem+ (a (* a (fl (/ b n)))) (m a)))))) (defthm rem0+1-2 (implies (and (natp a) (natp b) (natp c) (natp n) (= (rem b n) 1) (> n 0)) (= (rem (* a (+ (rem b n) (* (fl (/ b n)) n))) n) (rem a n))) :rule-classes () :hints (("Goal" :use (rem0+1-1)))) (defthm rem0+1-3 (implies (and (natp a) (natp b) (natp c) (natp n) (= (rem b n) 1) (> n 0)) (= (rem (* a b) n) (rem (* a (+ (rem b n) (* (fl (/ b n)) n))) n))) :rule-classes () :hints (("Goal" :use ((:instance rem-fl (m b)))))) (defthm rem0+1-4 (implies (and (natp a) (natp b) (natp c) (natp n) (= (rem b n) 1) (> n 0)) (= (rem (* a b) n) (rem a n))) :rule-classes () :hints (("Goal" :in-theory (disable a9 unicity-of-1) :use (rem0+1-2 rem0+1-3)))) (defthm rem0+1 (implies (and (natp a) (natp b) (natp c) (natp n) (> n 0) (= (rem b n) 1) (= (rem c n) 0)) (= (rem (+ (* a b) c) n) (rem a n))) :rule-classes () :hints (("Goal" :use (rem0+1-4 (:instance rem+rem (a (* a b)) (b c)))))) (defthm rel-prime-not-eql (implies (and (natp x) (natp y) (> x 1) (rel-prime x y)) (not (= x y))) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime g-c-d)))) (defthm not-member-rel-prime-all (implies (and (natp x) (> x 1) (rel-prime-all x m)) (not (member x m))) :hints (("Goal" :in-theory (enable rel-prime-all)) ("Subgoal *1/2'4'" :use ((:instance rel-prime-not-eql (x m1) (y m1)))))) (defun cong0-all (x l) (if (endp l) t (and (= (rem x (car l)) 0) (cong0-all x (cdr l))))) (defthm cong0-1 (implies (and (natp a) (natp m) (> m 1) (sublistp l1 l) (rel-prime-all m l1) (rel-prime-moduli l1) (rel-prime-all m l) (rel-prime-moduli l)) (cong0-all (* a (one-mod m l)) l1)) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-all rel-prime-moduli)) ("Subgoal *1/6" :use ((:instance rem-one-mod-0 (x m) (y (car l1))) (:instance one-mod-nat (x m)) (:instance rem< (m 0) (n (car l1))) (:instance rem0+0 (c 0) (a (one-mod m l)) (b a) (n (car l1))))))) (defun sublistp-induct (n l) (declare (xargs :measure (nfix (- (len l) n)))) (if (and (natp n) (< n (len l))) (sublistp-induct (1+ n) l) t)) (defthm sublistp-last (sublistp (nthcdr (len l) l) m)) (defthm nthcdr+1 (implies (natp n) (equal (NTHCDR (+ 1 N) L) (cdr (nthcdr n l))))) (defthm member-car-nthcdr (IMPLIES (AND (INTEGERP N) (<= 0 N) (< N (LEN L))) (MEMBER (CAR (NTHCDR N L)) L))) (defthm sublistp-nthcdr (implies (and (natp n) (<= n (len l))) (sublistp (nthcdr n l) l)) :rule-classes () :hints (("Goal" :induct (sublistp-induct n l)))) (defthm sublistp-l-l (sublistp l l) :hints (("Goal" :use ((:instance sublistp-nthcdr (n 0)))))) (defthm sublistp-remove (implies (and (sublistp m l) (not (member x m))) (sublistp m (remove x l)))) (defun distinctp (l) (if (endp l) t (and (not (member (car l) (cdr l))) (distinctp (cdr l))))) (defthm sublistp-cdr-remove (implies (and (sublistp m l) (distinctp m) (consp m)) (sublistp (cdr m) (remove (car m) l)))) (defthm rel-prime-sublist (implies (and (rel-prime-all x l) (sublistp m l)) (rel-prime-all x m)) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-all)))) (defthm rel-prime-moduli-sublist (implies (and (rel-prime-moduli l) (distinctp m) (sublistp m l)) (rel-prime-moduli m)) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli rel-prime-all)) ("Subgoal *1/7" :use ((:instance rel-prime-modulus-nat (x (car m))))) ("Subgoal *1/6" :use ((:instance rel-prime-modulus-nat (x (car m))))) ("Subgoal *1/5" :use ((:instance rel-prime-sublist (x (car m)) (m (cdr m)) (l (remove (car m) l))))))) (defthm cong0-2 (implies (and (natp a) (sublistp m l) (distinctp m) (rel-prime-moduli l)) (cong0-all (* a (one-mod (car m) (remove (car m) l))) (cdr m))) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli rel-prime-all) :use ((:instance cong0-1 (m (car m)) (l (remove (car m) l)) (l1 (cdr m))) (:instance rel-prime-all-moduli-remove (x (car m))) (:instance rel-prime-moduli-sublist) (:instance rel-prime-modulus-nat (x (car m))))))) (defthm cong0-3 (implies (and (rel-prime-moduli m) (natp x) (natp y) (natp-all a) (cong0-all x m) (= (len a) (len m)) (congruent-all y a m)) (congruent-all (+ x y) a m)) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli)) ("Subgoal *1/8" :use ((:instance rem< (m 1) (n (car m))) (:instance rem0+1 (a y) (b 1) (c x) (n (car m))))))) (defthm natp-crt1 (implies (and (natp-all a) (rel-prime-moduli m) (= (len a) (len m)) (rel-prime-moduli l) (distinctp m) (sublistp m l)) (natp (crt1 a m l))) :rule-classes () :hints (("Goal" :in-theory (enable rel-prime-moduli crt1)) ("Subgoal *1/2" :use ((:instance one-mod-nat (x (car m)) (l (remove (car m) l))))))) (defthm crt1-lemma (implies (and (natp-all a) (rel-prime-moduli m) (distinctp m) (= (len a) (len m)) (rel-prime-moduli l) (sublistp m l)) (congruent-all (crt1 a m l) a m)) :rule-classes () :hints (("Goal" :in-theory (enable congruent-all rel-prime-moduli crt1)) ("Subgoal *1/8" :use ((:instance rem0+1 (a (car a)) (n (car m)) (b (ONE-MOD (CAR M) (REMOVE (CAR M) L))) (c (CRT1 (CDR A) (CDR M) L))) (:instance rem-one-mod-1 (x (car m)) (l (remove (car m) l))) (:instance one-mod-nat (x (car m)) (l (remove (car m) l))) (:instance rem-crt1 (a (cdr a)) (m (cdr m)) (x (car m))))) ("Subgoal *1/7" :use ((:instance natp-crt1 (a (cdr a)) (m (cdr m))) (:instance cong0-2 (a (car a))) (:instance one-mod-nat (x (car m)) (l (remove (car m) l))) (:instance cong0-3 (y (CRT1 (CDR A) (CDR M) L)) (a (cdr a)) (m (cdr m)) (x (* (CAR A) (ONE-MOD (CAR M) (REMOVE (CAR M) L))))))))) (defthm distinctp-rel-prime-moduli (implies (rel-prime-moduli m) (distinctp m)) :hints (("Goal" :in-theory (enable rel-prime-moduli rel-prime-all)))) (in-theory (disable distinctp)) (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 () :hints (("Goal" :use (crt1-lemma)))) (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 () :hints (("Goal" :in-theory (enable crt) :use ((:instance natp-crt1 (l m)) (:instance crt1-thm (l m))))))