1(* ------------------------------------------------------------------------- *) 2(* Congruences from Number Theory *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "congruences"; 12 13(* ------------------------------------------------------------------------- *) 14 15(* Purpose: 16 subgroupTheory has finite_abelian_Fermat 17 groupInstancesTheory has Z_star and mult_mod 18 For Z_star p, show that MOD_MUL_INV can be evaluted by Fermat's Little Theorem. 19 For mult_mod p, show that MOD_MULT_INV can be evaluted by Fermat's Little Theorem. 20*) 21 22 23 24(* val _ = load "jcLib"; *) 25open jcLib; 26 27(* Get required theories *) 28(* (* val _ = load "groupTheory"; *) *) 29(* val _ = load "subgroupTheory"; *) 30(* val _ = load "groupInstancesTheory"; *) 31open groupTheory subgroupTheory groupInstancesTheory; 32 33(* val _ = load "groupProductTheory"; *) 34open groupProductTheory; 35 36(* Get dependent theories in lib *) 37(* (* val _ = load "helperNumTheory"; -- in monoidTheory via groupTheory *) *) 38(* (* val _ = load "helperSetTheory"; -- in monoidTheory via groupTheory *) *) 39open helperNumTheory helperSetTheory; 40 41(* (* val _ = load "EulerTheory"; *) *) 42open EulerTheory; 43 44(* open dependent theories *) 45open arithmeticTheory; 46(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 47open dividesTheory; 48 49 50(* ------------------------------------------------------------------------- *) 51(* Congruences Documentation *) 52(* ------------------------------------------------------------------------- *) 53(* Definitions and Theorems (# are exported): 54 55 Fermat's Little Theorem: 56 fermat_little |- !p a. prime p /\ 0 < a /\ a < p ==> (a ** (p - 1) MOD p = 1) 57 fermat_little_alt |- !p a. prime p ==> (a ** (p - 1) MOD p = if a MOD p = 0 then 0 else 1) 58 fermat_little_thm |- !p. prime p ==> !a. a ** p MOD p = a MOD p 59 fermat_roots |- !p. prime p ==> !x y z. (x ** p + y ** p = z ** p) ==> ((x + y) MOD p = z MOD p) 60 61 Multiplicative Inverse by Fermat's Little Theorem: 62 Zstar_inverse |- !p. prime p ==> !a. 0 < a /\ a < p ==> ((Zstar p).inv a = a ** (p - 2) MOD p) 63 Zstar_inverse_compute |- !p a. (Zstar p).inv a = 64 if prime p /\ 0 < a /\ a < p then a ** (p - 2) MOD p else (Zstar p).inv a 65 PRIME_2 |- prime 2 66 PRIME_3 |- prime 3 67 PRIME_5 |- prime 5 68 PRIME_7 |- prime 7 69 mult_mod_inverse |- !p. prime p ==> 70 !a. 0 < a /\ a < p ==> ((mult_mod p).inv a = a ** (p - 2) MOD p) 71 mult_mod_inverse_compute |- !p a. (mult_mod p).inv a = 72 if prime p /\ 0 < a /\ a < p then a ** (p - 2) MOD p else (mult_mod p).inv a 73*) 74 75(* ------------------------------------------------------------------------- *) 76(* Fermat's Little Theorem (by Zp finite abelian group) *) 77(* ------------------------------------------------------------------------- *) 78 79(* Theorem: For prime p, 0 < a < p, a**(p-1) = 1 (mod p) *) 80(* Proof: 81 Since 0 < a < p, a IN (Zstar p).carrier, 82 and (Zstar p) is a FiniteAbelian Group, by Zstar_finite_abelian_group 83 and CARD (Zstar p).carrier = (p-1) by Zstar_property. 84 this follows by finite_abelian_Fermat and Zstar_exp, which relates group_exp to EXP. 85 86> finite_abelian_Fermat |> ISPEC ``(Zstar p)``; 87val it = |- !a. FiniteAbelianGroup (Zstar p) /\ a IN (Zstar p).carrier ==> 88 ((Zstar p).exp a (CARD (Zstar p).carrier) = (Zstar p).id): thm 89*) 90val fermat_little = store_thm( 91 "fermat_little", 92 ``!p a. prime p /\ 0 < a /\ a < p ==> (a ** (p - 1) MOD p = 1)``, 93 rpt strip_tac >> 94 `FiniteAbelianGroup (Zstar p)` by rw_tac std_ss[Zstar_finite_abelian_group] >> 95 `a IN (Zstar p).carrier /\ ((Zstar p).id = 1)` by rw[Zstar_def, residue_def] >> 96 `CARD (Zstar p).carrier = p - 1` by rw_tac std_ss[PRIME_POS, Zstar_property] >> 97 metis_tac[finite_abelian_Fermat, Zstar_exp]); 98 99(* Theorem: Fermat's Little Theorem for all a: (a**(p-1) MOD p = if (a MOD p = 0) then 0 else 1 when p is prime. *) 100(* Proof: by cases of a, and restricted Fermat's Little Theorem. *) 101val fermat_little_alt = store_thm( 102 "fermat_little_alt", 103 ``!p a. prime p ==> (a**(p-1) MOD p = if (a MOD p = 0) then 0 else 1)``, 104 rpt strip_tac >> 105 `0 < p /\ 1 < p` by rw_tac std_ss[PRIME_POS, ONE_LT_PRIME] >> 106 `a ** (p-1) MOD p = (a MOD p) ** (p-1) MOD p` by metis_tac[EXP_MOD] >> 107 rw_tac std_ss[] >| [ 108 `0 < (p - 1)` by decide_tac >> 109 `?k. (p - 1) = SUC k` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >> 110 rw[EXP], 111 `0 < a MOD p` by decide_tac >> 112 `a MOD p < p` by rw[MOD_LESS] >> 113 metis_tac[fermat_little] 114 ]); 115 116(* Theorem: For prime p, a**p = a (mod p) *) 117(* Proof: by fermat_little. *) 118val fermat_little_thm = store_thm( 119 "fermat_little_thm", 120 ``!p. prime p ==> !a. a ** p MOD p = a MOD p``, 121 rpt strip_tac >> 122 `0 < p` by rw_tac std_ss[PRIME_POS] >> 123 `a ** p MOD p = (a MOD p) ** p MOD p` by rw_tac std_ss[MOD_EXP] >> 124 Cases_on `a MOD p = 0` >- 125 metis_tac[ZERO_MOD, ZERO_EXP, NOT_ZERO_LT_ZERO] >> 126 `0 < a MOD p` by decide_tac >> 127 `a MOD p < p` by rw_tac std_ss[MOD_LESS] >> 128 `p = SUC (p-1)` by decide_tac >> 129 `(a MOD p) ** p MOD p = ((a MOD p) * (a MOD p) ** (p-1)) MOD p` by metis_tac[EXP] >> 130 `_ = ((a MOD p) * (a MOD p) ** (p-1) MOD p) MOD p` by metis_tac[MOD_TIMES2, MOD_MOD] >> 131 `_ = ((a MOD p) * 1) MOD p` by rw_tac std_ss[fermat_little] >> 132 `_ = a MOD p` by rw_tac std_ss[MULT_RIGHT_1, MOD_MOD] >> 133 rw_tac std_ss[]); 134 135(* Theorem: For prime p > 2, x ** p + y ** p = z ** p ==> x + y = z (mod p) *) 136(* Proof: 137 x ** p + y ** p = z ** p 138 ==> x ** p + y ** p = z ** p mod p 139 ==> x + y = z mod p by Fermat's Little Theorem. 140*) 141val fermat_roots = store_thm( 142 "fermat_roots", 143 ``!p. prime p ==> !x y z. (x ** p + y ** p = z ** p) ==> ((x + y) MOD p = z MOD p)``, 144 rpt strip_tac >> 145 `0 < p` by rw_tac std_ss[PRIME_POS] >> 146 `z ** p MOD p = (x ** p + y ** p) MOD p` by rw_tac std_ss[] >> 147 `_ = (x ** p MOD p + y ** p MOD p) MOD p` by metis_tac[MOD_PLUS] >> 148 `_ = (x MOD p + y MOD p) MOD p` by rw_tac std_ss[fermat_little_thm] >> 149 `_ = (x + y) MOD p` by rw_tac std_ss[MOD_PLUS] >> 150 metis_tac[fermat_little_thm]); 151 152(* ------------------------------------------------------------------------- *) 153(* Multiplicative Inverse by Fermat's Little Theorem *) 154(* ------------------------------------------------------------------------- *) 155 156(* There is already: 157- Zstar_inv; 158> val it = |- !p. prime p ==> !x. 0 < x /\ x < p ==> ((Zstar p).inv x = (Zstar p).exp x (order (Zstar p) x - 1)) : thm 159*) 160 161(* Theorem: For prime p, (Zstar p).inv a = a**(p-2) MOD p *) 162(* Proof: 163 a * (a ** (p-2) MOD p = a**(p-1) MOD p = 1 by fermat_little. 164 Hence (a ** (p-2) MOD p) is the multiplicative inverse by group_rinv_unique. 165*) 166val Zstar_inverse = store_thm( 167 "Zstar_inverse", 168 ``!p. prime p ==> !a. 0 < a /\ a < p ==> ((Zstar p).inv a = (a**(p-2)) MOD p)``, 169 rpt strip_tac >> 170 `a IN (Zstar p).carrier` by rw_tac std_ss[Zstar_element] >> 171 `Group (Zstar p)` by rw_tac std_ss[Zstar_group] >> 172 `(Zstar p).id = 1` by rw_tac std_ss[Zstar_property] >> 173 `(Zstar p).exp a (p-2) = a**(p-2) MOD p` by rw_tac std_ss[Zstar_exp] >> 174 `0 < p` by decide_tac >> 175 `SUC (p-2) = p - 1` by decide_tac >> 176 `(Zstar p).op a (a**(p-2) MOD p) = (a * (a**(p-2) MOD p)) MOD p` by rw_tac std_ss[Zstar_property] >> 177 `_ = ((a MOD p) * (a**(p-2) MOD p)) MOD p` by rw_tac std_ss[LESS_MOD] >> 178 `_ = (a * a**(p-2)) MOD p` by rw_tac std_ss[MOD_TIMES2] >> 179 `_ = a ** (p-1) MOD p` by metis_tac[EXP] >> 180 `_ = 1` by rw_tac std_ss[fermat_little] >> 181 metis_tac[group_rinv_unique, group_exp_element]); 182 183(* Theorem: As function, for prime p, (Zstar p).inv a = a**(p-2) MOD p *) 184(* Proof: by Zstar_inverse. *) 185val Zstar_inverse_compute = store_thm( 186 "Zstar_inverse_compute", 187 ``!p a. (Zstar p).inv a = if (prime p /\ 0 < a /\ a < p) then (a**(p-2) MOD p) else ((Zstar p).inv a)``, 188 rw_tac std_ss[Zstar_inverse]); 189 190(* Theorem: 2 is prime. *) 191(* Proof: by definition of prime. *) 192val PRIME_2 = store_thm( 193 "PRIME_2", 194 ``prime 2``, 195 rw_tac std_ss [prime_def] >> 196 `0 < 2` by decide_tac >> 197 `0 < b /\ b <= 2` by metis_tac[DIVIDES_LE, ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 198 rw_tac arith_ss []); 199 200(* Theorem: 3 is prime. *) 201(* Proof: by definition of prime. *) 202val PRIME_3 = store_thm( 203 "PRIME_3", 204 ``prime 3``, 205 rw_tac std_ss[prime_def] >> 206 `b <= 3` by rw_tac std_ss[DIVIDES_LE] >> 207 `(b=0) \/ (b=1) \/ (b=2) \/ (b=3)` by decide_tac >- 208 fs[] >- 209 fs[] >- 210 full_simp_tac arith_ss [divides_def] >> 211 metis_tac[]); 212 213(* Theorem: 5 is prime. *) 214(* Proof: by definition of prime. *) 215val PRIME_5 = store_thm( 216 "PRIME_5", 217 ``prime 5``, 218 rw_tac std_ss[prime_def] >> 219 `0 < 5` by decide_tac >> 220 `0 < b /\ b <= 5` by metis_tac[DIVIDES_LE, ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 221 `(b = 1) \/ (b = 2) \/ (b = 3) \/ (b = 4) \/ (b = 5)` by decide_tac >- 222 rw_tac std_ss[] >- 223 full_simp_tac arith_ss [divides_def] >- 224 full_simp_tac arith_ss [divides_def] >- 225 full_simp_tac arith_ss [divides_def] >> 226 rw_tac std_ss[]); 227 228(* Theorem: 7 is prime. *) 229(* Proof: by definition of prime. *) 230val PRIME_7 = store_thm( 231 "PRIME_7", 232 ``prime 7``, 233 rw_tac std_ss[prime_def] >> 234 `0 < 7` by decide_tac >> 235 `0 < b /\ b <= 7` by metis_tac[DIVIDES_LE, ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 236 `(b = 1) \/ (b = 2) \/ (b = 3) \/ (b = 4) \/ (b = 5) \/ (b = 6) \/ (b = 7)` by decide_tac >- 237 rw_tac std_ss[] >- 238 full_simp_tac arith_ss [divides_def] >- 239 full_simp_tac arith_ss [divides_def] >- 240 full_simp_tac arith_ss [divides_def] >- 241 full_simp_tac arith_ss [divides_def] >- 242 full_simp_tac arith_ss [divides_def] >> 243 rw_tac std_ss[]); 244 245(* These computation uses Zstar_inv_compute of groupInstances. 246 247- val _ = computeLib.add_persistent_funs ["PRIME_5"]; 248- EVAL ``prime 5``; 249> val it = |- prime 5 <=> T : thm 250- EVAL ``(Zstar 5).inv 2``; 251> val it = |- (Zstar 5).inv 2 = 3 : thm 252- EVAL ``(Zstar 5).id``; 253> val it = |- (Zstar 5).id = 1 : thm 254- EVAL ``(Zstar 5).op 2 3``; 255> val it = |- (Zstar 5).op 2 3 = 1 : thm 256- EVAL ``(Zstar 5).inv 2``; 257> val it = |- (Zstar 5).inv 2 = 3 : thm 258- EVAL ``(Zstar 5).inv 3``; 259> val it = |- (Zstar 5).inv 3 = 2 : thm 260*) 261 262 263(* 264val th = mk_thm([], ``MOD_MULT_INV 7 x = (x ** 5) MOD 7``); 265val _ = save_thm("th", th); 266val _ = computeLib.add_persistent_funs ["th"]; 267 268val _ = computeLib.add_persistent_funs [("Zstar5_inv", Zstar5_inv)]; 269EVAL ``(Zstar 5).op 2 3``; 270> val it = |- (Zstar 5).op 2 3 = 1 : thm 271EVAL ``(Zstar 5).inv 2``; 272> val it = |- (Zstar 5).inv 2 = MOD_MUL_INV 5 2 : thm (before) 273> val it = |- (Zstar 5).inv 2 = 3 : thm 274*) 275 276 277(* There is already this in groupInstancesTheory: 278 279- mult_mod_inv; 280> val it = |- !p. prime p ==> !x. 0 < x /\ x < p ==> ((mult_mod p).inv x = (mult_mod p).exp x (order (mult_mod p) x - 1)) : thm 281*) 282 283(* Theorem: For prime p, (mult_mod p).inv a = a**(p-2) MOD p *) 284(* Proof: 285 a * (a ** (p-2) MOD p = a**(p-1) MOD p = 1 by fermat_little. 286 Hence (a ** (p-2) MOD p) is the multiplicative inverse by group_rinv_unique. 287*) 288val mult_mod_inverse = store_thm( 289 "mult_mod_inverse", 290 ``!p. prime p ==> !a. 0 < a /\ a < p ==> ((mult_mod p).inv a = (a**(p-2)) MOD p)``, 291 rpt strip_tac >> 292 `a IN (mult_mod p).carrier` by rw_tac std_ss[mult_mod_property] >> 293 `Group (mult_mod p)` by rw_tac std_ss[mult_mod_group] >> 294 `(mult_mod p).exp a (p-2) = (a**(p-2) MOD p)` by rw_tac std_ss[mult_mod_exp] >> 295 `0 < p /\ 1 < p` by rw_tac std_ss[PRIME_POS, ONE_LT_PRIME] >> 296 `SUC (p-2) = p - 1` by decide_tac >> 297 `(mult_mod p).exp a (p-2) IN (mult_mod p).carrier` by rw_tac std_ss[group_exp_element] >> 298 `(mult_mod p).op a (a**(p-2) MOD p) = (a * (a**(p-2) MOD p)) MOD p` by rw_tac std_ss[mult_mod_property] >> 299 `_ = (a * a**(p-2)) MOD p` by metis_tac[MOD_TIMES2, MOD_MOD] >> 300 `_ = a ** (p-1) MOD p` by metis_tac[EXP] >> 301 `_ = 1` by rw_tac std_ss[fermat_little] >> 302 metis_tac[group_rinv_unique, mult_mod_property]); 303 304(* Theorem: As function, for prime p, (mult_mod p).inv a = a**(p-2) MOD p *) 305(* Proof: by mult_mod_inverse. *) 306val mult_mod_inverse_compute = store_thm( 307 "mult_mod_inverse_compute", 308 ``!p a. (mult_mod p).inv a = if (prime p /\ 0 < a /\ a < p) then (a**(p-2) MOD p) else (mult_mod p).inv a``, 309 rw_tac std_ss[mult_mod_inverse]); 310 311(* These computation uses mult_mod_inv_compute of groupInstances. 312 313- val _ = computeLib.add_persistent_funs ["PRIME_7"]; 314- EVAL ``prime 7``; 315> val it = |- prime 7 <=> T : thm 316- EVAL ``(mult_mod 7).id``; 317> val it = |- (mult_mod 7).id = 1 : thm 318- EVAL ``(mult_mod 7).op 5 3``; 319> val it = |- (mult_mod 7).op 5 3 = 1 : thm 320- EVAL ``(mult_mod 7).inv 5``; 321> val it = |- (mult_mod 7).inv 5 = 3 : thm 322- EVAL ``(mult_mod 7).inv 3``; 323> val it = |- (mult_mod 7).inv 3 = 5 : thm 324*) 325(* ------------------------------------------------------------------------- *) 326 327(* export theory at end *) 328val _ = export_theory(); 329 330(*===========================================================================*) 331