Commit 1d4375f4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into renaming

parents 3652cc96 fa794f99
This diff is collapsed.
Require Import Reals Fcore.
Require Import Reals Flocq.Core.Fcore.
Require Import Gappa.Gappa_tactic Interval.Interval_tactic.
Open Scope R_scope.
Lemma rel_helper :
forall xa xe b : R,
xe <> 0 ->
(Rabs ((xa - xe) / xe) <= b <-> Rabs (xa - xe) <= b * Rabs xe).
Proof.
intros xa xe b Zx.
unfold Rdiv.
rewrite Rabs_mult, Rabs_Rinv by exact Zx.
split ; intros H.
- apply Rmult_le_reg_r with (/ Rabs xe).
apply Rinv_0_lt_compat.
now apply Rabs_pos_lt.
rewrite Rmult_assoc, Rinv_r, Rmult_1_r.
exact H.
now apply Rabs_no_R0.
- apply Rmult_le_reg_r with (Rabs xe).
now apply Rabs_pos_lt.
rewrite Rmult_assoc, Rinv_l, Rmult_1_r.
exact H.
now apply Rabs_no_R0.
Qed.
Lemma Rdiv_compat_r :
forall a b c : R, a <> 0 -> c <> 0 ->
(a*b) / (a*c) = b/c.
Proof.
intros a b c Ha Hc.
field.
apply conj.
apply Hc.
apply Ha.
Qed.
Notation pow2 := (bpow radix2).
Definition mul x y := (round radix2 (FLT_exp (-1074) 53) ZnearestE (x * y)).
Definition sub x y := (round radix2 (FLT_exp (-1074) 53) ZnearestE (x - y)).
Notation rnd := (round radix2 (FLT_exp (-1074) 53) ZnearestE).
Definition add x y := rnd (x + y).
Definition sub x y := rnd (x - y).
Definition mul x y := rnd (x * y).
Definition div x y := rnd (x / y).
Definition nearbyint x := round radix2 (FIX_exp 0) ZnearestE x.
Definition Log2h := 3048493539143 * pow2 (-42).
Definition Log2l := 544487923021427 * pow2 (-93).
Definition InvLog2 := 3248660424278399 * pow2 (-51).
Definition p0 := 1 * pow2 (-2).
Definition p1 := 4002712888408905 * pow2 (-59).
Definition p2 := 1218985200072455 * pow2 (-66).
Definition q0 := 1 * pow2 (-1).
Definition q1 := 8006155947364787 * pow2 (-57).
Definition q2 := 4573527866750985 * pow2 (-63).
Definition cw_exp (x : R) :=
let k := nearbyint (mul x InvLog2) in
let t := sub (sub x (mul k Log2h)) (mul k Log2l) in
let t2 := mul t t in
let p := add p0 (mul t2 (add p1 (mul t2 p2))) in
let q := add q0 (mul t2 (add q1 (mul t2 q2))) in
pow2 (Zfloor k + 1) * (add (div (mul t p) (sub q (mul t p))) (1/2)).
Lemma method_error :
forall t : R,
let t2 := t * t in
let p := p0 + t2 * (p1 + t2 * p2) in
let q := q0 + t2 * (q1 + t2 * q2) in
let f := 2 * ((t * p) / (q - t * p) + 1/2) in
Rabs t <= 355 / 1024 ->
Rabs ((f - exp t) / exp t) <= 23 * pow2 (-62).
Proof.
intros t t2 p q f Ht.
unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ; simpl ;
interval with (i_bisect_taylor t 9, i_prec 70).
Qed.
Lemma argument_reduction :
forall x : R,
generic_format radix2 (FLT_exp (-1074) 53) x ->
Rabs x <= 710 ->
let k := round radix2 (FIX_exp 0) ZnearestE (mul x InvLog2) in
-746 <= x <= 710 ->
let k := nearbyint (mul x InvLog2) in
let tf := sub (sub x (mul k Log2h)) (mul k Log2l) in
let te := x - k * ln 2 in
Rabs tf <= 355 / 1024 /\
Rabs (tf - te) <= 65537 * pow2 (-71).
Proof with auto with typeclass_instances.
intros x Fx Bx k tf te.
assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 710) as [Bx'|Bx'] by gappa.
assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 746) as [Bx'|Bx'] by gappa.
- assert (k = 0).
clear -Bx'.
refine (let H := _ in Rle_antisym _ _ (proj2 H) (proj1 H)).
unfold k, mul, InvLog2, Log2h ; gappa.
unfold k, mul, nearbyint, InvLog2, Log2h ; gappa.
unfold tf, te, mul, sub.
rewrite H.
rewrite 2!Rmult_0_l.
......@@ -44,5 +111,50 @@ assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 710) as [Bx'|Bx'] by gappa.
unfold te.
replace (x - k * ln 2) with (x - k * Log2h - k * (ln 2 - Log2h)) by ring.
revert Hl Ax.
unfold tf, te, k, sub, mul, InvLog2, Log2h, Log2l ; gappa.
unfold tf, te, k, sub, mul, nearbyint, InvLog2, Log2h, Log2l ; gappa.
Qed.
Theorem exp_correct :
forall x : R,
generic_format radix2 (FLT_exp (-1074) 53) x ->
-746 <= x <= 710 ->
Rabs ((cw_exp x - exp x) / exp x) <= 1 * pow2 (-51).
Proof.
intros x Fx Bx.
generalize (argument_reduction x Fx Bx).
unfold cw_exp.
set (k := nearbyint (mul x InvLog2)).
set (t := sub (sub x (mul k Log2h)) (mul k Log2l)).
set (t2 := mul t t).
intros [Bt Et].
clearbody t.
generalize (method_error t Bt).
intros Ef.
rewrite bpow_plus, Rmult_assoc.
assert (exp x = pow2 (Zfloor k) * exp (x - k * ln 2)) as ->.
assert (exists k', k = Z2R k') as [k' ->] by (eexists ; apply Rmult_1_r).
rewrite Zfloor_Z2R, bpow_exp, <- exp_plus.
apply f_equal.
simpl ; ring.
rewrite <- Rmult_minus_distr_l.
rewrite Rdiv_compat_r.
2: apply Rgt_not_eq, bpow_gt_0.
2: apply Rgt_not_eq, exp_pos.
clearbody k.
revert Et.
generalize (x - k * ln 2).
clear x Fx Bx.
intros x Ex.
assert (Rabs ((exp t - exp x) / exp x) <= 33 * pow2 (-60)).
unfold Rdiv.
rewrite Rmult_minus_distr_r.
rewrite Rinv_r by apply Rgt_not_eq, exp_pos.
rewrite <- exp_Ropp, <- exp_plus.
revert Ex.
unfold Rminus ; generalize (t + - x) ; clear.
simpl ; intros r Hr ; interval with (i_prec 60).
apply rel_helper. apply Rgt_not_eq, exp_pos.
apply rel_helper in H. 2: apply Rgt_not_eq, exp_pos.
apply rel_helper in Ef. 2: apply Rgt_not_eq, exp_pos.
unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; simpl bpow in * ; gappa.
Qed.
......@@ -209,54 +209,3 @@ clear -Hs1 ; omega.
Qed.
End Compute.
Goal
let beta := Build_radix 5 (eq_refl true) in
let prec := 3%Z in
forall c1 c2 mx,
let x := F2R (Float beta mx 0) in
(0 <= mx < 125)%Z ->
let rnd c := round beta (FLX_exp prec) (Znearest c) in
rnd c1 (R_sqrt.sqrt (rnd c2 (x * x)%R)) = x.
Proof with auto with typeclass_instances.
intros beta prec c1 c2 mx x Hm rnd.
assert (Hprec: Prec_gt_0 prec) by easy.
unfold x, rnd.
set (r c (s : bool) m l := cond_incr (round_N (if s then negb (c (- (m + 1))%Z) else c m) l) m).
rewrite mult_correct with (choice := r c2)...
2: intros x' m l H ; now apply inbetween_int_N_sign.
rewrite sqrt_correct with (prec := prec) (choice := r c1)...
2: intros e ; apply Zle_refl.
2: intros x' m l H ; now apply inbetween_int_N_sign.
apply Rminus_diag_uniq.
rewrite <- F2R_minus.
set (f mx := let x := Float beta mx 0 in Fminus beta
(sqrt beta (FLX_exp prec) prec (r c1) (mult beta (FLX_exp prec) (r c2) x x)) x).
fold (f mx).
assert (Fnum (f mx) = Z0).
clear x.
revert mx Hm.
set (g := fix g m := match m with O => true | S m => match Fnum (f (Z_of_nat m)) with Z0 => g m | _ => false end end).
assert (g 125 = true) by now vm_compute.
revert H.
clearbody f.
clear.
change 125%Z with (Z_of_nat 125).
induction (125).
intros _ mx [H1 H2].
elim (Zlt_irrefl 0).
now apply Zle_lt_trans with mx.
simpl g.
rewrite inj_S.
intros H mx [H1 H2].
apply Zlt_succ_le in H2.
destruct (Zle_lt_or_eq _ _ H2) as [H3|H3].
destruct (Fnum (f (Z.of_nat n))) ; try easy.
now apply IHn ; try split.
rewrite H3.
now destruct (Fnum (f (Z.of_nat n))).
destruct (f mx).
simpl in H.
rewrite H.
apply F2R_0.
Qed.
......@@ -621,7 +621,7 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
[now apply Rplus_le_lt_compat;
[|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|].
apply Rle_trans with (2 * bpow (fexp1 ex - 1)).
- rewrite Rmult_plus_distr_r, Rmult_1_l.
- replace (2 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + bpow (fexp1 ex - 1)) by ring.
apply Rplus_le_compat; [|now apply bpow_le; omega].
apply Rle_trans with (bpow (fexp2 ex)); [|now apply bpow_le; omega].
rewrite <- (Rmult_1_l (bpow (fexp2 _))); unfold cexp.
......@@ -639,7 +639,8 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
replace (bpow ex) with (/ 2 * (2 * bpow ex)) by field.
rewrite <- Rmult_plus_distr_l; apply Rmult_le_compat_l; [lra|].
apply Rle_trans with (3 * bpow (fexp1 ex - 1)).
+ rewrite (Rmult_plus_distr_r _ 2); rewrite Rmult_1_l; apply Rplus_le_compat.
+ replace (3 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + 2 * bpow (fexp1 ex - 1)) by ring.
apply Rplus_le_compat.
* apply bpow_le; unfold cexp; rewrite Hex'; omega.
* apply Rmult_le_compat_l; [lra|]; apply bpow_le; omega.
+ rewrite <- (Rmult_1_l (bpow (fexp1 _))).
......@@ -1754,8 +1755,8 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
rewrite <- Rmult_plus_distr_r.
replace (Z2R m) with (/ 2 * (2 * Z2R m)) by field.
rewrite <- (Rmult_1_r (/ 2)) at 2; rewrite <- Rmult_plus_distr_l.
change 2 with (Z2R 2) at 2; rewrite <- Z2R_mult.
change 1 with (Z2R 1) at 3; rewrite <- Z2R_plus.
change (2 * Z2R m + 1) with (Z2R 2 * Z2R m + Z2R 1).
rewrite <- Z2R_mult, <- Z2R_plus.
rewrite <- Hm.
unfold Zminus; rewrite Zplus_comm; rewrite bpow_plus.
rewrite <- Rmult_assoc; rewrite (Rmult_assoc (/ 2)).
......@@ -1801,7 +1802,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
rewrite <- Rmult_plus_distr_l.
apply Rlt_le_trans with (/ 2 * (2 * u)).
* apply Rmult_lt_compat_l; [lra|].
rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
replace (2 * u) with (u + u) by ring.
apply Rplus_lt_compat_l.
unfold u, ulp, cexp; apply bpow_lt.
omega.
......@@ -1832,7 +1833,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
* rewrite Xmid' at 1.
rewrite <- Rmult_plus_distr_l.
apply Rmult_lt_compat_l; [lra|].
rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
replace (2 * u) with (u + u) by ring.
apply Rplus_lt_compat_l.
unfold u, ulp, cexp; apply bpow_lt.
omega.
......@@ -1862,7 +1863,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
apply (Rmult_le_reg_l 2); [lra|].
rewrite <- Rmult_assoc; replace (2 * _) with 1 by field;
rewrite Rmult_1_l.
rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
rewrite double.
unfold u, ulp, cexp; rewrite <- Hlx.
apply Rplus_le_compat_l; apply bpow_le; omega.
- (* rd <> 0 *)
......@@ -1947,7 +1948,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
rewrite Rmult_1_l.
rewrite ulp_neq_0; trivial.
unfold cexp; rewrite <- Hlr; change (bpow (fexp1 _)) with u.
rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
rewrite double.
apply Rplus_lt_compat_l; unfold u, ulp, cexp, f2; apply bpow_lt.
omega. }
rewrite Hl2.
......@@ -1972,7 +1973,8 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
apply (Rmult_lt_reg_l 2); [lra|]; rewrite <- Rmult_assoc.
replace (2 * / 2) with 1 by field; rewrite Rmult_1_l.
change (bpow f1) with u.
rewrite Rmult_plus_distr_r; rewrite Rmult_1_l; apply Rplus_lt_compat_l.
rewrite double.
apply Rplus_lt_compat_l.
unfold f2, u, ulp, cexp; apply bpow_lt; omega. }
unfold Znearest.
rewrite Hfld.
......@@ -2123,7 +2125,7 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
[now apply Rplus_le_lt_compat;
[|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|].
apply Rle_trans with (2 * bpow (fexp1 ex - 1)).
- rewrite Rmult_plus_distr_r, Rmult_1_l.
- replace (2 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + bpow (fexp1 ex - 1)) by ring.
apply Rplus_le_compat; [|now apply bpow_le; omega].
apply Rle_trans with (bpow (fexp2 ex)); [|now apply bpow_le; omega].
rewrite <- (Rmult_1_l (bpow _)).
......@@ -2143,7 +2145,8 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
replace (bpow ex) with (/ 2 * (2 * bpow ex)) by field.
rewrite <- Rmult_plus_distr_l; apply Rmult_le_compat_l; [lra|].
apply Rle_trans with (3 * bpow (fexp1 ex - 1)).
+ rewrite (Rmult_plus_distr_r _ 2); rewrite Rmult_1_l; apply Rplus_le_compat.
+ replace (3 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + 2 * bpow (fexp1 ex - 1)) by ring.
apply Rplus_le_compat.
* rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_le; unfold cexp; rewrite Hex'; omega.
* apply Rmult_le_compat_l; [lra|]; apply bpow_le; omega.
......
......@@ -205,7 +205,7 @@ apply Rmult_le_compat_r with (1 := HM).
now apply Rplus_le_compat.
unfold Zminus.
rewrite bpow_plus.
simpl (bpow radix2 1).
change (bpow radix2 1) with 2%R.
rewrite F2R_bpow.
ring.
Qed.
......
Require Import Fcore.
Require Import Flocq.Core.Fcore.
Require Import Interval.Interval_tactic.
Section Sec1.
......@@ -1580,7 +1580,7 @@ Hypothesis pGt1: (2 < prec)%Z.
Hypothesis pradix5: (radix_val beta=5)%Z -> (3 < prec)%Z.
Theorem sqrt_sqr: forall x y:R, format x ->
Lemma sqrt_sqr_except: forall x y:R, format x ->
-1 <= round_flx1 (x / round_flx2(sqrt (round_flx3(round_flx4(x*x)+round_flx5(y*y))))) <= 1.
Proof with auto with typeclass_instances.
intros x y Fx.
......@@ -1614,3 +1614,260 @@ repeat apply f_equal; apply f_equal2; apply f_equal; ring.
Qed.
End Sec5.
Require Import Compute.
Require Import Flocq.Calc.Fcalc_bracket Flocq.Calc.Fcalc_round Flocq.Calc.Fcalc_ops Flocq.Calc.Fcalc_div.
Section Sec6.
Lemma sqrt_sqr_special_case:
let beta := Build_radix 5 (eq_refl true) in
let prec := 3%Z in
forall c1 c2 mx,
let x := F2R (Float beta mx 0) in
(0 <= mx < 125)%Z ->
let rnd c := round beta (FLX_exp prec) (Znearest c) in
rnd c1 (R_sqrt.sqrt (rnd c2 (x * x)%R)) = x.
Proof with auto with typeclass_instances.
intros beta prec c1 c2 mx x Hm rnd.
assert (Hprec: Prec_gt_0 prec) by easy.
unfold x, rnd.
set (r c (s : bool) m l := cond_incr (round_N (if s then negb (c (- (m + 1))%Z) else c m) l) m).
rewrite mult_correct with (choice := r c2)...
2: intros x' m l H ; now apply inbetween_int_N_sign.
rewrite sqrt_correct with (prec := prec) (choice := r c1)...
2: intros e ; apply Zle_refl.
2: intros x' m l H ; now apply inbetween_int_N_sign.
apply Rminus_diag_uniq.
rewrite <- F2R_minus.
set (f mx := let x := Float beta mx 0 in Fminus beta
(sqrt beta (FLX_exp prec) prec (r c1) (mult beta (FLX_exp prec) (r c2) x x)) x).
fold (f mx).
assert (Fnum (f mx) = Z0).
clear x.
revert mx Hm.
set (g := fix g m := match m with O => true | S m => match Fnum (f (Z_of_nat m)) with Z0 => g m | _ => false end end).
assert (g 125 = true) by now vm_compute.
revert H.
clearbody f.
clear.
change 125%Z with (Z_of_nat 125).
induction (125).
intros _ mx [H1 H2].
elim (Zlt_irrefl 0).
now apply Zle_lt_trans with mx.
simpl g.
rewrite inj_S.
intros H mx [H1 H2].
apply Zlt_succ_le in H2.
destruct (Zle_lt_or_eq _ _ H2) as [H3|H3].
destruct (Fnum (f (Z.of_nat n))) ; try easy.
now apply IHn ; try split.
rewrite H3.
now destruct (Fnum (f (Z.of_nat n))).
destruct (f mx).
simpl in H.
rewrite H.
apply F2R_0.
Qed.
End Sec6.
Section Sec7.
Open Scope R_scope.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Lemma round_FLX_mult_bpow: forall rnd, Valid_rnd rnd ->
forall x e, round beta (FLX_exp prec) rnd (x*bpow e) =
round beta (FLX_exp prec) rnd x*bpow e.
Proof with auto with typeclass_instances.
intros rnd Hrnd x e.
case (Req_dec x 0); intros Hx.
rewrite Hx, Rmult_0_l, round_0...
ring.
unfold round, FLX_exp, scaled_mantissa, canonic_exp.
rewrite ln_beta_mult_bpow; try exact Hx.
unfold F2R; simpl.
rewrite Rmult_assoc; rewrite <- bpow_plus.
rewrite Rmult_assoc; rewrite <- bpow_plus.
f_equal; f_equal.
f_equal; f_equal; f_equal; ring.
ring.
Qed.
Lemma round_FLX_gt_0: forall rnd, Valid_rnd rnd -> Prec_gt_0 prec ->
forall x, 0 < x -> 0 < round beta (FLX_exp prec) rnd x.
Proof with auto with typeclass_instances.
intros rnd Hrnd Hprec x Hx.
destruct (ln_beta beta x) as (e,He).
apply Rlt_le_trans with (round beta (FLX_exp prec) rnd (bpow (e-1))).
rewrite round_generic...
apply bpow_gt_0.
apply generic_format_bpow.
unfold FLX_exp; unfold Prec_gt_0 in Hprec; omega.
apply round_le...
rewrite <- Rabs_right.
apply He, Rgt_not_eq; easy.
apply Rle_ge; left; easy.
Qed.
Variable choice1 : Z -> bool.
Variable choice2 : Z -> bool.
Variable choice3 : Z -> bool.
Variable choice4 : Z -> bool.
Variable choice5 : Z -> bool.
Notation format := (generic_format beta (FLX_exp prec)).
Notation round_flx1 :=(round beta (FLX_exp prec) (Znearest choice1)).
Notation round_flx2 :=(round beta (FLX_exp prec) (Znearest choice2)).
Notation round_flx3 :=(round beta (FLX_exp prec) (Znearest choice3)).
Notation round_flx4 :=(round beta (FLX_exp prec) (Znearest choice4)).
Notation round_flx5 :=(round beta (FLX_exp prec) (Znearest choice5)).
Hypothesis pGt1: (2 < prec)%Z.
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 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:=(canonic_exp beta (FLX_exp prec) x)).
fold m; fold e.
replace (Z2R m * bpow e * (Z2R m * bpow e)) with
((Z2R m * Z2R 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 (Z2R 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_Z2R.
apply Rle_lt_trans with (1:=Zfloor_lb _).
rewrite <- (Rabs_right (scaled_mantissa _ _ _)); try (apply Rle_ge; easy).
apply Rlt_le_trans with (1:=abs_scaled_mantissa_lt_bpow _ _ _).
unfold canonic_exp, FLX_exp.
ring_simplify (ln_beta beta x - (ln_beta 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; omega.
apply Rle_trans with (1:=Rle_0_sqr (Z2R 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.
Theorem sqrt_sqr: forall x y:R, format x ->
-1 <= round_flx1 (x / round_flx2(R_sqrt.sqrt (round_flx3(round_flx4(x*x)+round_flx5(y*y))))) <= 1.
Proof with auto with typeclass_instances.
intros x y Fx.
assert (Y:Valid_exp (FLX_exp prec)).
apply FLX_exp_valid; unfold Prec_gt_0; omega.
assert (H: ((radix_val beta=5)%Z -> (3 < prec)%Z) \/
((radix_val beta=5)%Z /\ (prec=3)%Z)).
case (Zle_lt_or_eq 3 prec); omega.
case H; intros H'; clear H.
now apply sqrt_sqr_except.
destruct H' as (H1,H2).
apply Rabs_le_inv.
apply abs_round_le_generic...
apply generic_format_FLX.
exists (Float beta 1 0); split.
unfold F2R; simpl; ring.
simpl.
apply Zpower_gt_1; omega.
case (Req_dec x 0); intros Hx.
rewrite Hx; unfold Rdiv; rewrite Rmult_0_l, Rabs_R0.
left; apply Rlt_0_1.
unfold Rdiv; rewrite Rabs_mult.
apply Rle_trans with (Rabs x * / (Rabs x)).
2: right; field.
2: apply Rgt_not_eq, Rabs_pos_lt; easy.
apply Rmult_le_compat_l.
apply Rabs_pos.
rewrite Rabs_right.
apply Rinv_le.
apply Rabs_pos_lt; easy.
apply Rle_trans with (round_flx2 (R_sqrt.sqrt (round_flx4 (x * x)))).
right; apply sym_eq.
now apply sqrt_sqr_special_case_all.
apply round_le...
apply sqrt_le_1_alt.
apply round_ge_generic...
apply generic_format_round...
apply Rplus_le_reg_r with (-round_flx4 (x * x)); ring_simplify.
replace 0 with (round_flx5 0).
apply round_le...
apply Rle_trans with (1:=Rle_0_sqr y).
right; unfold Rsqr; ring.
apply round_0...
apply Rle_ge; left.
apply Rinv_0_lt_compat.
apply round_FLX_gt_0...
unfold Prec_gt_0; omega.
apply sqrt_lt_R0.
apply round_FLX_gt_0...
unfold Prec_gt_0; omega.
apply Rle_lt_trans with (0+ round_flx5 (y * y)).
rewrite Rplus_0_l.
replace 0 with (round_flx5 0).
apply round_le...
apply Rle_trans with (1:=Rle_0_sqr y).
right; unfold Rsqr; ring.
apply round_0...
apply Rplus_lt_compat_r.
apply round_FLX_gt_0...
unfold Prec_gt_0; omega.
apply Rlt_le_trans with (Rsqr x).
now apply Rlt_0_sqr.
right; unfold Rsqr; ring.
Qed.
End Sec7.
......@@ -181,7 +181,7 @@ Qed.
(** Links between FLT and FIX (underflow) *)
Theorem cexp_FLT_FIX :
forall x, x <> R0 ->
forall x, x <> 0%R ->
(Rabs x < bpow (emin + prec))%R ->
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.
Proof.
......
......@@ -211,7 +211,7 @@ Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_FTZ x :=
if Rle_bool R1 (Rabs x) then rnd x else Z0.
if Rle_bool 1 (Rabs x) then rnd x else Z0.
Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
Proof with auto with typeclass_instances.
......@@ -264,7 +264,7 @@ Proof.
intros x Hx.
unfold round, scaled_mantissa, cexp.
destruct (mag beta x) as (ex, He). simpl.
assert (Hx0: x <> R0).
assert (Hx0: x <> 0%R).
intros Hx0.
apply Rle_not_lt with (1 := Hx).
rewrite Hx0, Rabs_R0.
......@@ -280,7 +280,7 @@ rewrite Rle_bool_true.
apply refl_equal.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).
change R1 with (bpow 0).
change 1%R with (bpow 0).
rewrite <- (Zplus_opp_r (FLX_exp prec ex)).
rewrite bpow_plus.
apply Rmult_le_compat_r.
......@@ -314,7 +314,7 @@ rewrite Rle_bool_false.
apply F2R_0.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).
change R1 with (bpow 0).
change 1%R with (bpow 0).
rewrite <- (Zplus_opp_r (FTZ_exp ex)).
rewrite bpow_plus.
apply Rmult_lt_compat_r.
......
......@@ -134,7 +134,7 @@ Qed.
(** Sign facts *)
Theorem F2R_0 :
forall e : Z,
F2R (Float beta 0 e) = R0.
F2R (Float beta 0 e) = 0%R.
Proof.
intros e.
unfold F2R. simpl.
......@@ -143,7 +143,7 @@ Qed.
Theorem F2R_eq_0_reg :
forall m e : Z,
F2R (Float beta m e) = R0 ->
F2R (Float beta m e) = 0%R ->
m = Z0.
Proof.
intros m e H.
......
......@@ -260,7 +260,7 @@ apply Rmult_1_r.
Qed.
Theorem scaled_mantissa_0 :
scaled_mantissa 0 = R0.
scaled_mantissa 0 = 0%R.
Proof.
apply Rmult_0_l.
Qed.
......@@ -675,7 +675,7 @@ Theorem round_bounded_small_pos :
forall x ex,
(ex <= fexp ex)%Z ->
(bpow (ex - 1) <= x < bpow ex)%R ->
round x = R0 \/ round x = bpow (fexp ex).
round x = 0%R \/ round x = bpow (fexp ex).
Proof.
intros x ex He Hx.
unfold round, scaled_mantissa.
......@@ -759,19 +759,19 @@ now apply sym_eq.
Qed.
Theorem round_0 :
round 0 = R0.
round 0 = 0%R.
Proof.
unfold round, scaled_mantissa.
rewrite Rmult_0_l.
fold (Z2R 0).