proposition: Lemma sqrt_sqr_special_case_all: (radix_val beta=5)%Z -> (prec=3)%Z -> forall x, format x -> round_flx2 (R_sqrt.sqrt (round_flx4 (x * x))) = Rabs x.
proof: Proof. Proof with auto with typeclass_instances. intros H1 H2. assert (forall x : R, 0 < x -> format x -> round_flx2 (R_sqrt.sqrt (round_flx4 (x * x))) = x). intros x Hx Fx. rewrite Fx. unfold F2R; simpl. pose (m:=(Ztrunc (scaled_mantissa beta (FLX_exp prec) x))). pose (e := cexp beta (FLX_exp prec) x). fold m; fold e. replace (IZR m * bpow e * (IZR m * bpow e)) with ((IZR m * IZR m)*(bpow e*bpow e)) by ring. rewrite <- bpow_plus. rewrite round_FLX_mult_bpow... rewrite sqrt_mult. replace (R_sqrt.sqrt (bpow (e + e))) with (bpow e). rewrite round_FLX_mult_bpow... f_equal. replace (IZR m) with (F2R (Float beta m 0)). rewrite H2. replace beta with {| radix_val := 5; radix_prop := eq_refl |}. apply sqrt_sqr_special_case. assert (0 <= scaled_mantissa beta (FLX_exp prec) x). apply Rmult_le_pos;[now left|apply bpow_ge_0]. unfold m; rewrite Ztrunc_floor; try easy. split. apply Zfloor_lub; simpl; easy. apply lt_IZR. apply Rle_lt_trans with (1:=Zfloor_lb _). rewrite <- (Rabs_right (scaled_mantissa _ _ _)); try (apply Rle_ge; easy). apply Rlt_le_trans with (1 := scaled_mantissa_lt_bpow _ _ _). unfold cexp, FLX_exp. ring_simplify (mag beta x - (mag beta x - prec))%Z. rewrite H2; simpl. unfold Z.pow_pos; simpl; rewrite H1. simpl; right; ring. apply radix_val_inj; rewrite H1; easy. unfold F2R; simpl; ring. apply sym_eq, sqrt_lem_1. apply bpow_ge_0. apply bpow_ge_0. now rewrite bpow_plus. apply Rle_trans with (round_flx4 0). right; apply sym_eq, round_0... apply round_le... apply FLX_exp_valid; unfold Prec_gt_0; lia. apply Rle_trans with (1:=Rle_0_sqr (IZR m)). right; unfold Rsqr; ring. apply bpow_ge_0. intros x Fx; case (Rle_or_lt 0 x); intros Hx. case Hx; intros Hx'. rewrite Rabs_right; try apply Rle_ge; try assumption. now apply H. rewrite <- Hx', Rabs_R0, Rmult_0_l, round_0... rewrite sqrt_0, round_0... replace (x*x) with ((-x)*(-x)) by ring. rewrite Rabs_left; try assumption. apply H. apply Ropp_lt_cancel. now rewrite Ropp_involutive, Ropp_0. now apply generic_format_opp. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic) ComputeMore Flocq(Bracket Round Operations Div)