proposition: Lemma Bdiv_correct_aux : forall m sx mx ex sy my ey, let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in let z := let '(mz, ez, lz) := SFdiv_core_binary prec emax (Zpos mx) ex (Zpos my) ey in binary_round_aux m (xorb sx sy) mz ez lz in valid_binary z = true /\ if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x / y))) (bpow radix2 emax) then SF2R radix2 z = round radix2 fexp (round_mode m) (x / y) /\ is_finite_SF z = true /\ sign_SF z = xorb sx sy else z = binary_overflow m (xorb sx sy).
proof: Proof. intros m sx mx ex sy my ey. unfold SFdiv_core_binary. rewrite 2!Zdigits2_Zdigits. set (e' := Z.min _ _). match goal with |- context [Z.div_eucl ?m _] => set (mx' := m) end. generalize (Fdiv_core_correct radix2 (Zpos mx) ex (Zpos my) ey e' eq_refl eq_refl). unfold Fdiv_core. rewrite Zle_bool_true by apply Z.le_min_r. assert (mx' = Zpos mx * Zpower radix2 (ex - ey - e'))%Z as <-. { unfold mx'. destruct (ex - ey - e')%Z as [|p|p]. now rewrite Zmult_1_r. now rewrite Z.shiftl_mul_pow2. easy. } clearbody mx'. destruct Z.div_eucl as [q r]. intros Bz. assert (xorb sx sy = Rlt_bool (F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) * / F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey)) 0) as ->. { apply eq_sym. case sy ; simpl. change (Zneg my) with (Z.opp (Zpos my)). rewrite F2R_Zopp. rewrite <- Ropp_inv_permute. rewrite Ropp_mult_distr_r_reverse. case sx ; simpl. apply Rlt_bool_false. rewrite <- Ropp_mult_distr_l_reverse. apply Rmult_le_pos. rewrite <- F2R_opp. now apply F2R_ge_0. apply Rlt_le. apply Rinv_0_lt_compat. now apply F2R_gt_0. apply Rlt_bool_true. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply Rinv_0_lt_compat. now apply F2R_gt_0. apply Rgt_not_eq. now apply F2R_gt_0. case sx. apply Rlt_bool_true. rewrite F2R_Zopp. rewrite Ropp_mult_distr_l_reverse. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply Rinv_0_lt_compat. now apply F2R_gt_0. apply Rlt_bool_false. apply Rmult_le_pos. now apply F2R_ge_0. apply Rlt_le. apply Rinv_0_lt_compat. now apply F2R_gt_0. } unfold Rdiv. apply binary_round_aux_correct'. - apply Rmult_integral_contrapositive_currified. now apply F2R_neq_0 ; case sx. apply Rinv_neq_0_compat. now apply F2R_neq_0 ; case sy. - rewrite Rabs_mult, Rabs_Rinv. + rewrite <- 2!F2R_Zabs, 2!abs_cond_Zopp; simpl. replace (SpecFloat.new_location _ _) with (Bracket.new_location (Z.pos my) r loc_Exact); [exact Bz|]. case my as [p|p|]; [reflexivity| |reflexivity]. unfold Bracket.new_location, SpecFloat.new_location; simpl. unfold Bracket.new_location_even, SpecFloat.new_location_even; simpl. now case Zeq_bool; [|case r as [|rp|rp]; case Z.compare]. + now apply F2R_neq_0 ; case sy. - rewrite <- cexp_abs, Rabs_mult, Rabs_Rinv. rewrite 2!F2R_cond_Zopp, 2!abs_cond_Ropp, <- Rabs_Rinv. rewrite <- Rabs_mult, cexp_abs. apply Z.le_trans with (1 := Z.le_min_l _ _). apply FLT_exp_monotone. now apply mag_div_F2R. now apply F2R_neq_0. now apply F2R_neq_0 ; case sy. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative