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