proposition: Lemma Fsqrt_correct : forall beta mode prec (x : float beta), FtoX (Fsqrt mode prec x) = Xround beta mode prec (Xsqrt_nan (FtoX x)).
proof: Proof. Proof with auto with typeclass_instances. intros beta mode prec [ | | sx mx ex] ; simpl ; unfold Xsqrt_nan' ; try easy. case is_negative_spec. intros H. elim (Rlt_irrefl _ H). intros _. apply sym_eq. apply (f_equal Xreal). rewrite sqrt_0. apply round_0... unfold Fsqrt, Fsqrt_aux, Fsqrt_aux2. case is_negative_spec. case sx ; simpl. easy. intros H. elim (Rlt_not_le _ _ H). apply Rlt_le. apply FtoR_Rpos. case sx. intros H. elim (Rle_not_lt _ _ H). apply FtoR_Rneg. intros _. unfold Xround. set (e1 := Z.max _ _). destruct (if Z.even _ then _ else _) as [s' e''] eqn:Hse. set (e' := Z.div2 e''). assert (e' = Z.div2 (ex - e1) /\ s' = ex - 2 * e')%Z as [He1 He2]. { generalize (Zdiv2_odd_eqn (ex - e1)). rewrite <- Z.negb_even. destruct Z.even eqn:H ; injection Hse ; intros <- <-. rewrite Zplus_0_r. intros H0. apply (conj eq_refl). fold e' in H0. rewrite <- H0. ring. change (if negb false then _ else _) with 1%Z. intros H'. unfold e'. rewrite H' at 1 3. rewrite Z.add_simpl_r. rewrite Zdiv2_div, (Zmult_comm 2), Z.div_mul by easy. apply (conj eq_refl). clear -H' ; lia. } assert (e' = Z.min (Z.div2 (Zdigits beta (Zpos mx) + ex) - Zpos prec) (Z.div2 ex)) as He1'. { rewrite He1. unfold e1. rewrite <- Z.sub_min_distr_l, Zminus_0_r. rewrite <- Z.min_mono. replace (ex - _)%Z with (Zdigits beta (Zpos mx) + ex + (-Zpos prec) * 2)%Z by ring. now rewrite Zdiv2_div, Z.div_add, <- Zdiv2_div. intros x y ; apply f_equal. intros x y. rewrite 2!Zdiv2_div. now apply Z.div_le_mono. } assert (2 * e' <= ex)%Z as He. { rewrite He1'. set (foo := (Z.div2 _ - _)%Z). clear. assert (Z.min foo (Z.div2 ex) <= Z.div2 ex)%Z as H by apply Z.le_min_r. generalize (Zdiv2_odd_eqn ex). destruct Z.odd ; intros ; lia. } generalize (Sqrt.Fsqrt_core_correct beta (Zpos mx) ex e' eq_refl He). unfold Sqrt.Fsqrt_core. set (m' := match s' with Z0 => _ | _ => _ end). assert (m' = Zpos mx * Zpower beta (ex - 2 * e'))%Z as ->. { rewrite <- He2. destruct s' as [|p|p]. now rewrite Zmult_1_r. easy. clear -He He2 ; lia. } destruct Z.sqrtrem as [m' r]. set (lz := if Zeq_bool _ _ then _ else _). intros H1. assert (Zpos prec <= Zdigits beta m')%Z as H2. { assert (e' <= Z.div2 (Zdigits beta (Zpos mx) + ex + 1) - Zpos prec)%Z as He'. { rewrite He1'. apply Z.le_trans with (1 := Z.le_min_l _ _). apply Zplus_le_compat_r. rewrite 2!Zdiv2_div. apply Z.div_le_mono. easy. apply Z.le_succ_diag_r. } refine (_ (cexp_inbetween_float _ (FLX_exp (Zpos prec)) _ _ _ _ _ H1 (or_introl _))). unfold cexp, FLX_exp. rewrite (Sqrt.mag_sqrt_F2R beta (Zpos mx) ex eq_refl). clear -He He' ; intros ; lia. apply sqrt_lt_R0. now apply F2R_gt_0. unfold cexp, FLX_exp. now rewrite (Sqrt.mag_sqrt_F2R beta (Zpos mx) ex eq_refl). } destruct m' as [|p|p]. now elim H1. apply (Fround_at_prec_correct beta mode prec false p e'). apply sqrt_lt_R0. apply FtoR_Rpos. rewrite convert_location_bij. now rewrite FtoR_split. rewrite <- digits_conversion. intros H3. elim (Z.lt_irrefl _ (Z.le_lt_trans _ _ _ H2 H3)). destruct (Bracket.inbetween_float_bounds _ _ _ _ _ H1) as (_, H5). elim (Rlt_not_le _ _ H5). apply Rle_trans with R0. apply F2R_le_0. unfold Fnum. now apply (Zlt_le_succ (Zneg p)). apply sqrt_ge_0. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic