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 (* Definitions **************************************************************)
  15
  16 (* natural numbers *)
  17
  18 inductive nat : Type[0] ≝
  19   | O : nat
  20   | S : nat → nat.
  21
  22 interpretation "Natural numbers" 'N = nat.
  23
  24 alias num (instance 0) = "natural number".
  25
  26 definition pred ≝
  27  λn. match n with [ O ⇒ O | S p ⇒ p].
  28
  29 definition not_zero: nat → Prop ≝
  30  λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
  31
  32 (* order relations *)
  33
  34 inductive le (n:nat) : nat → Prop ≝
  35   | le_n : le n n
  36   | le_S : ∀ m:nat. le n m → le n (S m).
  37
  38 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
  39
  40 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
  41
  42 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
  43
  44 interpretation "natural 'less than'" 'lt x y = (lt x y).
  45
  46 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
  47
  48 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
  49
  50 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
  51
  52 definition gt: nat → nat → Prop ≝ λn,m.m<n.
  53
  54 interpretation "natural 'greater than'" 'gt x y = (gt x y).
  55
  56 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
  57
  58 (* abstract properties *)
  59
  60 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
  61
  62 (* arithmetic operations *)
  63
  64 let rec plus n m ≝
  65  match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
  66
  67 interpretation "natural plus" 'plus x y = (plus x y).
  68
  69 let rec times n m ≝
  70  match n with [ O ⇒ 0 | S p ⇒ m + (times p m) ].
  71
  72 interpretation "natural times" 'times x y = (times x y).
  73
  74 let rec minus n m ≝
  75  match n with
  76  [ O ⇒ O
  77  | S p ⇒
  78         match m with
  79           [ O ⇒ S p
  80     | S q ⇒ minus p q ]].
  81
  82 interpretation "natural minus" 'minus x y = (minus x y).
  83
  84 (* Generic conclusion ******************************************************)
  85
  86 theorem nat_case:
  87  ∀n:nat.∀P:nat → Prop.
  88   (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
  89 #n #P (elim n) /2/ qed.
  90
  91 theorem nat_elim2 :
  92  ∀R:nat → nat → Prop.
  93   (∀n:nat. R O n)
  94   → (∀n:nat. R (S n) O)
  95   → (∀n,m:nat. R n m → R (S n) (S m))
  96   → ∀n,m:nat. R n m.
  97 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
  98
  99 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
 100 /2/ qed.
 101
 102 (* Equalities ***************************************************************)
 103
 104 theorem pred_Sn : ∀n. n = pred (S n).
 105 // qed.
 106
 107 theorem injective_S : injective nat nat S.
 108 // qed.
 109
 110 theorem S_pred: ∀n. 0 < n → S(pred n) = n.
 111 #n #posn (cases posn) //
 112 qed.
 113
 114 theorem plus_O_n: ∀n:nat. n = 0 + n.
 115 // qed.
 116
 117 theorem plus_n_O: ∀n:nat. n = n + 0.
 118 #n (elim n) normalize // qed.
 119
 120 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
 121 #n (elim n) normalize // qed.
 122
 123 theorem commutative_plus: commutative ? plus.
 124 #n (elim n) normalize // qed.
 125
 126 theorem associative_plus : associative nat plus.
 127 #n (elim n) normalize // qed.
 128
 129 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
 130 // qed.
 131
 132 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 133 #n (elim n) normalize /3/ qed.
 134
 135 theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n).
 136 /2/ qed.
 137
 138 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
 139 // qed.
 140
 141 theorem times_O_n: ∀n:nat. 0 = 0 * n.
 142 // qed.
 143
 144 theorem times_n_O: ∀n:nat. 0 = n * 0.
 145 #n (elim n) // qed.
 146
 147 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
 148 #n (elim n) normalize // qed.
 149
 150 theorem commutative_times : commutative nat times.
 151 #n (elim n) normalize // qed.
 152
 153 theorem distributive_times_plus : distributive nat times plus.
 154 #n (elim n) normalize // qed.
 155
 156 theorem distributive_times_plus_r :
 157   ∀a,b,c:nat. (b+c)*a = b*a + c*a.
 158 // qed.
 159
 160 theorem associative_times: associative nat times.
 161 #n (elim n) normalize // qed.
 162
 163 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 164 // qed.
 165
 166 theorem times_n_1 : ∀n:nat. n = n * 1.
 167 // qed.
 168
 169 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
 170 // qed.
 171
 172 theorem minus_O_n: ∀n:nat.0=0-n.
 173 #n (cases n) // qed.
 174
 175 theorem minus_n_O: ∀n:nat.n=n-0.
 176 #n (cases n) // qed.
 177
 178 theorem minus_n_n: ∀n:nat.0=n-n.
 179 #n (elim n) // qed.
 180
 181 theorem minus_Sn_n: ∀n:nat. S 0 = (S n)-n.
 182 #n (elim n) normalize // qed.
 183
 184 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 185 @nat_elim2 normalize // qed.
 186
 187 lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
 188 // qed.
 189
 190 lemma discr_plus_xy_minus_xz: ∀x,z,y. x + y = x - z → y = 0.
 191 #x elim x -x // #x #IHx * normalize
 192 [ #y #H @(IHx 0) <minus_n_O /2 width=1/
 193 | #z #y >plus_n_Sm #H lapply (IHx … H) -x -z #H destruct
 194 ]
 195 qed-.
 196
 197 (* Negated equalities *******************************************************)
 198
 199 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
 200 /2/ qed.
 201
 202 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
 203 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
 204
 205 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
 206 #n (elim n) /2/ qed.
 207
 208 (* Atomic conclusion *******************************************************)
 209
 210 (* not_zero *)
 211
 212 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
 213 #n #m #Hlt (elim Hlt) // qed.
 214
 215 (* le *)
 216
 217 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 218 #n #m #lenm (elim lenm) /2/ qed.
 219
 220 theorem le_O_n : ∀n:nat. 0 ≤ n.
 221 #n (elim n) /2/ qed.
 222
 223 theorem le_n_Sn : ∀n:nat. n ≤ S n.
 224 /2/ qed.
 225
 226 theorem transitive_le : transitive nat le.
 227 #a #b #c #leab #lebc (elim lebc) /2/
 228 qed.
 229
 230 theorem le_pred_n : ∀n:nat. pred n ≤ n.
 231 #n (elim n) // qed.
 232
 233 theorem monotonic_pred: monotonic ? le pred.
 234 #n #m #lenm (elim lenm) /2/ qed.
 235
 236 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 237 (* demo *)
 238 /2/ qed-.
 239
 240 theorem monotonic_le_plus_r:
 241 ∀n:nat.monotonic nat le (λm.n + m).
 242 #n #a #b (elim n) normalize //
 243 #m #H #leab @le_S_S /2/ qed.
 244
 245 theorem monotonic_le_plus_l:
 246 ∀m:nat.monotonic nat le (λn.n + m).
 247 /2/ qed.
 248
 249 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2
 250 → n1 + m1 ≤ n2 + m2.
 251 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
 252 /2/ qed.
 253
 254 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 255 /2/ qed.
 256
 257 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
 258 /2/ qed.
 259
 260 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
 261 /2/ qed.
 262
 263 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
 264 /2/ qed.
 265
 266 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
 267 // qed-.
 268
 269 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
 270 #a (elim a) normalize /3/ qed.
 271
 272 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
 273 /2/ qed-.
 274
 275 theorem monotonic_le_times_r:
 276 ∀n:nat.monotonic nat le (λm. n * m).
 277 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
 278 #a #lea @le_plus //
 279 qed.
 280
 281 theorem le_times: ∀n1,n2,m1,m2:nat.
 282 n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
 283 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
 284 qed.
 285
 286 (* interessante *)
 287 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
 288 #n #m #H /2/ qed.
 289
 290 theorem le_times_to_le:
 291 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
 292 #a @nat_elim2 normalize
 293   [//
 294   |#n #H1 #H2
 295      @(transitive_le ? (a*S n)) /2/
 296   |#n #m #H #lta #le
 297      @le_S_S @H /2/
 298   ]
 299 qed-.
 300
 301 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
 302 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/
 303 qed.
 304
 305 theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
 306 #a #b #c #H @(le_plus_to_le_r … b) /2/
 307 qed.
 308
 309 lemma lt_to_le: ∀x,y. x < y → x ≤ y.
 310 /2 width=2/ qed.
 311
 312 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
 313 // qed-.
 314
 315 lemma le_x_times_x: ∀x. x ≤ x * x.
 316 #x elim x -x //
 317 qed.
 318
 319 (* lt *)
 320
 321 theorem transitive_lt: transitive nat lt.
 322 #a #b #c #ltab #ltbc (elim ltbc) /2/
 323 qed.
 324
 325 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
 326 #n #m #p #H #H1 (elim H1) /2/ qed.
 327
 328 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
 329 #n #m #p #H (elim H) /3/ qed.
 330
 331 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
 332 /2/ qed.
 333
 334 theorem ltn_to_ltO: ∀n,m:nat. n < m → 0 < m.
 335 /2/ qed.
 336
 337 theorem lt_O_S : ∀n:nat. O < S n.
 338 /2/ qed.
 339
 340 theorem monotonic_lt_plus_r:
 341 ∀n:nat.monotonic nat lt (λm.n+m).
 342 /2/ qed.
 343
 344 theorem monotonic_lt_plus_l:
 345 ∀n:nat.monotonic nat lt (λm.m+n).
 346 /2/ qed.
 347
 348 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
 349 #n #m #p #q #ltnm #ltpq
 350 @(transitive_lt ? (n+q))/2/ qed.
 351
 352 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
 353 /2/ qed.
 354
 355 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
 356 /2/ qed-.
 357
 358 theorem increasing_to_monotonic: ∀f:nat → nat.
 359   increasing f → monotonic nat lt f.
 360 #f #incr #n #m #ltnm (elim ltnm) /2/
 361 qed.
 362
 363 theorem monotonic_lt_times_r:
 364   ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
 365 #c #posc #n #m #ltnm
 366 (elim ltnm) normalize
 367   [/2/
 368   |#a #_ #lt1 @(transitive_le … lt1) //
 369   ]
 370 qed.
 371
 372 theorem monotonic_lt_times_l:
 373   ∀c:nat. 0 < c → monotonic nat lt (λt.(t*c)).
 374 /2/
 375 qed.
 376
 377 theorem lt_to_le_to_lt_times:
 378 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
 379 #n #m #p #q #ltnm #lepq #posq
 380 @(le_to_lt_to_lt ? (n*q))
 381   [@monotonic_le_times_r //
 382   |@monotonic_lt_times_l //
 383   ]
 384 qed.
 385
 386 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
 387 #n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
 388 qed.
 389
 390 theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
 391 #a #b #c #H @le_plus_to_minus_r //
 392 qed.
 393
 394 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
 395 /2 width=1/ qed.
 396
 397 theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
 398 (* demo *)
 399 /2/ qed-.
 400
 401 (* not le, lt *)
 402
 403 theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
 404 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
 405
 406 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
 407 /3/ qed.
 408
 409 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
 410 /3/ qed.
 411
 412 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
 413 #n (elim n) /2/ qed.
 414
 415 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
 416 #n #m #Hltnm (elim Hltnm) /3/ qed.
 417
 418 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
 419 @nat_elim2 #n
 420  [#abs @False_ind /2/
 421  |/2/
 422  |#m #Hind #HnotleSS @le_S_S @Hind /2/
 423  ]
 424 qed.
 425
 426 (* not lt, le *)
 427
 428 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
 429 #n #m #H @le_S_S_to_le @not_le_to_lt /2/ qed.
 430
 431 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
 432 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
 433
 434 (* Compound conclusion ******************************************************)
 435
 436 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
 437 @nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
 438 qed.
 439
 440 theorem decidable_le: ∀n,m. decidable (n≤m).
 441 @nat_elim2 #n /2/ #m * /3/ qed.
 442
 443 theorem decidable_lt: ∀n,m. decidable (n < m).
 444 #n #m @decidable_le  qed.
 445
 446 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
 447 #n #m #lenm (elim lenm) /3/ qed.
 448
 449 theorem eq_or_gt: ∀n. 0 = n ∨ 0 < n.
 450 #n elim (le_to_or_lt_eq 0 n ?) // /2 width=1/
 451 qed-.
 452
 453 theorem increasing_to_le2: ∀f:nat → nat. increasing f →
 454   ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
 455 #f #incr #m #lem (elim lem)
 456   [@(ex_intro ? ? O) /2/
 457   |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
 458     [@(ex_intro ? ? a) % /2/
 459     |@(ex_intro ? ? (S a)) % //
 460     ]
 461   ]
 462 qed.
 463
 464 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
 465 /3/ qed-.
 466
 467 lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
 468 /3/ qed-.
 469
 470 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 471 #m #n elim (decidable_lt m n) /2/ /3/
 472 qed-.
 473
 474 lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
 475 #m #n elim (decidable_le m n) /2/ /4/
 476 qed-.
 477
 478 lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z.
 479 #x #y #H elim H -y /2 width=3 by ex2_intro/
 480 #y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/
 481 qed-.
 482
 483 (* More general conclusion **************************************************)
 484
 485 theorem nat_ind_plus: ∀R:predicate nat.
 486                       R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
 487 /3 by nat_ind/ qed-.
 488
 489 theorem lt_O_n_elim: ∀n:nat. 0 < n →
 490   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
 491 #n (elim n) // #abs @False_ind /2/ @absurd
 492 qed.
 493
 494 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
 495 #n (cases n) // #a #abs @False_ind /2/ qed.
 496
 497 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 498 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
 499 #n #m #Hle #P (elim Hle) /3/ qed.
 500
 501 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
 502 (∀m.(∀p. p < m → P p) → P m) → P n.
 503 #n #P #H
 504 cut (∀q:nat. q ≤ n → P q) /2/
 505 (elim n)
 506  [#q #HleO (* applica male *)
 507     @(le_n_O_elim ? HleO)
 508     @H #p #ltpO @False_ind /2/ (* 3 *)
 509  |#p #Hind #q #HleS
 510     @H #a #lta @Hind @le_S_S_to_le /2/
 511  ]
 512 qed.
 513
 514 fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
 515                 (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
 516                 ∀n,a. f a = n → P a.
 517 #A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
 518 qed-.
 519
 520 lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
 521              (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
 522 #A #f #P #H #a
 523 @(f_ind_aux … H) -H [2: // | skip ]
 524 qed-.
 525
 526 fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
 527                  (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
 528                  ∀n,a1,a2. f a1 a2 = n → P a1 a2.
 529 #A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
 530 qed-.
 531
 532 lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
 533               (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
 534               ∀a1,a2. P a1 a2.
 535 #A1 #A2 #f #P #H #a1 #a2
 536 @(f2_ind_aux … H) -H [2: // | skip ]
 537 qed-.
 538
 539 fact f3_ind_aux: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
 540                  (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
 541                  ∀n,a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3.
 542 #A1 #A2 #A3 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
 543 qed-.
 544
 545 lemma f3_ind: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
 546               (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
 547               ∀a1,a2,a3. P a1 a2 a3.
 548 #A1 #A2 #A3 #f #P #H #a1 #a2 #a3
 549 @(f3_ind_aux … H) -H [2: // | skip ]
 550 qed-.
 551
 552 (* More negated equalities **************************************************)
 553
 554 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
 555 #n #m #H @not_to_not /2/ qed.
 556
 557 (* More equalities **********************************************************)
 558
 559 theorem le_n_O_to_eq : ∀n:nat. n ≤ 0 → 0=n.
 560 #n (cases n) // #a  #abs @False_ind /2/ qed.
 561
 562 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
 563 @nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
 564 qed.
 565
 566 theorem increasing_to_injective: ∀f:nat → nat.
 567   increasing f → injective nat nat f.
 568 #f #incr #n #m cases(decidable_le n m)
 569   [#lenm cases(le_to_or_lt_eq … lenm) //
 570    #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
 571    @increasing_to_monotonic //
 572   |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
 573    @lt_to_not_eq @increasing_to_monotonic /2/
 574   ]
 575 qed.
 576
 577 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
 578 (* qualcosa da capire qui
 579 #n #m #lenm nelim lenm napplyS refl_eq. *)
 580 @nat_elim2
 581   [//
 582   |#n #abs @False_ind /2/
 583   |#n #m #Hind #c applyS Hind /2/
 584   ]
 585 qed.
 586
 587 theorem plus_minus:
 588 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
 589 @nat_elim2
 590   [//
 591   |#n #p #abs @False_ind /2/
 592   |normalize/3/
 593   ]
 594 qed.
 595
 596 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
 597 /2/ qed.
 598
 599 theorem plus_minus_m_m: ∀n,m:nat.
 600   m ≤ n → n = (n-m)+m.
 601 #n #m #lemn @sym_eq /2/ qed.
 602
 603 theorem minus_to_plus :∀n,m,p:nat.
 604   m ≤ n → n-m = p → n = m+p.
 605 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
 606 qed.
 607
 608 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
 609 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
 610 qed.
 611
 612 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m →
 613 pred n - pred m = n - m.
 614 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 615 qed.
 616
 617 theorem plus_minus_associative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
 618 /2 by plus_minus/ qed.
 619
 620 (* More atomic conclusion ***************************************************)
 621
 622 (* le *)
 623
 624 theorem le_n_fn: ∀f:nat → nat.
 625   increasing f → ∀n:nat. n ≤ f n.
 626 #f #incr #n (elim n) /2/
 627 qed-.
 628
 629 theorem monotonic_le_minus_l:
 630 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
 631 @nat_elim2 #p #q
 632   [#lePO @(le_n_O_elim ? lePO) //
 633   |//
 634   |#Hind #n (cases n) // #a #leSS @Hind /2/
 635   ]
 636 qed.
 637
 638 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
 639 #n #m #p #lep @transitive_le
 640   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
 641 qed.
 642
 643 theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
 644 #a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
 645 qed.
 646
 647 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
 648 #n #m #p #lep /2/ qed.
 649
 650 theorem monotonic_le_minus_r:
 651 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
 652 #p #q #n #lepq @le_plus_to_minus
 653 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
 654 qed.
 655
 656 theorem increasing_to_le: ∀f:nat → nat.
 657   increasing f → ∀m:nat.∃i.m ≤ f i.
 658 #f #incr #m (elim m) /2/#n * #a #lenfa
 659 @(ex_intro ?? (S a)) /2/
 660 qed.
 661
 662 (* thus is le_plus
 663 lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
 664 #x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
 665 *)
 666
 667 lemma minus_le: ∀x,y. x - y ≤ x.
 668 /2 width=1/ qed.
 669
 670 (* lt *)
 671
 672 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 673 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
 674 #Heq @not_le_to_lt /2/ qed-.
 675
 676 theorem lt_times_n_to_lt_l:
 677 ∀n,p,q:nat. p*n < q*n → p < q.
 678 #n #p #q #Hlt (elim (decidable_lt p q)) //
 679 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
 680 applyS monotonic_le_times_r /2/
 681 qed.
 682
 683 theorem lt_times_n_to_lt_r:
 684 ∀n,p,q:nat. n*p < n*q → p < q.
 685 /2/ qed-.
 686
 687 theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
 688 #a #b #c #H @not_le_to_lt
 689 @(not_to_not … (lt_to_not_le …H)) /2/
 690 qed.
 691
 692 theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
 693 #a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
 694 @lt_to_not_le //
 695 qed.
 696
 697 theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
 698 #n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
 699 qed.
 700
 701 theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 702 #p #q #n #H1 #H2
 703 @lt_plus_to_minus_r <plus_minus_m_m //
 704 qed.
 705
 706 (* More compound conclusion *************************************************)
 707
 708 lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
 709 * /2 width=1/ #x * /2 width=1/ #y normalize #H
 710 lapply (minus_le x y) <H -H #H
 711 elim (not_le_Sn_n x) #H0 elim (H0 ?) //
 712 qed-.
 713
 714 lemma plus_le_0: ∀x,y. x + y ≤ 0 → x = 0 ∧ y = 0.
 715 #x #y #H elim (le_inv_plus_l … H) -H #H1 #H2 /3 width=1/
 716 qed-.
 717
 718 (* Still more equalities ****************************************************)
 719
 720 theorem eq_minus_O: ∀n,m:nat.
 721   n ≤ m → n-m = O.
 722 #n #m #lenm @(le_n_O_elim (n-m)) /2/
 723 qed.
 724
 725 theorem distributive_times_minus: distributive ? times minus.
 726 #a #b #c
 727 (cases (decidable_lt b c)) #Hbc
 728  [> eq_minus_O [2:/2/] >eq_minus_O //
 729   @monotonic_le_times_r /2/
 730  |@sym_eq (applyS plus_to_minus) <distributive_times_plus
 731   @eq_f (applyS plus_minus_m_m) /2/
 732 qed.
 733
 734 theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
 735 #n #m #p
 736 cases (decidable_le (m+p) n) #Hlt
 737   [@plus_to_minus @plus_to_minus <associative_plus
 738    @minus_to_plus //
 739   |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
 740    #H >eq_minus_O /2/ (* >eq_minus_O // *)
 741   ]
 742 qed.
 743
 744 theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
 745   p+(n-m) = n-(m-p).
 746 #n #m #p #lepm #lemn
 747 @sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
 748 <commutative_plus <plus_minus_m_m //
 749 qed.
 750
 751 lemma minus_minus_associative: ∀x,y,z. z ≤ y → y ≤ x → x - (y - z) = x - y + z.
 752 /2 width=1 by minus_minus/ qed-.
 753
 754 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
 755 /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
 756
 757 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 758 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
 759 qed.
 760
 761 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 762 /2 width=1/ qed.
 763
 764 lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
 765 // qed.
 766
 767 lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
 768 // qed.
 769
 770 lemma minus_plus_minus_l: ∀x,y,z. y ≤ z → (z + x) - (z - y) = x + y.
 771 /2 width=1 by minus_minus_associative/ qed-.
 772
 773 (* Stilll more atomic conclusion ********************************************)
 774
 775 (* le *)
 776
 777 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
 778 #m1 #m2 #H #n1 #n2 >commutative_plus
 779 #H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
 780 #H #_ @(transitive_le … H) /2 width=1/
 781 qed-.
 782
 783 (*********************** boolean arithmetics ********************)
 784
 785 include "basics/bool.ma".
 786
 787 let rec eqb n m ≝
 788 match n with
 789   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
 790   | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
 791   ].
 792
 793 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
 794 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
 795 @nat_elim2
 796   [#n (cases n) normalize /3/
 797   |normalize /3/
 798   |normalize /4/
 799   ]
 800 qed.
 801
 802 theorem eqb_n_n: ∀n. eqb n n = true.
 803 #n (elim n) normalize // qed.
 804
 805 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
 806 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
 807
 808 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
 809 #n #m @(eqb_elim n m) /2/ qed.
 810
 811 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
 812 // qed.
 813
 814 theorem not_eq_to_eqb_false: ∀n,m:nat.
 815   n ≠  m → eqb n m = false.
 816 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
 817
 818 let rec leb n m ≝
 819 match n with
 820     [ O ⇒ true
 821     | (S p) ⇒
 822         match m with
 823         [ O ⇒ false
 824               | (S q) ⇒ leb p q]].
 825
 826 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
 827 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
 828 @nat_elim2 normalize
 829   [/2/
 830   |/3/
 831   |#n #m #Hind #P #Pt #Pf @Hind
 832     [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
 833   ]
 834 qed.
 835
 836 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
 837 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
 838
 839 theorem leb_false_to_not_le:∀n,m.
 840   leb n m = false → n ≰ m.
 841 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
 842
 843 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
 844 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
 845
 846 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
 847 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
 848
 849 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
 850 /3/ qed.
 851
 852 (* min e max *)
 853 definition min: nat →nat →nat ≝
 854 λn.λm. if leb n m then n else m.
 855
 856 definition max: nat →nat →nat ≝
 857 λn.λm. if leb n m then m else n.
 858
 859 lemma commutative_min: commutative ? min.
 860 #n #m normalize @leb_elim
 861   [@leb_elim normalize /2/
 862   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
 863   ] qed.
 864
 865 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
 866 #i #n #m normalize @leb_elim normalize /2/ qed.
 867
 868 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
 869 /2/ qed-.
 870
 871 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
 872 #i #n #m #lein #leim normalize (cases (leb n m))
 873 normalize // qed.
 874
 875 lemma commutative_max: commutative ? max.
 876 #n #m normalize @leb_elim
 877   [@leb_elim normalize /2/
 878   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
 879   ] qed.
 880
 881 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
 882 #i #n #m normalize @leb_elim normalize /2/ qed.
 883
 884 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 885 /2/ qed-.
 886
 887 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 888 #i #n #m #leni #lemi normalize (cases (leb n m))
 889 normalize // qed.