proposition: Theorem mmul_aux5:forall xh xl, [[WW xh xl]] < [|b|] * 2 ^ Zpos p -> let xl1 := w_pos_mod zp xl in let r := match add_mul_div zp1 W0 (WW xh xl) with W0 => match w_compare xl1 b with | Lt => xl1 | Eq => w0 | Gt => w1 end | WW _ xl2 => _add_mod xl1 xl2 end in [|r|] = [[WW xh xl]] mod [|b|].
proof: Proof. intros xh xl Hx xl1 r; unfold r; clear r. generalize (mmul_aux4 _ Hx). simpl ww_to_Z; rewrite p_b. rewrite mmul_aux2. assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith. rewrite zp1_b; rewrite <- p_p1; auto with zarith. assert (0 <= Zpos p); auto with zarith. generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub ZnZ.spec_zdigits spec_low W0 (WW xh xl) zp1 Hp). unfold add_mul_div; case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto. rewrite Zmult_0_l; rewrite Zplus_0_l. rewrite zp1_b. generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. intros H1 H2. rewrite <- H2. rewrite Zplus_0_l. generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; auto with zarith. unfold xl1; unfold w_pos_mod. rewrite <- p_b; rewrite <- zp_b. rewrite <- ZnZ.spec_pos_mod; auto with zarith. unfold w_compare; rewrite ZnZ.spec_compare; case Z.compare_spec; intros Hc; match goal with H: context[b] |- _ => generalize H; clear H end; try rewrite _w0_is_0. intros H3; rewrite H3. rewrite Z_mod_same; auto with zarith. intros H3; rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z (ZnZ.pos_mod zp xl)); unfold w_to_Z; auto with zarith. rewrite p_b; rewrite ZnZ.spec_pos_mod; auto with zarith. intros H3; assert (HH: [|xl|] mod 2 ^ Zpos p = 2 ^ Zpos p). apply Zle_antisym; auto with zarith. case (Z_mod_lt ([|xl|]) (2 ^ Zpos p)); auto with zarith. rewrite zp_b in H3; auto with zarith. rewrite zp_b; rewrite HH. rewrite <- Zmod_minus_one; auto with zarith. rewrite _w1_is_1; rewrite Zmod_small; auto with zarith. rewrite Zmult_0_l; rewrite Zplus_0_l. rewrite zp1_b. generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. intros w2 w3 H1 H2; rewrite <- H2. generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; auto with zarith. rewrite <- p_b; rewrite <- zp_b. rewrite <- ZnZ.spec_pos_mod; auto with zarith. unfold xl1; unfold w_pos_mod. rewrite Zplus_comm. apply _add_mod_correct; auto with zarith. assert (tmp: forall x, 2 * x = x + x); auto with zarith; rewrite tmp; apply Zplus_le_lt_compat; clear tmp; auto with zarith. rewrite ZnZ.spec_pos_mod; auto with zarith. rewrite p_b; case (Z_mod_lt [|xl|] (2 ^ Zpos p)); auto with zarith. rewrite zp_b; auto with zarith. rewrite H2; apply Zdiv_lt_upper_bound; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux