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 lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
 116 \forall a,b:nat.
 117 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
 118 intros.
 119 elim H2.
 120 rewrite > H3.
 121 rewrite > (sym_times a n2).
 122 rewrite > (div_times_ltO n2 a)
 123 [ apply (divides_to_lt_O n2 b)
 124   [ assumption
 125   | apply (witness n2 b a).
 126     rewrite > sym_times.
 127     assumption
 128   ]
 129 | assumption
 130 ]
 131 qed.
 132
 133 (* some properties of div operator between natural numbers *)
 134
 135 theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
 136 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
 137 intros.
 138 elim H1.
 139 rewrite > H2.
 140 rewrite > (sym_times c n2).
 141 cut(O \lt c)
 142 [ rewrite > (div_times_ltO n2 c)
 143   [ rewrite < assoc_times.
 144     rewrite > (div_times_ltO (a *n2) c)
 145     [ reflexivity
 146     | assumption
 147     ]
 148   | assumption
 149   ]
 150 | apply (divides_to_lt_O c b);
 151     assumption.
 152 ]
 153 qed.
 154
 155 (*
 156 theorem div_times_to_eqSO: \forall a,d:nat.
 157 O \lt d \to a*d = d \to a = (S O).
 158 intros.
 159 apply (inj_times_r1 d)
 160 [ assumption
 161 | rewrite > sym_times.
 162   rewrite < (times_n_SO d).
 163   assumption
 164 ]
 165 qed.*)
 166
 167
 168 theorem div_mod_minus:
 169 \forall a,b:nat. O \lt b \to
 170 (a /b)*b = a - (a \mod b).
 171 intros.
 172 rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
 173 [ apply (minus_plus_m_m (times (div a b) b) (mod a b))
 174 | assumption
 175 ]
 176 qed.
 177
 178 (*
 179 theorem sum_div_eq_div: \forall a,b,c:nat.
 180 O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
 181 intros.
 182 elim H2.
 183 rewrite > H3.
 184 rewrite > (sym_times c n2).
 185 rewrite > (div_plus_times c n2 b)
 186 [ rewrite > (div_times_ltO n2 c)
 187   [ reflexivity
 188   | assumption
 189   ]
 190 | assumption
 191 ]
 192 qed.
 193 *)
 194
 195 (* A corollary to the division theorem (between natural numbers).
 196  *
 197  * Forall a,b,c: Nat, b > O,
 198  *  a/b = c iff (b*c <= a && a < b*(c+1)
 199  *
 200  * two parts of the theorem are proved separately
 201  *  - (=>) th_div_interi_2
 202  *  - (<=) th_div_interi_1
 203  *)
 204
 205 theorem th_div_interi_2: \forall a,b,c:nat.
 206 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
 207 intros.
 208 split
 209 [ rewrite < H1.
 210   rewrite > sym_times.
 211   rewrite > div_mod_minus
 212   [ apply (le_minus_m a (a \mod b))
 213   | assumption
 214   ]
 215 | rewrite < (times_n_Sm b c).
 216   rewrite < H1.
 217   rewrite > sym_times.
 218   rewrite > (div_mod a b) in \vdash (? % ?)
 219   [ rewrite > (sym_plus b ((a/b)*b)).
 220     apply lt_plus_r.
 221     apply lt_mod_m_m.
 222     assumption
 223   | assumption
 224   ]
 225 ]
 226 qed.
 227
 228
 229 theorem th_div_interi_1: \forall a,c,b:nat.
 230 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 231 intros.
 232 apply (le_to_le_to_eq)
 233 [ apply (leb_elim (a/b) c);intros
 234   [ assumption
 235   | cut (c \lt (a/b))
 236     [ apply False_ind.
 237       apply (lt_to_not_le (a \mod b) O)
 238       [ apply (lt_plus_to_lt_l ((a/b)*b)).
 239         simplify.
 240         rewrite < sym_plus.
 241         rewrite < div_mod
 242         [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
 243           [ assumption
 244           | rewrite > (sym_times (a/b) b).
 245             apply le_times_r.
 246             assumption
 247           ]
 248         | assumption
 249         ]
 250       | apply le_O_n
 251       ]
 252     | apply not_le_to_lt.
 253       assumption
 254     ]
 255   ]
 256 | apply (leb_elim c (a/b));intros
 257   [ assumption
 258   | cut((a/b) \lt c)
 259     [ apply False_ind.
 260       apply (lt_to_not_le (a \mod b) b)
 261       [ apply (lt_mod_m_m).
 262         assumption
 263       | apply (le_plus_to_le ((a/b)*b)).
 264         rewrite < (div_mod a b)
 265         [ apply (trans_le ? (b*c) ?)
 266           [ rewrite > (sym_times (a/b) b).
 267             rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
 268             rewrite < distr_times_plus.
 269             rewrite > sym_plus.
 270             simplify in \vdash (? (? ? %) ?).
 271             apply le_times_r.
 272             assumption
 273           | assumption
 274           ]
 275         | assumption
 276         ]
 277       ]
 278     | apply not_le_to_lt.
 279       assumption
 280     ]
 281   ]
 282 ]
 283 qed.
 284
 285
 286 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
 287 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
 288 intros.
 289 apply sym_eq.
 290 cut (b*d \le a \land a \lt b*(S d))
 291 [ elim Hcut.
 292   apply th_div_interi_1
 293   [ rewrite > (S_pred b)
 294     [ rewrite > (S_pred c)
 295       [ apply (lt_O_times_S_S)
 296       | assumption
 297       ]
 298     | assumption
 299     ]
 300   | rewrite > assoc_times.
 301     rewrite > (sym_times c d).
 302     rewrite < assoc_times.
 303     rewrite > (sym_times (b*d) c).
 304     rewrite > (sym_times a c).
 305     apply (le_times_r c (b*d) a).
 306     assumption
 307   | rewrite > (sym_times a c).
 308     rewrite > (assoc_times ).
 309     rewrite > (sym_times c (S d)).
 310     rewrite < (assoc_times).
 311     rewrite > (sym_times (b*(S d)) c).
 312     apply (lt_times_r1 c a (b*(S d)));
 313       assumption
 314   ]
 315 | apply (th_div_interi_2)
 316   [ assumption
 317   | apply sym_eq.
 318     assumption
 319   ]
 320 ]
 321 qed.
 322
 323 theorem times_numerator_denominator: \forall a,b,c:nat.
 324 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
 325 intros.
 326 apply (times_numerator_denominator_aux a b c (a/b))
 327 [ assumption
 328 | assumption
 329 | reflexivity
 330 ]
 331 qed.
 332
 333 theorem times_mod: \forall a,b,c:nat.
 334 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
 335 intros.
 336 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
 337 [ apply div_mod_spec_intro
 338   [ apply (lt_mod_m_m (a*c) (b*c)).
 339     rewrite > (S_pred b)
 340     [ rewrite > (S_pred c)
 341       [ apply lt_O_times_S_S
 342       | assumption
 343       ]
 344     | assumption
 345     ]
 346   | rewrite > (times_numerator_denominator a b c)
 347     [ apply (div_mod (a*c) (b*c)).
 348       rewrite > (S_pred b)
 349       [ rewrite > (S_pred c)
 350         [ apply (lt_O_times_S_S)
 351         | assumption
 352         ]
 353       | assumption
 354       ]
 355     | assumption
 356     | assumption
 357     ]
 358   ]
 359 | constructor 1
 360   [ rewrite > (sym_times b c).
 361     apply (lt_times_r1 c)
 362     [ assumption
 363     | apply (lt_mod_m_m).
 364       assumption
 365     ]
 366   | rewrite < (assoc_times (a/b) b c).
 367     rewrite > (sym_times a c).
 368     rewrite > (sym_times ((a/b)*b) c).
 369     rewrite < (distr_times_plus c ? ?).
 370     apply eq_f.
 371     apply (div_mod a b).
 372     assumption
 373   ]
 374 ]
 375 qed.
 376
 377
 378
 379
 380
 381
 382
 383
 384
 385
 386