Changeset 10 for C-semantics
- Timestamp:
- Jul 6, 2010, 11:53:23 AM (11 years ago)
- Location:
- C-semantics
- Files:
-
- 3 added
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/AST.ma
r9 r10 21 21 include "Integers.ma". 22 22 include "Floats.ma". 23 include "binary/positive.ma". 23 24 24 25 (* * * Syntactic elements *) … … 26 27 (* * Identifiers (names of local variables, of global symbols and functions, 27 28 etc) are represented by the type [positive] of positive integers. *) 29 30 ndefinition ident ≝ Pos. 31 32 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 33 #x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y); 34 ##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed. 35 28 36 (* 29 Definition ident := positive.30 31 Definition ident_eq := peq.32 *)33 37 (* XXX: we use nats for now, but if in future we use binary like compcert 34 38 then the maps will be easier to define. *) … … 45 49 ##] 46 50 ##] nqed. 47 51 *) 48 52 (* * The intermediate languages are weakly typed, using only two types: 49 53 [Tint] for integers and pointers, and [Tfloat] for floating-point -
C-semantics/Cexec.ma
r9 r10 429 429 on d:decide to ? + (¬?). 430 430 431 ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P. 432 #P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed. 433 434 ncoercion decide_inject2 : 435 ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2 436 on d:decide to res ?. 437 431 438 alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)". 432 439 alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)". … … 438 445 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 439 446 440 (* Not very happy about this. *) 441 nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ 447 nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝ 442 448 match t1 with 443 449 [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ] 444 450 | Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] 445 451 | Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] 446 | Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr_ ⇒ dn ] | _ ⇒ dn ]452 | Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] 447 453 | Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒ 448 match type_eq_dec t t' with [ inl_ ⇒449 match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr_ ⇒ dn ] | _ ⇒ dn ]450 | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl_ ⇒451 match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr_ ⇒ dn ] | _ ⇒ dn ]454 match assert_type_eq t t' with [ OK _ ⇒ 455 match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] 456 | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ 457 match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] 452 458 | Tstruct i fl ⇒ 453 459 match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ 454 match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr_ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]460 match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ] 455 461 | Tunion i fl ⇒ 456 462 match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ 457 match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr_ ⇒ dn ] | _ ⇒ dn ]463 match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] 458 464 | Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] 459 465 ] 460 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠tl2) ≝466 and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝ 461 467 match tl1 with 462 468 [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ] 463 469 | Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒ 464 match type_eq_dec t1 t2 with [ inl_ ⇒465 match typelist_eq_dec ts1 ts2 with [ inl_ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]470 match assert_type_eq t1 t2 with [ OK _ ⇒ 471 match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ] 466 472 ] 467 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠fl2) ≝473 and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝ 468 474 match fl1 with 469 475 [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ] 470 476 | Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒ 471 477 match ident_eq i1 i2 with [ inl _ ⇒ 472 match type_eq_dec t1 t2 with [ inl_ ⇒473 match fieldlist_eq_dec fs1 fs2 with [ inl_ ⇒ dy | _ ⇒ dn ]478 match assert_type_eq t1 t2 with [ OK _ ⇒ 479 match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ] 474 480 | _ ⇒ dn ] | _ ⇒ dn ] ] 475 481 ]. 476 482 (* A poor man's clear, otherwise automation picks up recursive calls without 477 483 checking that the argument is smaller. *) 478 ngeneralize in type_eq_dec; 479 ngeneralize in typelist_eq_dec; 480 ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6; 481 ndestruct; //; @; #H; ndestruct; 482 ##[ nelim c8; /2/ 483 ##| nelim c6; /2/ 484 ##| nelim c4; /2/ 485 ##| nelim c4; /2/ 486 ##| nelim c8; /2/ 487 ##| nelim c6; /2/ 488 ##| nelim c8; /2/ 489 ##| nelim c6; /2/ 490 ##| nelim c8; /2/ 491 ##| nelim c6; /2/ 492 ##| nelim c8; /2/ 493 ##| nelim c6; /2/ 494 ##| nelim c4; /2/ 495 ##| nelim c8; /2/ 496 ##| nelim c6; /2/ 497 ##| nelim c12; /2/ 498 ##| nelim c10; /2/ 499 ##| nelim c8; /2/ 500 ##] nqed. 501 502 ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝ 503 λA,dec,x,y. 504 match dec … x y with 505 [ inl p ⇒ OK ? p 506 | inr _ ⇒ Error ? 507 ]. 484 ngeneralize in assert_type_eq; 485 ngeneralize in assert_typelist_eq; 486 ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //; 487 (* XXX: I have no idea why the first // didn't catch these. *) 488 //; //; //; //; //; //; //; //; //; 489 nqed. 508 490 509 491 nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝ … … 527 509 vargs ← exec_exprlist ge e m al;: 528 510 fd ← opt_to_res ? (find_funct Genv ? ge vf);: 529 p ← a re_equal ? type_eq_dec(type_of_fundef fd) (typeof a);:511 p ← assert_type_eq (type_of_fundef fd) (typeof a);: 530 512 k' ← match lhs with 531 513 [ None ⇒ OK ? (Kcall (None ?) f e k) -
C-semantics/Coqlib.ma
r3 r10 18 18 library. *) 19 19 20 include " arithmetics/Z.ma".20 include "binary/Z.ma". 21 21 include "datatypes/sums.ma". 22 22 include "datatypes/list.ma". … … 347 347 auto. 348 348 Qed. 349 350 (** Properties of powers of two. *) 351 352 Lemma two_power_nat_O : two_power_nat O = 1. 353 Proof. reflexivity. Qed. 354 355 Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0. 356 Proof. 357 induction n. rewrite two_power_nat_O. omega. 358 rewrite two_power_nat_S. omega. 359 Qed. 360 361 Lemma two_power_nat_two_p: 362 forall x, two_power_nat x = two_p (Z_of_nat x). 363 Proof. 364 induction x. auto. 365 rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega. 366 Qed. 367 349 *) 350 (* * Properties of powers of two. *) 351 352 nlemma two_power_nat_O : two_power_nat O = one. 353 //; nqed. 354 355 nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0. 356 //; nqed. 357 358 nlemma two_power_nat_two_p: 359 ∀x. Z_two_power_nat x = two_p (Z_of_nat x). 360 #x; ncases x; 361 ##[ //; 362 ##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //; 363 ##] nqed. 364 (* 368 365 Lemma two_p_monotone: 369 366 forall x y, 0 <= x <= y -> two_p x <= two_p y. … … 577 574 (* * Alignment: [align n amount] returns the smallest multiple of [amount] 578 575 greater than or equal to [n]. *) 579 naxiom align : Z → Z → Z. 580 (* 576 (*naxiom align : Z → Z → Z.*) 577 581 578 ndefinition align ≝ λn: Z. λamount: Z. 582 579 ((n + amount - 1) / amount) * amount. 583 580 (* 584 581 Lemma align_le: forall x y, y > 0 -> x <= align x y. 585 582 Proof. -
C-semantics/Integers.ma
r9 r10 17 17 18 18 include "arithmetics/nat.ma". 19 include " arithmetics/Z.ma".19 include "binary/Z.ma". 20 20 include "extralib.ma". 21 21 … … 62 62 *) 63 63 64 naxiom two_power_nat : nat → Z. 64 (*naxiom two_power_nat : nat → Z.*) 65 65 66 66 ndefinition wordsize : nat ≝ 32. 67 ndefinition modulus : Z ≝ two_power_nat wordsize.67 ndefinition modulus : Z ≝ Z_two_power_nat wordsize. 68 68 ndefinition half_modulus : Z ≝ modulus / 2. 69 69 ndefinition max_unsigned : Z ≝ modulus - 1. … … 75 75 nnormalize; //; nqed. 76 76 77 (* 78 Remark modulus_power: 77 nremark modulus_power: 79 78 modulus = two_p (Z_of_nat wordsize). 80 Proof. 81 unfold modulus. apply two_power_nat_two_p. 82 Qed. 83 84 Remark modulus_pos: 79 //; nqed. 80 81 nremark modulus_pos: 85 82 modulus > 0. 86 Proof. 87 rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega. 88 Qed. 89 *) 83 //; nqed. 84 90 85 (* * Representation of machine integers *) 91 86 -
C-semantics/Maps.ma
r3 r10 172 172 *) 173 173 174 naxiom PTree : TREE ident. 174 (* XXX: need real tree impl *) 175 nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝ 176 match l with 177 [ nil ⇒ None ? 178 | cons h t ⇒ 179 match h with [ mk_pair hi ha ⇒ 180 match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ] 181 ]. 182 183 naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) → 184 ∀a,b: list (ident × A). (a = b) + (a ≠ b). 185 naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A). 186 naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B). 187 naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A). 188 naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B. 189 190 ndefinition PTree : TREE ident ≝ 191 mk_TREE ? 192 ident_eq 193 (λA. list (ident × A)) 194 assoc_tree_eq 195 (λA. nil ?) 196 assoc_get 197 (λA,i,a,l.〈i,a〉::l) 198 assoc_remove 199 assoc_tree_map 200 assoc_elements 201 assoc_tree_fold. 175 202 176 203 (* -
C-semantics/Mem.ma
r9 r10 25 25 *) 26 26 27 include "arithmetics/Z.ma". 27 include "arithmetics/nat.ma". 28 include "binary/Z.ma". 28 29 include "datatypes/sums.ma". 29 30 include "datatypes/list.ma". … … 127 128 | Mfloat64 => 7]. 128 129 130 alias symbol "plus" (instance 2) = "integer plus". 129 131 nlemma size_chunk_pred: 130 132 ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk. … … 164 166 nlemma align_size_chunk_divides: 165 167 ∀chunk. (align_chunk chunk ∣ size_chunk chunk). 166 #chunk;ncases chunk;nnormalize; @;//;##[ napply 2; ##| // ##]168 #chunk;ncases chunk;nnormalize;/3/; 167 169 nqed. 168 170 … … 176 178 (* The initial store. *) 177 179 178 ndefinition oneZ ≝ pos O.180 ndefinition oneZ ≝ pos one. 179 181 180 182 nremark one_pos: OZ < oneZ. … … 186 188 187 189 ndefinition empty: mem ≝ 188 mk_mem (λx.empty_block OZ OZ) (pos O) one_pos.190 mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. 189 191 190 192 ndefinition nullptr: block ≝ OZ. … … 501 503 nchange in ⊢ (??(???%)?) with (update ????); 502 504 nwhd in ⊢(??%?);nrewrite > (update_s content …); 503 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … );//;napply sym_neq;//;505 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//; 504 506 nqed. 505 507 … … 512 514 nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp; 513 515 ##[nrewrite > Hp; 514 n lapply (eqb_to_Prop n1 n2);ncases (eqbn1 n2); #Hn;516 napply (eqb_elim n1 n2); #Hn; 515 517 ##[nrewrite > Hn;@; @; //; 516 518 ##|@2;/2/] … … 1055 1057 ##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …); 1056 1058 #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4; 1057 napply (eq_f ?? (λx. Z_of_nat (1 + x)) ???);//##]1059 napply (eq_f ?? (λx.1 + x) ???);//##] 1058 1060 nqed. 1059 1061 … … 1582 1584 ##| napply (Zleb_true_to_Zle … H2) 1583 1585 ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon 1584 ##| n apply (witness ?? (abs ofs)); nnormalize; nrewrite > (Zplus_z_OZ ?); //1586 ##| ncases ofs; /2/; 1585 1587 ##] 1586 1588 ##| *; #Hval;#Hlo;#Hhi;#Hal; … … 1699 1701 ##| #ineq; @1; @1; napply ineq; 1700 1702 ##] nqed. 1701 1703 (* XXX: reenable once I've sorted out performance a bit 1702 1704 ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem. 1703 1705 ∀b1,b1',delta1,b2,b2',delta2. … … 2365 2367 ##] 2366 2368 ##] nqed. 2367 (* XXX: reenable once I've sorted out Integers.ma a bit 2369 2368 2370 nlemma valid_pointer_inject_no_overflow: 2369 2371 ∀f,m1,m2,b,ofs,b',x. -
C-semantics/extralib.ma
r3 r10 13 13 (**************************************************************************) 14 14 15 include "arithmetics/Z.ma".16 15 include "datatypes/sums.ma". 17 16 include "datatypes/list.ma". 18 17 include "Plogic/equality.ma". 18 include "binary/Z.ma". 19 include "binary/positive.ma". 19 20 20 21 nlemma eq_rect_Type0_r: … … 61 62 62 63 (* XXX: divides goes to arithmetics *) 63 ninductive divides (n,m:nat) : Prop ≝ 64 | witness : ∀p:nat.m = times n p → divides n m. 65 interpretation "divides" 'divides n m = (divides n m). 66 interpretation "not divides" 'ndivides n m = (Not (divides n m)). 67 68 ndefinition dividesZ ≝ λx,y:Z. abs x ∣ abs y. 64 ninductive dividesP (n,m:Pos) : Prop ≝ 65 | witness : ∀p:Pos.m = times n p → dividesP n m. 66 interpretation "positive divides" 'divides n m = (dividesP n m). 67 interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). 68 69 ndefinition dividesZ : Z → Z → Prop ≝ 70 λx,y. match x with 71 [ OZ ⇒ False 72 | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] 73 | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] 74 ]. 75 69 76 interpretation "integer divides" 'divides n m = (dividesZ n m). 70 77 interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)). 71 78 72 79 (* should be proved in nat.ma, but it's not! *) 73 naxiom eqb_to_Prop : ∀n,m.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. 80 naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. 81 82 nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. 83 #n m; napply eqb_elim; //; nqed. 74 84 75 85 nlemma injective_Z_of_nat : injective ? ? Z_of_nat. … … 77 87 #n;#m;ncases n;ncases m;nnormalize;//; 78 88 ##[ ##1,2: #n';#H;ndestruct 79 ##| #n';#m'; #H; ndestruct; //89 ##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); // 80 90 ##] nqed. 81 91 … … 92 102 nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. 93 103 #x;#y; 94 #n; 95 nelim n;##[ ##2: #n'; #IH; ##]104 napply pos_elim 105 ##[ ##2: #n'; #IH; ##] 96 106 nrewrite > (Zplus_Zsucc_Zpred y ?); 97 nwhd in ⊢ (?→??(??%));98 ##[#H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);107 ##[ nrewrite > (Zpred_Zsucc (pos n')); 108 #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??); 99 109 napply Zsucc_le; 100 110 ##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le; … … 115 125 /3/; #H; nrewrite > H; //; nqed. 116 126 127 ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. 128 #x y; ncases x; 129 ##[ ncases y; 130 ##[ ##1,2: // 131 ##| #n; napply False_ind; 132 ##] 133 ##| #n; ncases y; 134 ##[ nnormalize; napply False_ind; 135 ##| #m; napply (pos_cases … n); /2/; 136 ##| #m; nnormalize; napply False_ind; 137 ##] 138 ##| #n; ncases y; /2/; 139 ##] nqed. 140 117 141 ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. 118 #n;#m;#p; nlapply (Z_compare_to_Prop n p); nelim (Z_compare n p); 119 ##[ //; 120 ##| #H; nrewrite > H; #A;#B; napply False_ind; nlapply (Zlt_to_Zle … A); 121 #C; nlapply (transitive_Zle … C B); nelim p; /2/; #n';nelim n'; /2/; 122 ##| #A; #B; #C; nlapply (transitive_Zlt … A B); #D; 123 napply False_ind; nlapply (Zlt_to_Zle … D); 124 #E; nlapply (transitive_Zle … E C); nelim p; /2/; #n';nelim n'; /2/; 125 ##] nqed. 126 127 nlemma decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). 142 #n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt; 143 napply (transitive_Zle … Hle); /2/; 144 nqed. 145 146 ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). 128 147 #z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H; 129 148 ##[@;// … … 180 199 match y with 181 200 [ OZ ⇒ false 182 | pos m ⇒ leb ( Sn) m201 | pos m ⇒ leb (succ n) m 183 202 | neg m ⇒ false ] 184 203 | neg n ⇒ … … 186 205 [ OZ ⇒ true 187 206 | pos m ⇒ true 188 | neg m ⇒ leb ( Sm) n ]].207 | neg m ⇒ leb (succ m) n ]]. 189 208 190 209 … … 205 224 206 225 ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. 207 #n ;#m;ncases n;ncases m; nnormalize; /2/;226 #n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct; 208 227 nqed. 209 228 … … 225 244 226 245 ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. 227 #n;#m;ncases n;ncases m; nnormalize; /2/; 228 ##[ #n';#m';ncases n';nnormalize; 229 ##[ ##2: #n';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##] 230 //; 231 ##| #n';#m';ncases m';nnormalize; 232 ##[ ##2: #m';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##] 233 //; 234 ##] nqed. 246 #n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct; 247 nqed. 235 248 236 249 ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. … … 258 271 259 272 (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *) 260 notation > "'if' term 19 e 'then' term 19 t 'else' term 68 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.261 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 68 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.273 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 274 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 262 275 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). 263 276 … … 280 293 (* division *) 281 294 282 nlet rec divide_aux (b,m,n,p:nat) on b ≝ 283 if leb (S m) n then 〈p,m〉 else 284 match b with 285 [ O ⇒ 〈p,m〉 286 | S b' ⇒ divide_aux b' (m-n) n (S p) 287 ]. 288 289 ndefinition divide ≝ λm,n. divide_aux m m n O. 295 ninductive natp : Type ≝ 296 | pzero : natp 297 | ppos : Pos → natp. 298 299 ndefinition natp0 ≝ 300 λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ]. 301 302 ndefinition natp1 ≝ 303 λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ]. 304 305 nlet rec divide (m,n:Pos) on m ≝ 306 match m with 307 [ one ⇒ 308 match n with 309 [ one ⇒ 〈ppos one,pzero〉 310 | _ ⇒ 〈pzero,ppos one〉 311 ] 312 | p0 m' ⇒ 313 match divide m' n with 314 [ mk_pair q r ⇒ 315 match r with 316 [ pzero ⇒ 〈natp0 q,pzero〉 317 | ppos r' ⇒ 318 match partial_minus (p0 r') n with 319 [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉 320 | MinusZero ⇒ 〈natp1 q, pzero〉 321 | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 322 ] 323 ] 324 ] 325 | p1 m' ⇒ 326 match divide m' n with 327 [ mk_pair q r ⇒ 328 match r with 329 [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ] 330 | ppos r' ⇒ 331 match partial_minus (p1 r') n with 332 [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉 333 | MinusZero ⇒ 〈natp1 q, pzero〉 334 | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 335 ] 336 ] 337 ] 338 ]. 339 290 340 ndefinition div ≝ λm,n. fst ?? (divide m n). 291 341 ndefinition mod ≝ λm,n. snd ?? (divide m n). … … 306 356 nqed. 307 357 308 nlemma minus_plus_distrib: ∀n,m,p. m-(n+p) = m-n-p. 309 #n;nelim n; //; #n';#IH;#m;#p;nnormalize; 310 nelim m; //; nqed. 358 nlemma pred_minus: ∀n,m. pred n - m = pred (n-m). 359 napply pos_elim; /3/; 360 nqed. 361 362 nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p. 363 napply pos_elim; 364 ##[ // 365 ##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/; 366 ##] nqed. 311 367 312 368 ntheorem plus_minus_r: 313 ∀m,n,p: nat. m ≤n → p+(n-m) = (p+n)-m.369 ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m. 314 370 #m;#n;#p;#le;nrewrite > (symmetric_plus …); 315 371 nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed. 316 372 317 nlemma plus_minus_le: ∀m,n,p . m≤n → m+p-n≤p.373 nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p. 318 374 #m;#n;#p;nelim m;/2/; nqed. 319 375 (* 320 376 nlemma le_to_minus: ∀m,n. m≤n → m-n = 0. 321 377 #m;#n;nelim n; … … 324 380 nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/ 325 381 ##] nqed. 326 327 nlemma minus_times_distrib_l: ∀n,m,p:nat. p*m-p*n = p*(m-n). 328 #n;#m;#p;nelim (decidable_le n m);#le; 329 ##[ nelim p; //;#p'; #IH; nnormalize; nrewrite > (minus_plus_distrib …); 330 nrewrite < (plus_minus … le); nrewrite < IH; 382 *) 383 nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n). 384 #n;#m;#p;(*nelim (decidable_lt n m);*)#lt; 385 (*##[*) napply (pos_elim … p); //;#p'; #IH; 386 nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); 387 nrewrite > (minus_plus_distrib …); 388 nrewrite < (plus_minus … lt); nrewrite < IH; 331 389 nrewrite > (plus_minus_r …); /2/; 332 ##| 333 nlapply (not_le_to_lt … le); #lt; 334 nelim p; //; #p'; 335 ncut (m-n = 0); ##[ /3/ ##] 336 #mn; nrewrite > mn; nrewrite < (times_n_O …); #H; 337 nnormalize; napply sym_eq; napply le_n_O_to_eq; nrewrite < H; 390 nqed. 391 (*##| 392 nlapply (not_lt_to_le … lt); #le; 393 napply (pos_elim … p); //; #p'; 394 ncut (m-n = one); ##[ /3/ ##] 395 #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …); 396 #H; nrewrite < H in ⊢ (???%); 397 napply sym_eq; napply le_n_one_to_eq; nrewrite < H; 338 398 nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l; 339 399 /2/; … … 346 406 napply False_ind; napply (absurd ? H ( not_le_Sn_n n)); 347 407 nqed. 348 349 nlemma divide_aux_ok : ∀b,m,n,p,dv,md:nat. 350 n > 0 → b ≥ m → 351 divide_aux b m n p = 〈dv,md〉 → 352 m + p*n = dv*n + md ∧ md < n. 353 #b;nelim b; 354 ##[ #m;#n;#p;#dv;#md;#npos;#bound; 355 nwhd in ⊢ (??%% → ?); nelim (leb (S m) n); nwhd in ⊢ (??%% → ?); #H; 356 ndestruct; 357 @; /2/ 358 ##| #b';#IH;#m;#n;#p;#dv;#md; 359 #npos; #bound; nwhd in ⊢ (??%? → ?); napply leb_elim; 360 ##[ #Hlt; nwhd in ⊢ (??%? → ?); #H; 361 ndestruct; 362 /2/; 363 ##| #Hnlt; ncut (n≤m); ##[ nlapply (not_le_to_lt … Hnlt); /2/; ##] 364 #Hnm; nwhd in ⊢ (??%? → ?); #H; 365 nlapply (IH … H); ##[ napply le_S_S_to_le; napply (transitive_le ? m); //; 366 nrewrite < (minus_Sn_m …); //; napply (lt_O_n_elim …npos); #n'; 367 nrewrite > (minus_S_S …); /2/; 368 ##| // 369 ##| nnormalize; nrewrite < (associative_plus …); nrewrite < (plus_minus_m_m …); //; 370 ##] 371 ##] nqed. 372 373 ntheorem divide_divides: ∀m,n,dv,md:nat. 374 n > 0 → divide m n = 〈dv,md〉 → m = dv * n + md ∧ md < n. 375 #m;#n;#dv;#md;#npos; nwhd in ⊢ (??%? → ?); #DIVIDE; 376 nlapply (divide_aux_ok … DIVIDE); //; nqed. 377 378 nlemma mod0_divides: ∀m,n,dv:nat. 379 m>0 → divide n m = 〈dv,O〉 → m∣n. 380 #m;#n;#dv;#mpos;#DIVIDE;@ dv; nlapply (divide_divides … DIVIDE); //; *; //; 381 nqed. 382 383 nlemma divides_mod0: ∀dv,m,n:nat. 384 m>0 → n = dv*m → divide n m = 〈dv,O〉. 385 #dv;#m;#n;#mpos;#DIV;nlapply (refl ? (divide n m)); 386 nelim (divide n m) in ⊢ (???% → ?); #dv';#md'; #DIVIDE; 387 nlapply (divide_divides … mpos DIVIDE); *; 388 nrewrite > DIV in ⊢ (% → ?); #H; nlapply (plus_to_minus … H); 389 nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv' …); 390 nrewrite > (minus_times_distrib_l …); 391 nelim (decidable_le dv dv'); 392 ##[ #le; ncut (dv-dv' = 0); ##[ /2/ ##] 393 #eq; nrewrite > eq; nrewrite < (times_n_O …); #md0; #_; 394 nrewrite > DIVIDE; nrewrite < md0 in H ⊢ %; nrewrite < (plus_n_O …); 395 #H; ncut (dv = dv'); ##[ napply le_to_le_to_eq; //; 396 napply (le_times_to_le m); //; ##] 397 //; 398 ##| #nle; ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##] 399 #Hdv; #H; ncut (md' ≥ m); /2/; #A;#B; napply False_ind; 400 napply (absurd ? A (lt_to_not_le … B)); 401 ##] nqed. 402 403 nlemma dec_divides_1: ∀m,n:nat. m>0 → (m∣n) + ¬(m∣n). 404 #m;#n;#mpos; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %); 405 #dv;#md; ncases md; 406 ##[ #H; @1; napply mod0_divides; //; 408 *) 409 410 nlet rec natp_plus (n,m:natp) ≝ 411 match n with 412 [ pzero ⇒ m 413 | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ] 414 ]. 415 416 nlet rec natp_times (n,m:natp) ≝ 417 match n with 418 [ pzero ⇒ pzero 419 | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ] 420 ]. 421 422 ninductive natp_lt : natp → Pos → Prop ≝ 423 | plt_zero : ∀n. natp_lt pzero n 424 | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m. 425 426 nlemma lt_p0: ∀n:Pos. one < p0 n. 427 #n; nnormalize; /2/; nqed. 428 429 nlemma lt_p1: ∀n:Pos. one < p1 n. 430 #n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed. 431 432 nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉. 433 #m; nelim m; 434 ##[ //; 435 ##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //; 436 ##] nqed. 437 438 nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n). 439 #n P Q; napply succ_elim; /2/; nqed. 440 441 nlemma partial_minus_to_Prop: ∀n,m. 442 match partial_minus n m with 443 [ MinusNeg ⇒ n < m 444 | MinusZero ⇒ n = m 445 | MinusPos r ⇒ n = m+r 446 ]. 447 #n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m); 448 nnormalize; ncases (partial_minus n m); /2/; nqed. 449 450 nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m. 451 #n m lt; nelim lt; /2/; 452 nqed. 453 454 nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m. 455 #n m lt; napply (transitive_lt ? (p0 m) ?); /2/; 456 nqed. 457 458 nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m. 459 #n m lt; ninversion lt; 460 ##[ #H; nrewrite > (succ_injective … H); //; 461 ##| #p H1 H2 H3;nrewrite > (succ_injective … H3); 462 napply (transitive_lt ? (p0 p) ?); /2/; 463 ##] 464 nqed. 465 466 nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m. 467 #n m lt; nelim lt; /2/; 468 nqed. 469 470 471 472 nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m. 473 #n m lt;ninversion lt; 474 ##[ #p H; ndestruct; 475 ##| #n' m' lt e1 e2; ndestruct; //; 476 ##] nqed. 477 478 nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b. 479 #a b; /2/; nqed. 480 481 nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b. 482 #a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed. 483 484 nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. 485 /2/; nqed. 486 487 nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. 488 #A B a1 a2 b1 b2 H; ndestruct; //; 489 nqed. 490 491 nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. 492 #A B a1 a2 b1 b2 H; ndestruct; //; 493 nqed. 494 495 ntheorem divide_ok : ∀m,n,dv,md. 496 divide m n = 〈dv,md〉 → 497 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. 498 #m n; napply (pos_cases … n); 499 ##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/; 500 ##| #n'; nelim m; 501 ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; 502 ##| #m' IH dv md; nnormalize; 503 nlapply (refl ? (divide m' (succ n'))); 504 nelim (divide m' (succ n')) in ⊢ (???% → % → ?); 505 #dv' md' DIVr; nelim (IH … DIVr); 506 nnormalize; ncases md'; 507 ##[ ncases dv'; nnormalize; 508 ##[ #H; ndestruct; 509 ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; 510 ##] 511 ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; 512 nnormalize; #n md'' Hr1 Hr2; 513 nlapply (plt_lt … Hr2); #Hr2'; 514 nlapply (partial_minus_to_Prop md'' n); 515 ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize; 516 #lt; #e; ndestruct; @; /2/; napply plt_pos; 517 ##[ ##1,3,5,7: napply double_lt1; /2/; 518 ##| ##2,4: napply double_lt3; /2/; 519 ##| ##*: napply double_lt2; /2/; 520 ##] 521 ##] 522 ##| #m' IH dv md; nwhd in ⊢ (??%? → ?); 523 nlapply (refl ? (divide m' (succ n'))); 524 nelim (divide m' (succ n')) in ⊢ (???% → % → ?); 525 #dv' md' DIVr; nelim (IH … DIVr); 526 nwhd in ⊢ (? → ? → ??%? → ?); ncases md'; 527 ##[ ncases dv'; nnormalize; 528 ##[ #H; ndestruct; 529 ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/; 530 ##] 531 ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; 532 nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2; 533 nlapply (plt_lt … Hr2); #Hr2'; 534 nwhd in ⊢ (??%? → ?); 535 nlapply (partial_minus_to_Prop (p0 md'') (succ n')); 536 ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##] 537 ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize; 538 #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##] 539 #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##] 540 nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e); 541 nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos; 542 ##[ ncut (succ n' + r'' < p0 (succ n')); /2/; 543 ##| ncut (succ n' + r'' < p0 (succ n')); /2/; 544 ##| /2/; 545 ##| /2/; 546 ##] 547 ##] 548 ##] 549 ##] nqed. 550 551 nlemma mod0_divides: ∀m,n,dv:Pos. 552 divide n m = 〈ppos dv,pzero〉 → m∣n. 553 #m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *; 554 nnormalize; #H; ndestruct; //; 555 nqed. 556 557 nlemma divides_mod0: ∀dv,m,n:Pos. 558 n = dv*m → divide n m = 〈ppos dv,pzero〉. 559 #dv;#m;#n;#DIV;nlapply (refl ? (divide n m)); 560 nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE; 561 nlapply (divide_ok … DIVIDE); *; 562 ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##] 563 ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE; nnormalize; 564 nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct; 565 ##[ nlapply (plus_to_minus … e0); 566 nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …); 567 ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt; 568 nrewrite > (minus_times_distrib_l …); //; 569 570 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##] 571 #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind; 572 napply (absurd ? B (lt_to_not_le … A)); 573 574 ##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/; 575 576 ##| nrewrite > DIVIDE; ncut (dv = dv''); /2/; 577 ##] 578 nqed. 579 580 nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n). 581 #m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %); 582 #dv;#md; ncases md; ncases dv; 583 ##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct 584 ##| #dv'; #H; @1; napply mod0_divides; /2/; 407 585 ##| #md'; #DIVIDES; @2; napply nmk; *; #dv'; 408 nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); //;586 nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); 409 587 nrewrite > DIVIDES; #H'; 410 588 ndestruct; 411 ##] nqed. 412 413 nlemma dec_divides: ∀m,n:nat. (m∣n) + ¬(m∣n). 414 #m;#n; ncases m; /2/; 415 ncases n; 416 ##[ @1; @ O; //; 417 ##| #n'; @ 2; @; *; /2/ 589 ##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv'; 590 nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); 591 nrewrite > DIVIDES; #H'; 592 ndestruct; 418 593 ##] nqed. 419 594 420 595 ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q). 421 #p;#q;napply dec_divides; nqed. 422 596 #p;#q;ncases p; 597 ##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##] 598 ##| ##*: #n; ncases q; nnormalize; /2/; 599 ##] nqed. 600 601 ndefinition natp_to_Z ≝ 602 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ]. 603 604 ndefinition natp_to_negZ ≝ 605 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ]. 423 606 424 607 (* TODO: check these definitions are right. They are supposed to be the same 425 608 as Zdiv/Zmod in Coq. *) 426 609 ndefinition divZ ≝ λx,y. 427 match divide (abs x) (abs y) with 428 [ mk_pair q r ⇒ 429 match x with 610 match x with 611 [ OZ ⇒ OZ 612 | pos n ⇒ 613 match y with 430 614 [ OZ ⇒ OZ 431 | pos m ⇒ 432 match y with 433 [ OZ ⇒ OZ 434 | pos n ⇒ q 435 | neg n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ] 436 ] 437 | neg m ⇒ 438 match y return λ_.Z with 439 [ OZ ⇒ OZ 440 | pos n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ] 441 | neg n ⇒ q 442 ] 615 | pos m ⇒ natp_to_Z (fst ?? (divide n m)) 616 | neg m ⇒ match divide n m with [ mk_pair q r ⇒ 617 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] 618 ] 619 | neg n ⇒ 620 match y with 621 [ OZ ⇒ OZ 622 | pos m ⇒ match divide n m with [ mk_pair q r ⇒ 623 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] 624 | neg m ⇒ natp_to_Z (fst ?? (divide n m)) 443 625 ] 444 626 ]. 445 627 446 628 ndefinition modZ ≝ λx,y. 447 match divide (abs x) (abs y) with 448 [ mk_pair q r ⇒ 449 match x with 629 match x with 630 [ OZ ⇒ OZ 631 | pos n ⇒ 632 match y with 450 633 [ OZ ⇒ OZ 451 | pos m ⇒ 452 match y return λ_.Z with 453 [ OZ ⇒ OZ 454 | pos n ⇒ r 455 | neg n ⇒ match r with [ O ⇒ O | _ ⇒ y-r ] 456 ] 457 | neg m ⇒ 458 match y return λ_.Z with 459 [ OZ ⇒ OZ 460 | pos n ⇒ match r with [ O ⇒ O | _ ⇒ y+r ] 461 | neg n ⇒ r 462 ] 634 | pos m ⇒ natp_to_Z (snd ?? (divide n m)) 635 | neg m ⇒ match divide n m with [ mk_pair q r ⇒ 636 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ] 637 ] 638 | neg n ⇒ 639 match y with 640 [ OZ ⇒ OZ 641 | pos m ⇒ match divide n m with [ mk_pair q r ⇒ 642 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ] 643 | neg m ⇒ natp_to_Z (snd ?? (divide n m)) 463 644 ] 464 645 ].
Note: See TracChangeset
for help on using the changeset viewer.