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