aboutsummaryrefslogtreecommitdiffstats
path: root/flocq/Appli
diff options
context:
space:
mode:
Diffstat (limited to 'flocq/Appli')
-rw-r--r--flocq/Appli/Fappli_IEEE.v10
-rw-r--r--flocq/Appli/Fappli_double_round.v30
-rw-r--r--flocq/Appli/Fappli_rnd_odd.v67
3 files changed, 46 insertions, 61 deletions
diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index 6400304b..b6ccd84f 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -39,7 +39,7 @@ Inductive full_float :=
Definition FF2R beta x :=
match x with
| F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e)
- | _ => R0
+ | _ => 0%R
end.
End AnyRadix.
@@ -104,7 +104,7 @@ Definition B2FF x :=
Definition B2R f :=
match f with
| B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
- | _ => R0
+ | _ => 0%R
end.
Theorem FF2R_B2FF :
@@ -346,11 +346,11 @@ Proof.
intros. destruct x, y; try (apply B2R_inj; now eauto).
- simpl in H2. congruence.
- symmetry in H1. apply Rmult_integral in H1.
- destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b0; discriminate H1.
+ destruct H1. apply (eq_Z2R _ 0) in H1. destruct b0; discriminate H1.
simpl in H1. pose proof (bpow_gt_0 radix2 e).
rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
- apply Rmult_integral in H1.
- destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b; discriminate H1.
+ destruct H1. apply (eq_Z2R _ 0) in H1. destruct b; discriminate H1.
simpl in H1. pose proof (bpow_gt_0 radix2 e).
rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
Qed.
@@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y :=
Theorem Bdiv_correct :
forall div_nan m x y,
- B2R y <> R0 ->
+ B2R y <> 0%R ->
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then
B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\
is_finite (Bdiv div_nan m x y) = is_finite x /\
diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v
index 3ff6c31a..2c4937ab 100644
--- a/flocq/Appli/Fappli_double_round.v
+++ b/flocq/Appli/Fappli_double_round.v
@@ -183,8 +183,8 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
apply Rplus_le_compat_r.
apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|].
unfold ulp, canonic_exp; bpow_simplify.
- rewrite <- (Rinv_r 2) at 3; [|lra].
- rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|].
+ apply Rmult_le_reg_l with (1 := Rlt_0_2).
+ replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field.
apply Rle_trans with 1; [|lra].
change 1 with (bpow 0); apply bpow_le.
omega.
@@ -1037,10 +1037,11 @@ destruct Hexp as (_,(_,(_,Hexp4))).
assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z);
[now apply Hexp4; omega|].
assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
-{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
- rewrite <- Rinv_mult_distr; [|lra|lra].
+{ replace (/2 * /2) with (/4) by field.
+ rewrite (bpow_opp _ 2).
apply Rinv_le; [lra|].
- change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r.
+ apply (Z2R_le (2 * 2) (beta * (beta * 1))).
+ rewrite Zmult_1_r.
now apply Zmult_le_compat; omega. }
assert (P2 : (0 < 2)%Z) by omega.
unfold double_round_eq.
@@ -1384,10 +1385,11 @@ assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z);
assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z);
[now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|].
assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
-{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
- rewrite <- Rinv_mult_distr; [|lra|lra].
+{ replace (/2 * /2) with (/4) by field.
+ rewrite (bpow_opp _ 2).
apply Rinv_le; [lra|].
- change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r.
+ apply (Z2R_le (2 * 2) (beta * (beta * 1))).
+ rewrite Zmult_1_r.
now apply Zmult_le_compat; omega. }
assert (Ly : y < bpow (ln_beta y)).
{ apply Rabs_lt_inv.
@@ -1449,7 +1451,7 @@ apply double_round_gt_mid.
unfold canonic_exp.
apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify.
apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)).
- * rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
+ * replace (2 * bpow (fexp1 (ln_beta (x - y)) - 1)) with (bpow (fexp1 (ln_beta (x - y)) - 1) + bpow (fexp1 (ln_beta (x - y)) - 1)) by ring.
apply Rplus_le_compat_l.
now apply bpow_le.
* unfold Zminus; rewrite bpow_plus.
@@ -1458,10 +1460,10 @@ apply double_round_gt_mid.
apply Rmult_le_compat_l; [now apply bpow_ge_0|].
unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
rewrite Zmult_1_r.
- rewrite <- (Rinv_r 2) at 3; [|lra].
- rewrite Rmult_comm; apply Rmult_le_compat_l; [lra|].
- apply Rinv_le; [lra|].
- now change 2 with (Z2R 2); apply Z2R_le.
+ apply Z2R_le, Rinv_le in Hbeta.
+ simpl in Hbeta.
+ lra.
+ apply Rlt_0_2.
Qed.
(* double_round_minus_aux{0,1,2} together *)
@@ -4220,7 +4222,7 @@ destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y))
bpow_simplify.
rewrite (Rmult_comm _ y).
do 2 rewrite Rmult_assoc.
- change (Z2R _ * _) with x'.
+ change (Z2R (Zfloor _) * _) with x'.
change (bpow _) with u1.
apply (Rmult_lt_reg_l (/ 2)); [lra|].
rewrite Rmult_plus_distr_l.
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v
index 4741047f..b6d985ac 100644
--- a/flocq/Appli/Fappli_rnd_odd.v
+++ b/flocq/Appli/Fappli_rnd_odd.v
@@ -20,7 +20,7 @@ COPYING file for more details.
(** * Rounding to odd and its properties, including the equivalence
between rnd_NE and double rounding with rnd_odd and then rnd_NE *)
-
+Require Import Reals Psatz.
Require Import Fcore.
Require Import Fcalc_ops.
@@ -577,29 +577,23 @@ Qed.
Lemma d_le_m: (F2R d <= m)%R.
-apply Rmult_le_reg_l with 2%R.
-auto with real.
-apply Rplus_le_reg_l with (-F2R d)%R.
-apply Rle_trans with (F2R d).
-right; ring.
-apply Rle_trans with (F2R u).
-apply Rle_trans with x.
-apply Hd.
-apply Hu.
-right; unfold m; field.
+Proof.
+assert (F2R d <= F2R u)%R.
+ apply Rle_trans with x.
+ apply Hd.
+ apply Hu.
+unfold m.
+lra.
Qed.
Lemma m_le_u: (m <= F2R u)%R.
-apply Rmult_le_reg_l with 2%R.
-auto with real.
-apply Rplus_le_reg_l with (-F2R u)%R.
-apply Rle_trans with (F2R d).
-right; unfold m; field.
-apply Rle_trans with (F2R u).
-apply Rle_trans with x.
-apply Hd.
-apply Hu.
-right; ring.
+Proof.
+assert (F2R d <= F2R u)%R.
+ apply Rle_trans with x.
+ apply Hd.
+ apply Hu.
+unfold m.
+lra.
Qed.
Lemma ln_beta_m: (0 < F2R d)%R -> (ln_beta beta m =ln_beta beta (F2R d) :>Z).
@@ -641,20 +635,13 @@ now apply Rgt_not_eq.
now apply generic_format_canonic.
now left.
replace m with (F2R d).
-destruct (ln_beta beta (F2R d)) as (e,He).
+destruct (ln_beta beta (F2R d)) as (e,He).
simpl in *; rewrite Rabs_right in He.
apply He.
now apply Rgt_not_eq.
apply Rle_ge; now left.
-assert (F2R d = F2R u).
-apply Rmult_eq_reg_l with (/2)%R.
-apply Rplus_eq_reg_l with (/2*F2R u)%R.
-apply trans_eq with m.
-unfold m, Rdiv; ring.
-rewrite H; field.
-auto with real.
-apply Rgt_not_eq, Rlt_gt; auto with real.
-unfold m; rewrite <- H0; field.
+unfold m in H |- *.
+lra.
Qed.
@@ -666,7 +653,7 @@ apply ln_beta_unique_pos.
unfold m; rewrite <- Y, Rplus_0_l.
rewrite u_eq.
destruct (ln_beta beta x) as (e,He).
-rewrite Rabs_right in He.
+rewrite Rabs_pos_eq in He by now apply Rlt_le.
rewrite round_UP_small_pos with (ex:=e).
rewrite ln_beta_bpow.
ring_simplify (fexp e + 1 - 1)%Z.
@@ -676,7 +663,7 @@ unfold Rdiv; apply Rmult_le_compat_l.
apply bpow_ge_0.
simpl; unfold Z.pow_pos; simpl.
rewrite Zmult_1_r; apply Rinv_le.
-auto with real.
+exact Rlt_0_2.
apply (Z2R_le 2).
specialize (radix_gt_1 beta).
omega.
@@ -684,13 +671,11 @@ apply Rlt_le_trans with (bpow (fexp e)*1)%R.
2: right; ring.
unfold Rdiv; apply Rmult_lt_compat_l.
apply bpow_gt_0.
-rewrite <- Rinv_1 at 3.
-apply Rinv_lt; auto with real.
+lra.
now apply He, Rgt_not_eq.
apply exp_small_round_0_pos with beta (Zfloor) x...
now apply He, Rgt_not_eq.
now rewrite <- d_eq, Y.
-now left.
Qed.
@@ -723,9 +708,8 @@ unfold Rdiv; apply f_equal.
unfold F2R; simpl; unfold Z.pow_pos; simpl.
rewrite Zmult_1_r, Hb, Z2R_mult.
simpl; field.
-apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
-simpl; auto with real.
-rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
+rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
apply radix_pos.
apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z.
unfold Fmult.
@@ -752,9 +736,8 @@ unfold Rdiv; apply f_equal.
unfold F2R; simpl; unfold Z.pow_pos; simpl.
rewrite Zmult_1_r, Hb, Z2R_mult.
simpl; field.
-apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
-simpl; auto with real.
-rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
+rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
apply radix_pos.
apply trans_eq with (-1+Fexp u)%Z.
unfold Fmult.
generated by cgit (git 2.34.1) at 2024-06-12 00:23:34 +0000