Changeset 14 for C-semantics/extralib.ma
- Timestamp:
- Jul 21, 2010, 3:08:58 PM (11 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/extralib.ma
r11 r14 649 649 | pos m ⇒ natp_to_Z (snd ?? (divide n m)) 650 650 | neg m ⇒ match divide n m with [ mk_pair q r ⇒ 651 match r with [ pzero ⇒ OZ | _ ⇒ y -(natp_to_Z r) ] ]651 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ] 652 652 ] 653 653 | neg n ⇒ … … 655 655 [ OZ ⇒ OZ 656 656 | pos m ⇒ match divide n m with [ mk_pair q r ⇒ 657 match r with [ pzero ⇒ OZ | _ ⇒ y +(natp_to_Z r) ] ]657 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ] 658 658 | neg m ⇒ natp_to_Z (snd ?? (divide n m)) 659 659 ] … … 664 664 interpretation "integer division" 'divide m n = (divZ m n). 665 665 interpretation "integer modulus" 'module m n = (modZ m n). 666 667 nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x. 668 #x y; ncases y; 669 ##[ #H; napply (False_ind … H); 670 ##| #m; #_; ncases x; //; #n; 671 nwhd in ⊢ (?%?); 672 nlapply (pos_compare_to_Prop n m); 673 ncases (pos_compare n m); /2/; 674 #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/; 675 ##| #m H; napply (False_ind … H); 676 ##] nqed. 677 678 nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. 679 #n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m); 680 ##[ //; 681 ##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/; 682 ##] nqed. 683 684 ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y. 685 #x y; ncases y; 686 ##[ #H; napply (False_ind … H); 687 ##| #m; #_; ncases x; 688 ##[ @;//; 689 ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); 690 ncases (divide n m) in ⊢ (???% → %); #dv md H; 691 nelim (divide_ok … H); #e l; nelim l; /2/; 692 ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); 693 ncases (divide n m) in ⊢ (???% → %); #dv md H; 694 nelim (divide_ok … H); #e l; nelim l; 695 ##[ /2/; 696 ##| #md' m' l'; @; 697 ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …); 698 nrewrite > (pos_compare_lt … l'); //; 699 ##| /2/; 700 ##] 701 ##] 702 ##] 703 ##| #m H; napply (False_ind … H); 704 ##] nqed.
Note: See TracChangeset
for help on using the changeset viewer.