 Timestamp:
 Aug 31, 2012, 2:12:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2192 r2311 510 510 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". 511 511 512 (* Some properties of addition_n *) 513 lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry. 514 #n elim n 515 [ 1: #a #b #carry 516 lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl 517  2: #n' #Hind #a #b #carry 518 lapply (BitVector_Sn … a) lapply (BitVector_Sn … b) 519 * #bhd * #btl #Heqb 520 * #ahd * #atl #Heqa destruct 521 lapply (Hind atl btl carry) 522 whd in match (add_with_carries ????) in ⊢ ((??%%) → (??%%)); 523 normalize in match (rewrite_l ??????); 524 normalize nodelta 525 #Heq >Heq 526 generalize in match (fold_right2_i ????????); * #res #carries 527 normalize nodelta 528 cases ahd cases bhd @refl 529 ] qed. 530 531 lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a. 532 #n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries 533 @refl 534 qed. 535 536 (*  *) 537 (* Associativity proof for addition_n. The proof relies on the observation 538 * that the two carries (inner and outer) in the associativity equation are not 539 * independent. In fact, the global carry can be encoded in a threevalued bits 540 * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope 541 * this proof can be simplified, but now it's proved at least. *) 542 543 inductive ternary : Type[0] ≝ 544  Zero_carry : ternary 545  One_carry : ternary 546  Two_carry : ternary. 547 548 definition carry_0 ≝ λcarry. 549 match carry with 550 [ Zero_carry ⇒ 〈false, Zero_carry〉 551  One_carry ⇒ 〈true, Zero_carry〉 552  Two_carry ⇒ 〈false, One_carry〉 ]. 553 554 definition carry_1 ≝ λcarry. 555 match carry with 556 [ Zero_carry ⇒ 〈true, Zero_carry〉 557  One_carry ⇒ 〈false, One_carry〉 558  Two_carry ⇒ 〈true, One_carry〉 ]. 559 560 definition carry_2 ≝ λcarry. 561 match carry with 562 [ Zero_carry ⇒ 〈false, One_carry〉 563  One_carry ⇒ 〈true, One_carry〉 564  Two_carry ⇒ 〈false, Two_carry〉 ]. 565 566 definition carry_3 ≝ λcarry. 567 match carry with 568 [ Zero_carry ⇒ 〈true, One_carry〉 569  One_carry ⇒ 〈false, Two_carry〉 570  Two_carry ⇒ 〈true, Two_carry〉 ]. 571 572 (* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry, 573 according to the last one. *) 574 definition ternary_carry_of ≝ λxa,xb,xc,carry. 575 if xa then 576 if xb then 577 if xc then 578 carry_3 carry 579 else 580 carry_2 carry 581 else 582 if xc then 583 carry_2 carry 584 else 585 carry_1 carry 586 else 587 if xb then 588 if xc then 589 carry_2 carry 590 else 591 carry_1 carry 592 else 593 if xc then 594 carry_1 carry 595 else 596 carry_0 carry. 597 598 let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝ 599 match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with 600 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉 601  VCons sz' xa tla ⇒ λb',c'. 602 let xb ≝ head' … b' in 603 let xc ≝ head' … c' in 604 let tlb ≝ tail … b' in 605 let tlc ≝ tail … c' in 606 let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in 607 let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in 608 〈bit ::: bits, carry〉 609 ] b c. 610 611 (* convert the classical carries (inner and outer) to ternary) *) 612 definition carries_to_ternary ≝ λcarry1,carry2. 613 if carry1 614 then if carry2 615 then Two_carry 616 else One_carry 617 else if carry2 618 then One_carry 619 else Zero_carry. 620 621 (* Copied back from Clight/casts.ma *) 622 lemma add_with_carries_unfold : ∀n,x,y,c. 623 add_with_carries n x y c = fold_right2_i ????? n x y. 624 // qed. 625 626 lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry. 627 add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry = 628 (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in 629 let last_carry ≝ 630 match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 631 [VEmpty⇒carry 632 VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] 633 in 634 if last_carry then 635 let bit ≝ xorb (xorb a_hd b_hd) true in 636 let carry ≝ carry_of a_hd b_hd true in 637 〈bit:::lower_bits,carry:::carries〉 638 else 639 let bit ≝ xorb (xorb a_hd b_hd) false in 640 let carry ≝ carry_of a_hd b_hd false in 641 〈bit:::lower_bits,carry:::carries〉). 642 #n #a_hd #a_tl #b_hd #b_tl #carry 643 whd in match (add_with_carries ????); 644 normalize nodelta 645 <add_with_carries_unfold 646 cases (add_with_carries n a_tl b_tl carry) 647 #lower_bits #carries normalize nodelta 648 elim n in a_tl b_tl lower_bits carries; 649 [ 1: #a_tl #b_tl #lower_bits #carries 650 >(BitVector_O … carries) normalize nodelta 651 cases carry normalize nodelta 652 cases a_hd cases b_hd // 653  2: #n' #Hind #a_tl #b_tl #lower_bits #carries 654 lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl 655 #Heq >Heq normalize nodelta 656 cases carries_hd cases a_hd cases b_hd normalize nodelta 657 // 658 ] qed. 659 660 (* Correction of [canonical_add], left side. Note the invariant on carries. *) 661 lemma canonical_add_left : ∀n,carry1,carry2,a,b,c. 662 let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in 663 let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in 664 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in 665 res_ab_c = res_canonical 666 ∧ (match n return λx. BitVector x → BitVector x → Prop with 667 [ O ⇒ λ_.λ_. True 668  S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry 669 ] flags_ab flags_ab_c). 670 #n elim n 671 [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 672  2: #n' #Hind #carry1 #carry2 #a #b #c 673 elim (BitVector_Sn … a) #xa * #a' #Heq_a 674 elim (BitVector_Sn … b) #xb * #b' #Heq_b 675 elim (BitVector_Sn … c) #xc * #c' #Heq_c 676 lapply (Hind … carry1 carry2 a' b' c') Hind 677 destruct >add_with_carries_Sn 678 elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta 679 lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a' 680 Hflags_ab Hres_ab c' b' a' 681 cases n' 682 [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 683 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 684 >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab) 685 normalize nodelta #_ 686 cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // 687  2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 688 elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab 689 normalize nodelta 690 elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab 691 cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta 692 >add_with_carries_Sn 693 elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c 694 normalize nodelta 695 elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c 696 normalize nodelta 697 cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c 698 normalize nodelta 699 whd in match (canonical_add (S (S ?)) ? ? ? ?); 700 whd in match (tail ???); whd in match (tail ???); 701 elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize 702 * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize 703 >Hres_ab_is_canonical 704 cases xa cases xb cases xc try @conj try @refl 705 ] 706 ] qed. 707 708 (* Symmetric. The two sides are most certainly doable in a single induction, but lazyness 709 prevails over style. *) 710 lemma canonical_add_right : ∀n,carry1,carry2,a,b,c. 711 let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in 712 let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in 713 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in 714 res_a_bc = res_canonical 715 ∧ (match n return λx. BitVector x → BitVector x → Prop with 716 [ O ⇒ λ_.λ_. True 717  S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry 718 ] flags_bc flags_a_bc). 719 #n elim n 720 [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 721  2: #n' #Hind #carry1 #carry2 #a #b #c 722 elim (BitVector_Sn … a) #xa * #a' #Heq_a 723 elim (BitVector_Sn … b) #xb * #b' #Heq_b 724 elim (BitVector_Sn … c) #xc * #c' #Heq_c 725 lapply (Hind … carry1 carry2 a' b' c') Hind 726 destruct >add_with_carries_Sn 727 elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta 728 lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a' 729 Hflags_bc Hres_bc c' b' a' 730 cases n' 731 [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 732 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 733 >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc) 734 normalize nodelta #_ 735 cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // 736  2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 737 elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc 738 normalize nodelta 739 elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc 740 cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta 741 >add_with_carries_Sn 742 elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc 743 normalize nodelta 744 elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc 745 normalize nodelta 746 cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc 747 whd in match (canonical_add (S (S ?)) ????); 748 whd in match (tail ???); whd in match (tail ???); 749 elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize 750 * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize 751 >Hres_bc_is_canonical 752 cases xa cases xb cases xc try @conj try @refl 753 ] 754 ] qed. 755 756 757 (* Note that we prove a result more general that just associativity: we can vary the carries. *) 758 lemma associative_add_with_carries : 759 ∀n,carry1,carry2,a,b,c. 760 (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2)) 761 = 762 (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)). 763 #n cases n 764 [ 1: #carry1 #carry2 #a #b #c 765 >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) 766 normalize try @refl 767  2: #n' #carry1 #carry2 #a #b #c 768 lapply (canonical_add_left … carry1 carry2 a b c) 769 lapply (canonical_add_right … carry1 carry2 a b c) 770 normalize nodelta 771 elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc 772 elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab 773 normalize nodelta 774 elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc 775 normalize nodelta 776 elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c 777 normalize nodelta 778 cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry 779 normalize nodelta 780 * #HA #HB * #HC #HD destruct @refl 781 ] qed. 782 783 (* This closes the proof of associativity for bitvector addition. *) 784 785 lemma associative_addition_n : ∀n,a,b,c. addition_n n a (addition_n n b c) = addition_n n (addition_n n a b) c. 786 #n #a #b #c 787 whd in match (addition_n ???) in ⊢ (??%%); 788 whd in match (addition_n n b c); 789 whd in match (addition_n n a b); 790 lapply (associative_add_with_carries … false false a b c) 791 elim (add_with_carries n b c false) #bc_bits #bc_flags 792 elim (add_with_carries n a b false) #ab_bits #ab_flags 793 normalize nodelta 794 elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags 795 elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags 796 normalize 797 #H @H 798 qed. 799 800 801 512 802 definition max_u ≝ λn,a,b. if lt_u n a b then b else a. 513 803 definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
Note: See TracChangeset
for help on using the changeset viewer.