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

 2 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 
Deliverables/D3.1/Csemantics/binary/positive.ma
r10 r487 15 15 (* little endian positive binary numbers. *) 16 16 17 include "basics/functions.ma". 18 include "basics/eq.ma". 17 include "basics/logic.ma". 19 18 include "arithmetics/nat.ma". 20 include "arithmetics/compare.ma". 21 22 ninductive Pos : Type ≝ 19 include "oldlib/eq.ma". 20 21 (* arithmetics/comparison.ma > *) 22 inductive compare : Type[0] ≝ 23  LT : compare 24  EQ : compare 25  GT : compare. 26 27 definition compare_invert: compare → compare ≝ 28 λc.match c with 29 [ LT ⇒ GT 30  EQ ⇒ EQ 31  GT ⇒ LT ]. 32 33 (* < *) 34 35 inductive Pos : Type[0] ≝ 23 36  one : Pos 24 37  p1 : Pos → Pos 25 38  p0 : Pos → Pos. 26 39 27 nlet rec pred (n:Pos) ≝40 let rec pred (n:Pos) ≝ 28 41 match n with 29 42 [ one ⇒ one … … 32 45 ]. 33 46 34 nremarktest : pred (p0 (p0 (p0 one))) = p1 (p1 one).35 //; nqed.36 37 nlet rec succ (n:Pos) ≝47 example test : pred (p0 (p0 (p0 one))) = p1 (p1 one). 48 //; qed. 49 50 let rec succ (n:Pos) ≝ 38 51 match n with 39 52 [ one ⇒ p0 one … … 42 55 ]. 43 56 44 nlemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n).45 #P H0 H1 n; ncases n; nnormalize; //; nqed.46 47 ntheorem pred_succ_n : ∀n. n = pred (succ n).48 #n ; nelim n;49 ##[ ##1,3: //50 ## #p'; nnormalize; napply succ_elim;/2/;51 ##] nqed.57 lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n). 58 #P #H0 #H1 #n cases n; normalize; //; qed. 59 60 theorem pred_succ_n : ∀n. n = pred (succ n). 61 #n elim n; 62 [ 1,3: // 63  #p' normalize; @succ_elim /2/; 64 ] qed. 52 65 (* 53 ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n).54 #n ; nelim n;55 ##[ #H; napply False_ind; nelim H; /2/;56 ## //;57 ## #n'; ncases n'; /2/; #n''; #IH; #_; nrewrite < IH; nnormalize;66 theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). 67 #n elim n; 68 [ #H @False_ind elim H; /2/; 69  //; 70  #n' cases n'; /2/; #n'' #IH #_ <IH normalize; 58 71 *) 59 ntheorem succ_injective: injective Pos Pos succ.60 //; nqed.61 62 nlet rec nat_of_pos (p:Pos) : nat ≝72 theorem succ_injective: injective Pos Pos succ. 73 //; qed. 74 75 let rec nat_of_pos (p:Pos) : nat ≝ 63 76 match p with 64 77 [ one ⇒ 1 … … 67 80 ]. 68 81 69 nlet rec succ_pos_of_nat (n:nat) : Pos ≝82 let rec succ_pos_of_nat (n:nat) : Pos ≝ 70 83 match n with 71 84 [ O ⇒ one … … 73 86 ]. 74 87 75 ntheorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).76 //; nqed.77 78 ntheorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.79 #n ; nelim n;80 ##[ #m; ncases m;81 ##[ //82 ## #m'; nnormalize; napply succ_elim; #p H; ndestruct83 ##]84 ## #n' IH m; ncases m;85 ##[ nnormalize; napply succ_elim; #p H; ndestruct;86 ## nnormalize; #m' H; nrewrite > (IH m' ?);//;87 ##]88 ##] nqed.89 90 nremark test2 : nat_of_pos (p0 (p1 one)) = 6. //; nqed.88 theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n). 89 //; qed. 90 91 theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat. 92 #n elim n; 93 [ #m cases m; 94 [ // 95  #m' normalize; @succ_elim #p #H destruct 96 ] 97  #n' #IH #m cases m; 98 [ normalize; @succ_elim #p #H destruct; 99  normalize; #m' #H >(IH m' ?) //; 100 ] 101 ] qed. 102 103 example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed. 91 104 92 105 (* Usual induction principle; proof roughly following Coq's, 93 106 apparently due to Conor McBride. *) 94 107 95 ninductive possucc : Pos → Prop ≝108 inductive possucc : Pos → Prop ≝ 96 109  psone : possucc one 97 110  pssucc : ∀n. possucc n → possucc (succ n). 98 111 99 nlet rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝112 let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ 100 113 match p return λn',p'.possucc (p0 n') with 101 114 [ psone ⇒ pssucc ? psone … … 103 116 ]. 104 117 105 nlet rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝118 let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ 106 119 match p return λn',p'. possucc (p1 n') with 107 120 [ psone ⇒ pssucc ? (pssucc ? psone) … … 109 122 ]. 110 123 111 nlet rec possuccinj (n:Pos) : possucc n ≝124 let rec possuccinj (n:Pos) : possucc n ≝ 112 125 match n with 113 126 [ one ⇒ psone … … 116 129 ]. 117 130 118 nlet rec possucc_elim131 let rec possucc_elim 119 132 (P : Pos → Prop) 120 133 (Pone : P one) … … 127 140 ]. 128 141 129 ndefinition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n.130 #P Pone Psucc n; napply (possucc_elim … (possuccinj n)); /2/; nqed.131 132 nlet rec possucc_cases142 definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n. 143 #P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed. 144 145 let rec possucc_cases 133 146 (P : Pos → Prop) 134 147 (Pone : P one) … … 141 154 ]. 142 155 143 ndefinition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n.144 #P Pone Psucc n; napply (possucc_cases … (possuccinj n)); /2/; nqed.145 146 ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n).147 napply pos_elim; 148 ##[ #H; napply False_ind; nelim H; /2/;149 ## //;150 ##] nqed.151 152 ntheorem not_eq_one_succ : ∀n:Pos. one ≠ succ n.153 #n ; nelim n; nnormalize;154 ##[ @; #H; ndestruct;155 ## ##2,3: #n' H; @; #H'; ndestruct;156 ##] nqed.157 158 ntheorem not_eq_n_succn: ∀n:Pos. n ≠ succ n.159 #n ; nelim n;160 ##[ //;161 ## ##*: #n' IH; nnormalize; @; #H; ndestruct162 ##] nqed.163 164 ntheorem pos_elim2:156 definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n. 157 #P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed. 158 159 theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). 160 @pos_elim 161 [ #H @False_ind elim H; /2/; 162  //; 163 ] qed. 164 165 theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n. 166 #n elim n; normalize; 167 [ % #H destruct; 168  2,3: #n' #H % #H' destruct; 169 ] qed. 170 171 theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. 172 #n elim n; 173 [ //; 174  *: #n' #IH normalize; % #H destruct 175 ] qed. 176 177 theorem pos_elim2: 165 178 ∀R:Pos → Pos → Prop. 166 179 (∀n:Pos. R one n) … … 168 181 → (∀n,m:Pos. R n m → R (succ n) (succ m)) 169 182 → ∀n,m:Pos. R n m. 170 #R ROn RSO RSS; napply pos_elim;//;171 #n0 Rn0m; napply pos_elim; /2/; nqed.172 173 174 ntheorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m).175 napply pos_elim2; #n; 176 ##[ napply (pos_elim ??? n);/2/;177 ## /3/;178 ## #m Hind; ncases Hind; /3/;179 ##] nqed.180 181 nlet rec plus n m ≝183 #R #ROn #RSO #RSS @pos_elim //; 184 #n0 #Rn0m @pos_elim /2/; qed. 185 186 187 theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m). 188 @pos_elim2 #n 189 [ @(pos_elim ??? n) /2/; 190  /3/; 191  #m #Hind cases Hind; /3/; 192 ] qed. 193 194 let rec plus n m ≝ 182 195 match n with 183 196 [ one ⇒ succ m … … 198 211 interpretation "positive plus" 'plus x y = (plus x y). 199 212 200 ntheorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m).201 #n ; nelim n; nnormalize;202 ##[ //203 ## ##2,3: #n' IH m; ncases m; /3/;204 n normalize; ncases n'; //;205 ##] nqed.206 207 ntheorem symmetric_plus : symmetric? plus.208 #n ; nelim n;209 ##[ #y; ncases y; nnormalize; //;210 ## ##2,3: #n' IH y; ncases y; nnormalize; //;211 ##] nqed.212 213 ntheorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.214 #n m; nrewrite > (symmetric_plus (succ n) m);215 nrewrite < (plus_n_succm …); //; nqed.216 217 ntheorem associative_plus : associative Pos plus.218 napply pos_elim; 219 ##[ nnormalize; //;220 ## #x' IHx; napply pos_elim; 221 ##[ #z; nrewrite < (pluss_succn_m …); nrewrite < (pluss_succn_m …);222 nrewrite < (pluss_succn_m …);//;223 ## #y' IHy' z;224 nrewrite < (pluss_succn_m y' …);225 nrewrite < (plus_n_succm …);226 nrewrite < (plus_n_succm …);227 nrewrite < (pluss_succn_m ? z); nrewrite > (IHy' …);//;228 ##]229 ##] nqed.230 231 ntheorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m).232 napply pos_elim; nnormalize; /3/; nqed.233 234 ntheorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n).235 /2/; nqed.236 237 ntheorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m).238 #n ; nelim n;239 ##[ nnormalize; //;240 ## #n' IH m; nnormalize; nrewrite > (IH m); nrewrite < (pluss_succn_m …); 241 nrewrite < (pred_succ_n ?); nrewrite < (succ_pred_n …);//;242 nelim n'; nnormalize; /2/;243 ##] nqed.244 245 nlet rec times n m ≝213 theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m). 214 #n elim n; normalize; 215 [ // 216  2,3: #n' #IH #m cases m; /3/; 217 normalize; cases n'; //; 218 ] qed. 219 220 theorem commutative_plus : commutative ? plus. 221 #n elim n; 222 [ #y cases y; normalize; //; 223  2,3: #n' #IH #y cases y; normalize; //; 224 ] qed. 225 226 theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. 227 #n #m >(commutative_plus (succ n) m) 228 <(plus_n_succm …) //; qed. 229 230 theorem associative_plus : associative Pos plus. 231 @pos_elim 232 [ normalize; //; 233  #x' #IHx @pos_elim 234 [ #z <(pluss_succn_m …) <(pluss_succn_m …) 235 <(pluss_succn_m …) //; 236  #y' #IHy' #z 237 <(pluss_succn_m y' …) 238 <(plus_n_succm …) 239 <(plus_n_succm …) 240 <(pluss_succn_m ? z) >(IHy' …) //; 241 ] 242 ] qed. 243 244 theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). 245 @pos_elim normalize; /3/; qed. 246 247 theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). 248 /2/; qed. 249 250 theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m). 251 #n elim n; 252 [ normalize; //; 253  #n' #IH #m normalize; >(IH m) <(pluss_succn_m …) 254 <(pred_succ_n ?) <(succ_pred_n …) //; 255 elim n'; normalize; /2/; 256 ] qed. 257 258 let rec times n m ≝ 246 259 match n with 247 260 [ one ⇒ m … … 252 265 interpretation "positive times" 'times x y = (times x y). 253 266 254 nlemma p0_times2: ∀n. p0 n = (succ one) * n.255 //; nqed.256 257 nlemma plus_times2: ∀n. n + n = (succ one) * n.258 #n ; nelim n;259 ##[ //;260 ## ##2,3: #n' IH; nnormalize; nrewrite > IH;//;261 ##] nqed.262 263 264 ntheorem times_succn_m: ∀n,m. m+n*m = (succ n)*m.265 #n ; nelim n;266 ##[ /2/267 ## #n' IH; nnormalize; #m; nrewrite < (IH m);//;268 ## /2/269 ##] nqed.270 271 ntheorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m).272 napply pos_elim; 273 ##[ //274 ## #n IH m; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);/3/;275 ##] nqed.276 277 ntheorem times_n_one: ∀n:Pos. n * one = n.278 #n ; nelim n; /3/; nqed.279 280 ntheorem symmetric_times: symmetricPos times.281 napply pos_elim; /2/; nqed.282 283 ntheorem distributive_times_plus : distributive Pos times plus.284 napply pos_elim; /2/; nqed.285 286 ntheorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a.287 //; nqed.288 289 ntheorem associative_times: associative Pos times.290 napply pos_elim; 291 ##[ //;292 ## #x IH y z; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);//;293 ##] nqed.294 295 nlemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z).296 //; nqed.267 lemma p0_times2: ∀n. p0 n = (succ one) * n. 268 //; qed. 269 270 lemma plus_times2: ∀n. n + n = (succ one) * n. 271 #n elim n; 272 [ //; 273  2,3: #n' #IH normalize; >IH //; 274 ] qed. 275 276 277 theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m. 278 #n elim n; 279 [ /2/ 280  #n' #IH normalize; #m <(IH m) //; 281  /2/ 282 ] qed. 283 284 theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m). 285 @pos_elim 286 [ // 287  #n #IH #m <(times_succn_m …) <(times_succn_m …) /3/; 288 ] qed. 289 290 theorem times_n_one: ∀n:Pos. n * one = n. 291 #n elim n; /3/; qed. 292 293 theorem commutative_times: commutative Pos times. 294 @pos_elim /2/; qed. 295 296 theorem distributive_times_plus : distributive Pos times plus. 297 @pos_elim /2/; qed. 298 299 theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. 300 //; qed. 301 302 theorem associative_times: associative Pos times. 303 @pos_elim 304 [ //; 305  #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //; 306 ] qed. 307 308 lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). 309 //; qed. 297 310 298 311 (*** ordering relations ***) … … 301 314 but it means the proofs are much the same. *) 302 315 303 ninductive le (n:Pos) : Pos → Prop ≝316 inductive le (n:Pos) : Pos → Prop ≝ 304 317  le_n : le n n 305 318  le_S : ∀m:Pos. le n m → le n (succ m). … … 308 321 interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)). 309 322 310 ndefinition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m.323 definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. 311 324 312 325 interpretation "positive 'less than'" 'lt x y = (lt x y). 313 326 interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)). 314 327 315 ndefinition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n.328 definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. 316 329 317 330 interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y). 318 331 interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)). 319 332 320 ndefinition gt: Pos → Pos → Prop ≝ λn,m. m<n.333 definition gt: Pos → Pos → Prop ≝ λn,m. m<n. 321 334 322 335 interpretation "positive 'greater than'" 'gt x y = (gt x y). 323 336 interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)). 324 337 325 ntheorem transitive_le: transitive Pos le.326 #a b c leab lebc; nelim lebc; /2/; nqed.327 328 ntheorem transitive_lt: transitive Pos lt.329 #a b c ltab ltbc; nelim ltbc; /2/; nqed.330 331 ntheorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.332 #n m lenm; nelim lenm; /2/; nqed.333 334 ntheorem le_one_n : ∀n:Pos. one ≤ n.335 napply pos_elim; /2/; nqed.336 337 ntheorem le_n_succn : ∀n:Pos. n ≤ succ n.338 /2/; nqed.339 340 ntheorem le_pred_n : ∀n:Pos. pred n ≤ n.341 napply pos_elim; //; nqed.342 343 ntheorem monotonic_pred: monotonic Pos le pred.344 #n m lenm; nelim lenm; /2/;nqed.345 346 ntheorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.347 /2/; nqed.338 theorem transitive_le: transitive Pos le. 339 #a #b #c #leab #lebc elim lebc; /2/; qed. 340 341 theorem transitive_lt: transitive Pos lt. 342 #a #b #c #ltab #ltbc elim ltbc; /2/; qed. 343 344 theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m. 345 #n #m #lenm elim lenm; /2/; qed. 346 347 theorem le_one_n : ∀n:Pos. one ≤ n. 348 @pos_elim /2/; qed. 349 350 theorem le_n_succn : ∀n:Pos. n ≤ succ n. 351 /2/; qed. 352 353 theorem le_pred_n : ∀n:Pos. pred n ≤ n. 354 @pos_elim //; qed. 355 356 theorem monotonic_pred: monotonic Pos le pred. 357 #n #m #lenm elim lenm; /2/;qed. 358 359 theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m. 360 /2/; qed. 348 361 349 362 (* lt vs. le *) 350 ntheorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.351 #n ; @; #H; ninversion H; /2/; nqed.352 353 ntheorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.354 /3/; nqed.355 356 ntheorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.357 /3/; nqed.358 359 ntheorem decidable_le: ∀n,m:Pos. decidable (n≤m).360 napply pos_elim2; #n;/2/;361 #m ; *; /3/; nqed.362 363 ntheorem decidable_lt: ∀n,m:Pos. decidable (n < m).364 #n ; #m; napply decidable_le ; nqed.365 366 ntheorem not_le_succ_n: ∀n:Pos. succ n ≰ n.367 napply pos_elim;//;368 #m IH; napply not_le_to_not_le_succ_succ;//;369 nqed.370 371 ntheorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.372 napply pos_elim2; #n; 373 ##[#abs; napply False_ind;/2/;374 ##/2/;375 ###m;#Hind;#HnotleSS; napply le_succ_succ;/3/;376 ##]377 nqed.378 379 ntheorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.380 #n m Hltnm; nelim Hltnm;381 ##[ //382 ## #p H; napply not_to_not;/2/;383 ##] nqed.384 385 ntheorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.386 /4/; nqed.387 388 389 ntheorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.390 #n ; #m; #H;napply lt_to_not_le; /2/;nqed.363 theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one. 364 #n % #H inversion H /2/; qed. 365 366 theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m. 367 /3/; qed. 368 369 theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m. 370 /3/; qed. 371 372 theorem decidable_le: ∀n,m:Pos. decidable (n≤m). 373 @pos_elim2 #n /2/; 374 #m *; /3/; qed. 375 376 theorem decidable_lt: ∀n,m:Pos. decidable (n < m). 377 #n #m @decidable_le qed. 378 379 theorem not_le_succ_n: ∀n:Pos. succ n ≰ n. 380 @pos_elim //; 381 #m #IH @not_le_to_not_le_succ_succ //; 382 qed. 383 384 theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n. 385 @pos_elim2 #n 386 [#abs @False_ind /2/; 387 /2/; 388 #m #Hind #HnotleSS @le_succ_succ /3/; 389 ] 390 qed. 391 392 theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n. 393 #n #m #Hltnm elim Hltnm; 394 [ // 395  #p #H @not_to_not /2/; 396 ] qed. 397 398 theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n. 399 /4/; qed. 400 401 402 theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n. 403 #n #m #H @lt_to_not_le /2/;qed. 391 404 392 405 (* lt and le trans *) 393 406 394 ntheorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.395 #n ; #m; #p; #H; #H1; nelim H1; /2/; nqed.396 397 ntheorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.398 #n ; #m; #p; #H; nelim H; /3/; nqed.399 400 ntheorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.401 /2/; nqed.402 403 ntheorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.404 /2/; nqed.405 406 ntheorem lt_one_n_elim: ∀n:Pos. one < n →407 theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p. 408 #n #m #p #H #H1 elim H1; /2/; qed. 409 410 theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p. 411 #n #m #p #H elim H; /3/; qed. 412 413 theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m. 414 /2/; qed. 415 416 theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m. 417 /2/; qed. 418 419 theorem lt_one_n_elim: ∀n:Pos. one < n → 407 420 ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n. 408 napply pos_elim; //; #abs; napply False_ind;/2/;409 nqed.421 @pos_elim //; #abs @False_ind /2/; 422 qed. 410 423 411 424 (* le to lt or eq *) 412 ntheorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.413 #n ; #m; #lenm; nelim lenm; /3/; nqed.425 theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m. 426 #n #m #lenm elim lenm; /3/; qed. 414 427 415 428 (* not eq *) 416 ntheorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.417 #n ; #m; #H; napply not_to_not;/2/; nqed.418 419 ntheorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.420 #n ; #m; #Hneq; #Hle; ncases (le_to_or_lt_eq ?? Hle); //;421 #Heq ; /3/; nqed.429 theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m. 430 #n #m #H @not_to_not /2/; qed. 431 432 theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m. 433 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //; 434 #Heq /3/; qed. 422 435 423 436 (* le elimination *) 424 ntheorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.425 napply pos_cases; //; #a ; #abs; 426 napply False_ind; /2/;nqed.427 428 ntheorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.429 napply pos_cases; //; #a; #abs; 430 napply False_ind; /2/; nqed.431 432 ntheorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m →437 theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n. 438 @pos_cases //; #a ; #abs 439 @False_ind /2/;qed. 440 441 theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n. 442 @pos_cases //; #a #abs 443 @False_ind /2/; qed. 444 445 theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m → 433 446 ∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P. 434 #n ; #m; #Hle; #P; nelim Hle; /3/; nqed.447 #n #m #Hle #P elim Hle; /3/; qed. 435 448 436 449 (* le and eq *) 437 450 438 ntheorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.439 napply pos_elim2;/4/;440 nqed.441 442 ntheorem lt_one_S : ∀n:Pos. one < succ n.443 /2/; nqed.451 theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m. 452 @pos_elim2 /4/; 453 qed. 454 455 theorem lt_one_S : ∀n:Pos. one < succ n. 456 /2/; qed. 444 457 445 458 (* well founded induction principles *) 446 459 447 ntheorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop.460 theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop. 448 461 (∀m.(∀p. p < m → P p) → P m) → P n. 449 #n ; #P; #H;450 ncut (∀q:Pos. q ≤ n → P q);/2/;451 napply (pos_elim … n); 452 ##[#q; #HleO;(* applica male *)453 napply (le_n_one_elim ? HleO);454 napply H; #p; #ltpO;455 napply False_ind;/2/; (* 3 *)456 ###p; #Hind; #q; #HleS;457 napply H; #a; #lta; napply Hind;458 napply le_S_S_to_le;/2/;459 ##]460 nqed.462 #n #P #H 463 cut (∀q:Pos. q ≤ n → P q);/2/; 464 @(pos_elim … n) 465 [#q #HleO (* applica male *) 466 @(le_n_one_elim ? HleO) 467 @H #p #ltpO 468 @False_ind /2/; (* 3 *) 469 #p #Hind #q #HleS 470 @H #a #lta @Hind 471 @le_S_S_to_le /2/; 472 ] 473 qed. 461 474 462 475 (*********************** monotonicity ***************************) 463 ntheorem monotonic_le_plus_r:476 theorem monotonic_le_plus_r: 464 477 ∀n:Pos.monotonic Pos le (λm.n + m). 465 #n ; #a; #b; napply (pos_elim … n); nnormalize; /2/;466 #m ; #H; #leab;/3/; nqed.467 468 ntheorem monotonic_le_plus_l:478 #n #a #b @(pos_elim … n) normalize; /2/; 479 #m #H #leab /3/; qed. 480 481 theorem monotonic_le_plus_l: 469 482 ∀m:Pos.monotonic Pos le (λn.n + m). 470 /2/; nqed.471 472 ntheorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2 → m1 ≤ m2483 /2/; qed. 484 485 theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2 → m1 ≤ m2 473 486 → n1 + m1 ≤ n2 + m2. 474 #n1 ; #n2; #m1; #m2; #len; #lem; napply (transitive_le ? (n1+m2));475 /2/; nqed.476 477 ntheorem le_plus_n :∀n,m:Pos. m ≤ n + m.478 /3/; nqed.479 480 nlemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.481 /2/; nqed.482 483 nlemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.484 /2/; nqed.485 486 ntheorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.487 /2/; nqed.488 489 ntheorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.490 //; nqed.491 492 ntheorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.493 napply pos_elim; nnormalize; /3/; nqed.494 495 ntheorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.496 /2/; nqed.487 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) 488 /2/; qed. 489 490 theorem le_plus_n :∀n,m:Pos. m ≤ n + m. 491 /3/; qed. 492 493 lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m. 494 /2/; qed. 495 496 lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m. 497 /2/; qed. 498 499 theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n. 500 /2/; qed. 501 502 theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n. 503 //; qed. 504 505 theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m. 506 @pos_elim normalize; /3/; qed. 507 508 theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m. 509 /2/; qed. 497 510 498 511 (* plus & lt *) 499 512 500 ntheorem monotonic_lt_plus_r:513 theorem monotonic_lt_plus_r: 501 514 ∀n:Pos.monotonic Pos lt (λm.n+m). 502 /2/; nqed.503 504 ntheorem monotonic_lt_plus_l:515 /2/; qed. 516 517 theorem monotonic_lt_plus_l: 505 518 ∀n:Pos.monotonic Pos lt (λm.m+n). 506 /2/; nqed.507 508 ntheorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.509 #n ; #m; #p; #q; #ltnm; #ltpq;510 napply (transitive_lt ? (n+q));/2/; nqed.511 512 ntheorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.513 #n m p H; napply (le_to_lt_to_lt … H);514 /2/; nqed.515 516 ntheorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.517 /2/; nqed.518 519 ntheorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.520 /2/; nqed.519 /2/; qed. 520 521 theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q. 522 #n #m #p #q #ltnm #ltpq 523 @(transitive_lt ? (n+q)) /2/; qed. 524 525 theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p. 526 #n #m #p #H @(le_to_lt_to_lt … H) 527 /2/; qed. 528 529 theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q. 530 /2/; qed. 531 532 theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q. 533 /2/; qed. 521 534 522 535 (* times *) 523 ntheorem monotonic_le_times_r:536 theorem monotonic_le_times_r: 524 537 ∀n:Pos.monotonic Pos le (λm. n * m). 525 #n ; #x; #y; #lexy; napply (pos_elim … n); nnormalize;//;(* lento /2/;*)526 #a ; #lea;/2/;527 nqed.528 529 ntheorem le_times: ∀n1,n2,m1,m2:Pos.538 #n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*) 539 #a #lea /2/; 540 qed. 541 542 theorem le_times: ∀n1,n2,m1,m2:Pos. 530 543 n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2. 531 #n1 ; #n2; #m1; #m2; #len; #lem;532 napply (transitive_le ? (n1*m2));(* /2/ slow *)533 ##[ napply monotonic_le_times_r;//;534 ## napplyS monotonic_le_times_r;//;535 ##]536 nqed.537 538 ntheorem lt_times_n: ∀n,m:Pos. m ≤ n*m.539 #n m; /2/; nqed.540 541 ntheorem le_times_to_le:544 #n1 #n2 #m1 #m2 #len #lem 545 @(transitive_le ? (n1*m2)) (* /2/ slow *) 546 [ @monotonic_le_times_r //; 547  applyS monotonic_le_times_r;//; 548 ] 549 qed. 550 551 theorem lt_times_n: ∀n,m:Pos. m ≤ n*m. 552 #n #m /2/; qed. 553 554 theorem le_times_to_le: 542 555 ∀a,n,m:Pos. a * n ≤ a * m → n ≤ m. 543 #a ; napply pos_elim2; nnormalize;544 ##[//;545 ###n; nrewrite > (times_n_one …); nrewrite < (times_n_succm …);546 #H ; napply False_ind;547 nelim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/;548 ###n; #m; #H; #le;549 napply le_succ_succ; napply H;/2/;550 ##]551 nqed.552 553 ntheorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m.554 #n ; #m; #lenm;(* interessante *)555 napplyS (le_plus n m); //; nqed.556 #a @pos_elim2 normalize; 557 [//; 558 #n >(times_n_one …) <(times_n_succm …) 559 #H @False_ind 560 elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/; 561 #n #m #H #le 562 @le_succ_succ @H /2/; 563 ] 564 qed. 565 566 theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m. 567 #n #m #lenm (* interessante *) 568 applyS (le_plus n m); //; qed. 556 569 557 570 (* prove injectivity of times from above *) 558 ntheorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m).559 #n m p H; napply le_to_le_to_eq;571 theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). 572 #n #m #p #H @le_to_le_to_eq 560 573 /2/; 561 nqed.562 563 ntheorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n).564 /2/; nqed.574 qed. 575 576 theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). 577 /2/; qed. 565 578 566 579 (* times & lt *) 567 580 568 ntheorem monotonic_lt_times_l:581 theorem monotonic_lt_times_l: 569 582 ∀c:Pos. monotonic Pos lt (λt.(t*c)). 570 #c n m ltnm;571 nelim ltnm; nnormalize;572 ##[/2/;573 ###a; #_; #lt1; napply (transitive_le ??? lt1);//;574 ##]575 nqed.576 577 ntheorem monotonic_lt_times_r:583 #c #n #m #ltnm 584 elim ltnm; normalize; 585 [/2/; 586 #a #_ #lt1 @(transitive_le ??? lt1) //; 587 ] 588 qed. 589 590 theorem monotonic_lt_times_r: 578 591 ∀c:Pos. monotonic Pos lt (λt.(c*t)). 579 #a b c H;580 nrewrite > (symmetric_times a b); nrewrite > (symmetric_times a c); 581 /2/; nqed.582 583 ntheorem lt_to_le_to_lt_times:592 #a #b #c #H 593 >(commutative_times a b) >(commutative_times a c) 594 /2/; qed. 595 596 theorem lt_to_le_to_lt_times: 584 597 ∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q. 585 #n ; #m; #p; #q; #ltnm; #lepq;586 napply (le_to_lt_to_lt ? (n*q)); 587 ##[napply monotonic_le_times_r;//;588 ##napply monotonic_lt_times_l;//;589 ##]590 nqed.591 592 ntheorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q.593 #n ; #m; #p; #q; #ltnm; #ltpq;594 napply lt_to_le_to_lt_times;/2/;595 nqed.596 597 ntheorem lt_times_n_to_lt_l:598 #n #m #p #q #ltnm #lepq 599 @(le_to_lt_to_lt ? (n*q)) 600 [@monotonic_le_times_r //; 601 @monotonic_lt_times_l //; 602 ] 603 qed. 604 605 theorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q. 606 #n #m #p #q #ltnm #ltpq 607 @lt_to_le_to_lt_times /2/; 608 qed. 609 610 theorem lt_times_n_to_lt_l: 598 611 ∀n,p,q:Pos. p*n < q*n → p < q. 599 #n ; #p; #q; #Hlt;600 nelim (decidable_lt p q);//;601 #nltpq ; napply False_ind;602 napply (absurd ? ? (lt_to_not_le ? ? Hlt)); 603 napplyS monotonic_le_times_r;/2/;604 nqed.605 606 ntheorem lt_times_n_to_lt_r:612 #n #p #q #Hlt 613 elim (decidable_lt p q);//; 614 #nltpq @False_ind 615 @(absurd ? ? (lt_to_not_le ? ? Hlt)) 616 applyS monotonic_le_times_r;/2/; 617 qed. 618 619 theorem lt_times_n_to_lt_r: 607 620 ∀n,p,q:Pos. n*p < n*q → p < q. 608 /2/; nqed.621 /2/; qed. 609 622 610 623 (**** minus ****) 611 624 612 ninductive minusresult : Type≝625 inductive minusresult : Type[0] ≝ 613 626  MinusNeg: minusresult 614 627  MinusZero: minusresult 615 628  MinusPos: Pos → minusresult. 616 629 617 nlet rec partial_minus (n,m:Pos) : minusresult ≝630 let rec partial_minus (n,m:Pos) : minusresult ≝ 618 631 match n with 619 632 [ one ⇒ match m with [ one ⇒ MinusZero  _ ⇒ MinusNeg ] … … 636 649 ]. 637 650 638 nremark testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; nqed.639 nremark testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; nqed.640 nremark testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; nqed.641 nremark testminus3: partial_minus (p0 one) one = MinusPos one. //; nqed.642 nremark testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; nqed.643 644 ndefinition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p  _ ⇒ one ].651 example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed. 652 example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed. 653 example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed. 654 example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed. 655 example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed. 656 657 definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p  _ ⇒ one ]. 645 658 646 659 interpretation "natural minus" 'minus x y = (minus x y). 647 660 648 nlemma partialminus_S: ∀n,m:Pos.661 lemma partialminus_S: ∀n,m:Pos. 649 662 match partial_minus (succ n) m with 650 663 [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero  _ ⇒ partial_minus n m = MinusPos (pred p) ] 651 664  _ ⇒ partial_minus n m = MinusNeg 652 665 ]. 653 #n ; nelim n;654 ##[ #m; ncases m;655 ##[ //;656 ## ##2,3: #m'; ncases m'; //;657 ##]666 #n elim n; 667 [ #m cases m; 668 [ //; 669  2,3: #m' cases m'; //; 670 ] 658 671 (* The other two cases are the same. I'd combine them, but the numbering 659 672 would be even more horrific. *) 660 ## #n' IH m; ncases m;661 ##[ nnormalize; nrewrite < (pred_succ_n n'); ncases n'; //;662 ## ##2,3: #m'; nnormalize; nlapply (IH m'); ncases (partial_minus (succ n') m');663 ##[ ##1,2,4,5: nnormalize; #H; nrewrite > H;//;664 ## ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H;//;665 ## ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H;//;666 ##]667 ##]668 ##]669 ## #n' IH m; ncases m;670 ##[ nnormalize; nrewrite < (pred_succ_n n'); ncases n'; //;671 ## ##2,3: #m'; nnormalize; nlapply (IH m'); ncases (partial_minus (succ n') m');672 ##[ ##1,2,4,5: nnormalize; #H; nrewrite > H;//;673 ## ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H;//;674 ## ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H;//;675 ##]676 ##]677 ##]678 ##] nqed.679 680 nlemma partialminus_n_S: ∀n,m:Pos.673  #n' #IH #m cases m; 674 [ normalize; <(pred_succ_n n') cases n'; //; 675  2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); 676 [ 1,2,4,5: normalize; #H >H //; 677  3,6: #p cases p; [ 1,4: normalize; #H >H //; 678  2,3,5,6: #p' normalize; #H >H //; 679 ] 680 ] 681 ] 682  #n' #IH #m cases m; 683 [ normalize; <(pred_succ_n n') cases n'; //; 684  2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); 685 [ 1,2,4,5: normalize; #H >H //; 686  3,6: #p cases p; [ 1,4: normalize; #H >H //; 687  2,3,5,6: #p' normalize; #H >H //; 688 ] 689 ] 690 ] 691 ] qed. 692 693 lemma partialminus_n_S: ∀n,m:Pos. 681 694 match partial_minus n m with 682 695 [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero … … 685 698  _ ⇒ partial_minus n (succ m) = MinusNeg 686 699 ]. 687 #n ; nelim n;688 ##[ #m; ncases m; //;700 #n elim n; 701 [ #m cases m; //; 689 702 (* Again, lots of unnecessary duplication! *) 690 ## #n' IH m; ncases m;691 ##[ nnormalize; ncases n'; //;692 ## #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');693 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;694 ## #p; ncases p; nnormalize; ##[ #H; nrewrite > H;//;695 ## ##2,3: #p'; #H; nrewrite > H;//;696 ##]697 ##]698 ## #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');699 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;700 ## #p; ncases p; nnormalize; ##[ #H; nrewrite > H;//;701 ## ##2,3: #p'; #H; nrewrite > H;//;702 ##]703 ##]704 ##]705 ## #n' IH m; ncases m;706 ##[ nnormalize; ncases n'; //;707 ## #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');708 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;709 ## #p; ncases p; nnormalize; ##[ #H; nrewrite > H;//;710 ## ##2,3: #p'; #H; nrewrite > H;//;711 ##]712 ##]713 ## #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');714 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;715 ## #p; ncases p; nnormalize; ##[ #H; nrewrite > H;//;716 ## ##2,3: #p'; #H; nrewrite > H;//;717 ##]718 ##]719 ##]720 ##] nqed.721 722 ntheorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m.723 #n ; nelim n;724 ##[ #m; ncases m;725 ##[ //;726 ## ##2,3: #m'; ncases m'; //;727 ##]728 ## #n' IH m; ncases m;729 ##[ nnormalize; ncases n'; /2/; nnormalize; #n''; nrewrite < (pred_succ_n n''); ncases n'';//;730 ## #m'; nnormalize; nrewrite > (IH ?);//;731 ## #m'; nnormalize; nlapply (partialminus_S n' m'); ncases (partial_minus (succ n') m');732 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;733 ## #p; ncases p; ##[ nnormalize; #H; nrewrite > H;//;734 ## ##2,3: #p';nnormalize; #H; nrewrite > H;//;735 ##]736 ##]737 ##]738 ## #n' IH m; ncases m;739 ##[ nnormalize; ncases n'; /2/;740 ## #m'; nnormalize; nlapply (partialminus_n_S n' m'); ncases (partial_minus n' m');741 ##[ ##1,2: nnormalize; #H; nrewrite > H;//;742 ## #p; ncases p; ##[ nnormalize; #H; nrewrite > H;//;743 ## ##2,3: #p';nnormalize; #H; nrewrite > H;//;744 ##]745 ##]746 ## #m'; nnormalize; nrewrite > (IH ?);//;747 ##]748 ##] nqed.749 750 ntheorem minus_S_S: ∀n,m:Pos. (succ n)  (succ m) = nm.751 #n m; nnormalize; nrewrite > (partialminus_S_S n m); //; nqed.752 753 ntheorem minus_one_n: ∀n:Pos.one=onen.754 #n ; ncases n; //; nqed.755 756 ntheorem minus_n_one: ∀n:Pos.pred n=none.757 #n ; ncases n; //; nqed.758 759 nlemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero.760 #n ; nelim n;761 ##[ //;762 ## ##2,3: nnormalize; #n' IH; nrewrite > IH;//763 ##] nqed.764 765 ntheorem minus_n_n: ∀n:Pos.one=nn.766 #n ; nnormalize; nrewrite > (partial_minus_n_n n);//;767 nqed.768 769 ntheorem minus_Sn_n: ∀n:Pos. one = (succ n)n.770 #n ; ncut (partial_minus (succ n) n = MinusPos one);771 ##[ nelim n;772 ##[ //;773 ## nnormalize; #n' IH; nrewrite > IH;//;774 ## nnormalize; #n' IH; nrewrite > (partial_minus_n_n n');//;775 ##]776 ## #H; nnormalize; nrewrite > H;//;777 ##] nqed.778 779 ntheorem minus_Sn_m: ∀m,n:Pos. m < n → succ n m = succ (nm).703  #n' #IH #m cases m; 704 [ normalize; cases n'; //; 705  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); 706 [ 1,2: normalize; #H >H //; 707  #p cases p; normalize; [ #H >H //; 708  2,3: #p' #H >H //; 709 ] 710 ] 711  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); 712 [ 1,2: normalize; #H >H //; 713  #p cases p; normalize; [ #H >H //; 714  2,3: #p' #H >H //; 715 ] 716 ] 717 ] 718  #n' #IH #m cases m; 719 [ normalize; cases n'; //; 720  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); 721 [ 1,2: normalize; #H >H //; 722  #p cases p; normalize; [ #H >H //; 723  2,3: #p' #H >H //; 724 ] 725 ] 726  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); 727 [ 1,2: normalize; #H >H //; 728  #p cases p; normalize; [ #H >H //; 729  2,3: #p' #H >H //; 730 ] 731 ] 732 ] 733 ] qed. 734 735 theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m. 736 #n elim n; 737 [ #m cases m; 738 [ //; 739  2,3: #m' cases m'; //; 740 ] 741  #n' #IH #m cases m; 742 [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//; 743  #m' normalize; >(IH ?) //; 744  #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m'); 745 [ 1,2: normalize; #H >H //; 746  #p cases p; [ normalize; #H >H //; 747  2,3: #p' normalize; #H >H //; 748 ] 749 ] 750 ] 751  #n' #IH #m cases m; 752 [ normalize; cases n'; /2/; 753  #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m'); 754 [ 1,2: normalize; #H >H //; 755  #p cases p; [ normalize; #H >H //; 756  2,3: #p' normalize; #H >H //; 757 ] 758 ] 759  #m' normalize; >(IH ?) //; 760 ] 761 ] qed. 762 763 theorem minus_S_S: ∀n,m:Pos. (succ n)  (succ m) = nm. 764 #n #m normalize; >(partialminus_S_S n m) //; qed. 765 766 theorem minus_one_n: ∀n:Pos.one=onen. 767 #n cases n; //; qed. 768 769 theorem minus_n_one: ∀n:Pos.pred n=none. 770 #n cases n; //; qed. 771 772 lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero. 773 #n elim n; 774 [ //; 775  2,3: normalize; #n' #IH >IH // 776 ] qed. 777 778 theorem minus_n_n: ∀n:Pos.one=nn. 779 #n normalize; >(partial_minus_n_n n) //; 780 qed. 781 782 theorem minus_Sn_n: ∀n:Pos. one = (succ n)n. 783 #n cut (partial_minus (succ n) n = MinusPos one); 784 [ elim n; 785 [ //; 786  normalize; #n' #IH >IH //; 787  normalize; #n' #IH >(partial_minus_n_n n') //; 788 ] 789  #H normalize; >H //; 790 ] qed. 791 792 theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n m = succ (nm). 780 793 (* qualcosa da capire qui 781 #n ; #m; #lenm; nelim lenm; napplyS refl_eq. *)782 napply pos_elim2; 783 ##[#n H; napply (lt_one_n_elim n H);//;784 ###n; #abs; napply False_ind;/2/785 ###n; #m; #Hind; #c; napplyS Hind; /2/;786 ##]787 nqed.788 789 ntheorem not_eq_to_le_to_le_minus:794 #n #m #lenm elim lenm; napplyS refl_eq. *) 795 @pos_elim2 796 [#n #H @(lt_one_n_elim n H) //; 797 #n #abs @False_ind /2/ 798 #n #m #Hind #c applyS Hind; /2/; 799 ] 800 qed. 801 802 theorem not_eq_to_le_to_le_minus: 790 803 ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m  one. 791 #n ; napply pos_cases; //; #m;792 #H ; #H1; napply le_S_S_to_le;793 napplyS (not_eq_to_le_to_lt n (succ m) H H1);794 nqed.795 796 ntheorem eq_minus_S_pred: ∀n,m:Pos. n  (succ m) = pred(n m).797 napply pos_elim2; 798 ##[ #n; ncases n; nnormalize; //;799 ## #n; napply (pos_elim … n);//;800 ## //;801 ##] nqed.802 803 nlemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m).804 #n m H;805 napply (lt_one_n_elim … H);/3/;806 nqed.807 808 ntheorem plus_minus:804 #n @pos_cases //; #m 805 #H #H1 @le_S_S_to_le 806 applyS (not_eq_to_le_to_lt n (succ m) H H1); 807 qed. 808 809 theorem eq_minus_S_pred: ∀n,m:Pos. n  (succ m) = pred(n m). 810 @pos_elim2 811 [ #n cases n; normalize; //; 812  #n @(pos_elim … n) //; 813  //; 814 ] qed. 815 816 lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m). 817 #n #m #H 818 @(lt_one_n_elim … H) /3/; 819 qed. 820 821 theorem plus_minus: 809 822 ∀m,n,p:Pos. m < n → (nm)+p = (n+p)m. 810 napply pos_elim2; 811 ##[ #n p H; nrewrite < (minus_n_one ?); nrewrite < (minus_n_one ?);/2/;812 ###n; #p; #abs; napply False_ind;/2/;813 ###n m IH p H; nrewrite > (eq_minus_S_pred …); nrewrite > (eq_minus_S_pred …);814 ncut (n<m); ##[ /2/ ##] #H';815 nrewrite > (pred_Sn_plus …);816 ##[ nrewrite > (minus_Sn_m …);/2/;817 nrewrite < (pluss_succn_m …);818 nrewrite < (pluss_succn_m …);819 nrewrite > (minus_Sn_m …);820 ##[ nrewrite < (pred_succ_n …);821 nrewrite < (pred_succ_n …);822 napply IH;/2/;823 ## /2/;824 ##]825 ## nrewrite > (minus_Sn_m … H');//;826 ##]827 ##] nqed.823 @pos_elim2 824 [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/; 825 #n #p #abs @False_ind /2/; 826 #n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …) 827 cut (n<m); [ /2/ ] #H' 828 >(pred_Sn_plus …) 829 [ >(minus_Sn_m …) /2/; 830 <(pluss_succn_m …) 831 <(pluss_succn_m …) 832 >(minus_Sn_m …) 833 [ <(pred_succ_n …) 834 <(pred_succ_n …) 835 @IH /2/; 836  /2/; 837 ] 838  >(minus_Sn_m … H') //; 839 ] 840 ] qed. 828 841 829 842 (* XXX: putting this in the appropriate case screws up auto?! *) 830 ntheorem succ_plus_one: ∀n. succ n = n + one.831 #n ; nelim n; //; nqed.832 833 ntheorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p).834 #p ; nelim p; nnormalize;835 ##[ //;836 ## #q IH; nrewrite < (plus_n_O …); nrewrite < (plus_n_O …); 837 nrewrite > IH; nrewrite < (plus_n_Sm …);//;838 ## //;839 ##] nqed.840 841 ntheorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.842 #n ; nelim n; //; nqed.843 844 ntheorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)m.845 #n ; napply pos_elim;846 ##[ //;847 ## #m IH; nrewrite < (plus_n_succm …); 848 nrewrite > (eq_minus_S_pred …);849 nrewrite > (minus_Sn_m …);/2/;850 ##] nqed.851 852 ntheorem plus_minus_m_m: ∀n,m:Pos.843 theorem succ_plus_one: ∀n. succ n = n + one. 844 #n elim n; //; qed. 845 846 theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p). 847 #p elim p; normalize; 848 [ //; 849  #q #IH <(plus_n_O …) <(plus_n_O …) 850 >IH <(plus_n_Sm …) //; 851  //; 852 ] qed. 853 854 theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. 855 #n elim n; //; qed. 856 857 theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)m. 858 #n @pos_elim 859 [ //; 860  #m #IH <(plus_n_succm …) 861 >(eq_minus_S_pred …) 862 >(minus_Sn_m …) /2/; 863 ] qed. 864 865 theorem plus_minus_m_m: ∀n,m:Pos. 853 866 m < n → n = (nm)+m. 854 #n ; #m; #lemn; napplyS sym_eq;855 napplyS (plus_minus m n m); //; nqed.856 857 ntheorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (nm)+m.858 napply pos_elim; 859 ##[//860 ###a; #Hind; napply pos_cases;//;861 #n ;862 nrewrite > (minus_S_S …);867 #n #m #lemn applyS sym_eq; 868 applyS (plus_minus m n m); //; qed. 869 870 theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (nm)+m. 871 @pos_elim 872 [// 873 #a #Hind @pos_cases //; 874 #n 875 >(minus_S_S …) 863 876 /2/; 864 ##]865 nqed.866 867 ntheorem minus_to_plus :∀n,m,p:Pos.877 ] 878 qed. 879 880 theorem minus_to_plus :∀n,m,p:Pos. 868 881 m < n → nm = p → n = m+p. 869 #n ; #m; #p; #lemn; #eqp; napplyS plus_minus_m_m; //;870 nqed.871 872 ntheorem plus_to_minus :∀n,m,p:Pos.n = m+p → nm = p.882 #n #m #p #lemn #eqp applyS plus_minus_m_m; //; 883 qed. 884 885 theorem plus_to_minus :∀n,m,p:Pos.n = m+p → nm = p. 873 886 (* /4/ done in 43.5 *) 874 #n ; #m; #p; #eqp;875 napply sym_eq; 876 napplyS (minus_plus_m_m p m);877 nqed.878 879 ntheorem minus_pred_pred : ∀n,m:Pos. one < n → one < m →887 #n #m #p #eqp 888 @sym_eq 889 applyS (minus_plus_m_m p m); 890 qed. 891 892 theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → 880 893 pred n  pred m = n  m. 881 #n ; #m; #posn; #posm;882 napply (lt_one_n_elim n posn); 883 napply (lt_one_n_elim m posm);//.884 nqed.894 #n #m #posn #posm 895 @(lt_one_n_elim n posn) 896 @(lt_one_n_elim m posm) //. 897 qed. 885 898 886 899 (* monotonicity and galois *) 887 900 888 ntheorem monotonic_le_minus_l:901 theorem monotonic_le_minus_l: 889 902 ∀p,q,n:Pos. q ≤ p → qn ≤ pn. 890 napply pos_elim2; #p; #q; 891 ##[#lePO; napply (le_n_one_elim ? lePO);//;892 ##//;893 ###Hind; napply pos_cases;894 ##[/2/;895 ###a; #leSS; nrewrite > (minus_S_S …); nrewrite > (minus_S_S …); napply Hind;/2/;896 ##]897 ##]898 nqed.899 900 ntheorem le_minus_to_plus: ∀n,m,p:Pos. nm ≤ p → n≤ p+m.901 #n ; #m; #p; #lep;902 napply transitive_le; 903 ##[##napply le_plus_minus_m_m904 ##napply monotonic_le_plus_l;//;905 ##]906 nqed.907 908 ntheorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → nm ≤ p.909 #n ; #m; #p; #lep;903 @pos_elim2 #p #q 904 [#lePO @(le_n_one_elim ? lePO) //; 905 //; 906 #Hind @pos_cases 907 [/2/; 908 #a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/; 909 ] 910 ] 911 qed. 912 913 theorem le_minus_to_plus: ∀n,m,p:Pos. nm ≤ p → n≤ p+m. 914 #n #m #p #lep 915 @transitive_le 916 [apply le_plus_minus_m_m 917 @monotonic_le_plus_l //; 918 ] 919 qed. 920 921 theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → nm ≤ p. 922 #n #m #p #lep 910 923 (* bello *) 911 napplyS monotonic_le_minus_l;//;924 applyS monotonic_le_minus_l;//; 912 925 (* /2/; *) 913 nqed.914 915 ntheorem monotonic_le_minus_r:926 qed. 927 928 theorem monotonic_le_minus_r: 916 929 ∀p,q,n:Pos. q ≤ p → np ≤ nq. 917 #p ; #q; #n; #lepq;918 napply le_plus_to_minus; 919 napply (transitive_le ??? (le_plus_minus_m_m ? q));/2/;920 nqed.930 #p #q #n #lepq 931 @le_plus_to_minus 932 @(transitive_le ??? (le_plus_minus_m_m ? q)) /2/; 933 qed. 921 934 922 935 (*********************** boolean arithmetics ********************) 923 936 include "basics/bool.ma". 924 937 925 nlet rec eqb n m ≝938 let rec eqb n m ≝ 926 939 match n with 927 940 [ one ⇒ match m with [ one ⇒ true  _ ⇒ false] … … 929 942  p1 p ⇒ match m with [ p1 q ⇒ eqb p q  _ ⇒ false] 930 943 ]. 931 932 ntheorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.944 945 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop. 933 946 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 934 #n; nelim n; 935 ##[ #m; ncases m; nnormalize; 936 ##[ /2/; 937 ## ##2,3: #m' P t f; napply f; @; #H; ndestruct; 938 ##] 939 ## #n' IH m; ncases m; nnormalize; 940 ##[ #P t f; napply f; @; #H; ndestruct; 941 ## #m' P t f; napply IH; 942 ##[ /2/; 943 ## (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct; 944 nelim ne; /2/; 945 ##] 946 ## #m' P t f; napply f; @; #H; ndestruct; 947 ##] 948 ## #n' IH m; ncases m; nnormalize; 949 ##[ #P t f; napply f; @; #H; ndestruct; 950 ## #m' P t f; napply f; @; #H; ndestruct; 951 ## #m' P t f; napply IH; 952 ##[ /2/; 953 ## (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct; 954 nelim ne; /2/; 955 ##] 956 ##] 957 ##] nqed. 958 959 ntheorem eqb_n_n: ∀n:Pos. eqb n n = true. 960 #n; nelim n; nnormalize; //. 961 nqed. 962 963 ntheorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. 964 #n; #m; napply (eqb_elim n m);//; 965 #_; #abs; napply False_ind; /2/; 966 nqed. 967 968 ntheorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. 969 #n; #m; napply (eqb_elim n m);/2/; 970 nqed. 971 972 ntheorem eq_to_eqb_true: ∀n,m:Pos. 947 #n elim n; 948 [ #m cases m normalize 949 [ /2/ 950  2,3: #m' #P #t #f @f % #H destruct 951 ] 952  #n' #IH #m cases m normalize 953 [ #P #t #f @f % #H destruct 954  #m' #P #t #f @IH 955 [ /2/ 956  * #ne @f % #e @ne destruct @refl 957 ] 958  #m' #P #t #f @f % #H destruct; 959 ] 960  #n' #IH #m cases m; normalize; 961 [ #P #t #f @f % #H destruct; 962  #m' #P #t #f @f % #H destruct; 963  #m' #P #t #f @IH 964 [ /2/; 965  * #ne @f % #e @ne destruct @refl 966 ] 967 ] 968 ] qed. 969 970 theorem eqb_n_n: ∀n:Pos. eqb n n = true. 971 #n elim n; normalize; //. 972 qed. 973 974 theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. 975 #n #m @(eqb_elim n m) //; 976 #_ #abs @False_ind /2/; 977 qed. 978 979 theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. 980 #n #m @(eqb_elim n m) /2/; 981 qed. 982 983 theorem eq_to_eqb_true: ∀n,m:Pos. 973 984 n = m → eqb n m = true. 974 //; nqed.975 976 ntheorem not_eq_to_eqb_false: ∀n,m:Pos.985 //; qed. 986 987 theorem not_eq_to_eqb_false: ∀n,m:Pos. 977 988 n ≠ m → eqb n m = false. 978 #n ; #m; #noteq;979 napply eqb_elim;//;980 #Heq ; napply False_ind;/2/;981 nqed.982 983 nlet rec leb n m ≝989 #n #m #noteq 990 @eqb_elim //; 991 #Heq @False_ind /2/; 992 qed. 993 994 let rec leb n m ≝ 984 995 match partial_minus n m with 985 996 [ MinusNeg ⇒ true … … 988 999 ]. 989 1000 990 nlemma leb_unfold_hack: ∀n,m:Pos. leb n m =1001 lemma leb_unfold_hack: ∀n,m:Pos. leb n m = 991 1002 match partial_minus n m with 992 1003 [ MinusNeg ⇒ true 993 1004  MinusZero ⇒ true 994 1005  MinusPos _ ⇒ false 995 ]. #n m; (* XXX: why on earth do I need to case split? *) ncases n; //; nqed.996 997 ntheorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop.1006 ]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed. 1007 1008 theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. 998 1009 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). 999 napply pos_elim2; 1000 ##[ #n; ncases n; nnormalize; /2/;1001 ## #n; ncases n; nnormalize;1002 ##[ /2/;1003 ## ##2,3: #m' P t f; napply f; /2/; @; #H; ninversion H;1004 ##[ #H'; ndestruct;1005 ## #p;/2/;1006 ##]1007 ##]1008 ## #n m IH P t f; nrewrite > (leb_unfold_hack …); 1009 nrewrite > (partialminus_S_S n m);1010 nrewrite < (leb_unfold_hack …);1011 napply IH; #H;/3/;1012 ##] nqed.1013 1014 ntheorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m.1015 #n ; #m; napply leb_elim;1016 ##[//;1017 ###_; #abs; napply False_ind;/2/;1018 ##]1019 nqed.1020 1021 ntheorem leb_false_to_not_le:∀n,m:Pos.1010 @pos_elim2 1011 [ #n cases n; normalize; /2/; 1012  #n cases n; normalize; 1013 [ /2/; 1014  2,3: #m' #P #t #f @f /2/; % #H inversion H; 1015 [ #H' destruct; 1016  #p /2/; 1017 ] 1018 ] 1019  #n #m #IH #P #t #f >(leb_unfold_hack …) 1020 >(partialminus_S_S n m) 1021 <(leb_unfold_hack …) 1022 @IH #H /3/; 1023 ] qed. 1024 1025 theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m. 1026 #n #m @leb_elim 1027 [//; 1028 #_ #abs @False_ind /2/; 1029 ] 1030 qed. 1031 1032 theorem leb_false_to_not_le:∀n,m:Pos. 1022 1033 leb n m = false → n ≰ m. 1023 #n ; #m; napply leb_elim;1024 ##[#_; #abs; napply False_ind;/2/;1025 ##//;1026 ##]1027 nqed.1028 1029 ntheorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true.1030 #n ; #m; napply leb_elim;//;1031 #H ; #H1; napply False_ind;/2/;1032 nqed.1033 1034 ntheorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false.1035 #n ; #m; napply leb_elim;//;1036 #H ; #H1; napply False_ind;/2/;1037 nqed.1038 1039 ntheorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false.1040 /3/; nqed.1034 #n #m @leb_elim 1035 [#_ #abs @False_ind /2/; 1036 //; 1037 ] 1038 qed. 1039 1040 theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true. 1041 #n #m @leb_elim //; 1042 #H #H1 @False_ind /2/; 1043 qed. 1044 1045 theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false. 1046 #n #m @leb_elim //; 1047 #H #H1 @False_ind /2/; 1048 qed. 1049 1050 theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. 1051 /3/; qed. 1041 1052 1042 1053 1043 1054 (***** comparison *****) 1044 1055 1045 ndefinition pos_compare : Pos → Pos → compare ≝1056 definition pos_compare : Pos → Pos → compare ≝ 1046 1057 λn,m.match partial_minus n m with 1047 1058 [ MinusNeg ⇒ LT … … 1050 1061 ]. 1051 1062 1052 ntheorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ.1053 #n ; nnormalize; nrewrite > (partial_minus_n_n n);1054 //; nqed.1055 1056 ntheorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m).1057 #n m; nnormalize;1058 nrewrite > (partialminus_S_S …); 1063 theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. 1064 #n normalize; >(partial_minus_n_n n) 1065 //; qed. 1066 1067 theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m). 1068 #n #m normalize; 1069 >(partialminus_S_S …) 1059 1070 //; 1060 nqed.1061 1062 ntheorem pos_compare_pred_pred:1071 qed. 1072 1073 theorem pos_compare_pred_pred: 1063 1074 ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m). 1064 #n ;#m;#Hn;#Hm;1065 napply (lt_one_n_elim n Hn); 1066 napply (lt_one_n_elim m Hm); 1067 #p ;#q; nrewrite < (pred_succ_n ?); nrewrite < (pred_succ_n ?);1068 nrewrite < (pos_compare_S_S …);//;1069 nqed.1070 1071 ntheorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT.1072 #n ; nelim n; //; nqed.1073 1074 ntheorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT.1075 #n ; nelim n; //; nqed.1076 1077 ntheorem pos_compare_to_Prop:1075 #n #m #Hn #Hm 1076 @(lt_one_n_elim n Hn) 1077 @(lt_one_n_elim m Hm) 1078 #p #q <(pred_succ_n ?) <(pred_succ_n ?) 1079 <(pos_compare_S_S …) //; 1080 qed. 1081 1082 theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. 1083 #n elim n; //; qed. 1084 1085 theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. 1086 #n elim n; //; qed. 1087 1088 theorem pos_compare_to_Prop: 1078 1089 ∀n,m.match (pos_compare n m) with 1079 1090 [ LT ⇒ n < m 1080 1091  EQ ⇒ n = m 1081 1092  GT ⇒ m < n ]. 1082 #n ;#m;1083 napply(pos_elim2 (λn,m.match (pos_compare n m) with1093 #n #m 1094 @(pos_elim2 (λn,m.match (pos_compare n m) with 1084 1095 [ LT ⇒ n < m 1085 1096  EQ ⇒ n = m 1086 1097  GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *) 1087 ##[##1,2:napply pos_cases; 1088 ##[ ##1,3: /2/;1089 ## ##2,4: #m'; ncases m'; //;1090 ##]1091 ###n1;#m1;nnormalize;nrewrite < (pos_compare_S_S …); ncases (pos_compare n1 m1);1092 ##[##1,3:nnormalize;#IH;napply le_succ_succ;//;1093 ##nnormalize;#IH;nrewrite > IH;//]1094 nqed.1095 1096 ntheorem pos_compare_n_m_m_n:1098 [1,2:@pos_cases 1099 [ 1,3: /2/; 1100  2,4: #m' cases m'; //; 1101 ] 1102 #n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1); 1103 [1,3:normalize;#IH @le_succ_succ //; 1104 normalize;#IH >IH //] 1105 qed. 1106 1107 theorem pos_compare_n_m_m_n: 1097 1108 ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n). 1098 #n ;#m;1099 napply(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n)))1100 ##[##1,2:#n1;ncases n1;/2/;1101 ###n1;#m1; 1102 nrewrite < (pos_compare_S_S …); 1103 nrewrite < (pos_compare_S_S …); 1104 #IH ;nnormalize;napplyIH]1105 nqed.1109 #n #m 1110 @(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n))) 1111 [1,2:#n1 cases n1;/2/; 1112 #n1 #m1 1113 <(pos_compare_S_S …) 1114 <(pos_compare_S_S …) 1115 #IH normalize @IH] 1116 qed. 1106 1117 1107 ntheorem pos_compare_elim :1118 theorem pos_compare_elim : 1108 1119 ∀n,m:Pos. ∀P:compare → Prop. 1109 1120 (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m). 1110 #n ;#m;#P;#Hlt;#Heq;#Hgt;1111 ncut (match (pos_compare n m) with1121 #n #m #P #Hlt #Heq #Hgt 1122 cut (match (pos_compare n m) with 1112 1123 [ LT ⇒ n < m 1113 1124  EQ ⇒ n=m 1114 1125  GT ⇒ m < n] → 1115 1126 P (pos_compare n m)) 1116 ##[ncases (pos_compare n m);1117 ##[napplyHlt1118 ##napplyHeq1119 ##napplyHgt]1120 ###Hcut;napply Hcut;//;1121 nqed.1122 1123 ninductive cmp_cases (n,m:Pos) : CProp[0] ≝1127 [cases (pos_compare n m); 1128 [@Hlt 1129 @Heq 1130 @Hgt] 1131 #Hcut @Hcut //; 1132 qed. 1133 1134 inductive cmp_cases (n,m:Pos) : CProp[0] ≝ 1124 1135  cmp_le : n ≤ m → cmp_cases n m 1125 1136  cmp_gt : m < n → cmp_cases n m. 1126 1137 1127 ntheorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.1138 theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. 1128 1139 (* sic 1129 #n;#m;#H;nelim H 1130 ##[// 1131 ##/2/] *) 1132 /2/; nqed. 1133 1134 nlemma cmp_nat: ∀n,m:Pos.cmp_cases n m. 1135 #n;#m; nlapply (pos_compare_to_Prop n m); 1136 ncases (pos_compare n m);nnormalize; /3/; 1137 nqed. 1138 1139 1140 1141 1142 1143 nlet rec two_power_nat (n:nat) : Pos ≝ 1140 #n #m #H elim H 1141 [// 1142 /2/] *) 1143 /2/; qed. 1144 1145 lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. 1146 #n #m lapply (pos_compare_to_Prop n m) 1147 cases (pos_compare n m);normalize; /3/; 1148 qed. 1149 1150 1151 1152 1153 let rec two_power_nat (n:nat) : Pos ≝ 1144 1154 match n with 1145 1155 [ O ⇒ one … … 1147 1157 ]. 1148 1158 1149 ndefinition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).1159 definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
Note: See TracChangeset
for help on using the changeset viewer.