Changeset 487 for Deliverables/D3.1/Csemantics/extralib.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/extralib.ma
r400 r487 13 13 (**************************************************************************) 14 14 15 include " datatypes/sums.ma".16 include " datatypes/list.ma".17 include " Plogic/equality.ma".15 include "basics/types.ma". 16 include "basics/list.ma". 17 include "basics/logic.ma". 18 18 include "binary/Z.ma". 19 19 include "binary/positive.ma". 20 20 21 nlemma eq_rect_Type0_r:21 lemma eq_rect_Type0_r: 22 22 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 23 #A ; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.24 nqed.25 26 nlemma eq_rect_r2:23 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. 24 qed. 25 26 lemma eq_rect_r2: 27 27 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. 28 #A ; #a; #x; #p; ncases p; #P; #H; nassumption.29 nqed.30 31 nlemma eq_rect_Type2_r:28 #A #a #x #p cases p; #P #H assumption. 29 qed. 30 31 lemma eq_rect_Type2_r: 32 32 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 33 #A ; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.34 nqed.35 36 nlemma eq_rect_CProp0_r:33 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. 34 qed. 35 36 lemma eq_rect_CProp0_r: 37 37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 38 #A ; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.39 nqed.40 41 nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.42 #A ;#x;#y;*;#H;napply nmk;#H';/2/;43 nqed.38 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. 39 qed. 40 41 lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x. 42 #A #x #y *;#H @nmk #H' /2/; 43 qed. 44 44 45 45 (* stolen from logic/connectives.ma to give Prop version. *) … … 56 56 (* bool *) 57 57 58 ndefinition xorb : bool → bool → bool ≝58 definition xorb : bool → bool → bool ≝ 59 59 λx,y. match x with [ false ⇒ y  true ⇒ notb y ]. 60 60 … … 62 62 (* TODO: move to Z.ma *) 63 63 64 nlemma eqZb_z_z : ∀z.eqZb z z = true.65 #z ;ncases z;nnormalize;//;66 nqed.64 lemma eqZb_z_z : ∀z.eqZb z z = true. 65 #z cases z;normalize;//; 66 qed. 67 67 68 68 (* XXX: divides goes to arithmetics *) 69 ninductive dividesP (n,m:Pos) : Prop ≝69 inductive dividesP (n,m:Pos) : Prop ≝ 70 70  witness : ∀p:Pos.m = times n p → dividesP n m. 71 71 interpretation "positive divides" 'divides n m = (dividesP n m). 72 72 interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). 73 73 74 ndefinition dividesZ : Z → Z → Prop ≝74 definition dividesZ : Z → Z → Prop ≝ 75 75 λx,y. match x with 76 76 [ OZ ⇒ False … … 83 83 84 84 (* should be proved in nat.ma, but it's not! *) 85 nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ].86 #n ; nelim n;87 ##[ #m; ncases m; //;88 ## #n' IH m; ncases m; ##[ /2/; ## #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %;89 nlapply (IH m'); ncases (eqb n' m'); /2/; ##]90 ##] nqed.91 92 nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ].93 #n m; napply eqb_elim; //; nqed.94 95 nlemma injective_Z_of_nat : injective ? ? Z_of_nat.96 n normalize;97 #n ;#m;ncases n;ncases m;nnormalize;//;98 ##[ ##1,2: #n';#H;ndestruct99 ## #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0);//100 ##] nqed.101 102 nlemma reflexive_Zle : reflexive ? Zle.103 #x ; ncases x; //; nqed.104 105 nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).106 #n ;ncases n;nnormalize;//;nqed.107 108 nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.109 #x ; ncases x; //;110 #n ; ncases n; //; nqed.111 112 nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.113 #x ;#y;114 napplypos_elim115 ##[ ##2: #n'; #IH; ##]116 nrewrite > (Zplus_Zsucc_Zpred y ?); 117 ##[ nrewrite > (Zpred_Zsucc (pos n')); 118 #H ; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);119 napply Zsucc_le;120 ## #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le; 121 ##] nqed.85 lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. 86 #n elim n; 87 [ #m cases m; //; 88  #n' #IH #m cases m; [ /2/;  #m' whd in match (eqb (S n') (S m')) in ⊢ %; 89 lapply (IH m'); cases (eqb n' m'); /2/; ] 90 ] qed. 91 92 lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. 93 #n #m @eqb_elim //; qed. 94 95 lemma injective_Z_of_nat : injective ? ? Z_of_nat. 96 normalize; 97 #n #m cases n;cases m;normalize;//; 98 [ 1,2: #n' #H destruct 99  #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) // 100 ] qed. 101 102 lemma reflexive_Zle : reflexive ? Zle. 103 #x cases x; //; qed. 104 105 lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). 106 #n cases n;normalize;//;qed. 107 108 lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. 109 #x cases x; //; 110 #n cases n; //; qed. 111 112 lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. 113 #x #y 114 @pos_elim 115 [ 2: #n' #IH ] 116 >(Zplus_Zsucc_Zpred y ?) 117 [ >(Zpred_Zsucc (pos n')) 118 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??) 119 @Zsucc_le 120  #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le 121 ] qed. 122 122 123 123 (* XXX: Zmax must go to arithmetics *) 124 ndefinition Zmax : Z → Z → Z ≝124 definition Zmax : Z → Z → Z ≝ 125 125 λx,y.match Z_compare x y with 126 126 [ LT ⇒ y 127 127  _ ⇒ x ]. 128 128 129 nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.130 #x ;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);131 /3/; ncases x; /3/; nqed.132 133 nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.134 #x ;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);135 ncases x; /3/; nqed.136 137 ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.138 #x y; ncases x;139 ##[ ncases y;140 ##[ ##1,2: //141 ## #n; napply False_ind;142 ##]143 ## #n; ncases y;144 ##[ nnormalize; napply False_ind;145 ## #m; napply (pos_cases … n);/2/;146 ## #m; nnormalize; napply False_ind;147 ##]148 ## #n; ncases y; /2/;149 ##] nqed.129 lemma Zmax_l: ∀x,y. x ≤ Zmax x y. 130 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y); 131 /3/; cases x; /3/; qed. 132 133 lemma Zmax_r: ∀x,y. y ≤ Zmax x y. 134 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y); 135 cases x; /3/; qed. 136 137 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. 138 #x #y cases x; 139 [ cases y; 140 [ 1,2: // 141  #n @False_ind 142 ] 143  #n cases y; 144 [ normalize; @False_ind 145  #m @(pos_cases … n) /2/; 146  #m normalize; @False_ind 147 ] 148  #n cases y; /2/; 149 ] qed. 150 150 151 ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.152 #n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;153 napply (transitive_Zle … Hle);/2/;154 nqed.155 156 ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).157 #z1 ;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;158 ##[@;//159 ##@2;//##]160 nqed.161 162 nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.163 #z1 ;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //;164 #H ; #H'; napply False_ind; napply (absurd ? H H');165 nqed.151 theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. 152 #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt 153 @(transitive_Zle … Hle) /2/; 154 qed. 155 156 definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). 157 #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H 158 [% // 159 %2 //] 160 qed. 161 162 lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. 163 #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //; 164 #H #H' @False_ind @(absurd ? H H') 165 qed. 166 166 167 167 (* Z.ma *) 168 168 169 ndefinition Zge: Z → Z → Prop ≝169 definition Zge: Z → Z → Prop ≝ 170 170 λn,m:Z.m ≤ n. 171 171 172 172 interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). 173 173 174 ndefinition Zgt: Z → Z → Prop ≝174 definition Zgt: Z → Z → Prop ≝ 175 175 λn,m:Z.m<n. 176 176 … … 179 179 interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). 180 180 181 nlet rec Zleb (x:Z) (y:Z) : bool ≝181 let rec Zleb (x:Z) (y:Z) : bool ≝ 182 182 match x with 183 183 [ OZ ⇒ … … 197 197  neg m ⇒ leb m n ]]. 198 198 199 nlet rec Zltb (x:Z) (y:Z) : bool ≝199 let rec Zltb (x:Z) (y:Z) : bool ≝ 200 200 match x with 201 201 [ OZ ⇒ … … 217 217 218 218 219 ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.220 #n ;#m;ncases n;ncases m; //;221 ##[ ##1,2: #m'; nnormalize; #H; napply(False_ind ? H)222 ## ##3,5: #n';#m'; nnormalize; napply le_to_leb_true; 223 ## ##4: #n';#m'; nnormalize; #H; napply(False_ind ? H)224 ##] nqed.225 226 ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.227 #n ;#m;ncases n;ncases m; //;228 ##[ ##1,2: #m'; nnormalize; #H; ndestruct229 ## ##3,5: #n';#m'; nnormalize; napply leb_true_to_le; 230 ## ##4: #n';#m'; nnormalize; #H; ndestruct231 ##] nqed.232 233 ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.234 #n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;235 nqed.236 237 ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.238 #n ;#m;ncases n;ncases m; //;239 ##[ nnormalize; #H; napply(False_ind ? H)240 ## ##2,3: #m'; nnormalize; #H; napply(False_ind ? H)241 ## ##4,6: #n';#m'; nnormalize; napply le_to_leb_true; 242 ## #n';#m'; nnormalize; #H; napply(False_ind ? H)243 ##] nqed.244 245 ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.246 #n ;#m;ncases n;ncases m; //;247 ##[ nnormalize; #H; ndestruct248 ## ##2,3: #m'; nnormalize; #H; ndestruct249 ## ##4,6: #n';#m'; napply leb_true_to_le; 250 ## #n';#m'; nnormalize; #H; ndestruct251 ##] nqed.252 253 ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.254 #n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;255 nqed.256 257 ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].219 theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true. 220 #n #m cases n;cases m; //; 221 [ 1,2: #m' normalize; #H @(False_ind ? H) 222  3,5: #n' #m' normalize; @le_to_leb_true 223  4: #n' #m' normalize; #H @(False_ind ? H) 224 ] qed. 225 226 theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m. 227 #n #m cases n;cases m; //; 228 [ 1,2: #m' normalize; #H destruct 229  3,5: #n' #m' normalize; @leb_true_to_le 230  4: #n' #m' normalize; #H destruct 231 ] qed. 232 233 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. 234 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct; 235 qed. 236 237 theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. 238 #n #m cases n;cases m; //; 239 [ normalize; #H @(False_ind ? H) 240  2,3: #m' normalize; #H @(False_ind ? H) 241  4,6: #n' #m' normalize; @le_to_leb_true 242  #n' #m' normalize; #H @(False_ind ? H) 243 ] qed. 244 245 theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. 246 #n #m cases n;cases m; //; 247 [ normalize; #H destruct 248  2,3: #m' normalize; #H destruct 249  4,6: #n' #m' @leb_true_to_le 250  #n' #m' normalize; #H destruct 251 ] qed. 252 253 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. 254 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct; 255 qed. 256 257 theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 258 258 (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). 259 #n ;#m;#P;#Hle;#Hnle;260 nlapply (refl ? (Zleb n m));261 nelim (Zleb n m) in ⊢ ((???%)→%);262 #Hb ;263 ##[ napply Hle; napply(Zleb_true_to_Zle … Hb)264 ## napply Hnle; napply(Zleb_false_to_not_Zle … Hb)265 ##] nqed.266 267 ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].259 #n #m #P #Hle #Hnle 260 lapply (refl ? (Zleb n m)); 261 elim (Zleb n m) in ⊢ ((???%)→%); 262 #Hb 263 [ @Hle @(Zleb_true_to_Zle … Hb) 264  @Hnle @(Zleb_false_to_not_Zle … Hb) 265 ] qed. 266 267 theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 268 268 (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). 269 #n ;#m;#P;#Hlt;#Hnlt;270 nlapply (refl ? (Zltb n m));271 nelim (Zltb n m) in ⊢ ((???%)→%);272 #Hb ;273 ##[ napply Hlt; napply(Zltb_true_to_Zlt … Hb)274 ## napply Hnlt; napply(Zltb_false_to_not_Zlt … Hb)275 ##] nqed.276 277 nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.278 #x y; ncases x; ncases y; /2/;279 #n m; napply (pos_cases … n); napply (pos_cases … m);280 ##[ //;281 ## #n';/2/;282 ## #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m'));/2/;283 ## #n' m'; #H; nnormalize in H;284 nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m');/2/;285 ##] nqed.286 287 nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.288 #x y; ncases x; ncases y;289 ##[ ##1,2,7,8,9: /2/;290 ## ##3,4: #m; nnormalize; *;291 ## #m n; napply (pos_cases … n); napply (pos_cases … m); 292 ##[ ##1,2: /2/;293 ## #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n'));/2/;294 ## #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m');/2/;295 ##]296 ## #m n; nnormalize; *;297 ##] nqed.298 299 nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).300 #n ; ncases n; //; #n'; #a b H;301 ##[ napply (pos_elim … n'); 302 ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b);/2/;303 ## #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n''));//;304 nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …);/2/;305 ##]306 ## napply (pos_elim … n'); 307 ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b);/2/;308 ## #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n''));//;309 nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …);/2/;310 ##]311 ##] nqed.312 313 nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).314 /2/; nqed.315 316 nlet rec Z_times (x:Z) (y:Z) : Z ≝269 #n #m #P #Hlt #Hnlt 270 lapply (refl ? (Zltb n m)); 271 elim (Zltb n m) in ⊢ ((???%)→%); 272 #Hb 273 [ @Hlt @(Zltb_true_to_Zlt … Hb) 274  @Hnlt @(Zltb_false_to_not_Zlt … Hb) 275 ] qed. 276 277 lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. 278 #x #y cases x; cases y; /2/; 279 #n #m @(pos_cases … n) @(pos_cases … m) 280 [ //; 281  #n' /2/; 282  #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/; 283  #n' #m' #H normalize in H; 284 >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/; 285 ] qed. 286 287 lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. 288 #x #y cases x; cases y; 289 [ 1,2,7,8,9: /2/; 290  3,4: #m normalize; *; 291  #m #n @(pos_cases … n) @(pos_cases … m) 292 [ 1,2: /2/; 293  #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/; 294  #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/; 295 ] 296  #m #n normalize; *; 297 ] qed. 298 299 lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). 300 #n cases n; //; #n' #a #b #H 301 [ @(pos_elim … n') 302 [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/; 303  #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //; 304 >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/; 305 ] 306  @(pos_elim … n') 307 [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/; 308  #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //; 309 >(Zplus_Zpred …) >(Zplus_Zpred …) /2/; 310 ] 311 ] qed. 312 313 lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). 314 /2/; qed. 315 316 let rec Z_times (x:Z) (y:Z) : Z ≝ 317 317 match x with 318 318 [ OZ ⇒ OZ … … 339 339 (* datatypes/list.ma *) 340 340 341 ntheorem nil_append_nil_both:342 ∀A:Type . ∀l1,l2:list A.341 theorem nil_append_nil_both: 342 ∀A:Type[0]. ∀l1,l2:list A. 343 343 l1 @ l2 = [] → l1 = [] ∧ l2 = []. 344 #A l1 l2; ncases l1;345 ##[ ncases l2;346 ##[ /2/347 ## #h t H; ndestruct;348 ##]349 ## ncases l2;350 ##[ nnormalize; #h t H; ndestruct;351 ## nnormalize; #h1 t1 h2 h3 H; ndestruct;352 ##]353 ##] nqed.344 #A #l1 #l2 cases l1; 345 [ cases l2; 346 [ /2/ 347  #h #t #H destruct; 348 ] 349  cases l2; 350 [ normalize; #h #t #H destruct; 351  normalize; #h1 #t1 #h2 #h3 #H destruct; 352 ] 353 ] qed. 354 354 355 355 (* division *) 356 356 357 ninductive natp : Type≝357 inductive natp : Type[0] ≝ 358 358  pzero : natp 359 359  ppos : Pos → natp. 360 360 361 ndefinition natp0 ≝361 definition natp0 ≝ 362 362 λn. match n with [ pzero ⇒ pzero  ppos m ⇒ ppos (p0 m) ]. 363 363 364 ndefinition natp1 ≝364 definition natp1 ≝ 365 365 λn. match n with [ pzero ⇒ ppos one  ppos m ⇒ ppos (p1 m) ]. 366 366 367 nlet rec divide (m,n:Pos) on m ≝367 let rec divide (m,n:Pos) on m ≝ 368 368 match m with 369 369 [ one ⇒ … … 374 374  p0 m' ⇒ 375 375 match divide m' n with 376 [ mk_pair q r ⇒376 [ pair q r ⇒ 377 377 match r with 378 378 [ pzero ⇒ 〈natp0 q,pzero〉 … … 387 387  p1 m' ⇒ 388 388 match divide m' n with 389 [ mk_pair q r ⇒389 [ pair q r ⇒ 390 390 match r with 391 391 [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉  _ ⇒ 〈natp0 q,ppos one〉 ] … … 400 400 ]. 401 401 402 ndefinition div ≝ λm,n. fst ?? (divide m n).403 ndefinition mod ≝ λm,n. snd ?? (divide m n).404 405 ndefinition pairdisc ≝406 λA,B.λx,y: pairA B.402 definition div ≝ λm,n. fst ?? (divide m n). 403 definition mod ≝ λm,n. snd ?? (divide m n). 404 405 definition pairdisc ≝ 406 λA,B.λx,y:Prod A B. 407 407 match x with 408 [( mk_pair t0 t1) ⇒408 [(pair t0 t1) ⇒ 409 409 match y with 410 [( mk_pair u0 u1) ⇒410 [(pair u0 u1) ⇒ 411 411 ∀P: Type[1]. 412 412 (∀e0: (eq A (R0 ? t0) u0). 413 413 ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. 414 414 415 nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.416 #A ;#B;#x;#y;#e;nrewrite > e;ncases y;417 #a ;#b;nnormalize;#P;#PH;napply PH;@;418 nqed.419 420 nlemma pred_minus: ∀n,m. pred n  m = pred (nm).421 napply pos_elim;/3/;422 nqed.423 424 nlemma minus_plus_distrib: ∀n,m,p:Pos. m(n+p) = mnp.425 napply pos_elim; 426 ##[ //427 ## #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one);/2/;428 ##] nqed.429 430 ntheorem plus_minus_r:415 lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. 416 #A #B #x #y #e >e cases y; 417 #a #b normalize;#P #PH @PH % 418 qed. 419 420 lemma pred_minus: ∀n,m. pred n  m = pred (nm). 421 @pos_elim /3/; 422 qed. 423 424 lemma minus_plus_distrib: ∀n,m,p:Pos. m(n+p) = mnp. 425 @pos_elim 426 [ // 427  #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/; 428 ] qed. 429 430 theorem plus_minus_r: 431 431 ∀m,n,p:Pos. m < n → p+(nm) = (p+n)m. 432 #m ;#n;#p;#le;nrewrite > (symmetric_plus …);433 nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.434 435 nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+pn≤p.436 #m ;#n;#p;nelim m;/2/; nqed.432 #m #n #p #le >(commutative_plus …) 433 >(commutative_plus p ?) @plus_minus //; qed. 434 435 lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+pn≤p. 436 #m #n #p elim m;/2/; qed. 437 437 (* 438 nlemma le_to_minus: ∀m,n. m≤n → mn = 0.439 #m ;#n;nelim n;440 ##[ nrewrite < (minus_n_O …);/2/;441 ## #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;442 nrewrite > (eq_minus_S_pred …); nrewrite > (IH A);/2/443 ##] nqed.438 lemma le_to_minus: ∀m,n. m≤n → mn = 0. 439 #m #n elim n; 440 [ <(minus_n_O …) /2/; 441  #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct; 442 >(eq_minus_S_pred …) >(IH A) /2/ 443 ] qed. 444 444 *) 445 nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*mp*n = p*(mn).446 #n ;#m;#p;(*nelim (decidable_lt n m);*)#lt;447 (* ##[*) napply (pos_elim … p); //;#p'; #IH;448 nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);449 nrewrite > (minus_plus_distrib …);450 nrewrite < (plus_minus … lt); nrewrite < IH;451 nrewrite > (plus_minus_r …);/2/;452 nqed.453 (* ##454 nlapply (not_lt_to_le … lt); #le; 455 napply (pos_elim … p); //; #p'; 456 ncut (mn = one); ##[ /3/ ##]457 #mn ; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);458 #H ; nrewrite < H in ⊢ (???%);459 napply sym_eq; napply le_n_one_to_eq; nrewrite < H;460 nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;445 lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*mp*n = p*(mn). 446 #n #m #p (*elim (decidable_lt n m);*)#lt 447 (*[*) @(pos_elim … p) //;#p' #IH 448 <(times_succn_m …) <(times_succn_m …) <(times_succn_m …) 449 >(minus_plus_distrib …) 450 <(plus_minus … lt) <IH 451 >(plus_minus_r …) /2/; 452 qed. 453 (* 454 lapply (not_lt_to_le … lt); #le 455 @(pos_elim … p) //; #p' 456 cut (mn = one); [ /3/ ] 457 #mn >mn >(times_n_one …) >(times_n_one …) 458 #H <H in ⊢ (???%) 459 @sym_eq @le_n_one_to_eq <H 460 >(minus_plus_distrib …) @monotonic_le_minus_l 461 461 /2/; 462 ##] nqed.463 464 nlemma S_pred_m_n: ∀m,n. m > n → S (pred (mn)) = mn.465 #m ;#n;#H;nlapply (refl ? (mn));nelim (mn) in ⊢ (???% → %);//;466 #H' ; nlapply (minus_to_plus … H'); /2/;467 nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H; 468 napply False_ind; napply (absurd ? H ( not_le_Sn_n n)); 469 nqed.462 ] qed. 463 464 lemma S_pred_m_n: ∀m,n. m > n → S (pred (mn)) = mn. 465 #m #n #H lapply (refl ? (mn));elim (mn) in ⊢ (???% → %);//; 466 #H' lapply (minus_to_plus … H'); /2/; 467 <(plus_n_O …) #H'' >H'' in H #H 468 @False_ind @(absurd ? H ( not_le_Sn_n n)) 469 qed. 470 470 *) 471 471 472 nlet rec natp_plus (n,m:natp) ≝472 let rec natp_plus (n,m:natp) ≝ 473 473 match n with 474 474 [ pzero ⇒ m … … 476 476 ]. 477 477 478 nlet rec natp_times (n,m:natp) ≝478 let rec natp_times (n,m:natp) ≝ 479 479 match n with 480 480 [ pzero ⇒ pzero … … 482 482 ]. 483 483 484 ninductive natp_lt : natp → Pos → Prop ≝484 inductive natp_lt : natp → Pos → Prop ≝ 485 485  plt_zero : ∀n. natp_lt pzero n 486 486  plt_pos : ∀n,m. n < m → natp_lt (ppos n) m. 487 487 488 nlemma lt_p0: ∀n:Pos. one < p0 n.489 #n ; nnormalize; /2/; nqed.490 491 nlemma lt_p1: ∀n:Pos. one < p1 n.492 #n' ; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.493 494 nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.495 #m ; nelim m;496 ##[ //;497 ## ##2,3: #m' IH; nnormalize; nrewrite > IH;//;498 ##] nqed.499 500 nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q  p0 p ⇒ P (p0 p)  p1 p ⇒ P (p1 p) ] = P (succ n).501 #n P Q; napply succ_elim; /2/; nqed.502 503 nlemma partial_minus_to_Prop: ∀n,m.488 lemma lt_p0: ∀n:Pos. one < p0 n. 489 #n normalize; /2/; qed. 490 491 lemma lt_p1: ∀n:Pos. one < p1 n. 492 #n' normalize; >(?:p1 n' = succ (p0 n')) //; qed. 493 494 lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉. 495 #m elim m; 496 [ //; 497  2,3: #m' #IH normalize; >IH //; 498 ] qed. 499 500 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). 501 #n #P #Q @succ_elim /2/; qed. 502 503 lemma partial_minus_to_Prop: ∀n,m. 504 504 match partial_minus n m with 505 505 [ MinusNeg ⇒ n < m … … 507 507  MinusPos r ⇒ n = m+r 508 508 ]. 509 #n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);510 n normalize; ncases (partial_minus n m); /2/; nqed.511 512 nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.513 #n m lt; nelim lt; /2/;514 nqed.515 516 nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.517 #n m lt; napply (transitive_lt ? (p0 m) ?);/2/;518 nqed.519 520 nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.521 #n m lt; ninversion lt;522 ##[ #H; nrewrite > (succ_injective … H);//;523 ## #p H1 H2 H3;nrewrite > (succ_injective … H3); 524 napply (transitive_lt ? (p0 p) ?);/2/;525 ##]526 nqed.527 528 nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.529 #n m lt; nelim lt; /2/;530 nqed.531 532 533 534 nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.535 #n m lt;ninversion lt;536 ##[ #p H; ndestruct;537 ## #n' m' lt e1 e2; ndestruct; //; 538 ##] nqed.539 540 nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.541 #a b; /2/; nqed.542 543 nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.544 #a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.545 546 nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.547 /2/; nqed.548 549 nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.550 #A B a1 a2 b1 b2 H; ndestruct; //;551 nqed.552 553 nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.554 #A B a1 a2 b1 b2 H; ndestruct; //;555 nqed.556 557 ntheorem divide_ok : ∀m,n,dv,md.509 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m); 510 normalize; cases (partial_minus n m); /2/; qed. 511 512 lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m. 513 #n #m #lt elim lt; /2/; 514 qed. 515 516 lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m. 517 #n #m #lt @(transitive_lt ? (p0 m) ?) /2/; 518 qed. 519 520 lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m. 521 #n #m #lt inversion lt; 522 [ #H >(succ_injective … H) //; 523  #p #H1 #H2 #H3 >(succ_injective … H3) 524 @(transitive_lt ? (p0 p) ?) /2/; 525 ] 526 qed. 527 528 lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m. 529 #n #m #lt elim lt; /2/; 530 qed. 531 532 533 534 lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m. 535 #n #m #lt inversion lt; 536 [ #p #H destruct; 537  #n' #m' #lt #e1 #e2 destruct @lt 538 ] qed. 539 540 lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b. 541 #a #b /2/; qed. 542 543 lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b. 544 #a #b >(?:p1 b = succ (p0 b)) /2/; qed. 545 546 lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. 547 /2/; qed. 548 549 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. 550 #A #B #a1 #a2 #b1 #b2 #H destruct // 551 qed. 552 553 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. 554 #A #B #a1 #a2 #b1 #b2 #H destruct // 555 qed. 556 557 theorem divide_ok : ∀m,n,dv,md. 558 558 divide m n = 〈dv,md〉 → 559 559 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. 560 #m n; napply (pos_cases … n);561 ##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/; 562 ## #n'; nelim m;563 ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;564 ## #m' IH dv md; nwhd in ⊢ (??%? → ?(???%)?);565 nlapply (refl ? (divide m' (succ n')));566 nelim (divide m' (succ n')) in ⊢ (???% → % → ?);567 #dv' md' DIVr; nelim (IH … DIVr);568 nwhd in ⊢ (? → ? → ??%? → ?);569 ncases md';570 ##[ ncases dv'; nnormalize;571 ##[ #H; ndestruct;572 ## #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;573 ##]574 ## ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;575 n normalize; #n md'' Hr1 Hr2;576 nlapply (plt_lt … Hr2); #Hr2';577 nlapply (partial_minus_to_Prop md'' n);578 ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;579 #lt ; #e; ndestruct; @; ##[ /3/; ## ##*: /2/; ##] napply plt_pos;580 ##[ ##1,3,5,7: napply double_lt1;/2/;581 ## ##2,4: napply double_lt3;/2/;582 ## ##*: napply double_lt2;/2/;583 ##]584 ##]585 ## #m' IH dv md; nwhd in ⊢ (??%? → ?);586 nlapply (refl ? (divide m' (succ n')));587 nelim (divide m' (succ n')) in ⊢ (???% → % → ?);588 #dv' md' DIVr; nelim (IH … DIVr);589 nwhd in ⊢ (? → ? → ??%? → ?); ncases md';590 ##[ ncases dv'; nnormalize;591 ##[ #H; ndestruct;592 ## #dv'' Hr1 Hr2; #H; ndestruct; /3/;593 ##]594 ## (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;595 n normalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;596 nlapply (plt_lt … Hr2); #Hr2';597 nwhd in ⊢ (??%? → ?);598 nlapply (partial_minus_to_Prop (p0 md'') (succ n'));599 ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]600 ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;601 #Hr1 ; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]602 #lt ; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]603 nrewrite < (pair_eq1 ?????? e); nrewrite < (pair_eq2 ?????? e);604 n normalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;605 ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;606 ## ncut (succ n' + r'' < p0 (succ n')); /2/;607 ## /2/;608 ## /2/;609 ##]610 ##]611 ##]612 ##] nqed.613 614 nlemma mod0_divides: ∀m,n,dv:Pos.560 #m #n @(pos_cases … n) 561 [ >(divide_by_one m) #dv #md #H destruct /2/ 562  #n' elim m; 563 [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/ 564  #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?); 565 lapply (refl ? (divide m' (succ n'))); 566 elim (divide m' (succ n')) in ⊢ (???% → % → ?); 567 #dv' #md' #DIVr elim (IH … DIVr); 568 whd in ⊢ (? → ? → ??%? → ?); 569 cases md'; 570 [ cases dv'; normalize; 571 [ #H destruct 572  #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/ 573 ] 574  cases dv'; [ 2: #dv'' ] @succ_elim 575 normalize; #n #md'' #Hr1 #Hr2 576 lapply (plt_lt … Hr2); #Hr2' 577 lapply (partial_minus_to_Prop md'' n); 578 cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize 579 #lt #e destruct % [ /3/  *: /2/ ] @plt_pos 580 [ 1,3,5,7: @double_lt1 /2/; 581  2,4: @double_lt3 /2/; 582  *: @double_lt2 /2/; 583 ] 584 ] 585  #m' #IH #dv #md whd in ⊢ (??%? → ?); 586 lapply (refl ? (divide m' (succ n'))); 587 elim (divide m' (succ n')) in ⊢ (???% → % → ?); 588 #dv' #md' #DIVr elim (IH … DIVr); 589 whd in ⊢ (? → ? → ??%? → ?); cases md'; 590 [ cases dv'; normalize; 591 [ #H destruct; 592  #dv'' #Hr1 #Hr2 #H destruct; /3/; 593 ] 594  (*cases dv'; [ 2: #dv'' ] @succ_elim 595 normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2 596 lapply (plt_lt … Hr2); #Hr2' 597 whd in ⊢ (??%? → ?); 598 lapply (partial_minus_to_Prop (p0 md'') (succ n')); 599 cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ] 600 cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize 601 #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ] 602 #lt #e [ 1,3,4,6: >lt ] 603 <(pair_eq1 ?????? e) <(pair_eq2 ?????? e) 604 normalize in ⊢ (?(???%)?); % /2/; @plt_pos 605 [ cut (succ n' + r'' < p0 (succ n')); /2/; 606  cut (succ n' + r'' < p0 (succ n')); /2/; 607  /2/; 608  /2/; 609 ] 610 ] 611 ] 612 ] qed. 613 614 lemma mod0_divides: ∀m,n,dv:Pos. 615 615 divide n m = 〈ppos dv,pzero〉 → m∣n. 616 #m ;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;617 n normalize; #H; ndestruct; //;618 nqed.619 620 nlemma divides_mod0: ∀dv,m,n:Pos.616 #m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *) 617 normalize #H destruct // 618 qed. 619 620 lemma divides_mod0: ∀dv,m,n:Pos. 621 621 n = dv*m → divide n m = 〈ppos dv,pzero〉. 622 #dv ;#m;#n;#DIV;nlapply (refl ? (divide n m));623 nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE; 624 nlapply (divide_ok … DIVIDE); *;625 ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]626 ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE; nnormalize;627 nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;628 ##[ nlapply (plus_to_minus … e0);629 nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);630 ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;631 nrewrite > (minus_times_distrib_l …);//;632 633 (* ncut (0 < dvdv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]634 #Hdv ;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;635 napply (absurd ? B (lt_to_not_le … A));636 637 ## napply False_ind; napply (absurd ? (plt_lt … lt) ?);/2/;638 639 ## nrewrite > DIVIDE; ncut (dv = dv''); /2/;640 ##]641 nqed.642 643 nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).644 #m ;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);645 #dv ;#md; ncases md; ncases dv;646 ##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct647 ## #dv'; #H; @1; napply mod0_divides;/2/;648 ## #md'; #DIVIDES; @2; napply nmk; *; #dv'; 649 nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);650 nrewrite > DIVIDES; #H';651 ndestruct;652 ## #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv'; 653 nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);654 nrewrite > DIVIDES; #H';655 ndestruct;656 ##] nqed.657 658 ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).659 #p ;#q;ncases p;660 ##[ ncases q; nnormalize; ##[ @2; /2/; ## ##*: #m; @2; /2/; ##]661 ## ##*: #n; ncases q; nnormalize; /2/;662 ##] nqed.663 664 ndefinition natp_to_Z ≝622 #dv #m #n #DIV lapply (refl ? (divide n m)); 623 elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE 624 lapply (divide_ok … DIVIDE); *; 625 cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ] 626 cases md'; [ 2,4: #md'' ] #DIVIDE normalize; 627 >DIV in ⊢ (% → ?) #H #lt destruct; 628 [ lapply (plus_to_minus … e0); 629 >(commutative_times …) >(commutative_times dv'' …) 630 cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt 631 >(minus_times_distrib_l …) //; 632 633 (*cut (0 < dvdv'); [ lapply (not_le_to_lt … nle); /2/ ] 634 #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind 635 @(absurd ? B (lt_to_not_le … A)) 636 637  @False_ind @(absurd ? (plt_lt … lt) ?) /2/; 638 639  >DIVIDE cut (dv = dv''); /2/; 640 ] 641 qed. 642 643 lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n). 644 #m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %); 645 #dv #md cases md; cases dv; 646 [ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct 647  #dv' #H %1 @mod0_divides /2/; 648  #md' #DIVIDES %2 @nmk *; #dv' 649 >(commutative_times …) #H lapply (divides_mod0 … H); 650 >DIVIDES #H' 651 destruct; 652  #md' #dv' #DIVIDES %2 @nmk *; #dv' 653 >(commutative_times …) #H lapply (divides_mod0 … H); 654 >DIVIDES #H' 655 destruct; 656 ] qed. 657 658 theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q). 659 #p #q cases p; 660 [ cases q; normalize; [ %2 /2/;  *: #m %2 /2/; ] 661  *: #n cases q; normalize; /2/; 662 ] qed. 663 664 definition natp_to_Z ≝ 665 665 λn. match n with [ pzero ⇒ OZ  ppos p ⇒ pos p ]. 666 666 667 ndefinition natp_to_negZ ≝667 definition natp_to_negZ ≝ 668 668 λn. match n with [ pzero ⇒ OZ  ppos p ⇒ neg p ]. 669 669 670 670 (* TODO: check these definitions are right. They are supposed to be the same 671 671 as Zdiv/Zmod in Coq. *) 672 ndefinition divZ ≝ λx,y.672 definition divZ ≝ λx,y. 673 673 match x with 674 674 [ OZ ⇒ OZ … … 677 677 [ OZ ⇒ OZ 678 678  pos m ⇒ natp_to_Z (fst ?? (divide n m)) 679  neg m ⇒ match divide n m with [ mk_pair q r ⇒679  neg m ⇒ match divide n m with [ pair q r ⇒ 680 680 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] ] 681 681 ] … … 683 683 match y with 684 684 [ OZ ⇒ OZ 685  pos m ⇒ match divide n m with [ mk_pair q r ⇒685  pos m ⇒ match divide n m with [ pair q r ⇒ 686 686 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] ] 687 687  neg m ⇒ natp_to_Z (fst ?? (divide n m)) … … 689 689 ]. 690 690 691 ndefinition modZ ≝ λx,y.691 definition modZ ≝ λx,y. 692 692 match x with 693 693 [ OZ ⇒ OZ … … 696 696 [ OZ ⇒ OZ 697 697  pos m ⇒ natp_to_Z (snd ?? (divide n m)) 698  neg m ⇒ match divide n m with [ mk_pair q r ⇒698  neg m ⇒ match divide n m with [ pair q r ⇒ 699 699 match r with [ pzero ⇒ OZ  _ ⇒ y+(natp_to_Z r) ] ] 700 700 ] … … 702 702 match y with 703 703 [ OZ ⇒ OZ 704  pos m ⇒ match divide n m with [ mk_pair q r ⇒704  pos m ⇒ match divide n m with [ pair q r ⇒ 705 705 match r with [ pzero ⇒ OZ  _ ⇒ y(natp_to_Z r) ] ] 706 706  neg m ⇒ natp_to_Z (snd ?? (divide n m)) … … 713 713 interpretation "integer modulus" 'module m n = (modZ m n). 714 714 715 nlemma Zminus_Zlt: ∀x,y:Z. y>0 → xy < x.716 #x y; ncases y;717 ##[ #H; napply (False_ind … H); 718 ## #m; #_; ncases x; //; #n; 719 nwhd in ⊢ (?%?);720 nlapply (pos_compare_to_Prop n m);721 ncases (pos_compare n m); /2/;722 #lt ; nwhd; nrewrite < (minus_Sn_m … lt);/2/;723 ## #m H; napply (False_ind … H); 724 ##] nqed.725 726 nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.727 #n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);728 ##[ //;729 ## ##2,3: #H; napply False_ind; napply (absurd ? lt ?);/3/;730 ##] nqed.731 732 ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.733 #x y; ncases y;734 ##[ #H; napply (False_ind … H); 735 ## #m; #_; ncases x;736 ##[ @;//;737 ## #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));738 ncases (divide n m) in ⊢ (???% → %); #dv md H;739 nelim (divide_ok … H); #e l; nelim l; /2/;740 ## #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));741 ncases (divide n m) in ⊢ (???% → %); #dv md H;742 nelim (divide_ok … H); #e l; nelim l;743 ##[ /2/;744 ## #md' m' l'; @;745 ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);746 nrewrite > (pos_compare_lt … l');//;747 ## napply Zminus_Zlt;//;748 ##]749 ##]750 ##]751 ## #m H; napply (False_ind … H); 752 ##] nqed.715 lemma Zminus_Zlt: ∀x,y:Z. y>0 → xy < x. 716 #x #y cases y; 717 [ #H @(False_ind … H) 718  #m #_ cases x; //; #n 719 whd in ⊢ (?%?); 720 lapply (pos_compare_to_Prop n m); 721 cases (pos_compare n m); /2/ 722 #lt whd <(minus_Sn_m … lt) /2/; 723  #m #H @(False_ind … H) 724 ] qed. 725 726 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. 727 #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m); 728 [ //; 729  2,3: #H @False_ind @(absurd ? lt ?) /3/; 730 ] qed. 731 732 theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y. 733 #x #y cases y; 734 [ #H @(False_ind … H) 735  #m #_ cases x; 736 [ % //; 737  #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m)); 738 cases (divide n m) in ⊢ (???% → %); #dv #md #H 739 elim (divide_ok … H); #e #l elim l; /2/; 740  #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m)); 741 cases (divide n m) in ⊢ (???% → %); #dv #md #H 742 elim (divide_ok … H); #e #l elim l; 743 [ /2/; 744  #md' #m' #l' % 745 [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …) 746 >(pos_compare_lt … l') //; 747  @Zminus_Zlt //; 748 ] 749 ] 750 ] 751  #m #H @(False_ind … H) 752 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.