Changeset 2108 for src/ASM/Arithmetic.ma
 Timestamp:
 Jun 25, 2012, 2:39:06 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2032 r2108 534 534 \snd (half_add n l r). 535 535 536 axiom add_zero: 536 lemma half_add_carry_Sn: 537 ∀n: nat. 538 ∀l: BitVector n. 539 ∀hd: bool. 540 \fst (half_add (S n) (hd:::l) (false:::(zero n))) = 541 andb hd (\fst (half_add n l (zero n))). 542 #n #l elim l 543 [1: 544 #hd normalize cases hd % 545 2: 546 #n' #hd #tl #inductive_hypothesis #hd' 547 whd in match half_add; normalize nodelta 548 whd in match full_add; normalize nodelta 549 normalize in ⊢ (??%%); cases hd' normalize 550 @pair_elim #c1 #r #c1_r_refl cases c1 % 551 ] 552 qed. 553 554 lemma half_add_zero_carry_false: 555 ∀m: nat. 556 ∀b: BitVector m. 557 \fst (half_add m b (zero m)) = false. 558 #m #b elim b try % 559 #n #hd #tl #inductive_hypothesis 560 change with (false:::(zero ?)) in match (zero ?); 561 >half_add_carry_Sn >inductive_hypothesis cases hd % 562 qed. 563 564 axiom half_add_true_true_carry_true: 565 ∀n: nat. 566 ∀hd, hd': bool. 567 ∀l, r: BitVector n. 568 \fst (half_add (S n) (true:::l) (true:::r)) = true. 569 570 lemma add_Sn_carry_add: 571 ∀n: nat. 572 ∀hd, hd': bool. 573 ∀l, r: BitVector n. 574 add (S n) (hd:::l) (hd':::r) = 575 xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r. 576 #n #hd #hd' #l elim l 577 [1: 578 #r cases hd cases hd' 579 >(BitVector_O … r) normalize % 580 2: 581 #n' #hd'' #tl #inductive_hypothesis #r 582 cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct 583 cases hd cases hd' cases hd'' cases hd''' 584 whd in match (xorb ??); 585 cases daemon 586 ] 587 qed. 588 589 lemma add_zero: 537 590 ∀n: nat. 538 591 ∀l: BitVector n. 539 592 l = add n l (zero …). 593 #n #l elim l try % 594 #n' #hd #tl #inductive_hypothesis 595 change with (false:::zero ?) in match (zero ?); 596 >add_Sn_carry_add >half_add_zero_carry_false 597 cases hd <inductive_hypothesis % 598 qed. 599 600 axiom most_significant_bit_zero: 601 ∀size, m: nat. 602 ∀size_proof: 0 < size. 603 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false. 604 normalize in size_proof; normalize @le_S_S assumption 605 qed. 606 607 axiom zero_add_head: 608 ∀m: nat. 609 ∀tl, hd. 610 (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl). 611 612 lemma zero_add: 613 ∀m: nat. 614 ∀b: BitVector m. 615 add m (zero m) b = b. 616 #m #b elim b try % 617 #m' #hd #tl #inductive_hypothesis 618 <inductive_hypothesis in ⊢ (???%); 619 >zero_add_head % 620 qed. 621 622 axiom bitvector_of_nat_one_Sm: 623 ∀m: nat. 624 ∃b: BitVector m. 625 bitvector_of_nat (S m) 1 ≃ b @@ [[true]]. 626 627 axiom increment_zero_bitvector_of_nat_1: 628 ∀m: nat. 629 ∀b: BitVector m. 630 increment m b = add m (bitvector_of_nat m 1) b. 540 631 541 632 axiom add_associative: 542 ∀n: nat. 543 ∀l, c, r: BitVector n. 544 add … l (add … c r) = add … (add … l c) r. 633 ∀m: nat. 634 ∀l, c, r: BitVector m. 635 add m l (add m c r) = add m (add m l c) r. 636 637 lemma bitvector_of_nat_aux_buffer: 638 ∀m, n: nat. 639 ∀b: BitVector m. 640 bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b. 641 #m #n elim n 642 [1: 643 #b change with (? = add ? (zero …) b) 644 >zero_add % 645 2: 646 #n' #inductive_hypothesis #b 647 whd in match (bitvector_of_nat_aux ???); 648 >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%); 649 >inductive_hypothesis >increment_zero_bitvector_of_nat_1 650 >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1)) 651 <add_associative % 652 ] 653 qed. 654 655 definition sign_extension: Byte → Word ≝ 656 λc. 657 let b ≝ get_index_v ? 8 c 1 ? in 658 [[ b; b; b; b; b; b; b; b ]] @@ c. 659 normalize 660 repeat (@le_S_S) 661 @le_O_n 662 qed. 663 664 lemma bitvector_of_nat_sign_extension_equivalence: 665 ∀m: nat. 666 ∀size_proof: m < 128. 667 sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m. 668 #m #size_proof whd in ⊢ (??%?); 669 >most_significant_bit_zero 670 [1: 671 elim m 672 [1: 673 % 674 2: 675 #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta 676 whd in match (bitvector_of_nat_aux ???); 677 whd in match (bitvector_of_nat_aux ???) in ⊢ (???%); 678 >(bitvector_of_nat_aux_buffer 16 n') 679 cases daemon 680 ] 681 2: 682 assumption 683 ] 684 qed. 545 685 546 686 axiom add_commutative:
Note: See TracChangeset
for help on using the changeset viewer.