Commit c1117205 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added variants dedicated to rewriting.

parent 26b74fb8
......@@ -10,15 +10,13 @@ Section Fprop_relative_generic.
Variable fexp : Z -> Z.
Hypothesis prop_exp : valid_exp fexp.
Variable rnd : Zrounding.
Theorem generic_relative_error_lt_conversion :
forall x b, (0 < b)%R ->
forall rnd x b, (0 < b)%R ->
(Rabs (rounding beta fexp rnd x - x) < b * Rabs x)%R ->
exists eps,
(Rabs eps < b)%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R.
Proof.
intros x b Hb0 Hxb.
intros rnd x b Hb0 Hxb.
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
exists R0.
......@@ -38,6 +36,34 @@ rewrite Rinv_l with (1 := Hx0).
now rewrite Rabs_R1, Rmult_1_r.
Qed.
Theorem generic_relative_error_le_conversion :
forall rnd x b, (0 <= b)%R ->
(Rabs (rounding beta fexp rnd x - x) <= b * Rabs x)%R ->
exists eps,
(Rabs eps <= b)%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R.
Proof.
intros rnd x b Hb0 Hxb.
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
exists R0.
split.
now rewrite Rabs_R0.
rewrite Hx0, Rmult_0_l.
apply rounding_0.
(* *)
exists ((rounding beta fexp rnd x - x) / x)%R.
split. 2: now field.
unfold Rdiv.
rewrite Rabs_mult.
apply Rmult_le_reg_r with (Rabs x).
now apply Rabs_pos_lt.
rewrite Rmult_assoc, <- Rabs_mult.
rewrite Rinv_l with (1 := Hx0).
now rewrite Rabs_R1, Rmult_1_r.
Qed.
Variable rnd : Zrounding.
Variable emin p : Z.
Hypothesis Hmin : forall k, (emin < k)%Z -> (p <= k - fexp k)%Z.
......@@ -208,6 +234,22 @@ apply bpow_ge_0.
apply He.
Qed.
Theorem generic_relative_error_N_ex :
forall x,
(bpow emin <= Rabs x)%R ->
exists eps,
(Rabs eps <= /2 * bpow (-p + 1))%R /\ rounding beta fexp (ZrndN choice) x = (x * (1 + eps))%R.
Proof.
intros x Hx.
apply generic_relative_error_le_conversion.
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply generic_relative_error_N.
Qed.
Theorem generic_relative_error_N_F2R :
forall m, let x := F2R (Float beta m emin) in
(Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R.
......@@ -230,6 +272,21 @@ rewrite F2R_0, <- abs_F2R.
now apply Rabs_pos_lt.
Qed.
Theorem generic_relative_error_N_F2R_ex :
forall m, let x := F2R (Float beta m emin) in
exists eps,
(Rabs eps <= /2 * bpow (-p + 1))%R /\ rounding beta fexp (ZrndN choice) x = (x * (1 + eps))%R.
Proof.
intros m x.
apply generic_relative_error_le_conversion.
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply generic_relative_error_N_F2R.
Qed.
Theorem generic_relative_error_N_2 :
(0 < p)%Z ->
forall x,
......@@ -380,6 +437,22 @@ omega.
exact Hx.
Qed.
Theorem relative_error_N_FLT_ex :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
exists eps,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps))%R.
Proof.
intros x Hx.
apply generic_relative_error_le_conversion.
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply relative_error_N_FLT.
Qed.
Theorem relative_error_N_FLT_2 :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -409,6 +482,21 @@ generalize (Zmax_spec (k - prec) emin).
omega.
Qed.
Theorem relative_error_N_FLT_F2R_ex :
forall m, let x := F2R (Float beta m (emin + prec - 1)) in
exists eps,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps))%R.
Proof.
intros m x.
apply generic_relative_error_le_conversion.
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply relative_error_N_FLT_F2R.
Qed.
Theorem relative_error_N_FLT_F2R_2 :
forall m, let x := F2R (Float beta m (emin + prec - 1)) in
(Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x))%R.
......@@ -502,6 +590,21 @@ omega.
apply He.
Qed.
Theorem relative_error_N_FLX_ex :
forall x,
exists eps,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLX_exp prec) (ZrndN choice) x = (x * (1 + eps))%R.
Proof.
intros x.
apply generic_relative_error_le_conversion.
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply relative_error_N_FLX.
Qed.
Theorem relative_error_N_FLX_2 :
forall x,
(Rabs (rounding beta (FLX_exp prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (rounding beta (FLX_exp prec) (ZrndN choice) x))%R.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment