Tutorial/Number_theory.ml

   1 needs "Library/prime.ml";;
   2 needs "Library/pocklington.ml";;
   3 needs "Library/binomial.ml";;
   4
   5 prioritize_num();;
   6
   7 let FERMAT_PRIME_CONV n =
   8   let tm = subst [mk_small_numeral n,`x:num`] `prime(2 EXP (2 EXP x) + 1)` in
   9   (RAND_CONV NUM_REDUCE_CONV THENC PRIME_CONV) tm;;
  10
  11 FERMAT_PRIME_CONV 0;;
  12 FERMAT_PRIME_CONV 1;;
  13 FERMAT_PRIME_CONV 2;;
  14 FERMAT_PRIME_CONV 3;;
  15 FERMAT_PRIME_CONV 4;;
  16 FERMAT_PRIME_CONV 5;;
  17 FERMAT_PRIME_CONV 6;;
  18 FERMAT_PRIME_CONV 7;;
  19 FERMAT_PRIME_CONV 8;;
  20
  21 let CONG_TRIVIAL = prove
  22  (`!x y. n divides x /\ n divides y ==> (x == y) (mod n)`,
  23   MESON_TAC[CONG_0; CONG_SYM; CONG_TRANS]);;
  24
  25 let LITTLE_CHECK_CONV tm =
  26   EQT_ELIM((RATOR_CONV(LAND_CONV NUM_EXP_CONV) THENC CONG_CONV) tm);;
  27
  28 LITTLE_CHECK_CONV `(9 EXP 8 == 9) (mod 3)`;;
  29 LITTLE_CHECK_CONV `(9 EXP 3 == 9) (mod 3)`;;
  30 LITTLE_CHECK_CONV `(10 EXP 7 == 10) (mod 7)`;;
  31 LITTLE_CHECK_CONV `(2 EXP 7 == 2) (mod 7)`;;
  32 LITTLE_CHECK_CONV `(777 EXP 13 == 777) (mod 13)`;;
  33
  34 let DIVIDES_FACT_PRIME = prove
  35  (`!p. prime p ==> !n. p divides (FACT n) <=> p <= n`,
  36   GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT; LE] THENL
  37    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_0; PRIME_1];
  38     ASM_MESON_TAC[PRIME_DIVPROD_EQ; DIVIDES_LE; NOT_SUC; DIVIDES_REFL;
  39                   ARITH_RULE `~(p <= n) /\ p <= SUC n ==> p = SUC n`]]);;
  40
  41 let DIVIDES_BINOM_PRIME = prove
  42  (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
  43   REPEAT STRIP_TAC THEN
  44   MP_TAC(AP_TERM `(divides) p` (SPECL [`p - n`; `n:num`] BINOM_FACT)) THEN
  45   ASM_SIMP_TAC[DIVIDES_FACT_PRIME; PRIME_DIVPROD_EQ; SUB_ADD; LT_IMP_LE] THEN
  46   ASM_REWRITE_TAC[GSYM NOT_LT; LT_REFL] THEN
  47   ASM_SIMP_TAC[ARITH_RULE `0 < n /\ n < p ==> p - n < p`]);;
  48
  49 let DIVIDES_NSUM = prove
  50  (`!m n. (!i. m <= i /\ i <= n ==> p divides f(i)) ==> p divides nsum(m..n) f`,
  51   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
  52   ASM_MESON_TAC[LE; LE_TRANS; DIVIDES_0; DIVIDES_ADD; LE_REFL]);;
  53
  54 let FLT_LEMMA = prove
  55  (`!p a b. prime p ==> ((a + b) EXP p == a EXP p + b EXP p) (mod p)`,
  56   REPEAT STRIP_TAC THEN REWRITE_TAC[BINOMIAL_THEOREM] THEN
  57   SUBGOAL_THEN `1 <= p /\ 0 < p` STRIP_ASSUME_TAC THENL
  58    [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_IMP_NZ) THEN ARITH_TAC; ALL_TAC] THEN
  59   ASM_SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0; ARITH; NSUM_CLAUSES_RIGHT] THEN
  60   REWRITE_TAC[SUB_0; SUB_REFL; EXP; binom; BINOM_REFL; MULT_CLAUSES] THEN
  61   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a + b = (b + 0) + a`] THEN
  62   REPEAT(MATCH_MP_TAC CONG_ADD THEN REWRITE_TAC[CONG_REFL]) THEN
  63   REWRITE_TAC[CONG_0] THEN MATCH_MP_TAC DIVIDES_NSUM THEN
  64   ASM_MESON_TAC[DIVIDES_RMUL; DIVIDES_BINOM_PRIME; ARITH_RULE
  65    `0 < p /\ 1 <= i /\ i <= p - 1 ==> 0 < i /\ i < p`]);;
  66
  67 let FERMAT_LITTLE = prove
  68  (`!p a. prime p ==> (a EXP p == a) (mod p)`,
  69   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  70   INDUCT_TAC THENL
  71    [ASM_MESON_TAC[EXP_EQ_0; CONG_REFL; PRIME_0];
  72     ASM_MESON_TAC[ADD1; FLT_LEMMA; EXP_ONE; CONG_ADD; CONG_TRANS; CONG_REFL]]);;
  73
  74 let FERMAT_LITTLE_COPRIME = prove
  75  (`!p a. prime p /\ coprime(a,p) ==> (a EXP (p - 1) == 1) (mod p)`,
  76   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
  77   EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
  78   ASM_SIMP_TAC[PRIME_IMP_NZ; ARITH_RULE `~(p = 0) ==> SUC(p - 1) = p`] THEN
  79   ASM_SIMP_TAC[FERMAT_LITTLE; MULT_CLAUSES]);;
  80
  81 let FERMAT_LITTLE_VARIANT = prove
  82  (`!p a. prime p ==> (a EXP (1 + m * (p - 1)) == a) (mod p)`,
  83   REPEAT STRIP_TAC THEN
  84   FIRST_ASSUM(DISJ_CASES_TAC o SPEC `a:num` o MATCH_MP PRIME_COPRIME_STRONG)
  85   THENL [ASM_MESON_TAC[CONG_TRIVIAL; ADD_AC; ADD1; DIVIDES_REXP_SUC];
  86          ALL_TAC] THEN
  87   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
  88   REWRITE_TAC[EXP_ADD; EXP_1] THEN MATCH_MP_TAC CONG_MULT THEN
  89   REWRITE_TAC[GSYM EXP_EXP; CONG_REFL] THEN
  90   ASM_MESON_TAC[COPRIME_SYM; COPRIME_EXP; PHI_PRIME; FERMAT_LITTLE_COPRIME]);;
  91
  92 let RSA = prove
  93  (`prime p /\ prime q /\ ~(p = q) /\
  94    (d * e == 1) (mod ((p - 1) * (q - 1))) /\
  95    plaintext < p * q /\ (ciphertext = (plaintext EXP e) MOD (p * q))
  96    ==> (plaintext = (ciphertext EXP d) MOD (p * q))`,
  97   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  98   ASM_SIMP_TAC[MOD_EXP_MOD; MULT_EQ_0; PRIME_IMP_NZ; EXP_EXP] THEN
  99   SUBGOAL_THEN `(plaintext == plaintext EXP (e * d)) (mod (p * q))` MP_TAC THENL
 100    [ALL_TAC; ASM_SIMP_TAC[CONG; MULT_EQ_0; PRIME_IMP_NZ; MOD_LT]] THEN
 101   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 102   FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [CONG_TO_1]) THENL
 103    [ASM_MESON_TAC[MULT_EQ_1; ARITH_RULE `p - 1 = 1 <=> p = 2`]; ALL_TAC] THEN
 104   MATCH_MP_TAC CONG_CHINESE THEN ASM_SIMP_TAC[DISTINCT_PRIME_COPRIME] THEN
 105   ASM_MESON_TAC[FERMAT_LITTLE_VARIANT; MULT_AC; CONG_SYM]);;