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