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