proposition: Lemma spec_ww_add_mul_div : forall x y p, [[p]] <= Zpos (xO w_digits) -> [[ ww_add_mul_div p x y ]] = ([[x]] * (2^[[p]]) + [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
proof: Proof. intros x y p H. destruct x as [ |xh xl]; [assert (H1 := @spec_ww_add_mul_div_aux w_0 w_0) |assert (H1 := @spec_ww_add_mul_div_aux xh xl)]; (destruct y as [ |yh yl]; [generalize (H1 w_0 w_0 p H) | generalize (H1 yh yl p H)]; clear H1;w_rewrite);simpl ww_add_mul_div. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. intros Heq;rewrite <- Heq;clear Heq; auto. rewrite spec_ww_compare. case Z.compare_spec; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. apply Zmod_small. case (spec_to_w_Z p); intros HH1 HH2; split; auto. apply Z.lt_le_trans with (1 := H1). unfold base; apply Zpower2_le_lin; auto with zarith. rewrite HH0; auto with zarith. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. intros Heq;rewrite <- Heq;clear Heq. generalize (spec_ww_compare p (w_0W w_zdigits)); case ww_compare; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. rewrite Pos2Z.inj_xO in H;zarith. assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits). symmetry in H1; change ([[p]] > [[w_0W w_zdigits]]) in H1. revert H1. rewrite spec_low. rewrite spec_ww_sub; w_rewrite; intros H1. 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. unfold base; auto with zarith. unfold base; 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. case (spec_to_Z xh); auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase