Changeset 3259 for src/common/ByteValues.ma
 Timestamp:
 May 9, 2013, 12:49:38 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ByteValues.ma
r2927 r3259 277 277 [ BBbit b ⇒ OK … b 278 278  _ ⇒ Error … [MSG err]]. 279 280 definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝ 281 λA,eq,a1,a2. 282 match a1 with 283 [ Some x ⇒ match a2 with [Some y ⇒ eq x y  _ ⇒ false ] 284  None ⇒ match a2 with [None ⇒ true  _ ⇒ false] 285 ]. 286 287 lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq, 288 x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) → 289 (x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y). 290 #A #P #eq * [#x] * [1,3:*: #y] normalize #H #H1 #H2 291 [@H1 % 2,3: @H2 % #EQ destruct(EQ)] @H 292 [ #EQ @H1 >EQ % 293  * #H3 @H2 % #EQ destruct @H3 % 294 ] 295 qed. 296 297 298 definition eq_beval : beval → beval → bool ≝ 299 λbv1,bv2. 300 match bv1 with 301 [ BVundef ⇒ match bv2 with [ BVundef ⇒ true  _ ⇒ false ] 302  BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true  _ ⇒ false ] 303  BVXor pt1 pt1' p1 ⇒ 304 match bv2 with 305 [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧ 306 eq_option_map … eq_pointer pt1' pt2' ∧ 307 eqb (part_no … p1) (part_no … p2) 308  _ ⇒ false 309 ] 310  BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2  _ ⇒ false] 311  BVnull p1 ⇒ match bv2 with 312 [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2)  _ ⇒ false ] 313  BVptr ptr1 p1 ⇒ match bv2 with 314 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧ 315 eqb (part_no … p1) (part_no … p2) 316  _ ⇒ false 317 ] 318  BVpc pc1 p1 ⇒ match bv2 with 319 [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧ 320 eqb (part_no … p1) (part_no … p2) 321  _⇒ false 322 ] 323 ]. 324 325 lemma eq_beval_elim : ∀P:bool → Prop.∀x,y. 326 (x = y → P true) → (x ≠ y → P false) → P (eq_beval x y). 327 #P * 328 [ #pt1 #pt1' #p1  #b1  #p1  #ptr1 #p1  #pc1 #p1 ] 329 * 330 [1,8,15,22,29,36,43: 331 2,9,16,23,30,37,44: 332 3,10,17,24,31,38,45: #pt2 #pt2' #p2 333 4,11,18,25,32,39,46: #b2 334 5,12,19,26,33,40,47: #p2 335 6,13,20,26,34,41,48: #ptr2 #p2 336 *: #pc2 #p2 337 ] 338 normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct) 339 whd in match eq_beval; normalize nodelta 340 [ @eq_option_map_elim 341 [ @eq_pointer_elim 342 3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H % 343  normalize nodelta #EQ destruct(EQ) @eq_option_map_elim 344 [ @eq_pointer_elim 345 3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H % 346  #EQ destruct(EQ) cases p1 in H1 H2; p1 cases p2 p2 347 #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim 348 [ #EQ destruct(EQ) @H1 % 349  * #H @H2 % #EQ destruct(EQ) @H % 350 ] 351 ] 352 ] 353  @eq_bv_elim [#EQ destruct(EQ) @H1 %  * #H @H2 % #EQ destruct(EQ) @H %] 354  cases p1 in H1 H2; p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim 355 [ #EQ destruct(EQ) @H1 % 356  * #H @H2 % #EQ destruct @H % 357 ] 358  @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ) 359 cases p1 in H1 H2; p1 cases p2 p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim 360 [#EQ destruct @H1 % 361  * #H @H2 % #EQ destruct @H % 362 ] 363  @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct 364 cases p1 in H1 H2; p1 cases p2 p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim 365 [ #EQ destruct @H1 % 366  * #H @H2 % #EQ destruct @H % 367 ] 368 ] 369 qed.
Note: See TracChangeset
for help on using the changeset viewer.