Changeset 2032 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2030 r2032 46 46 reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v. 47 47 #n #m elim n 48 [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize > split_O_n //48 [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n // 49 49  2: #n' #Hind #exp #v #v' #H >truncate_tail 50 50 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed. … … 328 328 qed. 329 329 330 lemma split_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.330 lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2. 331 331 # A #m #n elim m 332 332 [ 1: normalize #v … … 343 343 ] qed. 344 344 345 lemma split_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.345 lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2. 346 346 # A #m #n elim m 347 347 [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize // … … 355 355 ] qed. 356 356 357 lemma split_zero:357 lemma vsplit_zero: 358 358 ∀A,m. 359 359 ∀v: Vector A m. 360 〈[[]], v〉 = split A 0 m v.360 〈[[]], v〉 = vsplit A 0 m v. 361 361 #A #m #v 362 362 elim v … … 368 368 369 369 370 lemma split_zero2:370 lemma vsplit_zero2: 371 371 ∀A,m. 372 372 ∀v: Vector A m. 373 〈[[]], v〉 = split' A 0 m v.373 〈[[]], v〉 = vsplit' A 0 m v. 374 374 #A #m #v 375 375 elim v … … 382 382 (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma. 383 383 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *) 384 axiom split_succ:384 axiom vsplit_succ: 385 385 ∀A, m, n. 386 386 ∀l: Vector A m. … … 388 388 ∀v: Vector A (m + n). 389 389 ∀hd. 390 v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 =split ? (S m) n (hd:::v)).391 392 axiom split_succ2:390 v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)). 391 392 axiom vsplit_succ2: 393 393 ∀A, m, n. 394 394 ∀l: Vector A m. … … 396 396 ∀v: Vector A (m + n). 397 397 ∀hd. 398 v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 =split' ? (S m) n (hd:::v)).398 v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)). 399 399 400 lemma split_prod2:400 lemma vsplit_prod2: 401 401 ∀A,m,n. 402 402 ∀p: Vector A (m + n). 403 403 ∀v: Vector A m. 404 404 ∀q: Vector A n. 405 p = v@@q → 〈v, q〉 = split' A m n p.405 p = v@@q → 〈v, q〉 = vsplit' A m n p. 406 406 #A #m 407 407 elim m … … 409 409 >hyp <(vector_append_zero A n q v) 410 410 >(prod_vector_zero_eq_left A …) 411 @ split_zero2411 @vsplit_zero2 412 412  #r #ih #n #p #v #q #hyp 413 413 >hyp … … 416 416 cases exists 417 417 #tl #jmeq >jmeq 418 @ split_succ2 [1: % 2: @ih % ]418 @vsplit_succ2 [1: % 2: @ih % ] 419 419 ] 420 420 qed. 421 421 422 lemma split_prod:422 lemma vsplit_prod: 423 423 ∀A,m,n. 424 424 ∀p: Vector A (m + n). 425 425 ∀v: Vector A m. 426 426 ∀q: Vector A n. 427 p = v@@q → 〈v, q〉 = split A m n p.427 p = v@@q → 〈v, q〉 = vsplit A m n p. 428 428 #A #m 429 429 elim m … … 431 431 >hyp <(vector_append_zero A n q v) 432 432 >(prod_vector_zero_eq_left A …) 433 @ split_zero433 @vsplit_zero 434 434  #r #ih #n #p #v #q #hyp 435 435 >hyp … … 438 438 cases exists 439 439 #tl #jmeq >jmeq 440 @split_succ [1: % 2: @ih % ] 441 ] 442 qed. 443 444 445 (* Stolen from AssemblyProof.ma *) 446 lemma super_rewrite2: 447 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 448 ∀P: ∀m. Vector A m → Prop. 449 n=m → v1 ≃ v2 → P n v1 → P m v2. 450 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 451 qed. 452 453 lemma vector_cons_append: 454 ∀A: Type[0]. 455 ∀n: nat. 456 ∀e: A. 457 ∀v: Vector A n. 458 e ::: v = [[ e ]] @@ v. 459 # A # N # E # V 460 elim V 461 [ normalize % 462  # NN # AA # VV # IH 463 normalize 464 % 465 qed. 466 467 lemma vector_cons_append2: 468 ∀A: Type[0]. 469 ∀n, m: nat. 470 ∀v: Vector A n. 471 ∀q: Vector A m. 472 ∀hd: A. 473 hd:::(v@@q) = (hd:::v)@@q. 474 #A #n #m #v #q 475 elim v 476 [ #hd % 477  #n' #hd' #tl' #ih #hd' <ih % 478 ] 479 qed. 480 481 lemma jmeq_cons_vector_monotone: 482 ∀A: Type[0]. 483 ∀m, n: nat. 484 ∀v: Vector A m. 485 ∀q: Vector A n. 486 ∀prf: m = n. 487 ∀hd: A. 488 v ≃ q → hd:::v ≃ hd:::q. 489 #A #m #n #v #q #prf #hd #E 490 @(super_rewrite2 A … E) 491 [ assumption  % ] 492 qed. 493 494 lemma vector_associative_append: 495 ∀A: Type[0]. 496 ∀n, m, o: nat. 497 ∀v: Vector A n. 498 ∀q: Vector A m. 499 ∀r: Vector A o. 500 ((v @@ q) @@ r) 501 ≃ 502 (v @@ (q @@ r)). 503 #A #n #m #o #v #q #r 504 elim v 505 [ % 506  #n' #hd #tl #ih 507 <(vector_cons_append2 A … hd) 508 @jmeq_cons_vector_monotone 509 // 440 @vsplit_succ [1: % 2: @ih % ] 510 441 ] 511 442 qed. … … 514 445 #s1 #v normalize elim s1 normalize nodelta 515 446 normalize in v; 516 elim ( split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))447 elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) 517 448 [ 2,4: // 518 449  1,3: #l * #r normalize nodelta #Eq1 519 <( split_prod bool 16 16 … Eq1)520 elim ( split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))450 <(vsplit_prod bool 16 16 … Eq1) 451 elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) 521 452 [ 2,4: // 522 453  1,3: #lr * #rr normalize nodelta #Eq2 523 <( split_prod bool 8 8 … Eq2)454 <(vsplit_prod bool 8 8 … Eq2) 524 455 cut (v = (l @@ lr) @@ rr) 525 456 [ 1,3 : destruct >(vector_associative_append ? 16 8) // 526 457  2,4: #Hrewrite destruct 527 <( split_prod bool 24 8 … Hrewrite) @refl458 <(vsplit_prod bool 24 8 … Hrewrite) @refl 528 459 ] 529 460 ] … … 555 486  22: normalize elim b_sg elim a_sg normalize 556 487 normalize in val; 557 elim ( split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))488 elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) 558 489 [ 2,4,6,8: normalize // 559 490  1,3,5,7: #left * #right normalize #Eq1 560 <( split_prod bool 16 16 … Eq1)561 elim ( split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))491 <(vsplit_prod bool 16 16 … Eq1) 492 elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) 562 493 [ 2,4,6,8: // 563 494  1,3,5,7: #rightleft * #rightright normalize #Eq2 564 <( split_prod bool 8 8 … Eq2)495 <(vsplit_prod bool 8 8 … Eq2) 565 496 cut (val = (left @@ rightleft) @@ rightright) 566 497 [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) // 567 498  2,4,6,8: #Hrewrite destruct 568 <( split_prod bool 24 8 … Hrewrite) @refl499 <(vsplit_prod bool 24 8 … Hrewrite) @refl 569 500 ] 570 501 ] … … 616 547 >Heq in i; #i @i qed. 617 548 618 (* cast_int_int behaves as truncate (≃ split) when downsizing *)549 (* cast_int_int behaves as truncate (≃ vsplit) when downsizing *) 619 550 (* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *) 620 551 621 lemma split_to_truncate : ∀m,n,i. (\snd (split bool m n i)) = truncate m n i.552 lemma vsplit_to_truncate : ∀m,n,i. (\snd (vsplit bool m n i)) = truncate m n i. 622 553 #m #n #i normalize // qed. 623 554 … … 640 571 whd in match (addition_n ???); 641 572 whd in match (addition_n ???) in ⊢ (???%); 642 > split_to_truncate >split_to_truncate573 >vsplit_to_truncate >vsplit_to_truncate 643 574 <truncate_add_with_carries 644 575 [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false); … … 677 608 @(ex_intro … tl) 678 609 >Heq >Heq 679 elim ( split_eq2 … tl) #l * #r #Eq610 elim (vsplit_eq2 … tl) #l * #r #Eq 680 611 normalize 681 <( split_prod bool n m tl l r Eq)682 <( split_prod2 bool n m tl l r Eq)612 <(vsplit_prod bool n m tl l r Eq) 613 <(vsplit_prod2 bool n m tl l r Eq) 683 614 normalize // 684 615 qed. … … 690 621 whd in match (truncate ???); 691 622 whd in match (truncate ???) in ⊢ (???%); 692 < split_zero <split_zero //623 <vsplit_zero <vsplit_zero // 693 624  2: #m' #Hind #n #i normalize in i; 694 625 elim (Vector_Sn … i) #hd * #tl #Heq … … 713 644 * #Left #Right normalize nodelta 714 645 #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ?  _ ⇒ ?]))))); 715 #b >( split_to_truncate (S m')) >truncate_tail646 #b >(vsplit_to_truncate (S m')) >truncate_tail 716 647 cases b 717 648 normalize nodelta … … 736 667 whd in match (subtraction ???); 737 668 whd in match (subtraction ???) in ⊢ (???%); 738 > split_to_truncate >split_to_truncate669 >vsplit_to_truncate >vsplit_to_truncate 739 670 >integer_neg_trunc <truncate_add_with_carries 740 671 [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
Note: See TracChangeset
for help on using the changeset viewer.