Changeset 535 for Deliverables/D3.1/Csemantics/Integers.ma
 Timestamp:
 Feb 16, 2011, 4:25:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Integers.ma
r487 r535 20 20 include "extralib.ma". 21 21 22 include "cerco/BitVector.ma". 23 include "cerco/BitVectorZ.ma". 24 include "cerco/Arithmetic.ma". 22 25 23 26 (* * * Comparisons *) … … 88 91 integer (type [Z]) plus a proof that it is in the range 0 (included) to 89 92 [modulus] (excluded. *) 90 (* XXX: hack to prevent normalization of huge proof term. *) 91 inductive inrange : Z → Prop ≝ 92  inrg_mod : ∀i:Z. inrange (i \mod modulus) 93  inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i. 94 inductive int: Type[0] ≝ 95  mk_int: ∀i:Z. inrange i → int. 96 (* 97 record int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }. 98 *) 99 definition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ]. 93 94 definition int : Type[0] ≝ BitVector wordsize. 95 96 definition intval: int → Z ≝ Z_of_unsigned_bitvector ?. 100 97 definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus. 101 #i cases i; 102 #x #H cases H; 103 [ #x' @modZ_lt_mod //; 104  //; 105 ] qed. 98 #i % whd in ⊢ (?%%) 99 [ @Z_unsigned_min 100  @Z_unsigned_max 101 ] qed. 106 102 107 103 (* The [unsigned] and [signed] functions return the Coq integer corresponding … … 118 114 (* Conversely, [repr] takes a Coq integer and returns the corresponding 119 115 machine integer. The argument is treated modulo [modulus]. *) 120 (*axiom repr : Z → int.*) 121 (* 122 definition repr : Z → int := λx. 123 mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos). 124 *) 125 definition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x). 116 117 definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z. 126 118 127 119 definition zero := repr 0. … … 130 122 definition iwordsize := repr (Z_of_nat wordsize). 131 123 132 axiom mk_int_eq: 133 ∀x,y,Px,Py. x = y → mk_int x Px = mk_int y Py. 134 (*Proof. 135 intros. subst y. 136 generalize (proof_irrelevance _ Px Py); intro. 137 subst Py. reflexivity. 138 Qed.*) 139 140 axiom eq_dec: ∀x,y: int. (x = y) + (x ≠ y). 141 (*Proof. 142 intros. destruct x; destruct y. case (zeq intval0 intval1); intro. 143 left. apply mkint_eq. auto. 144 right. red; intro. injection H. exact n. 145 Qed.*) 124 lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y). 125 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E 126 [ %1 lapply E @(eq_bv_elim … x y) [ //  #_ #X destruct ] 127  %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct  /2/ ] 128 ] qed. 146 129 147 130 (* * Arithmetic and logical operations over machine integers *) 148 131 149 definition eq : int → int → bool ≝ λx,y: int. 150 if eqZb (unsigned x) (unsigned y) then true else false. 132 definition eq : int → int → bool ≝ eq_bv wordsize. 151 133 definition lt : int → int → bool ≝ λx,y:int. 152 134 if Zltb (signed x) (signed y) then true else false. … … 207 189 ] 208 190  neg p ⇒ 209 match p with191 match p return λ_.bool × Z with 210 192 [ p1 q ⇒ 〈true, Zpred (neg q)〉 211 193  p0 q ⇒ 〈false, neg q〉 … … 528 510 theorem eq_sym: 529 511 ∀x,y. eq x y = eq y x. 530 #x #y whd in ⊢ (??%%); @eqZb_elim #H531 [ >H >(eqZb_z_z …) //532  >(eqZb_false … (sym_neq … H)) //512 #x #y @eq_bv_elim @eq_bv_elim /2/ 513 [ #NE #E @False_ind >E in NE * /2/ 514  #E #NE @False_ind >E in NE * /2/ 533 515 ] qed. 534 516 535 517 theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y). 536 #x #y whd in ⊢ (??%??); elim (eq_dec x y); #H 537 [ >H >(eqZb_z_z …) //; 538  >(eqZb_false …) //; 539 elim x in H ⊢ %; elim y; 540 #x' #Px #y' #Py #H normalize; @(not_to_not … H) @mk_int_eq 541 ] qed. 518 #x #y @eq_bv_elim #H @H qed. 542 519 543 520 theorem eq_true: ∀x. eq x x = true. … … 735 712 736 713 theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. 737 #i cases i; #i' #H cases H; /2/;714 #i @intrange 738 715 qed. 739 716
Note: See TracChangeset
for help on using the changeset viewer.