#|

 Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
 EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
 OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
 THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
 PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
 CORRECTION.

 IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
 DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
 CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
 (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
 OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
 POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

(NOTE-LIB "proveall" T)
(COMPILE-UNCOMPILED-DEFNS "tmp")
(DISABLE EUCLID)
(DISABLE QUOTIENT-DIVIDES)
(DISABLE IF-TIMES-THEN-DIVIDES)
(DISABLE TIMES)
(DEFN
  CRYPT
  (M E N)
  (IF
    (ZEROP E)
    1
    (IF (EVEN E)
        (REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2)
                                  N))
                   N)
        (REMAINDER (TIMES M
                          (REMAINDER
                            (SQUARE (CRYPT M (QUOTIENT E 2)
                                           N))
                            N))
                   N))))
(PROVE-LEMMA TIMES-MOD-1 (REWRITE)
             (EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
                               N)
                    (REMAINDER (TIMES X Y)
                               N)))
(PROVE-LEMMA TIMES-MOD-2 (REWRITE)
                       (EQUAL (REMAINDER (TIMES A
                                                (TIMES B
                                                       (REMAINDER Y N)))
                                         N)
                              (REMAINDER (TIMES A B Y)
                                         N))
                       ((USE (TIMES-MOD-1 (X (TIMES A B))))
                        (DISABLE TIMES-MOD-1)))
(PROVE-LEMMA CRYPT-CORRECT (REWRITE)
             (IMPLIES (NOT (EQUAL N 1))
                      (EQUAL (CRYPT M E N)
                             (REMAINDER (EXP M E)
                                        N))))
(PROVE-LEMMA TIMES-MOD-3 (REWRITE)
             (EQUAL (REMAINDER (TIMES (REMAINDER A N)
                                      B)
                               N)
                    (REMAINDER (TIMES A B)
                               N)))
(PROVE-LEMMA REMAINDER-EXP-LEMMA (REWRITE)
             (IMPLIES (EQUAL (REMAINDER Y A)
                             (REMAINDER Z A))
                      (EQUAL (EQUAL (REMAINDER (TIMES X Y)
                                               A)
                                    (REMAINDER (TIMES X Z)
                                               A))
                             T)))
(PROVE-LEMMA REMAINDER-EXP (REWRITE)
             (EQUAL (REMAINDER (EXP (REMAINDER A N)
                                    I)
                               N)
                    (REMAINDER (EXP A I)
                               N)))
(PROVE-LEMMA EXP-MOD-IS-1 (REWRITE)
                       (IMPLIES (EQUAL (REMAINDER (EXP M J)
                                                  P)
                                       1)
                                (EQUAL (REMAINDER (EXP M (TIMES I J))
                                                  P)
                                       1))
                       ((USE (EXP-EXP (I M)
                                      (J J)
                                      (K I))
                             (REMAINDER-EXP (A (EXP M J))
                                            (N P)))
                        (DISABLE EXP-EXP REMAINDER-EXP)))
(DEFN PDIFFERENCE (A B)
  (IF (LESSP A B)
      (DIFFERENCE B A)
      (DIFFERENCE A B))
  NIL

;   We wish to teach the system the trick of proving that A mod p = B mod p by
;   considering whether p A-B. If we used DIFFERENCE we would have to split on
;   whether A<B.  So we introduce PDIFFERENCE that contains that split.  Then
;   we prove the necessary facts about TIMES, REMAINDER and PDIFFERENCE. During
;   these proofs the case splits on A<B arise. But the case splits do not arise
;   in the statements of the lemmas and so don't arise when we try to apply
;   them.  After proving what we need about PDIFFERENCE we disable it.

  )
(PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PDIFFERENCE (REWRITE)
             (EQUAL (TIMES M (PDIFFERENCE A B))
                    (PDIFFERENCE (TIMES M A)
                                 (TIMES M B))))
(PROVE-LEMMA EQUAL-MODS-TRICK-1 (REWRITE)
             (IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B)
                                        P)
                             0)
                      (EQUAL (EQUAL (REMAINDER A P)
                                    (REMAINDER B P))
                             T)))
(PROVE-LEMMA EQUAL-MODS-TRICK-2 (REWRITE)
                       (IMPLIES (EQUAL (REMAINDER A P)
                                       (REMAINDER B P))
                                (EQUAL (REMAINDER (PDIFFERENCE A B)
                                                  P)
                                       0))
                       ((DISABLE DIFFERENCE-ELIM)))
(DISABLE PDIFFERENCE)
(PROVE-LEMMA PRIME-KEY-TRICK (REWRITE)
                       (IMPLIES (AND (EQUAL (REMAINDER (TIMES M A)
                                                       P)
                                            (REMAINDER (TIMES M B)
                                                       P))
                                     (NOT (EQUAL (REMAINDER M P)
                                                 0))
                                     (PRIME P))
                                (EQUAL (EQUAL (REMAINDER A P)
                                              (REMAINDER B P))
                                       T))
                       ((USE (PRIME-KEY-REWRITE (A M)
                                                (B (PDIFFERENCE A B)))
                             (EQUAL-MODS-TRICK-2 (A (TIMES M A))
                                                 (B (TIMES M B))))
                        (DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2)))
(PROVE-LEMMA PRODUCT-DIVIDES-LEMMA (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z)
                             0)
                      (EQUAL (REMAINDER (TIMES Y X)
                                        (TIMES Y Z))
                             0)))
(PROVE-LEMMA PRODUCT-DIVIDES (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X P)
                                  0)
                           (EQUAL (REMAINDER X Q)
                                  0)
                           (PRIME P)
                           (PRIME Q)
                           (NOT (EQUAL P Q)))
                      (EQUAL (REMAINDER X (TIMES P Q))
                             0)))
(PROVE-LEMMA THM-53-SPECIALIZED-TO-PRIMES NIL
             (IMPLIES (AND (PRIME P)
                           (PRIME Q)
                           (NOT (EQUAL P Q))
                           (EQUAL (REMAINDER A P)
                                  (REMAINDER B P))
                           (EQUAL (REMAINDER A Q)
                                  (REMAINDER B Q)))
                      (EQUAL (REMAINDER A (TIMES P Q))
                             (REMAINDER B (TIMES P Q))))
             NIL

;   The proof of this consists merely of applying trick 1 to backwards chain
;   from A mod PQ = B mod PQ to PQ A-B, then use PRODUCT-DIVIDES to back up to
;   P A-B and Q A-B, and then use trick 2 to come back to A mod P = B mod P.

             )
(PROVE-LEMMA COROLLARY-53 (REWRITE)
                       (IMPLIES (AND (PRIME P)
                                     (PRIME Q)
                                     (NOT (EQUAL P Q))
                                     (EQUAL (REMAINDER A P)
                                            (REMAINDER B P))
                                     (EQUAL (REMAINDER A Q)
                                            (REMAINDER B Q))
                                     (NUMBERP B)
                                     (LESSP B (TIMES P Q)))
                                (EQUAL (EQUAL (REMAINDER A (TIMES P Q))
                                              B)
                                       T))
                       ((USE (THM-53-SPECIALIZED-TO-PRIMES))
                        (DISABLE THM-53-SPECIALIZED-TO-PRIMES)))
(PROVE-LEMMA THM-55-SPECIALIZED-TO-PRIMES (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER M P)
                                       0)))
                      (EQUAL (EQUAL (REMAINDER (TIMES M X)
                                               P)
                                    (REMAINDER (TIMES M Y)
                                               P))
                             (EQUAL (REMAINDER X P)
                                    (REMAINDER Y P)))))
(PROVE-LEMMA COROLLARY-55 (REWRITE)
                       (IMPLIES (PRIME P)
                                (EQUAL (EQUAL (REMAINDER (TIMES M X)
                                                         P)
                                              (REMAINDER M P))
                                       (OR (EQUAL (REMAINDER M P)
                                                  0)
                                           (EQUAL (REMAINDER X P)
                                                  1))))
                       ((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1)))
                        (DISABLE THM-55-SPECIALIZED-TO-PRIMES)))
(DEFN ALL-DISTINCT (L)
  (IF (NLISTP L)
      T
      (AND (NOT (MEMBER (CAR L)
                        (CDR L)))
           (ALL-DISTINCT (CDR L)))))
(DEFN ALL-LESSEQP (L N)
  (IF (NLISTP L)
      T
      (AND (NOT (LESSP N (CAR L)))
           (ALL-LESSEQP (CDR L)
                        N))))
(DEFN ALL-NON-ZEROP (L)
  (IF (NLISTP L)
      T
      (AND (NOT (ZEROP (CAR L)))
           (ALL-NON-ZEROP (CDR L)))))
(DEFN POSITIVES (N)
  (IF (ZEROP N)
      NIL
      (CONS N (POSITIVES (SUB1 N)))))
(PROVE-LEMMA LISTP-POSITIVES (REWRITE)
             (EQUAL (LISTP (POSITIVES N))
                    (NOT (ZEROP N))))
(PROVE-LEMMA CAR-POSITIVES (REWRITE)
             (EQUAL (CAR (POSITIVES N))
                    (IF (ZEROP N)
                        0 N)))
(PROVE-LEMMA MEMBER-POSITIVES (REWRITE)
             (EQUAL (MEMBER X (POSITIVES N))
                    (IF (ZEROP X)
                        F
                        (LESSP X (ADD1 N)))))
(PROVE-LEMMA ALL-NON-ZEROP-DELETE (REWRITE)
             (IMPLIES (ALL-NON-ZEROP L)
                      (ALL-NON-ZEROP (DELETE X L))))
(PROVE-LEMMA ALL-DISTINCT-DELETE (REWRITE)
             (IMPLIES (ALL-DISTINCT L)
                      (ALL-DISTINCT (DELETE X L))))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-1 (REWRITE)
             (IMPLIES (AND (ALL-DISTINCT L)
                           (ALL-LESSEQP L (ADD1 N)))
                      (ALL-LESSEQP (DELETE (ADD1 N)
                                           L)
                                   N)))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-2 (REWRITE)
             (IMPLIES (AND (NOT (MEMBER (ADD1 N)
                                        X))
                           (ALL-LESSEQP X (ADD1 N)))
                      (ALL-LESSEQP X N)))
(PROVE-LEMMA PERM-MEMBER (REWRITE)
             (IMPLIES (AND (PERM A B)
                           (MEMBER X A))
                      (MEMBER X B)))
(DEFN PIGEON-HOLE-INDUCTION (L)
  (IF (LISTP L)
      (IF (MEMBER (LENGTH L)
                  L)
          (PIGEON-HOLE-INDUCTION (DELETE (LENGTH L)
                                         L))
          (PIGEON-HOLE-INDUCTION (CDR L)))
      T))
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE NIL
                       (IMPLIES (AND (ALL-NON-ZEROP L)
                                     (ALL-DISTINCT L)
                                     (ALL-LESSEQP L (LENGTH L)))
                                (PERM (POSITIVES (LENGTH L))
                                      L))
                       ((INDUCT (PIGEON-HOLE-INDUCTION L)))

;   We have proved this theorem without this induction hint, but that proof
;   requires many more lemmas. This is a good example of a theorem whose
;   induction is not suggested by any term in the theorem.

                       )
(PROVE-LEMMA PERM-TIMES-LIST NIL
             (IMPLIES (PERM L1 L2)
                      (EQUAL (TIMES-LIST L1)
                             (TIMES-LIST L2))))
(PROVE-LEMMA TIMES-LIST-POSITIVES (REWRITE)
             (EQUAL (TIMES-LIST (POSITIVES N))
                    (FACT N)))
(PROVE-LEMMA TIMES-LIST-EQUAL-FACT (REWRITE)
                       (IMPLIES (PERM (POSITIVES N)
                                      L)
                                (EQUAL (TIMES-LIST L)
                                       (FACT N)))
                       ((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
                                              (L2 L)))
                        (DISABLE PERM-TIMES-LIST)))
(PROVE-LEMMA PRIME-FACT (REWRITE)
                       (IMPLIES (AND (PRIME P)
                                     (LESSP N P))
                                (NOT (EQUAL (REMAINDER (FACT N)
                                                       P)
                                            0)))
                       ((INDUCT (FACT N))))
(DEFN S (N M P)
  (IF (ZEROP N)
      NIL
      (CONS (REMAINDER (TIMES M N)
                       P)
            (S (SUB1 N)
               M P))))
(PROVE-LEMMA REMAINDER-TIMES-LIST-S NIL
             (EQUAL (REMAINDER (TIMES-LIST (S N M P))
                               P)
                    (REMAINDER (TIMES (FACT N)
                                      (EXP M N))
                               P)))
(PROVE-LEMMA ALL-DISTINCT-S-LEMMA (REWRITE)
                       (IMPLIES (AND (PRIME P)
                                     (NOT (EQUAL (REMAINDER M P)
                                                 0))
                                     (NUMBERP N1)
                                     (LESSP N2 N1)
                                     (LESSP N1 P))
                                (NOT (MEMBER (REMAINDER (TIMES M N1)
                                                        P)
                                             (S N2 M P))))
                       ((INDUCT (S N2 M P))))
(PROVE-LEMMA ALL-DISTINCT-S (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER M P)
                                       0))
                           (LESSP N P))
                      (ALL-DISTINCT (S N M P))))
(PROVE-LEMMA ALL-NON-ZEROP-S (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER M P)
                                       0))
                           (LESSP N P))
                      (ALL-NON-ZEROP (S N M P))))
(PROVE-LEMMA ALL-LESSEQP-S (REWRITE)
             (IMPLIES (NOT (ZEROP P))
                      (ALL-LESSEQP (S N M P)
                                   (SUB1 P))))
(PROVE-LEMMA LENGTH-S (REWRITE)
             (EQUAL (LENGTH (S N M P))
                    (FIX N)))
(PROVE-LEMMA FERMAT-THM (REWRITE)
                       (IMPLIES (AND (PRIME P)
                                     (NOT (EQUAL (REMAINDER M P)
                                                 0)))
                                (EQUAL (REMAINDER (EXP M (SUB1 P))
                                                  P)
                                       1))
                       ((USE (PIGEON-HOLE-PRINCIPLE (L (S (SUB1 P)
                                                          M P)))
                             (REMAINDER-TIMES-LIST-S (N (SUB1 P))))
                        (DISABLE PIGEON-HOLE-PRINCIPLE 
                                 REMAINDER-TIMES-LIST-S)))
(PROVE-LEMMA
  CRYPT-INVERTS-STEP-1 NIL
  (IMPLIES (PRIME P)
           (EQUAL (REMAINDER (TIMES M (EXP M
                                           (TIMES K
                                                  (SUB1 P))))
                             P)
                  (REMAINDER M P))))
(PROVE-LEMMA
  CRYPT-INVERTS-STEP-1A
  (REWRITE)
  (IMPLIES (PRIME P)
           (EQUAL (REMAINDER (TIMES M (EXP M
                                           (TIMES K
                                                  (SUB1 P)
                                                  (SUB1 Q))))
                             P)
                  (REMAINDER M P)))
  ((USE (CRYPT-INVERTS-STEP-1 (K (TIMES K (SUB1 Q)))))
   (DISABLE CRYPT-INVERTS-STEP-1)))
(PROVE-LEMMA
  CRYPT-INVERTS-STEP-1B
  (REWRITE)
  (IMPLIES (PRIME Q)
           (EQUAL (REMAINDER (TIMES M (EXP M
                                           (TIMES K
                                                  (SUB1 P)
                                                  (SUB1 Q))))
                             Q)
                  (REMAINDER M Q)))
  ((USE (CRYPT-INVERTS-STEP-1 (P Q)
                              (K (TIMES K (SUB1 P)))))
   (DISABLE CRYPT-INVERTS-STEP-1)))
(PROVE-LEMMA CRYPT-INVERTS-STEP-2 (REWRITE)
             (IMPLIES
               (AND (PRIME P)
                    (PRIME Q)
                    (NOT (EQUAL P Q))
                    (NUMBERP M)
                    (LESSP M (TIMES P Q))
                    (EQUAL (REMAINDER ED (TIMES (SUB1 P)
                                                (SUB1 Q)))
                           1))
               (EQUAL (REMAINDER (EXP M ED)
                                 (TIMES P Q))
                      M)))
(PROVE-LEMMA CRYPT-INVERTS NIL
             (IMPLIES
               (AND (PRIME P)
                    (PRIME Q)
                    (NOT (EQUAL P Q))
                    (EQUAL N (TIMES P Q))
                    (NUMBERP M)
                    (LESSP M N)
                    (EQUAL (REMAINDER (TIMES E D)
                                      (TIMES (SUB1 P)
                                             (SUB1 Q)))
                           1))
               (EQUAL (CRYPT (CRYPT M E N)
                             D N)
                      M))
             NIL)

(MAKE-LIB "rsa" T)