Changeset 351 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Dec 1, 2010, 4:30:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r350 r351 37 37 38 38 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). 39 (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 40 *) 39 40 notation "hvbox(n break ≲ m)" 41 non associative with precedence 47 42 for @{ 'less_than_or_equalb $n $m }. 43 44 interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m). 45 41 46 42 47 ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ … … 54 59 55 60 interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). 56 (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). 57 *) 61 62 notation "hvbox(n break ≳ m)" 63 non associative with precedence 47 64 for @{ 'greater_than_or_equalb $n $m }. 65 66 interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m). 67 58 68 59 69 (* Add Boolean versions. *) … … 236 246 (* ===================================== *) 237 247 238 naxiom plus_minus_inverse_left:248 (*naxiom plus_minus_inverse_left: 239 249 ∀m, n: Nat. 240 250 (m + n)  n = m. 241 251 *) 252 242 253 ntheorem less_than_or_equal_monotone: 243 254 ∀m, n: Nat. … … 250 261 nqed. 251 262 252 ntheorem succ_less_than_or_equal_injective:263 ntheorem less_than_or_equal_injective: 253 264 ∀m, n: Nat. 254 265 (S m) ≤ (S n) → m ≤ n. … … 259 270 nqed. 260 271 261 naxiom plus_minus_inverse_right:262 ∀m, n: Nat.263 (m  n) + n = m.264 265 272 ntheorem succ_less_than_injective: 266 273 ∀m, n: Nat. … … 279 286 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; 280 287 nqed. 288 281 289 282 290 (* ===================================== *) … … 294 302 nqed. 295 303 296 naxiom less_than_or_equal_injective:297 ∀m, n: Nat.298 S m ≤ S n → m ≤ n.299 300 304 (* 301 305 nlemma less_than_or_equal_zero_equal_zero: … … 548 552 nqed. 549 553 554 555 nlemma succ_injective: 556 ∀m, n: Nat. 557 S m = S n → m = n. 558 #m n H; 559 napply (match H return λy.λ_.m = match y with [Z ⇒ Z  S z ⇒ z] with 560 [refl ⇒ ? ]); 561 @; 562 nqed. 563 564 ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'. 565 //; 566 nqed. 567 568 ntheorem plus_minus_inverse_right: 569 ∀m, n: Nat. 570 n ≤ m → (m  n) + n = m. 571 #m; nelim m 572 [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1); 573 #K; ncases (K H3) 574  #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/; 575 #w; nrewrite < succ_plus; /4/. ##] 576 nqed. 577 550 578 (* 551 nlemma succ_injective:552 ∀m, n: Nat.553 S m = S n → m = n.554 #m n.555 nelim m.556 #H.557 ninversion H.558 #H.559 ndestruct560 579 561 580 nlemma plus_minus_associate: … … 578 597 #N H. 579 598 *) 599 600 ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n. 601 #m; nelim m; //; #y H1 z; ncases z; nnormalize 602 [ #H; ndestruct  /3/ ] 603 nqed. 604 605 ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n). 606 #m; nelim m; nnormalize 607 [ #n H; ndestruct  #y H1 z; ncases z; nnormalize 608 [ #H; ndestruct  /3/ ] /2/. 609 nqed. 610 611 ndefinition less_than_or_equal_b_elim: 612 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → 613 P (less_than_or_equal_b m n). 614 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); 615 nlapply (less_than_or_equal_b_complete m n); 616 ncases (less_than_or_equal_b m n); /3/. 617 nqed. 618 619 ndefinition greater_than_or_equal_b_elim: 620 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) → 621 P (greater_than_or_equal_b m n). 622 #m n; napply less_than_or_equal_b_elim; 623 nqed. 624 625 ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n. 626 #m; nelim m 627 [ #n; ncases n [ #H; nnormalize in H; ndestruct  #z H; /2/ ] 628 ## #y H z; ncases z [ nnormalize; #K; ndestruct  #o K; 629 napply less_than_or_equal_monotone; napply H; napply K ] 630 nqed. 631 632 ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n). 633 #m; nelim m 634 [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct 635  #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/. 636 nqed. 637 638 ndefinition less_than_b_elim: 639 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) → 640 P (less_than_b m n). 641 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n); 642 ncases (less_than_b m n); /3/. 643 nqed. 644 645 ndefinition greater_than_b_elim: 646 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) → 647 P (greater_than_b m n). 648 #m n; napply less_than_b_elim. 649 nqed.
Note: See TracChangeset
for help on using the changeset viewer.