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