1(* ------------------------------------------------------------------------- *) 2(* Order Computations *) 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 "computeOrder"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories local *) 23 24(* open dependent theories *) 25(* val _ = load "fieldInstancesTheory"; *) 26 27(* Get dependent theories in lib *) 28(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 29(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 30(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *) 31(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *) 32open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; 33open pred_setTheory listTheory arithmeticTheory; 34 35(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 36(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 37open dividesTheory gcdTheory; 38 39(* val _ = load "fieldInstancesTheory"; *) 40open monoidInstancesTheory; 41open groupInstancesTheory; 42open ringInstancesTheory; 43open fieldInstancesTheory; 44open groupOrderTheory; 45open monoidOrderTheory; 46 47(* val _ = load "GaussTheory"; *) 48open EulerTheory; 49open GaussTheory; 50 51(* val _ = load "computeBasicTheory"; *) 52open computeBasicTheory; 53open logrootTheory logPowerTheory; 54 55 56(* ------------------------------------------------------------------------- *) 57(* Order Computations Documentation *) 58(* ------------------------------------------------------------------------- *) 59(* Datatype and Overloading: 60 sqrt_compute = root_compute 2 61*) 62(* Definitions and Theorems (# are exported): 63 64 Order Computation: 65 ordz_seek_def |- !n m j c. ordz_seek m n c j = if c <= j then 0 66 else if n ** j MOD m = 1 then j 67 else ordz_seek m n c (SUC j) 68 ordz_seek_alt |- !m n c j. ordz_seek m n c j = if c <= j then 0 69 else if n ** j MOD m = 1 then j 70 else ordz_seek m n c (j + 1) 71 ordz_seek_over |- !m n c j. c <= j ==> (ordz_seek m n c j = 0) 72 ordz_seek_1_n |- !n c j. ordz_seek 1 n c j = 0 73 ordz_seek_m_0 |- !m c j. 0 < m ==> (ordz_seek m 0 c j = 0) 74 ordz_seek_m_1 |- !m c j. 1 < m /\ j < c ==> (ordz_seek m 1 c j = j) 75 ordz_seek_from_0 |- !m n c. 0 < m ==> (ordz_seek m n c 0 = 0) 76 ordz_seek_not_0 |- !m n c j. ordz_seek m n c j <> 0 ==> j < c 77 ordz_seek_exit |- !m n c j. 0 < m /\ j < c /\ (n ** j MOD m = 1) ==> 78 (ordz_seek m n c j = j) 79 ordz_seek_next |- !m n c j. 0 < m /\ j < c /\ n ** j MOD m <> 1 ==> 80 (ordz_seek m n c j = ordz_seek m n c (SUC j)) 81 ordz_seek_not_0_lower |- !m n c j. 0 < m /\ ordz_seek m n c j <> 0 ==> j <= ordz_seek m n c j 82 ordz_seek_when_next |- !m n c j. (ordz_seek m n c j = SUC j) ==> j < c 83 ordz_seek_when_found |- !m n c j. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j) ==> (n ** j MOD m = 1) 84 ordz_seek_found_imp_1 |- !m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 85 (n ** (j + u) MOD m = 1) 86 ordz_seek_found_imp_2 |- !m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 87 !v. v < u ==> n ** (j + v) MOD m <> 1 88 ordz_seek_found_imp |- !m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 89 (n ** (j + u) MOD m = 1) /\ 90 !v. v < u ==> n ** (j + v) MOD m <> 1 91 ordz_seek_from_1_nonzero|- !m n c. 0 < m /\ 0 < ordz_seek m n c 1 ==> (ordz_seek m n c 1 = ordz m n) 92 ordz_seek_eq_0_if |- !m n c j. 0 < m /\ 0 < j /\ (ordz_seek m n c j = 0) ==> 93 c <= j \/ !k. j <= k /\ k < c ==> n ** k MOD m <> 1 94 ordz_seek_eq_0_if_alt |- !m n c j. 0 < m /\ 0 < j /\ j < c /\ (ordz_seek m n c j = 0) ==> 95 !k. j <= k /\ k < c ==> n ** k MOD m <> 1 96 ordz_seek_eq_0_only_if |- !m n c j. 0 < m /\ 97 (c <= j \/ 0 < j /\ !k. j <= k /\ k < c ==> n ** k MOD m <> 1) ==> 98 (ordz_seek m n c j = 0) 99 ordz_seek_eq_order |- !m n c. 1 < m /\ m <= c ==> (ordz_seek m n c 1 = ordz m n) 100 ordz_seek_thm |- !m n. 1 < m ==> (ordz_seek m n m 1 = ordz m n) 101 102 ordz_compute_def |- !m n. ordz_compute m n = if m = 0 then ordz 0 n 103 else if m = 1 then 1 else ordz_seek m n m 1 104 ordz_compute_eqn |- !m n. ordz_compute m n = ordz m n 105 106 Order Computation -- with optimisation: 107 order_search_def |- !n m k c. order_search m n c k = 108 if c <= k then k 109 else if exp_mod_compute n k m = 1 then k 110 else order_search m n c (k + 1) 111 order_compute_def |- !m n. order_compute m n = 112 if n = 0 then ordz m 0 113 else if m = 0 then ordz m n 114 else if gcd_compute m n = 1 then order_search m (n MOD m) (phi_compute m) 1 115 else 0 116 order_search_alt |- !m n c k. order_search m n c k = 117 if c <= k then k 118 else if n ** k MOD m = 1 then k 119 else order_search m n c (k + 1) 120 order_compute_alt |- !m n. order_compute m n = 121 if n = 0 then ordz m 0 122 else if m = 0 then ordz m n 123 else if coprime m n then order_search m (n MOD m) (phi m) 1 124 else 0 125 order_search_id |- !m n c. order_search m n c c = c 126 order_search_over |- !m n c k. c <= k ==> (order_search m n c k = k) 127 order_search_success |- !m n c k. k < c /\ (n ** k MOD m = 1) ==> (order_search m n c k = k) 128 order_search_lower |- !m n c k. k <= order_search m n c k 129 order_search_upper |- !m n c k. order_search m n c k <= MAX k c 130 order_search_property |- !m n c k. k <= c /\ (n ** c MOD m = 1) ==> (n ** order_search m n c k MOD m = 1) 131 order_search_minimal |- !m n c k. k <= c ==> !j. k <= j /\ j < order_search m n c k ==> n ** j MOD m <> 1 132 order_compute_eqn |- !m n. order_compute m n = ordz m n 133 134 Efficient Order Computation: 135 ordz_search_def |- !n m k c. ordz_search m n c k = 136 if c <= k then k 137 else if k divides c /\ (exp_mod_compute n k m = 1) then k 138 else ordz_search m n c (k + 1) 139 ordz_fast_def |- !m n. ordz_fast m n = 140 if n = 0 then ordz m 0 141 else if m = 0 then ordz m n 142 else if gcd_compute m n = 1 then ordz_search m (n MOD m) (phi_compute m) 1 143 else 0 144 ordz_search_alt |- !m n c k. ordz_search m n c k = 145 if c <= k then k 146 else if k divides c /\ (n ** k MOD m = 1) then k 147 else ordz_search m n c (k + 1) 148 ordz_fast_alt |- !m n. ordz_fast m n = 149 if n = 0 then ordz m 0 150 else if m = 0 then ordz m n 151 else if coprime m n then ordz_search m (n MOD m) (phi m) 1 152 else 0 153 ordz_search_id |- !m n c. ordz_search m n c c = c 154 ordz_search_over |- !m n c k. c <= k ==> (ordz_search m n c k = k) 155 ordz_search_success |- !m n c k. k < c /\ k divides c /\ (n ** k MOD m = 1) ==> (ordz_search m n c k = k) 156 ordz_search_lower |- !m n c k. k <= ordz_search m n c k 157 ordz_search_upper |- !m n c k. ordz_search m n c k <= MAX k c 158 ordz_search_property |- !m n c k. k <= c /\ (n ** c MOD m = 1) ==> 159 ordz_search m n c k divides c /\ (n ** ordz_search m n c k MOD m = 1) 160 ordz_search_minimal |- !m n c k. k <= c ==> 161 !j. k <= j /\ j < ordz_search m n c k ==> ~(j divides c /\ (n ** j MOD m = 1)) 162 ordz_fast_eqn |- !m n. ordz_fast m n = ordz m n 163 164*) 165 166(* ------------------------------------------------------------------------- *) 167(* Helper Theorems *) 168(* ------------------------------------------------------------------------- *) 169 170(* ------------------------------------------------------------------------- *) 171(* Order Computation *) 172(* ------------------------------------------------------------------------- *) 173(* Pseudocode: 174Input: m, n, c, j. m = modulus, c = cutoff, j = initial value. 175Output: ordz m n, the least index j such that (n ** j = 1) (mod m) 176 177 if m = 0, return 0 // since (mod 0) is undefined 178 loop: 179 if j = m, return 0 // exit 180 if (n ** j) mod m = 1 return j // found j satisfying the condition 181 j <- j + 1 // increment j 182 goto loop // go back 183 184To compute the correct ordz m n, set initial j = 1. 185The cutoff c can be (phi m), 186and (phi m < m for 1 < m), or (phi m <= m for all m) by phi_le. 187 188This is the simpliest method to arrive at a least value for order. 189Other versions can optimise: 190* by including coprime tests, as only n coprime with m has nonzero order. 191* by including divisibility tests, as (ordz m n) must divide (phi m). 192 193This simple method is easy for complexity analysis. 194 195Note: ZN_order_mod_1 |- !n. ordz 1 n = 1 196Thus when m = 0, should return 1. 197However, this will make complexity analysis harder, 198and the criteria for ordz_seek m n c j = 1 later. 199Since there is a caller to ordz_seek, 200better have the caller to handle this discrepancy. 201This is given explicitly in ordz_seek_thm. 202*) 203 204(* Define the order seek loop *) 205(* 206val ordz_seek_def = tDefine "ordz_seek" ` 207 ordz_seek m n c j = 208 if (m = 0) \/ c <= j then 0 209 else if (n ** j) MOD m = 1 then j else ordz_seek m n c (SUC j) 210`(WF_REL_TAC `measure (\(m,n,c,j). c - j)`); 211*) 212(* Use of c <= j to simplify the checks for a total function. *) 213val ordz_seek_def = tDefine "ordz_seek" ` 214 ordz_seek m n c j = 215 if c <= j then 0 216 else if (n ** j) MOD m = 1 then j else ordz_seek m n c (SUC j) 217`(WF_REL_TAC `measure (\(m,n,c,j). c - j)`); 218(* Skip m = 0 as this is not critical to termination, and caller will pass m <> 0. *) 219 220(* 221setting cutoff c = m. 222EVAL ``ordz_seek 7 2 7 1``; = 3 <- ordz 7 2 = 3. 223EVAL ``ordz_seek 7 2 7 2``; = 3 <- j < result 224EVAL ``ordz_seek 7 2 7 3``; = 3 <- j = result. 225EVAL ``ordz_seek 7 2 7 4``; = 6 <- j too high, get multiple of 3. 226EVAL ``ordz_seek 7 2 7 5``; = 6 <- j too high, get multiple of 3. 227EVAL ``ordz_seek 7 2 7 6``; = 6 <- j too high, get multiple of 3. 228EVAL ``ordz_seek 7 2 7 7``; = 0 <- j = c. 229EVAL ``ordz_seek 7 10 7 1``; = 6 <- ordz 7 10 = 6. 230EVAL ``ordz_seek 7 10 6 1``; = 0 <- cutoff c too low, 231Need m <= c. 232The MOD tests are: j = 1, 2, ..., (c - 1), since j = c will exit without MOD test. 233When c = m, all j = 1 to (m - 1) are tested. If no MOD equal to 1, return 0. 234*) 235 236(* Theorem: ordz_seek m n c j = if c <= j then 0 237 else if (n ** j) MOD m = 1 then j else ordz_seek m n c (j + 1) *) 238(* Proof: by ordz_seek_def *) 239val ordz_seek_alt = store_thm( 240 "ordz_seek_alt", 241 ``!m n c j. ordz_seek m n c j = if c <= j then 0 242 else if (n ** j) MOD m = 1 then j else ordz_seek m n c (j + 1)``, 243 rw[Once ordz_seek_def, ADD1]); 244 245(* Theorem: c <= j ==> (ordz_seek m n c j = 0) *) 246(* Proof: by ordz_seek_def. *) 247val ordz_seek_over = store_thm( 248 "ordz_seek_over", 249 ``!m n c j. c <= j ==> (ordz_seek m n c j = 0)``, 250 rw[Once ordz_seek_def]); 251 252(* Theorem: ordz_seek 1 n c j = 0 *) 253(* Proof: 254 By induction on (c - j). 255 Base: !c j. (0 = c - j) ==> (ordz_seek 1 n c j = 0) 256 0 = c - j 257 ==> c <= j by integer arithmetic 258 ==> ordz_seek 1 n c j = 0 by ordz_seek_def 259 Step: !c j. (v = c - j) ==> (ordz_seek 1 n c j = 0) ==> 260 !c j. (SUC v = c - j) ==> (ordz_seek 1 n c j = 0) 261 SUC v = c - j means v = c - j - 1 = c - SUC j. 262 and 0 < c - j means ~(c <= j). 263 But n ** j MOD 1 = 0 by MOD_1 264 Thus ordz_seek 1 n c j 265 = ordz_seek 1 n c (SUC j) by ordz_seek_def, n ** j MOD 1 <> 1 266 = 0 by induction hypothesis 267*) 268val ordz_seek_1_n = store_thm( 269 "ordz_seek_1_n", 270 ``!n c j. ordz_seek 1 n c j = 0``, 271 rpt strip_tac >> 272 Induct_on `c - j` >- 273 rw[Once ordz_seek_def] >> 274 rw[Once ordz_seek_def]); 275 276(* Theorem: 0 < m ==> (ordz_seek m 0 c j = 0) *) 277(* Proof: 278 By induction on (c - j). 279 Base: !c j. (0 = c - j) ==> (ordz_seek m 0 c j = 0) 280 0 = c - j 281 ==> c <= j by integer arithmetic 282 ==> ordz_seek 1 n c j = 0 by ordz_seek_def 283 Step: !c j. (v = c - j) ==> (ordz_seek m 0 c j = 0) ==> 284 !c j. (SUC v = c - j) ==> (ordz_seek m 0 c j = 0) 285 SUC v = c - j means v = c - j - 1 = c - SUC j. 286 and 0 < c - j means ~(c <= j). 287 If m = 0, ordz_seek m 0 c j = 0 by ordz_seek_def 288 If m <> 0, 289 Note 0 ** j MOD m = 0 by ZERO_MOD, 0 < m 290 ordz_seek m 0 c j 291 = ordz_seek m 0 c (SUC j) by ordz_seek_def, n ** j MOD m <> 1 292 = 0 by induction hypothesis 293*) 294val ordz_seek_m_0 = store_thm( 295 "ordz_seek_m_0", 296 ``!m c j. 0 < m ==> (ordz_seek m 0 c j = 0)``, 297 rpt strip_tac >> 298 Induct_on `c - j` >- 299 rw[Once ordz_seek_def] >> 300 rw[Once ordz_seek_def] >> 301 metis_tac[ZERO_EXP, ZERO_MOD, ONE_NOT_ZERO]); 302 303(* Theorem: 1 < m /\ j < c ==> (ordz_seek m 1 c j = j) *) 304(* Proof: 305 Note j < c means ~(c <= j) by arithmetic 306 and 1 ** j MOD m 307 = 1 MOD m by EXP_1 308 = 1 by ONE_MOD, 1 < m 309 Thus ordz_seek m 1 c j = SUC (c - j) by ordz_seek_def 310*) 311val ordz_seek_m_1 = store_thm( 312 "ordz_seek_m_1", 313 ``!m c j. 1 < m /\ j < c ==> (ordz_seek m 1 c j = j)``, 314 rw[Once ordz_seek_def]); 315 316(* Theorem: 0 < m ==> (ordz_seek m n c 0 = 0) *) 317(* Proof: 318 If m = 1, ordz_seek m n c 0 = 0 by ordz_seek_1_n 319 Otherwise, 1 < m. 320 ordz_seek m n c 0 321 = if c <= 0 then 0 322 else if n ** 0 MOD m = 1 then 0 323 else ordz_seek m n c 1 by ordz_seek_def 324 Note n ** 0 MOD m 325 = 1 MOD m by EXP_0 326 = 1 by ONE_MOD, 1 < m 327 Thus ordz_seek m n c 0 = 0. 328*) 329val ordz_seek_from_0 = store_thm( 330 "ordz_seek_from_0", 331 ``!m n c. 0 < m ==> (ordz_seek m n c 0 = 0)``, 332 rpt strip_tac >> 333 (Cases_on `m = 1` >> simp[ordz_seek_1_n]) >> 334 `n ** 0 MOD m = 1` by rw[EXP_0, ONE_MOD] >> 335 rw[Once ordz_seek_def]); 336 337(* Theorem: ordz_seek m n c j <> 0 ==> j < c *) 338(* Proof: by ordz_seek_def *) 339val ordz_seek_not_0 = store_thm( 340 "ordz_seek_not_0", 341 ``!m n c j. ordz_seek m n c j <> 0 ==> j < c``, 342 rw[Once ordz_seek_def]); 343 344(* Theorem: 0 < m /\ j < c /\ (n ** j MOD m = 1) ==> (ordz_seek m n c j = j) *) 345(* Proof: by ordz_seek_def *) 346val ordz_seek_exit = store_thm( 347 "ordz_seek_exit", 348 ``!m n c j. 0 < m /\ j < c /\ (n ** j MOD m = 1) ==> (ordz_seek m n c j = j)``, 349 rw[Once ordz_seek_def]); 350 351(* Theorem: 0 < m /\ j < c /\ 352 (n ** j MOD m <> 1) ==> (ordz_seek m n c j = ordz_seek m n c (SUC j)) *) 353(* Proof: by ordz_seek_def *) 354val ordz_seek_next = store_thm( 355 "ordz_seek_next", 356 ``!m n c j. 0 < m /\ j < c /\ 357 (n ** j MOD m <> 1) ==> (ordz_seek m n c j = ordz_seek m n c (SUC j))``, 358 rw[Once ordz_seek_def]); 359 360(* Theorem: 0 < m /\ ordz_seek m n c j <> 0 ==> j <= ordz_seek m n c j *) 361(* Proof: 362 By induction on ordz_seek_def, to show: 363 ordz_seek m n c j <> 0 ==> j <= ordz_seek m n c j 364 Note ordz_seek m n c j <> 0 by given 365 ==> 0 < j by ordz_seek_not_0 366 If n ** j MOD m = 1, 367 Then ordz_seek m n c j = j by ordz_seek_exit, 0 < m 368 If n ** j MOD m <> 1, 369 Then ordz_seek m n c j 370 = ordz_seek m n c (SUC j) by ordz_seek_next 371 >= SUC j by induction hypothesis 372 >= j by arithmetic 373*) 374val ordz_seek_not_0_lower = store_thm( 375 "ordz_seek_not_0_lower", 376 ``!m n c j. 0 < m /\ ordz_seek m n c j <> 0 ==> j <= ordz_seek m n c j``, 377 ho_match_mp_tac (theorem "ordz_seek_ind") >> 378 rw[] >> 379 imp_res_tac ordz_seek_not_0 >> 380 Cases_on `n ** j MOD m = 1` >- 381 rw[ordz_seek_exit] >> 382 `ordz_seek m n c j = ordz_seek m n c (SUC j)` by rw[GSYM ordz_seek_next] >> 383 decide_tac); 384 385(* Theorem: (ordz_seek m n c j = SUC j) ==> j < c *) 386(* Proof: 387 Note ordz_seek m n c j <> 0 by 0 < SUC j 388 ==> j < c by ordz_seek_not_0 389*) 390val ordz_seek_when_next = store_thm( 391 "ordz_seek_when_next", 392 ``!m n c j. (ordz_seek m n c j = SUC j) ==> j < c``, 393 rpt strip_tac >> 394 `ordz_seek m n c j <> 0` by fs[] >> 395 imp_res_tac ordz_seek_not_0); 396 397(* Theorem: 0 < m /\ 0 < j /\ (ordz_seek m n c j = j) ==> (n ** j MOD m = 1) *) 398(* Proof: 399 By contradiction, suppose n ** j MOD m <> 1. 400 Note ordz_seek m n c j <> 0 by ordz_seek m n c j = j, 0 < j 401 Thus 0 < j by ordz_seek_not_0 402 ==> ordz_seek m n c j = ordz_seek m n c (SUC j) by ordz_seek_next, n ** j MOD m <> 1 403 But SUC j <= ordz_seek m n c (SUC j) by ordz_seek_not_0_lower 404 ==> SUC j <= j by ordz_seek m n c j = j 405 This contradicts j < SUC j by LESS_SUC 406*) 407val ordz_seek_when_found = store_thm( 408 "ordz_seek_when_found", 409 ``!m n c j. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j) ==> (n ** j MOD m = 1)``, 410 spose_not_then strip_assume_tac >> 411 `ordz_seek m n c j <> 0` by fs[] >> 412 imp_res_tac ordz_seek_not_0 >> 413 `ordz_seek m n c j = ordz_seek m n c (SUC j)` by rw[GSYM ordz_seek_next] >> 414 `SUC j <= ordz_seek m n c (SUC j)` by rw[ordz_seek_not_0_lower] >> 415 decide_tac); 416 417(* This is a special case of the next theorem when u = 0. *) 418 419(* Theorem: 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 420 (n ** (j + u) MOD m = 1) *) 421(* Proof: 422 By induction from ordz_seek_def, to show: 423 0 < j /\ ordz_seek m n c j = j + u ==> n ** (j + u) MOD m = 1 424 Note ordz_seek m n c j <> 0 by 0 < j 425 ==> j < c by ordz_seek_not_0 426 If n ** j MOD m = 1, 427 Then ordz_seek m n c j = j by ordz_seek_exit 428 ==> j + u = j by ordz_seek m n c j = j + u 429 or u = 0 by arithmetic 430 n ** (j + u) MOD m 431 = n ** j MOD m by ADD_0 432 = 1 by this case. 433 If n ** j MOD m <> 1, 434 Then ordz_seek m n c j 435 = ordz_seek m n c (SUC j) by ordz_seek_next 436 Note u <> 1 by ordz_seek_when_found, ADD_0 437 Let v = u - 1. 438 Then v + SUC j = j + u by arithmetic 439 n ** (j + u) MOD m 440 = n ** (v + SUC j) MOD m by above 441 = 1 by induction hypothesis 442*) 443val ordz_seek_found_imp_1 = store_thm( 444 "ordz_seek_found_imp_1", 445 ``!m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> (n ** (j + u) MOD m = 1)``, 446 ho_match_mp_tac (theorem "ordz_seek_ind") >> 447 rw[] >> 448 `ordz_seek m n c j <> 0` by decide_tac >> 449 imp_res_tac ordz_seek_not_0 >> 450 Cases_on `n ** j MOD m = 1` >| [ 451 `ordz_seek m n c j = j` by rw[GSYM ordz_seek_exit] >> 452 `u = 0` by decide_tac >> 453 simp[], 454 `ordz_seek m n c j = ordz_seek m n c (SUC j)` by rw[GSYM ordz_seek_next] >> 455 `u <> 0` by metis_tac[ordz_seek_when_found, ADD_0] >> 456 qabbrev_tac `v = u - 1` >> 457 `v + SUC j = j + u` by rw[Abbr`v`] >> 458 metis_tac[NOT_ZERO, NOT_LESS] 459 ]); 460 461(* Theorem: 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 462 !v. v < u ==> n ** (j + v) MOD m <> 1 *) 463(* Proof: 464 By induction from ordz_seek_def, to show: 465 0 < j /\ ordz_seek m n c j = j + u /\ v < u ==> n ** (j + v) MOD m <> 1 466 By contradiction, suppose n ** (j + v) MOD m = 1. 467 Note ordz_seek m n c j <> 0 by ordz_seek m n c j = j + u, 0 < j 468 ==> j < c by ordz_seek_not_0 469 Note u <> 0 by v < u 470 471 If n ** j MOD m = 1, 472 Then ordz_seek m n c j = j by ordz_seek_exit 473 or j + u = j by ordz_seek m n c j = j + u 474 or u = 0, contradicts u <> 0 by ADD_0 475 476 If n ** j MOD m <> 1, 477 Then ordz_seek m n c j 478 = ordz_seek m n c (SUC j) by ordz_seek_next 479 Note v <> 0 by n ** (j + v) MOD m = 1, ADD_0 480 Let k = u - 1, h = v - 1. 481 Then h < k /\ SUC j + k = j + u /\ SUC j + h = j + v 482 by arithmetic 483 ==> n ** (j + v) MOD m <> 1 by induction hypothesis 484 This contradicts n ** (j + v) MOD m = 1. 485*) 486val ordz_seek_found_imp_2 = store_thm( 487 "ordz_seek_found_imp_2", 488 ``!m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 489 !v. v < u ==> n ** (j + v) MOD m <> 1``, 490 ho_match_mp_tac (theorem "ordz_seek_ind") >> 491 spose_not_then strip_assume_tac >> 492 `ordz_seek m n c j <> 0` by decide_tac >> 493 imp_res_tac ordz_seek_not_0 >> 494 `u <> 0` by decide_tac >> 495 Cases_on `n ** j MOD m = 1` >| [ 496 `ordz_seek m n c j = j` by rw[GSYM ordz_seek_exit] >> 497 decide_tac, 498 `ordz_seek m n c j = ordz_seek m n c (SUC j)` by rw[GSYM ordz_seek_next] >> 499 `v <> 0` by metis_tac[ADD_0] >> 500 qabbrev_tac `k = u - 1` >> 501 qabbrev_tac `h = v - 1` >> 502 `j + u = SUC j + k` by rw[Abbr`k`] >> 503 `j + v = SUC j + h` by rw[Abbr`h`] >> 504 `h < k` by rw[Abbr`h`, Abbr`k`] >> 505 `0 < SUC j` by decide_tac >> 506 metis_tac[NOT_ZERO, NOT_LESS] 507 ]); 508 509(* Combine to form a major result *) 510 511(* Theorem: 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 512 ((n ** (j + u) MOD m = 1) /\ !v. v < u ==> n ** (j + v) MOD m <> 1) *) 513(* Proof: by ordz_seek_found_imp_1, ordz_seek_found_imp_2 *) 514val ordz_seek_found_imp = store_thm( 515 "ordz_seek_found_imp", 516 ``!m n c j u. 0 < m /\ 0 < j /\ (ordz_seek m n c j = j + u) ==> 517 ((n ** (j + u) MOD m = 1) /\ !v. v < u ==> n ** (j + v) MOD m <> 1)``, 518 metis_tac[ordz_seek_found_imp_1, ordz_seek_found_imp_2]); 519 520(* Theorem: 0 < m /\ 0 < ordz_seek m n c 1 ==> (ordz_seek m n c 1 = ordz m n) *) 521(* Proof: 522 Let k = ordz_seek m n c 1. 523 Then k <> 0, so ?u. k = 1 + u by num_CASES 524 Thus n ** k MOD m = 1 /\ 525 !v. v < u ==> n ** (1 + v) MOD m <> 1 by ordz_seek_found_imp, putting j = 1. 526 This is the same as: 527 !j. 0 < j /\ j < k ==> n ** j MOD m <> 1 by index shifting 528 Also 1 < m by ordz_seek_1_n, k <> 0 529 Thus k = ordz m n by ZN_order_test_1 530*) 531val ordz_seek_from_1_nonzero = store_thm( 532 "ordz_seek_from_1_nonzero", 533 ``!m n c. 0 < m /\ 0 < ordz_seek m n c 1 ==> (ordz_seek m n c 1 = ordz m n)``, 534 rpt strip_tac >> 535 qabbrev_tac `k = ordz_seek m n c 1` >> 536 `k <> 0 /\ 0 < 1` by decide_tac >> 537 `?u. k = 1 + u` by metis_tac[num_CASES, SUC_ONE_ADD] >> 538 `(n ** k MOD m = 1) /\ !v. v < u ==> n ** (1 + v) MOD m <> 1` by metis_tac[ordz_seek_found_imp] >> 539 `!j. 0 < j /\ j < k ==> n ** j MOD m <> 1` by 540 (rpt strip_tac >> 541 `?v. j = 1 + v` by metis_tac[num_CASES, SUC_ONE_ADD, NOT_ZERO] >> 542 `v < u` by decide_tac >> 543 metis_tac[]) >> 544 `m <> 1` by metis_tac[ordz_seek_1_n] >> 545 rw[ZN_order_test_1]); 546 547(* Theorem: 0 < m /\ 0 < j /\ (ordz_seek m n c j = 0) ==> 548 (c <= j \/ (!k. j <= k /\ k < c ==> (n ** k) MOD m <> 1)) *) 549(* Proof: 550 Idea: 551 The induction is based on the range [j ..< c]. 552 Note ordz_seek m n c j = 0 by given 553 ordz_seek m n c c = 0 by definition 554 By contradiction, there is a k in the range [j ..< c] 555 such that (n ** k) MOD m = 1. 556 557 If SUC j = c, the smallest range, 558 Then k = j, as k is now squeezed between [j ..< SUC j]. 559 Then k < c by j < c 560 and (n ** k) MOD m = 1 by contradiction 561 ==> ordz_seek m n c k = k by ordz_seek_exit 562 or ordz_seek m n c j = j by k = j 563 This contradicts 564 ordz_seek m n c j = 0 by 0 < j 565 566 Otherwise, SUC j < c by j < c means SUC j <= c, noew SUC j <> c. 567 Then !k. SUC j <= k /\ k < c ==> n ** k MOD m <> 1 568 by induction hypothesis 569 Note j <= k means j = k \/ j < k by k in [j ..< c] 570 If j = k, we have the same contradiction as before: 571 Since (n ** k) MOD m = 1 572 gives (n ** j) MOD m = 1 573 thus ordz_seek m n c j = j by ordz_seek_exit 574 This contradicts 575 ordz_seek m n c j = 0 by 0 < j 576 If j < k, this is the same as SUC j <= k. 577 Thus the induction implication applies, 578 giving n ** k MOD m <> 1 579 This contradicts n ** k MOD m = 1. 580 581 By induction from ordz_seek_def, to show: 582 j < c /\ n ** j MOD m <> 1 ==> 583 (ordz_seek m n c (SUC j) = 0) ==> 584 c <= SUC j \/ !k. SUC j <= k /\ k < c ==> n ** k MOD m <> 1 585 Note 0 < j /\ j < c /\ ordz_seek m n c j = 0 586 ==> n ** j MOD m <> 1 by ordz_seek_exit 587 588 By contradiction, suppose the opposite: 589 ordz_seek m n c (SUC j) = 0 /\ SUC j < c /\ 590 ?k. SUC j <= k /\ k < c ==> n ** k MOD m <> 1 591 Thus k <> j, as n ** k MOD m = 1 by contradiction 592 Note j < c means SUC j <= c. 593 But SUC j <> c, as that will squeeze k = j, which contradicts k <> j. 594 Thus SUC j < c. 595 Also j <= k /\ k <> j means j < k, tus SUC j <= k. 596 With k < c, this leads to n ** k MOD <> 1, a contradiction. 597*) 598val ordz_seek_eq_0_if = store_thm( 599 "ordz_seek_eq_0_if", 600 ``!m n c j. 0 < m /\ 0 < j /\ (ordz_seek m n c j = 0) ==> 601 (c <= j \/ (!k. j <= k /\ k < c ==> (n ** k) MOD m <> 1))``, 602 ho_match_mp_tac (theorem "ordz_seek_ind") >> 603 spose_not_then strip_assume_tac >> 604 `j < c /\ j <> 0 /\ 0 < SUC j` by decide_tac >> 605 `n ** j MOD m <> 1` by metis_tac[ordz_seek_exit] >> 606 `ordz_seek m n c (SUC j) = 0` by rw[GSYM ordz_seek_next] >> 607 `k <> j` by metis_tac[] >> 608 first_x_assum (drule_all_then strip_assume_tac) >- 609 decide_tac >> 610 `SUC j <= k` by decide_tac >> 611 metis_tac[]); 612 613(* An alternative expression of the same theorem. *) 614 615(* Theorem: 0 < m /\ 0 < j /\ j < c /\ (ordz_seek m n c j = 0) ==> 616 !k. j <= k /\ k < c ==> (n ** k) MOD m <> 1 *) 617(* Proof: by ordz_seek_eq_0_if. *) 618val ordz_seek_eq_0_if_alt = store_thm( 619 "ordz_seek_eq_0_if_alt", 620 ``!m n c j. 0 < m /\ 0 < j /\ j < c /\ (ordz_seek m n c j = 0) ==> 621 !k. j <= k /\ k < c ==> (n ** k) MOD m <> 1``, 622 metis_tac[ordz_seek_eq_0_if, NOT_LESS]); 623 624(* Theorem: 0 < m /\ 625 (c <= j \/ (0 < j /\ !k. j <= k /\ k < c ==> (n ** k) MOD m <> 1)) ==> 626 (ordz_seek m n c j = 0) *) 627(* Proof: 628 By induction from ordz_seek_def, to show: 629 (1) c <= j ==> ordz_seek m n c j = 0, true by ordz_seek_def, c <= j 630 (2) 0 < j /\ !k. j <= k /\ k < c ==> n ** k MOD m <> 1 ==> ordz_seek m n c j = 0 631 By contradiction, suppose ordz_seek m n c j <> 0. 632 Then m <> 0 /\ j <> 0 by ordz_seek_not_0 633 If n ** j MOD m = 1, 634 Note j <= j by arithmetic 635 ==> n ** j MOD m <> 1 by !k implication 636 This contradicts n ** j MOD m = 1 by this case. 637 If n ** j MOD m <> 1, 638 Then ordz_seek m n c j 639 = ordz_seek m n c (SUC j) by ordz_seek_next 640 But j < c means SUC j <= c, or ~(c < SUC j) 641 ==> ordz_seek m n c (SUC j) = 0 by induction hypothesis 642 This contradicts ordz_seek m n c j <> 0. 643*) 644val ordz_seek_eq_0_only_if = store_thm( 645 "ordz_seek_eq_0_only_if", 646 ``!m n c j. 0 < m /\ 647 (c <= j \/ (0 < j /\ !k. j <= k /\ k < c ==> (n ** k) MOD m <> 1)) ==> 648 (ordz_seek m n c j = 0)``, 649 ho_match_mp_tac (theorem "ordz_seek_ind") >> 650 spose_not_then strip_assume_tac >- 651 fs[Once ordz_seek_def] >> 652 imp_res_tac ordz_seek_not_0 >> 653 Cases_on `n ** j MOD m = 1` >- 654 metis_tac[LESS_EQ_REFL] >> 655 `ordz_seek m n c j = ordz_seek m n c (SUC j)` by rw[ordz_seek_next] >> 656 `~(c <= SUC j)` by decide_tac >> 657 `ordz_seek m n c (SUC j) = 0` by fs[] >> 658 decide_tac); 659 660(* Theorem: 1 < m /\ m <= c ==> (ordz_seek m n c 1 = ordz m n) *) 661(* Proof: 662 If ordz_seek m n c 1 = 0, 663 Note 0 < 1 /\ 1 < c by 1 < m, m <= c 664 Then !k. 0 < k /\ k < c ==> n ** k MOD m <> 1 665 by ordz_seek_eq_0_if_alt, put j = 1 666 Thus ordz m n = 0 by ZN_order_eq_0_test, 1 < m 667 If ordz_seek m n c 1 <> 0, 668 Then ordz_seek m n c 1 = ordz m n by ordz_seek_from_1_nonzero 669*) 670val ordz_seek_eq_order = store_thm( 671 "ordz_seek_eq_order", 672 ``!m n c. 1 < m /\ m <= c ==> (ordz_seek m n c 1 = ordz m n)``, 673 rpt strip_tac >> 674 Cases_on `ordz_seek m n c 1 = 0` >| [ 675 `0 < m /\ 0 < 1 /\ 1 < c` by decide_tac >> 676 `!k. 1 <= k <=> 0 < k` by decide_tac >> 677 `!k. 0 < k /\ k < c ==> n ** k MOD m <> 1` by metis_tac[ordz_seek_eq_0_if_alt] >> 678 rw[ZN_order_eq_0_test], 679 rw[ordz_seek_from_1_nonzero] 680 ]); 681 682(* Theorem: 1 < m ==> (ordz_seek m n m 1 = ordz m n) *) 683(* Proof: by ordz_seek_eq_order, c = m <= m. *) 684val ordz_seek_thm = store_thm( 685 "ordz_seek_thm", 686 ``!m n. 1 < m ==> (ordz_seek m n m 1 = ordz m n)``, 687 rw[ordz_seek_eq_order]); 688 689(* Compute ordz m n, the simplest way *) 690val ordz_compute_def = Define` 691 ordz_compute m n = 692 if m = 0 then ordz 0 n (* MOD 0 is undefined *) 693 else if m = 1 then 1 (* ordz 1 n = 1 by ZN_order_mod_1 *) 694 else ordz_seek m n m 1 695 (* just the least k from 1 such that n ** k MOD m = 1 when 1 < m *) 696 (* if n = 0, ordz m 0 = 0 by ZN_order_0, and ordz_seek m 0 c j = 0 by ordz_seek_m_0 *) 697`; 698 699(* Examples: 700> EVAL ``ordz_compute 2 10``; = 0 1/2 = 0.5 terminating. 701> EVAL ``ordz_compute 3 10``; = 1 1/3 = 0.3333 with period 1. 702> EVAL ``ordz_compute 4 10``; = 0 1/4 = 0.25 terminating 703> EVAL ``ordz_compute 5 10``; = 0 1/5 = 0.2 terminating 704> EVAL ``ordz_compute 6 10``; = 0 1/6 = 0.16666 ... mixed, gcd (6, 10) = 2. 705> EVAL ``ordz_compute 7 10``; = 6 1/7 = 0.142857.... with period 6. 706> EVAL ``ordz_compute 8 10``; = 0 1/8 = 0.125 terminating 707> EVAL ``ordz_compute 9 10``; = 1 1/9 = 0.1111 ... with period 1. 708> EVAL ``ordz_compute 10 10``; = 0 1/10 = 0.1 terminating 709> EVAL ``ordz_compute 11 10``; = 2 1/11 = 0.0909 ... with period 2. 710> EVAL ``ordz_compute 12 10``; = 0 1/12 = 0.0833 ... mixed, gcd (12,10) = 2 711> EVAL ``ordz_compute 13 10``; = 6 1/13 = 0.076923076923 ... with period 6. 712> EVAL ``ordz_compute 17 10``; = 16 1/17 = 0.0588235294117647 ... with period 16. 713*) 714 715(* Theorem: ordz_compute m n = ordz m n *) 716(* Proof: 717 If m = 0, both are equal by ordz_compute_def 718 If m = 1, 719 LHS = ordz_compute 1 n = 1 by ordz_compute_def 720 RHS = ordz 1 n = 1 by ZN_order_mod_1 721 hence they are equal. 722 Otherwise, 1 < m. 723 ordz_compute m n 724 = ordz_seek m n m 1 by ordz_compute_def 725 = ordz m n by ordz_seek_eq_order, 1 < m 726*) 727val ordz_compute_eqn = store_thm( 728 "ordz_compute_eqn", 729 ``!m n. ordz_compute m n = ordz m n``, 730 rw[ordz_compute_def, ZN_order_mod_1, ordz_seek_eq_order]); 731 732(* ------------------------------------------------------------------------- *) 733(* Order Computation -- with optimisation *) 734(* ------------------------------------------------------------------------- *) 735(* Pseudocode: 736 737Input: m, n with 1 < m, 0 < n 738Output: ordz m n, the least index j such that (n ** j = 1) (mod m) 739 740if ~(coprime m n) return 0 // initial check 741// For coprime m n, ordz m (n MOD m) is a divisor of (phi m) by Euler-Fermat Theorem. 742// Search upwards for least index j 743j <- 1 // initial index 744c <- phi m // recompute constant 745n <- n MOD m // reduce n, by ordz m n = ordz m (n MOD m) 746while (j <= c) { 747 if (n ** j = 1 (mod m)) return j // test j 748 j <- j + 1 // increment j 749} 750return 0 // unreachable, unless no initial coprime check. 751 752*) 753 754(* A method to compute ordz m n: 755Step 1: if (gcd m n <> 1) then 0 756Step 2: Just search from j = 1 to (phi m), 757 If exp_mod_compute n j m = 1, return j. 758 Search is upwards for the first (least) index j. 759*) 760 761(* Question: How to show the number of steps is bounded? *) 762 763(* Formulate a recursive search for the least index, not using WHILE loop. *) 764val order_search_def = tDefine "order_search" ` 765 order_search m n c k = 766 (* search is from k to maximum c *) 767 if c <= k then k (* when k reaches c, k = c, must divide c, and exp_mod_compute n c m = 1 always. *) 768 else if exp_mod_compute n k m = 1 then k (* that is, found k such that (n ** k) MOD m = 1 *) 769 else order_search m n c (k + 1) (* current k is not suitable, try k + 1 instead. *) 770` (WF_REL_TAC `measure (\(m,n,c,k). c - k)`); 771(* 772val order_search_def = |- !n m k c. order_search m n c k = 773 if c <= k then k 774 else if exp_mod_compute n k m = 1 then k 775 else order_search m n c (k + 1): thm 776*) 777 778(* Compute ordz m n *) 779val order_compute_def = Define` 780 order_compute m n = 781 if n = 0 then ordz m 0 (* order is defined for nonzero only *) 782 else if m = 0 then ordz m n (* MOD 0 is undefined *) 783 else if (gcd_compute m n = 1) (* For coprimes, search from 1 ... *) 784 then order_search m (n MOD m) (phi_compute m) 1 (* ordz m n = ordz m (n MOD m), divisor of phi m *) 785 else 0 (* not coprime: order is 0 *) 786`; 787 788(* Examples: 789> EVAL ``order_compute 10 3``; --> 4 790> EVAL ``order_compute 10 4``; --> 0 791> EVAL ``order_compute 10 7``; --> 4 792> EVAL ``order_compute 10 19``; --> 2 793> EVAL ``order_compute 10 1``; --> 1 794 795> EVAL ``phi_compute 10``; --> 4 796 797Indeed, (ordz m n) is a divisor of (phi m). 798Since phi(10) = 4, ordz 10 n is a divisior of 4. 799 800> EVAL ``order_compute 1 2``; --> 1 801> EVAL ``order_compute 1 3``; --> 1 802 803*) 804 805(* Theorem: order_search m n c k = if c <= k then k 806 else if (n ** k) MOD m = 1 then k else order_search m n c (k + 1) *) 807(* Proof: by order_search_def, exp_mod_compute_eqn *) 808val order_search_alt = store_thm( 809 "order_search_alt", 810 ``!m n c k. order_search m n c k = if c <= k then k 811 else if (n ** k) MOD m = 1 then k else order_search m n c (k + 1)``, 812 rw[Once order_search_def, exp_mod_compute_eqn]); 813 814(* Theorem: order_compute m n = if n = 0 then ordz m 0 815 else if m = 0 then ordz m n 816 else if coprime m n then order_search m (n MOD m) (phi m) 1 else 0 *) 817(* Proof: by order_compute_def, gcd_compute_eqn, phi_compute_eqn *) 818val order_compute_alt = store_thm( 819 "order_compute_alt", 820 ``!m n. order_compute m n = 821 if n = 0 then ordz m 0 822 else if m = 0 then ordz m n 823 else if coprime m n then order_search m (n MOD m) (phi m) 1 else 0``, 824 rw[order_compute_def, gcd_compute_eqn, phi_compute_eqn]); 825 826(* Theorem: order_search m n c c = c *) 827(* Proof: order_search_def *) 828val order_search_id = store_thm( 829 "order_search_id", 830 ``!m n c. order_search m n c c = c``, 831 rw[Once order_search_def]); 832 833(* Theorem: c <= k ==> (order_search m n c k = k) *) 834(* Proof: order_search_def *) 835val order_search_over = store_thm( 836 "order_search_over", 837 ``!m n c k. c <= k ==> (order_search m n c k = k)``, 838 rw[Once order_search_def]); 839 840(* Theorem: k < c /\ ((n ** k) MOD m = 1) ==> (order_search m n c k = k) *) 841(* Proof: by order_search_alt *) 842val order_search_success = store_thm( 843 "order_search_success", 844 ``!m n c k. k < c /\ ((n ** k) MOD m = 1) ==> (order_search m n c k = k)``, 845 rw[Once order_search_alt]); 846 847(* Theorem: k <= order_search m n c k *) 848(* Proof: 849 By induction on (c - k). 850 Base: (0 = c - k) ==> k <= order_search m n c k 851 Note 0 = c - k means c <= k, 852 or c <= k by SUB_EQ_0 853 order_search m n c k 854 = k by order_search_alt, ~(k < c) 855 >= k by LESS_OR_EQ 856 Step: !c k. (v = c - k) ==> k <= order_search m n c k ==> 857 (SUC v = c - k) ==> k <= order_search m n c k 858 Note SUC v = c - k means k < c by SUC_POS 859 or v + 1 = c - k, or 860 v = c - (k + 1) by arithmetic 861 If n ** k MOD m = 1, 862 order_search m n c k 863 = k by order_search_alt, k < c 864 >= k by LESS_OR_EQ 865 If n ** k MOD m <> 1, 866 order_search m n c k 867 = order_search m n c (k + 1) by order_search_alt, k < c 868 >= k + 1 by induction hypothesis 869 >= k by arithmetic 870*) 871val order_search_lower = store_thm( 872 "order_search_lower", 873 ``!m n c k. k <= order_search m n c k``, 874 rpt strip_tac >> 875 Induct_on `c - k` >| [ 876 rpt strip_tac >> 877 rw[Once order_search_alt], 878 rpt strip_tac >> 879 `v = c - (k + 1)` by decide_tac >> 880 rw[Once order_search_alt] >> 881 metis_tac[LESS_EQ_TRANS, DECIDE``k <= k + 1``] 882 ]); 883 884(* Theorem: order_search m n c k <= MAX k c *) 885(* Proof: 886 By induction on (c - k). 887 Base: (0 = c - k) ==> order_search m n c k <= MAX k c 888 Note 0 = c - k means c <= k, 889 or c <= k by SUB_EQ_0 890 order_search m n c k 891 = k by order_search_alt, ~(k < c) 892 = MAX k c by c <= k 893 <= MAX k c by LESS_OR_EQ 894 Step: !c k. (v = c - k) ==> order_search m n c k <= MAX k c ==> 895 (SUC v = c - k) ==> order_search m n c k <= MAX k c 896 Note SUC v = c - k means k < c by SUC_POS 897 or v + 1 = c - k, or 898 v = c - (k + 1) by arithmetic 899 If n ** k MOD m = 1, 900 order_search m n c k 901 = k by order_search_alt, k < c 902 <= c by LESS_OR_EQ 903 If n ** k MOD m <> 1, 904 order_search m n c k 905 = order_search m n c (k + 1) by order_search_alt, k < c 906 <= MAX (k + 1) c by induction hypothesis 907 <= MAX k c by k < c ==> (k + 1) <= c 908 Indeed, MAX (k + 1) c = c = MAX k c by MAX_DEF 909*) 910val order_search_upper = store_thm( 911 "order_search_upper", 912 ``!m n c k. order_search m n c k <= MAX k c``, 913 rpt strip_tac >> 914 Induct_on `c - k` >| [ 915 rpt strip_tac >> 916 rw[Once order_search_alt], 917 rpt strip_tac >> 918 `v = c - (k + 1)` by decide_tac >> 919 `k <= MAX k c` by rw[] >> 920 rw_tac bool_ss[Once order_search_alt] >> 921 `MAX (k + 1) c = MAX k c` by rw[MAX_DEF] >> 922 metis_tac[] 923 ]); 924 925(* Theorem: k <= c /\ ((n ** c) MOD m = 1) ==> (n ** (order_search m n c k) MOD m = 1) *) 926(* Proof: 927 By induction on (c - k). 928 Base: (0 = c - k) ==> (n ** (order_search m n c k) MOD m = 1) 929 Let t = order_search m n c k. 930 Note 0 = c - k means c <= k by SUB_EQ_0 931 Thus k = c by c <= k, k <= c 932 ==> t = c by order_search_id 933 or n ** t MOD m = 1 by (n ** c) MOD m = 1 934 Step: !c k. (v = c - k) /\ k < c ==> (n ** (order_search m n c k) MOD m = 1) 935 ==> SUC v = c - k ==> (n ** (order_search m n c k) MOD m = 1) 936 Let t = order_search m n c k. 937 If n ** k MOD m = 1, 938 Then t = k by order_search_alt, k < c 939 so n ** t MOD m = 1 by n ** k MOD m = 1 (if condition) 940 If n ** k MOD m <> 1, 941 Then t = order_search m n c (k + 1) by order_search_alt, k < c 942 Note SUC v = c - k means k < c by SUC_POS 943 or v + 1 = c - k, or 944 v = c - (k + 1) by arithmetic 945 Also k + 1 <= c by k < c 946 If c = k + 1, 947 Then t = order_search m n c c 948 = c by order_search_id 949 so n ** t MOD m = 1 by n ** c MOD m = 1 (given) 950 If c <> k + 1, 951 Then k + 1 < c by k < c 952 ==> n ** t MOD m = 1 by induction hypothesis, k + 1 < c 953*) 954val order_search_property = store_thm( 955 "order_search_property", 956 ``!m n c k. k <= c /\ ((n ** c) MOD m = 1) ==> (n ** (order_search m n c k) MOD m = 1)``, 957 rpt strip_tac >> 958 Induct_on `c - k` >| [ 959 rpt strip_tac >> 960 `k = c` by decide_tac >> 961 rw[order_search_id], 962 rpt strip_tac >> 963 Cases_on `n ** k MOD m = 1` >- 964 rw[order_search_success] >> 965 `order_search m n c k = order_search m n c (k + 1)` by rw[Once order_search_alt] >> 966 `k + 1 <= c /\ (v = c - (k + 1))` by decide_tac >> 967 Cases_on `c = k + 1` >- 968 rw[order_search_id] >> 969 rw[] 970 ]); 971 972(* Theorem: k <= c ==> !j. k <= j /\ j < order_search m n c k ==> n ** j MOD m <> 1 *) 973(* Proof: 974 By contradiction, suppose some j with (n ** j MOD m = 1). 975 Let t = order_search m n c k. 976 If k = c, 977 Then t = k by order_search_id 978 But j < t = k by j < order_search m n c k (given) 979 This contradicts k <= j. 980 If k <> c, 981 Then k < c by k <= c, k <> c. 982 Use induction on (j - k). 983 Base: 0 = j - k /\ k <= j ==> F 984 Note 0 = j - k means j <= k. 985 Thus j = k by j <= k, k <= j. 986 so order_search m n c k = k by order_search_success, k < c, n ** j MOD m = 1 987 But j < order_search m n c k, 988 or j < j, which is false by LESS_REFL 989 Step: !j k. (v = j - k) /\ k < c /\ k <= j /\ j < order_search m n c k ==> F ==> 990 SUC v = j - k /\ k < c /\ k <= j /\ j < order_search m n c k ==> F 991 Note j < t by j < order_search m n c k 992 If n ** k MOD m = 1, 993 Then t = k by order_search_alt, k < c 994 Thus j < t = k by j < order_search m n c k 995 This contradicts k <= j. 996 If n ** k MOD m <> 1, 997 Then t = order_search m n c (k + 1) by order_search_alt, k < c [1] 998 Note t <= c by order_search_upper, MAX_DEF, k < c. 999 so j < c by LESS_LESS_EQ_TRANS 1000 ==> order_search m n c j = j by order_search_success, j < c [2] 1001 1002 Note SUC v = j - k means k < j by SUC_POS 1003 or v + 1 = j - k, or 1004 v = j - (k + 1) by arithmetic 1005 Also k + 1 <= j by k < j 1006 If j = k + 1, 1007 Then t = order_search m n c j by [1], j = k + 1 1008 = j by [2] 1009 or j < j, which is false by LESS_REFL, j < t. 1010 If j <> k + 1, 1011 Then k + 1 < j by k < j 1012 or k + 1 < c by j < c 1013 Thus giving F by induction hypothesis 1014*) 1015val order_search_minimal = store_thm( 1016 "order_search_minimal", 1017 ``!m n c k. k <= c ==> !j. k <= j /\ j < order_search m n c k ==> n ** j MOD m <> 1``, 1018 rpt strip_tac >> 1019 Cases_on `k = c` >| [ 1020 `order_search m n c k = k` by rw[order_search_id] >> 1021 decide_tac, 1022 `k < c` by decide_tac >> 1023 fs[] >> 1024 Induct_on `j - k` >| [ 1025 rpt strip_tac >> 1026 `j = k` by decide_tac >> 1027 metis_tac[order_search_success, DECIDE``~(n < n)``], 1028 rpt strip_tac >> 1029 Cases_on `n ** k MOD m = 1` >| [ 1030 `order_search m n c k = k` by rw[order_search_success] >> 1031 decide_tac, 1032 `j < c` by metis_tac[order_search_upper, MAX_DEF, LESS_LESS_EQ_TRANS] >> 1033 `order_search m n c j = j` by rw[order_search_success] >> 1034 `order_search m n c k = order_search m n c (k + 1)` by rw[Once order_search_alt] >> 1035 `k + 1 <= j /\ (v = j - (k + 1))` by decide_tac >> 1036 Cases_on `j = k + 1` >- 1037 metis_tac[DECIDE``~(n < n)``] >> 1038 `k + 1 < c` by decide_tac >> 1039 metis_tac[] 1040 ] 1041 ] 1042 ]); 1043 1044(* Theorem: order_compute m n = ordz m n *) 1045(* Proof: 1046 By order_compute_alt, this is to show: 1047 (1) m <> 0 /\ coprime m n ==> order_search m (n MOD m) (phi m) 1 = ordz m n 1048 Let k = order_search m (n MOD m) (phi m) 1. 1049 Note 1 <= k by order_search_lower 1050 If m = 1, 1051 Note k <= MAX (phi 1) 1 by order_search_upper 1052 = MAX 1 1 by phi_1 1053 = 1 by MAX_DEF 1054 Thus k = 1 by 1 <= k, k <= 1 1055 = ordz 1 n by ZN_order_mod_1 1056 If m <> 1, 1057 Then 1 < m by 0 < m, m <> 1 1058 and 0 < k by 1 <= k 1059 Now 0 < phi m by phi_pos, 0 < m 1060 or 1 <= phi m by 0 < phi m 1061 1062 Note coprime m (n MOD m) by coprime_mod, 0 < m 1063 and n MOD m < m by MOD_LESS, 0 < m 1064 Also 0 < n MOD m by MOD_NONZERO_WHEN_GCD_ONE, 1 < m 1065 and (n MOD m) ** (phi m) MOD m = 1 by Euler_Fermat_eqn, phi_eq_totient, 1 < m 1066 ==> ((n MOD m) ** k) MOD m = 1 by order_search_property, 1 <= phi m 1067 and !j. 1 <= j /\ j < k ==> ((n MOD m) ** j) MOD m <> 1 by order_search_minimal, 1 <= phi m 1068 Thus k = ordz m (n MOD m) by ZN_order_test_1 1069 = ordz m n by ZN_order_mod, 0 < m 1070 (2) m <> 0 /\ gcd m n <> 1 ==> 0 = ordz m n 1071 Note 0 < m by arithmetic 1072 Thus ordz m n = 0 by ZN_order_eq_0, 0 < m. 1073*) 1074val order_compute_eqn = store_thm( 1075 "order_compute_eqn", 1076 ``!m n. order_compute m n = ordz m n``, 1077 rw[order_compute_alt] >| [ 1078 `0 < m` by decide_tac >> 1079 qabbrev_tac `k = order_search m (n MOD m) (phi m) 1` >> 1080 `1 <= k` by rw[order_search_lower, Abbr`k`] >> 1081 Cases_on `m = 1` >| [ 1082 `k <= 1` by metis_tac[order_search_upper, phi_1, MAX_DEF] >> 1083 rw[ZN_order_mod_1], 1084 `0 < k /\ 1 < m` by decide_tac >> 1085 `0 < phi m` by rw[phi_pos] >> 1086 `1 <= phi m` by decide_tac >> 1087 `coprime m (n MOD m)` by rw[coprime_mod] >> 1088 `n MOD m < m` by rw[MOD_LESS] >> 1089 `0 < n MOD m` by rw[MOD_NONZERO_WHEN_GCD_ONE] >> 1090 `(n MOD m) ** (phi m) MOD m = 1` by rw[Euler_Fermat_eqn, phi_eq_totient] >> 1091 `((n MOD m) ** k) MOD m = 1` by rw[order_search_property, Abbr`k`] >> 1092 `!j. 0 < j /\ j < k ==> ((n MOD m) ** j) MOD m <> 1` 1093 by metis_tac[order_search_minimal, DECIDE``1 <= n <=> 0 < n``] >> 1094 `k = ordz m (n MOD m)` by rw[ZN_order_test_1] >> 1095 `_ = ordz m n` by rw[ZN_order_mod] >> 1096 rw[] 1097 ], 1098 rw[ZN_order_eq_0] 1099 ]); 1100 1101(* ------------------------------------------------------------------------- *) 1102(* Efficient Order Computation *) 1103(* ------------------------------------------------------------------------- *) 1104(* Pseudocode: 1105 1106Input: m, n with 1 < m, 0 < n 1107Output: ordz m n, the least index j such that (n ** j = 1) (mod m) 1108 1109if ~(coprime m n) return 0 // initial check 1110// For coprime m n, ordz m (n MOD m) is a divisor of (phi m) by Euler-Fermat Theorem. 1111// Search upwards for least index j 1112j <- 1 // initial index 1113c <- phi m // recompute constant 1114n <- n MOD n // reduce n, by ordz m n = ordz m (n MOD m) 1115while (j <= c) { 1116 if (j divides c) and (n ** j = 1 (mod m)) return j // test j 1117 j <- j + 1 // increment j 1118} 1119return 0 // unreachable, unless no initial coprime check. 1120 1121*) 1122 1123(* A method to compute ordz m n: 1124Step 1: if (gcd m n <> 1) then 0 1125Step 2: By Euler-Fermat theorem, ordz m n = ordz m (n MOD m) is a divisor of (phi m). 1126 Just search from j = 1 to (phi m), 1127 If exp_mod_compute n j m = 1, return j. 1128 Search is upwards for the first (least) index j. 1129*) 1130 1131(* Question: How to show the number of steps is bounded? *) 1132 1133(* Formulate a recursive search for the least index, not using WHILE loop. *) 1134val ordz_search_def = tDefine "ordz_search" ` 1135 ordz_search m n c k = 1136 (* search is from k to maximum c *) 1137 if c <= k then k (* when k reaches c, k = c, must divide c, and exp_mod_compute n c m = 1 always. *) 1138 else if k divides c /\ (exp_mod_compute n k m = 1) then k (* that is, found k such that (n ** k) MOD m = 1 *) 1139 else ordz_search m n c (k + 1) (* current k is not suitable, try k + 1 instead. *) 1140` (WF_REL_TAC `measure (\(m,n,c,k). c - k)`); 1141(* 1142val ordz_search_def = |- !n m k c. ordz_search m n c k = 1143 if c <= k then k 1144 else if k divides c /\ (exp_mod_compute n k m = 1) then k 1145 else ordz_search m n c (k + 1): thm 1146*) 1147 1148(* Compute ordz m n *) 1149val ordz_fast_def = Define` 1150 ordz_fast m n = 1151 if n = 0 then ordz m 0 (* order is defined for nonzero only *) 1152 else if m = 0 then ordz m n (* MOD 0 is undefined *) 1153 else if (gcd_compute m n = 1) (* For coprimes, search from 1 ... *) 1154 then ordz_search m (n MOD m) (phi_compute m) 1 (* ordz m n = ordz m (n MOD m), divisor of phi m *) 1155 else 0 (* not coprime: order is 0 *) 1156`; 1157 1158(* Examples: 1159> EVAL ``ordz_fast 10 3``; --> 4 1160> EVAL ``ordz_fast 10 4``; --> 0 1161> EVAL ``ordz_fast 10 7``; --> 4 1162> EVAL ``ordz_fast 10 19``; --> 2 1163> EVAL ``ordz_fast 10 1``; --> 1 1164 1165> EVAL ``phi_compute 10``; --> 4 1166 1167Indeed, (ordz m n) is a divisor of (phi m). 1168Since phi(10) = 4, ordz 10 n is a divisior of 4. 1169*) 1170 1171(* Theorem: ordz_search m n c k = if c <= k then k 1172 else if k divides c /\ ((n ** k) MOD m = 1) then k else ordz_search m n c (k + 1) *) 1173(* Proof: by ordz_search_def, exp_mod_compute_eqn *) 1174val ordz_search_alt = store_thm( 1175 "ordz_search_alt", 1176 ``!m n c k. ordz_search m n c k = if c <= k then k 1177 else if k divides c /\ ((n ** k) MOD m = 1) then k else ordz_search m n c (k + 1)``, 1178 rw[Once ordz_search_def, exp_mod_compute_eqn]); 1179 1180(* Theorem: ordz_fast m n = if n = 0 then ordz m 0 1181 else if m = 0 then ordz m n 1182 else if coprime m n then ordz_search m (n MOD m) (phi m) 1 else 0 *) 1183(* Proof: by ordz_fast_def, gcd_compute_eqn, phi_compute_eqn *) 1184val ordz_fast_alt = store_thm( 1185 "ordz_fast_alt", 1186 ``!m n. ordz_fast m n = 1187 if n = 0 then ordz m 0 1188 else if m = 0 then ordz m n 1189 else if coprime m n then ordz_search m (n MOD m) (phi m) 1 else 0``, 1190 rw[ordz_fast_def, gcd_compute_eqn, phi_compute_eqn]); 1191 1192(* Theorem: ordz_search m n c c = c *) 1193(* Proof: ordz_search_def *) 1194val ordz_search_id = store_thm( 1195 "ordz_search_id", 1196 ``!m n c. ordz_search m n c c = c``, 1197 rw[Once ordz_search_def]); 1198 1199(* Theorem: c <= k ==> (ordz_search m n c k = k) *) 1200(* Proof: ordz_search_def *) 1201val ordz_search_over = store_thm( 1202 "ordz_search_over", 1203 ``!m n c k. c <= k ==> (ordz_search m n c k = k)``, 1204 rw[Once ordz_search_def]); 1205 1206(* Theorem: k < c /\ k divides c /\ ((n ** k) MOD m = 1) ==> (ordz_search m n c k = k) *) 1207(* Proof: by ordz_search_alt *) 1208val ordz_search_success = store_thm( 1209 "ordz_search_success", 1210 ``!m n c k. k < c /\ k divides c /\ ((n ** k) MOD m = 1) ==> (ordz_search m n c k = k)``, 1211 rw[Once ordz_search_alt]); 1212 1213(* Theorem: k <= ordz_search m n c k *) 1214(* Proof: 1215 By induction on (c - k). 1216 Base: (0 = c - k) ==> k <= ordz_search m n c k 1217 Note 0 = c - k means c <= k, 1218 or c <= k by SUB_EQ_0 1219 ordz_search m n c k 1220 = k by ordz_search_alt, ~(k < c) 1221 >= k by LESS_OR_EQ 1222 Step: !c k. (v = c - k) ==> k <= ordz_search m n c k ==> 1223 (SUC v = c - k) ==> k <= ordz_search m n c k 1224 Note SUC v = c - k means k < c by SUC_POS 1225 or v + 1 = c - k, or 1226 v = c - (k + 1) by arithmetic 1227 If (k divides c /\ (n ** k MOD m = 1)), 1228 ordz_search m n c k 1229 = k by ordz_search_alt, k < c 1230 >= k by LESS_OR_EQ 1231 If ~(k divides c /\ (n ** k MOD m = 1)), 1232 ordz_search m n c k 1233 = ordz_search m n c (k + 1) by ordz_search_alt, k < c 1234 >= k + 1 by induction hypothesis 1235 >= k by arithmetic 1236*) 1237val ordz_search_lower = store_thm( 1238 "ordz_search_lower", 1239 ``!m n c k. k <= ordz_search m n c k``, 1240 rpt strip_tac >> 1241 Induct_on `c - k` >| [ 1242 rpt strip_tac >> 1243 rw[Once ordz_search_alt], 1244 rpt strip_tac >> 1245 `v = c - (k + 1)` by decide_tac >> 1246 rw[Once ordz_search_alt] >> 1247 metis_tac[LESS_EQ_TRANS, DECIDE``k <= k + 1``] 1248 ]); 1249 1250(* Theorem: ordz_search m n c k <= MAX k c *) 1251(* Proof: 1252 By induction on (c - k). 1253 Base: (0 = c - k) ==> ordz_search m n c k <= MAX k c 1254 Note 0 = c - k means c <= k, 1255 or c <= k by SUB_EQ_0 1256 ordz_search m n c k 1257 = k by ordz_search_alt, ~(k < c) 1258 = MAX k c by c <= k 1259 <= MAX k c by LESS_OR_EQ 1260 Step: !c k. (v = c - k) ==> ordz_search m n c k <= MAX k c ==> 1261 (SUC v = c - k) ==> ordz_search m n c k <= MAX k c 1262 Note SUC v = c - k means k < c by SUC_POS 1263 or v + 1 = c - k, or 1264 v = c - (k + 1) by arithmetic 1265 If (k divides c /\ (n ** k MOD m = 1)), 1266 ordz_search m n c k 1267 = k by ordz_search_alt, k < c 1268 <= c by LESS_OR_EQ 1269 If ~(k divides c /\ (n ** k MOD m = 1)), 1270 ordz_search m n c k 1271 = ordz_search m n c (k + 1) by ordz_search_alt, k < c 1272 <= MAX (k + 1) c by induction hypothesis 1273 <= MAX k c by k < c ==> (k + 1) <= c 1274 Indeed, MAX (k + 1) c = c = MAX k c by MAX_DEF 1275*) 1276val ordz_search_upper = store_thm( 1277 "ordz_search_upper", 1278 ``!m n c k. ordz_search m n c k <= MAX k c``, 1279 rpt strip_tac >> 1280 Induct_on `c - k` >| [ 1281 rpt strip_tac >> 1282 rw[Once ordz_search_alt], 1283 rpt strip_tac >> 1284 `v = c - (k + 1)` by decide_tac >> 1285 `k <= MAX k c` by rw[] >> 1286 rw_tac bool_ss[Once ordz_search_alt] >> 1287 `MAX (k + 1) c = MAX k c` by rw[MAX_DEF] >> 1288 metis_tac[] 1289 ]); 1290 1291(* Theorem: k <= c /\ ((n ** c) MOD m = 1) ==> 1292 (ordz_search m n c k) divides c /\ (n ** (ordz_search m n c k) MOD m = 1) *) 1293(* Proof: 1294 Let t = order_search m n c k. 1295 If k = c, 1296 Then t = c by ordz_search_id 1297 so t divides c by DIVIDES_REFL, t = c 1298 and n ** t MOD m = 1 by (n ** c) MOD m = 1 1299 If k <> c, 1300 Then k < c by arithmetic 1301 By induction on (c - k). 1302 Base: (0 = c - k) ==> (ordz_search m n c k) divides c /\ (n ** (ordz_search m n c k) MOD m = 1) 1303 Note 0 = c - k means c <= k 1304 or c <= k by SUB_EQ_0 1305 This contradicts k < c. 1306 Step: !c k. (v = c - k) /\ k <= c ==> (ordz_search m n c k) divides c /\ (n ** (ordz_search m n c k) MOD m = 1) 1307 ==> SUC v = c - k ==> (ordz_search m n c k) divides c /\ (n ** (ordz_search m n c k) MOD m = 1) 1308 If (k divides c /\ (n ** k MOD m = 1)), 1309 Then t = k by ordz_search_alt, k < c 1310 so t divides c by k divides c 1311 and n ** t MOD m = 1 by n ** k MOD m = 1 1312 If ~(k divides c /\ (n ** k MOD m = 1)), 1313 Then t = ordz_search m n c (k + 1) by ordz_search_alt, k < c 1314 Note SUC v = c - k means k < c by SUC_POS 1315 or v + 1 = c - k, or 1316 v = c - (k + 1) by arithmetic 1317 Also k + 1 <= c by k < c 1318 If c = k + 1, 1319 Then t = ordz_search m n c c 1320 = c by ordz_search_id 1321 and c divides c by DIVIDES_REFL 1322 and n ** c MOD m = 1 by given 1323 If c <> k + 1, 1324 Then k + 1 < c by k < c 1325 ==> t divides c 1326 and n ** t MOD m = 1 by induction hypothesis, k + 1 < c 1327*) 1328val ordz_search_property = store_thm( 1329 "ordz_search_property", 1330 ``!m n c k. k <= c /\ ((n ** c) MOD m = 1) ==> 1331 (ordz_search m n c k) divides c /\ (n ** (ordz_search m n c k) MOD m = 1)``, 1332 ntac 5 strip_tac >> 1333 Cases_on `k = c` >- 1334 metis_tac[ordz_search_id, DIVIDES_REFL] >> 1335 `k < c` by decide_tac >> 1336 fs[] >> 1337 Induct_on `c - k` >| [ 1338 ntac 5 strip_tac >> 1339 decide_tac, 1340 ntac 5 strip_tac >> 1341 Cases_on `k divides c /\ (n ** k MOD m = 1)` >- 1342 rw[ordz_search_success] >> 1343 `ordz_search m n c k = ordz_search m n c (k + 1)` by rw[Once ordz_search_alt] >> 1344 `k + 1 <= c /\ (v = c - (k + 1))` by decide_tac >> 1345 Cases_on `c = k + 1` >- 1346 rw[ordz_search_id] >> 1347 rw[] 1348 ]); 1349 1350(* Theorem: k <= c ==> !j. k <= j /\ j < ordz_search m n c k ==> ~(j divides c /\ (n ** j MOD m = 1)) *) 1351(* Proof: 1352 By contradiction, suppose some j divides c /\ (n ** j MOD m = 1). 1353 Let t = ordz_search m n c k. 1354 If k = c, 1355 Then t = k by ordz_search_id 1356 But j < t = k by j < order_search m n c k (given) 1357 This contradicts k <= j. 1358 If k <> c, 1359 Then k < c by k <= c, k <> c. 1360 Use induction on (j - k). 1361 Base: 0 = j - k /\ k <= j ==> F 1362 Note 0 = j - k means j <= k. 1363 Thus j = k by j <= k, k <= j. 1364 so ordz_search m n c k = k by ordz_search_success, k < c, j divides c, n ** j MOD m = 1 1365 But j < ordz_search m n c k, 1366 or j < j, which is false by LESS_REFL 1367 Step: !j k. (v = j - k) /\ k < c /\ k <= j /\ j < ordz_search m n c k ==> F ==> 1368 SUC v = j - k /\ k < c /\ k <= j /\ j < ordz_search m n c k ==> F 1369 Note j < t by j < ordz_search m n c k 1370 If (k divides c /\ (n ** k MOD m = 1)), 1371 Then t = k by ordz_search_alt, k < c 1372 Thus j < t = k by j < ordz_search m n c k 1373 This contradicts k <= j. 1374 If ~(k divides c /\ (n ** k MOD m = 1)), 1375 Then t = ordz_search m n c (k + 1) by ordz_search_alt, k < c [1] 1376 Note t <= c by ordz_search_upper, MAX_DEF, k < c. 1377 so j < c by LESS_LESS_EQ_TRANS 1378 ==> ordz_search m n c j = j by ordz_search_success, j < c [2] 1379 1380 Note SUC v = j - k means k < j by SUC_POS 1381 or v + 1 = j - k, or 1382 v = j - (k + 1) by arithmetic 1383 Also k + 1 <= j by k < j 1384 If j = k + 1, 1385 Then t = ordz_search m n c j by [1], j = k + 1 1386 = j by [2] 1387 or j < j, which is false by LESS_REFL, j < t. 1388 If j <> k + 1, 1389 Then k + 1 < j by k < j 1390 or k + 1 < c by j < c 1391 Thus giving F by induction hypothesis 1392*) 1393val ordz_search_minimal = store_thm( 1394 "ordz_search_minimal", 1395 ``!m n c k. k <= c ==> !j. k <= j /\ j < ordz_search m n c k ==> ~(j divides c /\ (n ** j MOD m = 1))``, 1396 rpt strip_tac >> 1397 Cases_on `k = c` >| [ 1398 `ordz_search m n c k = k` by rw[ordz_search_id] >> 1399 decide_tac, 1400 `k < c` by decide_tac >> 1401 fs[] >> 1402 Induct_on `j - k` >| [ 1403 rpt strip_tac >> 1404 `j = k` by decide_tac >> 1405 metis_tac[ordz_search_success, DECIDE``~(n < n)``], 1406 rpt strip_tac >> 1407 Cases_on `k divides c /\ (n ** k MOD m = 1)` >| [ 1408 `ordz_search m n c k = k` by rw[ordz_search_success] >> 1409 decide_tac, 1410 `j < c` by metis_tac[ordz_search_upper, MAX_DEF, LESS_LESS_EQ_TRANS] >> 1411 `ordz_search m n c j = j` by rw[ordz_search_success] >> 1412 `ordz_search m n c k = ordz_search m n c (k + 1)` by rw[Once ordz_search_alt] >> 1413 `k + 1 <= j /\ (v = j - (k + 1))` by decide_tac >> 1414 Cases_on `j = k + 1` >- 1415 metis_tac[DECIDE``~(n < n)``] >> 1416 `k + 1 < c` by decide_tac >> 1417 metis_tac[] 1418 ] 1419 ] 1420 ]); 1421 1422(* Theorem: ordz_fast m n = ordz m n *) 1423(* Proof: 1424 By ordz_fast_alt, this is to show: 1425 (1) m <> 0 /\ coprime m n ==> ordz_search m (n MOD m) (phi m) 1 = ordz m n 1426 Note ~(m <= 1) means 1 < m by NOT_LESS_EQUAL 1427 Let k = ordz_search m (n MOD m) (phi m) 1. 1428 Note 1 <= k by ordz_search_lower 1429 If m = 1, 1430 Note k <= MAX (phi 1) 1 by ordz_search_upper 1431 = MAX 1 1 by phi_1 1432 = 1 by MAX_DEF 1433 Thus k = 1 by 1 <= k, k <= 1 1434 = ordz 1 n by ZN_order_mod_1 1435 If m <> 1, 1436 Then 1 < m by 0 < m, m <> 1 1437 and 0 < k by 1 <= k 1438 Now 0 < phi m by phi_pos, 0 < m 1439 or 1 <= phi m by 0 < phi m 1440 1441 Note coprime m (n MOD m) by coprime_mod, 0 < m 1442 and n MOD m < m by MOD_LESS, 0 < m 1443 Also 0 < n MOD m by MOD_NONZERO_WHEN_GCD_ONE, 1 < m 1444 and (n MOD m) ** (phi m) MOD m = 1 by Euler_Fermat_eqn, phi_eq_totient, 1 < m 1445 ==> ((n MOD m) ** k) MOD m = 1 by ordz_search_property, 1 <= phi m 1446 and !j. 1 <= j /\ j < k /\ j divides (phi m) 1447 ==> ((n MOD m) ** j) MOD m <> 1 by ordz_search_minimal, 1 <= phi m 1448 or !j. 0 < j /\ j < k /\ j divides (phi m) 1449 ==> ((n MOD m) ** j) MOD m <> 1 by arithmetic 1450 Thus k = ordz m (n MOD m) by ZN_order_test_2 1451 = ordz m n by ZN_order_mod, 0 < m 1452 (2) m <> 0 /\ gcd m n <> 1 ==> 0 = ordz m n 1453 Note ~(m <= 1) means 1 < m by NOT_LESS_EQUAL 1454 Thus ordz m n = 0 by ZN_order_eq_0, 0 < m. 1455*) 1456val ordz_fast_eqn = store_thm( 1457 "ordz_fast_eqn", 1458 ``!m n. ordz_fast m n = ordz m n``, 1459 rw[ordz_fast_alt] >| [ 1460 `0 < m` by decide_tac >> 1461 qabbrev_tac `k = ordz_search m (n MOD m) (phi m) 1` >> 1462 `1 <= k` by rw[ordz_search_lower, Abbr`k`] >> 1463 Cases_on `m = 1` >| [ 1464 `k <= 1` by metis_tac[ordz_search_upper, phi_1, MAX_DEF] >> 1465 rw[ZN_order_mod_1], 1466 `0 < k /\ 1 < m` by decide_tac >> 1467 `0 < phi m` by rw[phi_pos] >> 1468 `1 <= phi m` by decide_tac >> 1469 `coprime m (n MOD m)` by rw[coprime_mod] >> 1470 `n MOD m < m` by rw[MOD_LESS] >> 1471 `0 < n MOD m` by rw[MOD_NONZERO_WHEN_GCD_ONE] >> 1472 `(n MOD m) ** (phi m) MOD m = 1` by rw[Euler_Fermat_eqn, phi_eq_totient] >> 1473 `((n MOD m) ** k) MOD m = 1` by rw[ordz_search_property, Abbr`k`] >> 1474 `!j. 0 < j /\ j < k /\ j divides (phi m) ==> ((n MOD m) ** j) MOD m <> 1` 1475 by metis_tac[ordz_search_minimal, DECIDE``1 <= n <=> 0 < n``] >> 1476 `k = ordz m (n MOD m)` by rw[ZN_order_test_2] >> 1477 `_ = ordz m n` by rw[ZN_order_mod] >> 1478 rw[] 1479 ], 1480 rw[ZN_order_eq_0] 1481 ]); 1482 1483(* ------------------------------------------------------------------------- *) 1484 1485(* export theory at end *) 1486val _ = export_theory(); 1487 1488(*===========================================================================*) 1489