 Timestamp:
 Aug 29, 2012, 11:21:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2302 r2304 2066 2066 〈f',vars〉 = function_switch_removal f → 2067 2067 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 → 2069 2069 switch_cont_sim (map ?? (fst ??) vars) k k' → 2070 2070 switch_state_sim … … 2328 2328 ] qed. 2329 2329 2330 2331 lemma 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 2334 qed. 2335 2330 2336 (*  *) 2331 2337 (* Associativity proof for addition_n. The proof relies on the observation … … 2389 2395 carry_0 carry. 2390 2396 2391 let rec canonical_add (n : nat) (a,b,c : BitVector n) on a : (BitVector n × ternary) ≝2397 let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝ 2392 2398 match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with 2393 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, Zero_carry〉2399 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉 2394 2400  VCons sz' xa tla ⇒ λb',c'. 2395 2401 let xb ≝ head' … b' in … … 2397 2403 let tlb ≝ tail … b' in 2398 2404 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 2400 2406 let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in 2401 2407 〈bit ::: bits, carry〉 … … 2444 2450 cases carries_hd cases a_hd cases b_hd normalize nodelta 2445 2451 // 2446 ] qed. 2452 ] qed. 2447 2453 2448 2454 (* 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 falsein2451 let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c falsein2452 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in2455 lemma 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 2453 2459 res_ab_c = res_canonical 2454 2460 ∧ (match n return λx. BitVector x → BitVector x → Prop with … … 2457 2463 ] flags_ab flags_ab_c). 2458 2464 #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 #c2465 [ 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 2461 2467 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2462 2468 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2463 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2464 lapply (Hind … a' b' c') Hind2469 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2470 lapply (Hind … carry1 carry2 a' b' c') Hind 2465 2471 destruct >add_with_carries_Sn 2466 elim (add_with_carries … a' b' false) #Hres_ab #Hflags_ab normalize nodelta2472 elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta 2467 2473 lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a' 2468 2474 Hflags_ab Hres_ab c' b' a' … … 2472 2478 >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab) 2473 2479 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 // 2475 2481  2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 2476 2482 elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab … … 2479 2485 cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta 2480 2486 >add_with_carries_Sn 2481 elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' false) #res_ab_c #flags_ab_c2487 elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c 2482 2488 normalize nodelta 2483 2489 elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c 2484 2490 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 2489 2497 >Hres_ab_is_canonical 2490 2498 cases xa cases xb cases xc try @conj try @refl 2491 2499 ] 2492 ] qed. 2500 ] qed. 2493 2501 2494 2502 (* Symmetric. The two sides are most certainly doable in a single induction, but lazyness 2495 2503 prevails over style. *) 2496 lemma canonical_add_right : ∀n, a,b,c.2497 let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c falsein2498 let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc falsein2499 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in2504 lemma 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 2500 2508 res_a_bc = res_canonical 2501 2509 ∧ (match n return λx. BitVector x → BitVector x → Prop with … … 2504 2512 ] flags_bc flags_a_bc). 2505 2513 #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 #c2514 [ 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 2508 2516 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2509 2517 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2510 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2511 lapply (Hind … a' b' c') Hind2518 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2519 lapply (Hind … carry1 carry2 a' b' c') Hind 2512 2520 destruct >add_with_carries_Sn 2513 elim (add_with_carries … b' c' false) #Hres_bc #Hflags_bc normalize nodelta2521 elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta 2514 2522 lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a' 2515 2523 Hflags_bc Hres_bc c' b' a' … … 2519 2527 >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc) 2520 2528 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 // 2522 2530  2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 2523 2531 elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc … … 2526 2534 cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta 2527 2535 >add_with_carries_Sn 2528 elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) false) #res_a_bc #flags_a_bc2536 elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc 2529 2537 normalize nodelta 2530 2538 elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc 2531 2539 normalize nodelta 2532 2540 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 2535 2544 * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize 2536 2545 >Hres_bc_is_canonical … … 2539 2548 ] qed. 2540 2549 2550 2551 (* Note that we prove a result more general that just associativity: we can vary the carries. *) 2541 2552 lemma 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)) 2544 2555 = 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)). 2546 2557 #n cases n 2547 [ 1: # a #b #c2558 [ 1: #carry1 #carry2 #a #b #c 2548 2559 >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) 2549 2560 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) 2552 2564 normalize nodelta 2553 elim (add_with_carries (S n') b c false) #res_bc #flags_bc2554 elim (add_with_carries (S n') a b false) #res_ab #flags_ab2565 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 2555 2567 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 2558 2571 normalize nodelta 2559 cases (canonical_add ? a b c ) #canonical_bits #last_carry2572 cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry 2560 2573 normalize nodelta 2561 2574 * #HA #HB * #HC #HD destruct @refl … … 2563 2576 2564 2577 (* 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_carries2568 @refl2569 qed.2570 2578 2571 2579 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. … … 2574 2582 whd in match (addition_n n b c); 2575 2583 whd in match (addition_n n a b); 2576 lapply (associative_add_with_carries … a b c)2584 lapply (associative_add_with_carries … false false a b c) 2577 2585 elim (add_with_carries n b c false) #bc_bits #bc_flags 2578 2586 elim (add_with_carries n a b false) #ab_bits #ab_flags … … 2671 2679 ] 2672 2680 ] 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 2682 lemma map_Sn : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n. 2683 2683 map A B (S n) f (hd ::: tl) = (f hd) ::: (map A B n f tl). 2684 2684 #A #B #n #f #hd #tl normalize @refl qed. 2685 2685 2686 lemma replicate_ unfold: ∀A,sz,elt.2686 lemma replicate_Sn : ∀A,sz,elt. 2687 2687 replicate A (S sz) elt = elt ::: (replicate A sz elt). 2688 2688 // qed. 2689 2689 2690 axiom subtraction_delta : ∀x,y,delta. 2690 lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed. 2691 2692 lemma 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 2698 lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed. 2699 lemma xorb_false : ∀a. xorb a false = a. * @refl qed. 2700 lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed. 2701 lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed. 2702 lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed. 2703 lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed. 2704 lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed. 2705 lemma 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 *) 2708 lemma carry_of_TT : ∀x. carry_of true true x = true. // qed. 2709 lemma carry_of_TF : ∀x. carry_of true false x = x. // qed. 2710 lemma carry_of_FF : ∀x. carry_of false false x = false. // qed. 2711 lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed. 2712 lemma 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 *) 2715 lemma andb_lsimpl_true : ∀x. andb true x = x. // qed. 2716 lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed. 2717 lemma andb_comm : ∀x,y. andb x y = andb y x. // qed. 2718 lemma notb_true : notb true = false. // qed. 2719 lemma notb_false : notb false = true. % #H destruct qed. 2720 lemma notb_fold : ∀x. if x then false else true = (¬x). // qed. 2721 2722 (* 2723 let rec one_bv (n : nat) on n : BitVector n ≝ 2724 match 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')) 2731 qed. 2732 *) 2733 definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)). 2734 2735 lemma 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⇒trueVCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy]) 2755 normalize #Heq destruct @refl 2756 ] qed. 2757 2758 lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)). 2759 #n lapply (one_bv_Sn_aux n) 2760 whd in match (one_bv ?) in ⊢ (? → (??%%)); 2761 elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags 2762 #H lapply (H bits flags (refl ??)) #H2 >H2 @refl 2763 qed. 2764 2765 lemma 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 2768 elim 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. *) 2783 lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n). 2784 #n 2785 whd in match (increment ??) in ⊢ (∀_.??%?); 2786 whd 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 2789 qed. 2790 2791 (* Explicit formulation of addition *) 2792 2793 (* Explicit formulation of the last carry bit *) 2794 let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝ 2795 match 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 2805 lemma 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 2809 lemma 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] *) 2813 lemma 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. *) 2842 definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit. 2843 match 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 2853 lemma 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 2857 lemma 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 *) 2861 lemma 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 2865 cases 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 bitvectors to bits into a vector by folding *) 2890 let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝ 2891 match 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 (* Twoarguments version *) 2899 let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝ 2900 match 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 2907 lemma 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. *) 2911 definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init). 2912 2913 lemma 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 2916 lemma 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 *) 2919 lemma 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⇒carryVCons (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 *) 2941 lemma 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 2947 lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3) 2948 elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta 2949 elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta 2950 #H @(sym_eq … H) 2951 qed. 2952 2953 lemma 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/ 2956 qed. 2957 2958 definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false. 2959 definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v). 2960 2961 (* fold andb on a bitvector. *) 2962 let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝ 2963 match b with 2964 [ VEmpty ⇒ true 2965  VCons sz elt tl ⇒ 2966 andb elt (andb_fold ? tl) 2967 ]. 2968 2969 lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed. 2970 2971 lemma 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 2973 qed. 2974 2975 lemma 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 2987 lemma 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 2990 elim (BitVector_Sn … a) #hd * #tl #Heq >Heq 2991 whd 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 twocomplement negation *) 3000 lemma 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 twocomplement negation. *) 3016 lemma 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 3041 lemma 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 3044 lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed. 3045 3046 (* Injectivity of increment *) 3047 lemma 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) *) 3075 lemma increment_inj_inv : ∀n. ∀a,b : BitVector n. 3076 a = b → increment_direct ? a = increment_direct ? b. // qed. 3077 3078 lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed. 3079 3080 lemma 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 3090 lemma 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. 3094 qed. 3095 3096 lemma 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 3106 lemma 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 3121 lemma 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 3125 qed. 3126 3127 (* Prove (a + b) = a + b *) 3128 lemma 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. 3130 whd in match twocomp_neg_direct; normalize nodelta 3131 lapply increment_inj_inv 3132 whd 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 3138 cases 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 3165 lemma 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 *) 3181 lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?). 3182 whd in match twocomp_neg_direct; 3183 whd in match increment_direct; 3184 normalize nodelta 3185 #n #a <associative_addition_n_direct 3186 elim (addition_n_direct_neg … a) #H #_ >H 3187 H a 3188 cases n try // 3189 #n' 3190 cut ((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 3200 qed. 3201 3202 (* Lift back the previous result to standard operations. *) 3203 lemma 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 3205 whd in match increment_direct; normalize nodelta 3206 whd in match two_complement_negation; normalize nodelta 3207 >increment_to_addition_n <addition_n_direct_ok 3208 whd in match addition_n; normalize nodelta 3209 elim (add_with_carries ????) #a #b @refl 3210 qed. 3211 3212 lemma 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 3215 lapply (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 3218 whd in match addition_n; normalize nodelta 3219 elim (add_with_carries n a b false) #bits #flags normalize nodelta 3220 elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags' 3221 normalize nodelta #H @H 3222 qed. 3223 3224 lemma 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 3227 whd in match (addition_n ???); 3228 elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H 3229 qed. 3230 3231 lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a. 3232 #n #a 3233 lapply (neutral_addition_n_direct n a) 3234 <addition_n_direct_ok 3235 whd in match (addition_n ???); 3236 elim (add_with_carries n a (zero n) false) #bits #flags #H @H 3237 qed. 3238 3239 lemma subtraction_delta : ∀x,y,delta. 2691 3240 subtraction offset_size 2692 3241 (addition_n offset_size x delta) 2693 3242 (addition_n offset_size y delta) = 2694 3243 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 3252 qed. 2783 3253 2784 3254 (* Offset subtraction is invariant by translation *) … … 3371 3841 ] 3372 3842 ] qed. 3373 3843 3374 3844 (* Commutation result for binary operators. *) 3375 3845 lemma binary_operation_value_eq :
Note: See TracChangeset
for help on using the changeset viewer.