Changeset 535 for Deliverables/D3.1/Csemantics
 Timestamp:
 Feb 16, 2011, 4:25:02 PM (9 years ago)
 Location:
 Deliverables/D3.1/Csemantics
 Files:

 6 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 
Deliverables/D3.1/Csemantics/Smallstep.ma
r487 r535 87 87 [ @(t'⧺t2) 88 88  // 89  <(Eapp_assoc …) //;89  <(Eapp_assoc …) <H2 @H5 90 90 ] 91 91 ] … … 104 104 star tr ge s1 t s3. 105 105 #tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3 106 @(star_trans … H1 … (star_one … H2)) //;106 @(star_trans … H1 … (star_one … H2)) @H3 107 107 qed. 108 108 … … 124 124 ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 > star tr ge s1 t s2. 125 125 #tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1 126 @(star_step … H1 H2 …) //;126 @(star_step … H1 H2 …) @e1; 127 127 qed. 128 128 … … 216 216 forever tr ge s1 (t ⧻ T). 217 217 #tr #ge #s1 #t1 #s2 #H elim H; 218 [ #s' #T #H2 //;218 [ #s' #T #H2 @H2 219 219  #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3 220 220 >e1 >(Eappinf_assoc …) … … 551 551 elim (IH ? B); #st3' *; #C #D 552 552 %{ st3'} % //; 553 @(star_trans ??? tA st2' ? tB ) //;554 elim A ; /2/; *; //;553 @(star_trans ??? tA st2' ? tB ?? C Ht) 554 elim A /2/ * // 555 555 ] qed. 556 556 
Deliverables/D3.1/Csemantics/cerco/BitVector.ma
r475 r535 123 123 false) b c. 124 124 125 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. 126 (x = y → P true) → 127 (x ≠ y → P false) → 128 P (eq_bv n x y). 129 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) 130 #Q * *; normalize /3/ 131 qed. 132 125 133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ 126 134 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in 
Deliverables/D3.1/Csemantics/cerco/Util.ma
r534 r535 13 13 ]. 14 14 15 (* 15 16 notation "hvbox('if' b 'then' t 'else' f)" 16 17 non associative with precedence 83 17 18 for @{ 'if_then_else $b $t $f }. 19 *) 20 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 }. 21 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 }. 18 22 19 23 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). 
Deliverables/D3.1/Csemantics/cerco/Vector.ma
r534 r535 12 12 include "arithmetics/nat.ma". 13 13 14 include "oldlib/eq.ma". 14 15 15 16 (* ===================================== *) … … 319 320 (* ===================================== *) 320 321 321 let rec reverse (A: Type[0]) (n: nat) 322 (v: Vector A n) on v ≝ 323 match v return (λm.λv. Vector A m) with 324 [ VEmpty ⇒ [[ ]] 325  VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) 326 ]. 327 // 328 qed. 322 (* At some points matita will attempt to reduce reverse with a known vector, 323 which reduces the equality proof for the cast. Normalising this proof needs 324 to be fast enough to keep matita usable. *) 325 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ 326 match n return λn'.∀m.S(n'+m) = n'+S m with 327 [ O ⇒ λm.refl ?? 328  S n' ⇒ λm. ? 329 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. 330 331 let rec revapp (A: Type[0]) (n: nat) (m:nat) 332 (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝ 333 match v return λn'.λ_. Vector A (n' + m) with 334 [ VEmpty ⇒ acc 335  VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ 336 ]. 337 > plus_n_Sm_fast @refl qed. 338 339 let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝ 340 (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. 341 < plus_n_O @refl qed. 329 342 330 343 (* ===================================== *) … … 436 449 qed. 437 450 451 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. 452 match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with 453 [ O ⇒ λP.λv.P [[ ]] → P v 454  S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 455 ] P v. 456 @(λA,n. λP:Vector A n → Prop. λv. match v return 457 ? 458 with [ VEmpty ⇒ ?  VCons m h t ⇒ ? ] P) 459 [ //  // ] qed. 460 (* XXX Proof below fails at qed. 461 #A #n #P * [ #H @H  #m #h #t #H @H ] qed. 462 *) 463 464 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 465 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 466 ∀n,x,y. 467 (x = y → P true) → 468 (x ≠ y → P false) → 469 P (eq_v A n f x y). 470 #P #A #f #f_elim #n #x elim x 471 [ #y @(vector_inv_n … y) 472 normalize /2/ 473  #m #h #t #IH #y @(vector_inv_n … y) 474 #h' #t' #Ht #Hf whd in ⊢ (?%) 475 @(f_elim ? h h') #Eh 476 [ @IH [ #Et @Ht >Eh >Et @refl  #NEt @Hf % #E' destruct (E') elim NEt /2/ ] 477  @Hf % #E' destruct (E') elim Eh /2/ 478 ] 479 ] qed. 480 438 481 (* ===================================== *) 439 482 (* Subvectors. *) 
Deliverables/D3.1/Csemantics/extralib.ma
r487 r535 331 331 ]. 332 332 interpretation "integer multiplication" 'times x y = (Z_times x y). 333 333 (* Now in cerco/Util.ma 334 334 (* Borrowed from standardlibrary/didactic/exercises/duality.ma with precedences tweaked *) 335 335 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 }. 336 336 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 }. 337 337 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). 338 338 *) 339 339 (* datatypes/list.ma *) 340 340
Note: See TracChangeset
for help on using the changeset viewer.