proposition: Lemma round_round_sqrt : forall fexp1 fexp2 : Z -> Z, Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_sqrt_hyp fexp1 fexp2 -> forall x, generic_format beta fexp1 x -> round_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x Fx. unfold round_round_eq. destruct (Rle_or_lt x 0) as [Npx|Px]. - rewrite (sqrt_neg _ Npx). now rewrite round_0; [|apply valid_rnd_N]. - assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; try assumption; lra|]. assert (Hfsx : (fexp1 (mag (sqrt x)) < mag (sqrt x))%Z). { destruct (Rle_or_lt x 1) as [Hx|Hx]. - apply (valid_exp_large fexp1 (mag x)); [exact Hfx|]. apply mag_le; [exact Px|]. rewrite <- (sqrt_def x) at 1; [|lra]. rewrite <- Rmult_1_r. apply Rmult_le_compat_l. + apply sqrt_pos. + rewrite <- sqrt_1. now apply sqrt_le_1_alt. - generalize ((proj1 (proj2 Hexp)) 1%Z). replace (_ - 1)%Z with 1%Z by ring. intro Hexp10. assert (Hf0 : (fexp1 1 < 1)%Z) by lia. clear Hexp10. apply (valid_exp_large fexp1 1); [exact Hf0|]. apply mag_ge_bpow. rewrite Zeq_minus; [|reflexivity]. unfold Raux.bpow; simpl. apply Rabs_ge; right. rewrite <- sqrt_1. apply sqrt_le_1_alt. now apply Rlt_le. } assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z). { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H). lia. } apply round_round_mid_cases. + exact Vfexp1. + exact Vfexp2. + now apply sqrt_lt_R0. + lia. + lia. + intros Hmid; exfalso; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ