proposition: Lemma add_carry_bits : forall a b (c0:bool), exists c, a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.
proof: Proof. intros a b c0. set (n:=max a b). assert (Ha : a<2^n). { apply lt_le_trans with (2^a). - apply pow_gt_lin_r, lt_1_2. - apply pow_le_mono_r. { order'. } unfold n. destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'. } assert (Hb : b<2^n). { apply lt_le_trans with (2^b). - apply pow_gt_lin_r, lt_1_2. - apply pow_le_mono_r. { order'. } unfold n. destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'. } clearbody n. revert a b c0 Ha Hb. induct n. - intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r. intros Ha Hb. exists c0. setoid_replace a with 0 by (generalize (le_0_l a); order'). setoid_replace b with 0 by (generalize (le_0_l b); order'). rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r. rewrite b2n_div2, b2n_bit0; now repeat split. - intros n 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. + apply div_lt_upper_bound; trivial. { order'. } now rewrite <- pow_succ_r'. + apply div_lt_upper_bound; trivial. { order'. } now rewrite <- pow_succ_r'. + exists (c0 + 2*c). repeat split. * { bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. - now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0. - rewrite <- !div2_bits, <- 2 lxor_spec. f_equiv. rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2. } * { rewrite add_b2n_double_div2. bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. - now rewrite add_b2n_double_bit0. - rewrite <- !div2_bits, IH2. autorewrite with bitwise. now rewrite add_b2n_double_div2. } * apply add_b2n_double_bit0. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog