matita/matita/lib/arithmetics/nat.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/relations.ma".
  13
  14 inductive nat : Type[0] ≝
  15   | O : nat
  16   | S : nat → nat.
  17
  18 interpretation "Natural numbers" 'N = nat.
  19
  20 alias num (instance 0) = "natural number".
  21
  22 definition pred ≝
  23  λn. match n with [ O ⇒ O | S p ⇒ p].
  24
  25 theorem pred_Sn : ∀n. n = pred (S n).
  26 // qed.
  27
  28 theorem injective_S : injective nat nat S.
  29 // qed.
  30
  31 (*
  32 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
  33 //. qed. *)
  34
  35 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
  36 /2/ qed.
  37
  38 definition not_zero: nat → Prop ≝
  39  λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
  40
  41 theorem not_eq_O_S : ∀n:nat. O ≠ S n.
  42 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
  43
  44 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
  45 #n (elim n) /2/ qed.
  46
  47 theorem nat_case:
  48  ∀n:nat.∀P:nat → Prop.
  49   (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
  50 #n #P (elim n) /2/ qed.
  51
  52 theorem nat_elim2 :
  53  ∀R:nat → nat → Prop.
  54   (∀n:nat. R O n)
  55   → (∀n:nat. R (S n) O)
  56   → (∀n,m:nat. R n m → R (S n) (S m))
  57   → ∀n,m:nat. R n m.
  58 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
  59
  60 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
  61 @nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
  62 qed.
  63
  64 (*************************** plus ******************************)
  65
  66 let rec plus n m ≝
  67  match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
  68
  69 interpretation "natural plus" 'plus x y = (plus x y).
  70
  71 theorem plus_O_n: ∀n:nat. n = O+n.
  72 // qed.
  73
  74 (*
  75 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
  76 // qed.
  77 *)
  78
  79 theorem plus_n_O: ∀n:nat. n = n+O.
  80 #n (elim n) normalize // qed.
  81
  82 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
  83 #n (elim n) normalize // qed.
  84
  85 (*
  86 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
  87 #n (elim n) normalize // qed.
  88 *)
  89
  90 (* deleterio?
  91 theorem plus_n_1 : ∀n:nat. S n = n+1.
  92 // qed.
  93 *)
  94
  95 theorem commutative_plus: commutative ? plus.
  96 #n (elim n) normalize // qed.
  97
  98 theorem associative_plus : associative nat plus.
  99 #n (elim n) normalize // qed.
 100
 101 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
 102 // qed.
 103
 104 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 105 #n (elim n) normalize /3/ qed.
 106
 107 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 108 \def injective_plus_r.
 109
 110 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
 111 /2/ qed. *)
 112
 113 (* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
 114 \def injective_plus_l. *)
 115
 116 (*************************** times *****************************)
 117
 118 let rec times n m ≝
 119  match n with [ O ⇒ O | S p ⇒ m+(times p m) ].
 120
 121 interpretation "natural times" 'times x y = (times x y).
 122
 123 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
 124 // qed.
 125
 126 theorem times_O_n: ∀n:nat. O = O*n.
 127 // qed.
 128
 129 theorem times_n_O: ∀n:nat. O = n*O.
 130 #n (elim n) // qed.
 131
 132 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
 133 #n (elim n) normalize // qed.
 134
 135 theorem commutative_times : commutative nat times.
 136 #n (elim n) normalize // qed.
 137
 138 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
 139 symmetric_times. *)
 140
 141 theorem distributive_times_plus : distributive nat times plus.
 142 #n (elim n) normalize // qed.
 143
 144 theorem distributive_times_plus_r :
 145   ∀a,b,c:nat. (b+c)*a = b*a + c*a.
 146 // qed.
 147
 148 theorem associative_times: associative nat times.
 149 #n (elim n) normalize // qed.
 150
 151 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 152 // qed.
 153
 154 (* ci servono questi risultati?
 155 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
 156 napply nat_elim2 /2/
 157 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
 158 // qed.
 159
 160 theorem times_n_SO : ∀n:nat. n = n * S O.
 161 #n // qed.
 162
 163 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
 164 normalize // qed.
 165
 166 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
 167 // qed.
 168
 169 theorem or_eq_eq_S: \forall n.\exists m.
 170 n = (S(S O))*m \lor n = S ((S(S O))*m).
 171 #n (elim n)
 172   ##[@ /2/
 173   ##|#a #H nelim H #b#ornelim or#aeq
 174     ##[@ b @ 2 //
 175     ##|@ (S b) @ 1 /2/
 176     ##]
 177 qed.
 178 *)
 179
 180 (******************** ordering relations ************************)
 181
 182 inductive le (n:nat) : nat → Prop ≝
 183   | le_n : le n n
 184   | le_S : ∀ m:nat. le n m → le n (S m).
 185
 186 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
 187
 188 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
 189
 190 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
 191
 192 interpretation "natural 'less than'" 'lt x y = (lt x y).
 193 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
 194
 195 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
 196 // qed. *)
 197
 198 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
 199
 200 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
 201
 202 definition gt: nat → nat → Prop ≝ λn,m.m<n.
 203
 204 interpretation "natural 'greater than'" 'gt x y = (gt x y).
 205 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
 206
 207 theorem transitive_le : transitive nat le.
 208 #a #b #c #leab #lebc (elim lebc) /2/
 209 qed.
 210
 211 (*
 212 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 213 \def transitive_le. *)
 214
 215 theorem transitive_lt: transitive nat lt.
 216 #a #b #c #ltab #ltbc (elim ltbc) /2/qed.
 217
 218 (*
 219 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
 220 \def transitive_lt. *)
 221
 222 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 223 #n #m #lenm (elim lenm) /2/ qed.
 224
 225 theorem le_O_n : ∀n:nat. O ≤ n.
 226 #n (elim n) /2/ qed.
 227
 228 theorem le_n_Sn : ∀n:nat. n ≤ S n.
 229 /2/ qed.
 230
 231 theorem le_pred_n : ∀n:nat. pred n ≤ n.
 232 #n (elim n) // qed.
 233
 234 theorem monotonic_pred: monotonic ? le pred.
 235 #n #m #lenm (elim lenm) /2/ qed.
 236
 237 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 238 (* demo *)
 239 /2/ qed.
 240
 241 (* this are instances of the le versions
 242 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
 243 /2/ qed.
 244
 245 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
 246 /2/ qed. *)
 247
 248 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
 249 #n #m #Hlt (elim Hlt) // qed.
 250
 251 (* lt vs. le *)
 252 theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
 253 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
 254
 255 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
 256 /3/ qed.
 257
 258 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
 259 /3/ qed.
 260
 261 theorem decidable_le: ∀n,m. decidable (n≤m).
 262 @nat_elim2 #n /2/ #m * /3/ qed.
 263
 264 theorem decidable_lt: ∀n,m. decidable (n < m).
 265 #n #m @decidable_le  qed.
 266
 267 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
 268 #n (elim n) /2/ qed.
 269
 270 (* this is le_S_S_to_le
 271 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
 272 /2/ qed.
 273 *)
 274
 275 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
 276 /2/ qed.
 277
 278 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
 279 @nat_elim2 #n
 280  [#abs @False_ind /2/
 281  |/2/
 282  |#m #Hind #HnotleSS @le_S_S /3/
 283  ]
 284 qed.
 285
 286 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
 287 #n #m #Hltnm (elim Hltnm) /3/ qed.
 288
 289 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
 290 /4/ qed.
 291
 292 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
 293 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
 294
 295 (* lt and le trans *)
 296
 297 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
 298 #n #m #p #H #H1 (elim H1) /2/ qed.
 299
 300 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
 301 #n #m #p #H (elim H) /3/ qed.
 302
 303 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
 304 /2/ qed.
 305
 306 theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
 307 /2/ qed.
 308
 309 (*
 310 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
 311 (S O) \lt n \to O \lt (pred n).
 312 intros.
 313 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
 314  apply (lt_pred (S O) n)
 315  [ apply (lt_O_S O)
 316  | assumption
 317  ]
 318 qed. *)
 319
 320 theorem lt_O_n_elim: ∀n:nat. O < n →
 321   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
 322 #n (elim n) // #abs @False_ind /2/
 323 qed.
 324
 325 theorem S_pred: ∀n. 0 < n → S(pred n) = n.
 326 #n #posn (cases posn) //
 327 qed.
 328
 329 (*
 330 theorem lt_pred: \forall n,m.
 331   O < n \to n < m \to pred n < pred m.
 332 apply nat_elim2
 333   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 334   |intros.apply False_ind.apply (not_le_Sn_O ? H1)
 335   |intros.simplify.unfold.apply le_S_S_to_le.assumption
 336   ]
 337 qed.
 338
 339 theorem le_pred_to_le:
 340  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
 341 intros 2
 342 elim n
 343 [ apply le_O_n
 344 | simplify in H2
 345   rewrite > (S_pred m)
 346   [ apply le_S_S
 347     assumption
 348   | assumption
 349   ]
 350 ].
 351 qed.
 352
 353 *)
 354
 355 (* le to lt or eq *)
 356 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
 357 #n #m #lenm (elim lenm) /3/ qed.
 358
 359 (* not eq *)
 360 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
 361 #n #m #H @not_to_not /2/ qed.
 362
 363 (*not lt
 364 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
 365 intros.
 366 unfold Not.
 367 intros.
 368 rewrite > H in H1.
 369 apply (lt_to_not_eq b b)
 370 [ assumption
 371 | reflexivity
 372 ]
 373 qed.
 374
 375 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
 376 intros
 377 unfold Not
 378 intro
 379 unfold lt in H
 380 unfold lt in H1
 381 generalize in match (le_S_S ? ? H)
 382 intro
 383 generalize in match (transitive_le ? ? ? H2 H1)
 384 intro
 385 apply (not_le_Sn_n ? H3).
 386 qed. *)
 387
 388 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 389 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
 390 #Heq /3/ qed.
 391 (*
 392 nelim (Hneq Heq) qed. *)
 393
 394 (* le elimination *)
 395 theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
 396 #n (cases n) // #a  #abs @False_ind /2/ qed.
 397
 398 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
 399 #n (cases n) // #a #abs @False_ind /2/ qed.
 400
 401 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 402 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
 403 #n #m #Hle #P (elim Hle) /3/ qed.
 404
 405 (* le and eq *)
 406
 407 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
 408 @nat_elim2 /4/
 409 qed.
 410
 411 theorem lt_O_S : ∀n:nat. O < S n.
 412 /2/ qed.
 413
 414 (*
 415 (* other abstract properties *)
 416 theorem antisymmetric_le : antisymmetric nat le.
 417 unfold antisymmetric.intros 2.
 418 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 419 intros.apply le_n_O_to_eq.assumption.
 420 intros.apply False_ind.apply (not_le_Sn_O ? H).
 421 intros.apply eq_f.apply H.
 422 apply le_S_S_to_le.assumption.
 423 apply le_S_S_to_le.assumption.
 424 qed.
 425
 426 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 427 \def antisymmetric_le.
 428
 429 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 430 intros
 431 unfold lt in H1
 432 generalize in match (le_S_S_to_le ? ? H1)
 433 intro
 434 apply antisym_le
 435 assumption.
 436 qed.
 437 *)
 438
 439 (* well founded induction principles *)
 440
 441 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
 442 (∀m.(∀p. p < m → P p) → P m) → P n.
 443 #n #P #H
 444 cut (∀q:nat. q ≤ n → P q) /2/
 445 (elim n)
 446  [#q #HleO (* applica male *)
 447     @(le_n_O_elim ? HleO)
 448     @H #p #ltpO @False_ind /2/ (* 3 *)
 449  |#p #Hind #q #HleS
 450     @H #a #lta @Hind @le_S_S_to_le /2/
 451  ]
 452 qed.
 453
 454 (* some properties of functions *)
 455 (*
 456 definition increasing \def \lambda f:nat \to nat.
 457 \forall n:nat. f n < f (S n).
 458
 459 theorem increasing_to_monotonic: \forall f:nat \to nat.
 460 increasing f \to monotonic nat lt f.
 461 unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
 462 apply (trans_le ? (f n1)).
 463 assumption.apply (trans_le ? (S (f n1))).
 464 apply le_n_Sn.
 465 apply H.
 466 qed.
 467
 468 theorem le_n_fn: \forall f:nat \to nat. (increasing f)
 469 \to \forall n:nat. n \le (f n).
 470 intros.elim n.
 471 apply le_O_n.
 472 apply (trans_le ? (S (f n1))).
 473 apply le_S_S.apply H1.
 474 simplify in H. unfold increasing in H.unfold lt in H.apply H.
 475 qed.
 476
 477 theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
 478 \to \forall m:nat. \exists i. m \le (f i).
 479 intros.elim m.
 480 apply (ex_intro ? ? O).apply le_O_n.
 481 elim H1.
 482 apply (ex_intro ? ? (S a)).
 483 apply (trans_le ? (S (f a))).
 484 apply le_S_S.assumption.
 485 simplify in H.unfold increasing in H.unfold lt in H.
 486 apply H.
 487 qed.
 488
 489 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
 490 \to \forall m:nat. (f O) \le m \to
 491 \exists i. (f i) \le m \land m <(f (S i)).
 492 intros.elim H1.
 493 apply (ex_intro ? ? O).
 494 split.apply le_n.apply H.
 495 elim H3.elim H4.
 496 cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
 497 elim Hcut.
 498 apply (ex_intro ? ? a).
 499 split.apply le_S. assumption.assumption.
 500 apply (ex_intro ? ? (S a)).
 501 split.rewrite < H7.apply le_n.
 502 rewrite > H7.
 503 apply H.
 504 apply le_to_or_lt_eq.apply H6.
 505 qed.
 506 *)
 507
 508 (*********************** monotonicity ***************************)
 509 theorem monotonic_le_plus_r:
 510 ∀n:nat.monotonic nat le (λm.n + m).
 511 #n #a #b (elim n) normalize //
 512 #m #H #leab @le_S_S /2/ qed.
 513
 514 (*
 515 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 516 ≝ monotonic_le_plus_r. *)
 517
 518 theorem monotonic_le_plus_l:
 519 ∀m:nat.monotonic nat le (λn.n + m).
 520 /2/ qed.
 521
 522 (*
 523 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 524 \def monotonic_le_plus_l. *)
 525
 526 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2
 527 → n1 + m1 ≤ n2 + m2.
 528 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
 529 /2/ qed.
 530
 531 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 532 /2/ qed.
 533
 534 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
 535 /2/ qed.
 536
 537 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
 538 /2/ qed.
 539
 540 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
 541 /2/ qed.
 542
 543 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
 544 // qed.
 545
 546 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
 547 #a (elim a) normalize /3/ qed.
 548
 549 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
 550 /2/ qed.
 551
 552 (* plus & lt *)
 553
 554 theorem monotonic_lt_plus_r:
 555 ∀n:nat.monotonic nat lt (λm.n+m).
 556 /2/ qed.
 557
 558 (*
 559 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
 560 monotonic_lt_plus_r. *)
 561
 562 theorem monotonic_lt_plus_l:
 563 ∀n:nat.monotonic nat lt (λm.m+n).
 564 /2/ qed.
 565
 566 (*
 567 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
 568 monotonic_lt_plus_l. *)
 569
 570 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
 571 #n #m #p #q #ltnm #ltpq
 572 @(transitive_lt ? (n+q))/2/ qed.
 573
 574 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
 575 /2/ qed.
 576
 577 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
 578 /2/ qed.
 579
 580 (*
 581 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
 582 a ≤ c → b < d → a + b < c+d.
 583 (* bello /2/ un po' lento *)
 584 #a #b #c #d #leac #lebd
 585 normalize napplyS le_plus // qed.
 586 *)
 587
 588 (* times *)
 589 theorem monotonic_le_times_r:
 590 ∀n:nat.monotonic nat le (λm. n * m).
 591 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
 592 #a #lea @le_plus //
 593 qed.
 594
 595 (*
 596 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
 597 \def monotonic_le_times_r. *)
 598
 599 (*
 600 theorem monotonic_le_times_l:
 601 ∀m:nat.monotonic nat le (λn.n*m).
 602 /2/ qed.
 603 *)
 604
 605 (*
 606 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
 607 \def monotonic_le_times_l. *)
 608
 609 theorem le_times: ∀n1,n2,m1,m2:nat.
 610 n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
 611 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
 612 qed.
 613
 614 (* interessante *)
 615 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
 616 #n #m #H /2/ qed.
 617
 618 theorem le_times_to_le:
 619 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
 620 #a @nat_elim2 normalize
 621   [//
 622   |#n #H1 #H2
 623      @(transitive_le ? (a*S n)) /2/
 624   |#n #m #H #lta #le
 625      @le_S_S @H /2/
 626   ]
 627 qed.
 628
 629 (*
 630 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
 631 #n #m #posm #lenm  (* interessante *)
 632 applyS (le_plus n m) // qed. *)
 633
 634 (* times & lt *)
 635 (*
 636 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
 637 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
 638 qed. *)
 639
 640 (*
 641 theorem lt_times_eq_O: \forall a,b:nat.
 642 O < a → a * b = O → b = O.
 643 intros.
 644 apply (nat_case1 b)
 645 [ intros.
 646   reflexivity
 647 | intros.
 648   rewrite > H2 in H1.
 649   rewrite > (S_pred a) in H1
 650   [ apply False_ind.
 651     apply (eq_to_not_lt O ((S (pred a))*(S m)))
 652     [ apply sym_eq.
 653       assumption
 654     | apply lt_O_times_S_S
 655     ]
 656   | assumption
 657   ]
 658 ]
 659 qed.
 660
 661 theorem O_lt_times_to_O_lt: \forall a,c:nat.
 662 O \lt (a * c) \to O \lt a.
 663 intros.
 664 apply (nat_case1 a)
 665 [ intros.
 666   rewrite > H1 in H.
 667   simplify in H.
 668   assumption
 669 | intros.
 670   apply lt_O_S
 671 ]
 672 qed.
 673
 674 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 675 intros.
 676 elim (le_to_or_lt_eq O ? (le_O_n m))
 677   [assumption
 678   |apply False_ind.
 679    rewrite < H1 in H.
 680    rewrite < times_n_O in H.
 681    apply (not_le_Sn_O ? H)
 682   ]
 683 qed. *)
 684
 685 (*
 686 theorem monotonic_lt_times_r:
 687 ∀n:nat.monotonic nat lt (λm.(S n)*m).
 688 /2/
 689 simplify.
 690 intros.elim n.
 691 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 692 apply lt_plus.assumption.assumption.
 693 qed. *)
 694
 695 theorem monotonic_lt_times_l:
 696   ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
 697 #c #posc #n #m #ltnm
 698 (elim ltnm) normalize
 699   [/2/
 700   |#a #_ #lt1 @(transitive_le … lt1) //
 701   ]
 702 qed.
 703
 704 theorem monotonic_lt_times_r:
 705   ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
 706 /2/ qed.
 707
 708 theorem lt_to_le_to_lt_times:
 709 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
 710 #n #m #p #q #ltnm #lepq #posq
 711 @(le_to_lt_to_lt ? (n*q))
 712   [@monotonic_le_times_r //
 713   |@monotonic_lt_times_l //
 714   ]
 715 qed.
 716
 717 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
 718 #n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
 719 qed.
 720
 721 theorem lt_times_n_to_lt_l:
 722 ∀n,p,q:nat. p*n < q*n → p < q.
 723 #n #p #q #Hlt (elim (decidable_lt p q)) //
 724 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
 725 applyS monotonic_le_times_r /2/
 726 qed.
 727
 728 theorem lt_times_n_to_lt_r:
 729 ∀n,p,q:nat. n*p < n*q → p < q.
 730 /2/ qed.
 731
 732 (*
 733 theorem nat_compare_times_l : \forall n,p,q:nat.
 734 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 735 intros.apply nat_compare_elim.intro.
 736 apply nat_compare_elim.
 737 intro.reflexivity.
 738 intro.absurd (p=q).
 739 apply (inj_times_r n).assumption.
 740 apply lt_to_not_eq. assumption.
 741 intro.absurd (q<p).
 742 apply (lt_times_to_lt_r n).assumption.
 743 apply le_to_not_lt.apply lt_to_le.assumption.
 744 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
 745 intro.apply nat_compare_elim.intro.
 746 absurd (p<q).
 747 apply (lt_times_to_lt_r n).assumption.
 748 apply le_to_not_lt.apply lt_to_le.assumption.
 749 intro.absurd (q=p).
 750 symmetry.
 751 apply (inj_times_r n).assumption.
 752 apply lt_to_not_eq.assumption.
 753 intro.reflexivity.
 754 qed. *)
 755
 756 (* times and plus
 757 theorem lt_times_plus_times: \forall a,b,n,m:nat.
 758 a < n \to b < m \to a*m + b < n*m.
 759 intros 3.
 760 apply (nat_case n)
 761   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 762   |intros.simplify.
 763    rewrite < sym_plus.
 764    unfold.
 765    change with (S b+a*m1 \leq m1+m*m1).
 766    apply le_plus
 767     [assumption
 768     |apply le_times
 769       [apply le_S_S_to_le.assumption
 770       |apply le_n
 771       ]
 772     ]
 773   ]
 774 qed. *)
 775
 776 (************************** minus ******************************)
 777
 778 let rec minus n m ≝
 779  match n with
 780  [ O ⇒ O
 781  | S p ⇒
 782         match m with
 783           [ O ⇒ S p
 784     | S q ⇒ minus p q ]].
 785
 786 interpretation "natural minus" 'minus x y = (minus x y).
 787
 788 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
 789 // qed.
 790
 791 theorem minus_O_n: ∀n:nat.O=O-n.
 792 #n (cases n) // qed.
 793
 794 theorem minus_n_O: ∀n:nat.n=n-O.
 795 #n (cases n) // qed.
 796
 797 theorem minus_n_n: ∀n:nat.O=n-n.
 798 #n (elim n) // qed.
 799
 800 theorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
 801 #n (elim n) normalize // qed.
 802
 803 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
 804 (* qualcosa da capire qui
 805 #n #m #lenm nelim lenm napplyS refl_eq. *)
 806 @nat_elim2
 807   [//
 808   |#n #abs @False_ind /2/
 809   |#n #m #Hind #c applyS Hind /2/
 810   ]
 811 qed.
 812
 813 (*
 814 theorem not_eq_to_le_to_le_minus:
 815   ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
 816 #n * #m (cases m// #m normalize
 817 #H #H1 napply le_S_S_to_le
 818 napplyS (not_eq_to_le_to_lt n (S m) H H1)
 819 qed. *)
 820
 821 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 822 @nat_elim2 normalize // qed.
 823
 824 theorem plus_minus:
 825 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
 826 @nat_elim2
 827   [//
 828   |#n #p #abs @False_ind /2/
 829   |normalize/3/
 830   ]
 831 qed.
 832
 833 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
 834 /2/ qed.
 835
 836 theorem plus_minus_m_m: ∀n,m:nat.
 837   m ≤ n → n = (n-m)+m.
 838 #n #m #lemn @sym_eq /2/ qed.
 839
 840 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
 841 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/
 842 qed.
 843
 844 theorem minus_to_plus :∀n,m,p:nat.
 845   m ≤ n → n-m = p → n = m+p.
 846 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
 847 qed.
 848
 849 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
 850 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
 851 qed.
 852
 853 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m →
 854 pred n - pred m = n - m.
 855 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 856 qed.
 857
 858
 859 (*
 860
 861 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 862 intros.elim H.elim (minus_Sn_n n).apply le_n.
 863 rewrite > minus_Sn_m.
 864 apply le_S.assumption.
 865 apply lt_to_le.assumption.
 866 qed.
 867
 868 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
 869 intros.
 870 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
 871 intro.elim n1.simplify.apply le_n_Sn.
 872 simplify.rewrite < minus_n_O.apply le_n.
 873 intros.simplify.apply le_n_Sn.
 874 intros.simplify.apply H.
 875 qed.
 876
 877 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
 878 intros 3.intro.
 879 (* autobatch *)
 880 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
 881 apply (trans_le (m-n) (S (m-(S n))) p).
 882 apply minus_le_S_minus_S.
 883 assumption.
 884 qed.
 885
 886 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 887 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
 888 intros.rewrite < minus_n_O.apply le_n.
 889 intros.simplify.apply le_n.
 890 intros.simplify.apply le_S.assumption.
 891 qed.
 892
 893 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 894 intros.apply (lt_O_n_elim n H).intro.
 895 apply (lt_O_n_elim m H1).intro.
 896 simplify.unfold lt.apply le_S_S.apply le_minus_m.
 897 qed.
 898
 899 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 900 intros 2.
 901 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
 902 intros.apply le_O_n.
 903 simplify.intros. assumption.
 904 simplify.intros.apply le_S_S.apply H.assumption.
 905 qed.
 906 *)
 907
 908 (* monotonicity and galois *)
 909
 910 theorem monotonic_le_minus_l:
 911 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
 912 @nat_elim2 #p #q
 913   [#lePO @(le_n_O_elim ? lePO) //
 914   |//
 915   |#Hind #n (cases n) // #a #leSS @Hind /2/
 916   ]
 917 qed.
 918
 919 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
 920 #n #m #p #lep @transitive_le
 921   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
 922 qed.
 923
 924 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
 925 #n #m #p #lep /2/ qed.
 926
 927 theorem monotonic_le_minus_r:
 928 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
 929 #p #q #n #lepq @le_plus_to_minus
 930 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
 931 qed.
 932
 933 theorem eq_minus_O: ∀n,m:nat.
 934   n ≤ m → n-m = O.
 935 #n #m #lenm @(le_n_O_elim (n-m)) /2/
 936 qed.
 937
 938 theorem distributive_times_minus: distributive ? times minus.
 939 #a #b #c
 940 (cases (decidable_lt b c)) #Hbc
 941  [> eq_minus_O /2/ >eq_minus_O //
 942   @monotonic_le_times_r /2/
 943  |@sym_eq (applyS plus_to_minus) <distributive_times_plus
 944   @eq_f (applyS plus_minus_m_m) /2/
 945 qed.
 946
 947 theorem minus_minus: ∀n,m,p. n-m-p = n -(m+p).
 948 #n #m #p
 949 cases (decidable_le (m+p) n) #Hlt
 950   [@plus_to_minus @plus_to_minus <associative_plus
 951    @minus_to_plus //
 952   |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
 953    #H >eq_minus_O /2/ >eq_minus_O //
 954   ]
 955 qed.
 956
 957 (*********************** boolean arithmetics ********************)
 958 include "basics/bool.ma".
 959
 960 let rec eqb n m ≝
 961 match n with
 962   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
 963   | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
 964   ].
 965
 966 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
 967 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
 968 @nat_elim2
 969   [#n (cases n) normalize /3/
 970   |normalize /3/
 971   |normalize /4/
 972   ]
 973 qed.
 974
 975 theorem eqb_n_n: ∀n. eqb n n = true.
 976 #n (elim n) normalize // qed.
 977
 978 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
 979 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
 980
 981 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
 982 #n #m @(eqb_elim n m) /2/ qed.
 983
 984 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
 985 // qed.
 986
 987 theorem not_eq_to_eqb_false: ∀n,m:nat.
 988   n ≠  m → eqb n m = false.
 989 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
 990
 991 let rec leb n m ≝
 992 match n with
 993     [ O ⇒ true
 994     | (S p) ⇒
 995         match m with
 996         [ O ⇒ false
 997               | (S q) ⇒ leb p q]].
 998
 999 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
1000 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
1001 @nat_elim2 normalize
1002   [/2/
1003   |/3/
1004   |#n #m #Hind #P #Pt #Pf @Hind
1005     [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
1006   ]
1007 qed.
1008
1009 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
1010 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1011
1012 theorem leb_false_to_not_le:∀n,m.
1013   leb n m = false → n ≰ m.
1014 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
1015
1016 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
1017 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1018
1019 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
1020 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
1021
1022 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
1023 /3/ qed.
1024
1025 (* serve anche ltb?
1026 ndefinition ltb ≝λn,m. leb (S n) m.
1027
1028 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
1029 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
1030 #n #m #P #Hlt #Hnlt
1031 napply leb_elim /3/ qed.
1032
1033 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
1034 #n #m #Hltb napply leb_true_to_le nassumption
1035 qed.
1036
1037 theorem ltb_false_to_not_lt:∀n,m.
1038   ltb n m = false → n ≮ m.
1039 #n #m #Hltb napply leb_false_to_not_le nassumption
1040 qed.
1041
1042 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
1043 #n #m #Hltb napply le_to_leb_true nassumption
1044 qed.
1045
1046 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
1047 #n #m #Hltb napply lt_to_leb_false /2/
1048 qed. *)
1049
1050 (* min e max *)
1051 definition min: nat →nat →nat ≝
1052 λn.λm. if_then_else ? (leb n m) n m.
1053
1054 definition max: nat →nat →nat ≝
1055 λn.λm. if_then_else ? (leb n m) m n.
1056
1057 lemma commutative_min: commutative ? min.
1058 #n #m normalize @leb_elim
1059   [@leb_elim normalize /2/
1060   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1061   ] qed.
1062
1063 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
1064 #i #n #m normalize @leb_elim normalize /2/ qed.
1065
1066 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
1067 /2/ qed.
1068
1069 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
1070 #i #n #m #lein #leim normalize (cases (leb n m))
1071 normalize // qed.
1072
1073 lemma commutative_max: commutative ? max.
1074 #n #m normalize @leb_elim
1075   [@leb_elim normalize /2/
1076   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
1077   ] qed.
1078
1079 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
1080 #i #n #m normalize @leb_elim normalize /2/ qed.
1081
1082 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
1083 /2/ qed.
1084
1085 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
1086 #i #n #m #leni #lemi normalize (cases (leb n m))
1087 normalize // qed.
1088