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 (* a basic property of divides predicate *)
 161
 162 theorem O_div_c_to_c_eq_O: \forall c:nat.
 163 O \divides c \to c = O.
 164 intros.
 165 apply antisymmetric_divides
 166 [ apply divides_n_O
 167 | assumption
 168 ]
 169 qed.
 170
 171 (* an alternative characterization for gcd *)
 172 theorem gcd1: \forall a,b,c:nat.
 173 c \divides a \to c \divides b \to
 174 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
 175 intros.
 176 elim (H2 ((gcd a b)))
 177 [ apply (antisymmetric_divides (gcd a b) c)
 178   [ apply (witness (gcd a b) c n2).
 179     assumption
 180   | apply divides_d_gcd;
 181       assumption
 182   ]
 183 | apply divides_gcd_n
 184 | rewrite > sym_gcd.
 185   apply divides_gcd_n
 186 ]
 187 qed.
 188
 189
 190 theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat.
 191 (gcd (c*a) (c*b)) = c*(gcd a b).
 192 intros.
 193 apply (nat_case1 c)
 194 [ intros.
 195   simplify.
 196   reflexivity
 197 | intros.
 198   rewrite < H.
 199   apply gcd1
 200   [ apply divides_times
 201     [ apply divides_n_n
 202     | apply divides_gcd_n.
 203     ]
 204   | apply divides_times
 205     [ apply divides_n_n
 206     | rewrite > sym_gcd.
 207       apply divides_gcd_n
 208     ]
 209   | intros.
 210     apply (divides_d_times_gcd)
 211     [ rewrite > H.
 212       apply lt_O_S
 213     | assumption
 214     | assumption
 215     ]
 216   ]
 217 ]
 218 qed.
 219
 220 theorem associative_nat_gcd: associative nat gcd.
 221 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
 222 intros.
 223 apply gcd1
 224 [ apply divides_d_gcd
 225   [ apply (trans_divides ? (gcd b c) ?)
 226     [ apply divides_gcd_m
 227     | apply divides_gcd_n
 228     ]
 229   | apply divides_gcd_n
 230   ]
 231 | apply (trans_divides ? (gcd b c) ?)
 232   [ apply divides_gcd_m
 233   | apply divides_gcd_m
 234   ]
 235 | intros.
 236   cut (d \divides a \land d \divides b)
 237   [ elim Hcut.
 238     cut (d \divides (gcd b c))
 239     [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
 240     | apply (divides_d_gcd c b d H1 H3)
 241     ]
 242   | split
 243     [ apply (trans_divides d (gcd a b) a H).
 244       apply divides_gcd_n
 245     | apply (trans_divides d (gcd a b) b H).
 246       apply divides_gcd_m
 247     ]
 248   ]
 249 ]
 250 qed.
 251
 252 theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
 253 a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
 254 intros.
 255 apply (nat_case1 a)
 256 [ intros.
 257   apply (nat_case1 b)
 258   [ intros.
 259     cut (d = O)
 260     [ rewrite > Hcut.
 261       simplify.
 262       apply divides_SO_n
 263     | rewrite > H2 in H1.
 264       rewrite > H3 in H1.
 265       apply sym_eq.
 266       assumption
 267     ]
 268   | intros.
 269     cut (O \lt d)
 270     [ rewrite > (S_pred d Hcut).
 271       simplify.
 272       rewrite > H2 in H.
 273       cut (c = O)
 274       [ rewrite > Hcut1.
 275         apply (divides_n_n O)
 276       | apply (lt_times_eq_O b c)
 277         [ rewrite > H3.
 278           apply lt_O_S
 279         | apply (O_div_c_to_c_eq_O (b*c) H)
 280         ]
 281       ]
 282     | rewrite < H1.
 283       apply lt_O_gcd.
 284       rewrite > H3.
 285       apply lt_O_S
 286     ]
 287   ]
 288 | intros.
 289   rewrite < H2.
 290   elim H.
 291   cut (d \divides a \land d \divides b)
 292   [ cut (O \lt a)
 293     [ cut (O \lt d)
 294       [ elim Hcut.
 295         rewrite < (NdivM_times_M_to_N a d) in H3
 296         [ rewrite < (NdivM_times_M_to_N b d) in H3
 297           [ cut (b/d*c = a/d*n2)
 298             [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
 299               [ apply (O_lt_times_to_O_lt (a/d) d).
 300                 rewrite > (NdivM_times_M_to_N a d);
 301                   assumption
 302               | apply (inj_times_r1 d ? ?)
 303                 [ assumption
 304                 | rewrite < (eq_gcd_times_times_eqv_times_gcd (a/d) (b/d) d).
 305                   rewrite < (times_n_SO d).
 306                   rewrite < (sym_times (a/d) d).
 307                   rewrite < (sym_times (b/d) d).
 308                   rewrite > (NdivM_times_M_to_N a d)
 309                   [ rewrite > (NdivM_times_M_to_N b d);
 310                       assumption
 311                   | assumption
 312                   | assumption
 313                   ]
 314                 ]
 315               | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
 316               ]
 317             | apply (inj_times_r1 d ? ?)
 318               [ assumption
 319               | rewrite > sym_times.
 320                 rewrite > (sym_times d ((a/d) * n2)).
 321                 rewrite > assoc_times.
 322                 rewrite > (assoc_times (a/d) n2 d).
 323                 rewrite > (sym_times c d).
 324                 rewrite > (sym_times n2 d).
 325                 rewrite < assoc_times.
 326                 rewrite < (assoc_times (a/d) d n2).
 327                 assumption
 328               ]
 329             ]
 330           | assumption
 331           | assumption
 332           ]
 333         | assumption
 334         | assumption
 335         ]
 336       | rewrite < H1.
 337         rewrite > sym_gcd.
 338         apply lt_O_gcd.
 339         assumption
 340       ]
 341     | rewrite > H2.
 342       apply lt_O_S
 343     ]
 344   | rewrite < H1.
 345     split
 346     [ apply divides_gcd_n
 347     | apply divides_gcd_m
 348     ]
 349   ]
 350 ]
 351 qed.
 352
 353 theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat.
 354 (gcd (a+m*b) b) = d \to (gcd a b) = d.
 355 intros.
 356 apply gcd1
 357 [ rewrite > (minus_plus_m_m a (m*b)).
 358   apply divides_minus
 359   [ rewrite < H.
 360     apply divides_gcd_n
 361   | rewrite > (times_n_SO d).
 362     rewrite > (sym_times d ?).
 363     apply divides_times
 364     [ apply divides_SO_n
 365     | rewrite < H.
 366       apply divides_gcd_m
 367     ]
 368   ]
 369 | rewrite < H.
 370   apply divides_gcd_m
 371 | intros.
 372   rewrite < H.
 373   apply divides_d_gcd
 374   [ assumption
 375   | apply divides_plus
 376     [ assumption
 377     | rewrite > (times_n_SO d1).
 378       rewrite > (sym_times d1 ?).
 379       apply divides_times
 380       [ apply divides_SO_n
 381       | assumption
 382       ]
 383     ]
 384   ]
 385 ]
 386 qed.
 387
 388 theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat.
 389 (gcd (a+m*b) b) = (gcd a b).
 390 intros.
 391 apply sym_eq.
 392 apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
 393 reflexivity.
 394 qed.
 395
 396 theorem gcd_div_div_eq_div_gcd: \forall a,b,m:nat.
 397 O \lt m \to m \divides a \to m \divides b \to
 398 (gcd (a/m) (b/m)) = (gcd a b) / m.
 399 intros.
 400 apply (inj_times_r1 m H).
 401 rewrite > (sym_times m ((gcd a b)/m)).
 402 rewrite > (NdivM_times_M_to_N (gcd a b) m)
 403 [ rewrite < eq_gcd_times_times_eqv_times_gcd.
 404   rewrite > (sym_times m (a/m)).
 405   rewrite > (sym_times m (b/m)).
 406   rewrite > (NdivM_times_M_to_N a m H H1).
 407   rewrite > (NdivM_times_M_to_N b m H H2).
 408   reflexivity
 409 | assumption
 410 | apply divides_d_gcd;
 411     assumption
 412 ]
 413 qed.
 414
 415
 416 theorem gcdSO_divides_divides_times_divides: \forall c,e,f:nat.
 417 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to
 418 (e*f) \divides c.
 419 intros.
 420 apply (nat_case1 e)
 421 [ intros.
 422   apply (nat_case1 c)
 423   [ intros.
 424     simplify.
 425     apply (divides_n_n O).
 426   | intros.
 427     rewrite > H3 in H1.
 428     apply False_ind.
 429     cut (O \lt O)
 430     [ apply (le_to_not_lt O O)
 431       [ apply (le_n O)
 432       | assumption
 433       ]
 434     | apply (divides_to_lt_O O c)
 435       [ rewrite > H4.
 436         apply lt_O_S
 437       | assumption
 438       ]
 439     ]
 440   ]
 441 | intros.
 442   rewrite < H3.
 443   elim H1.
 444   elim H2.
 445   rewrite > H5.
 446   rewrite > (sym_times e f).
 447   apply (divides_times)
 448   [ apply (divides_n_n)
 449   | rewrite > H5 in H1.
 450     apply (gcd_SO_to_divides_times_to_divides f e n)
 451     [ rewrite > H3.
 452       apply (lt_O_S m)
 453     | assumption
 454     | assumption
 455     ]
 456   ]
 457 ]
 458 qed.
 459
 460
 461 (* the following theorem shows that gcd is a multiplicative function in
 462    the following sense: if a1 and a2 are relatively prime, then
 463    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
 464  *)
 465 theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
 466 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
 467 intros.
 468 apply gcd1
 469 [ apply divides_times;
 470     apply divides_gcd_n
 471 | apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
 472   [ apply gcd1
 473     [ apply divides_SO_n
 474     | apply divides_SO_n
 475     | intros.
 476       cut (d \divides a)
 477       [ cut (d \divides b)
 478         [ rewrite < H.
 479           apply (divides_d_gcd b a d Hcut1 Hcut)
 480         | apply (trans_divides d (gcd b c) b)
 481           [ assumption
 482           | apply (divides_gcd_n)
 483           ]
 484         ]
 485       | apply (trans_divides d (gcd a c) a)
 486         [ assumption
 487         | apply (divides_gcd_n)
 488         ]
 489       ]
 490     ]
 491   | apply (divides_gcd_m)
 492   | apply (divides_gcd_m)
 493   ]
 494 | intros.
 495   rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
 496   rewrite > (sym_times (gcd a c) b).
 497   rewrite > (sym_times (gcd a c) c).
 498   rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
 499   rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
 500   apply (divides_d_gcd)
 501   [ apply (divides_d_gcd)
 502     [ rewrite > (times_n_SO d).
 503       apply (divides_times)
 504       [ assumption
 505       | apply divides_SO_n
 506       ]
 507     | rewrite > (times_n_SO d).
 508       apply (divides_times)
 509       [ assumption
 510       | apply divides_SO_n
 511       ]
 512     ]
 513   | apply (divides_d_gcd)
 514     [ rewrite > (times_n_SO d).
 515       rewrite > (sym_times d (S O)).
 516       apply (divides_times)
 517       [ apply (divides_SO_n)
 518       | assumption
 519       ]
 520     | rewrite < (sym_times a b).
 521       assumption
 522     ]
 523   ]
 524 ]
 525 qed.
 526
 527
 528 theorem gcd_eq_gcd_minus: \forall a,b:nat.
 529 a \lt b \to (gcd a b) = (gcd (b - a) b).
 530 intros.
 531 apply sym_eq.
 532 apply gcd1
 533 [ apply (divides_minus (gcd a b) b a)
 534   [ apply divides_gcd_m
 535   | apply divides_gcd_n
 536   ]
 537 | apply divides_gcd_m
 538 | intros.
 539   elim H1.
 540   elim H2.
 541   cut(b = (d*n2) + a)
 542   [ cut (b - (d*n2) = a)
 543     [ rewrite > H4 in Hcut1.
 544       rewrite < (distr_times_minus d n n2) in Hcut1.
 545       apply divides_d_gcd
 546       [ assumption
 547       | apply (witness d a (n - n2)).
 548         apply sym_eq.
 549         assumption
 550       ]
 551     | apply (plus_to_minus ? ? ? Hcut)
 552     ]
 553   | rewrite > sym_plus.
 554     apply (minus_to_plus)
 555     [ apply lt_to_le.
 556       assumption
 557     | assumption
 558     ]
 559   ]
 560 ]
 561 qed.
 562