proposition: Lemma spec_ww_add_mul_div_aux : forall xh xl yh yl p, let zdigits := w_0W w_zdigits in [[p]] <= Zpos (xO w_digits) -> [[match ww_compare p zdigits with | Eq => w_WW xl yh | Lt => w_WW (w_add_mul_div (low p) xh xl) (w_add_mul_div (low p) xl yh) | Gt => let n := low (ww_sub p zdigits) in w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl) end]] = ([[WW xh xl]] * (2^[[p]]) + [[WW yh yl]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
proof: Proof. intros xh xl yh yl p zdigits;assert (HwwB := wwB_pos w_digits). case (spec_to_w_Z p); intros Hv1 Hv2. replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits). 2 : rewrite Pos2Z.inj_xO;ring. replace (Zpos w_digits + Zpos w_digits - [[p]]) with (Zpos w_digits + (Zpos w_digits - [[p]])). 2:ring. intros Hp; assert (Hxh := spec_to_Z xh);assert (Hxl:=spec_to_Z xl); assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)); simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl); assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy. rewrite spec_ww_compare; case Z.compare_spec; intros H1. rewrite H1; unfold zdigits; rewrite spec_w_0W. rewrite spec_zdigits; rewrite Z.sub_diag; rewrite Z.add_0_r. simpl ww_to_Z; w_rewrite;zarith. fold wB. rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc;rewrite <- Z.add_assoc. rewrite <- Z.pow_2_r. rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring. simpl ww_to_Z; w_rewrite;zarith. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. apply Zmod_small. case (spec_to_w_Z p); intros HH1 HH2; split; auto. generalize H1; unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; intros tmp. apply Z.lt_le_trans with (1 := tmp). unfold base. apply Zpower2_le_lin; auto with zarith. 2: generalize H1; unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto with zarith. generalize H1; unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto; clear H1; intros H1. assert (HH: [|low p|] <= Zpos w_digits). rewrite HH0; auto with zarith. repeat rewrite spec_w_add_mul_div with (1 := HH). rewrite HH0. rewrite Z.mul_add_distr_r. pattern ([|xl|] * 2 ^ [[p]]) at 2; rewrite shift_unshift_mod with (n:= Zpos w_digits);fold wB;zarith. replace ([|xh|] * wB * 2^[[p]]) with ([|xh|] * 2^[[p]] * wB). 2:ring. rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite <- Z.add_assoc. unfold base at 5;rewrite <- Zmod_shift_r;zarith. unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits)); fold wB;fold wwB;zarith. rewrite wwB_wBwB;rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;zarith. unfold ww_digits;rewrite Pos2Z.inj_xO;zarith. apply Z_mod_lt;zarith. split;zarith. apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith. assert (Hv: [[p]] > Zpos w_digits). generalize H1; clear H1. unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto with zarith. clear H1. assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits). rewrite spec_low. rewrite spec_ww_sub. unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits. rewrite <- Zmod_div_mod; auto with zarith. rewrite Zmod_small; auto with zarith. split; auto with zarith. apply Z.le_lt_trans with (Zpos w_digits); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. exists wB; unfold base. unfold ww_digits; rewrite (Pos2Z.inj_xO w_digits). rewrite <- Zpower_exp; auto with zarith. apply f_equal with (f := fun x => 2 ^ x); auto with zarith. assert (HH: [|low (ww_sub p zdigits)|] <= Zpos w_digits). rewrite HH0; auto with zarith. replace (Zpos w_digits + (Zpos w_digits - [[p]])) with (Zpos w_digits - ([[p]] - Zpos w_digits)); zarith. lazy zeta; simpl ww_to_Z; w_rewrite;zarith. repeat rewrite spec_w_add_mul_div;zarith. rewrite HH0. pattern wB at 5;replace wB with (2^(([[p]] - Zpos w_digits) + (Zpos w_digits - ([[p]] - Zpos w_digits)))). rewrite Zpower_exp;zarith. rewrite Z.mul_assoc. rewrite Z_div_plus_l;zarith. rewrite shift_unshift_mod with (a:= [|yh|]) (p:= [[p]] - Zpos w_digits) (n := Zpos w_digits);zarith. fold wB. set (u := [[p]] - Zpos w_digits). replace [[p]] with (u + Zpos w_digits);zarith. rewrite Zpower_exp;zarith. rewrite Z.mul_assoc. fold wB. repeat rewrite Z.add_assoc. rewrite <- Z.mul_add_distr_r. repeat rewrite <- Z.add_assoc. unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits)); fold wB;fold wwB;zarith. unfold base;rewrite Zmod_shift_r with (a:= Zpos w_digits) (b:= Zpos w_digits);fold wB;fold wwB;zarith. rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;zarith. rewrite Z.mul_add_distr_r. replace ([|xh|] * wB * 2 ^ u) with ([|xh|]*2^u*wB). 2:ring. repeat rewrite <- Z.add_assoc. rewrite (Z.add_comm ([|xh|] * 2 ^ u * wB)). rewrite Z_mod_plus;zarith. rewrite Z_mod_mult;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. try (unfold u; lia). split;zarith. unfold u; apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. fold u. ring_simplify (u + (Zpos w_digits - u)); fold wB;zarith. unfold ww_digits;rewrite Pos2Z.inj_xO;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. try (unfold u; lia). unfold u; split;zarith. apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. fold u. ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith. try (unfold u;zarith). try (unfold u;zarith). set (u := [[p]] - Zpos w_digits). ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase