Changeset 2311 for src/ASM/Arithmetic.ma


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

Some more cleaning of switchRemoval ...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2192 r2311  
    510510alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
    511511
     512(* Some properties of addition_n *)
     513lemma 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
     531lemma 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
     534qed.
     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 three-valued 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
     543inductive ternary : Type[0] ≝
     544| Zero_carry : ternary
     545| One_carry : ternary
     546| Two_carry : ternary.
     547
     548definition 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   
     554definition 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
     560definition 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
     566definition 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. *)
     574definition ternary_carry_of ≝ λxa,xb,xc,carry.
     575if 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
     586else
     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
     598let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
     599match 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) *)
     612definition 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 *)
     622lemma 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   
     626lemma 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
     643whd in match (add_with_carries ????);
     644normalize nodelta
     645<add_with_carries_unfold
     646cases (add_with_carries n a_tl b_tl carry)
     647#lower_bits #carries normalize nodelta
     648elim 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. *)
     661lemma 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.  *)
     710lemma 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. *)
     758lemma 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
     785lemma 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
     787whd in match (addition_n ???) in ⊢ (??%%);
     788whd in match (addition_n n b c);
     789whd in match (addition_n n a b);
     790lapply (associative_add_with_carries … false false a b c)
     791elim (add_with_carries n b c false) #bc_bits #bc_flags
     792elim (add_with_carries n a b false) #ab_bits #ab_flags
     793normalize nodelta
     794elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
     795elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
     796normalize
     797#H @H
     798qed.
     799
     800
     801
    512802definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
    513803definition 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.