# Changeset 2311 for src

Ignore:
Timestamp:
Aug 31, 2012, 2:12:39 PM (8 years ago)
Message:

Some more cleaning of switchRemoval ...

File:
1 edited

Unmodified
Added
Removed
• ## src/ASM/Arithmetic.ma

 r2192 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". (* Some properties of addition_n *) lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry. #n elim n [ 1: #a #b #carry lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl | 2: #n' #Hind #a #b #carry lapply (BitVector_Sn … a) lapply (BitVector_Sn … b) * #bhd * #btl #Heqb * #ahd * #atl #Heqa destruct lapply (Hind atl btl carry) whd in match (add_with_carries ????) in ⊢ ((??%%) →  (??%%)); normalize in match (rewrite_l ??????); normalize nodelta #Heq >Heq generalize in match (fold_right2_i ????????); * #res #carries normalize nodelta cases ahd cases bhd @refl ] qed. lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a. #n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries @refl qed. (* -------------------------------------------------------------------------- *) (* Associativity proof for addition_n. The proof relies on the observation * that the two carries (inner and outer) in the associativity equation are not * independent. In fact, the global carry can be encoded in a three-valued bits * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope * this proof can be simplified, but now it's proved at least. *) inductive ternary : Type[0] ≝ | Zero_carry : ternary | One_carry : ternary | Two_carry : ternary. definition carry_0 ≝ λcarry. match carry with [ Zero_carry ⇒ 〈false, Zero_carry〉 | One_carry ⇒ 〈true, Zero_carry〉 | Two_carry ⇒ 〈false, One_carry〉 ]. definition carry_1 ≝ λcarry. match carry with [ Zero_carry ⇒ 〈true, Zero_carry〉 | One_carry ⇒ 〈false, One_carry〉 | Two_carry ⇒ 〈true, One_carry〉 ]. definition carry_2 ≝ λcarry. match carry with [ Zero_carry ⇒ 〈false, One_carry〉 | One_carry ⇒ 〈true, One_carry〉 | Two_carry ⇒ 〈false, Two_carry〉 ]. definition carry_3 ≝ λcarry. match carry with [ Zero_carry ⇒ 〈true, One_carry〉 | One_carry ⇒ 〈false, Two_carry〉 | Two_carry ⇒ 〈true, Two_carry〉 ]. (* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry, according to the last one. *) definition ternary_carry_of ≝ λxa,xb,xc,carry. if xa then if xb then if xc then carry_3 carry else carry_2 carry else if xc then carry_2 carry else carry_1 carry else if xb then if xc then carry_2 carry else carry_1 carry else if xc then carry_1 carry else carry_0 carry. let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝ match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with [ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉 | VCons sz' xa tla ⇒ λb',c'. let xb ≝ head' … b' in let xc ≝ head' … c' in let tlb ≝ tail … b' in let tlc ≝ tail … c' in let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in 〈bit ::: bits, carry〉 ] b c. (* convert the classical carries (inner and outer) to ternary) *) definition carries_to_ternary ≝ λcarry1,carry2. if carry1 then if carry2 then Two_carry else One_carry else if carry2 then One_carry else Zero_carry. (* Copied back from Clight/casts.ma *) lemma add_with_carries_unfold : ∀n,x,y,c. add_with_carries n x y c = fold_right2_i ????? n x y. // qed. lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry. add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry = (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in let last_carry ≝ match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with [VEmpty⇒carry |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] in if last_carry then let bit   ≝ xorb (xorb a_hd b_hd) true in let carry ≝ carry_of a_hd b_hd true in 〈bit:::lower_bits,carry:::carries〉 else let bit ≝ xorb (xorb a_hd b_hd) false in let carry ≝ carry_of a_hd b_hd false in 〈bit:::lower_bits,carry:::carries〉). #n #a_hd #a_tl #b_hd #b_tl #carry whd in match (add_with_carries ????); normalize nodelta (BitVector_O … carries) normalize nodelta cases carry normalize nodelta cases a_hd cases b_hd // | 2: #n' #Hind #a_tl #b_tl #lower_bits #carries lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl #Heq >Heq normalize nodelta cases carries_hd cases a_hd cases b_hd normalize nodelta // ] qed. (* Correction of [canonical_add], left side. Note the invariant on carries. *) lemma canonical_add_left : ∀n,carry1,carry2,a,b,c. let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in res_ab_c = res_canonical ∧ (match n return λx. BitVector x → BitVector x → Prop with [ O ⇒ λ_.λ_. True | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry ] flags_ab flags_ab_c). #n elim n [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // | 2: #n' #Hind #carry1 #carry2 #a #b #c elim (BitVector_Sn … a) #xa * #a' #Heq_a elim (BitVector_Sn … b) #xb * #b' #Heq_b elim (BitVector_Sn … c) #xc * #c' #Heq_c lapply (Hind … carry1 carry2 a' b' c') -Hind destruct >add_with_carries_Sn elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a' -Hflags_ab -Hres_ab -c' -b' -a' cases n' [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab) normalize nodelta #_ cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab normalize nodelta elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta >add_with_carries_Sn elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c normalize nodelta elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c normalize nodelta cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c normalize nodelta whd in match (canonical_add (S (S ?)) ? ? ? ?); whd in match (tail ???); whd in match (tail ???); elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize * #Hres_ab_is_canonical #Hlast_carry Hres_ab_is_canonical cases xa cases xb cases xc try @conj try @refl ] ] qed. (* Symmetric. The two sides are most certainly doable in a single induction, but lazyness prevails over style.  *) lemma canonical_add_right : ∀n,carry1,carry2,a,b,c. let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in res_a_bc = res_canonical ∧ (match n return λx. BitVector x → BitVector x → Prop with [ O ⇒ λ_.λ_. True | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry ] flags_bc flags_a_bc). #n elim n [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // | 2: #n' #Hind #carry1 #carry2 #a #b #c elim (BitVector_Sn … a) #xa * #a' #Heq_a elim (BitVector_Sn … b) #xb * #b' #Heq_b elim (BitVector_Sn … c) #xc * #c' #Heq_c lapply (Hind … carry1 carry2 a' b' c') -Hind destruct >add_with_carries_Sn elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a' -Hflags_bc -Hres_bc -c' -b' -a' cases n' [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc) normalize nodelta #_ cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try // | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc normalize nodelta elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta >add_with_carries_Sn elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc normalize nodelta elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc normalize nodelta cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc whd in match (canonical_add (S (S ?)) ????); whd in match (tail ???); whd in match (tail ???); elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize * #Hres_bc_is_canonical #Hlast_carry Hres_bc_is_canonical cases xa cases xb cases xc try @conj try @refl ] ] qed. (* Note that we prove a result more general that just associativity: we can vary the carries. *) lemma associative_add_with_carries : ∀n,carry1,carry2,a,b,c. (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2)) = (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)). #n cases n [ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) normalize try @refl | 2: #n' #carry1 #carry2 #a #b #c lapply (canonical_add_left … carry1 carry2 a b c) lapply (canonical_add_right … carry1 carry2 a b c) normalize nodelta elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab normalize nodelta elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc normalize nodelta elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c normalize nodelta cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry normalize nodelta * #HA #HB * #HC #HD destruct @refl ] qed. (* This closes the proof of associativity for bitvector addition. *) 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. #n #a #b #c whd in match (addition_n ???) in ⊢ (??%%); whd in match (addition_n n b c); whd in match (addition_n n a b); lapply (associative_add_with_carries … false false a b c) elim (add_with_carries n b c false) #bc_bits #bc_flags elim (add_with_carries n a b false) #ab_bits #ab_flags normalize nodelta elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags normalize #H @H qed. definition max_u ≝ λn,a,b. if lt_u n a b then b else a. 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.