matita/library_auto/auto/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/library_auto/nat/gcd".
  16
  17 include "auto/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.
  49   apply plus_to_minus.
  50   rewrite > sym_times.
  51   auto.
  52   (*letin x \def div.
  53   rewrite < (div_mod ? ? H).
  54   reflexivity.*)
  55 (*]*)
  56 qed.
  57
  58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  59 p \divides (m \mod n) \to p \divides n \to p \divides m.
  60 intros.
  61 elim H1.
  62 elim H2.
  63 apply (witness p m ((n1*(m / n))+n2)).
  64 rewrite > distr_times_plus.
  65 rewrite < H3.
  66 rewrite < assoc_times.
  67 rewrite < H4.
  68 rewrite < sym_times.
  69 auto.
  70 (*apply div_mod.
  71 assumption.*)
  72 qed.
  73
  74
  75 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  76 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
  77 intro.
  78 elim p
  79 [ absurd (O < n);auto
  80   (*[ assumption
  81   | apply le_to_not_lt.
  82     assumption
  83   ]*)
  84 | cut ((n1 \divides m) \lor (n1 \ndivides m))
  85   [ simplify.
  86     elim Hcut
  87     [ rewrite > divides_to_divides_b_true
  88       [ simplify.
  89         auto
  90         (*split
  91         [ assumption
  92         | apply (witness n1 n1 (S O)).
  93           apply times_n_SO
  94         ]*)
  95       | assumption
  96       | assumption
  97     ]
  98     | rewrite > not_divides_to_divides_b_false
  99       [ simplify.
 100         cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
 101         gcd_aux n n1 (m \mod n1) \divides mod m n1)
 102         [ elim Hcut1.
 103           auto
 104           (*split
 105           [ apply (divides_mod_to_divides ? ? n1);assumption
 106           | assumption
 107           ]*)
 108         | apply H
 109           [ cut (O \lt m \mod n1 \lor O = mod m n1)
 110             [ elim Hcut1
 111               [ assumption
 112               | apply False_ind.
 113                 auto
 114                 (*apply H4.
 115                 apply mod_O_to_divides
 116                 [ assumption
 117                 | apply sym_eq.
 118                   assumption
 119                 ]*)
 120               ]
 121             | auto
 122               (*apply le_to_or_lt_eq.
 123               apply le_O_n*)
 124             ]
 125           | auto
 126             (*apply lt_to_le.
 127             apply lt_mod_m_m.
 128             assumption*)
 129           | apply le_S_S_to_le.
 130             apply (trans_le ? n1);auto
 131             (*[ auto.change with (m \mod n1 < n1).
 132               apply lt_mod_m_m.
 133               assumption
 134             | assumption
 135             ]*)
 136           ]
 137         ]
 138       | assumption
 139       | assumption
 140       ]
 141     ]
 142   | auto
 143     (*apply (decidable_divides n1 m).
 144     assumption*)
 145   ]
 146 ]
 147 qed.
 148
 149 theorem divides_gcd_nm: \forall n,m.
 150 gcd n m \divides m \land gcd n m \divides n.
 151 intros.
 152 (*CSC: simplify simplifies too much because of a redex in gcd *)
 153 change with
 154 (match leb n m with
 155   [ true \Rightarrow
 156     match n with
 157     [ O \Rightarrow m
 158     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 159   | false \Rightarrow
 160     match m with
 161     [ O \Rightarrow n
 162     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
 163 \land
 164 match leb n m with
 165   [ true \Rightarrow
 166     match n with
 167     [ O \Rightarrow m
 168     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 169   | false \Rightarrow
 170     match m with
 171     [ O \Rightarrow n
 172     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
 173 apply (leb_elim n m)
 174 [ apply (nat_case1 n)
 175   [ simplify.
 176     intros.
 177     auto
 178     (*split
 179     [ apply (witness m m (S O)).
 180       apply times_n_SO
 181     | apply (witness m O O).
 182       apply times_n_O
 183     ]*)
 184   | intros.
 185     change with
 186     (gcd_aux (S m1) m (S m1) \divides m
 187     \land
 188     gcd_aux (S m1) m (S m1) \divides (S m1)).
 189     auto
 190     (*apply divides_gcd_aux_mn
 191     [ unfold lt.
 192       apply le_S_S.
 193       apply le_O_n
 194     | assumption
 195     | apply le_n
 196     ]*)
 197   ]
 198 | simplify.
 199   intro.
 200   apply (nat_case1 m)
 201   [ simplify.
 202     intros.
 203     auto
 204     (*split
 205     [ apply (witness n O O).
 206       apply times_n_O
 207     | apply (witness n n (S O)).
 208       apply times_n_SO
 209     ]*)
 210   | intros.
 211     change with
 212     (gcd_aux (S m1) n (S m1) \divides (S m1)
 213     \land
 214     gcd_aux (S m1) n (S m1) \divides n).
 215     cut (gcd_aux (S m1) n (S m1) \divides n
 216     \land
 217     gcd_aux (S m1) n (S m1) \divides S m1)
 218     [ elim Hcut.
 219       auto
 220       (*split;assumption*)
 221     | apply divides_gcd_aux_mn
 222       [ auto
 223         (*unfold lt.
 224         apply le_S_S.
 225         apply le_O_n*)
 226       | apply not_lt_to_le.
 227         unfold Not.
 228         unfold lt.
 229         intro.
 230         apply H.
 231         rewrite > H1.
 232         auto
 233         (*apply (trans_le ? (S n))
 234         [ apply le_n_Sn
 235         | assumption
 236         ]*)
 237       | apply le_n
 238       ]
 239     ]
 240   ]
 241 ]
 242 qed.
 243
 244 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
 245 intros.
 246 exact (proj2  ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
 247 qed.
 248
 249 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
 250 intros.
 251 exact (proj1 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
 252 qed.
 253
 254 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 255 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
 256 intro.
 257 elim p
 258 [ absurd (O < n);auto
 259   (*[ assumption
 260   | apply le_to_not_lt.
 261     assumption
 262   ]*)
 263 | simplify.
 264   cut (n1 \divides m \lor n1 \ndivides m)
 265   [ elim Hcut.
 266     rewrite > divides_to_divides_b_true;auto.
 267     (*[ simplify.
 268       assumption.
 269     | assumption.
 270     | assumption.
 271     ]*)
 272     rewrite > not_divides_to_divides_b_false
 273     [ simplify.
 274       apply H
 275       [ cut (O \lt m \mod n1 \lor O = m \mod n1)
 276         [ elim Hcut1
 277           [ assumption
 278           |
 279             absurd (n1 \divides m);auto
 280             (*[ apply mod_O_to_divides
 281               [ assumption.
 282               | apply sym_eq.assumption.
 283               ]
 284             | assumption
 285             ]*)
 286           ]
 287         | auto
 288           (*apply le_to_or_lt_eq.
 289           apply le_O_n*)
 290         ]
 291       | auto
 292         (*apply lt_to_le.
 293         apply lt_mod_m_m.
 294         assumption*)
 295       | apply le_S_S_to_le.
 296         auto
 297         (*apply (trans_le ? n1)
 298         [ change with (m \mod n1 < n1).
 299           apply lt_mod_m_m.
 300           assumption
 301         | assumption
 302         ]*)
 303       | assumption
 304       | auto
 305         (*apply divides_mod;
 306         assumption*)
 307       ]
 308     | assumption
 309     | assumption
 310     ]
 311   | auto
 312     (*apply (decidable_divides n1 m).
 313     assumption*)
 314   ]
 315 ]qed.
 316
 317 theorem divides_d_gcd: \forall m,n,d.
 318 d \divides m \to d \divides n \to d \divides gcd n m.
 319 intros.
 320 (*CSC: here simplify simplifies too much because of a redex in gcd *)
 321 change with
 322 (d \divides
 323 match leb n m with
 324   [ true \Rightarrow
 325     match n with
 326     [ O \Rightarrow m
 327     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 328   | false \Rightarrow
 329     match m with
 330     [ O \Rightarrow n
 331     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 332 apply (leb_elim n m)
 333 [ apply (nat_case1 n)
 334   [ simplify.
 335     intros.
 336     assumption
 337   | intros.
 338     change with (d \divides gcd_aux (S m1) m (S m1)).
 339     apply divides_gcd_aux
 340     [ auto
 341       (*unfold lt.
 342       apply le_S_S.
 343       apply le_O_n.*)
 344     | assumption.
 345     | apply le_n. (*chiude il goal anche con auto*)
 346     | assumption.
 347     | rewrite < H2.
 348       assumption
 349     ]
 350   ]
 351 | apply (nat_case1 m)
 352   [ simplify.
 353     intros.
 354     assumption
 355   | intros.
 356     change with (d \divides gcd_aux (S m1) n (S m1)).
 357     apply divides_gcd_aux
 358     [ auto
 359       (*unfold lt.
 360       apply le_S_S.
 361       apply le_O_n*)
 362     | auto
 363       (*apply lt_to_le.
 364       apply not_le_to_lt.
 365       assumption*)
 366     | apply le_n (*chiude il goal anche con auto*)
 367     | assumption
 368     | rewrite < H2.
 369       assumption
 370     ]
 371   ]
 372 ]
 373 qed.
 374
 375 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 376 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 377 intro.
 378 elim p
 379 [ absurd (O < n);auto
 380   (*[ assumption
 381   | apply le_to_not_lt
 382     assumption.
 383   ]*)
 384 | cut (O < m)
 385   [ cut (n1 \divides m \lor  n1 \ndivides m)
 386     [ simplify.
 387       elim Hcut1
 388       [ rewrite > divides_to_divides_b_true
 389         [ simplify.
 390           apply (ex_intro ? ? (S O)).
 391           apply (ex_intro ? ? O).
 392           auto
 393           (*left.
 394           simplify.
 395           rewrite < plus_n_O.
 396           apply sym_eq.apply minus_n_O*)
 397         | assumption
 398         | assumption
 399         ]
 400       | rewrite > not_divides_to_divides_b_false
 401         [ change with
 402           (\exists a,b.
 403           a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 404           \lor
 405           b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 406           cut
 407           (\exists a,b.
 408           a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 409           \lor
 410           b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
 411           [ elim Hcut2.
 412             elim H5.
 413             elim H6
 414             [ (* first case *)
 415               rewrite < H7.
 416               apply (ex_intro ? ? (a1+a*(m / n1))).
 417               apply (ex_intro ? ? a).
 418               right.
 419               rewrite < sym_plus.
 420               rewrite < (sym_times n1).
 421               rewrite > distr_times_plus.
 422               rewrite > (sym_times n1).
 423               rewrite > (sym_times n1).
 424               rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);auto
 425               (*[ rewrite > assoc_times.
 426                 rewrite < sym_plus.
 427                 rewrite > distr_times_plus.
 428                 rewrite < eq_minus_minus_minus_plus.
 429                 rewrite < sym_plus.auto.
 430                 rewrite < plus_minus
 431                 [ rewrite < minus_n_n.
 432                   reflexivity
 433                 | apply le_n
 434                 ]
 435               | assumption
 436               ]*)
 437             | (* second case *)
 438               rewrite < H7.
 439               apply (ex_intro ? ? (a1+a*(m / n1))).
 440               apply (ex_intro ? ? a).
 441               left.
 442               (* clear Hcut2.clear H5.clear H6.clear H. *)
 443               rewrite > sym_times.
 444               rewrite > distr_times_plus.
 445               rewrite > sym_times.
 446               rewrite > (sym_times n1).
 447               rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
 448               [ rewrite > distr_times_plus.
 449                 rewrite > assoc_times.
 450                 rewrite < eq_minus_minus_minus_plus.
 451                 auto
 452                 (*rewrite < sym_plus.
 453                 rewrite < plus_minus
 454                 [ rewrite < minus_n_n.
 455                   reflexivity
 456                 | apply le_n
 457                 ]*)
 458               | assumption
 459               ]
 460             ]
 461           | apply (H n1 (m \mod n1))
 462             [ cut (O \lt m \mod n1 \lor O = m \mod n1)
 463               [ elim Hcut2
 464                 [ assumption
 465                 | absurd (n1 \divides m);auto
 466                   (*[ apply mod_O_to_divides
 467                     [ assumption
 468                     | symmetry.
 469                       assumption
 470                     ]
 471                   | assumption
 472                   ]*)
 473                 ]
 474               | auto
 475                 (*apply le_to_or_lt_eq.
 476                 apply le_O_n*)
 477               ]
 478             | auto
 479               (*apply lt_to_le.
 480               apply lt_mod_m_m.
 481               assumption*)
 482             | apply le_S_S_to_le.
 483               auto
 484               (*apply (trans_le ? n1)
 485               [ change with (m \mod n1 < n1).
 486                 apply lt_mod_m_m.
 487                 assumption
 488               | assumption
 489               ]*)
 490             ]
 491           ]
 492         | assumption
 493         | assumption
 494         ]
 495       ]
 496     | auto
 497       (*apply (decidable_divides n1 m).
 498       assumption*)
 499     ]
 500   | auto
 501     (*apply (lt_to_le_to_lt ? n1);assumption *)
 502   ]
 503 ]
 504 qed.
 505
 506 theorem eq_minus_gcd:
 507  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 508 intros.
 509 unfold gcd.
 510 apply (leb_elim n m)
 511 [ apply (nat_case1 n)
 512   [ simplify.
 513     intros.
 514     apply (ex_intro ? ? O).
 515     apply (ex_intro ? ? (S O)).
 516     auto
 517     (*right.simplify.
 518     rewrite < plus_n_O.
 519     apply sym_eq.
 520     apply minus_n_O*)
 521   | intros.
 522     change with
 523     (\exists a,b.
 524     a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 525     \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 526     auto
 527     (*apply eq_minus_gcd_aux
 528     [ unfold lt.
 529       apply le_S_S.
 530       apply le_O_n
 531     | assumption
 532     | apply le_n
 533     ]*)
 534   ]
 535 | apply (nat_case1 m)
 536   [ simplify.
 537     intros.
 538     apply (ex_intro ? ? (S O)).
 539     apply (ex_intro ? ? O).
 540     auto
 541     (*left.simplify.
 542     rewrite < plus_n_O.
 543     apply sym_eq.
 544     apply minus_n_O*)
 545   | intros.
 546     change with
 547     (\exists a,b.
 548     a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 549     \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 550     cut
 551     (\exists a,b.
 552     a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 553     \lor
 554     b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))
 555     [ elim Hcut.
 556       elim H2.
 557       elim H3;apply (ex_intro ? ? a1);auto
 558       (*[ apply (ex_intro ? ? a1).
 559         apply (ex_intro ? ? a).
 560         right.
 561         assumption
 562       | apply (ex_intro ? ? a1).
 563         apply (ex_intro ? ? a).
 564         left.
 565         assumption
 566       ]*)
 567     | apply eq_minus_gcd_aux;auto
 568       (*[ unfold lt.
 569         apply le_S_S.
 570         apply le_O_n
 571       | auto.apply lt_to_le.
 572         apply not_le_to_lt.
 573         assumption
 574       | apply le_n.
 575       ]*)
 576     ]
 577   ]
 578 ]
 579 qed.
 580
 581 (* some properties of gcd *)
 582
 583 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 584 auto.
 585 (*intro.simplify.reflexivity.*)
 586 qed.
 587
 588 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 589 m = O \land n = O.
 590 intros.
 591 cut (O \divides n \land O \divides m)
 592 [ elim Hcut.
 593   auto
 594   (*elim H2.
 595   split
 596   [ assumption
 597   | elim H1.
 598     assumption
 599   ]*)
 600 | rewrite < H.
 601   apply divides_gcd_nm
 602 ]
 603 qed.
 604
 605 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 606 intros.
 607 auto.
 608 (*apply (nat_case1 (gcd m n))
 609 [ intros.
 610   generalize in match (gcd_O_to_eq_O m n H1).
 611   intros.
 612   elim H2.
 613   rewrite < H4 in \vdash (? ? %).
 614   assumption
 615 | intros.
 616   unfold lt.
 617   apply le_S_S.
 618   apply le_O_n
 619 ]*)
 620 qed.
 621
 622 theorem gcd_n_n: \forall n.gcd n n = n.
 623 intro.
 624 auto.
 625 (*elim n
 626 [ reflexivity
 627 | apply le_to_le_to_eq
 628   [ apply divides_to_le
 629     [ apply lt_O_S
 630     | apply divides_gcd_n
 631     ]
 632   | apply divides_to_le
 633     [ apply lt_O_gcd.apply lt_O_S
 634     | apply divides_d_gcd
 635       [ apply divides_n_n
 636       | apply divides_n_n
 637       ]
 638     ]
 639   ]
 640 ]*)
 641 qed.
 642
 643 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
 644 O < i.
 645 intros.
 646 elim (le_to_or_lt_eq ? ? (le_O_n i))
 647 [ assumption
 648 | absurd ((gcd i n) = (S O))
 649   [ assumption
 650   | rewrite < H2.
 651     simplify.
 652     unfold.
 653     intro.
 654     apply (lt_to_not_eq (S O) n H).
 655     auto
 656     (*apply sym_eq.
 657     assumption*)
 658   ]
 659 ]
 660 qed.
 661
 662 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
 663 i < n.
 664 intros.
 665 elim (le_to_or_lt_eq ? ? H1)
 666   [assumption
 667   |absurd ((gcd i n) = (S O))
 668     [assumption
 669     |rewrite > H3.
 670      rewrite > gcd_n_n.
 671      unfold.intro.
 672      apply (lt_to_not_eq (S O) n H).
 673      apply sym_eq.assumption
 674     ]
 675   ]
 676 qed.
 677
 678 theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
 679 intro.apply (nat_case n)
 680   [intros.reflexivity
 681   |intros.
 682    apply le_to_le_to_eq
 683     [apply divides_to_le
 684       [apply lt_O_S|apply divides_gcd_n]
 685     |apply divides_to_le
 686       [apply lt_O_gcd.rewrite > (times_n_O O).
 687        apply lt_times[apply lt_O_S|assumption]
 688       |apply divides_d_gcd
 689         [apply (witness ? ? m1).reflexivity
 690         |apply divides_n_n
 691         ]
 692       ]
 693     ]
 694   ]
 695 qed.
 696
 697 theorem symmetric_gcd: symmetric nat gcd.
 698 (*CSC: bug here: unfold symmetric does not work *)
 699 change with
 700 (\forall n,m:nat. gcd n m = gcd m n).
 701 intros.
 702 auto.
 703 (*cut (O < (gcd n m) \lor O = (gcd n m))
 704 [ elim Hcut
 705   [ cut (O < (gcd m n) \lor O = (gcd m n))
 706     [ elim Hcut1
 707       [ apply antisym_le
 708         [ apply divides_to_le
 709           [ assumption
 710           | apply divides_d_gcd
 711             [ apply divides_gcd_n
 712             | apply divides_gcd_m
 713             ]
 714           ]
 715         | apply divides_to_le
 716           [ assumption
 717           | apply divides_d_gcd
 718             [ apply divides_gcd_n
 719             | apply divides_gcd_m
 720             ]
 721           ]
 722         ]
 723       | rewrite < H1.
 724         cut (m=O \land n=O)
 725         [ elim Hcut2.
 726           rewrite > H2.
 727           rewrite > H3.
 728           reflexivity
 729         | apply gcd_O_to_eq_O.
 730           apply sym_eq.
 731           assumption
 732         ]
 733       ]
 734     | apply le_to_or_lt_eq.
 735       apply le_O_n
 736     ]
 737   | rewrite < H.
 738     cut (n=O \land m=O)
 739     [ elim Hcut1.
 740       rewrite > H1.
 741       rewrite > H2.
 742       reflexivity
 743     | apply gcd_O_to_eq_O.apply sym_eq.
 744       assumption
 745     ]
 746   ]
 747 | apply le_to_or_lt_eq.
 748   apply le_O_n
 749 ]*)
 750 qed.
 751
 752 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 753 symmetric_gcd.
 754
 755 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 756 intros.
 757 apply (nat_case n)
 758 [ apply le_n
 759 | intro.
 760   apply divides_to_le
 761   [ apply lt_O_gcd.
 762     auto
 763     (*rewrite > (times_n_O O).
 764     apply lt_times
 765     [ auto.unfold lt.
 766       apply le_S_S.
 767       apply le_O_n
 768     | assumption
 769     ]*)
 770   | apply divides_d_gcd;auto
 771     (*[ apply (transitive_divides ? (S m1))
 772       [ apply divides_gcd_m
 773       | apply (witness ? ? p).
 774         reflexivity
 775       ]
 776     | apply divides_gcd_n
 777     ]*)
 778   ]
 779 ]
 780 qed.
 781
 782 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
 783 gcd m (n*p) = (S O) \to gcd m n = (S O).
 784 intros.
 785 apply antisymmetric_le
 786 [ rewrite < H2.
 787   auto
 788   (*apply le_gcd_times.
 789   assumption*)
 790 | auto
 791   (*change with (O < gcd m n).
 792   apply lt_O_gcd.
 793   assumption*)
 794 ]
 795 qed.
 796
 797 (* for the "converse" of the previous result see the end  of this development *)
 798
 799 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
 800 (gcd n m) = (S O) \to \lnot (divides n m).
 801 intros.unfold.intro.
 802 elim H2.
 803 generalize in match H1.
 804 rewrite > H3.
 805 intro.
 806 cut (O < n2)
 807 [ elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
 808   [ cut (gcd n (n*n2) = n);auto
 809     (*[ auto.apply (lt_to_not_eq (S O) n)
 810       [ assumption
 811       | rewrite < H4.
 812         assumption
 813       ]
 814     | apply gcd_n_times_nm.
 815       assumption
 816     ]*)
 817   | auto
 818     (*apply (trans_lt ? (S O))
 819     [ apply le_n
 820     | assumption
 821     ]*)
 822   | assumption
 823   ]
 824 | elim (le_to_or_lt_eq O n2 (le_O_n n2))
 825   [ assumption
 826   | apply False_ind.
 827     apply (le_to_not_lt n (S O))
 828     [ rewrite < H4.
 829       apply divides_to_le;auto
 830       (*[ rewrite > H4.
 831         apply lt_O_S
 832       | apply divides_d_gcd
 833         [ apply (witness ? ? n2).
 834           reflexivity
 835         | apply divides_n_n
 836         ]
 837       ]*)
 838     | assumption
 839     ]
 840   ]
 841 ]
 842 qed.
 843
 844 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 845 intro.
 846 auto.
 847 (*apply antisym_le
 848 [ apply divides_to_le
 849   [ unfold lt.
 850     apply le_n
 851   | apply divides_gcd_n
 852   ]
 853 | cut (O < gcd (S O) n \lor O = gcd (S O) n)
 854   [ elim Hcut
 855     [ assumption
 856     | apply False_ind.
 857       apply (not_eq_O_S O).
 858       cut ((S O)=O \land n=O)
 859       [ elim Hcut1.
 860         apply sym_eq.
 861         assumption
 862       | apply gcd_O_to_eq_O.
 863         apply sym_eq.
 864         assumption
 865       ]
 866     ]
 867   | apply le_to_or_lt_eq.
 868     apply le_O_n
 869   ]
 870 ]*)
 871 qed.
 872
 873 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 874 divides (gcd m n) (gcd n (m \mod n)).
 875 intros.
 876 auto.
 877 (*apply divides_d_gcd
 878 [ apply divides_mod
 879   [ assumption
 880   | apply divides_gcd_n
 881   | apply divides_gcd_m
 882   ]
 883 | apply divides_gcd_m.
 884 ]*)
 885 qed.
 886
 887 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 888 divides (gcd n (m \mod n)) (gcd m n) .
 889 intros.
 890 auto.
 891 (*apply divides_d_gcd
 892 [ apply divides_gcd_n
 893 | apply (divides_mod_to_divides ? ? n)
 894   [ assumption
 895   | apply divides_gcd_m
 896   | apply divides_gcd_n
 897   ]
 898 ]*)
 899 qed.
 900
 901 theorem gcd_mod: \forall m,n:nat. O < n \to
 902 (gcd n (m \mod n)) = (gcd m n) .
 903 intros.
 904 auto.
 905 (*apply antisymmetric_divides
 906 [ apply divides_mod_gcd.
 907   assumption
 908 | apply divides_gcd_mod.
 909   assumption
 910 ]*)
 911 qed.
 912
 913 (* gcd and primes *)
 914
 915 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 916 gcd n m = (S O).
 917 intros.unfold prime in H.
 918 elim H.
 919 apply antisym_le
 920 [ apply not_lt_to_le.unfold Not.unfold lt.
 921   intro.
 922   apply H1.
 923   rewrite < (H3 (gcd n m));auto
 924   (*[ apply divides_gcd_m
 925   | apply divides_gcd_n
 926   | assumption
 927   ]*)
 928 | cut (O < gcd n m \lor O = gcd n m)
 929   [ elim Hcut
 930     [ assumption
 931     | apply False_ind.
 932       apply (not_le_Sn_O (S O)).
 933       cut (n=O \land m=O)
 934       [ elim Hcut1.
 935         rewrite < H5 in \vdash (? ? %).
 936         assumption
 937       | auto
 938         (*apply gcd_O_to_eq_O.
 939         apply sym_eq.
 940         assumption*)
 941       ]
 942     ]
 943   | auto
 944     (*apply le_to_or_lt_eq.
 945     apply le_O_n*)
 946   ]
 947 ]
 948 qed.
 949
 950 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 951 n \divides p \lor n \divides q.
 952 intros.
 953 cut (n \divides p \lor n \ndivides p)
 954 [elim Hcut
 955     [left.assumption
 956     |right.
 957      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
 958        [elim Hcut1.elim H3.elim H4
 959          [(* first case *)
 960           rewrite > (times_n_SO q).rewrite < H5.
 961           rewrite > distr_times_minus.
 962           rewrite > (sym_times q (a1*p)).
 963           rewrite > (assoc_times a1).
 964           elim H1.
 965           (*
 966              rewrite > H6.
 967              applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
 968              reflexivity. *)
 969           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *)
 970           (*
 971           rewrite < (sym_times n).rewrite < assoc_times.
 972           rewrite > (sym_times q).rewrite > assoc_times.
 973           rewrite < (assoc_times a1).rewrite < (sym_times n).
 974           rewrite > (assoc_times n).
 975           rewrite < distr_times_minus.
 976           apply (witness ? ? (q*a-a1*n2)).reflexivity
 977           *)
 978          |(* second case *)
 979           rewrite > (times_n_SO q).rewrite < H5.
 980           rewrite > distr_times_minus.
 981           rewrite > (sym_times q (a1*p)).
 982           rewrite > (assoc_times a1).
 983           elim H1.
 984           auto
 985           (*rewrite > H6.
 986           rewrite < sym_times.rewrite > assoc_times.
 987           rewrite < (assoc_times q).
 988           rewrite < (sym_times n).
 989           rewrite < distr_times_minus.
 990           apply (witness ? ? (n2*a1-q*a)).
 991           reflexivity*)
 992         ](* end second case *)
 993      | rewrite < (prime_to_gcd_SO n p);auto
 994       (* [ apply eq_minus_gcd
 995        | assumption
 996        | assumption
 997        ]*)
 998      ]
 999    ]
1000  | apply (decidable_divides n p).
1001    apply (trans_lt ? (S O))
1002     [ auto
1003       (*unfold lt.
1004       apply le_n*)
1005     | unfold prime in H.
1006       elim H.
1007       assumption
1008     ]
1009   ]
1010 qed.
1011
1012 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
1013 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
1014 intros.
1015 apply antisymmetric_le
1016 [ apply not_lt_to_le.
1017   unfold Not.intro.
1018   cut (divides (smallest_factor (gcd m (n*p))) n \lor
1019        divides (smallest_factor (gcd m (n*p))) p)
1020   [ elim Hcut
1021     [ apply (not_le_Sn_n (S O)).
1022       change with ((S O) < (S O)).
1023       rewrite < H2 in \vdash (? ? %).
1024       apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
1025       [ auto
1026         (*apply lt_SO_smallest_factor.
1027         assumption*)
1028       | apply divides_to_le;auto
1029         (*[ rewrite > H2.
1030           unfold lt.
1031           apply le_n
1032         | apply divides_d_gcd
1033           [ assumption
1034           | apply (transitive_divides ? (gcd m (n*p)))
1035             [ apply divides_smallest_factor_n.
1036               apply (trans_lt ? (S O))
1037               [ unfold lt.
1038                 apply le_n
1039               | assumption
1040               ]
1041             | apply divides_gcd_n
1042             ]
1043           ]
1044         ]*)
1045       ]
1046     | apply (not_le_Sn_n (S O)).
1047       change with ((S O) < (S O)).
1048       rewrite < H3 in \vdash (? ? %).
1049       apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
1050       [ apply lt_SO_smallest_factor.
1051         assumption
1052       | apply divides_to_le;auto
1053         (*[ rewrite > H3.
1054           unfold lt.
1055           apply le_n
1056         | apply divides_d_gcd
1057           [ assumption
1058           | apply (transitive_divides ? (gcd m (n*p)))
1059             [ apply divides_smallest_factor_n.
1060               apply (trans_lt ? (S O))
1061               [  unfold lt.
1062                 apply le_n
1063               | assumption
1064               ]
1065             | apply divides_gcd_n
1066             ]
1067           ]
1068         ]*)
1069       ]
1070     ]
1071   | apply divides_times_to_divides;auto
1072     (*[ apply prime_smallest_factor_n.
1073       assumption
1074     | auto.apply (transitive_divides ? (gcd m (n*p)))
1075       [ apply divides_smallest_factor_n.
1076         apply (trans_lt ? (S O))
1077         [ unfold lt.
1078           apply le_n
1079         | assumption
1080         ]
1081       | apply divides_gcd_m
1082       ]
1083     ]*)
1084   ]
1085 | auto
1086   (*change with (O < gcd m (n*p)).
1087   apply lt_O_gcd.
1088   rewrite > (times_n_O O).
1089   apply lt_times;assumption.*)
1090 ]
1091 qed.
1092
1093 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
1094 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
1095 intros.
1096 cut (n \divides p \lor n \ndivides p)
1097 [ elim Hcut
1098   [ assumption
1099   | cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
1100     [ elim Hcut1.elim H4.elim H5
1101       [(* first case *)
1102         rewrite > (times_n_SO p).rewrite < H6.
1103         rewrite > distr_times_minus.
1104         rewrite > (sym_times p (a1*m)).
1105         rewrite > (assoc_times a1).
1106         elim H2.
1107         applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
1108       |(* second case *)
1109         rewrite > (times_n_SO p).rewrite < H6.
1110         rewrite > distr_times_minus.
1111         rewrite > (sym_times p (a1*m)).
1112         rewrite > (assoc_times a1).
1113         elim H2.
1114         applyS (witness n ? ? (refl_eq ? ?)).
1115       ](* end second case *)
1116     | rewrite < H1.
1117       apply eq_minus_gcd
1118     ]
1119   ]
1120 | auto
1121   (*apply (decidable_divides n p).
1122   assumption.*)
1123 ]
1124 qed.