proposition: Lemma sqrt_DN_correct : forall p x, valid_lb x = true -> (valid_lb (sqrt_DN p x) = true /\ le_lower (toX (sqrt_DN p x)) (Xsqrt (toX x))).
proof: Proof. intros p x. unfold sqrt_DN. intros Vx; split; [now rewrite valid_lb_next_down| ]; revert Vx. rewrite valid_lb_correct. unfold classify. rewrite classify_spec. unfold toX, toF. rewrite <-!B2SF_Prim2B. rewrite next_down_equiv, sqrt_equiv. case_eq (Prim2B x); [intros sx|intros [ | ]| |intros [ | ] mx ex Bx]; intro Hx; try reflexivity; [ | | ]. { intros _; apply Ropp_le_contravar; simpl; rewrite sqrt_0; lra. } { intro H; discriminate H. } intros _. rewrite <-Hx. set (b_x := Prim2B x). set (b_sx := Bsqrt _ _). generalize (Bpred_correct _ _ Hprec Hmax b_sx). generalize (Bsqrt_correct _ _ Hprec Hmax mode_NE b_x). fold b_sx. assert (Hrx : B2R b_x = FtoR radix2 false mx ex). { now unfold b_x, B2R; rewrite Hx, <-FtoR_split. } intros [Rsx [Fsx Ssx]]. revert Fsx. set (ma := match b_x with B754_zero _ => _ | _ => _ end). replace ma with true. 2:{ unfold ma. revert Hrx. case b_x; [intros [ | ]..| |intros [ | ] m e He]; simpl; try reflexivity; [now generalize (Generic_proof.FtoR_Rpos radix2 mx ex); lra..| ]. rewrite FtoR_split; simpl; unfold Defs.F2R; simpl. set (p1 := (_ * _)%R). set (p2 := (_ * _)%R). assert (Hp1 : (p1 < 0)%R). { unfold p1. rewrite Rmult_comm, <-(Rmult_0_r (bpow radix2 e)). apply Rmult_lt_compat_l; [apply bpow_gt_0|auto with real]. } assert (Hp2 : (0 < p2)%R). { unfold p2. apply Rmult_lt_0_compat; [auto with real|apply bpow_gt_0]. } lra. } intro Fsx. intro H; generalize (H Fsx); clear H. case Rlt_bool; [ |now intros ->]. set (b_s := Bpred _). case_eq b_s; [intro ss..| |intros ss ms es Hes]; intro Hs. { intros [Rs _]; revert Rs; simpl => ->. rewrite Rsx, Hrx. unfold b_x; rewrite Hx. apply Ropp_le_contravar. apply Ulp.pred_round_le_id. { now apply FLT.FLT_exp_valid. } now apply Generic_fmt.valid_rnd_N. } { now case ss. } { now simpl. } intros [Rs _]; revert Rs; simpl. rewrite <-FtoR_split => ->. rewrite Rsx, Hrx. unfold b_x; rewrite Hx. apply Ropp_le_contravar. apply Ulp.pred_round_le_id. { now apply FLT.FLT_exp_valid. } now apply Generic_fmt.valid_rnd_N. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig