proposition: Lemma spec_ww_pos_mod : forall w p, [[ww_pos_mod p w]] = [[w]] mod (2 ^ [[p]]).
proof: Proof. assert (HHHHH:= lt_0_wB w_digits). assert (F0: forall x y, x - y + y = x) by zarith. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. unfold ww_pos_mod; case w1. reflexivity. intros xh xl; rewrite spec_ww_compare. case Z.compare_spec; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; intros H1. rewrite H1; simpl ww_to_Z. autorewrite with w_rewrite rm10. rewrite Zplus_mod by zarith. rewrite Z_mod_mult by zarith. autorewrite with rm10. rewrite Zmod_mod by zarith. rewrite Zmod_small; zarith. autorewrite with w_rewrite rm10. simpl ww_to_Z. rewrite spec_pos_mod. assert (HH0: [|low p|] = [[p]]). rewrite spec_low. apply Zmod_small. case (spec_to_w_Z p); intros HHH1 HHH2; split. zarith. apply Z.lt_le_trans with (1 := H1). unfold base; apply Zpower2_le_lin; zarith. rewrite HH0. rewrite Zplus_mod by zarith. unfold base. rewrite <- (F0 (Zpos w_digits) [[p]]). rewrite Zpower_exp by zarith. rewrite Z.mul_assoc. rewrite Z_mod_mult by zarith. autorewrite with w_rewrite rm10. rewrite Zmod_mod; zarith. rewrite spec_ww_compare. case Z.compare_spec; rewrite spec_ww_zdigits; rewrite spec_zdigits; intros H2. replace (2^[[p]]) with wwB. rewrite Zmod_small; zarith. unfold base; rewrite H2. rewrite spec_ww_digits; auto. assert (HH0: [|low (ww_sub p (w_0W w_zdigits))|] = [[p]] - Zpos w_digits). rewrite spec_low. rewrite spec_ww_sub. rewrite spec_w_0W; rewrite spec_zdigits. rewrite <- Zmod_div_mod. 2-3: zarith. rewrite Zmod_small. zarith. split. zarith. apply Z.lt_le_trans with (Zpos w_digits). zarith. unfold base; apply Zpower2_le_lin; zarith. exists wB; unfold base; rewrite <- Zpower_exp by zarith. rewrite spec_ww_digits; apply f_equal with (f := Z.pow 2); rewrite Pos2Z.inj_xO; zarith. simpl ww_to_Z; autorewrite with w_rewrite. rewrite spec_pos_mod; rewrite HH0. pattern [|xh|] at 2; rewrite Z_div_mod_eq_full with (b := 2 ^ ([[p]] - Zpos w_digits)) by zarith. rewrite (fun x => (Z.mul_comm (2 ^ x))); rewrite Z.mul_add_distr_r. unfold base; rewrite <- Z.mul_assoc; rewrite <- Zpower_exp by zarith. rewrite F0 by zarith. rewrite <- Z.add_assoc; rewrite Zplus_mod by zarith. rewrite Z_mod_mult. autorewrite with rm10. rewrite Zmod_mod. symmetry; apply Zmod_small. case (spec_to_Z xh); intros U1 U2. case (spec_to_Z xl); intros U3 U4. split. apply Z.add_nonneg_nonneg. 2: zarith. apply Z.mul_nonneg_nonneg. 2: zarith. match goal with |- 0 <= ?X mod ?Y => case (Z_mod_lt X Y); zarith end. match goal with |- ?X mod ?Y * ?U + ?Z < ?T => apply Z.le_lt_trans with ((Y - 1) * U + Z ); [case (Z_mod_lt X Y); zarith | idtac] end. match goal with |- ?X * ?U + ?Y < ?Z => apply Z.le_lt_trans with (X * U + (U - 1)) end. apply Z.add_le_mono_l. case (spec_to_Z xl); unfold base; zarith. rewrite Z.mul_sub_distr_r; rewrite <- Zpower_exp by zarith. rewrite F0; zarith. rewrite Zmod_small. zarith. case (spec_to_w_Z (WW xh xl)); intros U1 U2. split. zarith. apply Z.lt_le_trans with (1:= U2). unfold base; rewrite spec_ww_digits. apply Zpower_le_monotone. zarith. split. zarith. rewrite Pos2Z.inj_xO; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub