helm/software/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 include "nat/gcd.ma".
  16
  17 (* this file contains some important properites of gcd in N *)
  18
  19 (* an alternative characterization for gcd *)
  20 theorem gcd1: \forall a,b,c:nat.
  21 c \divides a \to c \divides b \to
  22 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
  23 intros.
  24 elim (H2 ((gcd a b)))
  25 [ apply (antisymmetric_divides (gcd a b) c)
  26   [ apply (witness (gcd a b) c n1).
  27     assumption
  28   | apply divides_d_gcd;
  29       assumption
  30   ]
  31 | apply divides_gcd_n
  32 | rewrite > sym_gcd.
  33   apply divides_gcd_n
  34 ]
  35 qed.
  36
  37
  38 theorem eq_gcd_times_times_times_gcd: \forall a,b,c:nat.
  39 (gcd (c*a) (c*b)) = c*(gcd a b).
  40 intros.
  41 apply (nat_case1 c)
  42 [ intros.
  43   simplify.
  44   reflexivity
  45 | intros.
  46   rewrite < H.
  47   apply gcd1
  48   [ apply divides_times
  49     [ apply divides_n_n
  50     | apply divides_gcd_n.
  51     ]
  52   | apply divides_times
  53     [ apply divides_n_n
  54     | rewrite > sym_gcd.
  55       apply divides_gcd_n
  56     ]
  57   | intros.
  58     apply (divides_d_times_gcd)
  59     [ rewrite > H.
  60       apply lt_O_S
  61     | assumption
  62     | assumption
  63     ]
  64   ]
  65 ]
  66 qed.
  67
  68 theorem associative_nat_gcd: associative nat gcd.
  69 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
  70 intros.
  71 apply gcd1
  72 [ apply divides_d_gcd
  73   [ apply (trans_divides ? (gcd b c) ?)
  74     [ apply divides_gcd_m
  75     | apply divides_gcd_n
  76     ]
  77   | apply divides_gcd_n
  78   ]
  79 | apply (trans_divides ? (gcd b c) ?)
  80   [ apply divides_gcd_m
  81   | apply divides_gcd_m
  82   ]
  83 | intros.
  84   cut (d \divides a \land d \divides b)
  85   [ elim Hcut.
  86     cut (d \divides (gcd b c))
  87     [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
  88     | apply (divides_d_gcd c b d H1 H3)
  89     ]
  90   | split
  91     [ apply (trans_divides d (gcd a b) a H).
  92       apply divides_gcd_n
  93     | apply (trans_divides d (gcd a b) b H).
  94       apply divides_gcd_m
  95     ]
  96   ]
  97 ]
  98 qed.
  99
 100
 101 theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
 102 O \lt m \to m \divides a \to m \divides b \to
 103 (gcd (a/m) (b/m)) = (gcd a b) / m.
 104 intros.
 105 apply (inj_times_r1 m H).
 106 rewrite > (sym_times m ((gcd a b)/m)).
 107 rewrite > (divides_to_div m (gcd a b))
 108 [ rewrite < eq_gcd_times_times_times_gcd.
 109   rewrite > (sym_times m (a/m)).
 110   rewrite > (sym_times m (b/m)).
 111   rewrite > (divides_to_div m a H1).
 112   rewrite > (divides_to_div m b H2).
 113   reflexivity
 114 | apply divides_d_gcd;
 115     assumption
 116 ]
 117 qed.
 118
 119
 120
 121 theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
 122 a \divides (b*c) \to (a/(gcd a b)) \divides c.
 123 intros.
 124 apply (nat_case1 a)
 125 [ intros.
 126   apply (nat_case1 b)
 127   [ (*It's an impossible situation*)
 128     intros.
 129     simplify.
 130     apply divides_SO_n
 131   | intros.
 132     cut (c = O)
 133     [ rewrite > Hcut.
 134       apply (divides_n_n O)
 135     | apply (lt_times_eq_O b c)
 136       [ rewrite > H2.
 137         apply lt_O_S
 138       | apply antisymmetric_divides
 139         [ apply divides_n_O
 140         | rewrite < H1.
 141           assumption
 142         ]
 143       ]
 144     ]
 145   ]
 146 | intros.
 147   rewrite < H1.
 148   elim H.
 149   cut (O \lt a)
 150   [ cut (O \lt (gcd a b))
 151     [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
 152       [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
 153         rewrite > (divides_to_div (gcd a b) a)
 154         [ assumption
 155         | apply divides_gcd_n
 156         ]
 157       | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
 158         [ apply eq_gcd_div_div_div_gcd
 159           [ assumption
 160           | apply divides_gcd_n
 161           | apply divides_gcd_m
 162           ]
 163         | assumption
 164         ]
 165       | apply (witness ? ? n1).
 166         apply (inj_times_r1 (gcd a b) Hcut1).
 167         rewrite < assoc_times.
 168         rewrite < sym_times in \vdash (? ? (? % ?) ?).
 169         rewrite > (divides_to_div (gcd a b) b)
 170         [ rewrite < assoc_times in \vdash (? ? ? %).
 171           rewrite < sym_times in \vdash (? ? ? (? % ?)).
 172           rewrite > (divides_to_div (gcd a b) a)
 173           [ assumption
 174           | apply divides_gcd_n
 175           ]
 176         | apply divides_gcd_m
 177         ]
 178       ]
 179     | rewrite > sym_gcd.
 180       apply lt_O_gcd.
 181       assumption
 182     ]
 183   | rewrite > H1.
 184     apply lt_O_S
 185   ]
 186 ]
 187 qed.
 188
 189 theorem gcd_plus_times_gcd: \forall a,b,d,m:nat.
 190 (gcd (a+m*b) b) = (gcd a b).
 191 intros.
 192 apply gcd1
 193 [ apply divides_plus
 194   [ apply divides_gcd_n
 195   | apply (trans_divides ? b ?)
 196     [ apply divides_gcd_m
 197     | rewrite > sym_times.
 198       apply (witness b (b*m) m).
 199       reflexivity
 200     ]
 201   ]
 202 | apply divides_gcd_m
 203 | intros.
 204   apply divides_d_gcd
 205   [ assumption
 206   | rewrite > (minus_plus_m_m a (m*b)).
 207     apply divides_minus
 208     [ assumption
 209     | apply (trans_divides ? b ?)
 210       [ assumption
 211       | rewrite > sym_times.
 212         apply (witness b (b*m) m).
 213         reflexivity
 214       ]
 215     ]
 216   ]
 217 ]
 218 qed.
 219
 220
 221
 222 theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
 223 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to
 224 (e*f) \divides c.
 225 intros.
 226 apply (nat_case1 c); intros
 227 [ apply divides_n_O
 228 | rewrite < H3.
 229   elim H1.
 230   elim H2.
 231   rewrite > H5.
 232   rewrite > (sym_times e f).
 233   apply (divides_times)
 234   [ apply (divides_n_n)
 235   | rewrite > H5 in H1.
 236     apply (gcd_SO_to_divides_times_to_divides f e n)
 237     [ rewrite < H5 in H1.
 238       rewrite > H3 in H1.
 239       apply (divides_to_lt_O e (S m))
 240       [ apply lt_O_S
 241       | assumption
 242       ]
 243     | assumption
 244     | assumption
 245     ]
 246   ]
 247 ]
 248 qed.
 249 (* the following theorem shows that gcd is a multiplicative function in
 250    the following sense: if a1 and a2 are relatively prime, then
 251    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
 252  *)
 253 theorem gcd_SO_to_eq_gcd_times_times_gcd_gcd: \forall a,b,c:nat.
 254 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
 255 intros.
 256 apply gcd1
 257 [ apply divides_times;
 258     apply divides_gcd_n
 259 | apply (gcd_SO_to_divides_to_divides_to_divides_times c (gcd a c) (gcd b c))
 260   [ apply gcd1
 261     [ apply divides_SO_n
 262     | apply divides_SO_n
 263     | intros.
 264       cut (d \divides a)
 265       [ cut (d \divides b)
 266         [ rewrite < H.
 267           apply (divides_d_gcd b a d Hcut1 Hcut)
 268         | apply (trans_divides d (gcd b c) b)
 269           [ assumption
 270           | apply (divides_gcd_n)
 271           ]
 272         ]
 273       | apply (trans_divides d (gcd a c) a)
 274         [ assumption
 275         | apply (divides_gcd_n)
 276         ]
 277       ]
 278     ]
 279   | apply (divides_gcd_m)
 280   | apply (divides_gcd_m)
 281   ]
 282 | intros.
 283   rewrite < (eq_gcd_times_times_times_gcd b c (gcd a c)).
 284   rewrite > (sym_times (gcd a c) b).
 285   rewrite > (sym_times (gcd a c) c).
 286   rewrite < (eq_gcd_times_times_times_gcd a c b).
 287   rewrite < (eq_gcd_times_times_times_gcd a c c).
 288   apply (divides_d_gcd)
 289   [ apply (divides_d_gcd)
 290     [ rewrite > (times_n_SO d).
 291       apply (divides_times)
 292       [ assumption
 293       | apply divides_SO_n
 294       ]
 295     | rewrite > (times_n_SO d).
 296       apply (divides_times)
 297       [ assumption
 298       | apply divides_SO_n
 299       ]
 300     ]
 301   | apply (divides_d_gcd)
 302     [ rewrite > (times_n_SO d).
 303       rewrite > (sym_times d (S O)).
 304       apply (divides_times)
 305       [ apply (divides_SO_n)
 306       | assumption
 307       ]
 308     | rewrite < (sym_times a b).
 309       assumption
 310     ]
 311   ]
 312 ]
 313 qed.
 314
 315
 316 theorem eq_gcd_gcd_minus: \forall a,b:nat.
 317 a \lt b \to (gcd a b) = (gcd (b - a) b).
 318 intros.
 319 apply sym_eq.
 320 apply gcd1
 321 [ apply (divides_minus (gcd a b) b a)
 322   [ apply divides_gcd_m
 323   | apply divides_gcd_n
 324   ]
 325 | apply divides_gcd_m
 326 | intros.
 327   elim H1.
 328   elim H2.
 329   cut(b = (d*n1) + a)
 330   [ cut (b - (d*n1) = a)
 331     [ rewrite > H4 in Hcut1.
 332       rewrite < (distr_times_minus d n n1) in Hcut1.
 333       apply divides_d_gcd
 334       [ assumption
 335       | apply (witness d a (n - n1)).
 336         apply sym_eq.
 337         assumption
 338       ]
 339     | apply (plus_to_minus ? ? ? Hcut)
 340     ]
 341   | rewrite > sym_plus.
 342     apply (minus_to_plus)
 343     [ apply lt_to_le.
 344       assumption
 345     | assumption
 346     ]
 347   ]
 348 ]
 349 qed.
 350