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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/binary/Z.ma
r400 r487 16 16 comments may no longer be applicable. *) 17 17 18 include "arithmetics/compare.ma". 18 (*include "arithmetics/compare.ma".*) 19 19 include "binary/positive.ma". 20 20 21 ninductive Z : Type≝21 inductive Z : Type[0] ≝ 22 22 OZ : Z 23 23  pos : Pos → Z 24 24  neg : Pos → Z. 25 25 26 interpretation "Integers" 'Z = Z. 27 28 ndefinition Z_of_nat ≝26 (*interpretation "Integers" 'D = Z.*) 27 28 definition Z_of_nat ≝ 29 29 λn. match n with 30 30 [ O ⇒ OZ 31 31  S n ⇒ pos (succ_pos_of_nat n)]. 32 32 33 ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.34 35 ndefinition neg_Z_of_nat \def33 coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. 34 35 definition neg_Z_of_nat \def 36 36 λn. match n with 37 37 [ O ⇒ OZ 38 38  S n ⇒ neg (succ_pos_of_nat n)]. 39 39 40 ndefinition abs ≝40 definition abs ≝ 41 41 λz.match z with 42 42 [ OZ ⇒ O … … 44 44  neg n ⇒ nat_of_pos n]. 45 45 46 ndefinition OZ_test ≝46 definition OZ_test ≝ 47 47 λz.match z with 48 48 [ OZ ⇒ true … … 50 50  neg _ ⇒ false]. 51 51 52 ntheorem OZ_test_to_Prop : ∀z:Z.52 theorem OZ_test_to_Prop : ∀z:Z. 53 53 match OZ_test z with 54 54 [true ⇒ z=OZ 55 55 false ⇒ z ≠ OZ]. 56 #z ;ncases z57 ##[napplyrefl58 ####*:#z1;napply nmk;#H;ndestruct]59 nqed.56 #z cases z 57 [ @refl 58 *:#z1 @nmk #H destruct] 59 qed. 60 60 61 61 (* discrimination *) 62 ntheorem injective_pos: injective Pos Z pos.63 #n ;#m;#H;ndestruct;//;64 nqed.62 theorem injective_pos: injective Pos Z pos. 63 #n #m #H destruct // 64 qed. 65 65 66 66 (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m 67 67 \def injective_pos. *) 68 68 69 ntheorem injective_neg: injective Pos Z neg.70 #n ;#m;#H;ndestruct;//;71 nqed.69 theorem injective_neg: injective Pos Z neg. 70 #n #m #H destruct // 71 qed. 72 72 73 73 (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m 74 74 \def injective_neg. *) 75 75 76 ntheorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. 77 #n;napply nmk;#H;ndestruct; 78 nqed. 79 80 ntheorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. 81 #n;napply nmk;#H;ndestruct; 82 nqed. 83 84 ntheorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. 85 #n;#m;napply nmk;#H;ndestruct; 86 nqed. 87 88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). 89 #x;#y;ncases x; 90 ##[ncases y; 91 ##[@;// 92 ####*:#n;@2;napply nmk;#H;ndestruct] 93 ###n;ncases y; 94 ##[@2;napply nmk;#H;ndestruct; 95 ###m;ncases (decidable_eq_pos n m);#H; 96 ##[nrewrite > H;@;// 97 ##@2;napply nmk;#H2;nelim H; 98 (* bug if you don't introduce H3 *)#H3;ndestruct; 99 napply H3;@] 100 ###m;@2;napply nmk;#H;ndestruct] 101 ###n;ncases y; 102 ##[@2;napply nmk;#H;ndestruct; 103 ###m;@2;napply nmk;#H;ndestruct 104 ###m;ncases (decidable_eq_pos n m);#H; 105 ##[nrewrite > H;@;// 106 ##@2;napply nmk;#H2;nelim H;#H3;ndestruct; 107 napply H3;@]##]##] 108 nqed. 109 110 ndefinition Zsucc ≝ 76 theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. 77 #n @nmk #H destruct; 78 qed. 79 80 theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. 81 #n @nmk #H destruct; 82 qed. 83 84 theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. 85 #n #m @nmk #H destruct; 86 qed. 87 88 theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). 89 #x #y cases x; 90 [cases y; 91 [% // 92 *:#n %2 @nmk #H destruct] 93 #n cases y; 94 [%2 @nmk #H destruct; 95 #m cases (decidable_eq_pos n m) #H 96 [>H % // 97 %2 @(not_to_not … H) #E destruct @refl 98 ] 99 #m %2 @nmk #H destruct] 100 #n cases y; 101 [%2 @nmk #H destruct; 102 #m %2 @nmk #H destruct 103 #m cases (decidable_eq_pos n m);#H 104 [>H % // 105 %2 @(not_to_not … H) #E destruct @refl 106 ]]] 107 qed. 108 109 definition Zsucc ≝ 111 110 λz. match z with 112 111 [ OZ ⇒ pos one … … 117 116  _ ⇒ neg (pred n)]]. 118 117 119 ndefinition Zpred ≝118 definition Zpred ≝ 120 119 λz. match z with 121 120 [ OZ ⇒ neg one … … 126 125  neg n ⇒ neg (succ n)]. 127 126 128 nlemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))).129 //; nqed.130 131 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.132 #z ;ncases z;133 ##[ //134 ## #n; nnormalize; ncases n; /2/;135 ## #n; ncases n; //; #n'; 136 nrewrite > (pred_succ_unfold_hack …); nrewrite < (succ_pred_n …);//;137 @; #H; ndestruct;138 nqed.139 140 nlemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))).141 //; nqed.142 143 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.144 #z ;ncases z145 ##[ //146 ## #n; ncases n;//; #n'; 147 nrewrite > (succ_pred_unfold_hack …); nrewrite < (succ_pred_n …);//;148 @; #H; ndestruct;149 ## #n; ncases n;/3/;150 ##]151 nqed.152 153 nlet rec Zle (x:Z) (y:Z) on x : Prop ≝127 lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))). 128 //; qed. 129 130 theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. 131 #z cases z; 132 [ // 133  #n normalize; cases n; /2/; 134  #n cases n; //; #n' 135 >(pred_succ_unfold_hack …) <(succ_pred_n …) //; 136 % #H destruct; 137 qed. 138 139 lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))). 140 //; qed. 141 142 theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. 143 #z cases z 144 [ // 145  #n cases n;//; #n' 146 >(succ_pred_unfold_hack …) <(succ_pred_n …) //; 147 % #H destruct; 148  #n cases n;/3/; 149 ] 150 qed. 151 152 let rec Zle (x:Z) (y:Z) on x : Prop ≝ 154 153 match x with 155 154 [ OZ ⇒ … … 172 171 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). 173 172 174 nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝173 let rec Zlt (x:Z) (y:Z) on x : Prop ≝ 175 174 match x with 176 175 [ OZ ⇒ … … 193 192 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)). 194 193 195 ntheorem irreflexive_Zlt: irreflexive Z Zlt.196 #x ;ncases x197 ##[napply nmk;//198 ####*:#n;napply(not_le_succ_n n) (* XXX: auto?? *)]199 nqed.194 theorem irreflexive_Zlt: irreflexive Z Zlt. 195 #x cases x 196 [@nmk // 197 *:#n @(not_le_succ_n n) (* XXX: auto?? *)] 198 qed. 200 199 201 200 (* transitivity *) 202 ntheorem transitive_Zle : transitive Z Zle.203 #x ;#y;#z;ncases x204 ##[ncases y205 ##[//206 ####*:#n;ncases z;//]207 ###n;ncases y208 ##[#H;ncases H209 ##(*##*:#m;#Hl;ncases z;//;*)210 #m ;#Hl;ncases z;//;#p;#Hr;211 napply (transitive_le n m p);//; (* XXX: auto??? *)212 ###m;#Hl;ncases Hl]213 ###n;ncases y214 ##[#Hl;ncases z215 ##[##1,2://216 ###m;#Hr;ncases Hr]217 ###m;#Hl;ncases z;218 ##[##1,2://219 ###p;#Hr;ncases Hr]220 ###m;#Hl;ncases z;//;#p;#Hr;221 napply (transitive_le p m n);//; (* XXX: auto??? *) ##]222 nqed.201 theorem transitive_Zle : transitive Z Zle. 202 #x #y #z cases x 203 [cases y 204 [// 205 *:#n cases z;//] 206 #n cases y 207 [#H cases H 208 (**:#m #Hl cases z;//;*) 209 #m #Hl cases z;//;#p #Hr 210 @(transitive_le n m p) //; (* XXX: auto??? *) 211 #m #Hl cases Hl] 212 #n cases y 213 [#Hl cases z 214 [1,2:// 215 #m #Hr cases Hr] 216 #m #Hl cases z; 217 [1,2:// 218 #p #Hr cases Hr] 219 #m #Hl cases z;//;#p #Hr 220 @(transitive_le p m n) //; (* XXX: auto??? *) ] 221 qed. 223 222 224 223 (* variant trans_Zle: transitive Z Zle 225 224 \def transitive_Zle.*) 226 225 227 ntheorem transitive_Zlt: transitive Z Zlt.228 #x ;#y;#z;ncases x229 ##[ncases y230 ##[//231 ###n;ncases z232 ##[#_;#Hr;ncases Hr233 ##//234 ###m;#_;#Hr;ncases Hr]235 ###n;#Hl;ncases Hl]236 ###n;ncases y237 ##[#Hl;ncases Hl238 ###m;ncases z239 ##[//240 ###p;napply transitive_lt (* XXX: auto??? *)241 ##//##]242 ###m;#Hl;ncases Hl]243 ###n;ncases y244 ##[ncases z;245 ##[##1,2://246 ###m;#_;#Hr;ncases Hr]247 ###m;ncases z;248 ##[##1,2://249 ###p;#_;#Hr;ncases Hr]250 ###m;ncases z251 ##[##1,2://252 ###p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]253 ##]254 ##]255 nqed.226 theorem transitive_Zlt: transitive Z Zlt. 227 #x #y #z cases x 228 [cases y 229 [// 230 #n cases z 231 [#_ #Hr cases Hr 232 // 233 #m #_ #Hr cases Hr] 234 #n #Hl cases Hl] 235 #n cases y 236 [#Hl cases Hl 237 #m cases z 238 [// 239 #p apply transitive_lt (* XXX: auto??? *) 240 //] 241 #m #Hl cases Hl] 242 #n cases y 243 [cases z; 244 [1,2:// 245 #m #_ #Hr cases Hr] 246 #m cases z; 247 [1,2:// 248 #p #_ #Hr cases Hr] 249 #m cases z 250 [1,2:// 251 #p #Hl #Hr apply (transitive_lt … Hr Hl)] 252 ] 253 ] 254 qed. 256 255 257 256 (* variant trans_Zlt: transitive Z Zlt … … 260 259 \def irreflexive_Zlt.*) 261 260 262 ntheorem Zlt_neg_neg_to_lt:261 theorem Zlt_neg_neg_to_lt: 263 262 ∀n,m:Pos. neg n < neg m → m < n. 264 263 //; 265 nqed.266 267 ntheorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m.264 qed. 265 266 theorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m. 268 267 //; 269 nqed.270 271 ntheorem Zlt_pos_pos_to_lt:268 qed. 269 270 theorem Zlt_pos_pos_to_lt: 272 271 ∀n,m:Pos. pos n < pos m → n < m. 273 272 //; 274 nqed.275 276 ntheorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m.273 qed. 274 275 theorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m. 277 276 //; 278 nqed.279 280 nlemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n.281 #n ; nnormalize; nrewrite < (pred_succ_n n); ncases n; //; nqed.282 283 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.284 #x ;#y;ncases x285 ##[ncases y286 ##[#H;ncases H287 ##//;288 ###p;#H;ncases H]289 ###n;ncases y290 ##[#H;ncases H291 ###p;nnormalize;//292 ###p;#H;ncases H]293 ###n;ncases y294 ##[##1,2:ncases n;//295 ###p;napply (pos_cases … n);296 ##[#H;nelim (not_le_succ_one p);#H2;napply H2;napply H (*//;*) (* XXX: auto? *)297 ###m;nrewrite > (Zsucc_neg_succ m);napply le_S_S_to_le;(* XXX: auto? *)298 ##]299 ##]300 ##]301 nqed.277 qed. 278 279 lemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n. 280 #n normalize; <(pred_succ_n n) cases n; //; qed. 281 282 theorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y. 283 #x #y cases x 284 [cases y 285 [#H cases H 286 //; 287 #p #H cases H] 288 #n cases y 289 [#H cases H 290 #p normalize;// 291 #p #H cases H] 292 #n cases y 293 [1,2:cases n;// 294 #p @(pos_cases … n) 295 [#H elim (not_le_succ_one p);#H2 @H2 @H (*// *) (* XXX: auto? *) 296 #m >(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *) 297 ] 298 ] 299 ] 300 qed. 302 301 303 302 (*** COMPARE ***) 304 303 305 304 (* boolean equality *) 306 nlet rec eqZb (x:Z) (y:Z) on x : bool ≝305 let rec eqZb (x:Z) (y:Z) on x : bool ≝ 307 306 match x with 308 307 [ OZ ⇒ … … 322 321  neg q ⇒ eqb p q]]. 323 322 324 ntheorem eqZb_to_Prop:323 theorem eqZb_to_Prop: 325 324 ∀x,y:Z. 326 325 match eqZb x y with 327 326 [ true ⇒ x=y 328 327  false ⇒ x ≠ y]. 329 #x;#y;ncases x 330 ##[ncases y; 331 ##[// 332 ##napply not_eq_OZ_pos (* XXX: auto? *) 333 ##napply not_eq_OZ_neg (* XXX: auto? *)] 334 ###n;ncases y; 335 ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/; 336 ###m;napply eqb_elim; 337 ##[// 338 ###H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/] 339 ###m;napply not_eq_pos_neg] 340 ###n;ncases y 341 ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/; 342 ###m;napply nmk;#H;ndestruct 343 ###m;napply eqb_elim; 344 ##[// 345 ###H;napply nmk;#H2;ndestruct;nelim H;/2/] 346 ##] 347 ##] 348 nqed. 349 350 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. 328 #x #y cases x 329 [cases y; 330 [// 331 @not_eq_OZ_pos (* XXX: auto? *) 332 @not_eq_OZ_neg (* XXX: auto? *)] 333 #n cases y; 334 [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/; 335 #m @eqb_elim 336 [// 337  * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m  neg m ⇒ m  OZ ⇒ one ] with [refl ⇒ ?]) // 338 ] 339 #m @not_eq_pos_neg] 340 #n cases y 341 [@nmk #H elim (not_eq_OZ_neg n);#H /2/; 342 #m @nmk #H destruct 343 #m @eqb_elim 344 [// 345  * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m  neg m ⇒ m  OZ ⇒ one ] with [refl ⇒ ?]) // 346 ] 347 ] 348 qed. 349 350 theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. 351 351 (x=y → P true) → (x ≠ y → P false) → P (eqZb x y). 352 #x ;#y;#P;#HP1;#HP2;353 ncut352 #x #y #P #HP1 #HP2 353 cut 354 354 (match (eqZb x y) with 355 355 [ true ⇒ x=y 356 356  false ⇒ x ≠ y] → P (eqZb x y)) 357 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)358 ##[napplyHP1359 ##napplyHP2]360 ###Hcut;napply Hcut;napplyeqZb_to_Prop]361 nqed.362 363 nlet rec Z_compare (x:Z) (y:Z) : compare ≝357 [cases (eqZb x y);normalize; (* XXX: auto?? *) 358 [@HP1 359 @HP2] 360 #Hcut @Hcut @eqZb_to_Prop] 361 qed. 362 363 let rec Z_compare (x:Z) (y:Z) : compare ≝ 364 364 match x with 365 365 [ OZ ⇒ … … 379 379  neg m ⇒ pos_compare m n ]]. 380 380 381 ntheorem Z_compare_to_Prop :381 theorem Z_compare_to_Prop : 382 382 ∀x,y:Z. match (Z_compare x y) with 383 383 [ LT ⇒ x < y 384 384  EQ ⇒ x=y 385 385  GT ⇒ y < x]. 386 #x ;#y;nelim x387 ##[nelim y;//;388 ##nelim y389 ##[##1,3://390 ###n;#m;nnormalize;391 ncut (match (pos_compare m n) with386 #x #y elim x 387 [elim y;//; 388 elim y 389 [1,3:// 390 #n #m normalize; 391 cut (match (pos_compare m n) with 392 392 [ LT ⇒ m < n 393 393  EQ ⇒ m = n … … 397 397  EQ ⇒ pos m = pos n 398 398  GT ⇒ (succ n) ≤ m]) 399 ##[ncases (pos_compare m n);//400 ###Hcut;napply Hcut;napplypos_compare_to_Prop]401 ##]402 ##nelim y403 ##[#n;//404 ##nnormalize;//405 ##nnormalize;#n;#m;406 ncut (match (pos_compare n m) with399 [cases (pos_compare m n);// 400 #Hcut @Hcut @pos_compare_to_Prop] 401 ] 402 elim y 403 [#n // 404 normalize;// 405 normalize;#n #m 406 cut (match (pos_compare n m) with 407 407 [ LT ⇒ n < m 408 408  EQ ⇒ n = m … … 412 412  EQ ⇒ neg m = neg n 413 413  GT ⇒ (succ m) ≤ n]) 414 ##[ncases (pos_compare n m);//415 ###Hcut;napply Hcut;napplypos_compare_to_Prop]416 ##]417 ##]418 nqed.419 420 nlet rec Zplus (x:Z) (y:Z) on x : Z ≝414 [cases (pos_compare n m);// 415 #Hcut @Hcut @pos_compare_to_Prop] 416 ] 417 ] 418 qed. 419 420 let rec Zplus (x:Z) (y:Z) on x : Z ≝ 421 421 match x with 422 422 [ OZ ⇒ y … … 442 442 interpretation "integer plus" 'plus x y = (Zplus x y). 443 443 444 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.445 #n ;#m;ncases n446 ##[//447 ###p;ncases m448 ##[nnormalize;//449 ###m';nnormalize;nrewrite > (nat_plus_pos_plus …);nrewrite > (succ_nat_pos ?);/2/]450 nqed.451 452 ntheorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m.453 //; nqed.454 455 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.456 #z ;ncases z;//;457 nqed.458 459 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.460 #x ;#y;ncases x;461 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//462 ###p;ncases y463 ##[//464 ##nnormalize;//465 ###q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);466 ncases (pos_compare q p);//]467 ###p;ncases y468 ##[//;469 ###q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);470 ncases (pos_compare q p);//471 ##nnormalize;//]472 ##]473 nqed.474 475 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z.476 #z ;ncases z477 ##[//478 ####*:#n;ncases n;//]479 nqed.480 481 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z.482 #z ;ncases z483 ##[//484 ####*:#n;ncases n;//]485 nqed.486 487 nlemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n.488 #n ; nnormalize; ncases n; /2/; nqed.489 490 ntheorem Zplus_pos_pos:444 theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m. 445 #n #m cases n 446 [// 447 #p cases m 448 [normalize;// 449 #m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/] 450 qed. 451 452 theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m. 453 //; qed. 454 455 theorem Zplus_z_OZ: ∀z:Z. z+OZ = z. 456 #z cases z;//; 457 qed. 458 459 theorem sym_Zplus : ∀x,y:Z. x+y = y+x. 460 #x #y cases x; 461 [>(Zplus_z_OZ ?) (*XXX*) // 462 #p cases y 463 [// 464 normalize;// 465 #q normalize;>(pos_compare_n_m_m_n ??) (*XXX*) 466 cases (pos_compare q p);//] 467 #p cases y 468 [//; 469 #q normalize;>(pos_compare_n_m_m_n ??) (*XXX*) 470 cases (pos_compare q p);// 471 normalize;//] 472 ] 473 qed. 474 475 theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z. 476 #z cases z 477 [// 478 *:#n cases n;//] 479 qed. 480 481 theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z. 482 #z cases z 483 [// 484 *:#n cases n;//] 485 qed. 486 487 lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n. 488 #n normalize; cases n; /2/; qed. 489 490 theorem Zplus_pos_pos: 491 491 ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). 492 #n ;#m;napply (pos_cases … n);493 ##[ napply (pos_cases … m);//;494 ###p;napply (pos_cases … m); 495 ##[nnormalize; nrewrite < (succ_plus_one …);//;496 ###q; nrewrite > (Zsucc_Zplus_pos_O …); nrewrite > (Zpred_pos_succ ?);497 n normalize; /2/;498 ##]499 ##]500 nqed.501 502 ntheorem Zplus_pos_neg:492 #n #m @(pos_cases … n) 493 [ @(pos_cases … m) //; 494 #p @(pos_cases … m) 495 [normalize; <(succ_plus_one …) //; 496 #q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?) 497 normalize; /2/; 498 ] 499 ] 500 qed. 501 502 theorem Zplus_pos_neg: 503 503 ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). 504 #n m;505 n normalize;506 nrewrite < (pos_compare_S_S …); 507 nrewrite > (partialminus_S_S …); 508 nrewrite > (partialminus_S_S …);//;509 nqed.510 511 nlemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q  p0 p ⇒ P n  p1 p ⇒ P n ] = P n.512 #A P Q n; napply succ_elim; //; nqed.513 514 nlemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n.515 #n ; ncases n; //;516 #n' ; nwhd in ⊢ (??%?); nnormalize; nrewrite < (pred_succ_n …);517 napply succ_elim; //; nqed.518 519 ntheorem Zplus_neg_pos :504 #n #m 505 normalize; 506 <(pos_compare_S_S …) 507 >(partialminus_S_S …) 508 >(partialminus_S_S …) //; 509 qed. 510 511 lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q  p0 p ⇒ P n  p1 p ⇒ P n ] = P n. 512 #A #P #Q #n @succ_elim //; qed. 513 514 lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n. 515 #n cases n; //; 516 #n' whd in ⊢ (??%?); normalize; <(pred_succ_n …) 517 @succ_elim //; qed. 518 519 theorem Zplus_neg_pos : 520 520 ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). 521 #n m; napply (pos_cases … n); napply (pos_cases … m);522 ##[ //;523 ## #m'; nrewrite > (Zpred_pos_succ …); 524 nrewrite > (?:pos (succ m') = Zsucc (pos m'));//;525 ## #m'; nnormalize; nrewrite > (pos_compare_S_one …); nnormalize;526 nrewrite > (partial_minus_S_one …); nnormalize; nrewrite > (pos_nonzero …);527 nrewrite < (pred_succ_n …);//;528 ## #m'; #n'; nnormalize; nrewrite < (pos_compare_S_S …); 529 nrewrite > (partialminus_S_S …);530 nrewrite > (partialminus_S_S …);531 nrewrite > (pos_nonzero …);532 nrewrite > (pos_nonzero …);533 nrewrite < (pred_succ_n …);534 nrewrite < (pred_succ_n …);535 n normalize; //;536 ##] nqed.537 538 ntheorem Zplus_neg_neg:521 #n #m @(pos_cases … n) @(pos_cases … m) 522 [ //; 523  #m' >(Zpred_pos_succ …) 524 >(?:pos (succ m') = Zsucc (pos m')) //; 525  #m' normalize; >(pos_compare_S_one …) normalize; 526 >(partial_minus_S_one …) normalize; >(pos_nonzero …) 527 <(pred_succ_n …) //; 528  #m' #n' normalize; <(pos_compare_S_S …) 529 >(partialminus_S_S …) 530 >(partialminus_S_S …) 531 >(pos_nonzero …) 532 >(pos_nonzero …) 533 <(pred_succ_n …) 534 <(pred_succ_n …) 535 normalize; //; 536 ] qed. 537 538 theorem Zplus_neg_neg: 539 539 ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)). 540 #n m; napply (pos_cases … n); napply (pos_cases … m);541 ##[ ##1,2: //;542 ## #n'; nnormalize in ⊢ (???(?%?));543 nrewrite > (pos_nonzero …);544 nrewrite < (pred_succ_n …); nnormalize; //;545 ## #m';#n'; nnormalize; nrewrite > (pos_nonzero …); 546 nrewrite < (pred_succ_n …); nnormalize; //;547 ##] nqed.548 549 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).550 #x ;#y;ncases x551 ##[ncases y552 ##[//553 ###n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//554 ###p;nrewrite < (Zsucc_Zplus_pos_O …);//]555 ##ncases y;/2/; #p; nrewrite > (sym_Zplus ? (Zpred OZ)); 556 nrewrite < Zpred_Zplus_neg_O;//;557 ##ncases y558 ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);559 nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//560 ####*:/2/]561 nqed.562 563 ntheorem Zplus_Zsucc_pos_pos :540 #n #m @(pos_cases … n) @(pos_cases … m) 541 [ 1,2: //; 542  #n' normalize in ⊢ (???(?%?)); 543 >(pos_nonzero …) 544 <(pred_succ_n …) normalize; //; 545  #m' #n' normalize; >(pos_nonzero …) 546 <(pred_succ_n …) normalize; //; 547 ] qed. 548 549 theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). 550 #x #y cases x 551 [cases y 552 [// 553 #n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) // 554 #p <(Zsucc_Zplus_pos_O …) //] 555 cases y;/2/; #p >(sym_Zplus ? (Zpred OZ)) 556 <Zpred_Zplus_neg_O //; 557 cases y 558 [#n <(sym_Zplus ??) <(sym_Zplus (Zpred OZ) ?) 559 <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc ?) // 560 *:/2/] 561 qed. 562 563 theorem Zplus_Zsucc_pos_pos : 564 564 ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). 565 #n m;nrewrite > (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zplus_pos_O ?);//;566 nqed.567 568 ntheorem Zplus_Zsucc_pos_neg:565 #n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //; 566 qed. 567 568 theorem Zplus_Zsucc_pos_neg: 569 569 ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). 570 #n ;#m;571 napply(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))572 ##[#n1;nelim n1573 ##[//574 ####*:#n2;#IH;nelim n2;//]575 ###n'; nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?); 576 nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?);577 nrewrite > (Zpred_Zsucc …);/2/578 ###n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nrewrite > IH; 579 nrewrite < (Zplus_pos_neg …);//]580 nqed.581 582 ntheorem Zplus_Zsucc_neg_neg :570 #n #m 571 @(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) 572 [#n1 elim n1 573 [// 574 *:#n2 #IH elim n2;//] 575 #n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) 576 >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) 577 >(Zpred_Zsucc …) /2/ 578 #n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH 579 <(Zplus_pos_neg …) //] 580 qed. 581 582 theorem Zplus_Zsucc_neg_neg : 583 583 ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). 584 #n ;#m;585 napply(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))586 ##[napply pos_elim; 587 ##[//588 ###n2;#IH;nnormalize;nrewrite < (pred_succ_n …); nrewrite > (pos_nonzero …);//]589 ## #n'; nnormalize;590 nrewrite > (pos_nonzero …);591 nrewrite < (pred_succ_n …); nnormalize;592 nrewrite < (succ_plus_one …);593 nrewrite < (succ_plus_one …); nrewrite > (pos_nonzero …);//;594 ## #n' m' IH; nnormalize;595 nrewrite > (pos_nonzero …); nnormalize;596 nrewrite < (pluss_succn_m …);597 nrewrite > (pos_nonzero …);//;598 ##]599 nqed.600 601 nlemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.602 #n m; nnormalize; nrewrite < (pos_compare_S_S …);603 nrewrite > (partialminus_S_S …); 604 nrewrite > (partialminus_S_S …); 605 //; nqed.606 607 608 ntheorem Zplus_Zsucc_neg_pos:584 #n #m 585 @(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) 586 [@pos_elim 587 [// 588 #n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //] 589  #n' normalize; 590 >(pos_nonzero …) 591 <(pred_succ_n …) normalize; 592 <(succ_plus_one …) 593 <(succ_plus_one …) >(pos_nonzero …) //; 594  #n' #m' #IH normalize; 595 >(pos_nonzero …) normalize; 596 <(pluss_succn_m …) 597 >(pos_nonzero …) //; 598 ] 599 qed. 600 601 lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. 602 #n #m normalize; <(pos_compare_S_S …) 603 >(partialminus_S_S …) 604 >(partialminus_S_S …) 605 //; qed. 606 607 608 theorem Zplus_Zsucc_neg_pos: 609 609 ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). 610 #n ;#m;611 napply(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m)))612 ##[napply pos_elim; 613 ##[//614 ###n2;#IH;nnormalize; nrewrite > (pos_nonzero …); nnormalize;615 nrewrite > (partial_minus_S_one …);//]616 ## #n'; 617 nrewrite > (sym_Zplus …);618 nrewrite < (Zsucc_Zplus_pos_O …);619 nrewrite > (sym_Zplus …);620 nrewrite < (Zsucc_Zplus_pos_O …);//;621 ###n' m' IH; 622 nrewrite > (neg_pos_succ …);//;623 ##] nqed.624 625 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).626 #x ;#y;ncases x627 ##[ncases y;//;(*#n;nnormalize;ncases n;//;*)628 ####*:#n;ncases y;//;#m;napplyZplus_Zsucc_neg_pos(* XXX: // didn't work! *)]629 nqed.630 631 ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).632 #x ;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))633 ##[nrewrite > (Zsucc_Zpred ?);//634 ###Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]635 nqed.636 637 nlemma eq_rect_Type0_r:610 #n #m 611 @(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m))) 612 [@pos_elim 613 [// 614 #n2 #IH normalize; >(pos_nonzero …) normalize; 615 >(partial_minus_S_one …) //] 616  #n' 617 >(sym_Zplus …) 618 <(Zsucc_Zplus_pos_O …) 619 >(sym_Zplus …) 620 <(Zsucc_Zplus_pos_O …) //; 621 #n' #m' #IH 622 >(neg_pos_succ …) //; 623 ] qed. 624 625 theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y). 626 #x #y cases x 627 [cases y;//;(*#n normalize;cases n;//;*) 628 *:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)] 629 qed. 630 631 theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y). 632 #x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)) 633 [>(Zsucc_Zpred ?) // 634 #Hcut >Hcut >(Zplus_Zsucc ??) //] 635 qed. 636 637 lemma eq_rect_Type0_r: 638 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; napply (eq_rect_r ??? p0); nassumption.640 nqed.641 642 ntheorem associative_Zplus: associative Z Zplus.639 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. 640 qed. 641 642 theorem associative_Zplus: associative Z Zplus. 643 643 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) 644 #x ;#y;#z;ncases x645 ##[//646 ##napply pos_elim; 647 ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;648 ###n1;#IH;649 nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);650 nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]651 ##napply pos_elim; 652 ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;653 ###n1;#IH;654 nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);655 nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]656 ##]657 nqed.644 #x #y #z cases x 645 [// 646 @pos_elim 647 [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //; 648 #n1 #IH 649 >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?) 650 >(Zplus_Zsucc ((pos n1)+y) ?) //] 651 @pos_elim 652 [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //; 653 #n1 #IH 654 >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?) 655 >(Zplus_Zpred ((neg n1)+y) ?) //] 656 ] 657 qed. 658 658 659 659 (* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) … … 661 661 662 662 (* Zopp *) 663 ndefinition Zopp : Z → Z ≝663 definition Zopp : Z → Z ≝ 664 664 λx:Z. match x with 665 665 [ OZ ⇒ OZ … … 669 669 interpretation "integer unary minus" 'uminus x = (Zopp x). 670 670 671 ntheorem eq_OZ_Zopp_OZ : OZ = ( OZ).671 theorem eq_OZ_Zopp_OZ : OZ = ( OZ). 672 672 //; 673 nqed.674 675 ntheorem Zopp_Zplus: ∀x,y:Z. (x+y) = x + y.676 #x ;#y;ncases x677 ##[ncases y;//678 ####*:#n;ncases y;//;#m;nnormalize;napply pos_compare_elim;nnormalize;//]679 nqed.680 681 ntheorem Zopp_Zopp: ∀x:Z. x = x.682 #x ;ncases x;//;683 nqed.684 685 ntheorem Zplus_Zopp: ∀ x:Z. x+ x = OZ.686 #x ;ncases x687 ##[//688 ####*:#n;nnormalize;nrewrite > (pos_compare_n_n ?);//]689 nqed.690 691 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).692 #x ;#z;#y;#H;693 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y); 694 nrewrite < (Zplus_Zopp x); 695 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???); 673 qed. 674 675 theorem Zopp_Zplus: ∀x,y:Z. (x+y) = x + y. 676 #x #y cases x 677 [cases y;// 678 *:#n cases y;//;#m normalize;@pos_compare_elim normalize;//] 679 qed. 680 681 theorem Zopp_Zopp: ∀x:Z. x = x. 682 #x cases x;//; 683 qed. 684 685 theorem Zplus_Zopp: ∀ x:Z. x+ x = OZ. 686 #x cases x 687 [// 688 *:#n normalize;>(pos_compare_n_n ?) //] 689 qed. 690 691 theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x). 692 #x #z #y #H 693 <(Zplus_z_OZ z) <(Zplus_z_OZ y) 694 <(Zplus_Zopp x) 695 <(associative_Zplus ???) <(associative_Zplus ???) 696 696 //; 697 nqed.698 699 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).700 #x ;#z;#y;#H;701 napply (injective_Zplus_l x); 702 nrewrite < (sym_Zplus ??); 697 qed. 698 699 theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). 700 #x #z #y #H 701 @(injective_Zplus_l x) 702 <(sym_Zplus ??) 703 703 //; 704 nqed.704 qed. 705 705 706 706 (* minus *) 707 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (y).707 definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (y). 708 708 709 709 interpretation "integer minus" 'minus x y = (Zminus x y). … … 711 711 712 712 713 ndefinition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).714 ndefinition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).715 ndefinition two_p : Z → Z ≝713 definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n). 714 definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n). 715 definition two_p : Z → Z ≝ 716 716 λz.match z with 717 717 [ OZ ⇒ pos one
Note: See TracChangeset
for help on using the changeset viewer.