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 (m \mod 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 (m \mod n).
  41 intros.elim H1.elim H2.
  42 (* apply (witness ? ? (n2 - n1*(m / n))). *)
  43 apply witness[|
  44 rewrite > distr_times_minus.
  45 rewrite < H3 in \vdash (? ? ? (? % ?)).
  46 rewrite < assoc_times.
  47 rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
  48 apply sym_eq.apply plus_to_minus.
  49 rewrite > sym_times.
  50 letin x \def div.
  51 rewrite < (div_mod ? ? H).
  52 reflexivity.
  53 ]
  54 qed.
  55
  56 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  57 p \divides (m \mod n) \to p \divides n \to p \divides m.
  58 intros.elim H1.elim H2.
  59 apply (witness p m ((n1*(m / n))+n2)).
  60 rewrite > distr_times_plus.
  61 rewrite < H3.
  62 rewrite < assoc_times.
  63 rewrite < H4.rewrite < sym_times.
  64 apply div_mod.assumption.
  65 qed.
  66
  67 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  68 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
  69 intro.elim p.
  70 absurd (O < n).assumption.apply le_to_not_lt.assumption.
  71 cut ((n1 \divides m) \lor (n1 \ndivides m)).
  72 simplify.
  73 elim Hcut.rewrite > divides_to_divides_b_true.
  74 simplify.
  75 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
  76 assumption.assumption.
  77 rewrite > not_divides_to_divides_b_false.
  78 simplify.
  79 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
  80 gcd_aux n n1 (m \mod n1) \divides mod m n1).
  81 elim Hcut1.
  82 split.apply (divides_mod_to_divides ? ? n1).
  83 assumption.assumption.assumption.assumption.
  84 apply H.
  85 cut (O \lt m \mod n1 \lor O = mod m n1).
  86 elim Hcut1.assumption.
  87 apply False_ind.apply H4.apply mod_O_to_divides.
  88 assumption.apply sym_eq.assumption.
  89 apply le_to_or_lt_eq.apply le_O_n.
  90 apply lt_to_le.
  91 apply lt_mod_m_m.assumption.
  92 apply le_S_S_to_le.
  93 apply (trans_le ? n1).
  94 change with (m \mod n1 < n1).
  95 apply lt_mod_m_m.assumption.assumption.
  96 assumption.assumption.
  97 apply (decidable_divides n1 m).assumption.
  98 qed.
  99
 100 theorem divides_gcd_nm: \forall n,m.
 101 gcd n m \divides m \land gcd n m \divides n.
 102 intros.
 103 (*CSC: simplify simplifies too much because of a redex in gcd *)
 104 change with
 105 (match leb n m with
 106   [ true \Rightarrow
 107     match n with
 108     [ O \Rightarrow m
 109     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 110   | false \Rightarrow
 111     match m with
 112     [ O \Rightarrow n
 113     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
 114 \land
 115 match leb n m with
 116   [ true \Rightarrow
 117     match n with
 118     [ O \Rightarrow m
 119     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 120   | false \Rightarrow
 121     match m with
 122     [ O \Rightarrow n
 123     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
 124 apply (leb_elim n m).
 125 apply (nat_case1 n).
 126 simplify.intros.split.
 127 apply (witness m m (S O)).apply times_n_SO.
 128 apply (witness m O O).apply times_n_O.
 129 intros.change with
 130 (gcd_aux (S m1) m (S m1) \divides m
 131 \land
 132 gcd_aux (S m1) m (S m1) \divides (S m1)).
 133 apply divides_gcd_aux_mn.
 134 unfold lt.apply le_S_S.apply le_O_n.
 135 assumption.apply le_n.
 136 simplify.intro.
 137 apply (nat_case1 m).
 138 simplify.intros.split.
 139 apply (witness n O O).apply times_n_O.
 140 apply (witness n n (S O)).apply times_n_SO.
 141 intros.change with
 142 (gcd_aux (S m1) n (S m1) \divides (S m1)
 143 \land
 144 gcd_aux (S m1) n (S m1) \divides n).
 145 cut (gcd_aux (S m1) n (S m1) \divides n
 146 \land
 147 gcd_aux (S m1) n (S m1) \divides S m1).
 148 elim Hcut.split.assumption.assumption.
 149 apply divides_gcd_aux_mn.
 150 unfold lt.apply le_S_S.apply le_O_n.
 151 apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
 152 rewrite > H1.apply (trans_le ? (S n)).
 153 apply le_n_Sn.assumption.apply le_n.
 154 qed.
 155
 156 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
 157 intros.
 158 exact (proj2  ? ? (divides_gcd_nm n m)).
 159 qed.
 160
 161 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
 162 intros.
 163 exact (proj1 ? ? (divides_gcd_nm n m)).
 164 qed.
 165
 166 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 167 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
 168 intro.elim p.
 169 absurd (O < n).assumption.apply le_to_not_lt.assumption.
 170 simplify.
 171 cut (n1 \divides m \lor n1 \ndivides m).
 172 elim Hcut.
 173 rewrite > divides_to_divides_b_true.
 174 simplify.assumption.
 175 assumption.assumption.
 176 rewrite > not_divides_to_divides_b_false.
 177 simplify.
 178 apply H.
 179 cut (O \lt m \mod n1 \lor O = m \mod n1).
 180 elim Hcut1.assumption.
 181 absurd (n1 \divides m).apply mod_O_to_divides.
 182 assumption.apply sym_eq.assumption.assumption.
 183 apply le_to_or_lt_eq.apply le_O_n.
 184 apply lt_to_le.
 185 apply lt_mod_m_m.assumption.
 186 apply le_S_S_to_le.
 187 apply (trans_le ? n1).
 188 change with (m \mod n1 < n1).
 189 apply lt_mod_m_m.assumption.assumption.
 190 assumption.
 191 apply divides_mod.assumption.assumption.assumption.
 192 assumption.assumption.
 193 apply (decidable_divides n1 m).assumption.
 194 qed.
 195
 196 theorem divides_d_gcd: \forall m,n,d.
 197 d \divides m \to d \divides n \to d \divides gcd n m.
 198 intros.
 199 (*CSC: here simplify simplifies too much because of a redex in gcd *)
 200 change with
 201 (d \divides
 202 match leb n m with
 203   [ true \Rightarrow
 204     match n with
 205     [ O \Rightarrow m
 206     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 207   | false \Rightarrow
 208     match m with
 209     [ O \Rightarrow n
 210     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 211 apply (leb_elim n m).
 212 apply (nat_case1 n).simplify.intros.assumption.
 213 intros.
 214 change with (d \divides gcd_aux (S m1) m (S m1)).
 215 apply divides_gcd_aux.
 216 unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 217 rewrite < H2.assumption.
 218 apply (nat_case1 m).simplify.intros.assumption.
 219 intros.
 220 change with (d \divides gcd_aux (S m1) n (S m1)).
 221 apply divides_gcd_aux.
 222 unfold lt.apply le_S_S.apply le_O_n.
 223 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 224 rewrite < H2.assumption.
 225 qed.
 226
 227 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 228 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 229 intro.
 230 elim p
 231   [absurd (O < n)
 232     [assumption
 233     |apply le_to_not_lt.assumption
 234     ]
 235   |cut (O < m)
 236     [cut (n1 \divides m \lor  n1 \ndivides m)
 237       [simplify.
 238        elim Hcut1
 239         [rewrite > divides_to_divides_b_true
 240           [simplify.
 241            apply (ex_intro ? ? (S O)).
 242            apply (ex_intro ? ? O).
 243            left.
 244            simplify.
 245            rewrite < plus_n_O.
 246            apply sym_eq.
 247            apply minus_n_O
 248           |assumption
 249           |assumption
 250           ]
 251         |rewrite > not_divides_to_divides_b_false
 252           [change with
 253            (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 254             \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 255            cut
 256            (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 257             \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
 258             [elim Hcut2.elim H5.elim H6
 259               [(* first case *)
 260                rewrite < H7.
 261                apply (ex_intro ? ? (a1+a*(m / n1))).
 262                apply (ex_intro ? ? a).
 263                right.
 264                rewrite < sym_plus.
 265                rewrite < (sym_times n1).
 266                rewrite > distr_times_plus.
 267                rewrite > (sym_times n1).
 268                rewrite > (sym_times n1).
 269                rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
 270                 [rewrite > assoc_times.
 271                  rewrite < sym_plus.
 272                  rewrite > distr_times_plus.
 273                  rewrite < eq_minus_minus_minus_plus.
 274                  rewrite < sym_plus.
 275                  rewrite < plus_minus
 276                   [rewrite < minus_n_n.reflexivity
 277                   |apply le_n
 278                   ]
 279                 |assumption
 280                 ]
 281               |(* second case *)
 282               rewrite < H7.
 283                apply (ex_intro ? ? (a1+a*(m / n1))).
 284                apply (ex_intro ? ? a).
 285                left.
 286                (* clear Hcut2.clear H5.clear H6.clear H. *)
 287                rewrite > sym_times.
 288                rewrite > distr_times_plus.
 289                rewrite > sym_times.
 290                rewrite > (sym_times n1).
 291                rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
 292                 [rewrite > distr_times_plus.
 293                  rewrite > assoc_times.
 294                  rewrite < eq_minus_minus_minus_plus.
 295                  rewrite < sym_plus.
 296                  rewrite < plus_minus
 297                   [rewrite < minus_n_n.reflexivity
 298                   |apply le_n
 299                   ]
 300                 |assumption
 301                 ]
 302               ]
 303             |apply (H n1 (m \mod n1))
 304               [cut (O \lt m \mod n1 \lor O = m \mod n1)
 305                 [elim Hcut2
 306                   [assumption
 307                   |absurd (n1 \divides m)
 308                     [apply mod_O_to_divides
 309                       [assumption
 310                       |symmetry.assumption
 311                       ]
 312                     |assumption
 313                     ]
 314                   ]
 315                 |apply le_to_or_lt_eq.
 316                  apply le_O_n
 317                 ]
 318               |apply lt_to_le.
 319                apply lt_mod_m_m.
 320                assumption
 321               |apply le_S_S_to_le.
 322                apply (trans_le ? n1)
 323                 [change with (m \mod n1 < n1).
 324                  apply lt_mod_m_m.
 325                  assumption
 326                 |assumption
 327                 ]
 328               ]
 329             ]
 330           |assumption
 331           |assumption
 332           ]
 333         ]
 334       |apply (decidable_divides n1 m).
 335        assumption
 336       ]
 337     |apply (lt_to_le_to_lt ? n1);assumption
 338     ]
 339   ]
 340 qed.
 341
 342 theorem eq_minus_gcd:
 343  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 344 intros.
 345 unfold gcd.
 346 apply (leb_elim n m).
 347 apply (nat_case1 n).
 348 simplify.intros.
 349 apply (ex_intro ? ? O).
 350 apply (ex_intro ? ? (S O)).
 351 right.simplify.
 352 rewrite < plus_n_O.
 353 apply sym_eq.apply minus_n_O.
 354 intros.
 355 change with
 356 (\exists a,b.
 357 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 358 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 359 apply eq_minus_gcd_aux.
 360 unfold lt. apply le_S_S.apply le_O_n.
 361 assumption.apply le_n.
 362 apply (nat_case1 m).
 363 simplify.intros.
 364 apply (ex_intro ? ? (S O)).
 365 apply (ex_intro ? ? O).
 366 left.simplify.
 367 rewrite < plus_n_O.
 368 apply sym_eq.apply minus_n_O.
 369 intros.
 370 change with
 371 (\exists a,b.
 372 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 373 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 374 cut
 375 (\exists a,b.
 376 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 377 \lor
 378 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
 379 elim Hcut.elim H2.elim H3.
 380 apply (ex_intro ? ? a1).
 381 apply (ex_intro ? ? a).
 382 right.assumption.
 383 apply (ex_intro ? ? a1).
 384 apply (ex_intro ? ? a).
 385 left.assumption.
 386 apply eq_minus_gcd_aux.
 387 unfold lt. apply le_S_S.apply le_O_n.
 388 apply lt_to_le.apply not_le_to_lt.assumption.
 389 apply le_n.
 390 qed.
 391
 392 (* some properties of gcd *)
 393
 394 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 395 intro.simplify.reflexivity.
 396 qed.
 397
 398 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 399 m = O \land n = O.
 400 intros.cut (O \divides n \land O \divides m).
 401 elim Hcut.elim H2.split.
 402 assumption.elim H1.assumption.
 403 rewrite < H.
 404 apply divides_gcd_nm.
 405 qed.
 406
 407 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 408 intros.
 409 apply (nat_case1 (gcd m n)).
 410 intros.
 411 generalize in match (gcd_O_to_eq_O m n H1).
 412 intros.elim H2.
 413 rewrite < H4 in \vdash (? ? %).assumption.
 414 intros.unfold lt.apply le_S_S.apply le_O_n.
 415 qed.
 416
 417 theorem gcd_n_n: \forall n.gcd n n = n.
 418 intro.elim n
 419   [reflexivity
 420   |apply le_to_le_to_eq
 421     [apply divides_to_le
 422       [apply lt_O_S
 423       |apply divides_gcd_n
 424       ]
 425     |apply divides_to_le
 426       [apply lt_O_gcd.apply lt_O_S
 427       |apply divides_d_gcd
 428         [apply divides_n_n|apply divides_n_n]
 429       ]
 430     ]
 431   ]
 432 qed.
 433
 434 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
 435 O < i.
 436 intros.
 437 elim (le_to_or_lt_eq ? ? (le_O_n i))
 438   [assumption
 439   |absurd ((gcd i n) = (S O))
 440     [assumption
 441     |rewrite < H2.
 442      simplify.
 443      unfold.intro.
 444      apply (lt_to_not_eq (S O) n H).
 445      apply sym_eq.assumption
 446     ]
 447   ]
 448 qed.
 449
 450 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
 451 i < n.
 452 intros.
 453 elim (le_to_or_lt_eq ? ? H1)
 454   [assumption
 455   |absurd ((gcd i n) = (S O))
 456     [assumption
 457     |rewrite > H3.
 458      rewrite > gcd_n_n.
 459      unfold.intro.
 460      apply (lt_to_not_eq (S O) n H).
 461      apply sym_eq.assumption
 462     ]
 463   ]
 464 qed.
 465
 466 theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
 467 intro.apply (nat_case n)
 468   [intros.reflexivity
 469   |intros.
 470    apply le_to_le_to_eq
 471     [apply divides_to_le
 472       [apply lt_O_S|apply divides_gcd_n]
 473     |apply divides_to_le
 474       [apply lt_O_gcd.rewrite > (times_n_O O).
 475        apply lt_times[apply lt_O_S|assumption]
 476       |apply divides_d_gcd
 477         [apply (witness ? ? m1).reflexivity
 478         |apply divides_n_n
 479         ]
 480       ]
 481     ]
 482   ]
 483 qed.
 484
 485 theorem symmetric_gcd: symmetric nat gcd.
 486 (*CSC: bug here: unfold symmetric does not work *)
 487 change with
 488 (\forall n,m:nat. gcd n m = gcd m n).
 489 intros.
 490 cut (O < (gcd n m) \lor O = (gcd n m)).
 491 elim Hcut.
 492 cut (O < (gcd m n) \lor O = (gcd m n)).
 493 elim Hcut1.
 494 apply antisym_le.
 495 apply divides_to_le.assumption.
 496 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 497 apply divides_to_le.assumption.
 498 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 499 rewrite < H1.
 500 cut (m=O \land n=O).
 501 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 502 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 503 apply le_to_or_lt_eq.apply le_O_n.
 504 rewrite < H.
 505 cut (n=O \land m=O).
 506 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 507 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 508 apply le_to_or_lt_eq.apply le_O_n.
 509 qed.
 510
 511 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 512 symmetric_gcd.
 513
 514 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 515 intros.
 516 apply (nat_case n).apply le_n.
 517 intro.
 518 apply divides_to_le.
 519 apply lt_O_gcd.
 520 rewrite > (times_n_O O).
 521 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
 522 apply divides_d_gcd.
 523 apply (transitive_divides ? (S m1)).
 524 apply divides_gcd_m.
 525 apply (witness ? ? p).reflexivity.
 526 apply divides_gcd_n.
 527 qed.
 528
 529 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
 530 gcd m (n*p) = (S O) \to gcd m n = (S O).
 531 intros.
 532 apply antisymmetric_le.
 533 rewrite < H2.
 534 apply le_gcd_times.assumption.
 535 change with (O < gcd m n).
 536 apply lt_O_gcd.assumption.
 537 qed.
 538
 539 (* for the "converse" of the previous result see the end  of this development *)
 540
 541 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
 542 (gcd n m) = (S O) \to \lnot (divides n m).
 543 intros.unfold.intro.
 544 elim H2.
 545 generalize in match H1.
 546 rewrite > H3.
 547 intro.
 548 cut (O < n2)
 549   [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
 550     [cut (gcd n (n*n2) = n)
 551       [apply (lt_to_not_eq (S O) n)
 552         [assumption|rewrite < H4.assumption]
 553       |apply gcd_n_times_nm.assumption
 554       ]
 555     |apply (trans_lt ? (S O))[apply le_n|assumption]
 556     |assumption
 557     ]
 558   |elim (le_to_or_lt_eq O n2 (le_O_n n2));
 559     [assumption
 560     |apply False_ind.
 561      apply (le_to_not_lt n (S O))
 562       [rewrite < H4.
 563        apply divides_to_le
 564         [rewrite > H4.apply lt_O_S
 565         |apply divides_d_gcd
 566           [apply (witness ? ? n2).reflexivity
 567           |apply divides_n_n
 568           ]
 569         ]
 570       |assumption
 571       ]
 572     ]
 573   ]
 574 qed.
 575
 576 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 577 intro.
 578 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
 579 apply divides_gcd_n.
 580 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 581 elim Hcut.assumption.
 582 apply False_ind.
 583 apply (not_eq_O_S O).
 584 cut ((S O)=O \land n=O).
 585 elim Hcut1.apply sym_eq.assumption.
 586 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 587 apply le_to_or_lt_eq.apply le_O_n.
 588 qed.
 589
 590 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 591 divides (gcd m n) (gcd n (m \mod n)).
 592 intros.
 593 apply divides_d_gcd.
 594 apply divides_mod.assumption.
 595 apply divides_gcd_n.
 596 apply divides_gcd_m.
 597 apply divides_gcd_m.
 598 qed.
 599
 600 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 601 divides (gcd n (m \mod n)) (gcd m n) .
 602 intros.
 603 apply divides_d_gcd.
 604 apply divides_gcd_n.
 605 apply (divides_mod_to_divides ? ? n).
 606 assumption.
 607 apply divides_gcd_m.
 608 apply divides_gcd_n.
 609 qed.
 610
 611 theorem gcd_mod: \forall m,n:nat. O < n \to
 612 (gcd n (m \mod n)) = (gcd m n) .
 613 intros.
 614 apply antisymmetric_divides.
 615 apply divides_mod_gcd.assumption.
 616 apply divides_gcd_mod.assumption.
 617 qed.
 618
 619 (* gcd and primes *)
 620
 621 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 622 gcd n m = (S O).
 623 intros.unfold prime in H.
 624 elim H.
 625 apply antisym_le.
 626 apply not_lt_to_le.unfold Not.unfold lt.
 627 intro.
 628 apply H1.rewrite < (H3 (gcd n m)).
 629 apply divides_gcd_m.
 630 apply divides_gcd_n.assumption.
 631 cut (O < gcd n m \lor O = gcd n m).
 632 elim Hcut.assumption.
 633 apply False_ind.
 634 apply (not_le_Sn_O (S O)).
 635 cut (n=O \land m=O).
 636 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 637 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 638 apply le_to_or_lt_eq.apply le_O_n.
 639 qed.
 640
 641 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 642 n \divides p \lor n \divides q.
 643 intros.
 644 cut (n \divides p \lor n \ndivides p)
 645   [elim Hcut
 646     [left.assumption
 647     |right.
 648      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
 649        [elim Hcut1.elim H3.elim H4
 650          [(* first case *)
 651           rewrite > (times_n_SO q).rewrite < H5.
 652           rewrite > distr_times_minus.
 653           rewrite > (sym_times q (a1*p)).
 654           rewrite > (assoc_times a1).
 655           elim H1.
 656           (*
 657              rewrite > H6.
 658              applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
 659              reflexivity. *);
 660           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
 661           (*
 662           rewrite < (sym_times n).rewrite < assoc_times.
 663           rewrite > (sym_times q).rewrite > assoc_times.
 664           rewrite < (assoc_times a1).rewrite < (sym_times n).
 665           rewrite > (assoc_times n).
 666           rewrite < distr_times_minus.
 667           apply (witness ? ? (q*a-a1*n2)).reflexivity
 668           *)
 669          |(* second case *)
 670           rewrite > (times_n_SO q).rewrite < H5.
 671           rewrite > distr_times_minus.
 672           rewrite > (sym_times q (a1*p)).
 673           rewrite > (assoc_times a1).
 674           elim H1.rewrite > H6.
 675           rewrite < sym_times.rewrite > assoc_times.
 676           rewrite < (assoc_times q).
 677           rewrite < (sym_times n).
 678           rewrite < distr_times_minus.
 679           apply (witness ? ? (n2*a1-q*a)).reflexivity
 680         ](* end second case *)
 681      |rewrite < (prime_to_gcd_SO n p)
 682        [apply eq_minus_gcd|assumption|assumption
 683        ]
 684      ]
 685    ]
 686  |apply (decidable_divides n p).
 687   apply (trans_lt ? (S O))
 688     [unfold lt.apply le_n
 689     |unfold prime in H.elim H. assumption
 690     ]
 691   ]
 692 qed.
 693
 694 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 695 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 696 intros.
 697 apply antisymmetric_le.
 698 apply not_lt_to_le.
 699 unfold Not.intro.
 700 cut (divides (smallest_factor (gcd m (n*p))) n \lor
 701      divides (smallest_factor (gcd m (n*p))) p).
 702 elim Hcut.
 703 apply (not_le_Sn_n (S O)).
 704 change with ((S O) < (S O)).
 705 rewrite < H2 in \vdash (? ? %).
 706 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 707 apply lt_SO_smallest_factor.assumption.
 708 apply divides_to_le.
 709 rewrite > H2.unfold lt.apply le_n.
 710 apply divides_d_gcd.assumption.
 711 apply (transitive_divides ? (gcd m (n*p))).
 712 apply divides_smallest_factor_n.
 713 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 714 apply divides_gcd_n.
 715 apply (not_le_Sn_n (S O)).
 716 change with ((S O) < (S O)).
 717 rewrite < H3 in \vdash (? ? %).
 718 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 719 apply lt_SO_smallest_factor.assumption.
 720 apply divides_to_le.
 721 rewrite > H3.unfold lt.apply le_n.
 722 apply divides_d_gcd.assumption.
 723 apply (transitive_divides ? (gcd m (n*p))).
 724 apply divides_smallest_factor_n.
 725 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 726 apply divides_gcd_n.
 727 apply divides_times_to_divides.
 728 apply prime_smallest_factor_n.
 729 assumption.
 730 apply (transitive_divides ? (gcd m (n*p))).
 731 apply divides_smallest_factor_n.
 732 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
 733 apply divides_gcd_m.
 734 change with (O < gcd m (n*p)).
 735 apply lt_O_gcd.
 736 rewrite > (times_n_O O).
 737 apply lt_times.assumption.assumption.
 738 qed.
 739
 740 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
 741 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
 742 intros.
 743 cut (n \divides p \lor n \ndivides p)
 744   [elim Hcut
 745     [assumption
 746     |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
 747       [elim Hcut1.elim H4.elim H5
 748         [(* first case *)
 749           rewrite > (times_n_SO p).rewrite < H6.
 750           rewrite > distr_times_minus.
 751           rewrite > (sym_times p (a1*m)).
 752           rewrite > (assoc_times a1).
 753           elim H2.
 754           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
 755          |(* second case *)
 756           rewrite > (times_n_SO p).rewrite < H6.
 757           rewrite > distr_times_minus.
 758           rewrite > (sym_times p (a1*m)).
 759           rewrite > (assoc_times a1).
 760           elim H2.
 761           applyS (witness n ? ? (refl_eq ? ?)).
 762         ](* end second case *)
 763      |rewrite < H1.apply eq_minus_gcd.
 764      ]
 765    ]
 766  |apply (decidable_divides n p).
 767   assumption.
 768  ]
 769 qed.