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 elim H
  77 [ simplify.
  78   apply (lt_O_S O)
  79 | rewrite < (pred_Sn n1).
  80   apply (lt_to_le_to_lt O (S (S O)) n1)
  81   [ apply le_S.
  82     apply (le_n (S O))
  83   | assumption
  84   ]
  85 ]
  86 qed.
  87
  88
  89 theorem NdivM_times_M_to_N: \forall n,m:nat.
  90 O \lt m \to m \divides n \to (n / m) * m = n.
  91 intros.
  92 rewrite > plus_n_O.
  93 apply sym_eq.
  94 cut (O = n \mod m)
  95 [ rewrite > Hcut.
  96   apply div_mod.
  97   assumption
  98 | apply sym_eq.
  99   apply divides_to_mod_O;
 100     assumption.
 101
 102 ]
 103 qed.
 104
 105 theorem lt_to_divides_to_div_le:  \forall a,c:nat.
 106 O \lt c \to c \divides a \to a/c \le a.
 107 intros.
 108 apply (le_times_to_le c (a/c) a)
 109 [ assumption
 110 | rewrite > (sym_times c (a/c)).
 111   rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
 112   [ rewrite < (sym_times a c).
 113     apply (O_lt_const_to_le_times_const).
 114     assumption
 115   | assumption
 116   | assumption
 117   ]
 118 ]
 119 qed.
 120
 121
 122 theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
 123 O \lt b \to (b*c) \le a \to c \le (a /b).
 124 intros.
 125 rewrite > (div_mod a b) in H1
 126 [ apply (le_times_to_le b ? ?)
 127   [ assumption
 128   | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
 129     [ elim Hcut
 130       [ rewrite < (sym_times c b).
 131         rewrite < (sym_times (a/b) b).
 132         assumption
 133       | cut (a/b \lt c)
 134         [ change in Hcut1 with ((S (a/b)) \le c).
 135           cut( b*(S (a/b)) \le b*c)
 136           [ rewrite > (sym_times b (S (a/b))) in Hcut2.
 137             simplify in Hcut2.
 138             cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
 139             [ cut (b \le (a \mod b))
 140               [ apply False_ind.
 141                 apply (lt_to_not_le (a \mod b) b)
 142                 [ apply (lt_mod_m_m).
 143                   assumption
 144                 | assumption
 145                 ]
 146               | apply (le_plus_to_le ((a/b)*b)).
 147                 rewrite > sym_plus.
 148                 assumption.
 149               ]
 150             | apply (trans_le ? (b*c) ?);
 151                 assumption
 152             ]
 153           | apply (le_times_r b ? ?).
 154             assumption
 155           ]
 156         | apply (lt_times_n_to_lt b (a/b) c)
 157           [ assumption
 158           | assumption
 159           ]
 160         ]
 161       ]
 162     | apply (leb_elim (c*b) ((a/b)*b))
 163       [ intros.
 164         left.
 165         assumption
 166       | intros.
 167         right.
 168         apply cic:/matita/nat/orders/not_le_to_lt.con.
 169         assumption
 170       ]
 171     ]
 172   ]
 173 | assumption
 174 ]
 175 qed.
 176
 177 theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
 178 \forall a,b:nat.
 179 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
 180 intros.
 181 elim H2.
 182 cut (O \lt n2)
 183 [ rewrite > H3.
 184   rewrite > (sym_times a n2).
 185   rewrite > (div_times_ltO n2 a);
 186     assumption
 187 | apply (divides_to_lt_O n2 b)
 188   [ assumption
 189   | apply (witness n2 b a).
 190     rewrite > sym_times.
 191     assumption
 192   ]
 193 ]
 194 qed.
 195
 196 (* some properties of div operator between natural numbers *)
 197
 198 theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
 199 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
 200 intros.
 201 elim H1.
 202 rewrite > H2.
 203 rewrite > (sym_times c n2).
 204 cut(O \lt c)
 205 [ rewrite > (div_times_ltO n2 c)
 206   [ rewrite < assoc_times.
 207     rewrite > (div_times_ltO (a *n2) c)
 208     [ reflexivity
 209     | assumption
 210     ]
 211   | assumption
 212   ]
 213 | apply (divides_to_lt_O c b);
 214     assumption.
 215 ]
 216 qed.
 217
 218
 219 theorem div_times_to_eqSO: \forall a,d:nat.
 220 O \lt d \to a*d = d \to a = (S O).
 221 intros.
 222 rewrite > (plus_n_O d) in H1:(? ? ? %).
 223 cut (a*d -d = O)
 224 [ rewrite  > sym_times in Hcut.
 225   rewrite > times_n_SO in Hcut:(? ? (? ? %) ?).
 226   rewrite < distr_times_minus in Hcut.
 227   cut ((a - (S O)) = O)
 228   [ apply (minus_to_plus a (S O) O)
 229     [ apply (nat_case1 a)
 230       [ intros.
 231         rewrite > H2 in H1.
 232         simplify in H1.
 233         rewrite < (plus_n_O d) in H1.
 234         rewrite < H1 in H.
 235         apply False_ind.
 236         change in H with ((S O) \le O).
 237         apply (not_le_Sn_O O H)
 238       | intros.
 239         apply (le_S_S O m).
 240         apply (le_O_n m)
 241       ]
 242     | assumption
 243     ]
 244   | apply (lt_times_eq_O d (a - (S O)));
 245       assumption
 246   ]
 247 | apply (plus_to_minus ).
 248   assumption
 249 ]
 250 qed.
 251
 252 theorem div_mod_minus:
 253 \forall a,b:nat. O \lt b \to
 254 (a /b)*b = a - (a \mod b).
 255 intros.
 256 apply sym_eq.
 257 apply (inj_plus_r (a \mod b)).
 258 rewrite > (sym_plus (a \mod b) ?).
 259 rewrite < (plus_minus_m_m a (a \mod b))
 260 [ rewrite > sym_plus.
 261   apply div_mod.
 262   assumption
 263 | rewrite > (div_mod a b) in \vdash (? ? %)
 264   [ rewrite > plus_n_O in \vdash (? % ?).
 265     rewrite > sym_plus.
 266     apply cic:/matita/nat/le_arith/le_plus_n.con
 267   | assumption
 268   ]
 269 ]
 270 qed.
 271
 272 theorem sum_div_eq_div: \forall a,b,c:nat.
 273 O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
 274 intros.
 275 elim H2.
 276 rewrite > H3.
 277 rewrite > (sym_times c n2).
 278 rewrite > (div_plus_times c n2 b)
 279 [ rewrite > (div_times_ltO n2 c)
 280   [ reflexivity
 281   | assumption
 282   ]
 283 | assumption
 284 ]
 285 qed.
 286
 287
 288 (* A corollary to the division theorem (between natural numbers).
 289  *
 290  * Forall a,b,c: Nat, b > O,
 291  *  a/b = c iff (b*c <= a && a < b*(c+1)
 292  *
 293  * two parts of the theorem are proved separately
 294  *  - (=>) th_div_interi_2
 295  *  - (<=) th_div_interi_1
 296  *)
 297
 298 theorem th_div_interi_2: \forall a,b,c:nat.
 299 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
 300 intros.
 301 split
 302 [ rewrite < H1.
 303   rewrite > sym_times.
 304   rewrite > div_mod_minus
 305   [ apply (le_minus_m a (a \mod b))
 306   | assumption
 307   ]
 308 | rewrite < (times_n_Sm b c).
 309   rewrite < H1.
 310   rewrite > sym_times.
 311   rewrite > div_mod_minus
 312   [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
 313     [ rewrite < (sym_plus a b).
 314       rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
 315       [ rewrite > (plus_n_O a) in \vdash (? % ?).
 316         apply (le_to_lt_to_plus_lt)
 317         [ apply (le_n a)
 318         | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.
 319           apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
 320           assumption
 321         ]
 322       | apply lt_to_le.
 323         apply lt_mod_m_m.
 324         assumption
 325       ]
 326     | rewrite > (div_mod a b) in \vdash (? ? %)
 327       [ rewrite > plus_n_O in \vdash (? % ?).
 328         rewrite > sym_plus.
 329         apply cic:/matita/nat/le_arith/le_plus_n.con
 330       | assumption
 331       ]
 332     ]
 333   | assumption
 334   ]
 335 ]
 336 qed.
 337
 338 theorem th_div_interi_1: \forall a,c,b:nat.
 339 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 340 intros.
 341 apply (le_to_le_to_eq)
 342 [ cut (a/b \le c \lor c \lt a/b)
 343   [ elim Hcut
 344     [ assumption
 345     | change in H3 with ((S c) \le (a/b)).
 346       cut (b*(S c) \le (b*(a/b)))
 347       [ rewrite > (sym_times b (S c)) in Hcut1.
 348         cut (a \lt (b * (a/b)))
 349         [ rewrite > (div_mod a b) in Hcut2:(? % ?)
 350           [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
 351             cut ((a \mod b) \lt O)
 352             [ apply False_ind.
 353               apply (lt_to_not_le (a \mod b) O)
 354               [ assumption
 355               | apply le_O_n
 356               ]
 357             | apply (lt_plus_to_lt_r ((a/b)*b)).
 358               rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
 359               assumption
 360             ]
 361           | assumption
 362           ]
 363         | apply (lt_to_le_to_lt ? (b*(S c)) ?)
 364           [ assumption
 365           | rewrite > (sym_times b (S c)).
 366             assumption
 367           ]
 368         ]
 369       | apply le_times_r.
 370         assumption
 371       ]
 372     ]
 373   | apply (leb_elim (a/b) c)
 374     [ intros.
 375       left.
 376       assumption
 377     | intros.
 378       right.
 379       apply cic:/matita/nat/orders/not_le_to_lt.con.
 380       assumption
 381     ]
 382   ]
 383 | apply (bTIMESc_le_a_to_c_le_aDIVb);
 384     assumption
 385 ]
 386 qed.
 387
 388 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
 389 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
 390 intros.
 391 apply sym_eq.
 392 cut (b*d \le a \land a \lt b*(S d))
 393 [ elim Hcut.
 394   apply th_div_interi_1
 395   [ rewrite > (S_pred b)
 396     [ rewrite > (S_pred c)
 397       [ apply (lt_O_times_S_S)
 398       | assumption
 399       ]
 400     | assumption
 401     ]
 402   | rewrite > assoc_times.
 403     rewrite > (sym_times c d).
 404     rewrite < assoc_times.
 405     rewrite > (sym_times (b*d) c).
 406     rewrite > (sym_times a c).
 407     apply (le_times_r c (b*d) a).
 408     assumption
 409   | rewrite > (sym_times a c).
 410     rewrite > (assoc_times ).
 411     rewrite > (sym_times c (S d)).
 412     rewrite < (assoc_times).
 413     rewrite > (sym_times (b*(S d)) c).
 414     apply (lt_times_r1 c a (b*(S d)));
 415       assumption
 416   ]
 417 | apply (th_div_interi_2)
 418   [ assumption
 419   | apply sym_eq.
 420     assumption
 421   ]
 422 ]
 423 qed.
 424
 425 theorem times_numerator_denominator: \forall a,b,c:nat.
 426 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
 427 intros.
 428 apply (times_numerator_denominator_aux a b c (a/b))
 429 [ assumption
 430 | assumption
 431 | reflexivity
 432 ]
 433 qed.
 434
 435 theorem times_mod: \forall a,b,c:nat.
 436 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
 437 intros.
 438 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
 439 [ apply div_mod_spec_intro
 440   [ apply (lt_mod_m_m (a*c) (b*c)).
 441     rewrite > (S_pred b)
 442     [ rewrite > (S_pred c)
 443       [ apply lt_O_times_S_S
 444       | assumption
 445       ]
 446     | assumption
 447     ]
 448   | rewrite > (times_numerator_denominator a b c)
 449     [ apply (div_mod (a*c) (b*c)).
 450       rewrite > (S_pred b)
 451       [ rewrite > (S_pred c)
 452         [ apply (lt_O_times_S_S)
 453         | assumption
 454         ]
 455       | assumption
 456       ]
 457     | assumption
 458     | assumption
 459     ]
 460   ]
 461 | constructor 1
 462   [ rewrite > (sym_times b c).
 463     apply (lt_times_r1 c)
 464     [ assumption
 465     | apply (lt_mod_m_m).
 466       assumption
 467     ]
 468   | rewrite < (assoc_times (a/b) b c).
 469     rewrite > (sym_times a c).
 470     rewrite > (sym_times ((a/b)*b) c).
 471     rewrite < (distr_times_plus c ? ?).
 472     apply eq_f.
 473     apply (div_mod a b).
 474     assumption
 475   ]
 476 ]
 477 qed.
 478
 479
 480
 481
 482
 483
 484
 485
 486
 487
 488