Changeset 1523 for src/utilities/binary
 Timestamp:
 Nov 21, 2011, 4:29:16 PM (10 years ago)
 Location:
 src/utilities/binary
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/Z.ma
r1521 r1523 635 635 qed. 636 636 637 lemma eq_rect_Type0_r:638 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.639 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.640 qed.641 642 637 theorem associative_Zplus: associative Z Zplus. 643 638 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) … … 719 714  neg _ ⇒ OZ (* same fib as Coq *) 720 715 ]. 716 717 718 719 lemma eqZb_z_z : ∀z.eqZb z z = true. 720 #z cases z;normalize;//; 721 qed. 722 723 724 725 lemma injective_Z_of_nat : injective ? ? Z_of_nat. 726 normalize; 727 #n #m cases n;cases m;normalize;//; 728 [ 1,2: #n' #H destruct 729  #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) // 730 ] qed. 731 732 lemma reflexive_Zle : reflexive ? Zle. 733 #x cases x; //; qed. 734 735 lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). 736 #n cases n;normalize;//;qed. 737 738 lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. 739 #x cases x; //; 740 #n cases n; //; qed. 741 742 lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. 743 #x #y 744 @pos_elim 745 [ 2: #n' #IH ] 746 >(Zplus_Zsucc_Zpred y ?) 747 [ >(Zpred_Zsucc (pos n')) 748 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??) 749 @Zsucc_le 750  #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le 751 ] qed. 752 753 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. 754 #x #y cases x; 755 [ cases y; 756 [ 1,2: // 757  #n @False_ind 758 ] 759  #n cases y; 760 [ normalize; @False_ind 761  #m @(pos_cases … n) /2/; 762  #m normalize; @False_ind 763 ] 764  #n cases y; /2/; 765 ] qed. 766 767 theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. 768 #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt 769 @(transitive_Zle … Hle) /2/; 770 qed. 771 772 include "basics/types.ma". 773 774 definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2). 775 #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H 776 [% // 777 %2 //] 778 qed. 779 780 lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. 781 #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //; 782 #H #H' @False_ind @(absurd ? H H') 783 qed. 784 785 (* Z.ma *) 786 787 definition Zge: Z → Z → Prop ≝ 788 λn,m:Z.m ≤ n. 789 790 interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). 791 792 definition Zgt: Z → Z → Prop ≝ 793 λn,m:Z.m<n. 794 795 interpretation "integer 'greater than'" 'gt x y = (Zgt x y). 796 797 interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). 798 799 let rec Zleb (x:Z) (y:Z) : bool ≝ 800 match x with 801 [ OZ ⇒ 802 match y with 803 [ OZ ⇒ true 804  pos m ⇒ true 805  neg m ⇒ false ] 806  pos n ⇒ 807 match y with 808 [ OZ ⇒ false 809  pos m ⇒ leb n m 810  neg m ⇒ false ] 811  neg n ⇒ 812 match y with 813 [ OZ ⇒ true 814  pos m ⇒ true 815  neg m ⇒ leb m n ]]. 816 817 let rec Zltb (x:Z) (y:Z) : bool ≝ 818 match x with 819 [ OZ ⇒ 820 match y with 821 [ OZ ⇒ false 822  pos m ⇒ true 823  neg m ⇒ false ] 824  pos n ⇒ 825 match y with 826 [ OZ ⇒ false 827  pos m ⇒ leb (succ n) m 828  neg m ⇒ false ] 829  neg n ⇒ 830 match y with 831 [ OZ ⇒ true 832  pos m ⇒ true 833  neg m ⇒ leb (succ m) n ]]. 834 835 836 837 theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true. 838 #n #m cases n;cases m; //; 839 [ 1,2: #m' normalize; #H @(False_ind ? H) 840  3,5: #n' #m' normalize; @le_to_leb_true 841  4: #n' #m' normalize; #H @(False_ind ? H) 842 ] qed. 843 844 theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m. 845 #n #m cases n;cases m; //; 846 [ 1,2: #m' normalize; #H destruct 847  3,5: #n' #m' normalize; @leb_true_to_le 848  4: #n' #m' normalize; #H destruct 849 ] qed. 850 851 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. 852 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct; 853 qed. 854 855 theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. 856 #n #m cases n;cases m; //; 857 [ normalize; #H @(False_ind ? H) 858  2,3: #m' normalize; #H @(False_ind ? H) 859  4,6: #n' #m' normalize; @le_to_leb_true 860  #n' #m' normalize; #H @(False_ind ? H) 861 ] qed. 862 863 theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. 864 #n #m cases n;cases m; //; 865 [ normalize; #H destruct 866  2,3: #m' normalize; #H destruct 867  4,6: #n' #m' @leb_true_to_le 868  #n' #m' normalize; #H destruct 869 ] qed. 870 871 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. 872 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct; 873 qed. 874 875 theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 876 (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). 877 #n #m #P #Hle #Hnle 878 lapply (refl ? (Zleb n m)); 879 elim (Zleb n m) in ⊢ ((???%)→%); 880 #Hb 881 [ @Hle @(Zleb_true_to_Zle … Hb) 882  @Hnle @(Zleb_false_to_not_Zle … Hb) 883 ] qed. 884 885 theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 886 (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). 887 #n #m #P #Hlt #Hnlt 888 lapply (refl ? (Zltb n m)); 889 elim (Zltb n m) in ⊢ ((???%)→%); 890 #Hb 891 [ @Hlt @(Zltb_true_to_Zlt … Hb) 892  @Hnlt @(Zltb_false_to_not_Zlt … Hb) 893 ] qed. 894 895 lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. 896 #x #y cases x; cases y; /2/; 897 #n #m @(pos_cases … n) @(pos_cases … m) 898 [ //; 899  #n' /2/; 900  #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/; 901  #n' #m' #H normalize in H; 902 >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/; 903 ] qed. 904 905 lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. 906 #x #y cases x; cases y; 907 [ 1,2,7,8,9: /2/; 908  3,4: #m normalize; *; 909  #m #n @(pos_cases … n) @(pos_cases … m) 910 [ 1,2: /2/; 911  #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/; 912  #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/; 913 ] 914  #m #n normalize; *; 915 ] qed. 916 917 lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). 918 #n cases n; //; #n' #a #b #H 919 [ @(pos_elim … n') 920 [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/; 921  #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //; 922 >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/; 923 ] 924  @(pos_elim … n') 925 [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/; 926  #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //; 927 >(Zplus_Zpred …) >(Zplus_Zpred …) /2/; 928 ] 929 ] qed. 930 931 lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). 932 /2/; qed. 933 934 let rec Z_times (x:Z) (y:Z) : Z ≝ 935 match x with 936 [ OZ ⇒ OZ 937  pos n ⇒ 938 match y with 939 [ OZ ⇒ OZ 940  pos m ⇒ pos (n*m) 941  neg m ⇒ neg (n*m) 942 ] 943  neg n ⇒ 944 match y with 945 [ OZ ⇒ OZ 946  pos m ⇒ neg (n*m) 947  neg m ⇒ pos (n*m) 948 ] 949 ]. 950 interpretation "integer multiplication" 'times x y = (Z_times x y). 951 952 953 954 definition Zmax : Z → Z → Z ≝ 955 λx,y.match Z_compare x y with 956 [ LT ⇒ y 957  _ ⇒ x ]. 958 959 lemma Zmax_l: ∀x,y. x ≤ Zmax x y. 960 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 961 /3/ qed. 962 963 lemma Zmax_r: ∀x,y. y ≤ Zmax x y. 964 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 965 whd in ⊢ (% → ??%); /3/ qed. 966 967 968 lemma Zminus_Zlt: ∀x,y:Z. y>0 → xy < x. 969 #x #y cases y; 970 [ #H @(False_ind … H) 971  #m #_ cases x; //; #n 972 whd in ⊢ (?%?); 973 lapply (pos_compare_to_Prop n m); 974 cases (pos_compare n m); /2/ 975 #lt whd <(minus_Sn_m … lt) /2/; 976  #m #H @(False_ind … H) 977 ] qed. 978 
src/utilities/binary/positive.ma
r1517 r1523 1160 1160 definition max : Pos → Pos → Pos ≝ 1161 1161 λn,m. match leb n m with [ true ⇒ m  _ ⇒ n]. 1162 1163 1164 1165 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. 1166 #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m); 1167 [ //; 1168  2,3: #H @False_ind @(absurd ? lt ?) /3/; 1169 ] qed. 1170 1171 lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. 1172 #n #m @eqb_elim //; qed.
Note: See TracChangeset
for help on using the changeset viewer.