1(* ------------------------------------------------------------------------- *) 2(* Polynomial computations in monadic style. *) 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 "countPoly"; 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(* val _ = load "countModuloTheory"; *) 24open countMonadTheory countMacroTheory; 25open countModuloTheory; 26 27open bitsizeTheory complexityTheory; 28open loopIncreaseTheory loopDecreaseTheory; 29open loopDivideTheory loopListTheory; 30 31(* Get dependent theories in lib *) 32(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 33(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 34open helperNumTheory helperSetTheory helperListTheory; 35open helperFunctionTheory; 36 37(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 38(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 39open pred_setTheory listTheory arithmeticTheory; 40open dividesTheory gcdTheory; 41open rich_listTheory listRangeTheory; 42 43(* (* val _ = load "logPowerTheory"; *) *) 44open logrootTheory logPowerTheory; 45 46(* (* val _ = load "monadsyntax"; *) *) 47open monadsyntax; 48open pairTheory optionTheory; 49 50(* val _ = load "ringInstancesTheory"; *) 51open ringInstancesTheory; (* for ZN order *) 52 53(* val _ = load "computeRingTheory"; *) 54open computeRingTheory; (* for ZN_poly_cmult_alt *) 55open computePolyTheory; (* for unity_mod_monomial *) 56 57open polynomialTheory polyWeakTheory; 58 59val _ = monadsyntax.enable_monadsyntax(); 60val _ = monadsyntax.enable_monad "Count"; 61 62 63(* ------------------------------------------------------------------------- *) 64(* Polynomial computations in monadic style Documentation *) 65(* ------------------------------------------------------------------------- *) 66(* Data type: 67*) 68(* Overloading: 69*) 70(* Definitions and Theorems (# are exported): 71 72 Helper: 73 74 Making polynomials: 75 poly_extendM_def |- !p k. poly_extendM p k = 76 do 77 k0 <- zeroM k; 78 if k0 then unit p 79 else do q <- consM 0 p; k' <- decM k; poly_extendM q k' od 80 od 81 poly_zeroM_def |- !k. poly_zeroM k = poly_extendM [] k 82 poly_oneM_def |- !n k. poly_oneM n k = 83 do 84 k0 <- zeroM k; 85 if k0 then unit [] 86 else 87 do 88 j <- decM k; 89 p <- poly_zeroM n j; 90 c <- modM 1 n; 91 consM c p 92 od 93 od 94# poly_extendM_value |- !n p k. valueOf (poly_extendM p k) = unity_mod_zero (ZN n) k ++ p 95 poly_extendM_nil |- !n k. valueOf (poly_extendM [] k) = unity_mod_zero (ZN n) k 96# poly_zeroM_value |- !n k. valueOf (poly_zeroM n k) = unity_mod_zero (ZN n) k 97# poly_oneM_value |- !n k. valueOf (poly_oneM n k) = unity_mod_one (ZN n) k 98 poly_zeroM_weak |- !n k. 0 < n ==> Weak (ZN n) (valueOf (poly_zeroM n k)) 99# poly_zeroM_length |- !n k. LENGTH (valueOf (poly_zeroM n k)) = k 100 poly_oneM_weak |- !n k. 0 < n ==> Weak (ZN n) (valueOf (poly_oneM n k)) 101# poly_oneM_length |- !n k. LENGTH (valueOf (poly_oneM n k)) = k 102 poly_extendM_steps_thm 103 |- !p k. stepsOf (poly_extendM p k) = 104 size k + if k = 0 then 0 105 else 1 + size k + stepsOf (poly_extendM (0::p) (k - 1)) 106 poly_extendM_steps_by_dec_loop 107 |- !p k. stepsOf (poly_extendM p k) = 108 if k = 0 then 1 109 else 1 + TWICE (size k) + stepsOf (poly_extendM (0::p) (k - 1)) 110 poly_extendM_steps_eqn 111 |- !p k. stepsOf (poly_extendM p k) = 1 + SUM (MAP (\j. 1 + TWICE (size j)) [1 .. k]) 112 poly_extendM_steps_upper 113 |- !p k. stepsOf (poly_extendM p k) <= 1 + k + TWICE k * size k 114 poly_extendM_steps_bound 115 |- !p k. stepsOf (poly_extendM p k) <= 4 * MAX 1 k * size k 116 poly_zeroM_steps_eqn 117 |- !n k. stepsOf (poly_zeroM n k) = 1 + SUM (MAP (\j. 1 + TWICE (size j)) [1 .. k]) 118 poly_zeroM_steps_upper 119 |- !n k. stepsOf (poly_zeroM n k) <= 1 + k + TWICE k * size k 120 poly_zeroM_steps_bound 121 |- !n k. stepsOf (poly_zeroM n k) <= 4 * MAX 1 k * size k 122 poly_oneM_steps_eqn 123 |- !n k. stepsOf (poly_oneM n k) = 124 if k = 0 then 1 125 else 1 + SUM (MAP (\j. 1 + TWICE (size j)) [1 .. k]) + size n 126 poly_oneM_steps_upper 127 |- !n k. stepsOf (poly_oneM n k) <= 1 + k + TWICE (size k) + TWICE k * size k + size n 128 poly_oneM_steps_bound 129 |- !n k. stepsOf (poly_oneM n k) <= 7 * MAX 1 k * size k * size n 130 131 Constant Polynomial: 132 poly_constM_def |- !n k c. poly_constM n k c = 133 do 134 k0 <- zeroM k; 135 if k0 then unit [] 136 else 137 do 138 j <- decM k; 139 p <- poly_zeroM n j; 140 d <- modM c n; 141 consM d p 142 od 143 od 144# poly_constM_value |- !n k c. 0 < n ==> valueOf (poly_constM n k c) = unity_mod_const (ZN n) k c 145 poly_constM_zero |- !k c. valueOf (poly_constM 0 k c) = if k = 0 then [] else PAD_RIGHT 0 k [c MOD 0] 146 poly_constM_weak |- !n k c. 0 < n ==> Weak (ZN n) (valueOf (poly_constM n k c)) 147# poly_constM_length |- !n k c. LENGTH (valueOf (poly_constM n k c)) = k 148 poly_constM_steps_eqn |- !n k c. stepsOf (poly_constM n k c) = 149 if k = 0 then 1 150 else 1 + SUM (MAP (\j. 1 + TWICE (size j)) [1 .. k]) + size c * size n 151 poly_constM_steps_upper 152 |- !n k c. stepsOf (poly_constM n k c) <= 153 1 + k + TWICE (size k) + TWICE k * size k + size c * size n 154 poly_constM_steps_bound 155 |- !n k c. stepsOf (poly_constM n k c) <= 156 7 * MAX 1 k * size k * size c * size n 157 158 Powers of X: 159 poly_X_expM_def |- !n k m. poly_X_expM n k m = 160 do 161 k0 <- zeroM k; 162 if k0 then unit [] 163 else 164 do 165 c <- modM 1 n; 166 k1 <- oneM k; 167 if k1 then consM c [] 168 else 169 do 170 j <- modM m k; 171 h <- subM k j; 172 i <- decM h; 173 p <- poly_zeroM n i; 174 q <- consM c p; 175 poly_extendM q j 176 od 177 od 178 od 179# poly_X_expM_value |- !n k m. 0 < n ==> valueOf (poly_X_expM n k m) = unity_mod_X_exp (ZN n) k m 180 poly_X_expM_zero |- !k m. valueOf (poly_X_expM 0 k m) = 181 if k = 0 then [] 182 else PAD_RIGHT 0 k (PAD_LEFT 0 (m MOD k + 1) [1 MOD 0]) 183 poly_X_expM_weak |- !n k m. 0 < n ==> Weak (ZN n) (valueOf (poly_X_expM n k m)) 184# poly_X_expM_length |- !n k m. LENGTH (valueOf (poly_X_expM n k m)) = k 185 poly_X_expM_steps_eqn |- !n k m. stepsOf (poly_X_expM n k m) = 186 if k = 0 then 1 187 else size n + TWICE (size k) + 188 if k = 1 then 1 189 else (if k = 0 then 0 else size m * size k) + 1 + 190 size (MAX k (m MOD k)) + size (k - m MOD k) + 191 stepsOf (poly_zeroM n (k - m MOD k - 1)) + 192 stepsOf (poly_extendM 193 (1 MOD n::unity_mod_zero (ZN n) (k - m MOD k - 1)) (m MOD k)) 194 poly_X_expM_steps_upper 195 |- !n k m. stepsOf (poly_X_expM n k m) <= 196 3 + TWICE k + size n + 4 * size k + size m * size k + 4 * k * size k 197 poly_X_expM_steps_bound 198 |- !n k m. stepsOf (poly_X_expM n k m) <= 199 15 * MAX 1 k * size k * size n * size m 200 201 Polynomial operations: 202 poly_eqM_def |- !q p. poly_eqM p q = 203 do 204 p0 <- nullM p; 205 q0 <- nullM q; 206 if p0 then unit q0 207 else if q0 then unit p0 208 else 209 do 210 h1 <- headM p; 211 t1 <- tailM p; 212 h2 <- headM q; 213 t2 <- tailM q; 214 e0 <- eqM h1 h2; 215 if e0 then poly_eqM t1 t2 else unit F 216 od 217 od 218# poly_eqM_value |- !p q. valueOf (poly_eqM p q) <=> p = q 219 poly_eqM_steps_thm 220 |- !p q. stepsOf (poly_eqM p q) = 221 2 + if (p = []) \/ (q = []) then 0 222 else 4 + size (MAX (HD p) (HD q)) + 223 if HD p <> HD q then 0 else stepsOf (poly_eqM (TL p) (TL q)) 224 poly_eqM_steps_by_list_loop 225 |- !p q. stepsOf (poly_eqM p q) = 226 if (p = []) \/ (q = []) then 2 227 else 6 + size (MAX (HD p) (HD q)) + 228 if HD p <> HD q then 0 else stepsOf (poly_eqM (TL p) (TL q)) 229 poly_eqM_steps_by_sum_le 230 |- !p q k. (LENGTH p = k) /\ (LENGTH q = k) ==> 231 stepsOf (poly_eqM p q) <= 232 2 + SUM (GENLIST (\j. 6 + size (MAX (EL j p) (EL j q))) k) 233 poly_eqM_steps_upper 234 |- !p q k n. Weak (ZN n) p /\ Weak (ZN n) q /\ 235 (LENGTH p = k) /\ (LENGTH q = k) ==> 236 stepsOf (poly_eqM p q) <= 2 + 6 * k + k * size n 237 poly_eqM_steps_bound 238 |- !p q k n. Weak (ZN n) p /\ Weak (ZN n) q /\ 239 (LENGTH p = k) /\ (LENGTH q = k) ==> 240 stepsOf (poly_eqM p q) <= 9 * MAX 1 k * size n 241 242 243 poly_cmultM_def |- !p n c. poly_cmultM n c p = 244 do 245 p0 <- nullM p; 246 if p0 then unit [] 247 else 248 do 249 h <- headM p; 250 t <- tailM p; 251 k <- mmulM n c h; 252 q <- poly_cmultM n c t; 253 consM k q 254 od 255 od 256# poly_cmultM_value |- !n c p. valueOf (poly_cmultM n c p) = weak_cmult (ZN n) c p 257 poly_cmultM_value_alt |- !n c p. Weak (ZN n) p ==> valueOf (poly_cmultM n c p) = c oz p 258 poly_cmultM_element |- !n c p j. j < LENGTH p ==> EL j (valueOf (poly_cmultM n c p)) = (c * EL j p) MOD n 259 poly_cmultM_weak |- !n c p. 0 < n ==> Weak (ZN n) (valueOf (poly_cmultM n c p)) 260# poly_cmultM_length |- !n c p. LENGTH (valueOf (poly_cmultM n c p)) = LENGTH p 261 poly_cmultM_steps_thm |- !n c p. stepsOf (poly_cmultM n c p) = 262 if (p = []) then 1 263 else 4 + size c * size (HD p) + 264 size (c * HD p) * size n + 265 stepsOf (poly_cmultM n c (TL p)) 266 poly_cmultM_steps_by_list_loop 267 |- !n c p. stepsOf (poly_cmultM n c p) = 268 if (p = []) then 1 269 else 4 + size c * size (HD p) + 270 size (c * HD p) * size n + 271 stepsOf (poly_cmultM n c (TL p)) 272 poly_cmultM_steps_eqn |- !n c p. stepsOf (poly_cmultM n c p) = 273 1 + SUM (GENLIST 274 (\j. 4 + size c * size (EL j p) + size (c * (EL j p)) * size n) 275 (LENGTH p)) 276 poly_cmultM_steps_upper |- !n c p k. Weak (ZN n) p /\ (LENGTH p = k) ==> 277 stepsOf (poly_cmultM n c p) <= 278 1 + 4 * k + TWICE k * size c * size n + k * size n ** 2 279 poly_cmultM_steps_bound |- !n c p k. Weak (ZN n) p /\ (LENGTH p = k) ==> 280 stepsOf (poly_cmultM n c p) <= 281 8 * MAX 1 k * size (MAX c n) * size n 282 283 Polynomial weak addition: 284 poly_addM_def |- !q p n. poly_addM n p q = 285 do 286 p0 <- nullM p; 287 q0 <- nullM q; 288 if p0 then unit q 289 else if q0 then unit p 290 else 291 do 292 h1 <- headM p; 293 h2 <- headM q; 294 t1 <- tailM p; 295 t2 <- tailM q; 296 h <- maddM n h1 h2; 297 r <- poly_addM n t1 t2; 298 consM h r 299 od 300 od 301# poly_addM_value |- !n p q. valueOf (poly_addM n p q) = weak_add (ZN n) p q 302 poly_addM_value_alt |- !n p q. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = LENGTH q) ==> 303 valueOf (poly_addM n p q) = p +z q 304 poly_addM_element |- !n p q j. j < LENGTH p /\ j < LENGTH q ==> 305 EL j (valueOf (poly_addM n p q)) = (EL j p + EL j q) MOD n 306 poly_addM_weak |- !n p q. 0 < n /\ (LENGTH p = LENGTH q) ==> 307 Weak (ZN n) (valueOf (poly_addM n p q)) 308# poly_addM_length |- !n p q. LENGTH (valueOf (poly_addM n p q)) = MAX (LENGTH p) (LENGTH q) 309 poly_addM_steps_thm |- !n p q. stepsOf (poly_addM n p q) = 310 if (p = []) \/ (q = []) then 2 311 else 7 + size (MAX (HD p) (HD q)) + 312 size (HD p + HD q) * size n + 313 stepsOf (poly_addM n (TL p) (TL q)) 314 poly_addM_steps_by_list_loop 315 |- !n p q. stepsOf (poly_addM n p q) = 316 if (p = []) \/ (q = []) then 2 317 else 7 + size (MAX (HD p) (HD q)) + 318 size (HD p + HD q) * size n + 319 stepsOf (poly_addM n (TL p) (TL q)) 320 poly_addM_steps_eqn |- !n p q k. (LENGTH p = k) /\ (LENGTH q = k) ==> 321 stepsOf (poly_addM n p q) = 322 2 + SUM (GENLIST (\j. 7 + size (MAX (EL j p) (EL j q)) + 323 size (EL j p + EL j q) * size n) k 324 poly_addM_steps_upper |- !n p q k. Weak (ZN n) p /\ Weak (ZN n) q /\ 325 (LENGTH p = k) /\ (LENGTH q = k) ==> 326 stepsOf (poly_addM n p q) <= 327 2 + 7 * k + TWICE k * size n + k * size n ** 2 328 poly_addM_steps_bound |- !n p q k. Weak (ZN n) p /\ Weak (ZN n) q /\ 329 (LENGTH p = k) /\ (LENGTH q = k) ==> 330 stepsOf (poly_addM n p q) <= 12 * MAX 1 k * size n ** 2 331 332 Polynomial multiplication by X: 333 poly_lastM_def |- !p. poly_lastM p = 334 do 335 p0 <- nullM p; 336 if p0 then unit (LAST []) 337 else 338 do 339 h <- headM p; 340 t <- tailM p; 341 t0 <- nullM t; 342 if t0 then unit h else poly_lastM t 343 od 344 od 345 poly_frontM_def |- !p. poly_frontM p = 346 do 347 p0 <- nullM p; 348 if p0 then unit (FRONT []) 349 else 350 do 351 h <- headM p; 352 t <- tailM p; 353 t0 <- nullM t; 354 if t0 then unit [] else do q <- poly_frontM t; consM h q od 355 od 356 od 357 poly_turnM_def |- !p. poly_turnM p = 358 do 359 p0 <- nullM p; 360 if p0 then unit [] 361 else do h <- poly_lastM p; t <- poly_frontM p; consM h t od 362 od 363 poly_lastM_value |- !p. valueOf (poly_lastM p) = LAST p 364 poly_frontM_value |- !p. valueOf (poly_frontM p) = FRONT p 365 poly_turnM_value |- !p. valueOf (poly_turnM p) = turn p 366 poly_lastM_steps_thm |- !p. stepsOf (poly_lastM p) = 367 if (p = []) then 1 368 else 4 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) 369 poly_lastM_steps_by_list_loop 370 |- !p. stepsOf (poly_lastM p) = 371 if (p = []) then 1 372 else 4 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) 373 poly_lastM_steps_upper|- !p. stepsOf (poly_lastM p) <= 1 + 4 * LENGTH p 374 poly_frontM_steps_thm |- !p. stepsOf (poly_frontM p) = 375 if (p = []) then 1 376 else 4 + (if (TL p = []) then 0 else 1) + 377 if (TL p = []) then 0 else stepsOf (poly_frontM (TL p)) 378 poly_frontM_steps_by_list_loop 379 |- !p. stepsOf (poly_frontM p) = 380 if (p = []) then 1 381 else 4 + (if (TL p = []) then 0 else 1) + 382 if (TL p = []) then 0 else stepsOf (poly_frontM (TL p)) 383 poly_frontM_steps_upper |- !p. stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p 384 poly_turnM_steps_thm |- !p. stepsOf (poly_turnM p) = 385 if (p = []) then 1 386 else 2 + stepsOf (poly_lastM p) + stepsOf (poly_frontM p) 387 poly_turnM_weak |- !n p. Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_turnM p)) 388 poly_turnM_length |- !p. LENGTH (valueOf (poly_turnM p)) = LENGTH p 389 poly_turnM_steps_upper |- !p. stepsOf (poly_turnM p) <= 4 + 9 * LENGTH p 390 poly_turnM_steps_bound |- !p k. (LENGTH p = k) ==> stepsOf (poly_turnM p) <= 13 * MAX 1 k 391 392 poly_lastM_steps_eqn |- !p. stepsOf (poly_lastM p) = if (p = []) then 1 else 4 * LENGTH p 393 poly_frontM_steps_eqn |- !p. stepsOf (poly_frontM p) = if (p = []) then 1 else 5 * LENGTH p - 1 394 poly_turnM_steps_eqn |- !p. stepsOf (poly_turnM p) = if (p = []) then 1 else 1 + 9 * LENGTH p 395 396 poly_multM_def |- !q p n. poly_multM n p q = 397 do 398 p0 <- nullM p; 399 q0 <- nullM q; 400 if p0 \/ q0 then unit [] 401 else 402 do 403 h <- headM q; 404 t <- tailM q; 405 p1 <- poly_cmultM n h p; 406 r <- poly_turnM p; 407 p2 <- poly_multM n r t; 408 poly_addM n p1 p2; 409 od 410 od 411# poly_multM_value |- !n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 412 valueOf (poly_multM n p q) = unity_mod_mult (ZN n) p q 413 poly_multM_value_thm |- !n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] /\ (LENGTH p = k) ==> 414 valueOf (poly_multM n p q) = p *z q 415 poly_multM_value_alt |- !n p q k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 416 (LENGTH p = k) /\ (LENGTH q = k) ==> 417 valueOf (poly_multM n p q) = p *z q 418 poly_multM_weak |- !n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 419 Weak (ZN n) (valueOf (poly_multM n p q)) 420 poly_multM_length |- !n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 421 LENGTH (valueOf (poly_multM n p q)) = 422 if q = [] then 0 else LENGTH p 423 poly_multM_nil |- !n p. 0 < n /\ Weak (ZN n) p ==> valueOf (poly_multM n p []) = [] 424 poly_multM_steps_thm |- !n p q. stepsOf (poly_multM n p q) = 425 if q = [] then 1 426 else 3 + stepsOf (poly_turnM p) + 427 stepsOf (poly_cmultM n (HD q) p) + 428 stepsOf (poly_addM n 429 (weak_cmult (ZN n) (HD q) p) 430 (valueOf (poly_multM n (turn p) (TL q)))) + 431 stepsOf (poly_multM n (turn p) (TL q)) 432 poly_multM_steps_nil |- !n p. stepsOf (poly_multM n p []) = 1 433 poly_multM_steps_sing_thm 434 |- !n p c. 0 < n /\ Weak (ZN n) p ==> 435 stepsOf (poly_multM n p [c]) = 436 6 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n c p) 437 poly_multM_steps_sing_upper 438 |- !n p c k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 439 stepsOf (poly_multM n p [c]) <= 440 10 + 9 * k + 8 * MAX 1 k * size (MAX c n) * size n 441 poly_multM_steps_sing_bound 442 |- !n p c k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 443 stepsOf (poly_multM n p [c]) <= 444 27 * MAX 1 k * size (MAX c n) * size n 445 poly_multM_steps_by_list_loop 446 |- !n p q. stepsOf (poly_multM n p q) = if q = [] then 1 447 else 3 + stepsOf (poly_turnM p) + 448 stepsOf (poly_cmultM n (HD q) p) + 449 stepsOf (poly_addM n 450 (weak_cmult (ZN n) (HD q) p) 451 (valueOf (poly_multM n (turn p) (TL q)))) + 452 stepsOf (poly_multM n (turn p) (TL q)) 453 poly_multM_steps_body_upper 454 |- !n. (let body p q = 3 + stepsOf (poly_turnM p) + 455 stepsOf (poly_cmultM n (HD q) p) + 456 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) 457 (valueOf (poly_multM n (turn p) (TL q)))) 458 in !p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] ==> 459 body p q <= 10 + LENGTH p * (20 + TWICE (size n) + 4 * size n ** 2)) 460 poly_multM_steps_body_cover 461 |- !n. (let body p q = 3 + stepsOf (poly_turnM p) + 462 stepsOf (poly_cmultM n (HD q) p) + 463 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) 464 (valueOf (poly_multM n (turn p) (TL q)))) 465 in !p q k. 0 < n /\ (LENGTH p = k) /\ (LENGTH q = k) /\ 466 Weak (ZN n) p /\ Weak (ZN n) q ==> 467 !j. j < k ==> body (turn_exp p j) (DROP j q) <= 468 10 + k * (20 + TWICE (size n) + 4 * size n ** 2)) 469 poly_multM_steps_upper|- !n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 470 (LENGTH p = k) /\ (LENGTH q = k) ==> 471 stepsOf (poly_multM n p q) <= 472 1 + 10 * k + 20 * k ** 2 + 473 TWICE (k ** 2) * size n + 4 * k ** 2 * size n ** 2 474 poly_multM_steps_bound|- !n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 475 (LENGTH p = k) /\ (LENGTH q = k) ==> 476 stepsOf (poly_multM n p q) <= 37 * MAX 1 k ** 2 * size n ** 2 477 poly_multM_steps_bound_alt 478 |- !n p q k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 479 (LENGTH p = k) /\ (LENGTH q = k) ==> 480 stepsOf (poly_multM n p q) <= 37 * k ** 2 * size n ** 2 481 482 poly_sqM_def |- !n p. poly_sqM n p = poly_multM n p p 483# poly_sqM_value |- !n p. 0 < n /\ Weak (ZN n) p ==> 484 valueOf (poly_sqM n p) = unity_mod_sq (ZN n) p 485 poly_sqM_value_thm |- !n p k. 0 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 486 (valueOf (poly_sqM n p) = sqz p) 487 poly_sqM_value_alt |- !n p k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 488 (valueOf (poly_sqM n p) = sqz p) 489 poly_sqM_weak |- !n p. 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_sqM n p)) 490 poly_sqM_length |- !n p. 0 < n /\ Weak (ZN n) p ==> 491 LENGTH (valueOf (poly_sqM n p)) = LENGTH p 492 poly_sqM_iterating_weak 493 |- !n p. 0 < n /\ Weak (ZN n) p ==> 494 !k. Weak (ZN n) (FUNPOW (\p. valueOf (poly_sqM n p)) k p) 495 poly_sqM_iterating_length 496 |- !n p. 0 < n /\ Weak (ZN n) p ==> 497 !k. LENGTH (FUNPOW (\p. valueOf (poly_sqM n p)) k p) = LENGTH p 498 poly_sqM_steps_thm |- !n p. 0 < n /\ Weak (ZN n) p ==> 499 stepsOf (poly_sqM n p) = 500 if (p = []) then 1 501 else 3 + stepsOf (poly_turnM p) + 502 stepsOf (poly_cmultM n (HD p) p) + 503 stepsOf (poly_addM n (weak_cmult (ZN n) (HD p) p) 504 (unity_mod_mult (ZN n) (turn p) (TL p))) + 505 stepsOf (poly_multM n (turn p) (TL p)) 506 poly_sqM_steps_upper |- !n p k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 507 stepsOf (poly_sqM n p) <= 508 1 + 10 * k + 20 * k ** 2 + 509 TWICE (k ** 2) * size n + 4 * k ** 2 * size n ** 2 510 poly_sqM_steps_bound |- !n p k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 511 stepsOf (poly_sqM n p) <= 37 * MAX 1 k ** 2 * size n ** 2 512 poly_sqM_steps_bound_alt 513 |- !n p k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 514 stepsOf (poly_sqM n p) <= 37 * k ** 2 * size n ** 2 515 516 poly_expM_def |- !p n j. poly_expM n p j = 517 do 518 j0 <- zeroM j; 519 if j0 then 520 do t <- consM 1 []; q <- poly_cmultM n 0 p; poly_addM n t q od 521 else 522 do 523 p1 <- poly_sqM n p; 524 h <- halfM j; 525 q <- poly_expM n p1 h; 526 ifM (evenM j) (return q) (poly_multM n p q) 527 od 528 od 529# poly_expM_value |- !n p j. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 530 valueOf (poly_expM n p j) = unity_mod_exp (ZN n) p j 531 poly_expM_value_thm |- !n p j k. 1 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 532 (valueOf (poly_expM n p j) = p **z j) 533 poly_expM_value_alt |- !n p j k. 1 < n /\ 0 < k /\ zweak p /\ (LENGTH p = k) ==> 534 (valueOf (poly_expM n p j) = p **z j) 535 poly_expM_weak |- !n p j. 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_expM n p j)) 536 poly_expM_length |- !n p j. 0 < n /\ Weak (ZN n) p ==> 537 LENGTH (valueOf (poly_expM n p j)) = 538 if n = 1 then 0 else if j = 0 then 1 else LENGTH p 539 poly_expM_0 |- !n p. valueOf (poly_expM n p 0) = if n = 1 then [] else [1] 540 poly_expM_trivial |- !p j. Weak (ZN 1) p ==> valueOf (poly_expM 1 p j) = [] 541 poly_expM_steps_thm |- !n p j. stepsOf (poly_expM n p j) = 542 size j + 543 if j = 0 then size n + if n = 1 then 0 else 1 544 else 1 + 4 * size j + stepsOf (poly_sqM n p) + 545 (if EVEN j then 0 else 546 stepsOf (poly_multM n p 547 (valueOf (poly_expM n 548 (valueOf (poly_sqM n p)) (HALF j))))) + 549 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)) 550 poly_expM_steps_by_div_loop 551 |- !n. (let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 552 if EVEN j then 0 553 else stepsOf (poly_multM n p 554 (valueOf (poly_expM n 555 (valueOf (poly_sqM n p)) (HALF j)))) 556 in !p j. stepsOf (poly_expM n p j) = 557 if j = 0 then 1 + size n + if n = 1 then 0 else 1 558 else body p j + 559 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))) 560 poly_expM_body_upper |- !n. (let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 561 if EVEN j then 0 562 else stepsOf (poly_multM n p 563 (valueOf (poly_expM n 564 (valueOf (poly_sqM n p)) (HALF j)))) 565 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 566 body p j <= 567 1 + 5 * size j + 74 * MAX 1 k ** 2 * size n ** 2) 568 poly_expM_body_bound |- !n. (let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 569 if EVEN j then 0 570 else stepsOf (poly_multM n p 571 (valueOf (poly_expM n 572 (valueOf (poly_sqM n p)) (HALF j)))) 573 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 574 body p j <= 80 * size j * MAX 1 k ** 2 * size n ** 2) 575 poly_expM_steps_upper |- !p n j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 576 stepsOf (poly_expM n p j) <= 577 2 + size n + 80 * MAX 1 k ** 2 * size j ** 2 * size n ** 2 578 poly_expM_steps_bound |- !p n j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 579 stepsOf (poly_expM n p j) <= 580 83 * MAX 1 k ** 2 * size j ** 2 * size n ** 2 581 poly_expM_steps_bound_alt 582 |- !p n j k. 1 < n /\ 0 < k /\ zweak p /\ (LENGTH p = k) ==> 583 stepsOf (poly_expM n p j) <= 584 83 * k ** 2 * size j ** 2 * size n ** 2 585 586 poly_get_coeffM_def |- !p j. poly_get_coeffM p j = 587 do 588 j0 <- zeroM j; 589 if j0 then headM p 590 else do q <- tailM p; i <- decM j; poly_get_coeffM q i od 591 od 592 poly_put_coeffM_def |- !x p j. poly_put_coeffM x p j = 593 do 594 q <- tailM p; 595 j0 <- zeroM j; 596 if j0 then consM x q 597 else 598 do 599 h <- headM p; 600 i <- decM j; 601 p1 <- poly_put_coeffM x q i; 602 consM h p1 603 od 604 od 605 606*) 607 608(* Eliminate parenthesis around equality *) 609val _ = ParseExtras.tight_equality(); 610 611(* ------------------------------------------------------------------------- *) 612(* Helper Theorems *) 613(* ------------------------------------------------------------------------- *) 614 615(* for EVAL IFm *) 616val _ = computeLib.set_skip computeLib.the_compset ``ifM`` (SOME 1); 617(* EVAL IFm must be in current script, e.g. EVAL ``expn 1 2 3``; *) 618 619(* ------------------------------------------------------------------------- *) 620(* Computations in (ZN n)[X]/(unity k). *) 621(* ------------------------------------------------------------------------- *) 622 623(* Note: 624All polynomial computations are carried out in (MOD n, unity k). 625To simplify computations, the polynomials are not normalised, 626so they all have the same length k: 627 <---- k -----> 628poly modulus (unity k): 0 0 0 ... 0 0 | 1 629polynomial remainders: . . . ... . . 630 631Thus the little theory of ZN_unity_mod is based on weak polynomials. 632*) 633 634(* ------------------------------------------------------------------------- *) 635(* Polynomial Computations in monadic style. *) 636(* ------------------------------------------------------------------------- *) 637 638(* ------------------------------------------------------------------------- *) 639(* Making polynomials. *) 640(* ------------------------------------------------------------------------- *) 641 642(* Pseudocode: 643 Given a polynomial p, extend its length to k by prefix with 0. 644 list_extend p k: 645 if k = 0, return p // [] ++ p = p 646 q <- 0::p // prefix with 0 647 return list_extend q (k - 1) // extend result with (k - 1) 0 prefix 648*) 649 650(* Extend poly to length k. *) 651val poly_extendM_def = tDefine "poly_extendM" ` 652 poly_extendM p k = 653 do 654 k0 <- zeroM k; 655 if k0 then return p 656 else do 657 q <- consM 0 p; 658 j <- decM k; 659 poly_extendM q j; 660 od 661 od 662`(WF_REL_TAC `measure (\(p,k). k)` >> simp[]); 663 664(* 665> EVAL ``poly_extendM [] 7``; = ([0; 0; 0; 0; 0; 0; 0],Count 42): thm 666*) 667 668(* Pseudocode: 669 Extend |0| to length k. 670 list_zero k: 671 return list_extend [] k // starting with [] for list_extend 672*) 673 674(* Make |0| of length k *) 675val poly_zeroM_def = Define` 676 poly_zeroM (n:num) k = poly_extendM [] k 677`; 678 679(* Pseudocode: 680 Extend |1 (mod n)| to length k. 681 list_one n k: 682 if k = 0, return [] // [] has length = 0 683 t <- list_extend [] (k - 1) // extend |0| to length (k - 1) 684 return (1 (mod n))::t // put in the constant term 685*) 686 687(* Make |1| of length k *) 688val poly_oneM_def = Define` 689 poly_oneM n k = 690 do 691 k0 <- zeroM k; 692 if k0 then return [] 693 else do 694 j <- decM k; 695 p <- poly_zeroM n j; 696 c <- modM 1 n; (* gives 1 MOD 0 if n = 0 *) 697 consM c p; (* LENGTH is 1 + j = k *) 698 od 699 od 700`; 701(* Note: 702poly_oneM n k can be defined as (later) poly_constM n k 1, 703but then the theorems will have a prefix: 0 < n. 704It just happens that poly_constM theorems are still valid at n = 0 when c = 1. 705*) 706 707(* 708> EVAL ``poly_zeroM 10 7``; = ([0; 0; 0; 0; 0; 0; 0],Count 42): thm 709> EVAL ``poly_oneM 10 7``; = ([1; 0; 0; 0; 0; 0; 0], Count 46): thm 710> EVAL ``poly_oneM 0 7``; = ([1 MOD 0; 0; 0; 0; 0; 0; 0],Count 42): thm 711*) 712 713 714(* Theorem: valueOf (poly_extendM p k) = (unity_mod_zero (ZN n) k) ++ p *) 715(* Proof: 716 By induction from poly_extendM_def. 717 If k = 0, 718 valueOf (poly_extendM p 0) 719 = p by poly_extendM_def 720 = [] ++ p by APPEND 721 If k <> 0, 722 Let f = K 0. 723 valueOf (poly_extendM p k) 724 = valueOf (poly_extendM (0::p) (k - 1)) by poly_extendM_def 725 = unity_mod_zero (ZN n) (k - 1) ++ [0] ++ p by induction hypothesis 726 = PAD_RIGHT 0 (k - 1) [0] ++ [0] ++ p by unity_mod_zero_def, unity_mod_const_def, ZN_property 727 = SNOC 0 (PAD_RIGHT 0 (k - 1 [0])) ++ p by SNOC_APPEND 728 = PAD_RIGHT 0 SUC (k - 1) [0] ++ p by PAD_RIGHT_SNOC, 1 <= k 729 = PAD_RIGHT 0 k [0] ++ p by SUC (k - 1) = k, k <> 0 730 = unity_mod_zero (ZN n) k ++ p by unity_mod_zero_def, unity_mod_const_def, ZN_property 731*) 732val poly_extendM_value = store_thm( 733 "poly_extendM_value[simp]", 734 ``!n p k. valueOf (poly_extendM p k) = (unity_mod_zero (ZN n) k) ++ p``, 735 strip_tac >> 736 ho_match_mp_tac (theorem "poly_extendM_ind") >> 737 rw[] >> 738 (Cases_on `k = 0` >> rw[unity_mod_zero_def, unity_mod_const_def, ZN_property]) >- 739 rw[Once poly_extendM_def] >> 740 rw[Once poly_extendM_def, unity_mod_zero_def, unity_mod_const_def, ZN_property] >| [ 741 `k = 1` by decide_tac >> 742 rw[PAD_RIGHT], 743 `SUC (k - 1) = k` by decide_tac >> 744 `PAD_RIGHT 0 (k - 1) [0] ++ [0] = SNOC 0 (PAD_RIGHT 0 (k - 1) [0])` by rw[] >> 745 `_ = PAD_RIGHT 0 (SUC (k - 1)) [0]` by rw[PAD_RIGHT_SNOC] >> 746 metis_tac[] 747 ]); 748 749(* Theorem: valueOf (poly_extendM [] k) = unity_mod_zero (ZN n) k *) 750(* Proof: 751 valueOf (poly_extendM [] k) 752 = unity_mod_zero (ZN n) k ++ [] by poly_extendM_value 753 = unity_mod_zero (ZN n) k by APPEND_NIL 754*) 755val poly_extendM_nil = store_thm( 756 "poly_extendM_nil", 757 ``!n k. valueOf (poly_extendM [] k) = unity_mod_zero (ZN n) k``, 758 metis_tac[poly_extendM_value, APPEND_NIL]); 759 760(* Theorem: valueOf (poly_zeroM n k) = unity_mod_zero (ZN n) k *) 761(* Proof: 762 valueOf (poly_zeroM n k) 763 = valueOf (poly_extendM [] k) by poly_zeroM_def 764 = unity_mod_zero (ZN n) k ++ [] by poly_extendM_value 765 = unity_mod_zero (ZN n) k by APPEND_NIL 766*) 767val poly_zeroM_value = store_thm( 768 "poly_zeroM_value[simp]", 769 ``!n k. valueOf (poly_zeroM n k) = unity_mod_zero (ZN n) k``, 770 metis_tac[poly_zeroM_def, poly_extendM_value, APPEND_NIL]); 771 772(* Theorem: valueOf (poly_oneM n k) = unity_mod_one (ZN n) k *) 773(* Proof: 774 If k = 0, 775 valueOf (poly_oneM n 0) 776 = valueOf (return []) by poly_oneM_def, k = 0 777 = [] 778 = unity_mod_one (ZN n) 0 by unity_mod_one_def, unity_mod_const_def 779 If k = 1, 780 valueOf (poly_oneM n 1) 781 = 1::[] by unity_mod_zero_def, unity_mod_const_def, k = 1 782 = [1] by CONS 783 = unity_mod_one (ZN n) 1 by unity_mod_one_def, unity_mod_const_def, k = 1 784 If k <> 1, 785 Then 0 < k - 1, and SUC (k - 1) = k by arithmetic 786 valueOf (poly_oneM n k) 787 = 1 MOD n::valueOf (poly_zeroM n (k - 1)) by poly_oneM_def, 0 < k 788 = 1 MOD n::unity_mod_zero (ZN n) (k - 1) by poly_zeroM_value 789 790 Let c = (ZN n).sum.exp (ZN n).prod.id 1. 791 Then c = 1 MOD n by ZN_num_1 792 unity_mod_one (ZN n) k 793 = PAD_RIGHT 0 k [c] by unity_mod_one_def, unity_mod_const_def, ZN_property 794 = PAD_RIGHT 0 (SUC (k - 1)) (c::[]) by k = SUC (k - 1) 795 = c::PAD_RIGHT 0 (k - 1) [] by PAD_RIGHT_CONS 796 = c::PAD_RIGHT 0 (k - 1) [0] by PAD_RIGHT_NIL_EQ, 0 < k - 1 797 = c::unity_mod_zero (ZN n) (k - 1) by unity_mod_zero_def, unity_mod_const_def, ZN_property 798 Thus LHS = RHS. 799*) 800val poly_oneM_value = store_thm( 801 "poly_oneM_value[simp]", 802 ``!n k. valueOf (poly_oneM n k) = unity_mod_one (ZN n) k``, 803 rpt strip_tac >> 804 Cases_on `k = 0` >- 805 rw[poly_oneM_def, unity_mod_one_def, unity_mod_const_def] >> 806 rw[poly_oneM_def, unity_mod_one_def, unity_mod_const_def] >> 807 qabbrev_tac `c = (ZN n).sum.exp (ZN n).prod.id 1` >> 808 `c = 1 MOD n` by rw[ZN_num_1, Abbr`c`] >> 809 rw[ZN_property] >> 810 Cases_on `k = 1` >- 811 rw[unity_mod_zero_def, unity_mod_const_def, PAD_RIGHT] >> 812 `0 < k - 1` by decide_tac >> 813 `SUC (k - 1) = k` by decide_tac >> 814 qabbrev_tac `c = 1 MOD n` >> 815 `c::unity_mod_zero (ZN n) (k - 1) = c::PAD_RIGHT 0 (k - 1) [0]` by rw[unity_mod_zero_def, unity_mod_const_def, ZN_property] >> 816 `_ = c::PAD_RIGHT 0 (k - 1) []` by rw[PAD_RIGHT_NIL_EQ] >> 817 `_ = PAD_RIGHT 0 k [c]` by metis_tac[PAD_RIGHT_CONS] >> 818 rw[]); 819 820(* Theorem: 0 < n ==> Weak (ZN n) (valueOf (poly_zeroM n k)) *) 821(* Proof: 822 Weak (ZN n) (valueOf (poly_zeroM n k)) 823 = Weak (ZN n) (unity_mod_zero (ZN n) k) by poly_zeroM_value 824 = Weak (ZN n) (unity_mod_const (ZN n) k 0) by unity_mod_zero_def 825 = T by ZN_unity_mod_const_weak, 0 < n 826*) 827val poly_zeroM_weak = store_thm( 828 "poly_zeroM_weak", 829 ``!n k. 0 < n ==> Weak (ZN n) (valueOf (poly_zeroM n k))``, 830 rw[unity_mod_zero_def, ZN_unity_mod_const_weak]); 831 832(* Theorem: LENGTH (valueOf (poly_zeroM n k)) = k *) 833(* Proof: 834 LENGTH (valueOf (poly_zeroM n k)) 835 = LENGTH (unity_mod_zero (ZN n) k) by poly_zeroM_value 836 = k by unity_mod_zero_length 837*) 838val poly_zeroM_length = store_thm( 839 "poly_zeroM_length[simp]", 840 ``!n k. LENGTH (valueOf (poly_zeroM n k)) = k``, 841 rw[unity_mod_zero_length]); 842 843(* Theorem: 0 < n ==> Weak (ZN n) (valueOf (poly_oneM n k)) *) 844(* Proof: 845 Weak (ZN n) (valueOf (poly_oneM n k)) 846 = Weak (ZN n) (unity_mod_one (ZN n) k) by poly_oneM_value 847 = Weak (ZN n) (unity_mod_const (ZN n) k 1) by unity_mod_one_def 848 = T by ZN_unity_mod_const_weak, 0 < n 849*) 850val poly_oneM_weak = store_thm( 851 "poly_oneM_weak", 852 ``!n k. 0 < n ==> Weak (ZN n) (valueOf (poly_oneM n k))``, 853 rw[unity_mod_one_def, ZN_unity_mod_const_weak]); 854 855(* Theorem: LENGTH (valueOf (poly_oneM n k)) = k *) 856(* Proof: 857 LENGTH (valueOf (poly_oneM n k)) 858 = LENGTH (unity_mod_one (ZN n) k) by poly_oneM_value 859 = k by unity_mod_one_length 860*) 861val poly_oneM_length = store_thm( 862 "poly_oneM_length[simp]", 863 ``!n k. LENGTH (valueOf (poly_oneM n k)) = k``, 864 rw[unity_mod_one_length]); 865 866(* Theorem: stepsOf (poly_extendM p k) = 867 size k + if (k = 0) then 0 else 1 + size k + stepsOf (poly_extendM (0::p) (k - 1)) *) 868(* Proof: 869 stepsOf (poly_extendM p k) 870 = stepsOf (zeroM k) + if (k = 0) then 0 else 871 stepsOf (consM 0 p) + stepsOf (decM k) + 872 stepsOf (poly_extendM (0::p) (k - 1)) by poly_extendM_def 873 = size k + if (k = 0) then 0 else 1 + size k + stepsOf (poly_extendM (0::p) (k - 1)) 874*) 875val poly_extendM_steps_thm = store_thm( 876 "poly_extendM_steps_thm", 877 ``!p k. stepsOf (poly_extendM p k) = 878 size k + if (k = 0) then 0 else 1 + size k + stepsOf (poly_extendM (0::p) (k - 1))``, 879 ho_match_mp_tac (theorem "poly_extendM_ind") >> 880 (rw[] >> rw[Once poly_extendM_def])); 881 882(* Theorem: stepsOf (poly_extendM p k) = 883 if k = 0 then 1 else 1 + 2 * size k + stepsOf (poly_extendM (0::p) (k - 1)) *) 884(* Proof: 885 stepsOf (poly_extendM p k) 886 = size k + if (k = 0) then 0 887 else 1 + size k + stepsOf (poly_extendM (0::p) (k - 1)) by poly_extendM_steps_thm 888 = if k = 0 then size k 889 else 1 + 2 * size k + stepsOf (poly_extendM (0::p) (k - 1)) 890 = if k = 0 then 1 else 1 + 2 * size k + stepsOf (poly_extendM (0::p) (k - 1)) 891*) 892val poly_extendM_steps_by_dec_loop = store_thm( 893 "poly_extendM_steps_by_dec_loop", 894 ``!p k. stepsOf (poly_extendM p k) = 895 if k = 0 then 1 else 1 + 2 * size k + stepsOf (poly_extendM (0::p) (k - 1))``, 896 rw[Once poly_extendM_steps_thm]); 897 898(* 899This puts poly_extendM_steps in the category: decreasing loop with cons and body. 900 param_seekM_steps_by_inc_loop: 901 !p k. loop p k = if k = 0 then quit p else body p k + loop (0::p) (k - 1) 902suitable for: loop2_dec_count_eqn 903*) 904 905 906(* Theorem: stepsOf (poly_extendM p k) = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) *) 907(* Proof: 908 Let quit = (\p. 1), 909 body = (\p k. 1 + 2 * size k), 910 f = (\p. 0::p), 911 loop = (\p k. stepsOf (poly_extendM p k)). 912 913 Then !p k. loop p k = if k = 0 then quit p else body p k + loop (f p) (k - 1). 914 Let n = hop 1 k, 915 z = FUNPOW f n k, 916 g = (\j. 1 + 2 * size j). 917 Note n = hop 1 k = k by hop_1_n 918 loop p k 919 = quit z + 920 SUM (GENLIST (\j. body (FUNPOW f j p) (k - j * 1)) k) by loop2_dec_count_eqn 921 = 1 + SUM (GENLIST (\j. g (k - j)) k) by expanding body 922 = 1 + SUM (MAP g [1 .. k]) by SUM_GENLIST_REVERSE 923*) 924val poly_extendM_steps_eqn = store_thm( 925 "poly_extendM_steps_eqn", 926 ``!p k. stepsOf (poly_extendM p k) = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k])``, 927 rpt strip_tac >> 928 qabbrev_tac `quit = \p:num list. 1` >> 929 qabbrev_tac `f = \p. 0::p` >> 930 qabbrev_tac `g = \j. 1 + 2 * size j` >> 931 qabbrev_tac `body = \(p:num list) k. g k` >> 932 qabbrev_tac `loop = \p k. stepsOf (poly_extendM p k)` >> 933 `loop p k = 1 + SUM (MAP g [1 .. k])` suffices_by rw[] >> 934 `0 < 1` by decide_tac >> 935 `!p k. loop p k = if k = 0 then quit p else body p k + loop (f p) (k - 1)` by metis_tac[poly_extendM_steps_by_dec_loop] >> 936 imp_res_tac loop2_dec_count_eqn >> 937 first_x_assum (qspecl_then [`k`, `p`] strip_assume_tac) >> 938 qabbrev_tac `foo = !p k. loop p k = if k = 0 then quit p else body p k + loop (f p) (k - 1)` >> 939 fs[hop_1_n, SUM_GENLIST_REVERSE, Abbr`quit`, Abbr`body`]); 940 941(* This is the first explicit solution of count by sum, 942 showing stepsOf (poly_extendM p k) is independent of list p. *) 943 944(* Theorem: stepsOf (poly_extendM p k) <= 1 + k + 2 * k * size k *) 945(* Proof: 946 stepsOf (poly_extendM p k) 947 = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) by poly_extendM_steps_eqn 948 <= 1 + SUM (GELNLIST (K (1 + 2 * size k)) k) by SUM_LE, size_monotone_le 949 = 1 + (1 + 2 * size k) * k by SUM_GENLIST_K 950 = 1 + k + 2 * k * size k by RIGHT_ADD_DISTRIB 951 Or, 952 Using the same abbreviations as poly_extendM_steps_eqn, 953 with MONO g by size_monotone_le 954 loop p k 955 <= quit (FUNPOW f (hop 1 k) p) + hop 1 k * g k by loop2_dec_count_mono_le 956 = 1 + k * (1 + 2 * size k) by hop_1_n, expanding g 957 = 1 + k + 2 * k * size k by LEFT_ADD_DISTRIB 958*) 959val poly_extendM_steps_upper = store_thm( 960 "poly_extendM_steps_upper", 961 ``!p k. stepsOf (poly_extendM p k) <= 1 + k + 2 * k * size k``, 962 rpt strip_tac >> 963 qabbrev_tac `f = \j. 1 + 2 * size j` >> 964 qabbrev_tac `c = 1 + 2 * size k` >> 965 `stepsOf (poly_extendM p k) = 1 + SUM (MAP f [1 .. k])` by rw[poly_extendM_steps_eqn, Abbr`f`] >> 966 `SUM (MAP f [1 .. k]) <= SUM (GENLIST (K c) k)` by 967 (irule SUM_LE >> 968 `LENGTH [1 .. k] = k` by rw[listRangeINC_LEN] >> 969 rw[listRangeINC_EL, EL_MAP, EL_GENLIST, Abbr`f`, Abbr`c`] >> 970 rw[size_monotone_le]) >> 971 `SUM (GENLIST (K c) k) = c * k` by rw[SUM_GENLIST_K] >> 972 `c * k = (1 + 2 * size k) * k` by rw[Abbr`c`] >> 973 decide_tac); 974(* Direct proof is easier, rather than using loop2_dec_count_mono_le. *) 975 976(* Theorem: stepsOf (poly_extendM p k) <= 4 * (MAX 1 k) * size k *) 977(* Proof: 978 stepsOf (poly_extendM p k) 979 <= 1 + k + 2 * k * size k by poly_extendM_steps_upper 980 <= (1 + 1 + 2) * k * size k by dominant term 981 = 4 * k * size k 982 Use (MAX 1 k) to cater for k = 0. 983*) 984val poly_extendM_steps_bound = store_thm( 985 "poly_extendM_steps_bound", 986 ``!p k. stepsOf (poly_extendM p k) <= 4 * (MAX 1 k) * size k``, 987 rpt strip_tac >> 988 `stepsOf (poly_extendM p k) <= 1 + k + 2 * k * size k` by rw[poly_extendM_steps_upper] >> 989 qabbrev_tac `m = MAX 1 k` >> 990 qabbrev_tac `t = m * size k` >> 991 `stepsOf (poly_extendM p k) <= 4 * t` suffices_by rw[Abbr`t`] >> 992 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 993 `0 < t` by rw[MULT_POS, Abbr`t`] >> 994 `1 <= t` by decide_tac >> 995 `k <= t` by 996 (`m <= t` by rw[Abbr`t`] >> 997 decide_tac) >> 998 `k * size k <= t` by rw[Abbr`t`] >> 999 decide_tac); 1000 1001(* Theorem: stepsOf (poly_zeroM n k) = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) *) 1002(* Proof: 1003 stepsOf (poly_zeroM n k) 1004 = stepsOf (poly_extendM [] k) by poly_zeroM_def 1005 = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) by poly_extendM_steps_eqn 1006*) 1007val poly_zeroM_steps_eqn = store_thm( 1008 "poly_zeroM_steps_eqn", 1009 ``!n k. stepsOf (poly_zeroM n k) = 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k])``, 1010 rw[poly_zeroM_def, poly_extendM_steps_eqn]); 1011 1012(* Theorem: stepsOf (poly_zeroM n k) <= 1 + k + 2 * k * size k *) 1013(* Proof: 1014 stepsOf (poly_zeroM n k) 1015 = stepsOf (poly_extendM [] k) by poly_zeroM_def 1016 <= 1 + k + 2 * k * size k by poly_extendM_steps_upper 1017*) 1018val poly_zeroM_steps_upper = store_thm( 1019 "poly_zeroM_steps_upper", 1020 ``!n k. stepsOf (poly_zeroM n k) <= 1 + k + 2 * k * size k``, 1021 rw_tac std_ss[poly_zeroM_def, poly_extendM_steps_upper]); 1022 1023(* Theorem: stepsOf (poly_zeroM n k) <= 4 * MAX 1 k * size k *) 1024(* Proof: 1025 stepsOf (poly_zeroM n k) 1026 = stepsOf (poly_extendM [] k) by poly_zeroM_def 1027 <= 4 * MAX 1 k * size k by poly_extendM_steps_bound 1028*) 1029val poly_zeroM_steps_bound = store_thm( 1030 "poly_zeroM_steps_bound", 1031 ``!n k. stepsOf (poly_zeroM n k) <= 4 * MAX 1 k * size k``, 1032 rw_tac std_ss[poly_zeroM_def, poly_extendM_steps_bound]); 1033 1034(* Theorem: stepsOf (poly_oneM n k) = 1035 if k = 0 then 1 1036 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size n *) 1037(* Proof: 1038 stepsOf (poly_oneM n k) 1039 = stepsOf (zeroM k) + if k = 0 then 0 1040 else stepsOf (decM k) + 1041 stepsOf (poly_zeroM n (k - 1)) + 1042 stepsOf (modM 1 n) + 1043 stepsOf (consM (1 MOD n) (unity_mod_zero (ZN n) k)) by poly_oneM_def 1044 = size k + if k = 0 then 0 1045 else size k + (1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. (k - 1)])) + 1046 (size 1 * size n) + 1 by poly_zeroM_steps_eqn 1047 = if k = 0 then 1 1048 else 1 + (1 + 2 * size k) + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size n 1049 by size_0, moving last 1 to front 1050 = if k = 0 then 1 1051 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size n 1052 by listRangeINC_SUM_MAP 1053*) 1054val poly_oneM_steps_eqn = store_thm( 1055 "poly_oneM_steps_eqn", 1056 ``!n k. stepsOf (poly_oneM n k) = 1057 if k = 0 then 1 1058 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size n``, 1059 rpt strip_tac >> 1060 (Cases_on `k = 0` >> simp[]) >- 1061 rw[poly_oneM_def] >> 1062 simp[poly_oneM_def, poly_zeroM_steps_eqn] >> 1063 qabbrev_tac `f = \j. 2 * size j + 1` >> 1064 `SUC (k - 1) = k` by decide_tac >> 1065 `SUM (MAP f [1 .. k]) = f k + SUM (MAP f [1 .. (k - 1)])` by metis_tac[listRangeINC_SUM_MAP, ADD1] >> 1066 `f k = 2 * size k + 1` by rw[Abbr`f`] >> 1067 decide_tac); 1068 1069(* Theorem: stepsOf (poly_oneM n k) <= 1 + k + 2 * size k + 2 * k * size k + size n *) 1070(* Proof: 1071 stepsOf (poly_oneM n k) 1072 = stepsOf (zeroM k) + if k = 0 then 0 1073 else stepsOf (decM k) + 1074 stepsOf (poly_zeroM n (k - 1)) + 1075 stepsOf (modM 1 n) + 1076 stepsOf (consM (1 MOD n) (unity_mod_zero (ZN n) k)) by poly_oneM_def 1077 <= size k + if k = 0 then 0 1078 else size k + (1 + (k - 1) + 2 * (k - 1) * size (k - 1)) + 1079 (size 1 * size n) + 1 by poly_zeroM_steps_upper 1080 <= size k + size k + k + 2 * k * size k + size n + 1 by size_1, size_monotone_lt 1081 = 1 + k + 2 * size k + 2 * k * size k + size n 1082*) 1083val poly_oneM_steps_upper = store_thm( 1084 "poly_oneM_steps_upper", 1085 ``!n k. stepsOf (poly_oneM n k) <= 1 + k + 2 * size k + 2 * k * size k + size n``, 1086 rw[poly_oneM_def] >> 1087 `stepsOf (poly_zeroM n (k - 1)) <= 1 + (k - 1) + 2 * (k - 1) * size (k - 1)` by rw[poly_zeroM_steps_upper] >> 1088 `1 + (k - 1) = k` by decide_tac >> 1089 `size (k - 1) <= size k` by rw[size_monotone_lt] >> 1090 `2 * (k - 1) * size (k - 1) <= 2 * k * size k` by rw[LE_MONO_MULT2] >> 1091 decide_tac); 1092 1093(* Theorem: stepsOf (poly_oneM n k) <= 7 * (MAX 1 k) * size k * size n *) 1094(* Proof: 1095 stepsOf (poly_oneM n k) 1096 <= 1 + k + 2 * size k + 2 * k * size k + size n by poly_oneM_steps_upper 1097 <= (1 + 1 + 2 + 2 + 1) * k * size k * size n by dominant term 1098 = 7 * k * size k * size n 1099 Use (MAX 1 k) to cater for k = 0. 1100*) 1101val poly_oneM_steps_bound = store_thm( 1102 "poly_oneM_steps_bound", 1103 ``!n k. stepsOf (poly_oneM n k) <= 7 * (MAX 1 k) * size k * size n``, 1104 rpt strip_tac >> 1105 `stepsOf (poly_oneM n k) <= 1 + k + 2 * size k + 2 * k * size k + size n` by rw[poly_oneM_steps_upper] >> 1106 qabbrev_tac `m = MAX 1 k` >> 1107 qabbrev_tac `t = m * size k * size n` >> 1108 `stepsOf (poly_oneM n k) <= 7 * t` suffices_by rw[Abbr`t`] >> 1109 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 1110 `0 < t` by rw[MULT_POS, Abbr`t`] >> 1111 `1 <= t` by decide_tac >> 1112 `k <= t` by 1113 (`0 < size k * size n` by rw[MULT_POS] >> 1114 `m <= m * (size k * size n)` by rw[] >> 1115 `m * (size k * size n) = t` by rw[Abbr`t`] >> 1116 decide_tac) >> 1117 `size k <= t` by 1118 (`0 < m * size n` by rw[MULT_POS] >> 1119 `size k <= size k * (m * size n)` by rw[] >> 1120 `size k * (m * size n) = t` by rw[Abbr`t`] >> 1121 decide_tac) >> 1122 `size n <= t` by 1123 (`0 < m * size k` by rw[MULT_POS] >> 1124 `size n <= size n * (m * size k)` by rw[] >> 1125 `size n * (m * size k) = t` by rw[Abbr`t`] >> 1126 decide_tac) >> 1127 `k * size k <= t` by 1128 (`0 < size n` by rw[] >> 1129 `k * size k <= m * size k` by rw[] >> 1130 `m * size k <= m * size k * size n` by rw[] >> 1131 `m * size k * size n = t` by rw[Abbr`t`] >> 1132 decide_tac) >> 1133 decide_tac); 1134 1135(* ------------------------------------------------------------------------- *) 1136(* Constant Polynomial *) 1137(* ------------------------------------------------------------------------- *) 1138 1139(* Pseudocode: 1140 Given modulus n and constant c, make |c MOD n| to length k. 1141 list_const k c: 1142 if k = 0, return [] // [] has length 0 1143 t <- list_zero (k - 1) // extend [] to length (k - 1) 1144 return (c MOD n)::t // put in constant term 1145*) 1146 1147(* Make c (MOD n, (unity k)) of length k. *) 1148val poly_constM_def = Define` 1149 poly_constM n k c = 1150 do 1151 (* k = 0 will give length = 0 *) 1152 k0 <- zeroM k; 1153 if k0 then return [] 1154 else do 1155 j <- decM k; 1156 p <- poly_zeroM n j; 1157 d <- modM c n; 1158 consM d p; (* the c MOD n, LENGTH 1 + j = k *) 1159 od 1160 od 1161`; 1162 1163(* 1164> EVAL ``poly_constM 10 7 13``; = ([3; 0; 0; 0; 0; 0; 0],Count 58): thm 1165> EVAL ``poly_constM 10 0 13``; = ([],Count 1): thm 1166> EVAL ``poly_constM 10 1 13``; = ([3],Count 20): thm 1167> EVAL ``unity_mod_const (ZN 10) 7 13``; = [3; 0; 0; 0; 0; 0; 0]: thm 1168> EVAL ``unity_mod_const (ZN 10) 0 13``; = []: thm 1169> EVAL ``unity_mod_const (ZN 10) 1 13``; = [3]: thm 1170*) 1171 1172 1173(* Theorem: 0 < n ==> (valueOf (poly_constM n k c) = unity_mod_const (ZN n) k c) *) 1174(* Proof: 1175 If k = 0 1176 valueOf (poly_constM n 0 c) 1177 = [] by poly_constM_def 1178 = unity_mod_const (ZN n) 0 c by unity_mod_const_def, k = 0 1179 If k <> 0, 1180 valueOf (poly_constM n k c) 1181 = (c MOD n)::valueOf (poly_zeroM n (k - 1)) by poly_constM_def 1182 = (c MOD n)::unity_mod_zero (ZN n) (k - 1) by poly_zeroM_value 1183 = (c MOD n)::PAD_RIGHT 0 (k - 1) [] by unity_mod_zero_alt, ZN_property 1184 = PAD_RIGHT 0 k [c MOD n] by PAD_RIGHT_CONS 1185 = PAD_RIGHT (ZN n).sum.id k [(ZN n).sum.exp (ZN n).prod.id c] by ZN_num_mod 1186 = unity_mod_const (ZN n) k c by unity_mod_const_def, k <> 0 1187*) 1188val poly_constM_value = store_thm( 1189 "poly_constM_value[simp]", 1190 ``!n k c. 0 < n ==> (valueOf (poly_constM n k c) = unity_mod_const (ZN n) k c)``, 1191 rw[poly_constM_def] >- 1192 rw[unity_mod_const_def] >> 1193 `SUC (k - 1) = k` by decide_tac >> 1194 `(c MOD n)::unity_mod_zero (ZN n) (k - 1) = (c MOD n)::(PAD_RIGHT 0 (k - 1) [])` by rw[unity_mod_zero_alt, ZN_property] >> 1195 `_ = PAD_RIGHT 0 k [c MOD n]` by rw[PAD_RIGHT_CONS] >> 1196 `_ = PAD_RIGHT (ZN n).sum.id k [(ZN n).sum.exp (ZN n).prod.id c]` by rw[ZN_num_mod, ZN_property] >> 1197 `_ = unity_mod_const (ZN n) k c` by rw[unity_mod_const_def] >> 1198 rw[]); 1199 1200 1201(* Theorem: valueOf (poly_constM 0 k c) = if k = 0 then [] else PAD_RIGHT 0 k [c MOD 0] *) 1202(* Proof: 1203 If k = 0, 1204 valueOf (poly_constM 0 k c) = [] by poly_constM_def 1205 If k <> 0, 1206 Let x = c MOD 0, 1207 = c MOD 0 :: valueOf (poly_zeroM n (k - 1)) by poly_constM_def 1208 = c MOD 0 :: unity_mod_zero (ZN n) (k - 1) by poly_zeroM_value 1209 = c MOD 0 :: PAD_RIGHT 0 k [] by unity_mod_zero_alt, ZN_property 1210 = PAD_RIGHT k [c MOD 0] by PAD_RIGHT_CONS 1211*) 1212val poly_constM_zero = store_thm( 1213 "poly_constM_zero", 1214 ``!k c. valueOf (poly_constM 0 k c) = if k = 0 then [] else PAD_RIGHT 0 k [c MOD 0]``, 1215 rw[poly_constM_def, unity_mod_zero_alt, ZN_property] >> 1216 `SUC (k - 1) = k` by decide_tac >> 1217 rw[PAD_RIGHT_CONS]); 1218 1219(* Theorem: 0 < n ==> Weak (ZN n) (valueOf (poly_constM n k c)) *) 1220(* Proof: 1221 Weak (ZN n) (valueOf (poly_constM n k c)) 1222 = Weak (ZN n) (unity_mod_const (ZN n) k c) by poly_constM_value 1223 = T by ZN_unity_mod_const_weak 1224*) 1225val poly_constM_weak = store_thm( 1226 "poly_constM_weak", 1227 ``!n k c. 0 < n ==> Weak (ZN n) (valueOf (poly_constM n k c))``, 1228 rw[ZN_unity_mod_const_weak]); 1229 1230(* Theorem: LENGTH (valueOf (poly_constM n k c)) = k *) 1231(* Proof: 1232 If n = 0, 1233 LENGTH (valueOf (poly_constM 0 k c)) 1234 = LENGTH (if k = 0 then [] else PAD_RIGHT 0 k [c MOD 0])) 1235 by poly_constM_zero 1236 = if k = 0 then 0 else LENGTH (PAD_RIGHT 0 k [c MOD 0]) 1237 = if k = 0 then 0 else MAX k 1 by PAD_RIGHT_LENGTH 1238 = if k = 0 then 0 else k by k <> 0, MAX_DEF 1239 = k 1240 If n <> 0, 1241 LENGTH (valueOf (poly_constM n k c)) 1242 = LENGTH (unity_mod_const (ZN n) k c)) by poly_constM_value, 0 < n 1243 = k by unity_mod_const_length 1244*) 1245val poly_constM_length = store_thm( 1246 "poly_constM_length[simp]", 1247 ``!n k c. LENGTH (valueOf (poly_constM n k c)) = k``, 1248 rpt strip_tac >> 1249 Cases_on `n = 0` >- 1250 rw[poly_constM_zero, PAD_RIGHT_LENGTH, MAX_DEF] >> 1251 rw[poly_constM_value, unity_mod_const_length]); 1252 1253(* Theorem: stepsOf (poly_constM n k c) = 1254 if k = 0 then 1 1255 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size c * size n *) 1256(* Proof: 1257 stepsOf (poly_constM n k c) 1258 = stepsOf (zeroM k) + if k = 0 then 0 1259 else stepsOf (decM k) + 1260 stepsOf (poly_zeroM n (k - 1)) + 1261 stepsOf (modM c n) + 1262 stepsOf (consM (c MOD n) (unity_mod_zero (ZN n) (k - 1))) 1263 by poly_constM_def 1264 = size k + if k = 0 then 0 1265 else size k + (1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. (k - 1)])) + 1266 (size c * size n) + 1 by poly_zeroM_steps_eqn 1267 = if k = 0 then 1 1268 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size c * size n 1269*) 1270val poly_constM_steps_eqn = store_thm( 1271 "poly_constM_steps_eqn", 1272 ``!n k c. stepsOf (poly_constM n k c) = 1273 if k = 0 then 1 1274 else 1 + SUM (MAP (\j. 1 + 2 * size j) [1 .. k]) + size c * size n``, 1275 rpt strip_tac >> 1276 (Cases_on `k = 0` >> simp[]) >- 1277 rw[poly_constM_def] >> 1278 simp[poly_constM_def, poly_zeroM_steps_eqn] >> 1279 qabbrev_tac `f = \j. 2 * size j + 1` >> 1280 `SUC (k - 1) = k` by decide_tac >> 1281 `SUM (MAP f [1 .. k]) = f k + SUM (MAP f [1 .. (k - 1)])` by metis_tac[listRangeINC_SUM_MAP, ADD1] >> 1282 `f k = 2 * size k + 1` by rw[Abbr`f`] >> 1283 decide_tac); 1284 1285(* Theorem: stepsOf (poly_constM n k c) <= 1 + k + 2 * size k + 2 * k * size k + size c * size n *) 1286(* Proof: 1287 stepsOf (poly_constM n k c) 1288 = stepsOf (zeroM k) + if k = 0 then 0 1289 else stepsOf (decM k) + 1290 stepsOf (poly_zeroM n (k - 1)) + 1291 stepsOf (modM c n) + 1292 stepsOf (consM (c MOD n) (unity_mod_zero (ZN n) (k - 1))) 1293 by poly_constM_def 1294 <= size k + if k = 0 then 0 1295 else size k + (1 + (k - 1) + 2 * (k - 1) * size (k - 1)) + 1296 (size c * size n) + 1 by poly_zeroM_steps_upper 1297 = size k + size k + k + 2 * k * size k + size c * size n + 1 by size_monotone_lt 1298 = 1 + k + 2 * size k + 2 * k * size k + size c * size n 1299*) 1300val poly_constM_steps_upper = store_thm( 1301 "poly_constM_steps_upper", 1302 ``!n k c. stepsOf (poly_constM n k c) <= 1 + k + 2 * size k + 2 * k * size k + size c * size n``, 1303 rw[poly_constM_def] >> 1304 `stepsOf (poly_zeroM n (k - 1)) <= 1 + (k - 1) + 2 * (k - 1) * size (k - 1)` by rw[poly_zeroM_steps_upper] >> 1305 `1 + (k - 1) = k` by decide_tac >> 1306 `size (k - 1) <= size k` by rw[size_monotone_lt] >> 1307 `2 * (k - 1) * size (k - 1) <= 2 * k * size k` by rw[LE_MONO_MULT2] >> 1308 decide_tac); 1309 1310(* Theorem: stepsOf (poly_constM n k c) <= 7 * (MAX 1 k) * size k * size c * size n *) 1311(* Proof: 1312 stepsOf (poly_constM n k c) 1313 <= 1 + k + 2 * size k + 2 * k * size k + size c * size n by poly_constM_steps_upper 1314 <= (1 + 1 + 2 + 2 + 1) * k * size k * size c * size n by dominant term 1315 = 7 * k * size k * size c * size n 1316 Use (MAX 1 k) to cater for k = 0. 1317*) 1318val poly_constM_steps_bound = store_thm( 1319 "poly_constM_steps_bound", 1320 ``!n k c. stepsOf (poly_constM n k c) <= 7 * (MAX 1 k) * size k * size c * size n``, 1321 rpt strip_tac >> 1322 `stepsOf (poly_constM n k c) <= 1 + k + 2 * size k + 2 * k * size k + size c * size n` by rw[poly_constM_steps_upper] >> 1323 qabbrev_tac `m = MAX 1 k` >> 1324 qabbrev_tac `t = m * size k * size c * size n` >> 1325 `stepsOf (poly_constM n k c) <= 7 * t` suffices_by rw[Abbr`t`] >> 1326 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 1327 `0 < t` by rw[MULT_POS, Abbr`t`] >> 1328 `1 <= t` by decide_tac >> 1329 `k <= t` by 1330 (`0 < size k * size c * size n` by rw[MULT_POS] >> 1331 `m <= m * (size k * size c * size n)` by rw[] >> 1332 `m * (size k * size c * size n) = t` by rw[Abbr`t`] >> 1333 decide_tac) >> 1334 `size k <= t` by 1335 (`0 < m * size c * size n` by rw[MULT_POS] >> 1336 `size k <= size k * (m * size c * size n)` by rw[] >> 1337 `size k * (m * size c * size n) = t` by rw[Abbr`t`] >> 1338 decide_tac) >> 1339 `k * size k <= t` by 1340 (`0 < size c * size n` by rw[MULT_POS] >> 1341 `k * size k <= m * size k` by rw[] >> 1342 `m * size k <= m * size k * (size c * size n)` by rw[] >> 1343 `m * size k * (size c * size n) = t` by rw[Abbr`t`] >> 1344 decide_tac) >> 1345 `size c * size n <= t` by 1346 (`0 < m * size k` by rw[MULT_POS] >> 1347 `size c * size n <= size c * size n * (m * size k)` by rw[] >> 1348 `size c * size n * (m * size k) = t` by rw[Abbr`t`] >> 1349 decide_tac) >> 1350 decide_tac); 1351 1352(* ------------------------------------------------------------------------- *) 1353(* Powers of X *) 1354(* ------------------------------------------------------------------------- *) 1355 1356(* Make X ** m (MOD n, (unity k)) of length k. *) 1357(* For X ** 1 = X, this is [0,1,0,...0] if k > 1, [1] if k = 1, [] if k = 0. *) 1358(* For X ** m, this is [0,0,..1,0,...0] if k > 1, the 1 at (m MOD k), 1359 <----------k--> 1360 <---(m MOD k)-> 1361 [1] if k = 1, due to (m MOD 1 = 0) by MOD_1, 1362 [] if k = 0, to keep length = k, always for making polynomials. 1363*) 1364 1365(* Pseudocode: 1366 Given modulus n, compute (X ** m) (mod n, unity k). 1367 list_Xexp k m: 1368 if k = 0, return [] // [] has length 0 1369 if k = 1, return [1 MOD n] // degenerate case 1370 j <- m MOD k // prefix zeroes in the list 1371 i <- k - (m MOD k) - 1 // suffix zeroes in the list 1372 p <- list_extend [] i // all the suffix zeroes 1373 q <- (1 MOD n):: p // put in the X 1374 return list_extend q j // extend with preceding zeroes 1375*) 1376 1377val poly_X_expM_def = Define` 1378 poly_X_expM n k m = 1379 do 1380 k0 <- zeroM k; 1381 if k0 then return [] 1382 else do 1383 c <- modM 1 n; (* coefficient of X *) 1384 k1 <- oneM k; 1385 if k1 then consM c [] 1386 else do 1387 j <- modM m k; (* j = m MOD k, the index of X. *) 1388 h <- subM k j; 1389 i <- decM h; (* number of leading zero = k - m MOD k - 1 *) 1390 p <- poly_zeroM n i; 1391 q <- consM c p; (* the X *) 1392 poly_extendM q j; (* j = number of after zero = m MOD k *) 1393 od 1394 od 1395 od 1396`; 1397 1398(* 1399> EVAL ``poly_X_expM 10 7 2``; = ([0; 0; 1; 0; 0; 0; 0],Count 53): thm 1400> EVAL ``poly_X_expM 10 7 0``; = ([1; 0; 0; 0; 0; 0; 0],Count 56): thm 1401> EVAL ``poly_X_expM 10 0 0``; = ([],Count 1): thm 1402> EVAL ``poly_X_expM 10 1 0``; = ([1],Count 7): thm 1403> EVAL ``poly_X_expM 10 7 3``; = ([0; 0; 0; 1; 0; 0; 0],Count 51): thm 1404> EVAL ``poly_X_expM 10 7 4``; = ([0; 0; 0; 0; 1; 0; 0],Count 55): thm 1405> EVAL ``poly_X_expM 10 7 5``; = ([0; 0; 0; 0; 0; 1; 0],Count 57): thm 1406> EVAL ``poly_X_expM 10 7 6``; = ([0; 0; 0; 0; 0; 0; 1],Count 60): thm 1407> EVAL ``poly_X_expM 10 7 7``; = ([1; 0; 0; 0; 0; 0; 0],Count 62): thm 1408 1409> EVAL ``unity_mod_special (ZN 10) 7 2 0``; = [0; 0; 1; 0; 0; 0; 0]: thm 1410> EVAL ``unity_mod_special (ZN 10) 7 0 0``; = [1; 0; 0; 0; 0; 0; 0]: thm 1411> EVAL ``unity_mod_special (ZN 10) 0 0 0``; = []: thm 1412> EVAL ``unity_mod_special (ZN 10) 1 0 0``; = [1]: thm 1413> EVAL ``unity_mod_special (ZN 10) 7 3 0``; = [0; 0; 0; 1; 0; 0; 0]: thm 1414> EVAL ``unity_mod_special (ZN 10) 7 4 0``; = [0; 0; 0; 0; 1; 0; 0]: thm 1415> EVAL ``unity_mod_special (ZN 10) 7 5 0``; = [0; 0; 0; 0; 0; 1; 0]: thm 1416> EVAL ``unity_mod_special (ZN 10) 7 6 0``; = [0; 0; 0; 0; 0; 0; 1]: thm 1417> EVAL ``unity_mod_special (ZN 10) 7 7 0``; = [1; 0; 0; 0; 0; 0; 0]: thm 1418 1419> EVAL ``poly_X_expM 0 7 2``; = ([0; 0; 1 MOD 0; 0; 0; 0; 0],Count 49): thm 1420> EVAL ``unity_mod_special (ZN 0) 7 2 0``; = [0; 0; 1; 0; 0; 0; 0]: thm 1421*) 1422 1423(* Theorem: 0 < n ==> (valueOf (poly_X_expM n k m) = unity_mod_X_exp (ZN n) k m) *) 1424(* Proof: 1425 If k = 0, 1426 valueOf (poly_X_expM n 0 m) 1427 = [] by poly_X_expM_def 1428 = |0| by poly_zero 1429 = unity_mod_X_exp (ZN n) 0 m by unity_mod_X_exp_0_n 1430 If k = 1, 1431 valueOf (poly_X_expM n 1 m) 1432 = [1 MOD n] by poly_X_expM_def 1433 = [(ZN n).sum.exp (ZN n).prod.id 1] by ZN_num_1 1434 = unity_mod_X_exp (ZN n) 1 m by unity_mod_X_exp_1_n 1435 Otherwise, 1436 Let c = 1 MOD n, h = m MOD k, 1437 ls = c::unity_mod_zero (ZN n) (k - (h + 1)). 1438 valueOf (poly_X_expM n k m) 1439 = valueOf (poly_extendM ls h) by poly_X_expM_def 1440 If h = 0, 1441 valueOf (poly_extendM ls 0) 1442 = unity_mod_zero (ZN n) 0 ++ ls by poly_extendM_value 1443 = |0| ++ ls = ls by unity_mod_zero_def, unity_mod_const_def, h = 0 1444 = c::unity_mod_zero (ZN n) (k - 1) by expanding ls, h = 0 1445 = c::PAD_RIGHT 0 (k - 1) [0] by unity_mod_zero_def, unity_mod_const_def, ZN_property 1446 = c::PAD_RIGHT 0 (k - 1) [] by PAD_RIGHT_NIL_EQ 1447 = PAD_RIGHT 0 (SUC (k - 1)) [c] by PAD_RIGHT_CONS 1448 = PAD_RIGHT 0 k [c] by SUC (k - 1) = k, 0 < k 1449 = unity_mod_special (ZN n) k m 0 by unity_mod_special_def, h = 0 1450 = unity_mod_X_exp (ZN n) k m by unity_mod_X_exp_def 1451 1452 If h <> 0, 1453 valueOf (poly_extendM ls h) 1454 = unity_mod_zero (ZN n) h ++ ls by poly_extendM_value 1455 = PAD_RIGHT 0 h [0] ++ ls by unity_mod_zero_def, unity_mod_const_def, ZN_property 1456 1457 unity_mod_X_exp (ZN n) k m 1458 = unity_mod_special (ZN n) k m 0 by unity_mod_X_exp_def 1459 = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [if n = 1 then 0 else 1]) 1460 by unity_mod_special_def, ZN_property 1461 = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [c]) by c = (if n = 1 then 0 else 1), by ONE_MOD, 0 < n. 1462 1463 Note h < k by MOD_LESS, 0 < n 1464 or h + 1 <= k by arithmetic 1465 If h + 1 = k, 1466 ls = c::unity_mod_zero (ZN n) 0 1467 = c::[] = [c] by unity_mod_zero_def, unity_mod_const_def 1468 This is to show: 1469 PAD_RIGHT 0 h [0] ++ [c] = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [c]) 1470 PAD_RIGHT 0 h [0] ++ [c] 1471 = [0] ++ GENLIST (K 0) (h - 1) ++ [c] by PAD_RIGHT 1472 = [0] ++ PAD_LEFT 0 h [c] by PAD_LEFT 1473 = 0::PAD_LEFT 0 h [c] by CONS_APPEND 1474 = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [c]) by LENGTH (0::PAD_LEFT 0 h [c]) = k 1475 If h + 1 < k, 1476 Let z = k - (h + 1). 1477 ls = c::unity_mod_zero (ZN n) z 1478 = c::PAD_RIGHT 0 z [0] by unity_mod_zero_def, unity_mod_const_def 1479 This is to show: 1480 PAD_RIGHT 0 h [0] ++ c::PAD_RIGHT 0 z [0] = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [c]) 1481 PAD_RIGHT 0 h [0] ++ c::PAD_RIGHT 0 z [0] 1482 = [0] ++ GENLIST (K 0) (h - 1) ++ [c] ++ 0::GENLIST (K 0) (z - 1) by PAD_RIGHT 1483 = 0::PAD_LEFT (K 0) h [c] ++ 0::GENLIST (K 0) (z - 1) by PAD_LEFT 1484 = 0::PAD_LEFT (K 0) h [c] ++ GENLIST (K 0) z by GENLIST_K_CONS 1485 = PAD_RIGHT 0 (z + (h + 1)) (0::PAD_LEFT 0 h [c]) by PAD_RIGHT, LENGTH (0::PAD_LEFT 0 h [c]) = h + 1 1486 = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [c]) by k = z + (h + 1) 1487*) 1488val poly_X_expM_value = store_thm( 1489 "poly_X_expM_value[simp]", 1490 ``!n k m. 0 < n ==> (valueOf (poly_X_expM n k m) = unity_mod_X_exp (ZN n) k m)``, 1491 rw[poly_X_expM_def] >- 1492 rw[unity_mod_X_exp_0_n] >> 1493 (Cases_on `k = 1` >> simp[]) >- 1494 rw[unity_mod_X_exp_1_n, ZN_num_1] >> 1495 qabbrev_tac `c = 1 MOD n` >> 1496 qabbrev_tac `h = m MOD k` >> 1497 qabbrev_tac `ls = c::unity_mod_zero (ZN n) (k - (h + 1))` >> 1498 (Cases_on `h = 0` >> simp[]) >| [ 1499 `valueOf (poly_extendM ls 0) = unity_mod_zero (ZN n) 0 ++ ls` by rw[poly_extendM_value] >> 1500 `_ = ls` by rw[unity_mod_zero_def, unity_mod_const_def] >> 1501 `unity_mod_X_exp (ZN n) k m = unity_mod_special (ZN n) k m 0` by rw[unity_mod_X_exp_def] >> 1502 `_ = PAD_RIGHT 0 k [(if n = 1 then 0 else 1) MOD n]` by rw[unity_mod_special_def, ZN_property] >> 1503 `(if n = 1 then 0 else 1) MOD n = c` by rw[Abbr`c`] >> 1504 rfs[unity_mod_zero_def, unity_mod_const_def, ZN_property, Abbr`ls`] >> 1505 `SUC (k - 1) = k` by decide_tac >> 1506 `1 <= k - 1` by decide_tac >> 1507 `c::PAD_RIGHT 0 (k - 1) [0] = c::PAD_RIGHT 0 (k - 1) []` by rw[PAD_RIGHT_NIL_EQ] >> 1508 `_ = PAD_RIGHT 0 k [c]` by rw[PAD_RIGHT_CONS] >> 1509 rw[], 1510 `valueOf (poly_extendM ls h) = unity_mod_zero (ZN n) h ++ ls` by rw[poly_extendM_value] >> 1511 `_ = PAD_RIGHT 0 h [0] ++ ls` by rw[unity_mod_zero_def, unity_mod_const_def, ZN_property] >> 1512 `unity_mod_X_exp (ZN n) k m = unity_mod_special (ZN n) k m 0` by rw[unity_mod_X_exp_def] >> 1513 `_ = PAD_RIGHT 0 k (0::PAD_LEFT 0 h [if n = 1 then 0 else 1])` by rw[unity_mod_special_def, ZN_property] >> 1514 `(if n = 1 then 0 else 1) = c` by rw[Abbr`c`] >> 1515 rfs[unity_mod_zero_def, unity_mod_const_def, ZN_property, Abbr`ls`] >> 1516 `h < k` by rw[Abbr`h`] >> 1517 `h + 1 <= k` by decide_tac >> 1518 (Cases_on `k <= h + 1` >> simp[]) >| [ 1519 `k = h + 1` by decide_tac >> 1520 rw[PAD_LEFT, PAD_RIGHT, ADD1], 1521 rw[PAD_LEFT, PAD_RIGHT] >> 1522 `SUC (k - (h + 2)) = k - SUC h` by decide_tac >> 1523 metis_tac[GENLIST_K_CONS] 1524 ] 1525 ]); 1526 1527 1528(* Theorem: valueOf (poly_X_expM 0 k m) = 1529 if k = 0 then [] else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0]) *) 1530(* Proof: 1531 Let x = 1 MOD n. 1532 If k = 0, 1533 valueOf (poly_X_expM 0 0 m) 1534 = [] by poly_X_expM_def 1535 If k = 1, 1536 Then m MOD 1 = 0 by MOD_1 1537 valueOf (poly_X_expM 0 1 m) 1538 = [x] by poly_X_expM_def 1539 = PAD_RIGHT 0 1 [x] by PAD_RIGHT 1540 = PAD_RIGHT 0 1 (PAD_LEFT 0 1 [x]) by PAD_LEFT 1541 Otherwise, 1542 Let ls = unity_mod_zero (ZN 0) (k - (m MOD k + 1)). 1543 valueOf (poly_X_expM 0 k m) 1544 = valueOf (poly_extendM (x::ls) (m MOD k)) by poly_X_expM_def, poly_zeroM_value 1545 = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls) by poly_extendM_value 1546 = unity_mod_zero (ZN n) (m MOD k) ++ [x] ++ ls by CONS_APPEND 1547 = PAD_RIGHT 0 (m MOD k) [] ++ [x] ++ ls by unity_mod_zero_alt, ZN_property 1548 = PAD_LEFT 0 (m MOD k + 1) [x] ++ ls by PAD_LEFT_BY_RIGHT 1549 = lt ++ unity_mod_zero (ZN 0) (k - (m MOD k + 1)) where lt = PAD_LEFT 0 (m MOD k + 1) [x] 1550 = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) [] by by unity_mod_zero_alt, ZN_property 1551 = PAD_RIGHT 0 k lt by PAD_RIGHT_BY_RIGHT, LENGTH lt = (m MOD k) + 1 1552 = PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0]) 1553*) 1554val poly_X_expM_zero = store_thm( 1555 "poly_X_expM_zero", 1556 ``!k m. valueOf (poly_X_expM 0 k m) = 1557 if k = 0 then [] else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0])``, 1558 rpt strip_tac >> 1559 Cases_on `k <= 1` >| [ 1560 `k = 0 \/ k = 1` by decide_tac >- 1561 rw[poly_X_expM_def] >> 1562 rw[poly_X_expM_def, PAD_LEFT, PAD_RIGHT], 1563 rw[poly_X_expM_def] >> 1564 qabbrev_tac `x = 1 MOD 0` >> 1565 qabbrev_tac `ls = unity_mod_zero (ZN 0) (k - (m MOD k + 1))` >> 1566 `valueOf (poly_extendM (x::ls) (m MOD k)) = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls)` by rw[poly_extendM_value] >> 1567 `ls = PAD_RIGHT 0 (k - (m MOD k + 1)) []` by rw[unity_mod_zero_alt, ZN_property, Abbr`ls`] >> 1568 rw[unity_mod_zero_alt, ZN_property] >> 1569 rw[PAD_LEFT_BY_RIGHT] >> 1570 qabbrev_tac `s = PAD_RIGHT 0 (m MOD k) [] ++ [x]` >> 1571 `LENGTH s = m MOD k + 1` by rw[PAD_RIGHT_LENGTH, Abbr`s`] >> 1572 metis_tac[PAD_RIGHT_BY_RIGHT] 1573 ]); 1574 1575(* Theorem: 0 < n ==> Weak (ZN n) (valueOf (poly_X_expM n k m)) *) 1576(* Proof: 1577 Weak (ZN n) (valueOf (poly_X_expM n k m)) 1578 = Weak (ZN n) (unity_mod_X_exp (ZN n) k m) by poly_X_expM_value 1579 = Weak (ZN n) (unity_mod_special (ZN n) k m 0) by unity_mod_X_exp_def 1580 = T by ZN_unity_mod_special_weak 1581*) 1582val poly_X_expM_weak = store_thm( 1583 "poly_X_expM_weak", 1584 ``!n k m. 0 < n ==> Weak (ZN n) (valueOf (poly_X_expM n k m))``, 1585 rw[unity_mod_X_exp_def, ZN_unity_mod_special_weak]); 1586 1587(* Theorem: LENGTH (valueOf (poly_X_expM n k m)) = k *) 1588(* Proof: 1589 If n = 0, 1590 LENGTH (valueOf (poly_X_expM n k m)) 1591 = LENGTH (if k = 0 then [] else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0])) 1592 by poly_X_expM_zero 1593 = if k = 0 then 0 else LENGTH (PAD_RIGHT 0 k ls) where ls = PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0] 1594 = if k = 0 then 0 else MAX k (LENGTH ls) by PAD_RIGHT_LENGTH 1595 = if k = 0 then 0 else MAX k (MAX (m MOD k + 1) 1) by PAD_LEFT_LENGTH 1596 = if k = 0 then 0 else MAX (MAX k (m MOD k)) 1 by MAX_ASSOC 1597 = if k = 0 then 0 else MAX k 1 by MOD_LESS, k <> 0 1598 = if k = 0 then 0 else k by MAX_DEF, 1 <= k 1599 = k 1600 If n <> 0, 1601 LENGTH (valueOf (poly_X_expM n k m)) 1602 = LENGTH (unity_mod_X_exp (ZN n) k m) by poly_X_expM_value, 0 < n 1603 = k by unity_mod_X_exp_length 1604*) 1605val poly_X_expM_length = store_thm( 1606 "poly_X_expM_length[simp]", 1607 ``!n k m. LENGTH (valueOf (poly_X_expM n k m)) = k``, 1608 rpt strip_tac >> 1609 Cases_on `n = 0` >| [ 1610 rw[poly_X_expM_zero, PAD_RIGHT_LENGTH, PAD_LEFT_LENGTH] >> 1611 rw[MAX_ASSOC, MAX_DEF] >> 1612 `m MOD k < k` by rw[MOD_LESS] >> 1613 decide_tac, 1614 rw[poly_X_expM_value, unity_mod_X_exp_length] 1615 ]); 1616 1617(* Theorem: stepsOf (poly_X_expM n k m) = 1618 if k = 0 then 1 1619 else size n + 2 * size k + if k = 1 then 1 1620 else (if k = 0 then 0 else size m * size k) + 1 + size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1621 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + 1622 stepsOf (poly_extendM ((1 MOD n)::unity_mod_zero (ZN n) (k - (m MOD k) - 1)) (m MOD k)) *) 1623(* Proof: 1624 stepsOf (poly_X_expM n k m) 1625 = stepsOf (zeroM k) + if k = 0 then 0 1626 else stepsOf (modM 1 n) + 1627 stepsOf (oneM k) + if k = 1 then 1 1628 else stepsOf (modM m k) + stepsOf (subM k (m MOD k)) + stepsOf (decM (k - (m MOD k))) + 1629 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + stepsOf (consM (1 MOD n) p) + 1630 stepsOf (poly_extendM q (m MOD k)) by poly_X_expM_def 1631 = size k + if k = 0 then 0 1632 else (size 1 * size n) + size k + if k = 1 then 1 1633 else (if k = 0 then 0 else size m * size k) + 1634 size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1635 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + 1 + stepsOf (poly_extendM q (m MOD k)) 1636 = size k + if k = 0 then 0 1637 else size n + size k + if k = 1 then 1 1638 else (if k = 0 then 0 else size m * size k) + 1 + 1639 size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1640 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + stepsOf (poly_extendM q (m MOD k)) 1641 = if k = 0 then 1 1642 else size n + 2 * size k + if k = 1 then 1 1643 else (if k = 0 then 0 else size m * size k) + 1 + size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1644 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + stepsOf (poly_extendM q (m MOD k)) 1645*) 1646val poly_X_expM_steps_eqn = store_thm( 1647 "poly_X_expM_steps_eqn", 1648 ``!n k m. stepsOf (poly_X_expM n k m) = 1649 if k = 0 then 1 1650 else size n + 2 * size k + if k = 1 then 1 1651 else (if k = 0 then 0 else size m * size k) + 1 + size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1652 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + 1653 stepsOf (poly_extendM ((1 MOD n)::unity_mod_zero (ZN n) (k - (m MOD k) - 1)) (m MOD k))``, 1654 rw[poly_X_expM_def, size_max]); 1655 1656(* Theorem: stepsOf (poly_X_expM n k m) <= 1657 3 + 2 * k + size n + 4 * size k + size m * size k + 4 * k * size k *) 1658(* Proof: 1659 stepsOf (poly_X_expM n k m) 1660 = if k = 0 then 1 1661 else size n + 2 * size k + if k = 1 then 1 1662 else (if k = 0 then 0 else size m * size k) + 1 + size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1663 stepsOf (poly_zeroM n (k - (m MOD k) - 1)) + 1664 stepsOf (poly_extendM ((1 MOD n)::unity_mod_zero (ZN n) (k - (m MOD k) - 1)) (m MOD k)) 1665 by poly_X_expM_steps_eqn 1666 <= size 1 * size n + 2 * size k + 1667 size m * size k + 1 + size (MAX k (m MOD k)) + size (k - (m MOD k)) + 1668 (1 + p + 2 * p * size p) + by poly_zeroM_steps_upper, p = k - (m MOD k) - 1 1669 (1 + q + 2 * q * size q) by poly_extendM_steps_upper, q = m MOD k 1670 Note m MOD k <= k by MOD_LESS_EQ, 0 < k 1671 Thus size (MAX k (m MOD k)) = size k by MAX_DEF 1672 and size (k - (m MOD k)) <= size k by size_monotone_le 1673 Also p < k, so size p <= size k by size_monotone_lt 1674 and q <= k, so size q <= size k by size_monotone_le 1675 1676 stepsOf (poly_X_expM n k m) 1677 <= size n + 2 * size k + 1678 size m * size k + 1 + size k + size k + 2 * (1 + k + 2 * k * size k) 1679 = 3 + size n + 4 * size k + 2 * k + size m * size k + 4 * k * size k 1680 = 3 + 2 * k + size n + 4 * size k + size m * size k + 4 * k * size k 1681*) 1682val poly_X_expM_steps_upper = store_thm( 1683 "poly_X_expM_steps_upper", 1684 ``!n k m. stepsOf (poly_X_expM n k m) <= 1685 3 + 2 * k + size n + 4 * size k + size m * size k + 4 * k * size k``, 1686 rpt strip_tac >> 1687 assume_tac poly_X_expM_steps_eqn >> 1688 last_x_assum (qspecl_then [`n`, `k`, `m`] strip_assume_tac) >> 1689 qabbrev_tac `h = m MOD k` >> 1690 qabbrev_tac `ls = 1 MOD n::unity_mod_zero (ZN n) (k - h - 1)` >> 1691 qabbrev_tac `j = k - h - 1` >> 1692 qabbrev_tac `t = size n` >> 1693 Cases_on `k = 0` >- 1694 rw[] >> 1695 Cases_on `k = 1` >- 1696 rw[] >> 1697 `h < k` by rw[Abbr`h`] >> 1698 `size (MAX k h) = size k` by rw[MAX_DEF] >> 1699 `stepsOf (poly_X_expM n k m) = 1 + t + 3 * (size k) + (size m * size k) + 1700 size (k - h) + stepsOf (poly_zeroM n j) + stepsOf (poly_extendM ls h)` by fs[] >> 1701 `size (k - h) <= size k` by rw[size_monotone_le] >> 1702 `stepsOf (poly_zeroM n j) <= 1 + k + 2 * k * size k` by 1703 (`stepsOf (poly_zeroM n j) <= 1 + j + 2 * j * size j` by rw[poly_zeroM_steps_upper] >> 1704 `j < k` by rw[Abbr`j`] >> 1705 `size j <= size k` by rw[size_monotone_lt] >> 1706 `j * size j <= k * size k` by rw[LE_MONO_MULT2] >> 1707 decide_tac) >> 1708 `stepsOf (poly_extendM ls h) <= 1 + k + 2 * k * size k` by 1709 (`stepsOf (poly_extendM ls h) <= 1 + h + 2 * h * size h` by rw[poly_extendM_steps_upper] >> 1710 `size h <= size k` by rw[size_monotone_lt] >> 1711 `h * size h <= k * size k` by rw[LE_MONO_MULT2] >> 1712 decide_tac) >> 1713 decide_tac); 1714 1715(* Theorem: stepsOf (poly_X_expM n k m) <= 15 * (MAX 1 k) * size k * size n * size m *) 1716(* Proof: 1717 stepsOf (poly_X_expM n k m) 1718 <= 3 + 2 * k + size n + 4 * size k + size m * size k + 4 * k * size k by poly_X_expM_steps_upper 1719 <= (3 + 2 + 1 + 4 + 1 + 4) * k * size k * size n * size m by dominant term 1720 = 15 * k * size k * size n * size m 1721 Use (MAX 1 k) to cater for k = 0. 1722*) 1723val poly_X_expM_steps_bound = store_thm( 1724 "poly_X_expM_steps_bound", 1725 ``!n k m. stepsOf (poly_X_expM n k m) <= 15 * (MAX 1 k) * size k * size n * size m``, 1726 rpt strip_tac >> 1727 `stepsOf (poly_X_expM n k m) <= 3 + 2 * k + size n + 4 * size k + size m * size k + 4 * k * size k` by rw[poly_X_expM_steps_upper] >> 1728 qabbrev_tac `h = MAX 1 k` >> 1729 qabbrev_tac `t = h * size k * size n * size m` >> 1730 `stepsOf (poly_X_expM n k m) <= 15 * t` suffices_by rw[Abbr`t`] >> 1731 `1 <= h /\ k <= h` by rw[Abbr`h`] >> 1732 `0 < t` by rw[MULT_POS, Abbr`t`] >> 1733 `1 <= t` by decide_tac >> 1734 `k <= t` by 1735 (`h <= h * (size k * size n * size m)` by rw[MULT_POS] >> 1736 `h * (size k * size n * size m) = t` by rw[Abbr`t`] >> 1737 decide_tac) >> 1738 `size n <= t` by 1739 (`size n <= size n * (h * size k * size m)` by rw[MULT_POS] >> 1740 `size n * (h * size k * size m) = t` by rw[Abbr`t`] >> 1741 decide_tac) >> 1742 `size k <= t` by 1743 (`size k <= size k * (h * size n * size m)` by rw[MULT_POS] >> 1744 `size k * (h * size n * size m) = t` by rw[Abbr`t`] >> 1745 decide_tac) >> 1746 `size m * size k <= t` by 1747 (`size m * size k <= size m * size k * (h * size n)` by rw[MULT_POS] >> 1748 `size m * size k * (h * size n) = t` by rw[Abbr`t`] >> 1749 decide_tac) >> 1750 `k * size k <= t` by 1751 (`k * size k <= h * size k` by rw[] >> 1752 `h * size k <= h * size k * (size m * size n)` by rw[MULT_POS] >> 1753 `h * size k * (size m * size n) = t` by rw[Abbr`t`] >> 1754 decide_tac) >> 1755 decide_tac); 1756 1757 1758(* ------------------------------------------------------------------------- *) 1759(* Polynomial operations *) 1760(* ------------------------------------------------------------------------- *) 1761 1762(* Equality of polynomial p q, both of length k *) 1763(* > EQ_LIST; 1764val it = |- !h1 h2. h1 = h2 ==> !l1 l2. l1 = l2 ==> h1::l1 = h2::l2: thm 1765*) 1766 1767(* Pseudocode: 1768 Given polynomials p and q, test if (p = q). 1769 list_eq p q: 1770 if p = [], return (q = []) // equal if [] = [] 1771 if q = [], return (p = []) // equal if [] = [] 1772 return (head p) = (head q) /\ // heads must equal 1773 list_eq (tail p) (tail q) // recursive call with tails: tails equal 1774*) 1775 1776val poly_eqM_def = tDefine "poly_eqM" ` 1777 poly_eqM p q = 1778 do 1779 p0 <- nullM p; 1780 q0 <- nullM q; 1781 if p0 then return q0 1782 else if q0 then return p0 1783 else do 1784 h1 <- headM p; 1785 t1 <- tailM p; 1786 h2 <- headM q; 1787 t2 <- tailM q; 1788 e0 <- eqM h1 h2; 1789 if e0 then poly_eqM t1 t2 1790 else return F 1791 od 1792 od 1793`(WF_REL_TAC `measure (\(p,q). LENGTH q)` >> simp[LENGTH_TL_LT]); 1794 1795(* 1796EVAL ``poly_eqM [1;1;0;1;0;0;1] [1;1;0;1;0;0;1]``; = (T,Count 51): thm 1797EVAL ``poly_eqM [1;1;0;1;0;0;1] [1;1;0;0;1;0;1]``; = (F,Count 28): thm 1798*) 1799 1800 1801(* Theorem: valueOf (poly_eqM p q) = (p = q) *) 1802(* Proof: 1803 By induction from poly_eqM_def. 1804 valueOf (poly_eqM p q) 1805 = if (p = []) then (q = []) 1806 else if (q = []) then (p = []) 1807 else if (HD p = HD q) then valueOf (poly_eqM (TL p) (TL q)) else F 1808 by poly_eqM_def 1809 = if (p = []) then (q = []) 1810 else if (q = []) then (p = []) 1811 else (HD p = HD q) /\ (TL p = TL q) by induction hypothesis 1812 = (p = q) by LIST_EQ_HEAD_TAIL 1813*) 1814Theorem poly_eqM_value[simp]: 1815 !p q. valueOf (poly_eqM p q) = (p = q) 1816Proof 1817 ho_match_mp_tac (theorem "poly_eqM_ind") >> 1818 rw[] >> 1819 rw[Once poly_eqM_def] >> rw[LIST_EQ_HEAD_TAIL] 1820QED 1821 1822(* Theorem: stepsOf (poly_eqM p q) = 1823 2 + if ((p = []) \/ (q = [])) then 0 1824 else 4 + size (MAX (HD p) (HD q)) + 1825 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) *) 1826(* Proof: 1827 stepsOf (poly_eqM p q) 1828 = stepsOf (nullM p) + stepsOf (nullM q) + 1829 if (p = []) then 0 else if (q = []) then 0 1830 else stepsOf (headM p) + stepsOf (tailM p) + 1831 stepsOf (headM q) + stepsOf (tailM q) + 1832 stepsOf (eqM (HD p) (HD q)) + 1833 if (HD p = HD q) then stepsOf (poly_eqM (TL p) (TL q)) else 0 by poly_eqM_def 1834 = 1 + 1 + if ((p = []) \/ (q = [])) then 0 1835 else 1 + 1 + 1 + 1 + size (MAX (HD p) (HD q)) + 1836 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) by size_max 1837 = 2 + if ((p = []) \/ (q = [])) then 0 1838 else 4 + size (MAX (HD p) (HD q)) + if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) 1839*) 1840val poly_eqM_steps_thm = store_thm( 1841 "poly_eqM_steps_thm", 1842 ``!p q. stepsOf (poly_eqM p q) = 1843 2 + if ((p = []) \/ (q = [])) then 0 1844 else 4 + size (MAX (HD p) (HD q)) + 1845 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q))``, 1846 ho_match_mp_tac (theorem "poly_eqM_ind") >> 1847 (rw[] >> rw[Once poly_eqM_def, size_max]) >- 1848 rw[Once poly_eqM_def] >> 1849 rw[Once poly_eqM_def]); 1850 1851(* Theorem: stepsOf (poly_eqM p q) = 1852 if ((p = []) \/ (q = [])) then 2 1853 else 6 + size (MAX (HD p) (HD q)) + 1854 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) *) 1855(* Proof: 1856 stepsOf (poly_eqM p q) 1857 = 2 + if ((p = []) \/ (q = [])) then 0 1858 else 4 + size (MAX (HD p) (HD q)) + 1859 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) by poly_eqM_steps_thm 1860 = if ((p = []) \/ (q = [])) then 2 1861 else 6 + size (MAX (HD p) (HD q)) + 1862 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q)) 1863*) 1864val poly_eqM_steps_by_list_loop = store_thm( 1865 "poly_eqM_steps_by_list_loop", 1866 ``!p q. stepsOf (poly_eqM p q) = 1867 if ((p = []) \/ (q = [])) then 2 1868 else 6 + size (MAX (HD p) (HD q)) + 1869 if (HD p <> HD q) then 0 else stepsOf (poly_eqM (TL p) (TL q))``, 1870 rw[Once poly_eqM_steps_thm]); 1871 1872 1873(* 1874This puts poly_eqM_steps in the category: list loop with body on head and tail transform with exit. 1875 mexpM_steps_by_sqmod_div_loop: 1876 !p q. loop p q = if (p = []) \/ (q = []) then 2 else body p q + 1877 if exit p q then 0 else loop (TL p) (TL q) 1878suitable for: loop2_list_tail_head_count_exit_sum_le 1879and also for: loop2_list_tail_head_upper_count_exit_le 1880*) 1881 1882(* Theorem: (LENGTH p = k) /\ (LENGTH q = k) ==> 1883 stepsOf (poly_eqM p q) <= 2 + SUM (GENLIST (\j. 6 + size (MAX (EL j p) (EL j q))) k) *) 1884(* Proof: 1885 Let quit = (\p q. 2), 1886 f = (\x y. 6 + size (MAX x y)), 1887 body = (\p q. f (HD p) (HD q)), 1888 exit = (\p q. HD p <> HD q), 1889 loop = (\p q. stepsOf (poly_eqM p q)). 1890 Then !p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + 1891 if exit p q then 0 else loop (TL p) (TL q) by poly_eqM_steps_by_list_loop 1892 Given (LENGTH p = k) and LENGTH q = k, 1893 Thus loop p q 1894 <= quit [] [] + 1895 SUM (GENLIST (\j. f (EL j p) (EL j q)) k) by loop2_list_tail_head_count_exit_sum_le 1896 = 2 + SUM (GENLIST (\j. f (EL j p) (EL j q)) k) 1897*) 1898val poly_eqM_steps_by_sum_le = store_thm( 1899 "poly_eqM_steps_by_sum_le", 1900 ``!p q k. (LENGTH p = k) /\ (LENGTH q = k) ==> 1901 stepsOf (poly_eqM p q) <= 2 + SUM (GENLIST (\j. 6 + size (MAX (EL j p) (EL j q))) k)``, 1902 rpt strip_tac >> 1903 qabbrev_tac `quit = \p:num list q:num list. 2` >> 1904 qabbrev_tac `f = \x y. 6 + size (MAX x y)` >> 1905 qabbrev_tac `body = \p q. f (HD p) (HD q)` >> 1906 qabbrev_tac `exit = \p q:num list. HD p <> HD q` >> 1907 qabbrev_tac `loop = \p q. stepsOf (poly_eqM p q)` >> 1908 `loop p q <= 2 + SUM (GENLIST (\j. f (EL j p) (EL j q)) k)` suffices_by rw[Abbr`loop`] >> 1909 `!p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + if exit p q then 0 else loop (TL p) (TL q)` by metis_tac[poly_eqM_steps_by_list_loop] >> 1910 `body = (\p q. f (HD p) (HD q))` by metis_tac[] >> 1911 imp_res_tac loop2_list_tail_head_count_exit_sum_le >> 1912 metis_tac[]); 1913 1914(* Theorem: Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 1915 stepsOf (poly_eqM p q) <= 2 + 6 * k + k * size n *) 1916(* Proof: 1917 Let quit = (\p q. 2), 1918 f = (\x y. 6 + size (MAX x y)), 1919 body = (\p q. f (HD p) (HD q)), 1920 exit = (\p q. HD p <> HD q), 1921 loop = (\p q. stepsOf (poly_eqM p q)). 1922 Then !p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + 1923 if exit p q then 0 else loop (TL p) (TL q) by poly_eqM_steps_by_list_loop 1924 Given (LENGTH p = k) and LENGTH q = k, 1925 and EVERY (\j. j <= n) p by ZN_weak 1926 and EVERY (\j. j <= n) q by ZN_weak 1927 and MONO2 f by MAX_DEF, size_monotone_le 1928 Thus loop p q 1929 <= quit [][] + k * f n n by loop2_list_tail_head_upper_count_exit_le 1930 = 2 + k * (6 + size (MAX n n)) by notation 1931 = 2 + k * (6 + size n) by MAX_IDEM 1932 = 2 + 6 * k + k * size n 1933*) 1934val poly_eqM_steps_upper = store_thm( 1935 "poly_eqM_steps_upper", 1936 ``!p q k n. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 1937 stepsOf (poly_eqM p q) <= 2 + 6 * k + k * size n``, 1938 rpt strip_tac >> 1939 qabbrev_tac `quit = \p:num list q:num list. 2` >> 1940 qabbrev_tac `f = \x y. 6 + size (MAX x y)` >> 1941 qabbrev_tac `body = \p q. f (HD p) (HD q)` >> 1942 qabbrev_tac `exit = \p q:num list. HD p <> HD q` >> 1943 qabbrev_tac `loop = \p q. stepsOf (poly_eqM p q)` >> 1944 `loop p q <= 2 + 6 * k + k * size n` suffices_by rw[Abbr`loop`] >> 1945 `!p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + if exit p q then 0 else loop (TL p) (TL q)` by metis_tac[poly_eqM_steps_by_list_loop] >> 1946 `MONO2 f` by 1947 (rw[Abbr`f`] >> 1948 `MAX x1 y1 <= MAX x2 y2` by rw[] >> 1949 rw[size_monotone_le]) >> 1950 `body = (\p q. f (HD p) (HD q))` by metis_tac[] >> 1951 assume_tac (loop2_list_tail_head_upper_count_exit_le |> ISPEC ``loop: num list -> num list -> num``) >> 1952 first_x_assum (qspecl_then [`body`, `quit`, `exit`, `f`] strip_assume_tac) >> 1953 qabbrev_tac `foo = !p q. loop p q = if (p = []) \/ (q = []) then quit p q 1954 else body p q + if exit p q then 0 else loop (TL p) (TL q)` >> 1955 `!x y k n. (LENGTH x = k) /\ (LENGTH y = k) /\ EVERY (\j. j < n) x /\ EVERY (\j. j < n) y ==> 1956 loop x y <= quit [] [] + k * f n n` by metis_tac[] >> 1957 first_x_assum (qspecl_then [`p`, `q`, `k`, `n`] strip_assume_tac) >> 1958 `loop p q <= 2 + k * f n n` by metis_tac[ZN_weak] >> 1959 `k * f n n = k * (6 + size n)` by rw[Abbr`f`] >> 1960 `_ = k * 6 + k * size n` by rw[] >> 1961 decide_tac); 1962 1963(* This is the result I like! *) 1964 1965(* Theorem: Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 1966 stepsOf (poly_eqM p q) <= 9 * (MAX 1 k) * size n *) 1967(* Proof: 1968 stepsOf (poly_eqM p q) 1969 <= 2 + 6 * k + k * size n by poly_eqM_steps_upper 1970 <= (2 + 6 + 1) * k * size n by dominant term 1971 = 9 * k * size n 1972 Use (MAX 1 k) to cater for k = 0. 1973*) 1974val poly_eqM_steps_bound = store_thm( 1975 "poly_eqM_steps_bound", 1976 ``!p q k n. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 1977 stepsOf (poly_eqM p q) <= 9 * (MAX 1 k) * size n``, 1978 rpt strip_tac >> 1979 `stepsOf (poly_eqM p q) <= 2 + 6 * k + k * size n` by rw[poly_eqM_steps_upper] >> 1980 qabbrev_tac `m = MAX 1 k` >> 1981 qabbrev_tac `t = m * size n` >> 1982 `stepsOf (poly_eqM p q) <= 9 * t` suffices_by rw[Abbr`t`] >> 1983 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 1984 `0 < t` by rw[MULT_POS, Abbr`t`] >> 1985 `1 <= t` by decide_tac >> 1986 `k <= t` by 1987 (`m <= m * size n` by rw[MULT_POS] >> 1988 `m * size n = t` by rw[Abbr`t`] >> 1989 decide_tac) >> 1990 `k * size n <= t` by 1991 (`k * size n <= m * size n` by rw[] >> 1992 `m * size n = t` by rw[Abbr`t`] >> 1993 decide_tac) >> 1994 decide_tac); 1995 1996(* ------------------------------------------------------------------------- *) 1997(* Polynomial multiplication by a scalar *) 1998(* ------------------------------------------------------------------------- *) 1999 2000(* Multiply polynomial p of length k by a scalar c in (MOD n, (unity k)) *) 2001(* > weak_cmult_def; 2002|- (!r c. c o [] = []) /\ !r c h t. c o (h::t) = c * h::c o t 2003*) 2004 2005(* Pseudocode: 2006 Given modulus n, a scalar c and polynomial p, compute (c o p) (mod n). 2007 list_cmult c p: 2008 if p = [], return [] // c o [] = [] 2009 h <- c * (head p) MOD n // c multiply with head 2010 t <- list_cmult c (tail p) // recursive call with tail: c o (tail p) 2011 return h::t // combine to give result 2012*) 2013 2014val poly_cmultM_def = tDefine "poly_cmultM" ` 2015 poly_cmultM n c p = 2016 do 2017 p0 <- nullM p; 2018 if p0 then return [] 2019 else do 2020 h <- headM p; 2021 t <- tailM p; 2022 k <- mmulM n c h; 2023 q <- poly_cmultM n c t; 2024 consM k q; 2025 od 2026 od 2027`(WF_REL_TAC `measure (\(n,c,p). LENGTH p)` >> simp[LENGTH_TL_LT]); 2028 2029(* 2030> EVAL ``poly_cmultM 10 3 [1;4;5;2;1;1;3]``; = ([3; 2; 5; 6; 3; 3; 9],Count 139): thm 2031> EVAL ``poly_cmultM 0 3 [1;4;5;2;1;1;3]``; = 2032 ([3 MOD 0; 12 MOD 0; 15 MOD 0; 6 MOD 0; 3 MOD 0; 3 MOD 0; 9 MOD 0], Count 55): thm 2033> EVAL ``poly_cmultM 0 (3 MOD 0) [1;4;5;2;1;1;3]``; -- run away! 2034*) 2035 2036(* Theorem: valueOf (poly_cmultM n c p) = weak_cmult (ZN n) c p *) 2037(* Proof: 2038 By induction from poly_cmultM_def. 2039 If p = [], 2040 valueOf (poly_cmultM n c p) 2041 = [] by poly_cmultM_def 2042 = weak_cmult (ZN n) c [] by weak_cmult_of_zero 2043 If p = h::t, 2044 valueOf (poly_cmultM n c p) 2045 = (c * h) MOD n :: valueOf (poly_cmultM n c t) by poly_cmultM_def 2046 = (c * h) MOD n :: weak_cmult (ZN n) c t by induction hypothesis 2047 = weak_cmult (ZN n) c p by weak_cmult_cons 2048*) 2049val poly_cmultM_value = store_thm( 2050 "poly_cmultM_value[simp]", 2051 ``!n c p. valueOf (poly_cmultM n c p) = weak_cmult (ZN n) c p``, 2052 ho_match_mp_tac (theorem "poly_cmultM_ind") >> 2053 rw[] >> 2054 rw[Once poly_cmultM_def] >> 2055 (Cases_on `p` >> fs[ZN_property])); 2056 2057(* Theorem: Weak (ZN n) p ==> (valueOf (poly_cmultM n c p) = c oz p) *) 2058(* Proof: by poly_cmultM_value, ZN_poly_cmult_alt *) 2059val poly_cmultM_value_alt = store_thm( 2060 "poly_cmultM_value_alt", 2061 ``!n c p. Weak (ZN n) p ==> (valueOf (poly_cmultM n c p) = c oz p)``, 2062 rw[ZN_poly_cmult_alt]); 2063 2064(* 2065weak_cmult_element |> ISPEC ``(ZN n)`` |> SIMP_RULE bool_ss [ZN_property]; 2066|- !c p j. j < LENGTH p ==> EL j (weak_cmult (ZN n) c p) = (c * EL j p) MOD n 2067*) 2068 2069(* Theorem: j < LENGTH p ==> (EL j (valueOf (poly_cmultM n c p)) = (c * EL j p) MOD n) *) 2070(* Proof: 2071 EL j (valueOf (poly_cmultM n c p)) 2072 = EL j (weak_cmult (ZN n) c p) by poly_cmultM_value 2073 = (c * EL j p) MD n by weak_cmult_element 2074*) 2075val poly_cmultM_element = store_thm( 2076 "poly_cmultM_element", 2077 ``!n c p j. j < LENGTH p ==> (EL j (valueOf (poly_cmultM n c p)) = (c * EL j p) MOD n)``, 2078 rw[weak_cmult_element, ZN_property]); 2079 2080(* Note: weak_cmult_weak |- !r. Ring r ==> !p. weak p ==> !c. c IN R ==> weak (c o p) 2081 requires c IN R. Here we just need c:num, not c < n for c IN (ZN n).carrier. 2082 Thus the following proof, using weak_cmult_element, is better, special for (ZN n). 2083*) 2084(* Theorem: 0 < n ==> Weak (ZN n) (valueOf (poly_cmultM n c p)) *) 2085(* Proof: 2086 Weak (ZN n) (valueOf (poly_cmultM n c p)) 2087 <=> Weak (ZN n) (weak_cmult (ZN n) c p) by poly_cmultM_value 2088 <=> EVERY (\c. c < n) (weak_cmult (ZN n) c p) by ZN_weak 2089 <=> !j. j < LENGTH ls ==> (EL j ls) < n by EVERY_EL, ls = weak_cmult (ZN n) c p 2090 <=> !j. j < LENGTH p ==> (c * EL j p) MOD n < n by weak_cmult_length, weak_cmult_element 2091 <=> !j. j < LENGTH p ==> T by MOD_LESS, 0 < n 2092 <=> T 2093*) 2094val poly_cmultM_weak = store_thm( 2095 "poly_cmultM_weak", 2096 ``!n c p. 0 < n ==> Weak (ZN n) (valueOf (poly_cmultM n c p))``, 2097 rw[ZN_weak] >> 2098 irule (EVERY_EL |> SPEC_ALL |> #2 o EQ_IMP_RULE) >> 2099 rw[weak_cmult_element, weak_cmult_length, ZN_property]); 2100 2101(* Theorem: LENGTH (valueOf (poly_cmultM n c p)) = LENGTH p *) 2102(* Proof: 2103 LENGTH (valueOf (poly_cmultM n c p)) 2104 = LENGTH (weak_cmult (ZN n) c p) by poly_cmultM_value 2105 = LENGTH p by weak_cmult_length 2106*) 2107val poly_cmultM_length = store_thm( 2108 "poly_cmultM_length[simp]", 2109 ``!n c p. LENGTH (valueOf (poly_cmultM n c p)) = LENGTH p``, 2110 rw[weak_cmult_length]); 2111 2112(* Theorem: stepsOf (poly_cmultM n c p) = 2113 if (p = []) then 1 2114 else 4 + size c * size (HD p) + size (c * HD p) * size n + 2115 stepsOf (poly_cmultM n c (TL p)) *) 2116(* Proof: 2117 stepsOf (poly_cmultM n c p) 2118 = stepsOf (nullM p) + if (p = []) then 0 2119 else stepsOf (headM p) + stepsOf (tailM p) + 2120 stepsOf (mmulM n c (HD p)) + 2121 stepsOf (poly_cmultM n c (TL p)) + 2122 stepsOf (consM ((c * HD p) MOD n) (valueOf (poly_cmultM n c (TL p)))) 2123 by poly_cmultM_def 2124 = 1 + if (p = []) then 0 2125 else 1 + 1 + (size c * size (HD p) + size (c * HD p) * size n + 2126 stepsOf (poly_cmultM n c (TL p)) + 1 by mmulM_steps 2127 = if (p = []) then 1 2128 else 4 + size c * size (HD p) + size (c * HD p) * size n + 2129 stepsOf (poly_cmultM n c (TL p)) by arithmetic 2130*) 2131val poly_cmultM_steps_thm = store_thm( 2132 "poly_cmultM_steps_thm", 2133 ``!n c p. stepsOf (poly_cmultM n c p) = 2134 if (p = []) then 1 2135 else 4 + size c * size (HD p) + size (c * HD p) * size n + 2136 stepsOf (poly_cmultM n c (TL p))``, 2137 ho_match_mp_tac (theorem "poly_cmultM_ind") >> 2138 rpt strip_tac >> 2139 (Cases_on `p` >> simp[Once poly_cmultM_def])); 2140 2141(* Theorem alias *) 2142val poly_cmultM_steps_by_list_loop = save_thm("poly_cmultM_steps_by_list_loop", poly_cmultM_steps_thm); 2143 2144(* 2145This puts poly_cmultM_steps in the category: list loop with body on head. 2146 poly_cmultM_steps_by_list_loop: 2147 !p. loop p = if (p = []) then c else body p + loop (TL p) 2148suitable for: loop_list_head_count_eqn 2149and also for: loop_list_head_upper_count_le 2150*) 2151 2152(* Theorem: stepsOf (poly_cmultM n c p) = 2153 1 + SUM (GENLIST (\j. 4 + size c * size (EL j p) + 2154 size (c * (EL j p)) * size n) (LENGTH p)) *) 2155(* Proof: 2156 Let f = (\j. 4 + size c * size j + size (c * j) * size n), 2157 body = (\p. f (HD p)), 2158 loop = (\p. stepsOf (poly_cmultM n c p)) 2159 Then loop p = if (p = []) then 1 else body p + loop (TL p) by poly_cmultM_steps_thm 2160 Thus loop p = 1 + SUM (GENLIST (\j. f (EL j p)) (LENGTH p)) by loop_list_head_count_eqn 2161*) 2162val poly_cmultM_steps_eqn = store_thm( 2163 "poly_cmultM_steps_eqn", 2164 ``!n c p. stepsOf (poly_cmultM n c p) = 2165 1 + SUM (GENLIST (\j. 4 + size c * size (EL j p) + size (c * (EL j p)) * size n) 2166 (LENGTH p))``, 2167 rpt strip_tac >> 2168 qabbrev_tac `f = \j. 4 + size c * size j + size (c * j) * size n` >> 2169 qabbrev_tac `body = \p. f (HD p)` >> 2170 qabbrev_tac `loop = \p. stepsOf (poly_cmultM n c p)` >> 2171 `loop p = 1 + SUM (GENLIST (\j. f (EL j p)) (LENGTH p))` suffices_by rw[] >> 2172 `!p. loop p = if (p = []) then 1 else body p + loop (TL p)` by metis_tac[poly_cmultM_steps_thm] >> 2173 `body = (\x. f (HD x))` by metis_tac[] >> 2174 imp_res_tac loop_list_head_count_eqn >> 2175 first_x_assum (qspec_then `p` strip_assume_tac)); 2176 2177(* Theorem: Weak (ZN n) p /\ (LENGTH p = k) ==> 2178 stepsOf (poly_cmultM n c p) <= 2179 1 + 4 * k + 2 * k * size c * size n + k * (size n) ** 2 *) 2180(* Proof: 2181 Let f = (\j. 4 + size c * size j + size (c * j) * size n), 2182 body = (\p. f (HD p)), 2183 loop = (stepsOf o poly_cmultM n c) 2184 Then loop p = if (p = []) then 1 else body p + loop (TL p) by poly_cmultM_steps_thm 2185 Now Weak (ZN n) p <=> EVERY (\j.j < n) p by ZN_weak 2186 and MONO f by size_monotone_le 2187 Thus loop p 2188 <= 1 + k * f n by loop_list_head_upper_count_le 2189 = 1 + k * (4 + size c * size n + size (c * n) * size n) 2190 <= 1 + 4 * k + k * size c * size n + k * size (c * n) * size n 2191 <= 1 + 4 * k + k * size c * size n + k * (size c + size n) * size n by size_mult_upper 2192 = 1 + 4 * k + 2 * k * size c * size n + k * size n ** 2 2193*) 2194val poly_cmultM_steps_upper = store_thm( 2195 "poly_cmultM_steps_upper", 2196 ``!n c p k. Weak (ZN n) p /\ (LENGTH p = k) ==> 2197 stepsOf (poly_cmultM n c p) <= 1 + 4 * k + 2 * k * size c * size n + k * (size n) ** 2``, 2198 rpt strip_tac >> 2199 qabbrev_tac `f = \j. 4 + size c * size j + size (c * j) * size n` >> 2200 qabbrev_tac `body = \p. f (HD p)` >> 2201 qabbrev_tac `loop = (stepsOf o poly_cmultM n c)` >> 2202 `loop p <= 1 + 4 * k + 2 * k * size c * size n + k * (size n) ** 2` suffices_by rw[Abbr`loop`, Abbr`f`] >> 2203 `!p. loop p = if (p = []) then 1 else body p + loop (TL p)` by metis_tac[poly_cmultM_steps_thm, combinTheory.o_THM] >> 2204 `MONO f` by 2205 (rw[size_monotone_le, Abbr`f`] >> 2206 `c * x <= c * y` by rw[] >> 2207 `size c * size x <= size c * size y /\ size n * size (c * x) <= size n * size (c * y)` by rw[size_monotone_le] >> 2208 decide_tac) >> 2209 `loop p <= 1 + k * f n` by metis_tac[loop_list_head_upper_count_le, ZN_weak] >> 2210 `k * f n <= 4 * k + TWICE k * size c * size n + k * size n ** 2` by 2211 (rw[Abbr`f`] >> 2212 qabbrev_tac `k = LENGTH p` >> 2213 `size (c * n) <= size c + size n` by rw[size_mult_upper] >> 2214 `size n * size (c * n) <= size n * (size c + size n)` by rw[] >> 2215 `size n * (size c + size n) = size n * size c + size n * size n` by decide_tac >> 2216 `_ = size n * size c + (size n) ** 2` by rw[] >> 2217 `k * (size c * size n + (size n * size (c * n) + 4)) <= 2218 k * (size c * size n + (size n * size c + (size n) ** 2 + 4))` by rw[] >> 2219 decide_tac) >> 2220 decide_tac); 2221 2222(* Theorem: Weak (ZN n) p /\ (LENGTH p = k) ==> 2223 stepsOf (poly_cmultM n c p) <= 8 * (MAX 1 k) * size (MAX c n) * size n *) 2224(* Proof: 2225 stepsOf (poly_cmultM n c p) 2226 <= 1 + 4 * k + 2 * k * size c * size n + k * size n ** 2 2227 by poly_cmultM_steps_upper 2228 <= (1 + 4 + 2 + 1) * k * size (MAX c n) * size n by dominant term 2229 = 8 * k * size (MAX c n) * size n 2230 Use (MAX 1 k) to cater for k = 0. 2231*) 2232val poly_cmultM_steps_bound = store_thm( 2233 "poly_cmultM_steps_bound", 2234 ``!n c p k. Weak (ZN n) p /\ (LENGTH p = k) ==> 2235 stepsOf (poly_cmultM n c p) <= 8 * (MAX 1 k) * size (MAX c n) * size n``, 2236 rpt strip_tac >> 2237 `stepsOf (poly_cmultM n c p) <= 2238 1 + 4 * k + 2 * k * size c * size n + k * size n ** 2` by rw[poly_cmultM_steps_upper] >> 2239 qabbrev_tac `m = MAX 1 k` >> 2240 qabbrev_tac `d = MAX c n` >> 2241 qabbrev_tac `t = m * size d * size n` >> 2242 `stepsOf (poly_cmultM n c p) <= 8 * t` suffices_by rw[] >> 2243 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 2244 `c <= d /\ n <= d` by rw[Abbr`d`] >> 2245 `0 < t` by rw[MULT_POS, Abbr`t`] >> 2246 `1 <= t` by decide_tac >> 2247 `k <= t` by 2248 (`m <= m * (size d * size n)` by rw[MULT_POS] >> 2249 `m * (size d * size n) = t` by rw[Abbr`t`] >> 2250 decide_tac) >> 2251 `k * size c * size n <= t` by 2252 (`k * size c * size n <= m * size d * size n` by rw[size_monotone_le, LE_MONO_MULT2] >> 2253 `m * size d * size n = t` by rw[Abbr`t`] >> 2254 decide_tac) >> 2255 `k * size n ** 2 <= t` by 2256 (`k * size n ** 2 = k * size n * size n` by rw[] >> 2257 `k * size n * size n <= m * size d * size n` by rw[size_monotone_le, LE_MONO_MULT2] >> 2258 `m * size d * size n = t` by rw[Abbr`t`] >> 2259 decide_tac) >> 2260 decide_tac); 2261 2262(* ------------------------------------------------------------------------- *) 2263(* Polynomial weak addition (by pair-wise add in mod n) *) 2264(* ------------------------------------------------------------------------- *) 2265 2266(* Add two polynomials p, q of the same length k in (MOD n, (unity k)) *) 2267(* > weak_add_def; 2268|- (!r q. [] || q = q) /\ (!v5 v4 r. (v4::v5) || [] = v4::v5) /\ 2269 !r qt qh pt ph. (ph::pt) || (qh::qt) = ph + qh::pt || qt 2270*) 2271 2272(* Pseudocode: 2273 Given modulus n, and polynomials p and q, compute p || q (mod n). 2274 list_add p q: 2275 if p = [], return q // [] || q = q 2276 if q = [], return p // p || [] = p 2277 h <- (head p) + (head q) MOD n // pair-wise add of heads 2278 t <- list_add (tail p) (tail q) // recursive call with tails: (tail p) || (tail q) 2279 return h::t // combine to give result 2280*) 2281val poly_addM_def = tDefine "poly_addM" ` 2282 poly_addM n p q = 2283 do 2284 p0 <- nullM p; 2285 q0 <- nullM q; 2286 if p0 then return q 2287 else if q0 then return p 2288 else do 2289 h1 <- headM p; 2290 h2 <- headM q; 2291 t1 <- tailM p; 2292 t2 <- tailM q; 2293 h <- maddM n h1 h2; 2294 r <- poly_addM n t1 t2; 2295 consM h r; 2296 od 2297 od 2298`(WF_REL_TAC `measure (\(n,p,q). LENGTH q)` >> simp[LENGTH_TL_LT]); 2299 2300(* 2301> EVAL ``poly_addM 10 [1;4;5;6;1;1;3] [1;5;1;6;3;3;2]``; = ([2; 9; 6; 2; 4; 4; 5],Count 155): thm 2302*) 2303 2304(* Theorem: valueOf (poly_addM n p q) = weak_add (ZN n) p q *) 2305(* Proof: 2306 If p = [], 2307 valueOf (poly_addM n [] q) 2308 = q by poly_addM_def 2309 = weak_add (ZN n) [] q by weak_add_nil 2310 If q = [], 2311 valueOf (poly_addM n p []) 2312 = p by poly_addM_def 2313 = weak_add (ZN n) p [] by weak_add_nil 2314 Otherwise, p <> [] /\ q <> []. 2315 Let p = h::t, q = k::s. 2316 valueOf (poly_addM n (h::t) (k::s)) 2317 = (h + k) MOD n :: valueOf (poly_addM n t s) by poly_addM_def 2318 = (h + k) MOD n :: weak_add (ZN n) t s by induction hypothesis 2319 = weak_add (ZN n) (h::t) (k::s) by weak_add_cons, ZN_property 2320*) 2321val poly_addM_value = store_thm( 2322 "poly_addM_value[simp]", 2323 ``!n p q. valueOf (poly_addM n p q) = weak_add (ZN n) p q``, 2324 ho_match_mp_tac (theorem "poly_addM_ind") >> 2325 rw[] >> 2326 rw[Once poly_addM_def] >> 2327 (Cases_on `p` >> Cases_on `q` >> fs[ZN_property])); 2328 2329(* Theorem: Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = LENGTH q) ==> 2330 (valueOf (poly_addM n p q) = p +z q) *) 2331(* Proof: by poly_addM_value, ZN_poly_add_alt *) 2332val poly_addM_value_alt = store_thm( 2333 "poly_addM_value_alt", 2334 ``!n p q. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = LENGTH q) ==> 2335 (valueOf (poly_addM n p q) = p +z q)``, 2336 rw[ZN_poly_add_alt]); 2337 2338(* Theorem: j < LENGTH p /\ j < LENGTH q ==> 2339 (EL j (valueOf (poly_addM n p q)) = ((EL j p) + (EL j q)) MOD n) *) 2340(* Proof: 2341 EL j (valueOf (poly_addM n p q)) 2342 = EL j (weak_add (ZN n) p q) by poly_addM_value 2343 = ((EL j p) + (EL j q)) MOD n by weak_add_element, ZN_property 2344*) 2345val poly_addM_element = store_thm( 2346 "poly_addM_element", 2347 ``!n p q j. j < LENGTH p /\ j < LENGTH q ==> 2348 (EL j (valueOf (poly_addM n p q)) = ((EL j p) + (EL j q)) MOD n)``, 2349 rw[weak_add_element, ZN_property]); 2350 2351(* Note: weak_add_weak |- !r. Ring r ==> !p q. weak p /\ weak q ==> weak (p || q) 2352 requires Weak (ZN n) p and Weak (ZN n) q. Here we just need p:num list and q:num list. 2353 Thus the following proof, using weak_add_element, is better, special for (ZN n). 2354*) 2355 2356(* Theorem: 0 < n /\ (LENGTH p = LENGTH q) ==> Weak (ZN n) (valueOf (poly_addM n p q)) *) 2357(* Proof: 2358 Note MAX (LENGTH p) (LENGTH q) = LENGTH p by MAX_DEF, LENGTH p = LENGTH q. 2359 Weak (ZN n) (valueOf (poly_addM n p q)) 2360 = Weak (ZN n) (weak_add (ZN n) p q) by poly_addM_value 2361 = EVERY (\j. j < n) (weak_add (ZN n) p q) by ZN_weak 2362 = !j. EL j (weak_add (ZN n) p q) < n by EVERY_EL 2363 = !j. (EL j p + EL j q) MOD n < n by weak_add_element, ZN_property 2364 = T by MOD_LESS, 0 < n 2365*) 2366val poly_addM_weak = store_thm( 2367 "poly_addM_weak", 2368 ``!n p q. 0 < n /\ (LENGTH p = LENGTH q) ==> Weak (ZN n) (valueOf (poly_addM n p q))``, 2369 rw[ZN_weak, EVERY_EL] >> 2370 fs[weak_add_length, MAX_DEF] >> 2371 `n' < LENGTH p /\ n' < LENGTH q` by decide_tac >> 2372 rw[weak_add_element, ZN_property]); 2373 2374(* Theorem: LENGTH (valueOf (poly_addM n p q)) = MAX (LENGTH p) (LENGTH q) *) 2375(* Proof: 2376 LENGTH (valueOf (poly_addM n p q)) 2377 = LENGTH (weak_add (ZN n) p q) by poly_addM_value 2378 = MAX (LENGTH p) (LENGTH q) by weak_add_length 2379*) 2380val poly_addM_length = store_thm( 2381 "poly_addM_length[simp]", 2382 ``!n p q. LENGTH (valueOf (poly_addM n p q)) = MAX (LENGTH p) (LENGTH q)``, 2383 rw[weak_add_length]); 2384 2385(* Theorem: stepsOf (poly_addM n p q) = 2386 if (p = []) \/ (q = []) then 2 2387 else 7 + size (MAX (HD p) (HD q)) + size (HD p + HD q) * size n + 2388 stepsOf (poly_addM n (TL p) (TL q)) *) 2389(* Proof: 2390 stepsOf (poly_addM n p q) 2391 = stepsOf (nullM p) + stepsOf (nullM q) + if (p = []) then 0 else if q = [] then 0 2392 else stepsOf (headM p) + stepsOf (headM q) + stepsOf (tailM p) + stepsOf (tailM q) + 2393 stepsOf (maddM n (HD p) (HD q)) + stepsOf (poly_addM n (TL p) (TL q)) + 2394 stepsOf (consM ((HD p + HD q) MOD n) r) by poly_addM_def 2395 = 1 + 1 + if (p = []) then 0 else if q = [] then 0 2396 else 1 + 1 + 1 + 1 + 2397 size (MAX (HD p) (HD q)) + size (HD p + HD q) * size n + 2398 stepsOf (poly_addM n (TL p) (TL q)) + 1 by size_max 2399 = if (p = []) \/ (q = []) then 2 2400 else 7 + size (MAX (HD p) (HD q)) + size (HD p + HD q) * size n + 2401 stepsOf (poly_addM n (TL p) (TL q)) 2402*) 2403val poly_addM_steps_thm = store_thm( 2404 "poly_addM_steps_thm", 2405 ``!n p q. stepsOf (poly_addM n p q) = 2406 if (p = []) \/ (q = []) then 2 2407 else 7 + size (MAX (HD p) (HD q)) + size (HD p + HD q) * size n + 2408 stepsOf (poly_addM n (TL p) (TL q))``, 2409 (rw[Once poly_addM_def, size_max] >> fs[])); 2410 2411(* Theorem alias *) 2412val poly_addM_steps_by_list_loop = save_thm("poly_addM_steps_by_list_loop", poly_addM_steps_thm); 2413 2414(* 2415This puts poly_addM_steps in the category: list loop with body on head and transform on head. 2416 poly_addM_steps_by_list_loop: 2417 !p q. loop p q = if (p = []) \/ (q = []) then c else body p q + loop (TL p) (TL q) 2418suitable for: loop2_list_tail_head_count_eqn 2419and also for: loop2_list_tail_head_upper_count_le 2420*) 2421 2422(* Theorem: (LENGTH p = k) /\ (LENGTH q = k) ==> 2423 (stepsOf (poly_addM n p q) = 2424 2 + SUM (GENLIST (\j. 7 + size (MAX (EL j p) (EL j q)) + 2425 size (EL j p + EL j q) * size n) k)) *) 2426(* Proof: 2427 Let quit = (\p q. 2), 2428 f = (\i j. 7 + size (MAX i j) + size (i + j) * size n), 2429 body = (\p q. f (HD p) (HD q)), 2430 loop = (\p q. stepsOf (poly_addM n p q)). 2431 Then loop p q = if (p = []) \/ (q = []) then quit p q else body p q + loop (TL p) (TL q) 2432 by poly_addM_steps_thm 2433 Thus loop p q 2434 = quit [][] + SUM (GENLIST (\j. f (EL j p) (EL j q)) k) by loop2_list_tail_head_count_eqn 2435 = 2 + SUM (GENLIST (\j. f (EL j p) (EL j q)) k) 2436*) 2437val poly_addM_steps_eqn = store_thm( 2438 "poly_addM_steps_eqn", 2439 ``!n p q k. (LENGTH p = k) /\ (LENGTH q = k) ==> 2440 (stepsOf (poly_addM n p q) = 2441 2 + SUM (GENLIST (\j. 7 + size (MAX (EL j p) (EL j q)) + 2442 size (EL j p + EL j q) * size n) k))``, 2443 rpt strip_tac >> 2444 qabbrev_tac `quit = \p:num list q:num list. 2` >> 2445 qabbrev_tac `f = \i j. 7 + size (MAX i j) + size (i + j) * size n` >> 2446 qabbrev_tac `body = \p q. f (HD p) (HD q)` >> 2447 qabbrev_tac `loop = \p q. stepsOf (poly_addM n p q)` >> 2448 qabbrev_tac `g = \j. 7 + size (MAX (EL j p) (EL j q)) + size (EL j p + EL j q) * size n` >> 2449 `loop p q = 2 + SUM (GENLIST g k)` suffices_by rw[] >> 2450 `g = \j. f (EL j p) (EL j q)` by rw[Abbr`g`, Abbr`f`] >> 2451 `SUM (GENLIST g k) = SUM (GENLIST (\j. f (EL j p) (EL j q)) k)` by rw[] >> 2452 `!p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + loop (TL p) (TL q)` by metis_tac[poly_addM_steps_thm] >> 2453 `body = (\p q. f (HD p) (HD q))` by metis_tac[] >> 2454 imp_res_tac loop2_list_tail_head_count_eqn >> 2455 metis_tac[]); 2456 2457(* Theorem: Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 2458 stepsOf (poly_addM n p q) <= 2 + 7 * k + 2 * k * size n + k * size n ** 2 *) 2459(* Proof: 2460 Let quit = (\p q. 2), 2461 f = (\i j. 7 + size (MAX i j) + size (i + j) * size n), 2462 body = (\p q. f (HD p) (HD q)), 2463 loop = (\p q. stepsOf (poly_addM n p q)). 2464 Then loop p q = if (p = []) \/ (q = []) then quit p q else body p q + loop (TL p) (TL q) 2465 by poly_addM_steps_thm 2466 Now MONO2 f by size_monotone_le 2467 Thus loop p q 2468 <= quit [][] + k * f n n by loop2_list_tail_head_upper_count_le 2469 = 2 + k * (7 + size (MAX n n) + size (n + n) * size n) by function application 2470 = 2 + k * (7 + size n + size (2 * n) * size n) by MAX_IDEM 2471 = 2 + k * (7 + size n + (size n + if n = 0 then 0 else 1) * size n) by size_twice 2472 <= 2 + k * (7 + size n + (size n + 1) * size n) by inequality 2473 = 2 + k * (7 + size n + size n ** 2 + size n) 2474 = 2 + 7 * k + 2 * k * size n + k * size n ** 2 2475*) 2476val poly_addM_steps_upper = store_thm( 2477 "poly_addM_steps_upper", 2478 ``!n p q k. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 2479 stepsOf (poly_addM n p q) <= 2 + 7 * k + 2 * k * size n + k * size n ** 2``, 2480 rpt strip_tac >> 2481 qabbrev_tac `quit = \p:num list q:num list. 2` >> 2482 qabbrev_tac `f = \i j. 7 + size (MAX i j) + size (i + j) * size n` >> 2483 qabbrev_tac `body = \p q. f (HD p) (HD q)` >> 2484 qabbrev_tac `loop = \p q. stepsOf (poly_addM n p q)` >> 2485 `loop p q <= 2 + 7 * k + 2 * k * size n + k * size n ** 2` suffices_by rw[] >> 2486 `!p q. loop p q = if (p = []) \/ (q = []) then quit p q else body p q + loop (TL p) (TL q)` by metis_tac[poly_addM_steps_thm] >> 2487 `EVERY (\j. j < n) p /\ EVERY (\j. j < n) q` by rw[GSYM ZN_weak] >> 2488 `MONO2 f` by 2489 (rw[size_monotone_le, Abbr`f`] >> 2490 `MAX x1 y1 <= MAX x2 y2` by rw[] >> 2491 `x1 + y1 <= x2 + y2` by decide_tac >> 2492 `size (MAX x1 y1) <= size (MAX x2 y2)` by rw[size_monotone_le] >> 2493 `size n * size (x1 + y1) <= size n * size (x2 + y2)` by rw[size_monotone_le] >> 2494 decide_tac) >> 2495 `body = (\p q. f (HD p) (HD q))` by metis_tac[] >> 2496 imp_res_tac loop2_list_tail_head_upper_count_le >> 2497 `loop p q <= 2 + k * f n n` by metis_tac[] >> 2498 `k * f n n <= 7 * k + 2 * k * size n + k * size n ** 2` by 2499 (rw[Abbr`f`] >> 2500 qabbrev_tac `k = LENGTH q` >> 2501 `k * (size n + (size n * size (2 * n) + 7)) = 2502 k * size n + k * size n * size (2 * n) + 7 * k` by decide_tac >> 2503 `size (2 * n) <= 1 + size n` by rw[size_twice] >> 2504 `k * size n * size (2 * n) <= k * size n * (1 + size n)` by rw[] >> 2505 `k * size n * (1 + size n) = k * size n + k * size n * size n` by decide_tac >> 2506 `k * size n * size n = k * size n ** 2` by rw[] >> 2507 decide_tac) >> 2508 decide_tac); 2509 2510(* Theorem: Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 2511 stepsOf (poly_addM n p q) <= 12 * (MAX 1 k) * size n ** 2 *) 2512(* Proof: 2513 stepsOf (poly_addM n p q) 2514 <= 2 + 7 * k + 2 * k * size n + k * size n ** 2 by poly_addM_steps_upper 2515 <= (2 + 7 + 2 + 1) * k * size n ** 2 by dominant term 2516 = 12 * k * size n ** 2 2517 Use (MAX 1 k) to cater for k = 0. 2518*) 2519val poly_addM_steps_bound = store_thm( 2520 "poly_addM_steps_bound", 2521 ``!n p q k. Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 2522 stepsOf (poly_addM n p q) <= 12 * (MAX 1 k) * size n ** 2``, 2523 rpt strip_tac >> 2524 `stepsOf (poly_addM n p q) <= 2 + 7 * k + 2 * k * size n + k * size n ** 2` by rw[poly_addM_steps_upper] >> 2525 qabbrev_tac `m = MAX 1 k` >> 2526 qabbrev_tac `t = m * (size n) ** 2` >> 2527 `stepsOf (poly_addM n p q) <= 12 * t` suffices_by rw[Abbr`t`] >> 2528 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 2529 `0 < t` by rw[MULT_POS, Abbr`t`] >> 2530 `1 <= t` by decide_tac >> 2531 `k <= t` by 2532 (`m <= m * (size n) ** 2` by rw[MULT_POS] >> 2533 `m * (size n) ** 2 = t` by rw[Abbr`t`] >> 2534 decide_tac) >> 2535 `k * size n <= t` by 2536 (`k * size n <= m * size n` by rw[] >> 2537 `m * size n <= m * size n * size n` by rw[MULT_POS] >> 2538 `m * size n * size n = t` by rw[Abbr`t`] >> 2539 decide_tac) >> 2540 `k * size n ** 2 <= t` by 2541 (`k * size n ** 2 <= m * size n ** 2` by rw[] >> 2542 `m * size n ** 2 = t` by rw[Abbr`t`] >> 2543 decide_tac) >> 2544 decide_tac); 2545 2546(* ------------------------------------------------------------------------- *) 2547(* Polynomial multiplication by X in (mod n, unity k) *) 2548(* ------------------------------------------------------------------------- *) 2549 2550(* > LAST_DEF; 2551val it = |- !h t. LAST (h::t) = if t = [] then h else LAST t: thm 2552*) 2553 2554(* Pseudocode: 2555 Given a polynomial p, compute (LAST p). 2556 list_last p: 2557 if p = [], return (LAST []) // undefined 2558 h <- head p // get head 2559 t <- tail p // examine tail 2560 if t = [] then return h // no tail, head is LAST 2561 return list_last t // skip head, recursive call for (LAST tail) 2562*) 2563 2564val poly_lastM_def = tDefine "poly_lastM" ` 2565 poly_lastM p = 2566 do 2567 p0 <- nullM p; 2568 if p0 then return (LAST []) 2569 else do 2570 h <- headM p; 2571 t <- tailM p; 2572 t0 <- nullM t; 2573 if t0 then return h 2574 else poly_lastM t; 2575 od 2576 od 2577`(WF_REL_TAC `measure LENGTH` >> simp[LENGTH_TL_LT]); 2578 2579(* > FRONT_DEF; 2580val it = |- !h t. FRONT (h::t) = if t = [] then [] else h::FRONT t: thm 2581*) 2582 2583(* Pseudocode: 2584 Given a polynomial p, compute (FRONT p). 2585 list_front p: 2586 if p = [], return (FRONT []) // undefined 2587 h <- head p // get head 2588 t <- tail p // examine tail 2589 if t = [] return [] // no tail, FRONT = empty tail 2590 q <- list_front t // get (FRONT tail) 2591 return h::q // combine to give result 2592*) 2593 2594val poly_frontM_def = tDefine "poly_frontM" ` 2595 poly_frontM p = 2596 do 2597 p0 <- nullM p; 2598 if p0 then return (FRONT []) 2599 else do 2600 h <- headM p; 2601 t <- tailM p; 2602 t0 <- nullM t; 2603 if t0 then return [] 2604 else do 2605 q <- poly_frontM t; 2606 consM h q 2607 od 2608 od 2609 od 2610`(WF_REL_TAC `measure LENGTH` >> simp[LENGTH_TL_LT]); 2611 2612(* Pseudocode: 2613 Given a polynomial p, compute p * X (mod unity k), where k = LENGTH p. 2614 list_turn p: 2615 if p = [], return [] // [] * X = [] 2616 h <- LAST p // get (LAST p) 2617 t <- FRONT p // get (FRONT p) 2618 return h::t // combine to give result 2619*) 2620 2621(* Multiply a polynomial p by X, in (mod unity k). *) 2622val poly_turnM_def = Define` 2623 poly_turnM p = 2624 do 2625 p0 <- nullM p; 2626 if p0 then return [] 2627 else do 2628 h <- poly_lastM p; 2629 t <- poly_frontM p; 2630 consM h t; 2631 od 2632 od 2633`; 2634 2635(* 2636EVAL ``poly_lastM [1;2;4;5;3]``; = (3,Count 20): thm 2637EVAL ``poly_frontM [1;2;4;5;3]``; = ([1; 2; 4; 5],Count 24): thm 2638EVAL ``poly_turnM [1;2;4;5;3]``; = ([3; 1; 2; 4; 5],Count 46): thm 2639*) 2640 2641(* Theorem: valueOf (poly_lastM p) = LAST p *) 2642(* Proof: 2643 If p = [], 2644 valueOf (poly_lastM []) 2645 = LAST [] by poly_lastM_def 2646 If p <> [], let p = h::t. 2647 valueOf (poly_lastM p) 2648 = if t = [] then h else valueOf (poly_lastM t) 2649 by poly_lastM_def 2650 = if t = [] then h else LAST t by induction hypothesis 2651 = LAST (h::t) by LAST_DEF 2652*) 2653val poly_lastM_value = store_thm( 2654 "poly_lastM_value[simp]", 2655 ``!p. valueOf (poly_lastM p) = LAST p``, 2656 ho_match_mp_tac (theorem "poly_lastM_ind") >> 2657 rw[] >> 2658 (Cases_on `p` >> rw[Once poly_lastM_def] >> fs[LAST_DEF])); 2659 2660(* Theorem: valueOf (poly_frontM p) = FRONT p *) 2661(* Proof: 2662 If p = [], 2663 valueOf (poly_frontM []) 2664 = FRONT [] by poly_frontM_def 2665 If p <> [], let p = h::t. 2666 valueOf (poly_frontM p) 2667 = if t = [] then [] else h::valueOf (poly_frontM t) 2668 by poly_frontM_def 2669 = if t = [] then [] else h::FRONT t by induction hypothesis 2670 = FRONT (h::t) by FRONT_DEF 2671*) 2672val poly_frontM_value = store_thm( 2673 "poly_frontM_value[simp]", 2674 ``!p. valueOf (poly_frontM p) = FRONT p``, 2675 ho_match_mp_tac (theorem "poly_frontM_ind") >> 2676 rw[] >> 2677 (Cases_on `p` >> rw[Once poly_frontM_def] >> fs[FRONT_DEF])); 2678 2679(* Theorem: valueOf (poly_turnM p) = turn p *) 2680(* Proof: 2681 If p = [], 2682 valueOf (poly_turnM []) 2683 = [] by poly_turnM_def 2684 = turn [] by turn_nil 2685 If p <> [], 2686 valueOf (poly_turnM p) 2687 = LAST p :: FRONT p by poly_turnM_def 2688 = turn p by turn_def 2689*) 2690val poly_turnM_value = store_thm( 2691 "poly_turnM_value[simp]", 2692 ``!p. valueOf (poly_turnM p) = turn p``, 2693 rw[poly_turnM_def, turn_def]); 2694 2695(* Theorem: stepsOf (poly_lastM p) = 2696 if (p = []) then 1 else 4 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) *) 2697(* Proof: 2698 stepsOf (poly_lastM p) 2699 = stepsOf (nullM p) + if (p = []) then 0 2700 else stepsOf (headM p) + stepsOf (tailM p) + 2701 stepsOf (nullM t) + if (TL p = []) then 0 2702 else stepsOf (poly_lastM (TL p)) by poly_lastM_def 2703 = 1 + if (p = []) then 0 2704 else 1 + 1 + 1 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) 2705 = 1 + if (p = []) then 0 else 3 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) 2706 = if (p = []) then 1 else 4 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p)) 2707*) 2708val poly_lastM_steps_thm = store_thm( 2709 "poly_lastM_steps_thm", 2710 ``!p. stepsOf (poly_lastM p) = 2711 if (p = []) then 1 else 4 + if (TL p = []) then 0 else stepsOf (poly_lastM (TL p))``, 2712 ho_match_mp_tac (theorem "poly_lastM_ind") >> 2713 (rw[] >> rw[Once poly_lastM_def])); 2714 2715(* Theorem alias *) 2716val poly_lastM_steps_by_list_loop = save_thm("poly_lastM_steps_by_list_loop", poly_lastM_steps_thm); 2717 2718(* 2719This puts poly_lastM_steps in the category: list loop with body and exit. 2720 poly_lastM_steps_by_list_loop: 2721 !p. loop p = if (p = []) then c else body p + if exit p then 0 else loop (TL p) 2722suitable for: loop_list_count_exit_le 2723*) 2724 2725(* Theorem: stepsOf (poly_lastM p) <= 1 + 4 * LENGTH p *) 2726(* Proof: 2727 Let body = (\p. 4), 2728 exit = (\p. TL p = []), 2729 loop = (\p. stepsOf (poly_lastM p)). 2730 Then !x. loop x = if x = [] then 1 else body x + if exit x then 0 else loop (TL x) 2731 by poly_lastM_steps_thm 2732 Now !x y. x <= y ==> body x <= body y as body is constant 2733 Thus loop p <= 1 + body p * LENGTH p by loop_list_count_exit_le 2734 = 1 + 4 * LENGTH p 2735*) 2736val poly_lastM_steps_upper = store_thm( 2737 "poly_lastM_steps_upper", 2738 ``!p. stepsOf (poly_lastM p) <= 1 + 4 * LENGTH p``, 2739 rpt strip_tac >> 2740 qabbrev_tac `body = \p:'a list. 4` >> 2741 qabbrev_tac `exit = \p. TL p = []` >> 2742 qabbrev_tac `loop = \p. stepsOf (poly_lastM p)` >> 2743 `loop p <= 1 + 4 * LENGTH p` suffices_by rw[] >> 2744 `!x. loop x = if x = [] then 1 else body x + if exit x then 0 else loop (TL x)` by metis_tac[poly_lastM_steps_thm] >> 2745 `!x y. x <= y ==> body x <= body y` by rw[Abbr`body`] >> 2746 imp_res_tac loop_list_count_exit_le >> 2747 metis_tac[]); 2748 2749(* Theorem: stepsOf (poly_frontM p) = 2750 if (p = []) then 1 2751 else (4 + if (TL p = []) then 0 else 1) + 2752 (if (TL p = []) then 0 else stepsOf (poly_frontM (TL p))) *) 2753(* Proof: 2754 stepsOf (poly_frontM p) 2755 = stepsOf (nullM p) + if (p = []) then 0 2756 else stepsOf (headM p) + stepsOf (tailM p) + 2757 stepsOf (nullM t) + if (TL p = []) then 0 2758 else stepsOf (poly_frontM (TL p)) + stepsOf (consM (HD p) (FRONT (TL p))) 2759 by poly_frontM_def 2760 = 1 + if (p = []) then 0 2761 else 1 + 1 + 1 + if (TL p = []) then 0 else stepsOf (poly_frontM (TL p)) + 1 2762 = 1 + if (p = []) then 0 else 3 + if (TL p = []) then 0 else (1 + stepsOf (poly_frontM (TL p))) 2763 = if (p = []) then 1 else 4 + if (TL p = []) then 0 else (1 + stepsOf (poly_frontM (TL p))) 2764 = if (p = []) then 1 else (4 + if (TL p = []) then 0 else 1) + (if (TL p = []) then 0 else stepsOf (poly_frontM (TL p))) 2765*) 2766val poly_frontM_steps_thm = store_thm( 2767 "poly_frontM_steps_thm", 2768 ``!p. stepsOf (poly_frontM p) = 2769 if (p = []) then 1 2770 else (4 + if (TL p = []) then 0 else 1) + 2771 (if (TL p = []) then 0 else stepsOf (poly_frontM (TL p)))``, 2772 ho_match_mp_tac (theorem "poly_frontM_ind") >> 2773 (rw[] >> rw[Once poly_frontM_def])); 2774 2775(* Theorem alias *) 2776val poly_frontM_steps_by_list_loop = save_thm("poly_frontM_steps_by_list_loop", poly_frontM_steps_thm); 2777 2778(* 2779This puts poly_frontM_steps in the category: list loop with body cover and exit. 2780 poly_frontM_steps_by_list_loop: 2781 !p. loop p = if (p = []) then c else body p + if exit p then 0 else loop (TL p) 2782suitable for: loop_list_count_cover_exit_le 2783*) 2784 2785(* Theorem: stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p *) 2786(* Proof: 2787 Let body = (\p. 4 + if (TL p = []) then 0 else 1), 2788 cover = (\p. 5), 2789 exit = (\p. TL p = []), 2790 loop = (\p. stepsOf (poly_frontM p)). 2791 Then !p. loop p = if (p = []) then 1 else body p + if exit p then 0 else loop (TL p) 2792 by poly_frontM_steps_thm 2793 Now !x. body x <= cover x by cases on TL p, 2794 and !x y. x <= y ==> cover x <= cover y by cover being a constant 2795 Thus loop p <= 1 + cover p * LENGTH p by loop_list_count_cover_exit_le 2796 = 1 + 5 * LENGTH p 2797*) 2798val poly_frontM_steps_upper = store_thm( 2799 "poly_frontM_steps_upper", 2800 ``!p. stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p``, 2801 rpt strip_tac >> 2802 qabbrev_tac `body = \p. 4 + if (TL p = []) then 0 else 1` >> 2803 qabbrev_tac `cover = \p:'a list. 5` >> 2804 qabbrev_tac `exit = \p. TL p = []` >> 2805 qabbrev_tac `loop = \p. stepsOf (poly_frontM p)` >> 2806 `loop p <= 1 + 5 * LENGTH p` suffices_by rw[] >> 2807 `!x. loop x = if x = [] then 1 else body x + if exit x then 0 else loop (TL x)` by metis_tac[poly_frontM_steps_thm] >> 2808 `!x. body x <= cover x` by rw[Abbr`body`, Abbr`cover`] >> 2809 `!x y. x <= y ==> cover x <= cover y` by rw[Abbr`cover`] >> 2810 imp_res_tac loop_list_count_cover_exit_le >> 2811 metis_tac[]); 2812 2813(* Michael's proof of the same theorem. *) 2814 2815(* Theorem: stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p *) 2816(* Proof: 2817 Let body = (\p. 4 + if (TL p = []) then 0 else 1), 2818 exit = (\p. TL p = []), 2819 loop = (\p. stepsOf (poly_frontM p)). 2820 Then !p. loop p = if (p = []) then 1 else body p + if exit p then 0 else loop (TL p) 2821 by poly_frontM_steps_thm 2822 Now !x. body x <= 5 by cases on TL p, 2823 Thus loop p <= 1 + 5 * LENGTH p by loop_list_count_constant_cover_exit_le 2824*) 2825val poly_frontM_steps_upper = store_thm( 2826 "poly_frontM_steps_upper", 2827 ``!p. stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p``, 2828 ho_match_mp_tac loop_list_count_constant_cover_exit_le >> 2829 qexists_tac `\p. TL p = []` >> 2830 qexists_tac `\p. 4 + if (TL p = []) then 0 else 1` >> 2831 rw[Once poly_frontM_steps_thm]); 2832 2833(* Theorem: stepsOf (poly_turnM p) = 2834 if (p = []) then 1 else 2 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p) *) 2835(* Proof: 2836 stepsOf (poly_turnM p) 2837 = stepsOf (nullM p) + if (p = []) then 0 2838 else stepsOf (poly_lastM p) + stepsOf(poly_frontM p) + stepsOf (consM h q) by poly_turnM_def 2839 = 1 + if (p = []) then 0 else 1 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p) 2840 = if (p = []) then 1 else 2 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p) 2841*) 2842val poly_turnM_steps_thm = store_thm( 2843 "poly_turnM_steps_thm", 2844 ``!p. stepsOf (poly_turnM p) = 2845 if (p = []) then 1 else 2 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p)``, 2846 rw[poly_turnM_def]); 2847 2848(* Theorem: stepsOf (poly_turnM p) <= 4 + 9 * LENGTH p *) 2849(* Proof: 2850 stepsOf (poly_turnM p) 2851 = if (p = []) then 1 else 2 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p) 2852 by poly_turnM_steps_thm 2853 <= 2 + stepsOf (poly_lastM p) + stepsOf(poly_frontM p) 2854 <= 2 + (1 + 4 * LENGTH p) + (1 + 5 * LENGTH p) by poly_lastM_steps_upper, poly_frontM_steps_upper 2855 = 4 + 9 * LENGTH p 2856*) 2857val poly_turnM_steps_upper = store_thm( 2858 "poly_turnM_steps_upper", 2859 ``!p. stepsOf (poly_turnM p) <= 4 + 9 * LENGTH p``, 2860 rpt strip_tac >> 2861 assume_tac poly_turnM_steps_thm >> 2862 last_x_assum (qspec_then `p` strip_assume_tac) >> 2863 (Cases_on `p = []` >> fs[]) >> 2864 `stepsOf (poly_lastM p) <= 1 + 4 * LENGTH p` by rw[poly_lastM_steps_upper] >> 2865 `stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p` by rw[poly_frontM_steps_upper] >> 2866 decide_tac); 2867 2868(* Theorem: (LENGTH p = k) ==> stepsOf (poly_turnM p) <= 13 * MAX 1 k *) 2869(* Proof: 2870 stepsOf (poly_turnM p) 2871 <= 4 + 9 * k by poly_turnM_steps_upper 2872 <= (4 + 9) * (MAX 1 k) by MAX_DEF 2873 = 13 * MAX 1 k 2874*) 2875val poly_turnM_steps_bound = store_thm( 2876 "poly_turnM_steps_bound", 2877 ``!p k. (LENGTH p = k) ==> stepsOf (poly_turnM p) <= 13 * MAX 1 k``, 2878 rpt strip_tac >> 2879 `stepsOf (poly_turnM p) <= 4 + 9 * k` by rw[poly_turnM_steps_upper] >> 2880 qabbrev_tac `m = MAX 1 k` >> 2881 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 2882 decide_tac); 2883 2884(* Theorem: Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_turnM p)) *) 2885(* Proof: 2886 Weak (ZN n) (valueOf (poly_turnM p)) 2887 = Weak (ZN n) (turn p) by poly_turnM_value 2888 = T by weak_turn, Weak (ZN n) p 2889*) 2890val poly_turnM_weak = store_thm( 2891 "poly_turnM_weak", 2892 ``!n p. Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_turnM p))``, 2893 rw[weak_turn]); 2894 2895(* Theorem: LENGTH (valueOf (poly_turnM p)) = LENGTH p *) 2896(* Proof: 2897 LENGTH (valueOf (poly_turnM p)) 2898 = LENGTH (turn p) by poly_turnM_value 2899 = LENGTH p by turn_length 2900*) 2901val poly_turnM_length = store_thm( 2902 "poly_turnM_length", 2903 ``!p. LENGTH (valueOf (poly_turnM p)) = LENGTH p``, 2904 rw[turn_length]); 2905 2906(* ------------------------------------------------------------------------- *) 2907(* Exact number of steps *) 2908(* ------------------------------------------------------------------------- *) 2909 2910(* 2911EVAL ``MAP (\n. stepsOf (poly_lastM [1 .. n])) [0 .. 10]``; 2912= [1; 4; 8; 12; 16; 20; 24; 28; 32; 36; 40] 2913EVAL ``MAP (\n. stepsOf (poly_frontM [1 .. n])) [0 .. 10]``; 2914= [1; 4; 9; 14; 19; 24; 29; 34; 39; 44; 49] 2915*) 2916 2917(* Theorem: stepsOf (poly_lastM p) = if (p = []) then 1 else 4 * LENGTH p *) 2918(* Proof: 2919 By induction on p. 2920 Base: stepsOf (poly_lastM []) = if [] = [] then 1 else 4 * LENGTH [] 2921 LHS = stepsOf (poly_lastM []) = 1 by poly_lastM_steps_thm 2922 = RHS 2923 Step: stepsOf (poly_lastM p) = if (p = []) then 1 else 4 * LENGTH p ==> 2924 !h. stepsOf (poly_lastM (h::p)) = if h::(p = []) then 1 else 4 * LENGTH (h::p) 2925 Note h::(p = []) is false. 2926 stepsOf (poly_lastM (h::p)) 2927 = 4 + if TL (h::p) = [] then 0 else stepsOf (poly_lastM (TL (h::p))) 2928 by poly_lastM_steps_thm 2929 = 4 + if (p = []) then 0 else stepsOf (poly_lastM p) 2930 = 4 + if (p = []) then 0 else 4 * LENGTH p 2931 by induction hypothesis 2932 = 4 + if (p = []) then 4 * LENGTH p else 4 * LENGTH p 2933 by LENGTH_NIL 2934 = 4 + 4 * LENGTH p 2935 = 4 * LENGTH (h::p) by LENGTH 2936*) 2937val poly_lastM_steps_eqn = store_thm( 2938 "poly_lastM_steps_eqn", 2939 ``!p. stepsOf (poly_lastM p) = if (p = []) then 1 else 4 * LENGTH p``, 2940 (Induct >> rw[Once poly_lastM_steps_thm])); 2941 2942(* Theorem: stepsOf (poly_frontM p) = if (p = []) then 1 else (5 * LENGTH p - 1) *) 2943(* Proof: 2944 By induction on p. 2945 Base: stepsOf (poly_frontM []) = if [] = [] then 1 else 5 * LENGTH [] - 1 2946 LHS = stepsOf (poly_frontM []) = 1 by poly_frontM_steps_thm 2947 = RHS 2948 Step: stepsOf (poly_frontM p) = if (p = []) then 1 else 5 * LENGTH p - 1 ==> 2949 !h. stepsOf (poly_frontM (h::p)) = if h::(p = []) then 1 else 5 * LENGTH (h::p) - 1 2950 Note h::(p = []) is false. 2951 stepsOf (poly_frontM (h::p)) 2952 = 4 + (if TL (h::p) = [] then 0 else 1) + 2953 if TL (h::p) = [] then 0 else stepsOf (poly_frontM (TL (h::p))) 2954 by poly_frontM_steps_thm 2955 = 4 + (if (p = []) then 0 else 1) + 2956 if (p = []) then 0 else stepsOf (poly_frontM p) 2957 = 4 + (if (p = []) then 0 else 1) + 2958 if (p = []) then 0 else (5 * LENGTH p - 1) 2959 by induction hypothesis 2960 = 4 + (if (p = []) then 5 * LENGTH p else 1) + 2961 if (p = []) then 5 * LENGTH p else (5 * LENGTH p - 1) 2962 by LENGTH_NIL 2963 = 4 + if (p = []) then 5 * LENGTH p else 5 * LENGTH p 2964 = 4 + 5 * LENGTH p 2965 = 5 * LENGTH (h::p) - 1 by LENGTH 2966*) 2967val poly_frontM_steps_eqn = store_thm( 2968 "poly_frontM_steps_eqn", 2969 ``!p. stepsOf (poly_frontM p) = if (p = []) then 1 else (5 * LENGTH p - 1)``, 2970 Induct >- 2971 rw[Once poly_frontM_steps_thm] >> 2972 rw[Once poly_frontM_steps_thm] >> 2973 `LENGTH p <> 0` by rw[LENGTH_NIL] >> 2974 decide_tac); 2975 2976(* Theorem: stepsOf (poly_turnM p) = if (p = []) then 1 else (1 + 9 * LENGTH p) *) 2977(* Proof: 2978 stepsOf (poly_turnM p) 2979 = if (p = []) then 1 else 2 + stepsOf (poly_lastM p) + stepsOf (poly_frontM p) 2980 by poly_turnM_steps_thm 2981 = if (p = []) then 1 else 2 + 2982 (if (p = []) then 1 else 4 * LENGTH p) + by poly_lastM_steps_eqn 2983 (if (p = []) then 1 else 5 * LENGTH p - 1) by poly_frontM_steps_eqn 2984 = if (p = []) then 1 else (2 + 4 * LENGTH p + 5 * LENGTH p - 1) 2985 = if (p = []) then 1 else (1 + 9 * LENGTH p) 2986*) 2987val poly_turnM_steps_eqn = store_thm( 2988 "poly_turnM_steps_eqn", 2989 ``!p. stepsOf (poly_turnM p) = if (p = []) then 1 else (1 + 9 * LENGTH p)``, 2990 rw[poly_turnM_steps_thm, poly_lastM_steps_eqn, poly_frontM_steps_eqn] >> 2991 `LENGTH p <> 0` by rw[LENGTH_NIL] >> 2992 decide_tac); 2993 2994(* ------------------------------------------------------------------------- *) 2995 2996(* Multiply polynomials p q, both of length k, in (MOD (unity k)) *) 2997(* > poly_slide_def; 2998|- (!r p1 p2. poly_slide r p1 p2 [] = p1) /\ 2999 !r p1 p2 h t. poly_slide r p1 p2 (h::t) = poly_slide r (h o p2 || p1) (turn p2) t 3000> unity_mod_mult_def 3001|- !r p q. unity_mod_mult r p q = poly_slide r |0| p q 3002*) 3003 3004(* Pseudocode: 3005 Given modulus n, and polynomials p and q, compute p o q (mod n). 3006 list_mult p q: 3007 if p = [], return [] // [] o q = [] 3008 if q = [], return [] // p o [] = [] 3009 h <- head q // get head of q 3010 t <- tail q // get tail of q 3011 p1 <- list_cmult h p // use head for list_cmult with p 3012 p2 <- list_mult (list_turn p) t // use tail for list_mult with (turn p) 3013 return list_add p1 p2 // add the results, pair-wise 3014*) 3015 3016val poly_multM_def = tDefine "poly_multM" ` 3017 poly_multM n p q = 3018 do 3019 q0 <- nullM q; 3020 if q0 then return [] 3021 else do 3022 h <- headM q; 3023 t <- tailM q; 3024 p1 <- poly_cmultM n h p; 3025 r <- poly_turnM p; 3026 p2 <- poly_multM n r t; 3027 poly_addM n p1 p2; 3028 od 3029 od 3030`(WF_REL_TAC `measure (\(n,p,q). LENGTH q)` >> simp[LENGTH_TL_LT]); 3031(* Note: the final poly_addM n p1 p2 can also be poly_addM n p2 p1, as addition is commutative. 3032 However, the commutative property depends on Ring (ZN n) and weak polynomials. 3033 To avoid this complication, use of poly_addM n p1 p2 fits unity_mod_mult_cons. *) 3034 3035(* 3036> EVAL ``poly_multM 10 [1;1;0;0;0;0;0] [1;1;0;0;0;0;0]``; = ([1; 2; 1; 0; 0; 0; 0],Count 1440): thm 3037> EVAL ``poly_multM 10 [1;1;0;0;0;0;0] [1;2;1;0;0;0;0]``; = ([1; 3; 3; 1; 0; 0; 0],Count 1471): thm 3038*) 3039 3040(* 3041 3042> EVAL ``poly_slide (ZN 10) [6] [1;2] [4;5]``; = [0; 3]: thm 3043> EVAL ``weak_add (ZN 10) [6] (poly_slide (ZN 10) [] [1;2] [4;5])``; = [0; 3]: thm 3044> EVAL ``weak_add (ZN 10) [6] (poly_slide (ZN 10) [7;8] [1;2] [4;5])``; = [7; 1]: thm 3045> EVAL ``poly_slide (ZN 10) (weak_add (ZN 10) [6] [7;8]) [1;2] [4;5]``; = [7; 1]: thm 3046 3047Thus: poly_slide r (t1 || t2) p q = t1 || poly_slide r t2 p q 3048 3049Conceptually this is simple: t1 || t2 is just the accumulator of partial result. 3050Indeed, poly_slide r |0| p q is supposed to do weak_mult of p and q, 3051and poly_slide r t p q is just weak_add t to this result, or t || poly_slide r |0| p q. 3052 3053*) 3054 3055(* 3056> unity_mod_mult_cons |> ISPEC ``(ZN n)`` |> SIMP_RULE bool_ss [ZN_property]; 3057val it = |- Ring (ZN n) ==> !p h t. Weak (ZN n) p /\ Weak (ZN n) (h::t) ==> 3058 unity_mod_mult (ZN n) p (h::t) = 3059 weak_add (ZN n) (weak_cmult (ZN n) h p) (unity_mod_mult (ZN n) (turn p) t): thm 3060*) 3061 3062(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3063 (valueOf (poly_multM n p q) = unity_mod_mult (ZN n) p q) *) 3064(* Proof: 3065 By induction from poly_multM_def. 3066 If q = [], 3067 valueOf (poly_multM n p []) 3068 = [] by poly_multM_def 3069 = unity_mod_mult (ZN n) p [] by unity_mod_mult_zero 3070 Otherwise, p <> [] and q <> []. 3071 Let q = h::t 3072 valueOf (poly_multM n p (h::t)) 3073 = (h o p || valueOf (poly_multM n (turn p) t) by poly_multM_def 3074 = (h o p || unity_mod_mult (ZN n) (turn p) t) by induction hypothesis 3075 = unity_mod_mult (ZN n) p (h::t) by unity_mod_mult_cons 3076*) 3077val poly_multM_value = store_thm( 3078 "poly_multM_value[simp]", 3079 ``!n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3080 (valueOf (poly_multM n p q) = unity_mod_mult (ZN n) p q)``, 3081 ho_match_mp_tac (theorem "poly_multM_ind") >> 3082 rw[] >> 3083 rw[Once poly_multM_def] >- 3084 metis_tac[unity_mod_mult_zero, poly_zero] >> 3085 (Cases_on `q` >> rw[ZN_property]) >> 3086 `Ring (ZN n)` by rw[ZN_ring] >> 3087 `Weak (ZN n) t` by metis_tac[weak_cons] >> 3088 rw[unity_mod_mult_cons, weak_turn]); 3089 3090(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] /\ (LENGTH p = k) ==> 3091 (valueOf (poly_multM n p q) = p *z q) *) 3092(* Proof: by poly_multM_value, ZN_poly_mult_alt *) 3093val poly_multM_value_thm = store_thm( 3094 "poly_multM_value_thm", 3095 ``!n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] /\ (LENGTH p = k) ==> 3096 (valueOf (poly_multM n p q) = p *z q)``, 3097 metis_tac[ZN_poly_mult_alt, poly_multM_value]); 3098 3099(* Above q <> [] is the minimal requirement. Next with 0 < k is symmetric. *) 3100 3101(* Theorem: 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 3102 (LENGTH p = k) /\ (LENGTH q = k) ==> (valueOf (poly_multM n p q) = p *z q) *) 3103(* Proof: by poly_multM_value_thm, LENGTH_NIL *) 3104val poly_multM_value_alt = store_thm( 3105 "poly_multM_value_alt", 3106 ``!n p q k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 3107 (LENGTH p = k) /\ (LENGTH q = k) ==> (valueOf (poly_multM n p q) = p *z q)``, 3108 metis_tac[poly_multM_value_thm, LENGTH_NIL, NOT_ZERO]); 3109 3110(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3111 Weak (ZN n) (valueOf (poly_multM n p q)) *) 3112(* Proof: 3113 Note Ring (ZN n) by 0 < n 3114 Weak (ZN n) (valueOf (poly_multM n p q)) 3115 = Weak (ZN n) (unity_mod_mult (ZN n) p q)) by poly_multM_value 3116 = T by unity_mod_mult_weak, Ring (ZN n) 3117*) 3118val poly_multM_weak = store_thm( 3119 "poly_multM_weak", 3120 ``!n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3121 Weak (ZN n) (valueOf (poly_multM n p q))``, 3122 rw[unity_mod_mult_weak, ZN_ring]); 3123 3124(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3125 LENGTH (valueOf (poly_multM n p q)) = if q = [] then 0 else LENGTH p *) 3126(* Proof: 3127 LENGTH (valueOf (poly_multM n p q)) 3128 = LENGTH (unity_mod_mult (ZN n) p q)) by poly_multM_value 3129 = if q = [] then 0 else LENGTH p by unity_mod_mult_length 3130*) 3131val poly_multM_length = store_thm( 3132 "poly_multM_length", 3133 ``!n p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3134 LENGTH (valueOf (poly_multM n p q)) = if q = [] then 0 else LENGTH p``, 3135 rw[unity_mod_mult_length]); 3136 3137(* Theorem: 0 < n /\ Weak (ZN n) p ==> (valueOf (poly_multM n p []) = []) *) 3138(* Proof: 3139 Note Weak (ZN n) [] by weak_zero 3140 and LENGTH (valueOf (poly_multM n p [])) = 0 by poly_multM_length 3141 Thus valueOf (poly_multM n p []) = [] by LENGTH_NIL 3142*) 3143val poly_multM_nil = store_thm( 3144 "poly_multM_nil", 3145 ``!n p. 0 < n /\ Weak (ZN n) p ==> (valueOf (poly_multM n p []) = [])``, 3146 rpt strip_tac >> 3147 `Weak (ZN n) []` by rw[] >> 3148 metis_tac[poly_multM_length, LENGTH_NIL]); 3149 3150(* Theorem: stepsOf (poly_multM n p q) = 3151 if q = [] then 1 3152 else 3 + stepsOf (poly_turnM p) + 3153 stepsOf (poly_cmultM n (HD q) p) + 3154 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) + 3155 stepsOf (poly_multM n (turn p) (TL q)) *) 3156(* Proof: 3157 stepsOf (poly_multM n p q) 3158 = stepsOf (nullM q) + if (q = []) then 0 3159 else stepsOf (headM q) + stepsOf (tailM q) + 3160 stepsOf (poly_turnM p) + stepsOf (poly_multM n (turn p) (TL q)) + 3161 stepsOf (poly_cmultM n (HD q) p) + 3162 stepsOf (poly_addM n (HD q o p) (unity_mod_mult (ZN n) (turn p) (TL q))) 3163 by poly_multM_def 3164 = 1 + if q = [] then 0 3165 else 1 + 1 + 3166 stepsOf (poly_turnM p) + stepsOf (poly_multM n (turn p) (TL q)) + 3167 stepsOf (poly_cmultM n (HD q) p) + 3168 stepsOf (poly_addM n (weak_cult (ZN n) (HD q) p) ((turn p) * (TL q))) 3169 = if q = [] then 1 else 3 + 3170 stepsOf (poly_turnM p) + 3171 stepsOf (poly_cmultM n (HD q) p) + 3172 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (unity_mod_mult (ZN n) (turn p) (TL q))) + 3173 stepsOf (poly_multM n (turn p) (TL q)) 3174 from Weak (ZN n) (turn p) by weak_turn 3175 and Weak (ZN n) (TL q) by weak_cons 3176 However, this requires knowing poly_multM_value. 3177 For an unconditional expression, 3178 = if q = [] then 1 else 3 + 3179 stepsOf (poly_turnM p) + 3180 stepsOf (poly_cmultM n (HD q) p) + 3181 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) + 3182 stepsOf (poly_multM n (turn p) (TL q)) 3183*) 3184val poly_multM_steps_thm = store_thm( 3185 "poly_multM_steps_thm", 3186 ``!n p q. stepsOf (poly_multM n p q) = 3187 if q = [] then 1 3188 else 3 + stepsOf (poly_turnM p) + 3189 stepsOf (poly_cmultM n (HD q) p) + 3190 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) + 3191 stepsOf (poly_multM n (turn p) (TL q))``, 3192 ho_match_mp_tac (theorem "poly_multM_ind") >> 3193 (rw[] >> rw[Once poly_multM_def, weak_turn])); 3194(* The unconditional from is more useful. *) 3195 3196(* Theorem: stepsOf (poly_multM n p []) = 1 *) 3197(* Proof: by poly_multM_steps_thm *) 3198val poly_multM_steps_nil = store_thm( 3199 "poly_multM_steps_nil", 3200 ``!n p. stepsOf (poly_multM n p []) = 1``, 3201 rw[Once poly_multM_steps_thm]); 3202 3203(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3204 (stepsOf (poly_multM n p [c]) = 3205 6 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n c p)) *) 3206(* Proof: 3207 stepsOf (poly_multM n p [c]) 3208 = 3 + stepsOf (poly_turnM p) + 3209 stepsOf (poly_cmultM n c p) + 3210 stepsOf (poly_addM n (weak_cmult (ZN n) c p) (valueOf (poly_multM n (turn p) []))) + 3211 stepsOf (poly_multM n (turn p) []) by poly_multM_steps_thm 3212 = 3 + stepsOf (poly_turnM p) + 3213 stepsOf (poly_cmultM n c p) + 3214 stepsOf (poly_addM n (weak_cmult (ZN n) c p) (unity_mod_mult (ZN n) (turn p) [])) + 3215 1 by poly_multM_steps_thm 3216 = 3 + stepsOf (poly_turnM p) + 3217 stepsOf (poly_cmultM n c p) + 3218 stepsOf (poly_addM n (weak_cmult (ZN n) c p) []) + 3219 1 by unity_mod_mult_length, LENGTH_NIL 3220 = 3 + stepsOf (poly_turnM p) + 3221 stepsOf (poly_cmultM n c p) + 3222 2 + 1 by poly_addM_steps_thm 3223 = 6 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n c p) 3224*) 3225val poly_multM_steps_sing_thm = store_thm( 3226 "poly_multM_steps_sing_thm", 3227 ``!n p c. 0 < n /\ Weak (ZN n) p ==> 3228 (stepsOf (poly_multM n p [c]) = 3229 6 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n c p))``, 3230 rw[Once poly_multM_steps_thm] >> 3231 rw[Once poly_multM_steps_thm] >> 3232 qabbrev_tac `q = valueOf (poly_multM n (turn p) [])` >> 3233 `q = []` by rw[poly_multM_nil, weak_turn, Abbr`q`] >> 3234 `stepsOf (poly_addM n (weak_cmult (ZN n) c p) q) = 2` by rw[Once poly_addM_steps_thm] >> 3235 decide_tac); 3236 3237(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3238 stepsOf (poly_multM n p [c]) <= 3239 10 + 9 * k + 8 * MAX 1 k * size (MAX c n) * size n *) 3240(* Proof: 3241 stepsOf (poly_multM n p [c]) 3242 = 6 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n c p) by poly_multM_steps_sing_thm 3243 <= 6 + (4 + 9 * k) + (8 * MAX 1 k * size (MAX c n) * size n) by poly_turnM_steps_upper, poly_cmultM_steps_bound 3244 = 10 + 9 * k + 8 * MAX 1 k * size (MAX c n) * size n 3245*) 3246val poly_multM_steps_sing_upper = store_thm( 3247 "poly_multM_steps_sing_upper", 3248 ``!n p c k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3249 stepsOf (poly_multM n p [c]) <= 10 + 9 * k + 8 * MAX 1 k * size (MAX c n) * size n``, 3250 rpt strip_tac >> 3251 imp_res_tac poly_multM_steps_sing_thm >> 3252 first_x_assum (qspec_then `c` strip_assume_tac) >> 3253 `stepsOf (poly_turnM p) <= 4 + 9 * k` by rw[poly_turnM_steps_upper] >> 3254 `stepsOf (poly_cmultM n c p) <= 8 * MAX 1 k * size (MAX c n) * size n` by rw[poly_cmultM_steps_bound] >> 3255 decide_tac); 3256 3257(* Theorem: 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3258 stepsOf (poly_multM n p [c]) <= 27 * MAX 1 k * size (MAX c n) * size n *) 3259(* Proof: 3260 Let k = LENGTH p. 3261 stepsOf (poly_multM n p [c]) 3262 <= 10 + 9 * k + 8 * MAX 1 k * size (MAX c n) * size n by poly_multM_steps_sing_upper 3263 <= (10 + 9 + 8) * MAX 1 k * size (MAX c n) * size n by dominant term 3264 = 27 * MAX 1 k * size (MAX c n) * size n 3265*) 3266val poly_multM_steps_sing_bound = store_thm( 3267 "poly_multM_steps_sing_bound", 3268 ``!n p c k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3269 stepsOf (poly_multM n p [c]) <= 27 * MAX 1 k * size (MAX c n) * size n``, 3270 rpt strip_tac >> 3271 imp_res_tac poly_multM_steps_sing_upper >> 3272 first_x_assum (qspec_then `c` strip_assume_tac) >> 3273 qabbrev_tac `m = MAX 1 k` >> 3274 qabbrev_tac `d = MAX c n` >> 3275 `0 < m * size d * size n` by rw[MULT_POS, Abbr`m`] >> 3276 `k <= m` by rw[Abbr`m`] >> 3277 `m <= m * (size d * size n)` by rw[MULT_POS] >> 3278 decide_tac); 3279 3280 3281(* Theorem alias *) 3282val poly_multM_steps_by_list_loop = save_thm("poly_multM_steps_by_list_loop", poly_multM_steps_thm); 3283 3284(* 3285This puts poly_multM_steps in the category: list loop with body cover and turn transform. 3286 poly_multM_steps_by_list_loop: 3287 !p q. loop p q = if q = [] then quit p else body p q + loop (turn p) (TL q) 3288suitable for: loop2_list_turn_head_count_cover_le 3289*) 3290 3291(* First, work out a cover for the body. *) 3292 3293(* Theorem: let body p q = 3 + stepsOf (poly_turnM p) + 3294 stepsOf (poly_cmultM n (HD q) p) + 3295 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) 3296 in !p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] ==> 3297 body p q <= 10 + (LENGTH p) * (20 + 2 * size n + 4 * size n ** 2) *) 3298(* Proof: 3299 Weak (ZN n) p, k = LENGTH p, 3300 Let body = (\p q. 3 + stepsOf (poly_turnM p) + 3301 stepsOf (poly_cmultM n (HD q) p) + 3302 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q))))) 3303 body p q 3304 = 3 + stepsOf (poly_turnM p) 3305 + stepsOf (poly_cmultM n (HD q) p) 3306 + stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q))))) 3307 <= 3 + (4 + 9 * k) by poly_turnM_steps_upper 3308 + (1 + 4 * k + 2 * k * size (HD q) * size n + k * size n ** 2) by poly_cmultM_steps_upper 3309 + (2 + 7 * k + 2 * k * size n + k * size n ** 2) by poly_addM_steps_upper 3310 last one assumes: 3311 TL q <> [], otherwise only gives 2, which is ok by poly_addM_steps_thm 3312 LENGTH (weak_cmult (ZN n) (HD q) p) = k by weak_cmult_length 3313 LENGTH (valueOf (poly_multM n (turn p) (TL q))) = k 3314 unity_mod_mult (ZN n) (turn p) (TL q) by unity_mod_mult_length, turn_length, TL q <> [] 3315 Weak (ZN n) (weak_cmult (ZN n) (HD q) p) by weak_cmult_weak, 0 < n, Ring (ZN n), (HD q) IN (ZN n).carrier 3316 Weak (ZN n) (valueOf (poly_multM n (turn p) (TL q))) by unity_mod_mult_weak 3317 = 10 + 20 * k + 2 * k * size n * (1 + size (HD q)) + 2 * k * size n ** 2 3318 <= 10 + 20 * k + 2 * k * size n * (1 + size n) + 2 * k * size n ** 2 by Weak (ZN n) q, size_monotone_lt 3319 = 10 + k * (20 + 2 * size n * (1 + size n) + 2 * size n ** 2) 3320 = 10 + k * (20 + 2 * size n + 4 * size n ** 2) 3321 For a fixed n, this is a function of k = LENGTH p! 3322*) 3323val poly_multM_steps_body_upper = store_thm( 3324 "poly_multM_steps_body_upper", 3325 ``!n. let body p q = 3 + stepsOf (poly_turnM p) + 3326 stepsOf (poly_cmultM n (HD q) p) + 3327 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) 3328 in !p q. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ q <> [] ==> 3329 body p q <= 10 + (LENGTH p) * (20 + 2 * size n + 4 * size n ** 2)``, 3330 rw_tac std_ss[] >> 3331 qabbrev_tac `k = LENGTH p` >> 3332 `Weak (ZN n) (turn p)` by rw[weak_turn] >> 3333 `Weak (ZN n) (TL q)` by metis_tac[weak_cons, TL, list_CASES] >> 3334 `valueOf (poly_multM n (turn p) (TL q)) = unity_mod_mult (ZN n) (turn p) (TL q)` by rw[poly_multM_value] >> 3335 `body p q = 3 + stepsOf (poly_turnM p) 3336 + stepsOf (poly_cmultM n (HD q) p) 3337 + stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (unity_mod_mult (ZN n) (turn p) (TL q)))` by metis_tac[] >> 3338 qabbrev_tac `ct = stepsOf (poly_turnM p)` >> 3339 qabbrev_tac `cc = stepsOf (poly_cmultM n (HD q) p)` >> 3340 qabbrev_tac `ca = stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (unity_mod_mult (ZN n) (turn p) (TL q)))` >> 3341 `ct <= 4 + 9 * k` by rw[poly_turnM_steps_upper, Abbr`ct`, Abbr`k`] >> 3342 `cc <= 1 + 4 * k + 3 * k * size n ** 2` by 3343 (`cc <= 1 + 4 * k + 2 * k * size (HD q) * size n + k * size n ** 2` by rw[poly_cmultM_steps_upper, Abbr`cc`, Abbr`k`] >> 3344 `EVERY (\j. j < n) q` by rw[GSYM ZN_weak] >> 3345 `HD q = EL 0 q` by rw[] >> 3346 `0 < LENGTH q` by metis_tac[LENGTH_NIL, NOT_ZERO] >> 3347 qabbrev_tac `P = \j. j < n` >> 3348 `!j. P j = (j < n)` by rw[Abbr`P`] >> 3349 `HD q < n` by metis_tac[EVERY_EL] >> 3350 `size (HD q) <= size n` by rw[size_monotone_lt] >> 3351 `k * size (HD q) * size n <= k * size n * size n` by rw[] >> 3352 `k * size n * size n = k * size n ** 2` by rw[] >> 3353 decide_tac) >> 3354 `ca <= 2 + 7 * k + 2 * k * size n + k * size n ** 2` by 3355 (qabbrev_tac `p1 = weak_cmult (ZN n) (HD q) p` >> 3356 qabbrev_tac `q1 = unity_mod_mult (ZN n) (turn p) (TL q)` >> 3357 Cases_on `TL q = []` >| [ 3358 `q1 = []` by metis_tac[unity_mod_mult_zero, poly_zero] >> 3359 `ca = 2` by metis_tac[poly_addM_steps_thm] >> 3360 decide_tac, 3361 `LENGTH p1 = k` by metis_tac[weak_cmult_length] >> 3362 `LENGTH q1 = k` by metis_tac[unity_mod_mult_length, turn_length] >> 3363 `Ring (ZN n)` by rw[ZN_ring] >> 3364 `(HD q) IN (ZN n).carrier` by metis_tac[weak_cons, HD, list_CASES] >> 3365 `Weak (ZN n) p1` by rw[weak_cmult_weak, Abbr`p1`] >> 3366 `Weak (ZN n) q1` by metis_tac[unity_mod_mult_weak] >> 3367 metis_tac[poly_addM_steps_upper] 3368 ]) >> 3369 decide_tac); 3370 3371(* Theorem: let body p q = 3 + stepsOf (poly_turnM p) + 3372 stepsOf (poly_cmultM n (HD q) p) + 3373 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) 3374 in !p q k. 0 < n /\ (LENGTH p = k) /\ (LENGTH q = k) /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3375 !j. j < k ==> body (turn_exp p j) (DROP j q) <= 10 + k * (20 + 2 * size n + 4 * size n ** 2) *) 3376(* Proof: 3377 Let p1 = turn_exp p j, 3378 q1 = DROP j q. 3379 3380 To apply poly_multM_steps_body_upper, require: 3381 0 < n /\ Weak (ZN n) p1 /\ Weak (ZN n) q1 /\ q1 <> [] ==> 3382 body p1 q1 <= 10 + (LENGTH p1) * (20 + 2 * size n + 4 * size n ** 2) 3383 3384 Note Weak (ZN n) p1 by weak_turn_exp 3385 and Weak (ZN n) q1 by weak_drop 3386 Also q1 <> [] by DROP_EQ_NIL, j < k = LENGTH q 3387 and LENGTH p1 = k by turn_exp_length 3388 The result follows by poly_multM_steps_body_upper 3389*) 3390val poly_multM_steps_body_cover = store_thm( 3391 "poly_multM_steps_body_cover", 3392 ``!n. let body p q = 3 + stepsOf (poly_turnM p) + 3393 stepsOf (poly_cmultM n (HD q) p) + 3394 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q)))) 3395 in !p q k. 0 < n /\ (LENGTH p = k) /\ (LENGTH q = k) /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3396 !j. j < k ==> body (turn_exp p j) (DROP j q) <= 10 + k * (20 + 2 * size n + 4 * size n ** 2)``, 3397 rw_tac std_ss[] >> 3398 qabbrev_tac `k = LENGTH p` >> 3399 qabbrev_tac `p1 = turn_exp p j` >> 3400 qabbrev_tac `q1 = DROP j q` >> 3401 `Weak (ZN n) p1` by rw[weak_turn_exp, Abbr`p1`] >> 3402 `Weak (ZN n) q1` by rw[weak_drop, Abbr`q1`] >> 3403 `q1 <> []` by rw[DROP_EQ_NIL, Abbr`q1`] >> 3404 `LENGTH p1 = k` by rw[turn_exp_length, Abbr`p1`] >> 3405 metis_tac[poly_multM_steps_body_upper]); 3406 3407(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 3408 stepsOf (poly_multM n p q) <= 3409 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2 *) 3410(* Proof: 3411 Let quit = (\p. 1), 3412 body = (\p q. 3 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n (HD q) p) + 3413 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q))))), 3414 loop = (\p q. stepsOf (poly_multM n p q)). 3415 Then !p q. loop p q = if (q = []) then quit p else body p q + loop (turn p) (TL q) 3416 by poly_multM_steps_thm 3417 Let c = 10 + k * (20 + 2 * (size n) + 4 * size n ** 2. 3418 Then !j. j < k ==> body (turn_exp p j) (DROP j q) <= (K c) j 3419 by poly_multM_steps_body_cover 3420 and MONO (K c) by constant function 3421 loop p q 3422 <= quit (turn_exp x k) + k * (K c) k by loop2_list_turn_head_count_cover_le 3423 = 1 + k * c by applicaiton of (K c), quit 3424 = 1 + k * (10 + k * (20 + 2 * (size n) + 4 * size n ** 2)) 3425 = 1 + 10 * k + k * k * (20 + 2 * (size n) + 4 * size n ** 2) 3426 = 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2 3427*) 3428val poly_multM_steps_upper = store_thm( 3429 "poly_multM_steps_upper", 3430 ``!n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 3431 stepsOf (poly_multM n p q) <= 3432 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2``, 3433 rpt strip_tac >> 3434 qabbrev_tac `quit = \p:num list. 1` >> 3435 qabbrev_tac `body = \p q. 3 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n (HD q) p) + 3436 stepsOf (poly_addM n (weak_cmult (ZN n) (HD q) p) (valueOf (poly_multM n (turn p) (TL q))))` >> 3437 qabbrev_tac `loop = \p q. stepsOf (poly_multM n p q)` >> 3438 `loop p q <= 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2` suffices_by rw[Abbr`loop`] >> 3439 `!x y. loop x y = if (y = []) then quit x else body x y + loop (turn x) (TL y)` by metis_tac[poly_multM_steps_thm] >> 3440 qabbrev_tac `c = 10 + k * (20 + 2 * (size n) + 4 * size n ** 2)` >> 3441 `!j. j < k ==> body (turn_exp p j) (DROP j q) <= (K c) j` by metis_tac[poly_multM_steps_body_cover, combinTheory.K_THM] >> 3442 `MONO (K c)` by rw[] >> 3443 imp_res_tac loop2_list_turn_head_count_cover_le >> 3444 `loop p q <= 1 + k * (K c) k` by metis_tac[] >> 3445 `1 + k * (K c) k = 1 + k * c` by rw[] >> 3446 `k * c = k * (10 + k * 20 + 2 * k * size n + 4 * k * size n ** 2)` by rw[Abbr`c`] >> 3447 `_ = 10 * k + 20 * (k * k) + 2 * (k * k) * size n + 4 * (k * k) * size n ** 2` by decide_tac >> 3448 `_ = 10 * k + 20 * (k ** 2) + 2 * (k ** 2) * size n + 4 * (k ** 2) * size n ** 2` by rw[] >> 3449 decide_tac); 3450 3451(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 3452 stepsOf (poly_multM n p q) <= 37 * (MAX 1 k) ** 2 * size n ** 2 *) 3453(* Proof: 3454 stepsOf (poly_multM n p q) 3455 <= 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2 3456 by poly_multM_steps_upper 3457 <= (1 + 10 + 20 + 2 + 4) * k ** 2 * size n ** 2 by dominant term 3458 = 37 * k ** 2 * size n ** 2 3459 Use (MAX 1 k) to cater for k = 0. 3460*) 3461val poly_multM_steps_bound = store_thm( 3462 "poly_multM_steps_bound", 3463 ``!n p q k. 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q /\ (LENGTH p = k) /\ (LENGTH q = k) ==> 3464 stepsOf (poly_multM n p q) <= 37 * (MAX 1 k) ** 2 * size n ** 2``, 3465 rpt strip_tac >> 3466 `stepsOf (poly_multM n p q) <= 3467 1 + 10 * k + 20 * k ** 2 + 2 * k ** 2 * size n + 4 * k ** 2 * size n ** 2` by rw[poly_multM_steps_upper] >> 3468 qabbrev_tac `m = MAX 1 k` >> 3469 qabbrev_tac `t = m ** 2 * size n ** 2` >> 3470 `stepsOf (poly_multM n p q) <= 37 * t` suffices_by rw[Abbr`t`] >> 3471 `1 <= m /\ k <= m` by rw[Abbr`m`] >> 3472 `0 < t` by rw[MULT_POS, Abbr`t`] >> 3473 `1 <= t` by decide_tac >> 3474 `k <= t` by 3475 (`m <= m * (m * size n ** 2)` by rw[MULT_POS] >> 3476 `m * (m * size n ** 2) = t` by rw[Abbr`t`] >> 3477 decide_tac) >> 3478 `k ** 2 <= t` by 3479 (`k ** 2 <= m ** 2` by rw[] >> 3480 `m ** 2 <= m ** 2 * size n ** 2` by rw[MULT_POS] >> 3481 `m ** 2 * size n ** 2 = t` by rw[Abbr`t`] >> 3482 decide_tac) >> 3483 `k ** 2 * size n <= t` by 3484 (`k ** 2 * size n <= m ** 2 * size n` by rw[] >> 3485 `m ** 2 * size n <= m ** 2 * size n * size n` by rw[MULT_POS] >> 3486 `m ** 2 * size n * size n = t` by rw[Abbr`t`] >> 3487 decide_tac) >> 3488 `k ** 2 * size n ** 2 <= t` by 3489 (`k ** 2 * size n ** 2 <= m ** 2 * size n ** 2` by rw[] >> 3490 `m ** 2 * size n ** 2 = t` by rw[Abbr`t`] >> 3491 decide_tac) >> 3492 decide_tac); 3493 3494(* Theorem: 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 3495 (LENGTH p = k) /\ (LENGTH q = k) ==> 3496 stepsOf (poly_multM n p q) <= 37 * k ** 2 * size n ** 2 *) 3497(* Proof: by poly_multM_steps_bound, MAX_1_POS *) 3498val poly_multM_steps_bound_alt = store_thm( 3499 "poly_multM_steps_bound_alt", 3500 ``!n p q k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ Weak (ZN n) q /\ 3501 (LENGTH p = k) /\ (LENGTH q = k) ==> 3502 stepsOf (poly_multM n p q) <= 37 * k ** 2 * size n ** 2``, 3503 metis_tac[poly_multM_steps_bound, MAX_1_POS]); 3504 3505(* ------------------------------------------------------------------------- *) 3506(* Squaring of polynomial *) 3507(* ------------------------------------------------------------------------- *) 3508 3509(* Squaring a polynomial p, of length k, in (MOD n, (unity k)). *) 3510val poly_sqM_def = Define` 3511 poly_sqM n p = poly_multM n p p 3512`; 3513 3514(* 3515EVAL ``poly_sqM 10 [1;1;0;0;0;0;0]``; = ([1; 2; 1; 0; 0; 0; 0],Count 1448): thm 3516EVAL ``poly_sqM 10 [1;2;1;0;0;0;0]``; = ([1; 4; 6; 4; 1; 0; 0],Count 1541): thm 3517EVAL ``poly_sqM 10 [1;4;6;4;1;0;0]``; = ([9; 9; 8; 6; 0; 6; 8],Count 2168): thm 3518*) 3519 3520(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3521 (valueOf (poly_sqM n p) = unity_mod_sq (ZN n) p) *) 3522(* Proof: 3523 valueOf (poly_sqM n p) 3524 = valueOf (poly_multM n p p) by poly_sqM_def 3525 = unity_mod_mult (ZN n) p p by poly_multM_value 3526 = unity_mod_sq (ZN n) p by unity_mod_sq_def 3527*) 3528val poly_sqM_value = store_thm( 3529 "poly_sqM_value[simp]", 3530 ``!n p. 0 < n /\ Weak (ZN n) p ==> 3531 (valueOf (poly_sqM n p) = unity_mod_sq (ZN n) p)``, 3532 rw[poly_sqM_def, unity_mod_sq_def]); 3533 3534(* Theorem: 0 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 3535 (valueOf (poly_sqM n p) = sqz p) *) 3536(* Proof: by poly_sqM_value, ZN_poly_sq_alt *) 3537val poly_sqM_value_thm = store_thm( 3538 "poly_sqM_value_thm", 3539 ``!n p k. 0 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 3540 (valueOf (poly_sqM n p) = sqz p)``, 3541 metis_tac[poly_sqM_value, ZN_poly_sq_alt]); 3542 3543(* Above p <> [] is the minimal requirement. Next with 0 < k is symmetric. *) 3544 3545(* Theorem: 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3546 (valueOf (poly_sqM n p) = sqz p) *) 3547(* Proof: by poly_sqM_value_thm, LENGTH_NIL *) 3548val poly_sqM_value_alt = store_thm( 3549 "poly_sqM_value_alt", 3550 ``!n p k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3551 (valueOf (poly_sqM n p) = sqz p)``, 3552 metis_tac[poly_sqM_value_thm, LENGTH_NIL, NOT_ZERO]); 3553 3554(* Theorem: 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_sqM n p)) *) 3555(* Proof: 3556 Note Ring (ZN n) by ZN_ring, 0 < n 3557 Weak (ZN n) (valueOf (poly_sqM n p)) 3558 = Weak (ZN n) (unity_mod_sq (ZN n) p) by poly_sqM_value 3559 = T by unity_mod_sq_weak, Ring (ZN n) 3560*) 3561val poly_sqM_weak = store_thm( 3562 "poly_sqM_weak", 3563 ``!n p. 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_sqM n p))``, 3564 rw[unity_mod_sq_weak, ZN_ring]); 3565 3566(* Theorem: 0 < n /\ Weak (ZN n) p ==> LENGTH (valueOf (poly_sqM n p)) = LENGTH p *) 3567(* Proof: 3568 LENGTH (valueOf (poly_sqM n p)) 3569 = LENGTH (unity_mod_sq (ZN n) p) by poly_sqM_value 3570 = LENGTH p by unity_mod_sq_length 3571*) 3572val poly_sqM_length = store_thm( 3573 "poly_sqM_length", 3574 ``!n p. 0 < n /\ Weak (ZN n) p ==> LENGTH (valueOf (poly_sqM n p)) = LENGTH p``, 3575 rw[unity_mod_sq_length]); 3576 3577(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3578 !k. Weak (ZN n) (FUNPOW (\p. valueOf (poly_sqM n p)) k p) *) 3579(* Proof: 3580 By induction on k. 3581 Let f = (\p. valueOf (poly_sqM n p)). 3582 Base: Weak (ZN n) (FUNPOW f 0 p) 3583 = Weak (ZN n) p by FUNPOW_0 3584 = T 3585 Step: Weak (ZN n) (FUNPOW f (SUC k) p) 3586 = Weak (ZN n) (f (FUNPOW f k p)) by FUNPOW_SUC 3587 = T by poly_sqM_weak, induction hypothesis 3588*) 3589val poly_sqM_iterating_weak = store_thm( 3590 "poly_sqM_iterating_weak", 3591 ``!n p. 0 < n /\ Weak (ZN n) p ==> 3592 !k. Weak (ZN n) (FUNPOW (\p. valueOf (poly_sqM n p)) k p)``, 3593 ntac 3 strip_tac >> 3594 qabbrev_tac `f = \p. valueOf (poly_sqM n p)` >> 3595 Induct >- 3596 metis_tac[FUNPOW_0] >> 3597 metis_tac[FUNPOW_SUC, poly_sqM_weak]); 3598 3599(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3600 !k. LENGTH (FUNPOW (\p. valueOf (poly_sqM n p)) k p) = LENGTH p *) 3601(* Proof: 3602 By induction on k. 3603 Let f = (\p. valueOf (poly_sqM n p)). 3604 Base: LENGTH (FUNPOW f 0 p) = LENGTH p, true by FUNPOW_0 3605 Step: LENGTH (FUNPOW f (SUC k) p) 3606 = LENGTH (f (FUNPOW f k p)) by FUNPOW_SUC 3607 = LENGTH p by poly_sqM_length, induction hypothesis 3608 since Weak (ZN n) (FUNPOW f k p) by poly_sqM_iterating_weak 3609*) 3610val poly_sqM_iterating_length = store_thm( 3611 "poly_sqM_iterating_length", 3612 ``!n p. 0 < n /\ Weak (ZN n) p ==> 3613 !k. LENGTH (FUNPOW (\p. valueOf (poly_sqM n p)) k p) = LENGTH p``, 3614 ntac 3 strip_tac >> 3615 qabbrev_tac `f = \p. valueOf (poly_sqM n p)` >> 3616 Induct >- 3617 metis_tac[FUNPOW_0] >> 3618 `Weak (ZN n) (FUNPOW f k p)` by rw[poly_sqM_iterating_weak, Abbr`f`] >> 3619 metis_tac[FUNPOW_SUC, poly_sqM_length]); 3620 3621(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3622 stepsOf (poly_sqM n p) = 3623 if (p = []) then 1 3624 else 3 + stepsOf (poly_turnM p) + 3625 stepsOf (poly_cmultM n (HD p) p) + 3626 stepsOf (poly_addM n (weak_cmult (ZN n) (HD p) p) 3627 (unity_mod_mult (ZN n) (turn p) (TL p))) + 3628 stepsOf (poly_multM n (turn p) (TL p)) *) 3629(* Proof: 3630 stepsOf (poly_sqM n p) 3631 = stepsOf (poly_multM n p p) by poly_sqM_def 3632 = if (p = []) then 1 3633 else 3 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n (HD p) p) + 3634 stepsOf (poly_addM n (weak_cmult (ZN n) (HD p) p) 3635 (valueOf (poly_multM n (turn p) (TL p)))) + 3636 stepsOf (poly_multM n (turn p) (TL p)) by poly_multM_steps_thm 3637 = if (p = []) then 1 3638 else 3 + stepsOf (poly_turnM p) + stepsOf (poly_cmultM n (HD p) p) + 3639 stepsOf (poly_addM n (weak_cmult (ZN n) (HD p) p) 3640 (unity_mod_mult (ZN n) (turn p) (TL p))) + 3641 stepsOf (poly_multM n (turn p) (TL p)) by poly_multM_value 3642*) 3643val poly_sqM_steps_thm = store_thm( 3644 "poly_sqM_steps_thm", 3645 ``!n p. 0 < n /\ Weak (ZN n) p ==> 3646 stepsOf (poly_sqM n p) = 3647 if (p = []) then 1 3648 else 3 + stepsOf (poly_turnM p) + 3649 stepsOf (poly_cmultM n (HD p) p) + 3650 stepsOf (poly_addM n (weak_cmult (ZN n) (HD p) p) 3651 (unity_mod_mult (ZN n) (turn p) (TL p))) + 3652 stepsOf (poly_multM n (turn p) (TL p))``, 3653 rw[poly_sqM_def, Once poly_multM_steps_thm] >> 3654 rw[poly_multM_value, weak_turn, weak_tail]); 3655 3656(* Theorem: 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3657 stepsOf (poly_sqM n p) <= 3658 1 + 10 * k + 20 * k ** 2 + 2 * (k ** 2) * size n + 4 * k ** 2 * size n ** 2 *) 3659(* Proof: 3660 stepsOf (poly_sqM n p) 3661 = stepsOf (poly_multM n p p) by poly_sqM_def 3662 <= 1 + 10 * k + 20 * k ** 2 + 2 * (k ** 2) * size n + 4 * k ** 2 * size n ** 2 3663 by poly_multM_steps_upper 3664*) 3665val poly_sqM_steps_upper = store_thm( 3666 "poly_sqM_steps_upper", 3667 ``!n p k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3668 stepsOf (poly_sqM n p) <= 3669 1 + 10 * k + 20 * k ** 2 + 2 * (k ** 2) * size n + 4 * k ** 2 * size n ** 2``, 3670 metis_tac[poly_sqM_def, poly_multM_steps_upper]); 3671 3672(* Theorem: 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3673 stepsOf (poly_sqM n p) <= 37 * MAX 1 k ** 2 * size n ** 2 *) 3674(* Proof: 3675 stepsOf (poly_sqM n p) 3676 = stepsOf (poly_multM n p p) by poly_sqM_def 3677 <= 37 * MAX 1 k ** 2 * size n ** 2 by poly_multM_steps_bound 3678*) 3679val poly_sqM_steps_bound = store_thm( 3680 "poly_sqM_steps_bound", 3681 ``!n p k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3682 stepsOf (poly_sqM n p) <= 37 * MAX 1 k ** 2 * size n ** 2``, 3683 metis_tac[poly_sqM_def, poly_multM_steps_bound]); 3684 3685(* Theorem: 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3686 stepsOf (poly_sqM n p) <= 37 * k ** 2 * size n ** 2 *) 3687(* Proof: by poly_sqM_steps_bound, MAX_1_POS *) 3688val poly_sqM_steps_bound_alt = store_thm( 3689 "poly_sqM_steps_bound_alt", 3690 ``!n p k. 0 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3691 stepsOf (poly_sqM n p) <= 37 * k ** 2 * size n ** 2``, 3692 metis_tac[poly_sqM_steps_bound, MAX_1_POS]); 3693 3694(* ------------------------------------------------------------------------- *) 3695(* Polynomial Exponential in (mod n, unity k) *) 3696(* ------------------------------------------------------------------------- *) 3697 3698(* Fast Exponentiation -- recursive form *) 3699 3700(* Pseudocode: 3701 Given a polynomial p, and index j, compute (p ** j) (mod n, unity k) 3702 list_exp p j = 3703 if j = 0 then return [1] // p ** 0 = |1| 3704 q <- list_exp (list_sq p) (HALF j) // recursive call with (list_sq p) and index (HALF j) 3705 return if (EVEN j) then q else (list_mult p q) // if OOD j, list_mult result with p 3706*) 3707 3708(* Polynomial exponentiation, p ** j (MOD n, unity k). *) 3709(* 3710val poly_expM_def = tDefine "poly_expM" ` 3711 poly_expM n p j = (* for p ** j. *) 3712 do 3713 j0 <- zeroM j; 3714 if j0 then do (* trick to keep length k without explicit k *) 3715 t <- consM 1 []; (* |1|, but too short *) 3716 q <- poly_cmultM n 0 p; (* |0| of same length *) 3717 poly_addM n t q (* |1| of same length *) 3718 od 3719 else do 3720 p1 <- poly_sqM n p; 3721 h <- halfM j; 3722 q <- poly_expM n p1 h; 3723 ifM (evenM j) (return q) (poly_multM n p q) 3724 od 3725 od 3726`(WF_REL_TAC `measure (\(n,p,j). j)` >> simp[]); 3727-- the case j = 0 does not match unity_mod_exp (ZN n) p 0 = |1| 3728*) 3729val poly_expM_def = tDefine "poly_expM" ` 3730 poly_expM n p j = (* for p ** j. *) 3731 do 3732 j0 <- zeroM j; 3733 if j0 then 3734 do (* make |1| = if #1 = #0 then [] else [#1] *) 3735 n1 <- oneM n; 3736 if n1 then return [] (* by 1 MOD 1 = 0 *) 3737 else consM 1 [] (* by 1 MOD n = 1, n <> 1 *) 3738 od 3739 else do 3740 p1 <- poly_sqM n p; 3741 h <- halfM j; 3742 q <- poly_expM n p1 h; 3743 ifM (evenM j) (return q) (poly_multM n p q) 3744 od 3745 od 3746`(WF_REL_TAC `measure (\(n,p,j). j)` >> simp[]); 3747 3748 3749(* 3750> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 0``; = ([1],Count 6): thm 3751> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 1``; = ([1; 1; 0; 0; 0; 0; 0],Count 1586): thm 3752> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 2``; = ([1; 2; 1; 0; 0; 0; 0],Count 4552): thm 3753> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 3``; = ([1; 3; 3; 1; 0; 0; 0],Count 6031): thm 3754> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 4``; = ([1; 4; 6; 4; 1; 0; 0],Count 6826): thm 3755> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 5``; = ([1; 5; 0; 0; 5; 1; 0],Count 8468): thm 3756> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 6``; = ([1; 6; 5; 0; 5; 6; 1],Count 8601): thm 3757> EVAL ``poly_expM 10 [1;1;0;0;0;0;0] 7``; = ([2; 7; 1; 5; 5; 1; 7],Count 10377): thm 3758*) 3759 3760(* Theorem: 0 < n /\ Weak (ZN n) p ==> 3761 valueOf (poly_expM n p j) = unity_mod_exp (ZN n) p j *) 3762(* Proof: 3763 By induction from poly_expM_def. 3764 Base: valueOf (if n = 1 then unit [] else consM 1 []) = unity_mod_exp (ZN n) p 0 3765 unity_mod_exp (ZN n) p 0 3766 = poly_one (ZN n) by unity_mod_exp_0 3767 = if (ZN n).prod.id = (ZN n).sum.id then [] else [(ZN n).prod.id] by poly_one 3768 and (ZN n).sum.id = 0 by ZN_property 3769 and (ZN n).prod.id = if n = 1 then 0 else 1 by ZN_property 3770 If n = 1, 3771 LHS = valueOf (unit []) = [] = RHS 3772 If n <> 1, 3773 LHS = valueOf (consM 1 []) = [1] = RHS 3774 Step: j <> 0 ==> 0 < n /\ Weak (ZN n) (valueOf (poly_sqM n p)) /\ Weak (ZN n) q ==> 3775 valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)) = 3776 unity_mod_exp (ZN n) (valueOf (poly_sqM n p)) (HALF j) ==> 3777 valueOf (poly_multM n p (valueOf (poly_expM n (unity_mod_sq (ZN n) p) (HALF j)))) = 3778 unity_mod_exp (ZN n) p j 3779 3780 If EVEN j, 3781 valueOf (poly_expM n p j) 3782 = valueOf (poly_expM n (unity_mod_sq (ZN n) p) (HALF j)) by poly_expM_def 3783 = unity_mod_exp (ZN n) (unity_mod_sq (ZN n) p) (HALF j) by induction hypothesis 3784 = unity_mod_exp (ZN n) p n by unity_mod_exp_even 3785 3786 If ~EVEN j, 3787 Then ODD j by ODD_EVEN 3788 valueOf (poly_expM n p j) 3789 = valueOf (poly_multM n p (valueOf (poly_expM n (unity_mod_sq (ZN n) p) (HALF j)))) 3790 by poly_expM_def 3791 = valueOf (poly_multM n p (unity_mod_exp (ZN n) (unity_mod_sq (ZN n) p) (HALF j)) 3792 by induction hypothesis 3793 = unity_mod_mult (ZN n) p (unity_mod_exp (ZN n) (unity_mod_sq (ZN n) p) (HALF j)) 3794 by poly_multM_value 3795 = unity_mod_exp (ZN n) p n by unity_mod_exp_odd 3796*) 3797val poly_expM_value = store_thm( 3798 "poly_expM_value[simp]", 3799 ``!n p j. 0 < n /\ Weak (ZN n) p ==> 3800 valueOf (poly_expM n p j) = unity_mod_exp (ZN n) p j``, 3801 ho_match_mp_tac (theorem "poly_expM_ind") >> 3802 rw[] >> 3803 rw[Once poly_expM_def] >- 3804 (Cases_on `n = 1` >> simp[unity_mod_exp_0, poly_one, ZN_property]) >> 3805 (Cases_on `EVEN j` >> simp[]) >| [ 3806 `valueOf (poly_expM n (unity_mod_sq (ZN n) p) (HALF j)) = 3807 valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))` by rw[poly_sqM_value] >> 3808 `_ = unity_mod_exp (ZN n) (valueOf (poly_sqM n p)) (HALF j)` by rw[poly_sqM_weak] >> 3809 `_ = unity_mod_exp (ZN n) p j` by rw[unity_mod_exp_even] >> 3810 rw[], 3811 `ODD j` by rw[ODD_EVEN] >> 3812 `valueOf (poly_multM n p (valueOf (poly_expM n (unity_mod_sq (ZN n) p) (HALF j)))) = 3813 valueOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))` by rw[poly_sqM_value] >> 3814 `_ = valueOf (poly_multM n p (unity_mod_exp (ZN n) (valueOf (poly_sqM n p)) (HALF j)))` by rw[poly_sqM_weak] >> 3815 `_ = unity_mod_mult (ZN n) p (unity_mod_exp (ZN n) (valueOf (poly_sqM n p)) (HALF j))` by rw[unity_mod_exp_weak, poly_sqM_weak, ZN_ring] >> 3816 `_ = unity_mod_exp (ZN n) p j` by rw[unity_mod_exp_odd] >> 3817 rw[] 3818 ]); 3819 3820(* Theorem: 1 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 3821 (valueOf (poly_expM n p j) = p **z j) *) 3822(* Proof: by poly_expM_value, ZN_poly_exp_alt. *) 3823val poly_expM_value_thm = store_thm( 3824 "poly_expM_value_thm", 3825 ``!n p j k. 1 < n /\ Weak (ZN n) p /\ p <> [] /\ (LENGTH p = k) ==> 3826 (valueOf (poly_expM n p j) = p **z j)``, 3827 metis_tac[poly_expM_value, ZN_poly_exp_alt, ONE_LT_POS]); 3828 3829(* Theorem: 1 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3830 (valueOf (poly_expM n p j) = p **z j) *) 3831(* Proof: by poly_expM_value_thm, LENGTH_NIL. *) 3832val poly_expM_value_alt = store_thm( 3833 "poly_expM_value_alt", 3834 ``!n p j k. 1 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3835 (valueOf (poly_expM n p j) = p **z j)``, 3836 metis_tac[poly_expM_value_thm, LENGTH_NIL, NOT_ZERO]); 3837 3838(* Theorem: 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_expM n p j)) *) 3839(* Proof: 3840 Note Ring (ZN n) by ZN_ring, 0 < n 3841 Weak (ZN n) (valueOf (poly_expM n p j)) 3842 = Weak (ZN n) (unity_mod_exp (ZN n) p j) by poly_expM_value 3843 = T by unity_mod_exp_weak 3844*) 3845val poly_expM_weak = store_thm( 3846 "poly_expM_weak", 3847 ``!n p j. 0 < n /\ Weak (ZN n) p ==> Weak (ZN n) (valueOf (poly_expM n p j))``, 3848 metis_tac[poly_expM_value, unity_mod_exp_weak, ZN_ring]); 3849 3850(* Theorem: 0 < n /\ Weak (ZN n) p /\ Weak (ZN n) q ==> 3851 LENGTH (valueOf (poly_expM n p j)) = 3852 if n = 1 then 0 else if j = 0 then 1 else LENGTH p *) 3853(* Proof: 3854 Note (ZN n).sum.id = (ZN n).prod.id only when n = 1 3855 by ZN_property 3856 LENGTH (valueOf (poly_expM n p j)) 3857 = LENGTH (unity_mod_exp (ZN n) p j) by poly_expM_value 3858 = if (ZN n).prod.id = (ZN n).sum.id then 0 else if j = 0 then 1 else LENGTH p 3859 by unity_mod_exp_length 3860 = if n = 1 then 0 else if j = 0 then 1 else LENGTH p 3861*) 3862val poly_expM_length = store_thm( 3863 "poly_expM_length", 3864 ``!n p j. 0 < n /\ Weak (ZN n) p ==> 3865 LENGTH (valueOf (poly_expM n p j)) = 3866 if n = 1 then 0 else if j = 0 then 1 else LENGTH p``, 3867 rpt strip_tac >> 3868 `((ZN n).prod.id = (ZN n).sum.id) <=> (n = 1)` by rw[ZN_property] >> 3869 assume_tac (unity_mod_exp_length |> ISPEC ``(ZN n)``) >> 3870 first_x_assum (qspecl_then [`p`, `j`] strip_assume_tac) >> 3871 metis_tac[poly_expM_value, unity_mod_exp_length]); 3872 3873(* Theorem: valueOf (poly_expM n p 0) = if n = 1 then [] else [1] *) 3874(* Proof: by poly_expM_def *) 3875val poly_expM_0 = store_thm( 3876 "poly_expM_0", 3877 ``!n p. valueOf (poly_expM n p 0) = if n = 1 then [] else [1]``, 3878 rw[Once poly_expM_def]); 3879 3880(* Theorem: Weak (ZN 1) p ==> (valueOf (poly_expM 1 p j) = []) *) 3881(* Proof: 3882 Note LENGTH (valueOf (poly_expM 1 p j)) = 0 by poly_expM_length 3883 Thus valueOf (poly_expM 1 p j) = [] by LENGTH_NIL 3884*) 3885val poly_expM_trivial = store_thm( 3886 "poly_expM_trivial", 3887 ``!p j. Weak (ZN 1) p ==> (valueOf (poly_expM 1 p j) = [])``, 3888 metis_tac[poly_expM_length, LENGTH_NIL, DECIDE``0 < 1``]); 3889 3890(* Theorem: stepsOf (poly_expM n p j) = 3891 size j + 3892 if j = 0 then (size n + if n = 1 then 0 else 1) 3893 else (1 + 4 * size j + stepsOf (poly_sqM n p) + 3894 (if EVEN j then 0 else 3895 stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))) + 3896 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))) *) 3897(* Proof: 3898 stepsOf (poly_expM n p j) 3899 = stepsOf (zeroM j) + 3900 if j = 0 then (stepsOf (oneM n) + if n = 1 then 0 else stepsOf (consM 1 [])) 3901 else stepsOf (poly_sqM n p) + stepsOf (halfM j) + 3902 stepsOf (poly_expM n (unity_mod_sq n p) (HALF j)) + stepsOf (evenM j) + 3903 if EVEN j then stepsOf (return q) else stepsOf (poly_multM n p q) 3904 where q = unity_mod_exp n (unity_mod_sq n p) (HALF j) by poly_expM_def 3905 = size j + if j = 0 then (size n + if n = 1 then 0 else 1) 3906 else stepsOf (poly_sqM n p) + 2 * size j + 3907 stepsOf (poly_expM n (unity_mod_sq n p) (HALF j)) + (1 + 2 * size j) + 3908 if EVEN j then 0 else stepsOf (poly_multM n p (unity_mod_exp n (unity_mod_sq n p) (HALF j))) 3909 = size j + if j = 0 then (size n + if n = 1 then 0 else 1) 3910 else stepsOf (poly_sqM n p) + 2 * size j + (1 + 2 * size j) + 3911 (if EVEN j then 0 else stepsOf (poly_multM n p (unity_mod_exp n (unity_mod_sq n p) (HALF j)))) + 3912 stepsOf (poly_expM n (unity_mod_sq n p) (HALF j)) 3913 = size j + if j = 0 then (size n + if n = 1 then 0 else 1) 3914 else 1 + 4 * size j +stepsOf (poly_sqM n p) + 3915 (if EVEN j then 0 else stepsOf (poly_multM n p (unity_mod_exp n (unity_mod_sq n p) (HALF j)))) + 3916 stepsOf (poly_expM n (unity_mod_sq n p) (HALF j)) 3917 use valueOf for unconditional form. 3918*) 3919val poly_expM_steps_thm = store_thm( 3920 "poly_expM_steps_thm", 3921 ``!n p j. stepsOf (poly_expM n p j) = 3922 size j + 3923 if j = 0 then (size n + if n = 1 then 0 else 1) 3924 else (1 + 4 * size j + stepsOf (poly_sqM n p) + 3925 (if EVEN j then 0 else 3926 stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))) + 3927 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))``, 3928 rw[Once poly_expM_def]); 3929 3930(* Theorem: let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 3931 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 3932 in !p j. stepsOf (poly_expM n p j) = 3933 if j = 0 then (1 + size n + if n = 1 then 0 else 1) 3934 else body p j + stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)) *) 3935(* Proof: 3936 stepsOf (poly_expM n p j) 3937 = size j + if j = 0 then (size n + if n = 1 then 0 else 1) 3938 else (1 + 4 * size j + stepsOf (poly_sqM n p) + 3939 (if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))) + 3940 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))) by poly_expM_steps_thm 3941 = if j = 0 then (size 0 + size n + if n = 1 then 0 else 1) 3942 else (size j + 1 + 4 * size j + stepsOf (poly_sqM n p) + 3943 (if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))) + 3944 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))) 3945 = if j = 0 then (if n = 1 then 2 else 2 + size n) 3946 else (1 + 5 * size j + stepsOf (poly_sqM n p) + 3947 (if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))) + 3948 stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))) 3949*) 3950val poly_expM_steps_by_div_loop = store_thm( 3951 "poly_expM_steps_by_div_loop", 3952 ``!n. let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 3953 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 3954 in !p j. stepsOf (poly_expM n p j) = 3955 if j = 0 then (1 + size n + if n = 1 then 0 else 1) 3956 else body p j + stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))``, 3957 (rw[Once poly_expM_steps_thm] >> Cases_on `j = 0` >> simp[])); 3958 3959(* 3960This puts poly_expM_steps in the category: dividing loop with body cover. 3961 poly_expM_steps_by_div_loop: 3962 !p j. loop p j = if j = 0 then quit p else body p j + loop (valueOf (poly_sqM n p)) (HALF j) 3963suitable for: loop2_div_rise_count_cover_le 3964Actually a conditional cover, so needs to fall back to: loop2_div_count_eqn 3965*) 3966 3967(* First, work out a cover for the body. *) 3968 3969(* Theorem: let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 3970 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 3971 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 3972 body p j <= 1 + 5 * size j + 74 * (MAX 1 k) ** 2 * size n ** 2 *) 3973(* Proof: 3974 body p j 3975 = 1 + 5 * size j + stepsOf (poly_sqM n p) + 3976 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 3977 = 1 + 5 * size j + stepsOf (poly_sqM n p) + 3978 if EVEN j then 0 else stepsOf (poly_multM n p q) 3979 where q = valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)) 3980 <= 1 + 5 * size j + stepsOf (poly_sqM n p) + stepsOf (poly_multM n p q) 3981 Note stepsOf (poly_sqM n p) 3982 <= 37 * (MAX 1 k) ** 2 * size n ** 2 by poly_sqM_steps_bound 3983 For stepsOf (poly_multM n p q), 3984 Note Weak (ZN n) q by poly_sqM_weak 3985 If n = 1, 3986 Then q = [] by poly_expM_trivial 3987 and stepsOf (poly_multM n p []) = 1 by poly_multM_steps_nil 3988 If HALF j = 0, 3989 Then q = [1] by poly_expM_0, n <> 1 3990 and stepsOf (poly_multM n p [1]) 3991 <= 27 * (MAX 1 k) * size (MAX 1 n) * size n by poly_multM_steps_sing_bound 3992 = 27 * (MAX 1 k) * size n * size n by MAX_DEF, 0 < n 3993 = 27 * (MAX 1 k) * size n ** 2 3994 Otherwise, 3995 (LENGTH q = k) by poly_expM_length, poly_sqM_length 3996 so stepsOf (poly_multM n p q) 3997 <= 37 * (MAX 1 k) ** 2 * size n ** 2 by poly_multM_steps_bound, LENGTHs match 3998 Overall, 3999 body p j 4000 <= 1 + 5 * size j + 2 * 37 * MAX 1 k ** 2 * size n ** 2 4001*) 4002val poly_expM_body_upper = store_thm( 4003 "poly_expM_body_upper", 4004 ``!n. let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 4005 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 4006 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4007 body p j <= 1 + 5 * size j + 74 * (MAX 1 k) ** 2 * size n ** 2``, 4008 rw_tac std_ss[] >> 4009 `body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 4010 if EVEN j then 0 4011 else 4012 stepsOf 4013 (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))` by fs[Abbr`body`] >> 4014 qabbrev_tac `q = valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))` >> 4015 `body p j <= 1 + 5 * size j + stepsOf (poly_sqM n p) + stepsOf (poly_multM n p q)` by rw[] >> 4016 qabbrev_tac `k = LENGTH p` >> 4017 `stepsOf (poly_sqM n p) <= 37 * MAX 1 k ** 2 * size n ** 2` by rw[poly_sqM_steps_bound] >> 4018 `Weak (ZN n) q` by rw[poly_expM_weak, poly_sqM_weak, Abbr`q`] >> 4019 Cases_on `n = 1` >| [ 4020 `q = []` by metis_tac[poly_expM_trivial, poly_sqM_weak] >> 4021 `stepsOf (poly_multM n p q) = 1` by metis_tac[poly_multM_steps_nil] >> 4022 `0 < MAX 1 k ** 2 * size n ** 2` by rw[] >> 4023 decide_tac, 4024 Cases_on `HALF j = 0` >| [ 4025 `q = [1]` by metis_tac[poly_expM_0] >> 4026 `MAX 1 n = n` by rw[MAX_DEF] >> 4027 `stepsOf (poly_multM n p q) <= 27 * (MAX 1 k) * size n * size n` by metis_tac[poly_multM_steps_sing_bound] >> 4028 `(MAX 1 k) <= (MAX 1 k) ** 2` by metis_tac[SELF_LE_SQ, EXP_2] >> 4029 `(MAX 1 k) * size n * size n <= (MAX 1 k) ** 2 * size n ** 2` by rw[] >> 4030 decide_tac, 4031 `LENGTH q = k` by metis_tac[poly_expM_length, poly_sqM_weak, poly_sqM_length] >> 4032 `stepsOf (poly_multM n p q) <= 37 * MAX 1 k ** 2 * size n ** 2` by rw[poly_multM_steps_bound] >> 4033 decide_tac 4034 ] 4035 ]); 4036 4037(* Theorem: let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 4038 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 4039 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4040 body p j <= 80 * size j * (MAX 1 k) ** 2 * size n ** 2 *) 4041(* Proof: 4042 body p j 4043 <= 1 + 5 * size j + 74 * (MAX 1 k) ** 2 * size n ** 2 by poly_expM_body_upper 4044 <= (1 + 5 + 74) * size j * (MAX 1 k) ** 2 * size n ** 2 by dominant term 4045 = 80 * size j * (MAX 1 k) ** 2 * size n ** 2 4046*) 4047val poly_expM_body_bound = store_thm( 4048 "poly_expM_body_bound", 4049 ``!n. let body p j = 1 + 5 * size j + stepsOf (poly_sqM n p) + 4050 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j)))) 4051 in !p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4052 body p j <= 80 * size j * (MAX 1 k) ** 2 * size n ** 2``, 4053 rpt strip_tac >> 4054 assume_tac poly_expM_body_upper >> 4055 first_x_assum (qspec_then `n` strip_assume_tac) >> 4056 qabbrev_tac `body = \p j. 1 + 5 * size j + stepsOf (poly_sqM n p) + 4057 if EVEN j then 0 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))` >> 4058 `!p j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> body p j <= 80 * size j * MAX 1 k ** 2 * size n ** 2` suffices_by fs[] >> 4059 rpt strip_tac >> 4060 `body p j <= 1 + 5 * size j + 74 * (MAX 1 k) ** 2 * size n ** 2` by metis_tac[] >> 4061 qabbrev_tac `m = MAX 1 k` >> 4062 qabbrev_tac `t = size j * m ** 2 * size n ** 2` >> 4063 `body p j <= 80 * t` suffices_by rw[Abbr`t`] >> 4064 `1 <= m` by rw[Abbr`m`] >> 4065 `0 < t` by rw[MULT_POS, Abbr`t`] >> 4066 `1 <= t` by decide_tac >> 4067 `size j <= t` by 4068 (`size j <= size j * (m ** 2 * size n ** 2)` by rw[MULT_POS] >> 4069 `size j * (m ** 2 * size n ** 2) = t` by rw[Abbr`t`] >> 4070 decide_tac) >> 4071 `m ** 2 * size n ** 2 <= t` by 4072 (`m ** 2 * size n ** 2 <= m ** 2 * size n ** 2 * size j` by rw[MULT_POS] >> 4073 `m ** 2 * size n ** 2 * size j = t` by rw[Abbr`t`] >> 4074 decide_tac) >> 4075 decide_tac); 4076 4077(* Theorem: 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4078 stepsOf (poly_expM n p j) <= 2 + size n + 80 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 *) 4079(* Proof: 4080 Let quit = (\p. 1 + size n + if n = 1 then 0 else 1), 4081 body = (\p j. 1 + 5 * size j + stepsOf (poly_sqM n p) + 4082 if EVEN j then 0 4083 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))), 4084 cover = (\p j. 80 * size j * (MAX 1 (LENGTH p)) ** 2 * size n ** 2), 4085 f = (\p. valueOf (poly_sqM n p)), 4086 loop = (\p j. stepsOf (poly_expM n p j)). 4087 Then !p j. loop p j = if j = 0 then quit p else body p j + loop (f p) (HALF j) 4088 by poly_expM_steps_by_div_loop 4089 Now !x y. body x y <= cover x y by poly_expM_body_bound 4090 and MONO2 cover by 4091 and RISING f by 4092 Let m = pop 2 j <= size n by pop_size 4093 q = FUNPOW f m p, 4094 g = (\t. body (FUNPOW f t p) (j DIV 2 ** t)), 4095 4096 Claim: SUM (GENLIST g m) <= SUM (GENLIST (K (cover p j)) m) 4097 Proof: Let i < m, want to show: 4098 EL i (GENLIST g m) <= EL i (GENLIST (K (cover p j)) m) 4099 Let u = FUNPOW i p, h = j DIV 2 ** i. 4100 This is to show: body u h <= cover p j 4101 Note Weak (ZN n) u by poly_sqM_iterating_weak 4102 and LENGTH u = LENGTH p by poly_sqM_iterating_length 4103 Note h <= j by DIV_LESS_EQ 4104 body q h 4105 <= cover q h by cover over body 4106 = cover p h by LENGTH q = LENGTH p, special form of cover 4107 <= cover p j by size_monotone_le 4108 The result follows by SUM_LE 4109 4110 Thus loop p j 4111 = quit q + SUM (GENLIST g m) by loop2_div_count_eqn 4112 <= quit q + SUM (GENLIST (K (cover p j)) m) by SUM_LE, claim 4113 <= (2 + size n) + (cover p j) * m by SUM_GENLIST_K 4114 <= (2 + size n) + 80 * size j * (MAX 1 k) ** 2 * size n ** 2 * size j 4115 = 2 + size n + 80 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 4116*) 4117val poly_expM_steps_upper = store_thm( 4118 "poly_expM_steps_upper", 4119 ``!p n j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4120 stepsOf (poly_expM n p j) <= 2 + size n + 80 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2``, 4121 rpt strip_tac >> 4122 assume_tac poly_expM_steps_by_div_loop >> 4123 first_x_assum (qspec_then `n` strip_assume_tac) >> 4124 assume_tac poly_expM_body_bound >> 4125 first_x_assum (qspec_then `n` strip_assume_tac) >> 4126 qabbrev_tac `quit = \p:num list. 1 + size n + if n = 1 then 0 else 1` >> 4127 qabbrev_tac `body = \p j. 1 + 5 * size j + stepsOf (poly_sqM n p) + 4128 if EVEN j then 0 4129 else stepsOf (poly_multM n p (valueOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))))` >> 4130 qabbrev_tac `cover = \p:num list j. 80 * size j * (MAX 1 (LENGTH p)) ** 2 * size n ** 2` >> 4131 qabbrev_tac `f = \p. valueOf (poly_sqM n p)` >> 4132 qabbrev_tac `loop = \p j. stepsOf (poly_expM n p j)` >> 4133 `loop p j <= 2 + size n + 80 * MAX 1 k ** 2 * size j ** 2 * size n ** 2` suffices_by rw[] >> 4134 `!p j. loop p j = if j = 0 then quit p else body p j + loop (f p) (HALF j)` by metis_tac[] >> 4135 `1 < 2` by decide_tac >> 4136 `!x y. Weak (ZN n) x ==> body x y <= cover x y` by metis_tac[] >> 4137 imp_res_tac loop2_div_count_eqn >> 4138 last_x_assum (qspecl_then [`j`, `p`] strip_assume_tac) >> 4139 qabbrev_tac `foo1 = let body = body in 4140 !p j. stepsOf (poly_expM n p j) = 4141 if j = 0 then 1 + size n + if n = 1 then 0 else 1 4142 else body p j + stepsOf (poly_expM n (valueOf (poly_sqM n p)) (HALF j))` >> 4143 qabbrev_tac `foo2 = !p j. loop p j = if j = 0 then quit p else body p j + loop (f p) (HALF j)` >> 4144 `pop 2 j <= size j` by rw[pop_size] >> 4145 qabbrev_tac `g = \j'. body (FUNPOW f j' p) (j DIV 2 ** j')` >> 4146 `quit (FUNPOW f (pop 2 j) p) <= 2 + size n` by rw[Abbr`quit`] >> 4147 `SUM (GENLIST g (pop 2 j)) <= SUM (GENLIST (K (cover p j)) (pop 2 j))` by 4148 (irule SUM_LE >> 4149 rw[Abbr`g`] >> 4150 qabbrev_tac `q = FUNPOW f k' p` >> 4151 qabbrev_tac `h = j DIV 2 ** k'` >> 4152 `Weak (ZN n) q` by rw[poly_sqM_iterating_weak, Abbr`q`, Abbr`f`] >> 4153 `LENGTH q = LENGTH p` by rw[poly_sqM_iterating_length, Abbr`q`, Abbr`f`] >> 4154 `body q h <= cover q h` by rw[] >> 4155 `cover q h = cover p h` by rw[Abbr`cover`] >> 4156 `h <= j` by rw[DIV_LESS_EQ, Abbr`h`] >> 4157 `cover p h <= cover p j` by rw[size_monotone_le, Abbr`cover`] >> 4158 decide_tac) >> 4159 `SUM (GENLIST (K (cover p j)) (pop 2 j)) = (cover p j) * (pop 2 j)` by rw[SUM_GENLIST_K] >> 4160 `cover p j * pop 2 j <= cover p j * size j` by rw[] >> 4161 `cover p j * size j = 80 * size j * MAX 1 k ** 2 * size n ** 2 * size j` by fs[Abbr`cover`] >> 4162 `80 * size j * MAX 1 k ** 2 * size n ** 2 * size j = 80 * MAX 1 k ** 2 * size j ** 2 * size n ** 2` by rw[] >> 4163 decide_tac); 4164 4165(* Theorem: 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4166 stepsOf (poly_expM n p j) <= 83 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 *) 4167(* Proof: 4168 stepsOf (poly_expM n p j) 4169 <= 2 + size n + 80 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 by poly_expM_steps_upper 4170 <= (2 + 1 + 80) * 80 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 by dominant term 4171 = 83 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2 4172*) 4173val poly_expM_steps_bound = store_thm( 4174 "poly_expM_steps_bound", 4175 ``!p n j k. 0 < n /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4176 stepsOf (poly_expM n p j) <= 83 * (MAX 1 k) ** 2 * size j ** 2 * size n ** 2``, 4177 rpt strip_tac >> 4178 assume_tac poly_expM_steps_upper >> 4179 first_x_assum (drule_all_then strip_assume_tac) >> 4180 first_x_assum (qspec_then `j` strip_assume_tac) >> 4181 `0 < MAX 1 k ** 2 * size j ** 2 * size n ** 2` by rw[MULT_POS] >> 4182 `size n <= size n * (MAX 1 k ** 2 * size j ** 2 * size n)` by rw[MULT_POS] >> 4183 `size n * (MAX 1 k ** 2 * size j ** 2 * size n) = MAX 1 k ** 2 * size j ** 2 * size n ** 2` by rw[] >> 4184 decide_tac); 4185 4186(* The following is just to match conditions in poly_expM_value_alt *) 4187 4188(* Theorem: 1 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4189 stepsOf (poly_expM n p j) <= 83 * k ** 2 * size j ** 2 * size n ** 2 *) 4190(* Proof: by poly_expM_steps_bound, MAX_1_POS *) 4191val poly_expM_steps_bound_alt = store_thm( 4192 "poly_expM_steps_bound_alt", 4193 ``!p n j k. 1 < n /\ 0 < k /\ Weak (ZN n) p /\ (LENGTH p = k) ==> 4194 stepsOf (poly_expM n p j) <= 83 * k ** 2 * size j ** 2 * size n ** 2``, 4195 metis_tac[poly_expM_steps_bound, MAX_1_POS, DECIDE``1 < n ==> 0 < n``]); 4196 4197(* ------------------------------------------------------------------------- *) 4198(* Polynomial Coefficients *) 4199(* ------------------------------------------------------------------------- *) 4200 4201(* Get coefficient j of polynomial of length k *) 4202(* > EL; 4203val it = |- (!l. EL 0 l = HD l) /\ !l n. EL (SUC n) l = EL n (TL l): thm 4204*) 4205val poly_get_coeffM_def = tDefine "poly_get_coeffM" ` 4206 poly_get_coeffM p j = (* always assume p <> |0|, j < k *) 4207 do 4208 j0 <- zeroM j; 4209 if j0 then headM p 4210 else do 4211 q <- tailM p; 4212 i <- decM j; 4213 poly_get_coeffM q i; 4214 od 4215 od 4216`(WF_REL_TAC `measure (\(p,j). j)` >> simp[]); 4217 4218(* Put x as coefficient j of polynomial of length k *) 4219(* > LUPDATE_def 4220val it = |- (!e n. LUPDATE e n [] = []) /\ (!e x l. LUPDATE e 0 (x::l) = e::l) /\ 4221 !e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l: thm 4222*) 4223val poly_put_coeffM_def = tDefine "poly_put_coeffM" ` 4224 poly_put_coeffM x p j = (* always assume p <> |0|, j < k *) 4225 do 4226 q <- tailM p; 4227 j0 <- zeroM j; 4228 if j0 then consM x q 4229 else do 4230 h <- headM p; 4231 i <- decM j; 4232 p1 <- poly_put_coeffM x q i; 4233 consM h p1; 4234 od 4235 od 4236`(WF_REL_TAC `measure (\(x,p,j). j)` >> simp[]); 4237 4238(* 4239> EVAL ``poly_get_coeffM [1;2;3;4;5] 2``; = (3,Count 10): thm 4240> EVAL ``poly_put_coeffM 0 [1;2;3;4;5] 2``; = ([1; 2; 0; 4; 5],Count 15): thm 4241*) 4242 4243(* ------------------------------------------------------------------------- *) 4244 4245(* export theory at end *) 4246val _ = export_theory(); 4247 4248(*===========================================================================*) 4249