Changeset 2304


Ignore:
Timestamp:
Aug 29, 2012, 11:21:49 PM (7 years ago)
Author:
garnier
Message:

Strengthened proof of associativity of bitvector addition. Some more lemmas on two complement negation wrt addition proved, through a slight detour using an ad-hoc definition of addition with explicit carries.
All of that to prove that -(a + b) = -a + -b, needed in turn for a simulation result on pointer subtractions.
switchRemoval.ma now typechecks. TBF: simulation proof for the transformation itself.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2302 r2304  
    20662066    〈f',vars〉 = function_switch_removal f →
    20672067    disjoint_extension env m env' m' vars E Hext →
    2068     switch_removal s (map ?? (fst ??) vars) u = Some ? result → 
     2068    switch_removal s (map ?? (fst ??) vars) u = Some ? result →
    20692069    switch_cont_sim (map ?? (fst ??) vars) k k' →
    20702070    switch_state_sim
     
    23282328] qed.
    23292329
     2330   
     2331lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
     2332#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
     2333@refl
     2334qed.
     2335
    23302336(* -------------------------------------------------------------------------- *)
    23312337(* Associativity proof for addition_n. The proof relies on the observation
     
    23892395      carry_0 carry.
    23902396
    2391 let rec canonical_add (n : nat) (a,b,c : BitVector n) on a : (BitVector n × ternary) ≝
     2397let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
    23922398match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with
    2393 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, Zero_carry
     2399[ VEmpty ⇒ λ_,_. 〈VEmpty ?, init
    23942400| VCons sz' xa tla ⇒ λb',c'.
    23952401  let xb ≝ head' … b' in
     
    23972403  let tlb ≝ tail … b' in
    23982404  let tlc ≝ tail … c' in
    2399   let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc in
     2405  let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in
    24002406  let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in
    24012407  〈bit ::: bits, carry〉
     
    24442450     cases carries_hd cases a_hd cases b_hd normalize nodelta
    24452451     //
    2446 ] qed. 
     2452] qed.
    24472453
    24482454(* Correction of [canonical_add], left side. Note the invariant on carries. *)
    2449 lemma canonical_add_left : ∀n,a,b,c.
    2450   let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b false in
    2451   let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c false in
    2452   let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in
     2455lemma canonical_add_left : ∀n,carry1,carry2,a,b,c.
     2456  let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in
     2457  let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in
     2458  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
    24532459  res_ab_c = res_canonical
    24542460  ∧ (match n return λx. BitVector x → BitVector x → Prop with
     
    24572463     ] flags_ab flags_ab_c).
    24582464#n elim n
    2459 [ 1: #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
    2460 | 2: #n' #Hind #a #b #c
     2465[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
     2466| 2: #n' #Hind #carry1 #carry2 #a #b #c
    24612467     elim (BitVector_Sn … a) #xa * #a' #Heq_a
    24622468     elim (BitVector_Sn … b) #xb * #b' #Heq_b
    2463      elim (BitVector_Sn … c) #xc * #c' #Heq_c     
    2464      lapply (Hind … a' b' c') -Hind
     2469     elim (BitVector_Sn … c) #xc * #c' #Heq_c
     2470     lapply (Hind … carry1 carry2 a' b' c') -Hind
    24652471     destruct >add_with_carries_Sn
    2466      elim (add_with_carries … a' b' false) #Hres_ab #Hflags_ab normalize nodelta
     2472     elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta
    24672473     lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a'
    24682474     -Hflags_ab -Hres_ab -c' -b' -a'
     
    24722478          >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab)
    24732479          normalize nodelta #_
    2474           cases xa cases xb cases xc normalize @conj try //
     2480          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
    24752481     | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
    24762482          elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
     
    24792485          cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta
    24802486          >add_with_carries_Sn
    2481           elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' false) #res_ab_c #flags_ab_c
     2487          elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c
    24822488          normalize nodelta
    24832489          elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c
    24842490          normalize nodelta
    2485           cases (hd_flags_ab_c) in Heq_flags_ab_c; #Heq_flags_ab_c
    2486           normalize nodelta normalize
    2487           elim (canonical_add (S n') a' b' c') #res_canonical #last_carry normalize
    2488           * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
     2491          cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c
     2492          normalize nodelta
     2493          whd in match (canonical_add (S (S ?)) ? ? ? ?);
     2494          whd in match (tail ???); whd in match (tail ???);
     2495          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
     2496          * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
    24892497          >Hres_ab_is_canonical
    24902498          cases xa cases xb cases xc try @conj try @refl
    24912499     ]
    2492 ] qed.     
     2500] qed.
    24932501
    24942502(* Symmetric. The two sides are most certainly doable in a single induction, but lazyness
    24952503   prevails over style.  *)
    2496 lemma canonical_add_right : ∀n,a,b,c.
    2497   let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c false in
    2498   let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc false in
    2499   let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in
     2504lemma canonical_add_right : ∀n,carry1,carry2,a,b,c.
     2505  let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in
     2506  let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in
     2507  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
    25002508  res_a_bc = res_canonical
    25012509  ∧ (match n return λx. BitVector x → BitVector x → Prop with
     
    25042512     ] flags_bc flags_a_bc).
    25052513#n elim n
    2506 [ 1: #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
    2507 | 2: #n' #Hind #a #b #c
     2514[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
     2515| 2: #n' #Hind #carry1 #carry2 #a #b #c
    25082516     elim (BitVector_Sn … a) #xa * #a' #Heq_a
    25092517     elim (BitVector_Sn … b) #xb * #b' #Heq_b
    2510      elim (BitVector_Sn … c) #xc * #c' #Heq_c     
    2511      lapply (Hind … a' b' c') -Hind
     2518     elim (BitVector_Sn … c) #xc * #c' #Heq_c
     2519     lapply (Hind … carry1 carry2 a' b' c') -Hind
    25122520     destruct >add_with_carries_Sn
    2513      elim (add_with_carries … b' c' false) #Hres_bc #Hflags_bc normalize nodelta
     2521     elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta
    25142522     lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a'
    25152523     -Hflags_bc -Hres_bc -c' -b' -a'
     
    25192527          >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc)
    25202528          normalize nodelta #_
    2521           cases xa cases xb cases xc normalize @conj try //
     2529          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
    25222530     | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
    25232531          elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc
     
    25262534          cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta
    25272535          >add_with_carries_Sn
    2528           elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) false) #res_a_bc #flags_a_bc
     2536          elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc
    25292537          normalize nodelta
    25302538          elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc
    25312539          normalize nodelta
    25322540          cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc
    2533           normalize
    2534           elim (canonical_add (S n') a' b' c') #res_canonical #last_carry normalize
     2541          whd in match (canonical_add (S (S ?)) ????);
     2542          whd in match (tail ???); whd in match (tail ???);
     2543          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
    25352544          * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize
    25362545          >Hres_bc_is_canonical
     
    25392548] qed.
    25402549
     2550
     2551(* Note that we prove a result more general that just associativity: we can vary the carries. *)
    25412552lemma associative_add_with_carries :
    2542   ∀n,a,b,c.
    2543   (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c false in res) false))
     2553  ∀n,carry1,carry2,a,b,c.
     2554  (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2))
    25442555   =
    2545   (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b false in res) c false)).
     2556  (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)).
    25462557#n cases n
    2547 [ 1: #a #b #c
     2558[ 1: #carry1 #carry2 #a #b #c
    25482559      >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c)
    25492560      normalize try @refl
    2550 | 2: #n' #a #b #c     
    2551      lapply (canonical_add_left … a b c) lapply (canonical_add_right … a b c)
     2561| 2: #n' #carry1 #carry2 #a #b #c
     2562     lapply (canonical_add_left … carry1 carry2 a b c)
     2563     lapply (canonical_add_right … carry1 carry2 a b c)
    25522564     normalize nodelta
    2553      elim (add_with_carries (S n') b c false) #res_bc #flags_bc
    2554      elim (add_with_carries (S n') a b false) #res_ab #flags_ab
     2565     elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc
     2566     elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab
    25552567     normalize nodelta
    2556      elim (add_with_carries (S n') a res_bc false) #res_a_bc #flags_a_bc
    2557      elim (add_with_carries (S n') res_ab c false) #res_ab_c #flags_ab_c
     2568     elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc
     2569     normalize nodelta     
     2570     elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c
    25582571     normalize nodelta
    2559      cases (canonical_add ? a b c) #canonical_bits #last_carry
     2572     cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry
    25602573     normalize nodelta
    25612574     * #HA #HB * #HC #HD destruct @refl
     
    25632576
    25642577(* This closes the proof of associativity for bitvector addition. *)     
    2565    
    2566 lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
    2567 #n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
    2568 @refl
    2569 qed.
    25702578
    25712579lemma 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.
     
    25742582whd in match (addition_n n b c);
    25752583whd in match (addition_n n a b);
    2576 lapply (associative_add_with_carries … a b c)
     2584lapply (associative_add_with_carries … false false a b c)
    25772585elim (add_with_carries n b c false) #bc_bits #bc_flags
    25782586elim (add_with_carries n a b false) #ab_bits #ab_flags
     
    26712679     ]
    26722680] qed.
    2673 
    2674 lemma fold_right2_O : ∀A,B,C,f,init,vec1,vec2.
    2675   fold_right2_i A B C f init 0 vec1 vec2 = init.
    2676 #A #B #C #f #init #vec1 #vec2
    2677 >(Vector_O … vec1) 
    2678 >(Vector_O … vec2)
    2679 normalize @refl
    2680 qed.
    2681 
    2682 lemma map_unfold : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n.
     2681       
     2682lemma map_Sn : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n.
    26832683  map A B (S n) f (hd ::: tl) = (f hd) ::: (map A B n f tl).
    26842684#A #B #n #f #hd #tl normalize @refl qed.
    26852685
    2686 lemma replicate_unfold : ∀A,sz,elt.
     2686lemma replicate_Sn : ∀A,sz,elt.
    26872687  replicate A (S sz) elt = elt ::: (replicate A sz elt).
    26882688// qed.
    26892689
    2690 axiom subtraction_delta : ∀x,y,delta.
     2690lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
     2691
     2692lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
     2693#n #xa #a normalize @refl qed.
     2694
     2695
     2696(* useful facts on xorb *)
     2697
     2698lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed.
     2699lemma xorb_false : ∀a. xorb a false = a. * @refl qed.
     2700lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed.
     2701lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed.
     2702lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed.
     2703lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed.
     2704lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed.
     2705lemma xorb_inj : ∀a,b,c. xorb a b = xorb a c ↔ b = c. * * * @conj try // normalize try // qed.
     2706
     2707(* useful facts on carry_of *)
     2708lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
     2709lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
     2710lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
     2711lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
     2712lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
     2713
     2714(* useful facts on various boolean operations *)
     2715lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
     2716lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
     2717lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
     2718lemma notb_true : notb true = false. // qed.
     2719lemma notb_false : notb false = true. % #H destruct qed.
     2720lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
     2721
     2722(*
     2723let rec one_bv (n : nat) on n : BitVector n ≝
     2724match n return λx. BitVector x with
     2725[ O ⇒ [[]]
     2726| S x' ⇒
     2727  match x' return λx. x = x' → BitVector (S x) with
     2728  [ O ⇒ λ_. [[true]]
     2729  | S x ⇒ λH. ? ] (refl ? x') ].
     2730>H @(false ::: (one_bv x'))
     2731qed.
     2732*)
     2733definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
     2734
     2735lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
     2736    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
     2737    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
     2738#n elim n
     2739[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
     2740     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
     2741     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
     2742     normalize #Heq destruct (Heq) @refl
     2743| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
     2744     destruct #Hind >add_with_carries_Sn >replicate_Sn
     2745     whd in match (zero ?) in Hind; lapply Hind
     2746     elim (add_with_carries (S (S n'))
     2747            (false:::replicate bool (S n') false)
     2748            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
     2749            normalize >add_with_carries_Sn in Hind;
     2750     elim (add_with_carries (S n') (replicate bool (S n') false)
     2751                    (replicate bool (S n') false) true) #flags' #bits'
     2752     normalize
     2753     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
     2754            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
     2755     normalize #Heq destruct @refl
     2756] qed.     
     2757
     2758lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
     2759#n lapply (one_bv_Sn_aux n)
     2760whd in match (one_bv ?) in ⊢ (? → (??%%));
     2761elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
     2762#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
     2763qed.
     2764
     2765lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
     2766    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
     2767#n   
     2768elim n
     2769[ 1: #a >(BitVector_O … a) normalize @refl
     2770| 2: #n' cases n'
     2771     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
     2772          >(BitVector_O … tl) normalize cases xa @refl
     2773     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
     2774          >one_bv_Sn >zero_Sn
     2775          lapply (Hind tl)
     2776          >add_with_carries_Sn >add_with_carries_Sn
     2777          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
     2778          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
     2779          normalize nodelta @refl
     2780] qed.         
     2781
     2782(* In order to use associativity on increment, we hide it under addition_n. *)
     2783lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
     2784#n
     2785whd in match (increment ??) in ⊢ (∀_.??%?);
     2786whd in match (addition_n ???) in ⊢ (∀_.???%);
     2787#a lapply (increment_to_addition_n_aux n a)
     2788#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
     2789qed.
     2790
     2791(* Explicit formulation of addition *)
     2792
     2793(* Explicit formulation of the last carry bit *)
     2794let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
     2795match n return λx. BitVector x → BitVector x → bool with
     2796[ O ⇒ λ_,_. init
     2797| S x ⇒ λa',b'.
     2798  let hd_a ≝ head' … a' in
     2799  let hd_b ≝ head' … b' in
     2800  let tl_a ≝ tail … a' in
     2801  let tl_b ≝ tail … b' in
     2802  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
     2803] a b.
     2804
     2805lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
     2806  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
     2807#n #init #a #b @refl qed.
     2808
     2809lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
     2810  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
     2811
     2812(* correction of [ith_carry] *)
     2813lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
     2814  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
     2815  head' … flags_ab = ith_carry ? a b init.
     2816#n elim n
     2817[ 1: #init #a #b #res_ab #flags_ab
     2818     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     2819     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     2820     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     2821     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     2822     destruct
     2823     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
     2824     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
     2825     @refl
     2826| 2: #n' #Hind #init #a #b #res_ab #flags_ab
     2827     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     2828     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     2829     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     2830     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     2831     destruct
     2832     lapply (Hind … init tl_a tl_b tl_res tl_flags)
     2833     >add_with_carries_Sn >(ith_carry_Sn (S n'))
     2834     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
     2835     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
     2836     normalize nodelta cases hd_flags_ab normalize nodelta
     2837     whd in match (head' ? (S n') ?); #H1 #H2
     2838     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
     2839] qed.
     2840
     2841(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
     2842definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
     2843match n return λx. BitVector x → BitVector x → bool with
     2844[ O ⇒ λ_,_. init
     2845| S x ⇒ λa',b'.
     2846  let hd_a ≝ head' … a' in
     2847  let hd_b ≝ head' … b' in
     2848  let tl_a ≝ tail … a' in
     2849  let tl_b ≝ tail … b' in
     2850  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
     2851] a b.
     2852
     2853lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
     2854  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
     2855#n #a #b // qed.
     2856
     2857lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
     2858  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
     2859
     2860(* correction of ith_bit *)
     2861lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
     2862  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
     2863  head' … res_ab = ith_bit ? a b init.
     2864#n
     2865cases n
     2866[ 1: #init #a #b #res_ab #flags_ab
     2867     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     2868     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     2869     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     2870     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     2871     destruct
     2872     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
     2873     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
     2874     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
     2875| 2: #n' #init #a #b #res_ab #flags_ab
     2876     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
     2877     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
     2878     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
     2879     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
     2880     destruct
     2881     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
     2882     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
     2883     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
     2884     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
     2885     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
     2886     <(H1 (refl ??)) @refl
     2887] qed.
     2888
     2889(* Transform a function from bit-vectors to bits into a vector by folding *)
     2890let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
     2891match v with
     2892[ VEmpty ⇒ VEmpty ?
     2893| VCons sz elt tl ⇒
     2894  let bit ≝ f ? v in
     2895  bit ::: (bitvector_fold ? tl f)
     2896].
     2897
     2898(* Two-arguments version *)
     2899let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
     2900match v1  with
     2901[ VEmpty ⇒ λ_. VEmpty ?
     2902| VCons sz elt tl ⇒ λv2'.
     2903  let bit ≝ f ? v1 v2 in
     2904  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
     2905] v2.
     2906
     2907lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
     2908  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
     2909
     2910(* These functions pack all the relevant information (including carries) directly. *)
     2911definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
     2912
     2913lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
     2914  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
     2915 
     2916lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
     2917
     2918(* Prove the equivalence of addition_n_direct with add_with_carries *)
     2919lemma addition_n_direct_ok : ∀n,carry,v1,v2.
     2920  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
     2921#n elim n
     2922[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
     2923| 2: #n' #Hind #carry #v1 #v2
     2924     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
     2925     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
     2926     lapply (Hind carry tl1 tl2)
     2927     lapply (ith_bit_ok ? carry v1 v2)
     2928     lapply (ith_carry_ok ? carry v1 v2)
     2929     destruct
     2930     #Hind >addition_n_direct_Sn
     2931     >ith_bit_Sn >add_with_carries_Sn
     2932     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
     2933     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
     2934            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
     2935     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
     2936     whd in match head'; normalize nodelta
     2937     #H1 #H2 >H1 >H2 @refl
     2938] qed.
     2939 
     2940(* trivially lift associativity to our new setting *)     
     2941lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
     2942  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
     2943  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
     2944#n #carry1 #carry2 #v1 #v2 #v3
     2945<addition_n_direct_ok <addition_n_direct_ok
     2946<addition_n_direct_ok <addition_n_direct_ok
     2947lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
     2948elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
     2949elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
     2950#H @(sym_eq … H)
     2951qed.
     2952
     2953lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
     2954  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
     2955#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
     2956qed.
     2957
     2958definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
     2959definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
     2960
     2961(* fold andb on a bitvector. *)
     2962let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
     2963match b with
     2964[ VEmpty ⇒ true
     2965| VCons sz elt tl ⇒
     2966  andb elt (andb_fold ? tl)
     2967].
     2968
     2969lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
     2970
     2971lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
     2972#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
     2973qed.
     2974
     2975lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
     2976  ith_carry … a (one_bv ?) false = andb_fold … a.
     2977#n elim n
     2978[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
     2979     cases hd normalize @refl
     2980| 2: #n' #Hind #a
     2981     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     2982     lapply (Hind … tl) #Hind >one_bv_Sn
     2983     >ith_carry_Sn whd in match (andb_fold ??);
     2984     cases hd >Hind @refl
     2985] qed.
     2986
     2987lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
     2988  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
     2989#n #a
     2990elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     2991whd in match (head' ???);
     2992-a cases n in tl;
     2993[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
     2994| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
     2995     >ith_increment_carry >tail_Sn
     2996     cases hd try //
     2997] qed.
     2998
     2999(* Lemma used to prove involutivity of two-complement negation *)
     3000lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
     3001   (andb_fold (S n) (negation_bv (S n) v) =
     3002    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
     3003#n elim n
     3004[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
     3005| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     3006     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
     3007     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
     3008     cases hd normalize nodelta
     3009     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
     3010     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
     3011     >ith_increment_carry
     3012     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
     3013] qed.
     3014   
     3015(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
     3016lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
     3017#n elim n
     3018[ 1: #v >(BitVector_O v) @refl
     3019| 2: #n' cases n'
     3020     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     3021          >(BitVector_O … tl) normalize cases hd @refl
     3022     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     3023          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
     3024          whd in match twocomp_neg_direct; normalize nodelta
     3025          whd in match increment_direct; normalize nodelta
     3026          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
     3027          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
     3028          generalize in match (addition_n_direct (S n'')
     3029                                                   (negation_bv (S n'')
     3030                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
     3031                                                   (one_bv (S n'')) false); #tail
     3032          >ith_increment_carry >ith_increment_carry
     3033          cases hd normalize nodelta
     3034          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
     3035          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
     3036          <twocomp_neg_involutive_aux
     3037          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
     3038      ]
     3039] qed.
     3040
     3041lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
     3042#n #a #b #va #vb #H destruct (H) @conj @refl qed.
     3043
     3044lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
     3045
     3046(* Injectivity of increment *)
     3047lemma increment_inj : ∀n. ∀a,b : BitVector n.
     3048  increment_direct ? a = increment_direct ? b →
     3049  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
     3050#n whd in match increment_direct; normalize nodelta elim n
     3051[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
     3052| 2: #n' cases n'
     3053   [ 1: #_ #a #b
     3054        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
     3055        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
     3056        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
     3057        normalize #H @conj try //
     3058   | 2: #n'' #Hind #a #b
     3059        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
     3060        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
     3061        lapply (Hind … tl_a tl_b) -Hind #Hind
     3062        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
     3063        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
     3064        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
     3065        lapply (Hind Heq2) * #Heq3 #Heq4
     3066        cut (hd_a = hd_b)
     3067        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
     3068             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
     3069             @refl ]
     3070        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
     3071        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
     3072] qed.
     3073
     3074(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
     3075lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
     3076  a = b → increment_direct ? a = increment_direct ? b. // qed.
     3077
     3078lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
     3079
     3080lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
     3081   ith_carry (S n) a (one_bv (S n)) false
     3082   = ith_carry (S n) a (zero (S n)) true.
     3083#n elim n
     3084[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
     3085| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
     3086     lapply (Hind tl_a) #Hind
     3087     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
     3088] qed.
     3089
     3090lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
     3091#n elim n //
     3092#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
     3093>ith_carry_Sn >(Hind tl) cases hd @refl.
     3094qed.
     3095
     3096lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
     3097  addition_n_direct ? v (zero ?) false = v.
     3098#n elim n
     3099[ 1: #v >(BitVector_O … v) normalize @refl
     3100| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
     3101     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
     3102     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
     3103     >xorb_false @refl
     3104] qed.
     3105
     3106lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
     3107#n elim n
     3108[ 1: #a >(BitVector_O … a) normalize @refl
     3109| 2: #n' cases n'
     3110     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
     3111     | 2: #n'' #Hind #a
     3112          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
     3113          lapply (Hind tl_a) -Hind #Hind
     3114          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
     3115          >addition_n_direct_Sn >ith_bit_Sn
     3116          >xorb_false >Hind @bitvector_cons_eq
     3117          >increment_to_carry_aux @refl
     3118     ]
     3119] qed.
     3120
     3121lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
     3122  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
     3123#n #a #b >increment_to_carry_zero <associative_addition_n_direct
     3124>neutral_addition_n_direct @refl
     3125qed.
     3126
     3127(* Prove -(a + b) = -a + -b *)
     3128lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
     3129  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
     3130whd in match twocomp_neg_direct; normalize nodelta
     3131lapply increment_inj_inv
     3132whd in match increment_direct; normalize nodelta
     3133#H #n #a #b
     3134<associative_addition_n_direct @H
     3135>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
     3136>increment_to_carry
     3137-H lapply b lapply a -b -a
     3138cases n
     3139[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
     3140| 2: #n' #a #b
     3141     cut (negation_bv ? (addition_n_direct ? a b false)
     3142           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
     3143          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
     3144     [ -n lapply b lapply a elim n'
     3145     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
     3146          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
     3147          cases hd_a cases hd_b normalize @conj @refl
     3148     | 2: #n #Hind #a #b
     3149          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
     3150          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
     3151          lapply (Hind tl_a tl_b) * #H1 #H2
     3152          @conj
     3153          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
     3154               >carry_notb >H2 @refl
     3155          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
     3156               >negation_bv_Sn >negation_bv_Sn
     3157               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
     3158               >xorb_lneg >xorb_rneg >notb_notb
     3159               <xorb_rneg >H2 @refl
     3160          ]
     3161      ] ]
     3162      * #H1 #H2 @H1
     3163] qed.
     3164
     3165lemma addition_n_direct_neg : ∀n. ∀a.
     3166 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
     3167 ∧ (ith_carry n a (negation_bv n a) false = false).
     3168#n elim n
     3169[ 1: #a >(BitVector_O … a) @conj @refl
     3170| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
     3171     lapply (Hind … tl) -Hind * #HA #HB
     3172     @conj
     3173     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
     3174     | 1: >negation_bv_Sn >addition_n_direct_Sn
     3175          >ith_bit_Sn >HB >xorb_false >HA
     3176          @bitvector_cons_eq elim hd @refl
     3177     ]
     3178] qed.     
     3179
     3180(* -a + a = 0 *)
     3181lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
     3182whd in match twocomp_neg_direct;
     3183whd in match increment_direct;
     3184normalize nodelta
     3185#n #a <associative_addition_n_direct
     3186elim (addition_n_direct_neg … a) #H #_ >H
     3187-H -a
     3188cases n try //
     3189#n'
     3190cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
     3191       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
     3192[ elim n'
     3193     [ 1: @conj @refl
     3194     | 2: #n' * #HA #HB @conj
     3195          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
     3196               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
     3197          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
     3198     ]
     3199] * #H1 #H2 @H1
     3200qed.
     3201
     3202(* Lift back the previous result to standard operations. *)
     3203lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
     3204#n #v whd in match twocomp_neg_direct; normalize nodelta
     3205whd in match increment_direct; normalize nodelta
     3206whd in match two_complement_negation; normalize nodelta
     3207>increment_to_addition_n <addition_n_direct_ok
     3208whd in match addition_n; normalize nodelta
     3209elim (add_with_carries ????) #a #b @refl
     3210qed.
     3211
     3212lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
     3213  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
     3214#n #a #b
     3215lapply (twocomp_neg_plus ? a b)
     3216>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
     3217<addition_n_direct_ok <addition_n_direct_ok
     3218whd in match addition_n; normalize nodelta
     3219elim (add_with_carries n a b false) #bits #flags normalize nodelta
     3220elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
     3221normalize nodelta #H @H
     3222qed.
     3223
     3224lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
     3225#n #a lapply (bitvector_opp_direct ? a)
     3226>twocomp_neg_direct_ok <addition_n_direct_ok
     3227whd in match (addition_n ???);
     3228elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
     3229qed.
     3230
     3231lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
     3232#n #a
     3233lapply (neutral_addition_n_direct n a)
     3234<addition_n_direct_ok
     3235whd in match (addition_n ???);
     3236elim (add_with_carries n a (zero n) false) #bits #flags #H @H
     3237qed.
     3238   
     3239lemma subtraction_delta : ∀x,y,delta.
    26913240  subtraction offset_size
    26923241    (addition_n offset_size x delta)
    26933242    (addition_n offset_size y delta) =
    26943243  subtraction offset_size x y.
    2695 (*
    2696 elim offset_size
    2697 [ 1: #x #y #delta
    2698      >(BitVector_O … x)
    2699      >(BitVector_O … y)
    2700      >(BitVector_O … delta)
    2701      //
    2702      
    2703 | 2: #sz elim sz (* I would like to do this elim much later, but it fails. *)
    2704     [ 1: #Hind #x #y #delta
    2705          lapply (BitVector_Sn … x)
    2706          lapply (BitVector_Sn … y)
    2707          lapply (BitVector_Sn … delta)
    2708          * #delta_hd * #delta_tl #Heq_delta
    2709          * #y_hd * #y_tl #Heq_y
    2710          * #x_hd * #x_tl #Heq_x
    2711          destruct
    2712          whd in match (addition_n ? (x_hd:::x_tl) ?);
    2713          whd in match (addition_n ? (y_hd:::y_tl) ?);
    2714          >add_with_carries_unfold
    2715          >add_with_carries_unfold
    2716          >fold_right2_i_unfold
    2717          >fold_right2_i_unfold
    2718          <add_with_carries_unfold
    2719          <add_with_carries_unfold
    2720          cases (add_with_carries 0 x_tl delta_tl false);
    2721          #x_delta_res #x_delta_flags normalize nodelta
    2722          cases (add_with_carries 0 y_tl delta_tl false)
    2723          #y_delta_res #y_delta_flags normalize nodelta
    2724          >(BitVector_O … x_delta_flags)
    2725          >(BitVector_O … y_delta_flags)
    2726          >(BitVector_O … x_delta_res)
    2727          >(BitVector_O … y_delta_res)
    2728          normalize nodelta
    2729          whd in match (xorb ? false) in ⊢ (??(??%%)?); normalize nodelta
    2730          whd in match (subtraction ???) in ⊢ (??%%);
    2731          >add_with_carries_unfold
    2732          whd in match (two_complement_negation ??);
    2733          whd in match (negation_bv ??);
    2734          whd in match (zero ?);
    2735          >add_with_carries_unfold
    2736          >fold_right2_i_unfold >fold_right2_O
    2737          normalize nodelta
    2738          >fold_right2_i_unfold >fold_right2_O
    2739          normalize nodelta
    2740          cases x_hd cases y_hd cases delta_hd normalize try @refl
    2741     | 2: #sz' #HindA #HindB #x #y #delta
    2742          lapply (BitVector_Sn … x)
    2743          lapply (BitVector_Sn … y)
    2744          lapply (BitVector_Sn … delta)
    2745          * #delta_hd * #delta_tl #Heq_delta
    2746          * #y_hd * #y_tl #Heq_y
    2747          * #x_hd * #x_tl #Heq_x
    2748          lapply (HindB x_tl y_tl delta_tl)
    2749          destruct
    2750          whd in match (addition_n ???) in ⊢ ((??(??%%)?) → ?); #Hind0
    2751          whd in match (addition_n ? (x_hd:::x_tl) ?);
    2752          whd in match (addition_n ? (y_hd:::y_tl) ?);
    2753          >add_with_carries_unfold
    2754          >add_with_carries_unfold
    2755          >fold_right2_i_unfold
    2756          >fold_right2_i_unfold
    2757          <add_with_carries_unfold
    2758          <add_with_carries_unfold
    2759          cases (add_with_carries (S sz') x_tl delta_tl false) in Hind0;
    2760          #x_delta_res #x_delta_flags normalize nodelta
    2761          cases (add_with_carries (S sz') y_tl delta_tl false)
    2762          #y_delta_res #y_delta_flags normalize nodelta
    2763          elim (BitVector_Sn … x_delta_flags) #hd_x_delta * #tl_x_delta #Heq_xdelta >Heq_xdelta
    2764          elim (BitVector_Sn … y_delta_flags) #hd_y_delta * #tl_y_delta #Heq_ydelta >Heq_ydelta
    2765          #Heq_ind
    2766          normalize nodelta
    2767          cases hd_x_delta cases hd_y_delta normalize nodelta
    2768          whd in match (subtraction ???) in ⊢ (??%%);
    2769          whd in match (two_complement_negation ??) in ⊢ (??%%);
    2770          whd in match (negation_bv ??) in ⊢ (??%%);
    2771          whd in match (zero (S (S sz')));
    2772          >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (??%?);
    2773          >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (???%);
    2774          lapply (add_with_carries_unfold
    2775                        (S (S sz'))
    2776                        ((¬y_hd):::map bool bool (S sz') notb y_tl)
    2777                        (false:::replicate bool (S sz') false)
    2778                        true) #Heq >Heq
    2779          >fold_right2_i_unfold >fold_right2_i_unfold
    2780          >add_with_carries_unfold in ⊢ (???(match (???%?) with [ _ ⇒ ? ] ));
    2781 
    2782 *)
     3244#x #y #delta whd in match subtraction; normalize nodelta
     3245(* Remove all the equal parts on each side of the equation. *)
     3246<associative_addition_n
     3247>two_complement_negation_plus
     3248<(commutative_addition_n … (two_complement_negation ? delta))
     3249>(associative_addition_n ? delta) >bitvector_opp_addition_n
     3250>(commutative_addition_n ? (zero ?)) >neutral_addition_n
     3251@refl
     3252qed.
    27833253
    27843254(* Offset subtraction is invariant by translation *)
     
    33713841     ]
    33723842] qed.               
    3373  
     3843
    33743844(* Commutation result for binary operators. *)
    33753845lemma binary_operation_value_eq :
Note: See TracChangeset for help on using the changeset viewer.