helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.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/propr_div_mod_lt_le_totient1_aux/".
  16
  17 include "nat/iteration2.ma".
  18
  19 (*this part of the library contains some properties useful to prove
  20   the main theorem in totient1.ma, and some new properties about gcd
  21   (see gcd_properties1.ma).
  22   These theorems are saved separately from the other part of the library
  23   in order to avoid to create circular dependences in it.
  24  *)
  25
  26 (* some basic properties of and - or*)
  27 theorem andb_sym: \forall A,B:bool.
  28 (A \land B) = (B \land A).
  29 intros.
  30 elim A;
  31   elim B;
  32     simplify;
  33     reflexivity.
  34 qed.
  35
  36 theorem andb_assoc: \forall A,B,C:bool.
  37 (A \land (B \land C)) = ((A \land B) \land C).
  38 intros.
  39 elim A;
  40   elim B;
  41     elim C;
  42       simplify;
  43       reflexivity.
  44 qed.
  45
  46 theorem orb_sym: \forall A,B:bool.
  47 (A \lor B) = (B \lor A).
  48 intros.
  49 elim A;
  50   elim B;
  51     simplify;
  52     reflexivity.
  53 qed.
  54
  55 theorem andb_t_t_t: \forall A,B,C:bool.
  56 A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
  57 intros.
  58 rewrite > H.
  59 rewrite > H1.
  60 rewrite > H2.
  61 reflexivity.
  62 qed.
  63
  64 (*properties about relational operators*)
  65
  66 theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
  67 (S a) \le b \to O \lt b.
  68 intros.
  69 elim H;
  70   apply lt_O_S.
  71 qed.
  72
  73 theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
  74 (S O) \lt n \to O \lt (pred n).
  75 intros.
  76 apply (Sa_le_b_to_O_lt_b (pred (S O)) (pred n) ?).
  77  apply (lt_pred (S O) n ? ?);
  78  [ apply (lt_O_S O)
  79  | apply (H)
  80  ]
  81 qed.
  82
  83
  84 theorem NdivM_times_M_to_N: \forall n,m:nat.
  85 O \lt m \to m \divides n \to (n / m) * m = n.
  86 intros.
  87 rewrite > plus_n_O.
  88 apply sym_eq.
  89 cut (n \mod m = O)
  90 [ rewrite < Hcut.
  91   apply div_mod.
  92   assumption
  93 | apply divides_to_mod_O;
  94     assumption.
  95 ]
  96 qed.
  97
  98 theorem lt_to_divides_to_div_le:  \forall a,c:nat.
  99 O \lt c \to c \divides a \to a/c \le a.
 100 intros.
 101 apply (le_times_to_le c (a/c) a)
 102 [ assumption
 103 | rewrite > (sym_times c (a/c)).
 104   rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
 105   [ rewrite < (sym_times a c).
 106     apply (O_lt_const_to_le_times_const).
 107     assumption
 108   | assumption
 109   | assumption
 110   ]
 111 ]
 112 qed.
 113
 114
 115 theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
 116 O \lt b \to (b*c) \le a \to c \le (a /b).
 117 intros.
 118 rewrite > (div_mod a b) in H1
 119 [ apply (le_times_to_le b ? ?)
 120   [ assumption
 121   | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
 122     [ elim Hcut
 123       [ rewrite < (sym_times c b).
 124         rewrite < (sym_times (a/b) b).
 125         assumption
 126       | cut (a/b \lt c)
 127         [ change in Hcut1 with ((S (a/b)) \le c).
 128           cut( b*(S (a/b)) \le b*c)
 129           [ rewrite > (sym_times b (S (a/b))) in Hcut2.
 130             simplify in Hcut2.
 131             cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
 132             [ cut (b \le (a \mod b))
 133               [ apply False_ind.
 134                 apply (lt_to_not_le (a \mod b) b)
 135                 [ apply (lt_mod_m_m).
 136                   assumption
 137                 | assumption
 138                 ]
 139               | apply (le_plus_to_le ((a/b)*b)).
 140                 rewrite > sym_plus.
 141                 assumption.
 142               ]
 143             | apply (trans_le ? (b*c) ?);
 144                 assumption
 145             ]
 146           | apply (le_times_r b ? ?).
 147             assumption
 148           ]
 149         | apply (lt_times_n_to_lt b (a/b) c)
 150           [ assumption
 151           | assumption
 152           ]
 153         ]
 154       ]
 155     | apply (leb_elim (c*b) ((a/b)*b))
 156       [ intros.
 157         left.
 158         assumption
 159       | intros.
 160         right.
 161         apply cic:/matita/nat/orders/not_le_to_lt.con.
 162         assumption
 163       ]
 164     ]
 165   ]
 166 | assumption
 167 ]
 168 qed.
 169
 170 theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
 171 \forall a,b:nat.
 172 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
 173 intros.
 174 elim H2.
 175 cut (O \lt n2)
 176 [ rewrite > H3.
 177   rewrite > (sym_times a n2).
 178   rewrite > (div_times_ltO n2 a);
 179     assumption
 180 | apply (divides_to_lt_O n2 b)
 181   [ assumption
 182   | apply (witness n2 b a).
 183     rewrite > sym_times.
 184     assumption
 185   ]
 186 ]
 187 qed.
 188
 189 (* some properties of div operator between natural numbers *)
 190
 191 theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
 192 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
 193 intros.
 194 elim H1.
 195 rewrite > H2.
 196 rewrite > (sym_times c n2).
 197 cut(O \lt c)
 198 [ rewrite > (div_times_ltO n2 c)
 199   [ rewrite < assoc_times.
 200     rewrite > (div_times_ltO (a *n2) c)
 201     [ reflexivity
 202     | assumption
 203     ]
 204   | assumption
 205   ]
 206 | apply (divides_to_lt_O c b);
 207     assumption.
 208 ]
 209 qed.
 210
 211
 212 theorem div_times_to_eqSO: \forall a,d:nat.
 213 O \lt d \to a*d = d \to a = (S O).
 214 intros.
 215 apply (cic:/matita/nat/div_and_mod/inj_times_r1.con d)
 216 [ assumption
 217 | rewrite > sym_times.
 218   rewrite < (times_n_SO d).
 219   assumption
 220 ]
 221 qed.
 222
 223
 224 theorem div_mod_minus:
 225 \forall a,b:nat. O \lt b \to
 226 (a /b)*b = a - (a \mod b).
 227 intros.
 228 rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
 229 [ apply (minus_plus_m_m (times (div a b) b) (mod a b))
 230 | assumption
 231 ]
 232 qed.
 233
 234 theorem sum_div_eq_div: \forall a,b,c:nat.
 235 O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
 236 intros.
 237 elim H2.
 238 rewrite > H3.
 239 rewrite > (sym_times c n2).
 240 rewrite > (div_plus_times c n2 b)
 241 [ rewrite > (div_times_ltO n2 c)
 242   [ reflexivity
 243   | assumption
 244   ]
 245 | assumption
 246 ]
 247 qed.
 248
 249
 250 (* A corollary to the division theorem (between natural numbers).
 251  *
 252  * Forall a,b,c: Nat, b > O,
 253  *  a/b = c iff (b*c <= a && a < b*(c+1)
 254  *
 255  * two parts of the theorem are proved separately
 256  *  - (=>) th_div_interi_2
 257  *  - (<=) th_div_interi_1
 258  *)
 259
 260 theorem th_div_interi_2: \forall a,b,c:nat.
 261 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
 262 intros.
 263 split
 264 [ rewrite < H1.
 265   rewrite > sym_times.
 266   rewrite > div_mod_minus
 267   [ apply (le_minus_m a (a \mod b))
 268   | assumption
 269   ]
 270 | rewrite < (times_n_Sm b c).
 271   rewrite < H1.
 272   rewrite > sym_times.
 273   rewrite > div_mod_minus
 274   [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
 275     [ rewrite < (sym_plus a b).
 276       rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
 277       [ rewrite > (plus_n_O a) in \vdash (? % ?).
 278         apply (le_to_lt_to_plus_lt)
 279         [ apply (le_n a)
 280         | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.
 281           apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
 282           assumption
 283         ]
 284       | apply lt_to_le.
 285         apply lt_mod_m_m.
 286         assumption
 287       ]
 288     | rewrite > (div_mod a b) in \vdash (? ? %)
 289       [ rewrite > plus_n_O in \vdash (? % ?).
 290         rewrite > sym_plus.
 291         apply cic:/matita/nat/le_arith/le_plus_n.con
 292       | assumption
 293       ]
 294     ]
 295   | assumption
 296   ]
 297 ]
 298 qed.
 299
 300 theorem th_div_interi_1: \forall a,c,b:nat.
 301 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 302 intros.
 303 apply (le_to_le_to_eq)
 304 [ cut (a/b \le c \lor c \lt a/b)
 305   [ elim Hcut
 306     [ assumption
 307     | change in H3 with ((S c) \le (a/b)).
 308       cut (b*(S c) \le (b*(a/b)))
 309       [ rewrite > (sym_times b (S c)) in Hcut1.
 310         cut (a \lt (b * (a/b)))
 311         [ rewrite > (div_mod a b) in Hcut2:(? % ?)
 312           [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
 313             cut ((a \mod b) \lt O)
 314             [ apply False_ind.
 315               apply (lt_to_not_le (a \mod b) O)
 316               [ assumption
 317               | apply le_O_n
 318               ]
 319             | apply (lt_plus_to_lt_r ((a/b)*b)).
 320               rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
 321               assumption
 322             ]
 323           | assumption
 324           ]
 325         | apply (lt_to_le_to_lt ? (b*(S c)) ?)
 326           [ assumption
 327           | rewrite > (sym_times b (S c)).
 328             assumption
 329           ]
 330         ]
 331       | apply le_times_r.
 332         assumption
 333       ]
 334     ]
 335   | apply (leb_elim (a/b) c)
 336     [ intros.
 337       left.
 338       assumption
 339     | intros.
 340       right.
 341       apply cic:/matita/nat/orders/not_le_to_lt.con.
 342       assumption
 343     ]
 344   ]
 345 | apply (bTIMESc_le_a_to_c_le_aDIVb);
 346     assumption
 347 ]
 348 qed.
 349
 350 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
 351 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
 352 intros.
 353 apply sym_eq.
 354 cut (b*d \le a \land a \lt b*(S d))
 355 [ elim Hcut.
 356   apply th_div_interi_1
 357   [ rewrite > (S_pred b)
 358     [ rewrite > (S_pred c)
 359       [ apply (lt_O_times_S_S)
 360       | assumption
 361       ]
 362     | assumption
 363     ]
 364   | rewrite > assoc_times.
 365     rewrite > (sym_times c d).
 366     rewrite < assoc_times.
 367     rewrite > (sym_times (b*d) c).
 368     rewrite > (sym_times a c).
 369     apply (le_times_r c (b*d) a).
 370     assumption
 371   | rewrite > (sym_times a c).
 372     rewrite > (assoc_times ).
 373     rewrite > (sym_times c (S d)).
 374     rewrite < (assoc_times).
 375     rewrite > (sym_times (b*(S d)) c).
 376     apply (lt_times_r1 c a (b*(S d)));
 377       assumption
 378   ]
 379 | apply (th_div_interi_2)
 380   [ assumption
 381   | apply sym_eq.
 382     assumption
 383   ]
 384 ]
 385 qed.
 386
 387 theorem times_numerator_denominator: \forall a,b,c:nat.
 388 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
 389 intros.
 390 apply (times_numerator_denominator_aux a b c (a/b))
 391 [ assumption
 392 | assumption
 393 | reflexivity
 394 ]
 395 qed.
 396
 397 theorem times_mod: \forall a,b,c:nat.
 398 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
 399 intros.
 400 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
 401 [ apply div_mod_spec_intro
 402   [ apply (lt_mod_m_m (a*c) (b*c)).
 403     rewrite > (S_pred b)
 404     [ rewrite > (S_pred c)
 405       [ apply lt_O_times_S_S
 406       | assumption
 407       ]
 408     | assumption
 409     ]
 410   | rewrite > (times_numerator_denominator a b c)
 411     [ apply (div_mod (a*c) (b*c)).
 412       rewrite > (S_pred b)
 413       [ rewrite > (S_pred c)
 414         [ apply (lt_O_times_S_S)
 415         | assumption
 416         ]
 417       | assumption
 418       ]
 419     | assumption
 420     | assumption
 421     ]
 422   ]
 423 | constructor 1
 424   [ rewrite > (sym_times b c).
 425     apply (lt_times_r1 c)
 426     [ assumption
 427     | apply (lt_mod_m_m).
 428       assumption
 429     ]
 430   | rewrite < (assoc_times (a/b) b c).
 431     rewrite > (sym_times a c).
 432     rewrite > (sym_times ((a/b)*b) c).
 433     rewrite < (distr_times_plus c ? ?).
 434     apply eq_f.
 435     apply (div_mod a b).
 436     assumption
 437   ]
 438 ]
 439 qed.
 440
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450