matita/contribs/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_autobatch/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   autobatch.
  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 autobatch.
  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);autobatch
  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         autobatch
  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           autobatch width = 4.
 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                 autobatch
 114                 (*apply H4.
 115                 apply mod_O_to_divides
 116                 [ assumption
 117                 | apply sym_eq.
 118                   assumption
 119                 ]*)
 120               ]
 121             | autobatch
 122               (*apply le_to_or_lt_eq.
 123               apply le_O_n*)
 124             ]
 125           | autobatch
 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);autobatch
 131             (*[ autobatch.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   | autobatch
 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     autobatch
 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     autobatch
 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     autobatch
 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       autobatch
 220       (*split;assumption*)
 221     | apply divides_gcd_aux_mn
 222       [ autobatch
 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         autobatch
 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)). (*autobatch 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)). (*autobatch 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);autobatch
 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;
 267     simplify; autobatch.
 268     (*[ simplify.
 269       assumption.
 270     | assumption.
 271     | assumption.
 272     ]*)
 273     rewrite > not_divides_to_divides_b_false
 274     [ simplify.
 275       apply H
 276       [ cut (O \lt m \mod n1 \lor O = m \mod n1)
 277         [ elim Hcut1
 278           [ assumption
 279           |
 280             absurd (n1 \divides m);autobatch
 281             (*[ apply mod_O_to_divides
 282               [ assumption.
 283               | apply sym_eq.assumption.
 284               ]
 285             | assumption
 286             ]*)
 287           ]
 288         | autobatch
 289           (*apply le_to_or_lt_eq.
 290           apply le_O_n*)
 291         ]
 292       | autobatch
 293         (*apply lt_to_le.
 294         apply lt_mod_m_m.
 295         assumption*)
 296       | apply le_S_S_to_le.
 297         autobatch
 298         (*apply (trans_le ? n1)
 299         [ change with (m \mod n1 < n1).
 300           apply lt_mod_m_m.
 301           assumption
 302         | assumption
 303         ]*)
 304       | assumption
 305       | autobatch
 306         (*apply divides_mod;
 307         assumption*)
 308       ]
 309     | assumption
 310     | assumption
 311     ]
 312   | autobatch
 313     (*apply (decidable_divides n1 m).
 314     assumption*)
 315   ]
 316 ]qed.
 317
 318 theorem divides_d_gcd: \forall m,n,d.
 319 d \divides m \to d \divides n \to d \divides gcd n m.
 320 intros.
 321 (*CSC: here simplify simplifies too much because of a redex in gcd *)
 322 change with
 323 (d \divides
 324 match leb n m with
 325   [ true \Rightarrow
 326     match n with
 327     [ O \Rightarrow m
 328     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 329   | false \Rightarrow
 330     match m with
 331     [ O \Rightarrow n
 332     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 333 apply (leb_elim n m)
 334 [ apply (nat_case1 n)
 335   [ simplify.
 336     intros.
 337     assumption
 338   | intros.
 339     change with (d \divides gcd_aux (S m1) m (S m1)).
 340     apply divides_gcd_aux
 341     [ unfold lt.autobatch
 342       (*apply le_S_S.
 343       apply le_O_n.*)
 344     | assumption.
 345     | apply le_n. (*chiude il goal anche con autobatch*)
 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     [ unfold lt.autobatch
 359       (*apply le_S_S.
 360       apply le_O_n*)
 361     | autobatch
 362       (*apply lt_to_le.
 363       apply not_le_to_lt.
 364       assumption*)
 365     | apply le_n (*chiude il goal anche con autobatch*)
 366     | assumption
 367     | rewrite < H2.
 368       assumption
 369     ]
 370   ]
 371 ]
 372 qed.
 373
 374 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 375 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 376 intro.
 377 elim p
 378 [ absurd (O < n);autobatch
 379   (*[ assumption
 380   | apply le_to_not_lt
 381     assumption.
 382   ]*)
 383 | cut (O < m)
 384   [ cut (n1 \divides m \lor  n1 \ndivides m)
 385     [ simplify.
 386       elim Hcut1
 387       [ rewrite > divides_to_divides_b_true
 388         [ simplify.
 389           apply (ex_intro ? ? (S O)).
 390           apply (ex_intro ? ? O).
 391           autobatch
 392           (*left.
 393           simplify.
 394           rewrite < plus_n_O.
 395           apply sym_eq.apply minus_n_O*)
 396         | assumption
 397         | assumption
 398         ]
 399       | rewrite > not_divides_to_divides_b_false
 400         [ change with
 401           (\exists a,b.
 402           a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 403           \lor
 404           b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 405           cut
 406           (\exists a,b.
 407           a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 408           \lor
 409           b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
 410           [ elim Hcut2.
 411             elim H5.
 412             elim H6
 413             [ (* first case *)
 414               rewrite < H7.
 415               apply (ex_intro ? ? (a1+a*(m / n1))).
 416               apply (ex_intro ? ? a).
 417               right.
 418               rewrite < sym_plus.
 419               rewrite < (sym_times n1).
 420               rewrite > distr_times_plus.
 421               rewrite > (sym_times n1).
 422               rewrite > (sym_times n1).
 423               rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);autobatch
 424               (*[ rewrite > assoc_times.
 425                 rewrite < sym_plus.
 426                 rewrite > distr_times_plus.
 427                 rewrite < eq_minus_minus_minus_plus.
 428                 rewrite < sym_plus.autobatch.
 429                 rewrite < plus_minus
 430                 [ rewrite < minus_n_n.
 431                   reflexivity
 432                 | apply le_n
 433                 ]
 434               | assumption
 435               ]*)
 436             | (* second case *)
 437               rewrite < H7.
 438               apply (ex_intro ? ? (a1+a*(m / n1))).
 439               apply (ex_intro ? ? a).
 440               left.
 441               (* clear Hcut2.clear H5.clear H6.clear H. *)
 442               rewrite > sym_times.
 443               rewrite > distr_times_plus.
 444               rewrite > sym_times.
 445               rewrite > (sym_times n1).
 446               rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
 447               [ rewrite > distr_times_plus.
 448                 rewrite > assoc_times.
 449                 rewrite < eq_minus_minus_minus_plus.
 450                 autobatch
 451                 (*rewrite < sym_plus.
 452                 rewrite < plus_minus
 453                 [ rewrite < minus_n_n.
 454                   reflexivity
 455                 | apply le_n
 456                 ]*)
 457               | assumption
 458               ]
 459             ]
 460           | apply (H n1 (m \mod n1))
 461             [ cut (O \lt m \mod n1 \lor O = m \mod n1)
 462               [ elim Hcut2
 463                 [ assumption
 464                 | absurd (n1 \divides m);autobatch
 465                   (*[ apply mod_O_to_divides
 466                     [ assumption
 467                     | symmetry.
 468                       assumption
 469                     ]
 470                   | assumption
 471                   ]*)
 472                 ]
 473               | autobatch
 474                 (*apply le_to_or_lt_eq.
 475                 apply le_O_n*)
 476               ]
 477             | autobatch
 478               (*apply lt_to_le.
 479               apply lt_mod_m_m.
 480               assumption*)
 481             | apply le_S_S_to_le.
 482               autobatch
 483               (*apply (trans_le ? n1)
 484               [ change with (m \mod n1 < n1).
 485                 apply lt_mod_m_m.
 486                 assumption
 487               | assumption
 488               ]*)
 489             ]
 490           ]
 491         | assumption
 492         | assumption
 493         ]
 494       ]
 495     | autobatch
 496       (*apply (decidable_divides n1 m).
 497       assumption*)
 498     ]
 499   | autobatch
 500     (*apply (lt_to_le_to_lt ? n1);assumption *)
 501   ]
 502 ]
 503 qed.
 504
 505 theorem eq_minus_gcd:
 506  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 507 intros.
 508 unfold gcd.
 509 apply (leb_elim n m)
 510 [ apply (nat_case1 n)
 511   [ simplify.
 512     intros.
 513     apply (ex_intro ? ? O).
 514     apply (ex_intro ? ? (S O)).
 515     autobatch
 516     (*right.simplify.
 517     rewrite < plus_n_O.
 518     apply sym_eq.
 519     apply minus_n_O*)
 520   | intros.
 521     change with
 522     (\exists a,b.
 523     a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 524     \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 525     autobatch
 526     (*apply eq_minus_gcd_aux
 527     [ unfold lt.
 528       apply le_S_S.
 529       apply le_O_n
 530     | assumption
 531     | apply le_n
 532     ]*)
 533   ]
 534 | apply (nat_case1 m)
 535   [ simplify.
 536     intros.
 537     apply (ex_intro ? ? (S O)).
 538     apply (ex_intro ? ? O).
 539     autobatch
 540     (*left.simplify.
 541     rewrite < plus_n_O.
 542     apply sym_eq.
 543     apply minus_n_O*)
 544   | intros.
 545     change with
 546     (\exists a,b.
 547     a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 548     \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 549     cut
 550     (\exists a,b.
 551     a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 552     \lor
 553     b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))
 554     [ elim Hcut.
 555       elim H2.
 556       elim H3;apply (ex_intro ? ? a1);autobatch
 557       (*[ apply (ex_intro ? ? a1).
 558         apply (ex_intro ? ? a).
 559         right.
 560         assumption
 561       | apply (ex_intro ? ? a1).
 562         apply (ex_intro ? ? a).
 563         left.
 564         assumption
 565       ]*)
 566     | apply eq_minus_gcd_aux;autobatch
 567       (*[ unfold lt.
 568         apply le_S_S.
 569         apply le_O_n
 570       | autobatch.apply lt_to_le.
 571         apply not_le_to_lt.
 572         assumption
 573       | apply le_n.
 574       ]*)
 575     ]
 576   ]
 577 ]
 578 qed.
 579
 580 (* some properties of gcd *)
 581
 582 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 583 autobatch.
 584 (*intro.simplify.reflexivity.*)
 585 qed.
 586
 587 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 588 m = O \land n = O.
 589 intros.
 590 cut (O \divides n \land O \divides m)
 591 [ elim Hcut.
 592   autobatch size = 7;
 593   (*
 594   split;
 595     [ apply antisymmetric_divides
 596       [ apply divides_n_O
 597       | assumption
 598       ]
 599     | apply antisymmetric_divides
 600       [ apply divides_n_O
 601       | assumption
 602       ]
 603     ]*)
 604 | rewrite < H.
 605   apply divides_gcd_nm
 606 ]
 607 qed.
 608
 609 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 610 intros.
 611 autobatch.
 612 (*
 613 apply (divides_to_lt_O (gcd m n) n ? ?);
 614   [apply (H).
 615   |apply (divides_gcd_m m n).
 616   ]
 617 *)
 618 qed.
 619
 620 theorem gcd_n_n: \forall n.gcd n n = n.
 621 intro.
 622 autobatch.
 623 (*
 624 apply (antisymmetric_divides (gcd n n) n ? ?);
 625   [apply (divides_gcd_n n n).
 626   |apply (divides_d_gcd n n n ? ?);
 627     [apply (reflexive_divides n).
 628     |apply (reflexive_divides n).
 629     ]
 630   ]
 631 *)
 632 qed.
 633
 634 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
 635 O < i.
 636 intros.
 637 elim (le_to_or_lt_eq ? ? (le_O_n i))
 638 [ assumption
 639 | absurd ((gcd i n) = (S O))
 640   [ assumption
 641   | rewrite < H2.
 642     simplify.
 643     unfold.
 644     intro.
 645     apply (lt_to_not_eq (S O) n H).
 646     autobatch
 647     (*apply sym_eq.
 648     assumption*)
 649   ]
 650 ]
 651 qed.
 652
 653 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
 654 i < n.
 655 intros.
 656 elim (le_to_or_lt_eq ? ? H1)
 657   [assumption
 658   |absurd ((gcd i n) = (S O))
 659     [assumption
 660     |rewrite > H3.
 661      rewrite > gcd_n_n.
 662      unfold.intro.
 663      apply (lt_to_not_eq (S O) n H).
 664      apply sym_eq.assumption
 665     ]
 666   ]
 667 qed.
 668
 669 theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
 670 intro.apply (nat_case n)
 671   [intros.reflexivity
 672   |intros.
 673    apply le_to_le_to_eq
 674     [apply divides_to_le
 675       [apply lt_O_S|apply divides_gcd_n]
 676     |apply divides_to_le
 677       [apply lt_O_gcd.rewrite > (times_n_O O).
 678        apply lt_times[apply lt_O_S|assumption]
 679       |apply divides_d_gcd
 680         [apply (witness ? ? m1).reflexivity
 681         |apply divides_n_n
 682         ]
 683       ]
 684     ]
 685   ]
 686 qed.
 687
 688 theorem symmetric_gcd: symmetric nat gcd.
 689 (*CSC: bug here: unfold symmetric does not work *)
 690 change with
 691 (\forall n,m:nat. gcd n m = gcd m n).
 692 intros.
 693 autobatch size = 7.
 694 (*
 695 apply (antisymmetric_divides (gcd n m) (gcd m n) ? ?);
 696   [apply (divides_d_gcd n m (gcd n m) ? ?);
 697     [apply (divides_gcd_n n m).
 698     |apply (divides_gcd_m n m).
 699     ]
 700   |apply (divides_d_gcd m n (gcd m n) ? ?);
 701     [apply (divides_gcd_n m n).
 702     |apply (divides_gcd_m m n).
 703     ]
 704   ]
 705 *)
 706 qed.
 707
 708 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 709 symmetric_gcd.
 710
 711 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 712 intros.
 713 apply (nat_case n)
 714 [ apply le_n
 715 | intro.
 716   apply divides_to_le
 717   [ apply lt_O_gcd.
 718     autobatch
 719     (*rewrite > (times_n_O O).
 720     apply lt_times
 721     [ autobatch.unfold lt.
 722       apply le_S_S.
 723       apply le_O_n
 724     | assumption
 725     ]*)
 726   | apply divides_d_gcd;autobatch
 727     (*[ apply (transitive_divides ? (S m1))
 728       [ apply divides_gcd_m
 729       | apply (witness ? ? p).
 730         reflexivity
 731       ]
 732     | apply divides_gcd_n
 733     ]*)
 734   ]
 735 ]
 736 qed.
 737
 738 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
 739 gcd m (n*p) = (S O) \to gcd m n = (S O).
 740 intros.
 741 apply antisymmetric_le
 742 [ rewrite < H2.
 743   autobatch
 744   (*apply le_gcd_times.
 745   assumption*)
 746 | autobatch
 747   (*change with (O < gcd m n).
 748   apply lt_O_gcd.
 749   assumption*)
 750 ]
 751 qed.
 752
 753 (* for the "converse" of the previous result see the end  of this development *)
 754
 755 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
 756 (gcd n m) = (S O) \to \lnot (divides n m).
 757 intros.unfold.intro.
 758 elim H2.
 759 generalize in match H1.
 760 rewrite > H3.
 761 intro.
 762 cut (O < n2)
 763 [ elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
 764   [ cut (gcd n (n*n2) = n);autobatch
 765     (*[ autobatch.apply (lt_to_not_eq (S O) n)
 766       [ assumption
 767       | rewrite < H4.
 768         assumption
 769       ]
 770     | apply gcd_n_times_nm.
 771       assumption
 772     ]*)
 773   | autobatch
 774     (*apply (trans_lt ? (S O))
 775     [ apply le_n
 776     | assumption
 777     ]*)
 778   | assumption
 779   ]
 780 | elim (le_to_or_lt_eq O n2 (le_O_n n2))
 781   [ assumption
 782   | apply False_ind.
 783     apply (le_to_not_lt n (S O))
 784     [ rewrite < H4.
 785       apply divides_to_le;autobatch
 786       (*[ rewrite > H4.
 787         apply lt_O_S
 788       | apply divides_d_gcd
 789         [ apply (witness ? ? n2).
 790           reflexivity
 791         | apply divides_n_n
 792         ]
 793       ]*)
 794     | assumption
 795     ]
 796   ]
 797 ]
 798 qed.
 799
 800 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 801 intro.
 802 autobatch.
 803 (*
 804 apply (symmetric_eq nat (S O) (gcd (S O) n) ?).
 805 apply (antisymmetric_divides (S O) (gcd (S O) n) ? ?);
 806   [apply (divides_SO_n (gcd (S O) n)).
 807   |apply (divides_gcd_n (S O) n).
 808   ]
 809 *)
 810 qed.
 811
 812 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 813 divides (gcd m n) (gcd n (m \mod n)).
 814 intros.
 815 autobatch width = 4.
 816 (*apply divides_d_gcd
 817 [ apply divides_mod
 818   [ assumption
 819   | apply divides_gcd_n
 820   | apply divides_gcd_m
 821   ]
 822 | apply divides_gcd_m.
 823 ]*)
 824 qed.
 825
 826 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 827 divides (gcd n (m \mod n)) (gcd m n) .
 828 intros.
 829 autobatch.
 830 (*apply divides_d_gcd
 831 [ apply divides_gcd_n
 832 | apply (divides_mod_to_divides ? ? n)
 833   [ assumption
 834   | apply divides_gcd_m
 835   | apply divides_gcd_n
 836   ]
 837 ]*)
 838 qed.
 839
 840 theorem gcd_mod: \forall m,n:nat. O < n \to
 841 (gcd n (m \mod n)) = (gcd m n) .
 842 intros.
 843 autobatch.
 844 (*apply antisymmetric_divides
 845 [ apply divides_mod_gcd.
 846   assumption
 847 | apply divides_gcd_mod.
 848   assumption
 849 ]*)
 850 qed.
 851
 852 (* gcd and primes *)
 853
 854 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 855 gcd n m = (S O).
 856 intros.unfold prime in H.
 857 elim H.
 858 apply antisym_le
 859 [ apply not_lt_to_le.unfold Not.unfold lt.
 860   intro.
 861   apply H1.
 862   rewrite < (H3 (gcd n m));
 863   [autobatch|autobatch| unfold lt; autobatch]
 864   (*[ apply divides_gcd_m
 865   | apply divides_gcd_n
 866   | assumption
 867   ]*)
 868 | cut (O < gcd n m \lor O = gcd n m)
 869   [ elim Hcut
 870     [ assumption
 871     | apply False_ind.
 872       apply (not_le_Sn_O (S O)).
 873       cut (n=O \land m=O)
 874       [ elim Hcut1.
 875         rewrite < H5 in \vdash (? ? %).
 876         assumption
 877       | autobatch
 878         (*apply gcd_O_to_eq_O.
 879         apply sym_eq.
 880         assumption*)
 881       ]
 882     ]
 883   | autobatch
 884     (*apply le_to_or_lt_eq.
 885     apply le_O_n*)
 886   ]
 887 ]
 888 qed.
 889
 890 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 891 n \divides p \lor n \divides q.
 892 intros.
 893 cut (n \divides p \lor n \ndivides p)
 894 [elim Hcut
 895     [left.assumption
 896     |right.
 897      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
 898        [elim Hcut1.elim H3.elim H4
 899          [(* first case *)
 900           rewrite > (times_n_SO q).rewrite < H5.
 901           rewrite > distr_times_minus.
 902           rewrite > (sym_times q (a1*p)).
 903           rewrite > (assoc_times a1).
 904           elim H1.
 905           (*
 906              rewrite > H6.
 907              applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
 908              reflexivity. *)
 909           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *)
 910           (*
 911           rewrite < (sym_times n).rewrite < assoc_times.
 912           rewrite > (sym_times q).rewrite > assoc_times.
 913           rewrite < (assoc_times a1).rewrite < (sym_times n).
 914           rewrite > (assoc_times n).
 915           rewrite < distr_times_minus.
 916           apply (witness ? ? (q*a-a1*n2)).reflexivity
 917           *)
 918          |(* second case *)
 919           rewrite > (times_n_SO q).rewrite < H5.
 920           rewrite > distr_times_minus.
 921           rewrite > (sym_times q (a1*p)).
 922           rewrite > (assoc_times a1).
 923           elim H1.
 924           autobatch
 925           (*rewrite > H6.
 926           rewrite < sym_times.rewrite > assoc_times.
 927           rewrite < (assoc_times q).
 928           rewrite < (sym_times n).
 929           rewrite < distr_times_minus.
 930           apply (witness ? ? (n2*a1-q*a)).
 931           reflexivity*)
 932         ](* end second case *)
 933      | rewrite < (prime_to_gcd_SO n p);autobatch
 934       (* [ apply eq_minus_gcd
 935        | assumption
 936        | assumption
 937        ]*)
 938      ]
 939    ]
 940  | apply (decidable_divides n p).
 941    apply (trans_lt ? (S O))
 942     [ autobatch
 943       (*unfold lt.
 944       apply le_n*)
 945     | unfold prime in H.
 946       elim H.
 947       assumption
 948     ]
 949   ]
 950 qed.
 951
 952 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 953 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 954 intros.
 955 apply antisymmetric_le
 956 [ apply not_lt_to_le.
 957   unfold Not.intro.
 958   cut (divides (smallest_factor (gcd m (n*p))) n \lor
 959        divides (smallest_factor (gcd m (n*p))) p)
 960   [ elim Hcut
 961     [ apply (not_le_Sn_n (S O)).
 962       change with ((S O) < (S O)).
 963       rewrite < H2 in \vdash (? ? %).
 964       apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
 965       [ autobatch
 966         (*apply lt_SO_smallest_factor.
 967         assumption*)
 968       | apply divides_to_le;
 969         [ autobatch |
 970         apply divides_d_gcd
 971          [ assumption
 972          | apply (transitive_divides ? (gcd m (n*p)))
 973            [ autobatch.
 974            | autobatch.
 975            ]
 976          ]
 977         ]
 978         (*[ rewrite > H2.
 979           unfold lt.
 980           apply le_n
 981         | apply divides_d_gcd
 982           [ assumption
 983           | apply (transitive_divides ? (gcd m (n*p)))
 984             [ apply divides_smallest_factor_n.
 985               apply (trans_lt ? (S O))
 986               [ unfold lt.
 987                 apply le_n
 988               | assumption
 989               ]
 990             | apply divides_gcd_n
 991             ]
 992           ]
 993         ]*)
 994       ]
 995     | apply (not_le_Sn_n (S O)).
 996       change with ((S O) < (S O)).
 997       rewrite < H3 in \vdash (? ? %).
 998       apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
 999       [ apply lt_SO_smallest_factor.
1000         assumption
1001       | apply divides_to_le;
1002         [ autobatch |
1003         apply divides_d_gcd
1004          [ assumption
1005          | apply (transitive_divides ? (gcd m (n*p)))
1006            [ autobatch.
1007            | autobatch.
1008            ]
1009          ]
1010         ]
1011         (*[ rewrite > H3.
1012           unfold lt.
1013           apply le_n
1014         | apply divides_d_gcd
1015           [ assumption
1016           | apply (transitive_divides ? (gcd m (n*p)))
1017             [ apply divides_smallest_factor_n.
1018               apply (trans_lt ? (S O))
1019               [  unfold lt.
1020                 apply le_n
1021               | assumption
1022               ]
1023             | apply divides_gcd_n
1024             ]
1025           ]
1026         ]*)
1027       ]
1028     ]
1029   | apply divides_times_to_divides;
1030     [ autobatch |
1031       apply (transitive_divides ? (gcd m (n*p)))
1032            [ autobatch.
1033            | autobatch.
1034            ]
1035          ]
1036         ]
1037     (*[ apply prime_smallest_factor_n.
1038       assumption
1039     | autobatch.apply (transitive_divides ? (gcd m (n*p)))
1040       [ apply divides_smallest_factor_n.
1041         apply (trans_lt ? (S O))
1042         [ unfold lt.
1043           apply le_n
1044         | assumption
1045         ]
1046       | apply divides_gcd_m
1047       ]
1048     ]*)
1049 | autobatch
1050   (*change with (O < gcd m (n*p)).
1051   apply lt_O_gcd.
1052   rewrite > (times_n_O O).
1053   apply lt_times;assumption.*)
1054 ]
1055 qed.
1056
1057 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
1058 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
1059 intros.
1060 cut (n \divides p \lor n \ndivides p)
1061 [ elim Hcut
1062   [ assumption
1063   | cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
1064     [ elim Hcut1.elim H4.elim H5
1065       [(* first case *)
1066         rewrite > (times_n_SO p).rewrite < H6.
1067         rewrite > distr_times_minus.
1068         rewrite > (sym_times p (a1*m)).
1069         rewrite > (assoc_times a1).
1070         elim H2.
1071         applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
1072       |(* second case *)
1073         rewrite > (times_n_SO p).rewrite < H6.
1074         rewrite > distr_times_minus.
1075         rewrite > (sym_times p (a1*m)).
1076         rewrite > (assoc_times a1).
1077         elim H2.
1078         applyS (witness n ? ? (refl_eq ? ?)).
1079       ](* end second case *)
1080     | rewrite < H1.
1081       apply eq_minus_gcd
1082     ]
1083   ]
1084 | autobatch
1085   (*apply (decidable_divides n p).
1086   assumption.*)
1087 ]
1088 qed.