proposition: Lemma add_carry_bits_aux : forall n, 0<=n -> forall a b (c0:bool), -(2^n) <= a < 2^n -> -(2^n) <= b < 2^n -> exists c, a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.
proof: Proof. intros n Hn. apply le_ind with (4:=Hn). - solve_proper. - intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r, <- !one_succ. intros (Ha1,Ha2) (Hb1,Hb2). le_elim Ha1; rewrite <- ?le_succ_l, ?succ_m1 in Ha1; le_elim Hb1; rewrite <- ?le_succ_l, ?succ_m1 in Hb1. + exists c0. rewrite (le_antisymm _ _ Ha2 Ha1), (le_antisymm _ _ Hb2 Hb1). rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r. rewrite b2z_div2, b2z_bit0; now repeat split. + exists (-c0). rewrite <- Hb1, (le_antisymm _ _ Ha2 Ha1). repeat split. * rewrite add_0_l, lxor_0_l, lxor_m1_l. unfold lnot. now rewrite opp_involutive, add_comm, add_opp_r, sub_1_r. * rewrite land_0_l, !lor_0_l, land_m1_r. symmetry. apply div_unique with c0. { left; destruct c0; simpl; split; order'. } now rewrite two_succ, mul_succ_l, mul_1_l, add_opp_r, sub_add. * rewrite bit0_odd, odd_opp; destruct c0; simpl; apply odd_1 || apply odd_0. + exists (-c0). rewrite <- Ha1, (le_antisymm _ _ Hb2 Hb1). repeat split. * rewrite add_0_r, lxor_0_r, lxor_m1_l. unfold lnot. now rewrite opp_involutive, add_comm, add_opp_r, sub_1_r. * rewrite land_0_r, lor_0_r, lor_0_l, land_m1_r. symmetry. apply div_unique with c0. { left; destruct c0; simpl; split; order'. } now rewrite two_succ, mul_succ_l, mul_1_l, add_opp_r, sub_add. * rewrite bit0_odd, odd_opp; destruct c0; simpl; apply odd_1 || apply odd_0. + exists (c0 + 2*(-1)). rewrite <- Ha1, <- Hb1. repeat split. * rewrite lxor_m1_l, lnot_m1, lxor_0_l. now rewrite two_succ, mul_succ_l, mul_1_l, add_comm, add_assoc. * rewrite land_m1_l, lor_m1_l. apply add_b2z_double_div2. * apply add_b2z_double_bit0. - clear n Hn. intros n Hn IH a b c0 Ha Hb. set (c1:=nextcarry a.[0] b.[0] c0). destruct (IH (a/2) (b/2) c1) as (c & IH1 & IH2 & Hc); clear IH. + split. * apply div_le_lower_bound. { order'. } now rewrite mul_opp_r, <- pow_succ_r. * apply div_lt_upper_bound. { order'. } now rewrite <- pow_succ_r. + split. * apply div_le_lower_bound. { order'. } now rewrite mul_opp_r, <- pow_succ_r. * apply div_lt_upper_bound. { order'. } now rewrite <- pow_succ_r. + exists (c0 + 2*c). repeat split. * { bitwise as m Hm. le_elim Hm. - rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial. f_equiv. rewrite add_b2z_double_div2, <- IH1. apply add_carry_div2. - rewrite <- Hm. now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0. } * { rewrite add_b2z_double_div2. bitwise as m Hm. le_elim Hm. - rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial. autorewrite with bitwise. now rewrite add_b2z_double_div2. - rewrite <- Hm. now rewrite add_b2z_double_bit0. } * apply add_b2z_double_bit0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog