helm/matita/library/nat/gcd.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/gcd".
  16
  17 include "nat/primes.ma".
  18
  19 let rec gcd_aux p m n: nat \def
  20 match divides_b n m with
  21 [ true \Rightarrow n
  22 | false \Rightarrow
  23   match p with
  24   [O \Rightarrow n
  25   |(S q) \Rightarrow gcd_aux q n (mod m n)]].
  26
  27 definition gcd : nat \to nat \to nat \def
  28 \lambda n,m:nat.
  29   match leb n m with
  30   [ true \Rightarrow
  31     match n with
  32     [ O \Rightarrow m
  33     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
  34   | false \Rightarrow
  35     match m with
  36     [ O \Rightarrow n
  37     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
  38
  39 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
  40 p \divides mod m n.
  41 intros.elim H1.elim H2.
  42 apply witness ? ? (n2 - n1*(div m n)).
  43 rewrite > distr_times_minus.
  44 rewrite < H3.
  45 rewrite < assoc_times.
  46 rewrite < H4.
  47 apply sym_eq.
  48 apply plus_to_minus.
  49 rewrite > div_mod m n in \vdash (? ? %).
  50 rewrite > sym_times.
  51 apply eq_plus_to_le ? ? (mod m n).
  52 reflexivity.
  53 assumption.
  54 rewrite > sym_times.
  55 apply div_mod.assumption.
  56 qed.
  57
  58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  59 p \divides mod m n \to p \divides n \to p \divides m.
  60 intros.elim H1.elim H2.
  61 apply witness p m ((n1*(div m n))+n2).
  62 rewrite > distr_times_plus.
  63 rewrite < H3.
  64 rewrite < assoc_times.
  65 rewrite < H4.rewrite < sym_times.
  66 apply div_mod.assumption.
  67 qed.
  68
  69 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  70 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
  71 intro.elim p.
  72 absurd O < n.assumption.apply le_to_not_lt.assumption.
  73 cut (n1 \divides m) \lor (n1 \ndivides m).
  74 change with
  75 (match divides_b n1 m with
  76 [ true \Rightarrow n1
  77 | false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land
  78 (match divides_b n1 m with
  79 [ true \Rightarrow n1
  80 | false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1.
  81 elim Hcut.rewrite > divides_to_divides_b_true.
  82 simplify.
  83 split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
  84 assumption.assumption.
  85 rewrite > not_divides_to_divides_b_false.
  86 change with
  87 gcd_aux n n1 (mod m n1) \divides m \land
  88 gcd_aux n n1 (mod m n1) \divides n1.
  89 cut gcd_aux n n1 (mod m n1) \divides n1 \land
  90 gcd_aux n n1 (mod m n1) \divides mod m n1.
  91 elim Hcut1.
  92 split.apply divides_mod_to_divides ? ? n1.
  93 assumption.assumption.assumption.assumption.
  94 apply H.
  95 cut O \lt mod m n1 \lor O = mod m n1.
  96 elim Hcut1.assumption.
  97 apply False_ind.apply H4.apply mod_O_to_divides.
  98 assumption.apply sym_eq.assumption.
  99 apply le_to_or_lt_eq.apply le_O_n.
 100 apply lt_to_le.
 101 apply lt_mod_m_m.assumption.
 102 apply le_S_S_to_le.
 103 apply trans_le ? n1.
 104 change with mod m n1 < n1.
 105 apply lt_mod_m_m.assumption.assumption.
 106 assumption.assumption.
 107 apply decidable_divides n1 m.assumption.
 108 qed.
 109
 110 theorem divides_gcd_nm: \forall n,m.
 111 gcd n m \divides m \land gcd n m \divides n.
 112 intros.
 113 change with
 114 match leb n m with
 115   [ true \Rightarrow
 116     match n with
 117     [ O \Rightarrow m
 118     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 119   | false \Rightarrow
 120     match m with
 121     [ O \Rightarrow n
 122     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
 123 \land
 124 match leb n m with
 125   [ true \Rightarrow
 126     match n with
 127     [ O \Rightarrow m
 128     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 129   | false \Rightarrow
 130     match m with
 131     [ O \Rightarrow n
 132     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n.
 133 apply leb_elim n m.
 134 apply nat_case1 n.
 135 simplify.intros.split.
 136 apply witness m m (S O).apply times_n_SO.
 137 apply witness m O O.apply times_n_O.
 138 intros.change with
 139 gcd_aux (S m1) m (S m1) \divides m
 140 \land
 141 gcd_aux (S m1) m (S m1) \divides (S m1).
 142 apply divides_gcd_aux_mn.
 143 simplify.apply le_S_S.apply le_O_n.
 144 assumption.apply le_n.
 145 simplify.intro.
 146 apply nat_case1 m.
 147 simplify.intros.split.
 148 apply witness n O O.apply times_n_O.
 149 apply witness n n (S O).apply times_n_SO.
 150 intros.change with
 151 gcd_aux (S m1) n (S m1) \divides (S m1)
 152 \land
 153 gcd_aux (S m1) n (S m1) \divides n.
 154 cut gcd_aux (S m1) n (S m1) \divides n
 155 \land
 156 gcd_aux (S m1) n (S m1) \divides S m1.
 157 elim Hcut.split.assumption.assumption.
 158 apply divides_gcd_aux_mn.
 159 simplify.apply le_S_S.apply le_O_n.
 160 apply not_lt_to_le.simplify.intro.apply H.
 161 rewrite > H1.apply trans_le ? (S n).
 162 apply le_n_Sn.assumption.apply le_n.
 163 qed.
 164
 165 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
 166 intros.
 167 exact proj2  ? ? (divides_gcd_nm n m).
 168 qed.
 169
 170 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
 171 intros.
 172 exact proj1 ? ? (divides_gcd_nm n m).
 173 qed.
 174
 175 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 176 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
 177 intro.elim p.
 178 absurd O < n.assumption.apply le_to_not_lt.assumption.
 179 change with
 180 d \divides
 181 (match divides_b n1 m with
 182 [ true \Rightarrow n1
 183 | false \Rightarrow gcd_aux n n1 (mod m n1)]).
 184 cut n1 \divides m \lor n1 \ndivides m.
 185 elim Hcut.
 186 rewrite > divides_to_divides_b_true.
 187 simplify.assumption.
 188 assumption.assumption.
 189 rewrite > not_divides_to_divides_b_false.
 190 change with d \divides gcd_aux n n1 (mod m n1).
 191 apply H.
 192 cut O \lt mod m n1 \lor O = mod m n1.
 193 elim Hcut1.assumption.
 194 absurd n1 \divides m.apply mod_O_to_divides.
 195 assumption.apply sym_eq.assumption.assumption.
 196 apply le_to_or_lt_eq.apply le_O_n.
 197 apply lt_to_le.
 198 apply lt_mod_m_m.assumption.
 199 apply le_S_S_to_le.
 200 apply trans_le ? n1.
 201 change with mod m n1 < n1.
 202 apply lt_mod_m_m.assumption.assumption.
 203 assumption.
 204 apply divides_mod.assumption.assumption.assumption.
 205 assumption.assumption.
 206 apply decidable_divides n1 m.assumption.
 207 qed.
 208
 209 theorem divides_d_gcd: \forall m,n,d.
 210 d \divides m \to d \divides n \to d \divides gcd n m.
 211 intros.
 212 change with
 213 d \divides
 214 match leb n m with
 215   [ true \Rightarrow
 216     match n with
 217     [ O \Rightarrow m
 218     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 219   | false \Rightarrow
 220     match m with
 221     [ O \Rightarrow n
 222     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 223 apply leb_elim n m.
 224 apply nat_case1 n.simplify.intros.assumption.
 225 intros.
 226 change with d \divides gcd_aux (S m1) m (S m1).
 227 apply divides_gcd_aux.
 228 simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 229 rewrite < H2.assumption.
 230 apply nat_case1 m.simplify.intros.assumption.
 231 intros.
 232 change with d \divides gcd_aux (S m1) n (S m1).
 233 apply divides_gcd_aux.
 234 simplify.apply le_S_S.apply le_O_n.
 235 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 236 rewrite < H2.assumption.
 237 qed.
 238
 239 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 240 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 241 intro.
 242 elim p.
 243 absurd O < n.assumption.apply le_to_not_lt.assumption.
 244 cut O < m.
 245 cut n1 \divides m \lor  n1 \ndivides m.
 246 change with
 247 \exists a,b.
 248 a*n1 - b*m = match divides_b n1 m with
 249 [ true \Rightarrow n1
 250 | false \Rightarrow gcd_aux n n1 (mod m n1)]
 251 \lor
 252 b*m - a*n1 = match divides_b n1 m with
 253 [ true \Rightarrow n1
 254 | false \Rightarrow gcd_aux n n1 (mod m n1)].
 255 elim Hcut1.
 256 rewrite > divides_to_divides_b_true.
 257 simplify.
 258 apply ex_intro ? ? (S O).
 259 apply ex_intro ? ? O.
 260 left.simplify.rewrite < plus_n_O.
 261 apply sym_eq.apply minus_n_O.
 262 assumption.assumption.
 263 rewrite > not_divides_to_divides_b_false.
 264 change with
 265 \exists a,b.
 266 a*n1 - b*m = gcd_aux n n1 (mod m n1)
 267 \lor
 268 b*m - a*n1 = gcd_aux n n1 (mod m n1).
 269 cut
 270 \exists a,b.
 271 a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
 272 \lor
 273 b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
 274 elim Hcut2.elim H5.elim H6.
 275 (* first case *)
 276 rewrite < H7.
 277 apply ex_intro ? ? (a1+a*(div m n1)).
 278 apply ex_intro ? ? a.
 279 right.
 280 rewrite < sym_plus.
 281 rewrite < sym_times n1.
 282 rewrite > distr_times_plus.
 283 rewrite > sym_times n1.
 284 rewrite > sym_times n1.
 285 rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
 286 rewrite > assoc_times.
 287 rewrite < sym_plus.
 288 rewrite > distr_times_plus.
 289 rewrite < eq_minus_minus_minus_plus.
 290 rewrite < sym_plus.
 291 rewrite < plus_minus.
 292 rewrite < minus_n_n.reflexivity.
 293 apply le_n.
 294 assumption.
 295 (* second case *)
 296 rewrite < H7.
 297 apply ex_intro ? ? (a1+a*(div m n1)).
 298 apply ex_intro ? ? a.
 299 left.
 300 rewrite > sym_times.
 301 rewrite > distr_times_plus.
 302 rewrite > sym_times.
 303 rewrite > sym_times n1.
 304 rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
 305 rewrite > distr_times_plus.
 306 rewrite > assoc_times.
 307 rewrite < eq_minus_minus_minus_plus.
 308 rewrite < sym_plus.
 309 rewrite < plus_minus.
 310 rewrite < minus_n_n.reflexivity.
 311 apply le_n.
 312 assumption.
 313 apply H n1 (mod m n1).
 314 cut O \lt mod m n1 \lor O = mod m n1.
 315 elim Hcut2.assumption.
 316 absurd n1 \divides m.apply mod_O_to_divides.
 317 assumption.
 318 symmetry.assumption.assumption.
 319 apply le_to_or_lt_eq.apply le_O_n.
 320 apply lt_to_le.
 321 apply lt_mod_m_m.assumption.
 322 apply le_S_S_to_le.
 323 apply trans_le ? n1.
 324 change with mod m n1 < n1.
 325 apply lt_mod_m_m.
 326 assumption.assumption.assumption.assumption.
 327 apply decidable_divides n1 m.assumption.
 328 apply lt_to_le_to_lt ? n1.assumption.assumption.
 329 qed.
 330
 331 theorem eq_minus_gcd:
 332  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 333 intros.
 334 change with
 335 \exists a,b.
 336 a*n - b*m =
 337 match leb n m with
 338   [ true \Rightarrow
 339     match n with
 340     [ O \Rightarrow m
 341     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 342   | false \Rightarrow
 343     match m with
 344     [ O \Rightarrow n
 345     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
 346 \lor b*m - a*n =
 347 match leb n m with
 348   [ true \Rightarrow
 349     match n with
 350     [ O \Rightarrow m
 351     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 352   | false \Rightarrow
 353     match m with
 354     [ O \Rightarrow n
 355     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 356 apply leb_elim n m.
 357 apply nat_case1 n.
 358 simplify.intros.
 359 apply ex_intro ? ? O.
 360 apply ex_intro ? ? (S O).
 361 right.simplify.
 362 rewrite < plus_n_O.
 363 apply sym_eq.apply minus_n_O.
 364 intros.
 365 change with
 366 \exists a,b.
 367 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 368 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
 369 apply eq_minus_gcd_aux.
 370 simplify. apply le_S_S.apply le_O_n.
 371 assumption.apply le_n.
 372 apply nat_case1 m.
 373 simplify.intros.
 374 apply ex_intro ? ? (S O).
 375 apply ex_intro ? ? O.
 376 left.simplify.
 377 rewrite < plus_n_O.
 378 apply sym_eq.apply minus_n_O.
 379 intros.
 380 change with
 381 \exists a,b.
 382 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 383 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
 384 cut
 385 \exists a,b.
 386 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 387 \lor
 388 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
 389 elim Hcut.elim H2.elim H3.
 390 apply ex_intro ? ? a1.
 391 apply ex_intro ? ? a.
 392 right.assumption.
 393 apply ex_intro ? ? a1.
 394 apply ex_intro ? ? a.
 395 left.assumption.
 396 apply eq_minus_gcd_aux.
 397 simplify. apply le_S_S.apply le_O_n.
 398 apply lt_to_le.apply not_le_to_lt.assumption.
 399 apply le_n.
 400 qed.
 401
 402 (* some properties of gcd *)
 403
 404 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 405 intro.simplify.reflexivity.
 406 qed.
 407
 408 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 409 m = O \land n = O.
 410 intros.cut O \divides n \land O \divides m.
 411 elim Hcut.elim H2.split.
 412 assumption.elim H1.assumption.
 413 rewrite < H.
 414 apply divides_gcd_nm.
 415 qed.
 416
 417 theorem symmetric_gcd: symmetric nat gcd.
 418 change with
 419 \forall n,m:nat. gcd n m = gcd m n.
 420 intros.
 421 cut O < (gcd n m) \lor O = (gcd n m).
 422 elim Hcut.
 423 cut O < (gcd m n) \lor O = (gcd m n).
 424 elim Hcut1.
 425 apply antisym_le.
 426 apply divides_to_le.assumption.
 427 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 428 apply divides_to_le.assumption.
 429 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 430 rewrite < H1.
 431 cut m=O \land n=O.
 432 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 433 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 434 apply le_to_or_lt_eq.apply le_O_n.
 435 rewrite < H.
 436 cut n=O \land m=O.
 437 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 438 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 439 apply le_to_or_lt_eq.apply le_O_n.
 440 qed.
 441
 442 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 443 symmetric_gcd.
 444
 445 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 446 intro.
 447 apply antisym_le.apply divides_to_le.simplify.apply le_n.
 448 apply divides_gcd_n.
 449 cut O < gcd (S O) n \lor O = gcd (S O) n.
 450 elim Hcut.assumption.
 451 apply False_ind.
 452 apply not_eq_O_S O.
 453 cut (S O)=O \land n=O.
 454 elim Hcut1.apply sym_eq.assumption.
 455 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 456 apply le_to_or_lt_eq.apply le_O_n.
 457 qed.
 458
 459 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 460 gcd n m = (S O).
 461 intros.simplify in H.change with gcd n m = (S O).
 462 elim H.
 463 apply antisym_le.
 464 apply not_lt_to_le.
 465 change with (S (S O)) \le gcd n m \to False.intro.
 466 apply H1.rewrite < H3 (gcd n m).
 467 apply divides_gcd_m.
 468 apply divides_gcd_n.assumption.
 469 cut O < gcd n m \lor O = gcd n m.
 470 elim Hcut.assumption.
 471 apply False_ind.
 472 apply not_le_Sn_O (S O).
 473 cut n=O \land m=O.
 474 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 475 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 476 apply le_to_or_lt_eq.apply le_O_n.
 477 qed.
 478
 479 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 480 n \divides p \lor n \divides q.
 481 intros.
 482 cut n \divides p \lor n \ndivides p.
 483 elim Hcut.
 484 left.assumption.
 485 right.
 486 cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
 487 elim Hcut1.elim H3.elim H4.
 488 (* first case *)
 489 rewrite > times_n_SO q.rewrite < H5.
 490 rewrite > distr_times_minus.
 491 rewrite > sym_times q (a1*p).
 492 rewrite > assoc_times a1.
 493 elim H1.rewrite > H6.
 494 rewrite < sym_times n.rewrite < assoc_times.
 495 rewrite > sym_times q.rewrite > assoc_times.
 496 rewrite < assoc_times a1.rewrite < sym_times n.
 497 rewrite > assoc_times n.
 498 rewrite < distr_times_minus.
 499 apply witness ? ? (q*a-a1*n2).reflexivity.
 500 (* second case *)
 501 rewrite > times_n_SO q.rewrite < H5.
 502 rewrite > distr_times_minus.
 503 rewrite > sym_times q (a1*p).
 504 rewrite > assoc_times a1.
 505 elim H1.rewrite > H6.
 506 rewrite < sym_times.rewrite > assoc_times.
 507 rewrite < assoc_times q.
 508 rewrite < sym_times n.
 509 rewrite < distr_times_minus.
 510 apply witness ? ? (n2*a1-q*a).reflexivity.
 511 (* end second case *)
 512 rewrite < prime_to_gcd_SO n p.
 513 apply eq_minus_gcd.
 514 assumption.assumption.
 515 apply decidable_divides n p.
 516 apply trans_lt ? (S O).simplify.apply le_n.
 517 simplify in H.elim H. assumption.
 518 qed.