proposition: Lemma spec_ww_div_gt_aux : forall ah al bh bl, [[WW ah al]] > [[WW bh bl]] -> 0 < [|bh|] -> let (q,r) := ww_div_gt_aux ah al bh bl in [[WW ah al]] = [[q]] * [[WW bh bl]] + [[r]] /\ 0 <= [[r]] < [[WW bh bl]].
proof: Proof. intros ah al bh bl Hgt Hpos;unfold ww_div_gt_aux. change (let (q, r) := let p := w_head0 bh in match w_compare p w_0 with | Gt => let b1 := w_add_mul_div p bh bl in let b2 := w_add_mul_div p bl w_0 in let a1 := w_add_mul_div p w_0 ah in let a2 := w_add_mul_div p ah al in let a3 := w_add_mul_div p al w_0 in let (q,r) := w_div32 a1 a2 a3 b1 b2 in (WW w_0 q, ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r) | _ => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)) end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]). assert (Hh := spec_head0 Hpos). lazy zeta. rewrite spec_compare; case Z.compare_spec; rewrite spec_w_0; intros HH. generalize Hh; rewrite HH; simpl Z.pow; rewrite Z.mul_1_l; intros (HH1, HH2); clear HH. assert (wwB <= 2*[[WW bh bl]]). apply Z.le_trans with (2*[|bh|]*wB). rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_le_mono_nonneg_r. zarith. rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. simpl ww_to_Z;rewrite Z.mul_add_distr_l;rewrite Z.mul_assoc. Spec_w_to_Z bl;zarith. Spec_ww_to_Z (WW ah al). rewrite spec_ww_sub;eauto. simpl;rewrite spec_ww_1;rewrite Z.mul_1_l;simpl. simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_small;split;zarith. case (spec_to_Z (w_head0 bh)); zarith. assert ([|w_head0 bh|] < Zpos w_digits). destruct (Z_lt_ge_dec [|w_head0 bh|] (Zpos w_digits));trivial. exfalso. enough (2 ^ [|w_head0 bh|] * [|bh|] >= wB) by zarith. apply Z.le_ge; replace wB with (wB * 1) by ring. Spec_w_to_Z bh;apply Z.mul_le_mono_nonneg. 1, 3-4: zarith. unfold base;apply Zpower_le_monotone;zarith. assert (HHHH : 0 < [|w_head0 bh|] < Zpos w_digits) by zarith. assert (Hb:= Z.lt_le_incl _ _ H). generalize (spec_add_mul_div w_0 ah Hb) (spec_add_mul_div ah al Hb) (spec_add_mul_div al w_0 Hb) (spec_add_mul_div bh bl Hb) (spec_add_mul_div bl w_0 Hb); rewrite spec_w_0; repeat rewrite Z.mul_0_l;repeat rewrite Z.add_0_l; rewrite Zdiv_0_l;repeat rewrite Z.add_0_r. Spec_w_to_Z ah;Spec_w_to_Z bh. unfold base;repeat rewrite Zmod_shift_r by zarith. assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH); assert (H5:=to_Z_div_minus_p bl HHHH). rewrite Z.mul_comm in Hh. assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith. unfold base in H0;rewrite Zmod_small by zarith. fold wB; rewrite (Zmod_small ([|bh|] * 2 ^ [|w_head0 bh|])) by zarith. intros U1 U2 U3 V1 V2. generalize (@spec_w_div32 (w_add_mul_div (w_head0 bh) w_0 ah) (w_add_mul_div (w_head0 bh) ah al) (w_add_mul_div (w_head0 bh) al w_0) (w_add_mul_div (w_head0 bh) bh bl) (w_add_mul_div (w_head0 bh) bl w_0)). destruct (w_div32 (w_add_mul_div (w_head0 bh) w_0 ah) (w_add_mul_div (w_head0 bh) ah al) (w_add_mul_div (w_head0 bh) al w_0) (w_add_mul_div (w_head0 bh) bh bl) (w_add_mul_div (w_head0 bh) bl w_0)) as (q,r). rewrite V1;rewrite V2. rewrite Z.mul_add_distr_r. rewrite <- (Z.add_assoc ([|bh|] * 2 ^ [|w_head0 bh|] * wB)). unfold base;rewrite <- shift_unshift_mod by zarith. fold wB. replace ([|bh|] * 2 ^ [|w_head0 bh|] * wB + [|bl|] * 2 ^ [|w_head0 bh|]) with ([[WW bh bl]] * 2^[|w_head0 bh|]). 2:simpl;ring. fold wwB. rewrite wwB_wBwB. rewrite Z.pow_2_r. rewrite U1;rewrite U2;rewrite U3. rewrite Z.mul_assoc. rewrite Z.mul_add_distr_r. rewrite (Z.add_assoc ([|ah|] / 2^(Zpos(w_digits) - [|w_head0 bh|])*wB * wB)). rewrite <- Z.mul_add_distr_r. rewrite <- Z.add_assoc. unfold base;repeat rewrite <- shift_unshift_mod by zarith. fold wB. replace ([|ah|] * 2 ^ [|w_head0 bh|] * wB + [|al|] * 2 ^ [|w_head0 bh|]) with ([[WW ah al]] * 2^[|w_head0 bh|]). 2:simpl;ring. intros Hd;destruct Hd. zarith. simpl. apply beta_lex_inv. 2-3: zarith. rewrite U1;rewrite V1. enough ([|ah|] / 2 ^ (Zpos (w_digits) - [|w_head0 bh|]) < wB/2) by zarith. apply Zdiv_lt_upper_bound. zarith. unfold base. replace (2^Zpos (w_digits)) with (2^(Zpos (w_digits) - 1)*2). rewrite Z_div_mult by zarith. rewrite <- Zpower_exp by zarith. apply Z.lt_le_trans with wB. zarith. unfold base;apply Zpower_le_monotone;zarith. pattern 2 at 2;replace 2 with (2^1);trivial. rewrite <- Zpower_exp by zarith. ring_simplify (Zpos (w_digits) - 1 + 1);trivial. change [[WW w_0 q]] with ([|w_0|]*wB+[|q|]);rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. replace [[ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry _ww_zdigits (w_0W (w_head0 bh))) W0 r]] with ([[r]]/2^[|w_head0 bh|]). assert (0 < 2^[|w_head0 bh|]). apply Z.pow_pos_nonneg;zarith. split. rewrite <- (Z_div_mult [[WW ah al]] (2^[|w_head0 bh|])) by zarith. rewrite H1;rewrite Z.mul_assoc;apply Z_div_plus_l;trivial. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith. rewrite spec_ww_add_mul_div. rewrite spec_ww_sub by zarith. rewrite spec_ww_digits_. change (Zpos (xO (w_digits))) with (2*Zpos (w_digits)). simpl ww_to_Z;rewrite Z.mul_0_l;rewrite Z.add_0_l. rewrite spec_w_0W. rewrite (fun x y => Zmod_small (x-y)). ring_simplify (2 * Zpos w_digits - (2 * Zpos w_digits - [|w_head0 bh|])). rewrite Zmod_small. zarith. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound]. 1-3: zarith. Spec_ww_to_Z r. apply Z.lt_le_trans with wwB. zarith. rewrite <- (Z.mul_1_r wwB);apply Z.mul_le_mono_nonneg;zarith. split. zarith. apply Z.le_lt_trans with (2 * Zpos w_digits). zarith. unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits). apply Zpower2_lt_lin; zarith. rewrite spec_ww_sub by zarith. rewrite spec_ww_digits_; rewrite spec_w_0W. rewrite Zmod_small. zarith. rewrite Pos2Z.inj_xO; split. zarith. apply Z.le_lt_trans with (2 * Zpos w_digits). zarith. unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits). apply Zpower2_lt_lin; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub