matita/library/nat/gcd_properties1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/gcd_properties1".
  16
  17 include "nat/propr_div_mod_lt_le_totient1_aux.ma".
  18
  19 (* this file contains some important properites of gcd in N *)
  20
  21 (*it's a generalization of the existing theorem divides_gcd_aux (in which
  22   c = 1), proved in file gcd.ma
  23  *)
  24 theorem divides_times_gcd_aux: \forall p,m,n,d,c.
  25 O \lt c \to O < n \to n \le m \to n \le p \to
  26 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
  27 intro.
  28 elim p
  29 [ absurd (O < n)
  30   [ assumption
  31   | apply le_to_not_lt.
  32     assumption
  33   ]
  34 | simplify.
  35   cut (n1 \divides m \lor n1 \ndivides m)
  36   [ elim Hcut
  37     [ rewrite > divides_to_divides_b_true
  38       [ simplify.
  39         assumption
  40       | assumption
  41       | assumption
  42       ]
  43     | rewrite > not_divides_to_divides_b_false
  44       [ simplify.
  45         apply H
  46         [ assumption
  47         | cut (O \lt m \mod n1 \lor O = m \mod n1)
  48           [ elim Hcut1
  49             [ assumption
  50             | absurd (n1 \divides m)
  51               [ apply mod_O_to_divides
  52                 [ assumption
  53                 | apply sym_eq.
  54                   assumption
  55                 ]
  56               | assumption
  57               ]
  58             ]
  59           | apply le_to_or_lt_eq.
  60             apply le_O_n
  61           ]
  62         | apply lt_to_le.
  63           apply lt_mod_m_m.
  64           assumption
  65         | apply le_S_S_to_le.
  66           apply (trans_le ? n1)
  67           [ change with (m \mod n1 < n1).
  68             apply lt_mod_m_m.
  69             assumption
  70           | assumption
  71           ]
  72         | assumption
  73         | rewrite < times_mod
  74           [ rewrite < (sym_times c m).
  75             rewrite < (sym_times c n1).
  76             apply divides_mod
  77             [ rewrite > (S_pred c)
  78               [ rewrite > (S_pred n1)
  79                 [ apply (lt_O_times_S_S)
  80                 | assumption
  81                 ]
  82               | assumption
  83               ]
  84             | assumption
  85             | assumption
  86             ]
  87           | assumption
  88           | assumption
  89           ]
  90         ]
  91       | assumption
  92       | assumption
  93       ]
  94     ]
  95   | apply (decidable_divides n1 m).
  96     assumption
  97   ]
  98 ]
  99 qed.
 100
 101 (*it's a generalization of the existing theorem divides_gcd_d (in which
 102   c = 1), proved in file gcd.ma
 103  *)
 104 theorem divides_d_times_gcd: \forall m,n,d,c.
 105 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
 106 intros.
 107 change with
 108 (d \divides c *
 109 match leb n m with
 110   [ true \Rightarrow
 111     match n with
 112     [ O \Rightarrow m
 113     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 114   | false \Rightarrow
 115     match m with
 116     [ O \Rightarrow n
 117     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 118 apply (leb_elim n m)
 119 [ apply (nat_case1 n)
 120   [ simplify.
 121     intros.
 122     assumption
 123   | intros.
 124     change with (d \divides c*gcd_aux (S m1) m (S m1)).
 125     apply divides_times_gcd_aux
 126     [ assumption
 127     | unfold lt.
 128       apply le_S_S.
 129       apply le_O_n
 130     | assumption
 131     | apply (le_n (S m1))
 132     | assumption
 133     | rewrite < H3.
 134       assumption
 135     ]
 136   ]
 137 | apply (nat_case1 m)
 138   [ simplify.
 139     intros.
 140     assumption
 141   | intros.
 142     change with (d \divides c * gcd_aux (S m1) n (S m1)).
 143     apply divides_times_gcd_aux
 144     [ unfold lt.
 145       change with (O \lt c).
 146       assumption
 147     | apply lt_O_S
 148     | apply lt_to_le.
 149       apply not_le_to_lt.
 150       assumption
 151     | apply (le_n (S m1)).
 152     | assumption
 153     | rewrite < H3.
 154       assumption
 155     ]
 156   ]
 157 ]
 158 qed.
 159
 160 (* 2 basic properties of divides predicate *)
 161 theorem aDIVb_to_bDIVa_to_aEQb:
 162 \forall a,b:nat.
 163 a \divides b \to b \divides a \to a = b.
 164 intros.
 165 apply antisymmetric_divides;
 166   assumption.
 167 qed.
 168
 169
 170 theorem O_div_c_to_c_eq_O: \forall c:nat.
 171 O \divides c \to c = O.
 172 intros.
 173 apply aDIVb_to_bDIVa_to_aEQb
 174 [ apply divides_n_O
 175 | assumption
 176 ]
 177 qed.
 178
 179 (* an alternative characterization for gcd *)
 180 theorem gcd1: \forall a,b,c:nat.
 181 c \divides a \to c \divides b \to
 182 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
 183 intros.
 184 elim (H2 ((gcd a b)))
 185 [ apply (aDIVb_to_bDIVa_to_aEQb (gcd a b) c)
 186   [ apply (witness (gcd a b) c n2).
 187     assumption
 188   | apply divides_d_gcd;
 189       assumption
 190   ]
 191 | apply divides_gcd_n
 192 | rewrite > sym_gcd.
 193   apply divides_gcd_n
 194 ]
 195 qed.
 196
 197
 198 theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat.
 199 (gcd (c*a) (c*b)) = c*(gcd a b).
 200 intros.
 201 apply (nat_case1 c)
 202 [ intros.
 203   simplify.
 204   reflexivity
 205 | intros.
 206   rewrite < H.
 207   apply gcd1
 208   [ apply divides_times
 209     [ apply divides_n_n
 210     | apply divides_gcd_n.
 211     ]
 212   | apply divides_times
 213     [ apply divides_n_n
 214     | rewrite > sym_gcd.
 215       apply divides_gcd_n
 216     ]
 217   | intros.
 218     apply (divides_d_times_gcd)
 219     [ rewrite > H.
 220       apply lt_O_S
 221     | assumption
 222     | assumption
 223     ]
 224   ]
 225 ]
 226 qed.
 227
 228   (*
 229   apply (nat_case1 a)
 230   [ intros.
 231     rewrite > (sym_times c O).
 232     simplify.
 233     reflexivity
 234   | intros.
 235     rewrite < H1.
 236     apply (nat_case1 b)
 237     [ intros.
 238       rewrite > (sym_times ? O).
 239       rewrite > (sym_gcd a O).
 240       rewrite > sym_gcd.
 241       simplify.
 242       reflexivity
 243     | intros.
 244       rewrite < H2.
 245       apply gcd1
 246       [ apply divides_times
 247         [ apply divides_n_n
 248         | apply divides_gcd_n.
 249         ]
 250       | apply divides_times
 251         [ apply divides_n_n
 252         | rewrite > sym_gcd.
 253           apply divides_gcd_n
 254         ]
 255       | intros.
 256         apply (divides_d_times_gcd)
 257         [ rewrite > H.
 258           apply lt_O_S
 259         | assumption
 260         | assumption
 261         ]
 262       ]
 263     ]
 264   ]
 265 ]
 266 qed.*)
 267
 268
 269 theorem associative_nat_gcd: associative nat gcd.
 270 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
 271 intros.
 272 apply gcd1
 273 [ apply divides_d_gcd
 274   [ apply (trans_divides ? (gcd b c) ?)
 275     [ apply divides_gcd_m
 276     | apply divides_gcd_n
 277     ]
 278   | apply divides_gcd_n
 279   ]
 280 | apply (trans_divides ? (gcd b c) ?)
 281   [ apply divides_gcd_m
 282   | apply divides_gcd_m
 283   ]
 284 | intros.
 285   cut (d \divides a \land d \divides b)
 286   [ elim Hcut.
 287     cut (d \divides (gcd b c))
 288     [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
 289     | apply (divides_d_gcd c b d H1 H3)
 290     ]
 291   | split
 292     [ apply (trans_divides d (gcd a b) a H).
 293       apply divides_gcd_n
 294     | apply (trans_divides d (gcd a b) b H).
 295       apply divides_gcd_m
 296     ]
 297   ]
 298 ]
 299 qed.
 300
 301 theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
 302 a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
 303 intros.
 304 apply (nat_case1 a)
 305 [ intros.
 306   apply (nat_case1 b)
 307   [ intros.
 308     cut (d = O)
 309     [ rewrite > Hcut.
 310       simplify.
 311       apply divides_SO_n
 312     | rewrite > H2 in H1.
 313       rewrite > H3 in H1.
 314       apply sym_eq.
 315       assumption
 316     ]
 317   | intros.
 318     cut (O \lt d)
 319     [ rewrite > (S_pred d Hcut).
 320       simplify.
 321       rewrite > H2 in H.
 322       cut (c = O)
 323       [ rewrite > Hcut1.
 324         apply (divides_n_n O)
 325       | apply (lt_times_eq_O b c)
 326         [ rewrite > H3.
 327           apply lt_O_S
 328         | apply (O_div_c_to_c_eq_O (b*c) H)
 329         ]
 330       ]
 331     | rewrite < H1.
 332       apply lt_O_gcd.
 333       rewrite > H3.
 334       apply lt_O_S
 335     ]
 336   ]
 337 | intros.
 338   rewrite < H2.
 339   elim H.
 340   cut (d \divides a \land d \divides b)
 341   [ cut (O \lt a)
 342     [ cut (O \lt d)
 343       [ elim Hcut.
 344         rewrite < (NdivM_times_M_to_N a d) in H3
 345         [ rewrite < (NdivM_times_M_to_N b d) in H3
 346           [ cut (b/d*c = a/d*n2)
 347             [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
 348               [ apply (O_lt_times_to_O_lt (a/d) d).
 349                 rewrite > (NdivM_times_M_to_N a d);
 350                   assumption
 351               | apply (inj_times_r1 d ? ?)
 352                 [ assumption
 353                 | rewrite < (eq_gcd_times_times_eqv_times_gcd (a/d) (b/d) d).
 354                   rewrite < (times_n_SO d).
 355                   rewrite < (sym_times (a/d) d).
 356                   rewrite < (sym_times (b/d) d).
 357                   rewrite > (NdivM_times_M_to_N a d)
 358                   [ rewrite > (NdivM_times_M_to_N b d);
 359                       assumption
 360                   | assumption
 361                   | assumption
 362                   ]
 363                 ]
 364               | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
 365               ]
 366             | apply (inj_times_r1 d ? ?)
 367               [ assumption
 368               | rewrite > sym_times.
 369                 rewrite > (sym_times d ((a/d) * n2)).
 370                 rewrite > assoc_times.
 371                 rewrite > (assoc_times (a/d) n2 d).
 372                 rewrite > (sym_times c d).
 373                 rewrite > (sym_times n2 d).
 374                 rewrite < assoc_times.
 375                 rewrite < (assoc_times (a/d) d n2).
 376                 assumption
 377               ]
 378             ]
 379           | assumption
 380           | assumption
 381           ]
 382         | assumption
 383         | assumption
 384         ]
 385       | rewrite < H1.
 386         rewrite > sym_gcd.
 387         apply lt_O_gcd.
 388         assumption
 389       ]
 390     | rewrite > H2.
 391       apply lt_O_S
 392     ]
 393   | rewrite < H1.
 394     split
 395     [ apply divides_gcd_n
 396     | apply divides_gcd_m
 397     ]
 398   ]
 399 ]
 400 qed.
 401
 402 theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat.
 403 (gcd (a+m*b) b) = d \to (gcd a b) = d.
 404 intros.
 405 apply gcd1
 406 [ rewrite > (minus_plus_m_m a (m*b)).
 407   apply divides_minus
 408   [ rewrite < H.
 409     apply divides_gcd_n
 410   | rewrite > (times_n_SO d).
 411     rewrite > (sym_times d ?).
 412     apply divides_times
 413     [ apply divides_SO_n
 414     | rewrite < H.
 415       apply divides_gcd_m
 416     ]
 417   ]
 418 | rewrite < H.
 419   apply divides_gcd_m
 420 | intros.
 421   rewrite < H.
 422   apply divides_d_gcd
 423   [ assumption
 424   | apply divides_plus
 425     [ assumption
 426     | rewrite > (times_n_SO d1).
 427       rewrite > (sym_times d1 ?).
 428       apply divides_times
 429       [ apply divides_SO_n
 430       | assumption
 431       ]
 432     ]
 433   ]
 434 ]
 435 qed.
 436
 437 theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat.
 438 (gcd (a+m*b) b) = (gcd a b).
 439 intros.
 440 apply sym_eq.
 441 apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
 442 reflexivity.
 443 qed.
 444
 445 theorem gcd_div_div_eq_div_gcd: \forall a,b,m:nat.
 446 O \lt m \to m \divides a \to m \divides b \to
 447 (gcd (a/m) (b/m)) = (gcd a b) / m.
 448 intros.
 449 apply (inj_times_r1 m H).
 450 rewrite > (sym_times m ((gcd a b)/m)).
 451 rewrite > (NdivM_times_M_to_N (gcd a b) m)
 452 [ rewrite < eq_gcd_times_times_eqv_times_gcd.
 453   rewrite > (sym_times m (a/m)).
 454   rewrite > (sym_times m (b/m)).
 455   rewrite > (NdivM_times_M_to_N a m H H1).
 456   rewrite > (NdivM_times_M_to_N b m H H2).
 457   reflexivity
 458 | assumption
 459 | apply divides_d_gcd;
 460     assumption
 461 ]
 462 qed.
 463
 464
 465 theorem gcdSO_divides_divides_times_divides: \forall c,e,f:nat.
 466 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to
 467 (e*f) \divides c.
 468 intros.
 469 apply (nat_case1 e)
 470 [ intros.
 471   apply (nat_case1 c)
 472   [ intros.
 473     simplify.
 474     apply (divides_n_n O).
 475   | intros.
 476     rewrite > H3 in H1.
 477     apply False_ind.
 478     cut (O \lt O)
 479     [ apply (le_to_not_lt O O)
 480       [ apply (le_n O)
 481       | assumption
 482       ]
 483     | apply (divides_to_lt_O O c)
 484       [ rewrite > H4.
 485         apply lt_O_S
 486       | assumption
 487       ]
 488     ]
 489   ]
 490 | intros.
 491   rewrite < H3.
 492   elim H1.
 493   elim H2.
 494   rewrite > H5.
 495   rewrite > (sym_times e f).
 496   apply (divides_times)
 497   [ apply (divides_n_n)
 498   | rewrite > H5 in H1.
 499     apply (gcd_SO_to_divides_times_to_divides f e n)
 500     [ rewrite > H3.
 501       apply (lt_O_S m)
 502     | assumption
 503     | assumption
 504     ]
 505   ]
 506 ]
 507 qed.
 508
 509
 510 (* the following theorem shows that gcd is a multiplicative function in
 511    the following sense: if a1 and a2 are relatively prime, then
 512    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
 513  *)
 514 theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
 515 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
 516 intros.
 517 apply gcd1
 518 [ apply divides_times;
 519     apply divides_gcd_n
 520 | apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
 521   [ apply gcd1
 522     [ apply divides_SO_n
 523     | apply divides_SO_n
 524     | intros.
 525       cut (d \divides a)
 526       [ cut (d \divides b)
 527         [ rewrite < H.
 528           apply (divides_d_gcd b a d Hcut1 Hcut)
 529         | apply (trans_divides d (gcd b c) b)
 530           [ assumption
 531           | apply (divides_gcd_n)
 532           ]
 533         ]
 534       | apply (trans_divides d (gcd a c) a)
 535         [ assumption
 536         | apply (divides_gcd_n)
 537         ]
 538       ]
 539     ]
 540   | apply (divides_gcd_m)
 541   | apply (divides_gcd_m)
 542   ]
 543 | intros.
 544   rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
 545   rewrite > (sym_times (gcd a c) b).
 546   rewrite > (sym_times (gcd a c) c).
 547   rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
 548   rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
 549   apply (divides_d_gcd)
 550   [ apply (divides_d_gcd)
 551     [ rewrite > (times_n_SO d).
 552       apply (divides_times)
 553       [ assumption
 554       | apply divides_SO_n
 555       ]
 556     | rewrite > (times_n_SO d).
 557       apply (divides_times)
 558       [ assumption
 559       | apply divides_SO_n
 560       ]
 561     ]
 562   | apply (divides_d_gcd)
 563     [ rewrite > (times_n_SO d).
 564       rewrite > (sym_times d (S O)).
 565       apply (divides_times)
 566       [ apply (divides_SO_n)
 567       | assumption
 568       ]
 569     | rewrite < (sym_times a b).
 570       assumption
 571     ]
 572   ]
 573 ]
 574 qed.
 575
 576
 577 theorem gcd_eq_gcd_minus: \forall a,b:nat.
 578 a \lt b \to (gcd a b) = (gcd (b - a) b).
 579 intros.
 580 apply sym_eq.
 581 apply gcd1
 582 [ apply (divides_minus (gcd a b) b a)
 583   [ apply divides_gcd_m
 584   | apply divides_gcd_n
 585   ]
 586 | apply divides_gcd_m
 587 | intros.
 588   elim H1.
 589   elim H2.
 590   cut(b = (d*n2) + a)
 591   [ cut (b - (d*n2) = a)
 592     [ rewrite > H4 in Hcut1.
 593       rewrite < (distr_times_minus d n n2) in Hcut1.
 594       apply divides_d_gcd
 595       [ assumption
 596       | apply (witness d a (n - n2)).
 597         apply sym_eq.
 598         assumption
 599       ]
 600     | apply (plus_to_minus ? ? ? Hcut)
 601     ]
 602   | rewrite > sym_plus.
 603     apply (minus_to_plus)
 604     [ apply lt_to_le.
 605       assumption
 606     | assumption
 607     ]
 608   ]
 609 ]
 610 qed.
 611