proposition: Theorem div_correct : forall x y : float beta, F2R y <> 0%R -> round beta fexp rnd (F2R x / F2R y) = F2R (div x y).
proof: Proof. intros x y Hy. unfold div. case Zeq_bool_spec ; intros Hm. destruct x as [mx ex]. simpl in Hm. rewrite Hm, 2!F2R_0. unfold Rdiv. rewrite Rmult_0_l. now apply round_0. assert (0 < F2R (Fabs x))%R as Hx. destruct x as [mx ex]. now apply F2R_gt_0, Z.abs_pos. assert (0 < F2R (Fabs y))%R as Hy'. destruct y as [my ey]. apply F2R_gt_0, Z.abs_pos. contradict Hy. rewrite Hy. apply F2R_0. generalize (Fdiv_correct fexp _ _ Hx Hy'). destruct Fdiv as [[m e] l]. intros [Hs1 Hs2]. rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l). - destruct truncate as [[m' e'] l']. apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))). rewrite Rsgn_div. apply f_equal2 ; apply Rsgn_F2R. contradict Hm. apply eq_0_F2R with (1 := Hm). exact Hy. - unfold Rdiv. rewrite Rabs_mult, Rabs_Rinv by exact Hy. now rewrite <- 2!F2R_abs. - left. rewrite <- cexp_abs. unfold Rdiv. rewrite Rabs_mult, Rabs_Rinv by exact Hy. now rewrite <- 2!F2R_abs. Qed.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)