proposition: Lemma spec_double_divn1 : forall n a b, 0 < [|b|] -> let (q,r) := double_divn1 n a b in [!n|a!] = [!n|q!] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|].
proof: Proof. intros n a b H. unfold double_divn1. case (spec_head0 H); intros H0 H1. case (spec_to_Z (w_head0 b)); intros HH1 HH2. rewrite spec_compare; case Z.compare_spec; rewrite spec_0; intros H2; auto with zarith. assert (Hv1: wB/2 <= [|b|]). generalize H0; rewrite H2; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto. assert (Hv2: [|w_0|] < [|b|]). rewrite spec_0; auto. generalize (spec_double_divn1_0 Hv1 n a Hv2). rewrite spec_0;rewrite Z.mul_0_l; rewrite Z.add_0_l; auto. contradict H2; auto with zarith. assert (HHHH : 0 < [|w_head0 b|]); auto with zarith. assert ([|w_head0 b|] < Zpos w_digits). case (Z.le_gt_cases (Zpos w_digits) [|w_head0 b|]); auto; intros HH. assert (2 ^ [|w_head0 b|] < wB). apply Z.le_lt_trans with (2 ^ [|w_head0 b|] * [|b|]);auto with zarith. replace (2 ^ [|w_head0 b|]) with (2^[|w_head0 b|] * 1);try (ring;fail). apply Z.mul_le_mono_nonneg;auto with zarith. assert (wB <= 2^[|w_head0 b|]). unfold base;apply Zpower_le_monotone;auto with zarith. lia. assert ([|w_add_mul_div (w_head0 b) b w_0|] = 2 ^ [|w_head0 b|] * [|b|]). rewrite (spec_add_mul_div b w_0); auto with zarith. rewrite spec_0;rewrite Zdiv_0_l; try lia. rewrite Z.add_0_r; rewrite Z.mul_comm. rewrite Zmod_small; auto with zarith. assert (H5 := spec_to_Z (high n a)). assert ([|w_add_mul_div (w_head0 b) w_0 (high n a)|] <[|w_add_mul_div (w_head0 b) b w_0|]). rewrite H4. rewrite spec_add_mul_div;auto with zarith. rewrite spec_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. assert (([|high n a|]/2^(Zpos w_digits - [|w_head0 b|])) < wB). assert (H6 := Z.pow_pos_nonneg 2 (Zpos w_digits - [|w_head0 b|])); auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with wB;auto with zarith. pattern wB at 1;replace wB with (wB*1);try ring. apply Z.mul_le_mono_nonneg;auto with zarith. rewrite Zmod_small;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with wB;auto with zarith. apply Z.le_trans with (2 ^ [|w_head0 b|] * [|b|] * 2). rewrite <- wB_div_2; try lia. apply Z.mul_le_mono_nonneg;auto with zarith. pattern 2 at 1;rewrite <- Z.pow_1_r. apply Zpower_le_monotone;split;auto with zarith. rewrite <- H4 in H0. assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. assert (H7:= spec_double_divn1_p H0 Hb3 n a (double_0 w_0 n) H6). destruct (double_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n (w_add_mul_div (w_head0 b) w_0 (high n a)) a (double_0 w_0 n)) as (q,r). assert (U:= spec_double_digits n). rewrite spec_double_0 in H7;trivial;rewrite Zdiv_0_l in H7. rewrite Z.add_0_r in H7. rewrite spec_add_mul_div in H7;auto with zarith. rewrite spec_0 in H7;rewrite Z.mul_0_l in H7;rewrite Z.add_0_l in H7. assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB = [!n|a!] / 2^(Zpos (w_digits << n) - [|w_head0 b|])). rewrite Zmod_small;auto with zarith. rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. replace (Zpos (w_digits << n) - Zpos w_digits + (Zpos w_digits - [|w_head0 b|])) with (Zpos (w_digits << n) - [|w_head0 b|]);trivial;ring. assert (H8 := Z.pow_pos_nonneg 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. split;auto with zarith. apply Z.le_lt_trans with ([|high n a|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. pattern ([|high n a|]) at 1;rewrite <- Z.mul_1_r. apply Z.mul_le_mono_nonneg;auto with zarith. rewrite H8 in H7;unfold double_wB,base in H7. rewrite <- shift_unshift_mod in H7;auto with zarith. rewrite H4 in H7. assert ([|w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r|] = [|r|]/2^[|w_head0 b|]). rewrite spec_add_mul_div. rewrite spec_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) with ([|w_head0 b|]). rewrite Zmod_small;auto with zarith. assert (H9 := spec_to_Z r). split;auto with zarith. apply Z.le_lt_trans with ([|r|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. pattern ([|r|]) at 1;rewrite <- Z.mul_1_r. apply Z.mul_le_mono_nonneg;auto with zarith. assert (H10 := Z.pow_pos_nonneg 2 ([|w_head0 b|]));auto with zarith. rewrite spec_sub. rewrite Zmod_small; auto with zarith. split; auto with zarith. case (spec_to_Z w_zdigits); auto with zarith. rewrite spec_sub. rewrite Zmod_small; auto with zarith. split; auto with zarith. case (spec_to_Z w_zdigits); auto with zarith. case H7; intros H71 H72. split. rewrite <- (Z_div_mult [!n|a!] (2^[|w_head0 b|]));auto with zarith. rewrite H71;rewrite H9. replace ([!n|q!] * (2 ^ [|w_head0 b|] * [|b|])) with ([!n|q!] *[|b|] * 2^[|w_head0 b|]); try (ring;fail). rewrite Z_div_plus_l;auto with zarith. assert (H10 := spec_to_Z (w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r));split; auto with zarith. rewrite H9. apply Zdiv_lt_upper_bound. auto with zarith. rewrite Z.mul_comm;auto with zarith. exact (spec_double_to_Z w_digits w_to_Z spec_to_Z n a). Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase