proposition: Theorem spec_w_div2s : forall a1 a2 b, wB/2 <= [|b|] -> [+|a1|] <= 2 * [|b|] -> let (q,r) := w_div2s a1 a2 b in [+|a1|] * wB + [|a2|] = [+|q|] * (2 * [|b|]) + [+|r|] /\ 0 <= [+|r|] < 2 * [|b|].
proof: Proof. intros a1 a2 b H. assert (HH: 0 < [|b|]). { assert (U := wB_pos w_digits). apply Z.lt_le_trans with (2 := H). apply Z.lt_le_trans with 1. zarith. apply Zdiv_le_lower_bound; zarith. } unfold w_div2s; case a1; intros w0 H0. match goal with |- context[w_div21c ?y ?z ?t] => generalize (@spec_w_div21c y z t H); case (w_div21c y z t); autorewrite with w_rewrite; auto end. intros c w1; case c. simpl interp_carry; intros w2 (Hw1, Hw2). match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); case (w_is_even y) end. repeat rewrite C0_id. rewrite add_mult_div_2. intros H1; split. 2: zarith. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; ring. repeat rewrite C0_id. rewrite add_mult_div_2. rewrite spec_w_add_c by zarith. intros H1; split. 2: zarith. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; ring. intros w2; rewrite C1_plus_wB. intros (Hw1, Hw2). match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); case (w_is_even y) end. repeat rewrite C0_id. intros H1; split. 2: zarith. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1. repeat rewrite C0_id. rewrite add_mult_div_2_plus_1; unfold base. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp by zarith; rewrite Z.pow_1_r end. rewrite Pos2Z.inj_sub_max. rewrite Z.max_r by zarith. ring. repeat rewrite C0_id. rewrite spec_w_add_c. intros H1; split. 2: zarith. rewrite add_mult_div_2_plus_1. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1. unfold base. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp by zarith; rewrite Z.pow_1_r end. rewrite Pos2Z.inj_sub_max. rewrite Z.max_r by zarith. ring. repeat rewrite C1_plus_wB in H0. rewrite C1_plus_wB. match goal with |- context[w_div21c ?y ?z ?t] => generalize (@spec_w_div21c y z t H); case (w_div21c y z t); autorewrite with w_rewrite; auto end. intros c w1; case c. intros w2 (Hw1, Hw2); rewrite C0_id in Hw1. rewrite <- Zplus_mod_one in Hw1. rewrite Zmod_small in Hw1. match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); case (w_is_even y) end. repeat rewrite C0_id. intros H1; split. 2: zarith. rewrite add_mult_div_2_plus_1. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)) by zarith. rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; unfold base. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp by zarith; rewrite Z.pow_1_r end. rewrite Pos2Z.inj_sub_max. rewrite Z.max_r by zarith. ring. repeat rewrite C0_id. rewrite add_mult_div_2_plus_1. rewrite spec_w_add_c. intros H1; split. 2: zarith. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)) by zarith. rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; unfold base. match goal with |- context[_ ^ ?X] => assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite <- (tmp X); clear tmp; rewrite Zpower_exp by zarith; rewrite Z.pow_1_r end. rewrite Pos2Z.inj_sub_max. rewrite Z.max_r by zarith. ring. split. destruct (spec_to_Z b). destruct (spec_to_Z w0);zarith. destruct (spec_to_Z b);zarith. destruct (spec_to_Z b);zarith. intros w2; rewrite C1_plus_wB. rewrite <- Zplus_mod_one. rewrite Zmod_small. intros (Hw1, Hw2). match goal with |- context[w_is_even ?y] => generalize (spec_w_is_even y); case (w_is_even y) end. repeat (rewrite C0_id || rewrite C1_plus_wB). intros H1; split. 2: zarith. rewrite add_mult_div_2. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)) by zarith. rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; ring. repeat (rewrite C0_id || rewrite C1_plus_wB). rewrite spec_w_add_c by zarith. intros H1; split. 2: zarith. rewrite add_mult_div_2. replace (wB + [|w0|]) with ([|b|] + ([|w0|] - [|b|] + wB)) by zarith. rewrite Z.mul_add_distr_r; rewrite <- Z.add_assoc. rewrite Hw1. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] 2) by zarith. rewrite H1; ring. split. destruct (spec_to_Z b). destruct (spec_to_Z w0);zarith. destruct (spec_to_Z b);zarith. destruct (spec_to_Z b);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase