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/gcd.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
 242 theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
 243 O \lt m \to m \divides a \to m \divides b \to
 244 (gcd (a/m) (b/m)) = (gcd a b) / m.
 245 intros.
 246 apply (inj_times_r1 m H).
 247 rewrite > (sym_times m ((gcd a b)/m)).
 248 rewrite > (divides_to_times_div (gcd a b) m)
 249 [ rewrite < eq_gcd_times_times_times_gcd.
 250   rewrite > (sym_times m (a/m)).
 251   rewrite > (sym_times m (b/m)).
 252   rewrite > (divides_to_times_div a m H H1).
 253   rewrite > (divides_to_times_div b m H H2).
 254   reflexivity
 255 | assumption
 256 | apply divides_d_gcd;
 257     assumption
 258 ]
 259 qed.
 260
 261
 262
 263 theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
 264 a \divides (b*c) \to (a/(gcd a b)) \divides c.
 265 intros.
 266 apply (nat_case1 a)
 267 [ intros.
 268   apply (nat_case1 b)
 269   [ (*It's an impossible situation*)
 270     intros.
 271     simplify.
 272     apply divides_SO_n
 273   | intros.
 274     cut (c = O)
 275     [ rewrite > Hcut.
 276       apply (divides_n_n O)
 277     | apply (lt_times_eq_O b c)
 278       [ rewrite > H2.
 279         apply lt_O_S
 280       | apply antisymmetric_divides
 281         [ apply divides_n_O
 282         | rewrite < H1.
 283           assumption
 284         ]
 285       ]
 286     ]
 287   ]
 288 | intros.
 289   rewrite < H1.
 290   elim H.
 291   cut (O \lt a)
 292   [ cut (O \lt (gcd a b))
 293     [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
 294       [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
 295         rewrite > (divides_to_times_div a (gcd a b))
 296         [ assumption
 297         | assumption
 298         | apply divides_gcd_n
 299         ]
 300       | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
 301         [ apply eq_gcd_div_div_div_gcd
 302           [ assumption
 303           | apply divides_gcd_n
 304           | apply divides_gcd_m
 305           ]
 306         | assumption
 307         ]
 308       | apply (witness ? ? n2).
 309         apply (inj_times_r1 (gcd a b) Hcut1).
 310         rewrite < assoc_times.
 311         rewrite < sym_times in \vdash (? ? (? % ?) ?).
 312         rewrite > (divides_to_times_div b (gcd a b))
 313         [ rewrite < assoc_times in \vdash (? ? ? %).
 314           rewrite < sym_times in \vdash (? ? ? (? % ?)).
 315           rewrite > (divides_to_times_div a (gcd a b))
 316           [ assumption
 317           | assumption
 318           | apply divides_gcd_n
 319           ]
 320         | assumption
 321         | apply divides_gcd_m
 322         ]
 323       ]
 324     | rewrite > sym_gcd.
 325       apply lt_O_gcd.
 326       assumption
 327     ]
 328   | rewrite > H1.
 329     apply lt_O_S
 330   ]
 331 ]
 332 qed.
 333
 334 theorem gcd_plus_times_gcd: \forall a,b,d,m:nat.
 335 (gcd (a+m*b) b) = (gcd a b).
 336 intros.
 337 apply gcd1
 338 [ apply divides_plus
 339   [ apply divides_gcd_n
 340   | apply (trans_divides ? b ?)
 341     [ apply divides_gcd_m
 342     | rewrite > sym_times.
 343       apply (witness b (b*m) m).
 344       reflexivity
 345     ]
 346   ]
 347 | apply divides_gcd_m
 348 | intros.
 349   apply divides_d_gcd
 350   [ assumption
 351   | rewrite > (minus_plus_m_m a (m*b)).
 352     apply divides_minus
 353     [ assumption
 354     | apply (trans_divides ? b ?)
 355       [ assumption
 356       | rewrite > sym_times.
 357         apply (witness b (b*m) m).
 358         reflexivity
 359       ]
 360     ]
 361   ]
 362 ]
 363 qed.
 364
 365
 366
 367 theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
 368 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to
 369 (e*f) \divides c.
 370 intros.
 371 apply (nat_case1 c); intros
 372 [ apply divides_n_O
 373 | rewrite < H3.
 374   elim H1.
 375   elim H2.
 376   rewrite > H5.
 377   rewrite > (sym_times e f).
 378   apply (divides_times)
 379   [ apply (divides_n_n)
 380   | rewrite > H5 in H1.
 381     apply (gcd_SO_to_divides_times_to_divides f e n)
 382     [ rewrite < H5 in H1.
 383       rewrite > H3 in H1.
 384       apply (divides_to_lt_O e (S m))
 385       [ apply lt_O_S
 386       | assumption
 387       ]
 388     | assumption
 389     | assumption
 390     ]
 391   ]
 392 ]
 393 qed.
 394 (* the following theorem shows that gcd is a multiplicative function in
 395    the following sense: if a1 and a2 are relatively prime, then
 396    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
 397  *)
 398 theorem gcd_SO_to_eq_gcd_times_times_gcd_gcd: \forall a,b,c:nat.
 399 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
 400 intros.
 401 apply gcd1
 402 [ apply divides_times;
 403     apply divides_gcd_n
 404 | apply (gcd_SO_to_divides_to_divides_to_divides_times c (gcd a c) (gcd b c))
 405   [ apply gcd1
 406     [ apply divides_SO_n
 407     | apply divides_SO_n
 408     | intros.
 409       cut (d \divides a)
 410       [ cut (d \divides b)
 411         [ rewrite < H.
 412           apply (divides_d_gcd b a d Hcut1 Hcut)
 413         | apply (trans_divides d (gcd b c) b)
 414           [ assumption
 415           | apply (divides_gcd_n)
 416           ]
 417         ]
 418       | apply (trans_divides d (gcd a c) a)
 419         [ assumption
 420         | apply (divides_gcd_n)
 421         ]
 422       ]
 423     ]
 424   | apply (divides_gcd_m)
 425   | apply (divides_gcd_m)
 426   ]
 427 | intros.
 428   rewrite < (eq_gcd_times_times_times_gcd b c (gcd a c)).
 429   rewrite > (sym_times (gcd a c) b).
 430   rewrite > (sym_times (gcd a c) c).
 431   rewrite < (eq_gcd_times_times_times_gcd a c b).
 432   rewrite < (eq_gcd_times_times_times_gcd a c c).
 433   apply (divides_d_gcd)
 434   [ apply (divides_d_gcd)
 435     [ rewrite > (times_n_SO d).
 436       apply (divides_times)
 437       [ assumption
 438       | apply divides_SO_n
 439       ]
 440     | rewrite > (times_n_SO d).
 441       apply (divides_times)
 442       [ assumption
 443       | apply divides_SO_n
 444       ]
 445     ]
 446   | apply (divides_d_gcd)
 447     [ rewrite > (times_n_SO d).
 448       rewrite > (sym_times d (S O)).
 449       apply (divides_times)
 450       [ apply (divides_SO_n)
 451       | assumption
 452       ]
 453     | rewrite < (sym_times a b).
 454       assumption
 455     ]
 456   ]
 457 ]
 458 qed.
 459
 460
 461 theorem eq_gcd_gcd_minus: \forall a,b:nat.
 462 a \lt b \to (gcd a b) = (gcd (b - a) b).
 463 intros.
 464 apply sym_eq.
 465 apply gcd1
 466 [ apply (divides_minus (gcd a b) b a)
 467   [ apply divides_gcd_m
 468   | apply divides_gcd_n
 469   ]
 470 | apply divides_gcd_m
 471 | intros.
 472   elim H1.
 473   elim H2.
 474   cut(b = (d*n2) + a)
 475   [ cut (b - (d*n2) = a)
 476     [ rewrite > H4 in Hcut1.
 477       rewrite < (distr_times_minus d n n2) in Hcut1.
 478       apply divides_d_gcd
 479       [ assumption
 480       | apply (witness d a (n - n2)).
 481         apply sym_eq.
 482         assumption
 483       ]
 484     | apply (plus_to_minus ? ? ? Hcut)
 485     ]
 486   | rewrite > sym_plus.
 487     apply (minus_to_plus)
 488     [ apply lt_to_le.
 489       assumption
 490     | assumption
 491     ]
 492   ]
 493 ]
 494 qed.
 495