matita/library/nat/lt_arith.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/div_and_mod.ma".
  18
  19 (* plus *)
  20 theorem monotonic_lt_plus_r:
  21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
  22 simplify.intros.
  23 elim n.simplify.assumption.
  24 simplify.unfold lt.
  25 apply le_S_S.assumption.
  26 qed.
  27
  28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
  29 monotonic_lt_plus_r.
  30
  31 theorem monotonic_lt_plus_l:
  32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
  33 simplify.
  34 intros.
  35 rewrite < sym_plus. rewrite < (sym_plus n).
  36 apply lt_plus_r.assumption.
  37 qed.
  38
  39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
  40 monotonic_lt_plus_l.
  41
  42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
  43 intros.
  44 apply (trans_lt ? (n + q)).
  45 apply lt_plus_r.assumption.
  46 apply lt_plus_l.assumption.
  47 qed.
  48
  49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
  50 intro.elim n.
  51 rewrite > plus_n_O.
  52 rewrite > (plus_n_O q).assumption.
  53 apply H.
  54 unfold lt.apply le_S_S_to_le.
  55 rewrite > plus_n_Sm.
  56 rewrite > (plus_n_Sm q).
  57 exact H1.
  58 qed.
  59
  60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
  61 intros.apply (lt_plus_to_lt_l n).
  62 rewrite > sym_plus.
  63 rewrite > (sym_plus q).assumption.
  64 qed.
  65
  66 theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat.
  67 a \le c \to b \lt d \to (a + b) \lt (c+d).
  68 intros.
  69 cut (a \lt c \lor a = c)
  70 [ elim Hcut
  71   [ apply (lt_plus );
  72       assumption
  73   | rewrite > H2.
  74     apply (lt_plus_r c b d).
  75     assumption
  76   ]
  77 | apply le_to_or_lt_eq.
  78   assumption
  79 ]
  80 qed.
  81
  82
  83 (* times and zero *)
  84 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
  85 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
  86 qed.
  87
  88 theorem lt_times_eq_O: \forall a,b:nat.
  89 O \lt a \to (a * b) = O \to b = O.
  90 intros.
  91 apply (nat_case1 b)
  92 [ intros.
  93   reflexivity
  94 | intros.
  95   rewrite > H2 in H1.
  96   rewrite > (S_pred a) in H1
  97   [ apply False_ind.
  98     apply (eq_to_not_lt O ((S (pred a))*(S m)))
  99     [ apply sym_eq.
 100       assumption
 101     | apply lt_O_times_S_S
 102     ]
 103   | assumption
 104   ]
 105 ]
 106 qed.
 107
 108 theorem O_lt_times_to_O_lt: \forall a,c:nat.
 109 O \lt (a * c) \to O \lt a.
 110 intros.
 111 apply (nat_case1 a)
 112 [ intros.
 113   rewrite > H1 in H.
 114   simplify in H.
 115   assumption
 116 | intros.
 117   apply lt_O_S
 118 ]
 119 qed.
 120
 121 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 122 intros.
 123 elim (le_to_or_lt_eq O ? (le_O_n m))
 124   [assumption
 125   |apply False_ind.
 126    rewrite < H1 in H.
 127    rewrite < times_n_O in H.
 128    apply (not_le_Sn_O ? H)
 129   ]
 130 qed.
 131
 132 (* times *)
 133 theorem monotonic_lt_times_r:
 134 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
 135 simplify.
 136 intros.elim n.
 137 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 138 apply lt_plus.assumption.assumption.
 139 qed.
 140
 141 (* a simple variant of the previus monotionic_lt_times *)
 142 theorem monotonic_lt_times_variant: \forall c:nat.
 143 O \lt c \to monotonic nat lt (\lambda t.(t*c)).
 144 intros.
 145 apply (increasing_to_monotonic).
 146 unfold increasing.
 147 intros.
 148 simplify.
 149 rewrite > sym_plus.
 150 rewrite > plus_n_O in \vdash (? % ?).
 151 apply lt_plus_r.
 152 assumption.
 153 qed.
 154
 155 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 156 \def monotonic_lt_times_r.
 157
 158 theorem monotonic_lt_times_l:
 159 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
 160 simplify.
 161 intros.
 162 rewrite < sym_times.rewrite < (sym_times (S m)).
 163 apply lt_times_r.assumption.
 164 qed.
 165
 166 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
 167 \def monotonic_lt_times_l.
 168
 169 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
 170 intro.
 171 elim n.
 172 apply (lt_O_n_elim m H).
 173 intro.
 174 cut (lt O q).
 175 apply (lt_O_n_elim q Hcut).
 176 intro.change with (O < (S m1)*(S m2)).
 177 apply lt_O_times_S_S.
 178 apply (ltn_to_ltO p q H1).
 179 apply (trans_lt ? ((S n1)*q)).
 180 apply lt_times_r.assumption.
 181 cut (lt O q).
 182 apply (lt_O_n_elim q Hcut).
 183 intro.
 184 apply lt_times_l.
 185 assumption.
 186 apply (ltn_to_ltO p q H2).
 187 qed.
 188
 189 theorem lt_times_r1:
 190 \forall n,m,p. O < n \to m < p \to n*m < n*p.
 191 intros.
 192 elim H;apply lt_times_r;assumption.
 193 qed.
 194
 195 theorem lt_times_l1:
 196 \forall n,m,p. O < n \to m < p \to m*n < p*n.
 197 intros.
 198 elim H;apply lt_times_l;assumption.
 199 qed.
 200
 201 theorem lt_to_le_to_lt_times :
 202 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
 203 intros.
 204 apply (le_to_lt_to_lt ? (n*m1))
 205   [apply le_times_r.assumption
 206   |apply lt_times_l1
 207     [assumption|assumption]
 208   ]
 209 qed.
 210
 211 theorem lt_times_to_lt_l:
 212 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 213 intros.
 214 cut (p < q \lor p \nlt q).
 215 elim Hcut.
 216 assumption.
 217 absurd (p * (S n) < q * (S n)).
 218 assumption.
 219 apply le_to_not_lt.
 220 apply le_times_l.
 221 apply not_lt_to_le.
 222 assumption.
 223 exact (decidable_lt p q).
 224 qed.
 225
 226 theorem lt_times_n_to_lt:
 227 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
 228 intro.
 229 apply (nat_case n)
 230   [intros.apply False_ind.apply (not_le_Sn_n ? H)
 231   |intros 4.apply lt_times_to_lt_l
 232   ]
 233 qed.
 234
 235 theorem lt_times_to_lt_r:
 236 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 237 intros.
 238 apply (lt_times_to_lt_l n).
 239 rewrite < sym_times.
 240 rewrite < (sym_times (S n)).
 241 assumption.
 242 qed.
 243
 244 theorem lt_times_n_to_lt_r:
 245 \forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
 246 intro.
 247 apply (nat_case n)
 248   [intros.apply False_ind.apply (not_le_Sn_n ? H)
 249   |intros 4.apply lt_times_to_lt_r
 250   ]
 251 qed.
 252
 253
 254
 255 theorem nat_compare_times_l : \forall n,p,q:nat.
 256 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 257 intros.apply nat_compare_elim.intro.
 258 apply nat_compare_elim.
 259 intro.reflexivity.
 260 intro.absurd (p=q).
 261 apply (inj_times_r n).assumption.
 262 apply lt_to_not_eq. assumption.
 263 intro.absurd (q<p).
 264 apply (lt_times_to_lt_r n).assumption.
 265 apply le_to_not_lt.apply lt_to_le.assumption.
 266 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
 267 intro.apply nat_compare_elim.intro.
 268 absurd (p<q).
 269 apply (lt_times_to_lt_r n).assumption.
 270 apply le_to_not_lt.apply lt_to_le.assumption.
 271 intro.absurd (q=p).
 272 symmetry.
 273 apply (inj_times_r n).assumption.
 274 apply lt_to_not_eq.assumption.
 275 intro.reflexivity.
 276 qed.
 277
 278 (* times and plus *)
 279 theorem lt_times_plus_times: \forall a,b,n,m:nat.
 280 a < n \to b < m \to a*m + b < n*m.
 281 intros 3.
 282 apply (nat_case n)
 283   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 284   |intros.simplify.
 285    rewrite < sym_plus.
 286    unfold.
 287    change with (S b+a*m1 \leq m1+m*m1).
 288    apply le_plus
 289     [assumption
 290     |apply le_times
 291       [apply le_S_S_to_le.assumption
 292       |apply le_n
 293       ]
 294     ]
 295   ]
 296 qed.
 297
 298 (* div *)
 299
 300 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
 301 intros 4.apply (lt_O_n_elim m H).intros.
 302 apply (lt_times_to_lt_r m1).
 303 rewrite < times_n_O.
 304 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
 305 rewrite < H2.
 306 rewrite < sym_times.
 307 rewrite < div_mod.
 308 rewrite > H2.
 309 assumption.
 310 unfold lt.apply le_S_S.apply le_O_n.
 311 qed.
 312
 313 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 314 intros.
 315 apply (nat_case1 (n / m)).intro.
 316 assumption.intros.rewrite < H2.
 317 rewrite > (div_mod n m) in \vdash (? ? %).
 318 apply (lt_to_le_to_lt ? ((n / m)*m)).
 319 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 320 rewrite < sym_times.
 321 rewrite > H2.
 322 simplify.unfold lt.
 323 rewrite < plus_n_O.
 324 rewrite < plus_n_Sm.
 325 apply le_S_S.
 326 apply le_S_S.
 327 apply le_plus_n.
 328 apply le_times_r.
 329 assumption.
 330 rewrite < sym_plus.
 331 apply le_plus_n.
 332 apply (trans_lt ? (S O)).
 333 unfold lt. apply le_n.assumption.
 334 qed.
 335
 336 theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
 337 q/n/m = q/(n*m).
 338 intros.
 339 apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
 340   [apply div_mod_spec_intro
 341     [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
 342       [rewrite < times_n_Sm.
 343        apply lt_plus_l.
 344        apply lt_mod_m_m.
 345        assumption
 346       |apply le_times_r.
 347        apply lt_mod_m_m.
 348        assumption
 349       ]
 350     |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
 351      rewrite < assoc_times.
 352      rewrite > (eq_times_div_minus_mod ? ? H1).
 353      rewrite > sym_times.
 354      rewrite > distributive_times_minus.
 355      rewrite > sym_times.
 356      rewrite > (eq_times_div_minus_mod ? ? H).
 357      rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
 358      rewrite < assoc_plus.
 359      rewrite < plus_minus_m_m
 360       [rewrite < plus_minus_m_m
 361         [reflexivity
 362         |apply (eq_plus_to_le ? ? ((q/n)*n)).
 363          rewrite < sym_plus.
 364          apply div_mod.
 365          assumption
 366         ]
 367       |apply (trans_le ? (n*(q/n)))
 368         [apply le_times_r.
 369          apply (eq_plus_to_le ? ? ((q/n)/m*m)).
 370          rewrite < sym_plus.
 371          apply div_mod.
 372          assumption
 373         |rewrite > sym_times.
 374          rewrite > eq_times_div_minus_mod
 375           [apply le_n
 376           |assumption
 377           ]
 378         ]
 379       ]
 380     ]
 381   |apply div_mod_spec_div_mod.
 382    rewrite > (times_n_O O).
 383    apply lt_times;assumption
 384   ]
 385 qed.
 386
 387 theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
 388 q/n/m = q/m/n.
 389 intros.
 390 apply (trans_eq ? ? (q/(n*m)))
 391   [apply eq_div_div_div_times;assumption
 392   |rewrite > sym_times.
 393    apply sym_eq.
 394    apply eq_div_div_div_times;assumption
 395   ]
 396 qed.
 397
 398 theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
 399 intros.
 400 rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
 401   [rewrite > eq_div_div_div_div
 402     [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
 403      apply div_mod.
 404      apply lt_O_S
 405     |apply lt_O_S
 406     |assumption
 407     ]
 408   |apply lt_O_S
 409   ]
 410 qed.
 411 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
 412 (* The theorem is shown in two different parts: *)
 413
 414 theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
 415 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
 416 intros.
 417 split
 418 [ rewrite < H1.
 419   rewrite > sym_times.
 420   rewrite > eq_times_div_minus_mod
 421   [ apply (le_minus_m a (a \mod b))
 422   | assumption
 423   ]
 424 | rewrite < (times_n_Sm b c).
 425   rewrite < H1.
 426   rewrite > sym_times.
 427   rewrite > (div_mod a b) in \vdash (? % ?)
 428   [ rewrite > (sym_plus b ((a/b)*b)).
 429     apply lt_plus_r.
 430     apply lt_mod_m_m.
 431     assumption
 432   | assumption
 433   ]
 434 ]
 435 qed.
 436
 437 theorem lt_to_le_times_to_lt_S_to_div: \forall a,c,b:nat.
 438 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 439 intros.
 440 apply (le_to_le_to_eq)
 441 [ apply (leb_elim (a/b) c);intros
 442   [ assumption
 443   | cut (c \lt (a/b))
 444     [ apply False_ind.
 445       apply (lt_to_not_le (a \mod b) O)
 446       [ apply (lt_plus_to_lt_l ((a/b)*b)).
 447         simplify.
 448         rewrite < sym_plus.
 449         rewrite < div_mod
 450         [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
 451           [ assumption
 452           | rewrite > (sym_times (a/b) b).
 453             apply le_times_r.
 454             assumption
 455           ]
 456         | assumption
 457         ]
 458       | apply le_O_n
 459       ]
 460     | apply not_le_to_lt.
 461       assumption
 462     ]
 463   ]
 464 | apply (leb_elim c (a/b));intros
 465   [ assumption
 466   | cut((a/b) \lt c)
 467     [ apply False_ind.
 468       apply (lt_to_not_le (a \mod b) b)
 469       [ apply (lt_mod_m_m).
 470         assumption
 471       | apply (le_plus_to_le ((a/b)*b)).
 472         rewrite < (div_mod a b)
 473         [ apply (trans_le ? (b*c) ?)
 474           [ rewrite > (sym_times (a/b) b).
 475             rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
 476             rewrite < distr_times_plus.
 477             rewrite > sym_plus.
 478             simplify in \vdash (? (? ? %) ?).
 479             apply le_times_r.
 480             assumption
 481           | assumption
 482           ]
 483         | assumption
 484         ]
 485       ]
 486     | apply not_le_to_lt.
 487       assumption
 488     ]
 489   ]
 490 ]
 491 qed.
 492
 493
 494 theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat.
 495 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
 496 intros.
 497 apply sym_eq.
 498 cut (b*(a/b) \le a \land a \lt b*(S (a/b)))
 499 [ elim Hcut.
 500   apply lt_to_le_times_to_lt_S_to_div
 501   [ rewrite > (S_pred b)
 502     [ rewrite > (S_pred c)
 503       [ apply (lt_O_times_S_S)
 504       | assumption
 505       ]
 506     | assumption
 507     ]
 508   | rewrite > assoc_times.
 509     rewrite > (sym_times c (a/b)).
 510     rewrite < assoc_times.
 511     rewrite > (sym_times (b*(a/b)) c).
 512     rewrite > (sym_times a c).
 513     apply (le_times_r c (b*(a/b)) a).
 514     assumption
 515   | rewrite > (sym_times a c).
 516     rewrite > (assoc_times ).
 517     rewrite > (sym_times c (S (a/b))).
 518     rewrite < (assoc_times).
 519     rewrite > (sym_times (b*(S (a/b))) c).
 520     apply (lt_times_r1 c a (b*(S (a/b))));
 521       assumption
 522   ]
 523 | apply (lt_to_div_to_and_le_times_lt_S)
 524   [ assumption
 525   | reflexivity
 526   ]
 527 ]
 528 qed.
 529
 530 theorem times_mod: \forall a,b,c:nat.
 531 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
 532 intros.
 533 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
 534 [ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c)
 535   [ apply div_mod_spec_div_mod.
 536     rewrite > (S_pred b)
 537     [ rewrite > (S_pred c)
 538       [ apply lt_O_times_S_S
 539       | assumption
 540       ]
 541     | assumption
 542     ]
 543   | assumption
 544   | assumption
 545   ]
 546 | apply div_mod_spec_intro
 547   [ rewrite > (sym_times b c).
 548     apply (lt_times_r1 c)
 549     [ assumption
 550     | apply (lt_mod_m_m).
 551       assumption
 552     ]
 553   | rewrite < (assoc_times (a/b) b c).
 554     rewrite > (sym_times a c).
 555     rewrite > (sym_times ((a/b)*b) c).
 556     rewrite < (distr_times_plus c ? ?).
 557     apply eq_f.
 558     apply (div_mod a b).
 559     assumption
 560   ]
 561 ]
 562 qed.
 563
 564
 565
 566
 567 (* general properties of functions *)
 568 theorem monotonic_to_injective: \forall f:nat\to nat.
 569 monotonic nat lt f \to injective nat nat f.
 570 unfold injective.intros.
 571 apply (nat_compare_elim x y).
 572 intro.apply False_ind.apply (not_le_Sn_n (f x)).
 573 rewrite > H1 in \vdash (? ? %).
 574 change with (f x < f y).
 575 apply H.apply H2.
 576 intros.assumption.
 577 intro.apply False_ind.apply (not_le_Sn_n (f y)).
 578 rewrite < H1 in \vdash (? ? %).
 579 change with (f y < f x).
 580 apply H.apply H2.
 581 qed.
 582
 583 theorem increasing_to_injective: \forall f:nat\to nat.
 584 increasing f \to injective nat nat f.
 585 intros.apply monotonic_to_injective.
 586 apply increasing_to_monotonic.assumption.
 587 qed.
 588