Changeset 1523 for src/utilities
- Timestamp:
- Nov 21, 2011, 4:29:16 PM (9 years ago)
- Location:
- src/utilities
- Files:
-
- 1 added
- 3 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 → x-y < 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. -
src/utilities/extralib.ma
r1516 r1523 17 17 include "basics/logic.ma". 18 18 include "utilities/pair.ma". 19 include "utilities/binary/Z.ma".20 include "utilities/binary/positive.ma".21 19 22 20 lemma eq_rect_Type0_r: … … 51 49 λx,y. match x with [ false ⇒ y | true ⇒ notb y ]. 52 50 53 54 (* TODO: move to Z.ma *) 55 56 lemma eqZb_z_z : ∀z.eqZb z z = true. 57 #z cases z;normalize;//; 58 qed. 59 60 (* XXX: divides goes to arithmetics *) 61 inductive dividesP (n,m:Pos) : Prop ≝ 62 | witness : ∀p:Pos.m = times n p → dividesP n m. 63 interpretation "positive divides" 'divides n m = (dividesP n m). 64 interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). 65 66 definition dividesZ : Z → Z → Prop ≝ 67 λx,y. match x with 68 [ OZ ⇒ False 69 | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] 70 | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] 71 ]. 72 73 interpretation "integer divides" 'divides n m = (dividesZ n m). 74 interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)). 51 52 75 53 76 54 (* should be proved in nat.ma, but it's not! *) … … 82 60 ] qed. 83 61 84 lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].85 #n #m @eqb_elim //; qed.86 87 lemma injective_Z_of_nat : injective ? ? Z_of_nat.88 normalize;89 #n #m cases n;cases m;normalize;//;90 [ 1,2: #n' #H destruct91 | #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //92 ] qed.93 94 lemma reflexive_Zle : reflexive ? Zle.95 #x cases x; //; qed.96 97 lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).98 #n cases n;normalize;//;qed.99 100 lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.101 #x cases x; //;102 #n cases n; //; qed.103 104 lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.105 #x #y106 @pos_elim107 [ 2: #n' #IH ]108 >(Zplus_Zsucc_Zpred y ?)109 [ >(Zpred_Zsucc (pos n'))110 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)111 @Zsucc_le112 | #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le113 ] qed.114 115 (* XXX: Zmax must go to arithmetics *)116 definition Zmax : Z → Z → Z ≝117 λx,y.match Z_compare x y with118 [ LT ⇒ y119 | _ ⇒ x ].120 121 lemma Zmax_l: ∀x,y. x ≤ Zmax x y.122 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)123 /3/ qed.124 125 lemma Zmax_r: ∀x,y. y ≤ Zmax x y.126 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)127 whd in ⊢ (% → ??%); /3/ qed.128 129 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.130 #x #y cases x;131 [ cases y;132 [ 1,2: //133 | #n @False_ind134 ]135 | #n cases y;136 [ normalize; @False_ind137 | #m @(pos_cases … n) /2/;138 | #m normalize; @False_ind139 ]140 | #n cases y; /2/;141 ] qed.142 143 theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.144 #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt145 @(transitive_Zle … Hle) /2/;146 qed.147 148 definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).149 #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H150 [% //151 |%2 //]152 qed.153 154 lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.155 #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;156 #H #H' @False_ind @(absurd ? H H')157 qed.158 159 (* Z.ma *)160 161 definition Zge: Z → Z → Prop ≝162 λn,m:Z.m ≤ n.163 164 interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).165 166 definition Zgt: Z → Z → Prop ≝167 λn,m:Z.m<n.168 169 interpretation "integer 'greater than'" 'gt x y = (Zgt x y).170 171 interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).172 173 let rec Zleb (x:Z) (y:Z) : bool ≝174 match x with175 [ OZ ⇒176 match y with177 [ OZ ⇒ true178 | pos m ⇒ true179 | neg m ⇒ false ]180 | pos n ⇒181 match y with182 [ OZ ⇒ false183 | pos m ⇒ leb n m184 | neg m ⇒ false ]185 | neg n ⇒186 match y with187 [ OZ ⇒ true188 | pos m ⇒ true189 | neg m ⇒ leb m n ]].190 191 let rec Zltb (x:Z) (y:Z) : bool ≝192 match x with193 [ OZ ⇒194 match y with195 [ OZ ⇒ false196 | pos m ⇒ true197 | neg m ⇒ false ]198 | pos n ⇒199 match y with200 [ OZ ⇒ false201 | pos m ⇒ leb (succ n) m202 | neg m ⇒ false ]203 | neg n ⇒204 match y with205 [ OZ ⇒ true206 | pos m ⇒ true207 | neg m ⇒ leb (succ m) n ]].208 209 210 211 theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.212 #n #m cases n;cases m; //;213 [ 1,2: #m' normalize; #H @(False_ind ? H)214 | 3,5: #n' #m' normalize; @le_to_leb_true215 | 4: #n' #m' normalize; #H @(False_ind ? H)216 ] qed.217 218 theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.219 #n #m cases n;cases m; //;220 [ 1,2: #m' normalize; #H destruct221 | 3,5: #n' #m' normalize; @leb_true_to_le222 | 4: #n' #m' normalize; #H destruct223 ] qed.224 225 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;227 qed.228 229 theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.230 #n #m cases n;cases m; //;231 [ normalize; #H @(False_ind ? H)232 | 2,3: #m' normalize; #H @(False_ind ? H)233 | 4,6: #n' #m' normalize; @le_to_leb_true234 | #n' #m' normalize; #H @(False_ind ? H)235 ] qed.236 237 theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.238 #n #m cases n;cases m; //;239 [ normalize; #H destruct240 | 2,3: #m' normalize; #H destruct241 | 4,6: #n' #m' @leb_true_to_le242 | #n' #m' normalize; #H destruct243 ] qed.244 245 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;247 qed.248 249 theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].250 (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).251 #n #m #P #Hle #Hnle252 lapply (refl ? (Zleb n m));253 elim (Zleb n m) in ⊢ ((???%)→%);254 #Hb255 [ @Hle @(Zleb_true_to_Zle … Hb)256 | @Hnle @(Zleb_false_to_not_Zle … Hb)257 ] qed.258 259 theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].260 (n < m → P true) → (n ≮ m → P false) → P (Zltb n m).261 #n #m #P #Hlt #Hnlt262 lapply (refl ? (Zltb n m));263 elim (Zltb n m) in ⊢ ((???%)→%);264 #Hb265 [ @Hlt @(Zltb_true_to_Zlt … Hb)266 | @Hnlt @(Zltb_false_to_not_Zlt … Hb)267 ] qed.268 269 lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.270 #x #y cases x; cases y; /2/;271 #n #m @(pos_cases … n) @(pos_cases … m)272 [ //;273 | #n' /2/;274 | #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;275 | #n' #m' #H normalize in H;276 >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;277 ] qed.278 279 lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.280 #x #y cases x; cases y;281 [ 1,2,7,8,9: /2/;282 | 3,4: #m normalize; *;283 | #m #n @(pos_cases … n) @(pos_cases … m)284 [ 1,2: /2/;285 | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;286 | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;287 ]288 | #m #n normalize; *;289 ] qed.290 291 lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).292 #n cases n; //; #n' #a #b #H293 [ @(pos_elim … n')294 [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;295 | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;296 >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;297 ]298 | @(pos_elim … n')299 [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;300 | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;301 >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;302 ]303 ] qed.304 305 lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).306 /2/; qed.307 308 let rec Z_times (x:Z) (y:Z) : Z ≝309 match x with310 [ OZ ⇒ OZ311 | pos n ⇒312 match y with313 [ OZ ⇒ OZ314 | pos m ⇒ pos (n*m)315 | neg m ⇒ neg (n*m)316 ]317 | neg n ⇒318 match y with319 [ OZ ⇒ OZ320 | pos m ⇒ neg (n*m)321 | neg m ⇒ pos (n*m)322 ]323 ].324 interpretation "integer multiplication" 'times x y = (Z_times x y).325 62 (* datatypes/list.ma *) 326 63 … … 338 75 ] 339 76 ] qed. 340 341 (* division *)342 343 inductive natp : Type[0] ≝344 | pzero : natp345 | ppos : Pos → natp.346 347 definition natp0 ≝348 λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].349 350 definition natp1 ≝351 λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].352 353 let rec divide (m,n:Pos) on m ≝354 match m with355 [ one ⇒356 match n with357 [ one ⇒ 〈ppos one,pzero〉358 | _ ⇒ 〈pzero,ppos one〉359 ]360 | p0 m' ⇒361 match divide m' n with362 [ pair q r ⇒363 match r with364 [ pzero ⇒ 〈natp0 q,pzero〉365 | ppos r' ⇒366 match partial_minus (p0 r') n with367 [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉368 | MinusZero ⇒ 〈natp1 q, pzero〉369 | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉370 ]371 ]372 ]373 | p1 m' ⇒374 match divide m' n with375 [ pair q r ⇒376 match r with377 [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]378 | ppos r' ⇒379 match partial_minus (p1 r') n with380 [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉381 | MinusZero ⇒ 〈natp1 q, pzero〉382 | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉383 ]384 ]385 ]386 ].387 388 definition div ≝ λm,n. fst ?? (divide m n).389 definition mod ≝ λm,n. snd ?? (divide m n).390 391 lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).392 @pos_elim /3/;393 qed.394 395 lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.396 @pos_elim397 [ //398 | #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;399 ] qed.400 401 theorem plus_minus_r:402 ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.403 #m #n #p #le >(commutative_plus …)404 >(commutative_plus p ?) @plus_minus //; qed.405 406 lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.407 #m #n #p elim m;/2/; qed.408 (*409 lemma le_to_minus: ∀m,n. m≤n → m-n = 0.410 #m #n elim n;411 [ <(minus_n_O …) /2/;412 | #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;413 >(eq_minus_S_pred …) >(IH A) /2/414 ] qed.415 *)416 lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).417 #n #m #p (*elim (decidable_lt n m);*)#lt418 (*[*) @(pos_elim … p) //;#p' #IH419 <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)420 >(minus_plus_distrib …)421 <(plus_minus … lt) <IH422 >(plus_minus_r …) /2/;423 qed.424 (*|425 lapply (not_lt_to_le … lt); #le426 @(pos_elim … p) //; #p'427 cut (m-n = one); [ /3/ ]428 #mn >mn >(times_n_one …) >(times_n_one …)429 #H <H in ⊢ (???%)430 @sym_eq @le_n_one_to_eq <H431 >(minus_plus_distrib …) @monotonic_le_minus_l432 /2/;433 ] qed.434 435 lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.436 #m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;437 #H' lapply (minus_to_plus … H'); /2/;438 <(plus_n_O …) #H'' >H'' in H #H439 @False_ind @(absurd ? H ( not_le_Sn_n n))440 qed.441 *)442 443 let rec natp_plus (n,m:natp) ≝444 match n with445 [ pzero ⇒ m446 | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]447 ].448 449 let rec natp_times (n,m:natp) ≝450 match n with451 [ pzero ⇒ pzero452 | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]453 ].454 455 inductive natp_lt : natp → Pos → Prop ≝456 | plt_zero : ∀n. natp_lt pzero n457 | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.458 459 lemma lt_p0: ∀n:Pos. one < p0 n.460 #n normalize; /2/; qed.461 462 lemma lt_p1: ∀n:Pos. one < p1 n.463 #n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.464 465 lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.466 #m elim m;467 [ //;468 | 2,3: #m' #IH normalize; >IH //;469 ] qed.470 471 lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).472 #n #P #Q @succ_elim /2/; qed.473 474 lemma partial_minus_to_Prop: ∀n,m.475 match partial_minus n m with476 [ MinusNeg ⇒ n < m477 | MinusZero ⇒ n = m478 | MinusPos r ⇒ n = m+r479 ].480 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);481 normalize; cases (partial_minus n m); /2/; qed.482 483 lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.484 #n #m #lt elim lt; /2/;485 qed.486 487 lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.488 #n #m #lt @(transitive_lt ? (p0 m) ?) /2/;489 qed.490 491 lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.492 #n #m #lt inversion lt;493 [ #H >(succ_injective … H) //;494 | #p #H1 #H2 #H3 >(succ_injective … H3)495 @(transitive_lt ? (p0 p) ?) /2/;496 ]497 qed.498 499 lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.500 #n #m #lt elim lt; /2/;501 qed.502 503 504 505 lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.506 #n #m #lt inversion lt;507 [ #p #H destruct;508 | #n' #m' #lt #e1 #e2 destruct @lt509 ] qed.510 511 lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.512 #a #b /2/; qed.513 514 lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.515 #a #b >(?:p1 b = succ (p0 b)) /2/; qed.516 517 lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.518 /2/; qed.519 520 theorem divide_ok : ∀m,n,dv,md.521 divide m n = 〈dv,md〉 →522 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.523 #m #n @(pos_cases … n)524 [ >(divide_by_one m) #dv #md #H destruct normalize /2/525 | #n' elim m;526 [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/527 | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);528 lapply (refl ? (divide m' (succ n')));529 elim (divide m' (succ n')) in ⊢ (???% → % → ?);530 #dv' #md' #DIVr elim (IH … DIVr);531 whd in ⊢ (? → ? → ??%? → ?);532 cases md';533 [ cases dv'; normalize;534 [ #H destruct535 | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/536 ]537 | cases dv'; [ 2: #dv'' ] @succ_elim538 normalize; #n #md'' #Hr1 #Hr2539 lapply (plt_lt … Hr2); #Hr2'540 lapply (partial_minus_to_Prop md'' n);541 cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize542 #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos543 [ 1,3,5,7: @double_lt1 /2/;544 | 2,4: @double_lt3 /2/;545 | *: @double_lt2 /2/;546 ]547 ]548 | #m' #IH #dv #md whd in ⊢ (??%? → ?);549 lapply (refl ? (divide m' (succ n')));550 elim (divide m' (succ n')) in ⊢ (???% → % → ?);551 #dv' #md' #DIVr elim (IH … DIVr);552 whd in ⊢ (? → ? → ??%? → ?); cases md';553 [ cases dv'; normalize;554 [ #H destruct;555 | #dv'' #Hr1 #Hr2 #H destruct; /3/;556 ]557 | (*cases dv'; [ 2: #dv'' ] @succ_elim558 normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2559 lapply (plt_lt … Hr2); #Hr2'560 whd in ⊢ (??%? → ?);561 lapply (partial_minus_to_Prop (p0 md'') (succ n'));562 cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]563 cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize564 #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]565 #lt #e [ 1,3,4,6: >lt ]566 <(pair_eq1 ?????? e) <(pair_eq2 ?????? e)567 normalize in ⊢ (?(???%)?); % /2/; @plt_pos568 [ cut (succ n' + r'' < p0 (succ n')); /2/;569 | cut (succ n' + r'' < p0 (succ n')); /2/; ]]]]570 qed.571 572 lemma mod0_divides: ∀m,n,dv:Pos.573 divide n m = 〈ppos dv,pzero〉 → m∣n.574 #m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)575 normalize #H destruct //576 qed.577 578 lemma divides_mod0: ∀dv,m,n:Pos.579 n = dv*m → divide n m = 〈ppos dv,pzero〉.580 #dv #m #n #DIV lapply (refl ? (divide n m));581 elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE582 lapply (divide_ok … DIVIDE); *;583 cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]584 cases md'; [ 2,4: #md'' ] #DIVIDE normalize;585 >DIV in ⊢ (% → ?); #H #lt destruct;586 [ lapply (plus_to_minus … e0);587 >(commutative_times …) >(commutative_times dv'' …)588 cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt589 >(minus_times_distrib_l …) //;590 591 (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]592 #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind593 @(absurd ? B (lt_to_not_le … A))594 595 | @False_ind @(absurd ? (plt_lt … lt) ?) /2/;596 597 | >DIVIDE cut (dv = dv''); /2/;598 ]599 qed.600 601 lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).602 #m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);603 #dv #md cases md; cases dv;604 [ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct605 | #dv' #H %1 @mod0_divides /2/;606 | #md' #DIVIDES %2 @nmk *; #dv'607 >(commutative_times …) #H lapply (divides_mod0 … H);608 >DIVIDES #H'609 destruct;610 | #md' #dv' #DIVIDES %2 @nmk *; #dv'611 >(commutative_times …) #H lapply (divides_mod0 … H);612 >DIVIDES #H'613 destruct;614 ] qed.615 616 theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).617 #p #q cases p;618 [ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]619 | *: #n cases q; normalize; /2/;620 ] qed.621 622 definition natp_to_Z ≝623 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].624 625 definition natp_to_negZ ≝626 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].627 628 (* TODO: check these definitions are right. They are supposed to be the same629 as Zdiv/Zmod in Coq. *)630 definition divZ ≝ λx,y.631 match x with632 [ OZ ⇒ OZ633 | pos n ⇒634 match y with635 [ OZ ⇒ OZ636 | pos m ⇒ natp_to_Z (fst ?? (divide n m))637 | neg m ⇒ match divide n m with [ pair q r ⇒638 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]639 ]640 | neg n ⇒641 match y with642 [ OZ ⇒ OZ643 | pos m ⇒ match divide n m with [ pair q r ⇒644 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]645 | neg m ⇒ natp_to_Z (fst ?? (divide n m))646 ]647 ].648 649 definition modZ ≝ λx,y.650 match x with651 [ OZ ⇒ OZ652 | pos n ⇒653 match y with654 [ OZ ⇒ OZ655 | pos m ⇒ natp_to_Z (snd ?? (divide n m))656 | neg m ⇒ match divide n m with [ pair q r ⇒657 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]658 ]659 | neg n ⇒660 match y with661 [ OZ ⇒ OZ662 | pos m ⇒ match divide n m with [ pair q r ⇒663 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]664 | neg m ⇒ natp_to_Z (snd ?? (divide n m))665 ]666 ].667 668 interpretation "natural division" 'divide m n = (div m n).669 interpretation "natural modulus" 'module m n = (mod m n).670 interpretation "integer division" 'divide m n = (divZ m n).671 interpretation "integer modulus" 'module m n = (modZ m n).672 673 lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.674 #x #y cases y;675 [ #H @(False_ind … H)676 | #m #_ cases x; //; #n677 whd in ⊢ (?%?);678 lapply (pos_compare_to_Prop n m);679 cases (pos_compare n m); /2/680 #lt whd <(minus_Sn_m … lt) /2/;681 | #m #H @(False_ind … H)682 ] qed.683 684 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.685 #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);686 [ //;687 | 2,3: #H @False_ind @(absurd ? lt ?) /3/;688 ] qed.689 690 theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.691 #x #y cases y;692 [ #H @(False_ind … H)693 | #m #_ cases x;694 [ % //;695 | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));696 cases (divide n m) in ⊢ (???% → %); #dv #md #H697 elim (divide_ok … H); #e #l elim l; /2/;698 | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));699 cases (divide n m) in ⊢ (???% → %); #dv #md #H700 elim (divide_ok … H); #e #l elim l;701 [ /2/;702 | #md' #m' #l' %703 [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)704 >(pos_compare_lt … l') //;705 | @Zminus_Zlt //;706 ]707 ]708 ]709 | #m #H @(False_ind … H)710 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.