proposition: Theorem Fdiv_correct : forall beta mode prec (x y : float beta), FtoX (Fdiv mode prec x y) = Xround beta mode prec (Xdiv (FtoX x) (FtoX y)).
proof: Proof. Proof with auto with typeclass_instances. intros beta mode prec [ | | sx mx ex] [ | | sy my ey] ; simpl ; unfold Xdiv' ; try rewrite is_zero_0 ; try apply refl_equal ; rewrite is_zero_correct_float. unfold Rdiv. rewrite Rmult_0_l. apply sym_eq. apply (f_equal Xreal). apply round_0... unfold Xround, Fdiv, Fdiv_aux, Fdiv_aux2. set (e := Z.min ((Zdigits beta (Zpos mx) + ex) - (Zdigits beta (Zpos my) + ey) - Zpos prec) (ex - ey)). generalize (Div.Fdiv_core_correct beta (Zpos mx) ex (Zpos my) ey e eq_refl eq_refl). unfold Div.Fdiv_core. rewrite Zle_bool_true by apply Z.le_min_r. match goal with |- context [let (m,e') := ?v in let '(q,r) := Zfast_div_eucl _ _ in _] => set (me := v) end. assert (me = (Zpos mx * Zpower beta (ex - ey - e), e))%Z as ->. { unfold me, e ; clear. destruct (_ + Zpos prec - _)%Z as [|p|p] eqn:He. - rewrite Z.min_r by lia. now rewrite Z.sub_diag, Zmult_1_r. - rewrite Z.min_l by lia. change (Zneg p) with (Z.opp (Zpos p)). fold (Zpower beta (Zpos p)). rewrite <- He. apply (f_equal2 (fun v1 v2 => (_ * Zpower beta v1, v2)%Z)) ; ring. - rewrite Z.min_r by lia. now rewrite Z.sub_diag, Zmult_1_r. } rewrite Zfast_div_eucl_correct. destruct Z.div_eucl as [m r]. set (l := new_location _ _ _). intros H1. assert (Zpos prec <= Zdigits beta m)%Z as H2. { generalize (Div.mag_div_F2R beta (Zpos mx) ex (Zpos my) ey eq_refl eq_refl). cbv zeta. intros H2. refine (_ (cexp_inbetween_float _ (FLX_exp (Zpos prec)) _ _ _ _ _ H1 (or_introl _))). unfold cexp, FLX_exp, e. intros H3. lia. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply Rinv_0_lt_compat. now apply F2R_gt_0. unfold cexp, FLX_exp, e. lia. } destruct m as [|p|p]. - now elim H2. - replace (FtoR beta sx mx ex / FtoR beta sy my ey)%R with (if xorb sx sy then - (FtoR beta false mx ex / FtoR beta false my ey) else (FtoR beta false mx ex / FtoR beta false my ey))%R. apply (Fround_at_prec_correct beta mode prec _ p e). apply Rmult_lt_0_compat. apply FtoR_Rpos. apply Rinv_0_lt_compat. apply FtoR_Rpos. rewrite convert_location_bij. now rewrite 2!FtoR_split. rewrite <- digits_conversion. intros H3. elim (Z.lt_irrefl _ (Z.le_lt_trans _ _ _ H2 H3)). rewrite 4!FtoR_split. assert (F2R (Defs.Float beta (Zpos my) ey) <> 0%R). apply Rgt_not_eq. now apply F2R_gt_0. unfold cond_Zopp. now case sx ; case sy ; repeat rewrite F2R_Zopp ; simpl ; field. destruct (Bracket.inbetween_float_bounds _ _ _ _ _ H1) as (_, H5). elim (Rlt_not_le _ _ H5). apply Rle_trans with 0%R. apply F2R_le_0. unfold Fnum. now apply (Zlt_le_succ (Zneg p)). - apply Rlt_le. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply Rinv_0_lt_compat. now apply F2R_gt_0. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic