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