diff --git a/src/Appli/Fappli_Axpy.v b/src/Appli/Fappli_Axpy.v index 4e5049fc2ef320dc5eeeb0e122e155cbec1e1368..02f66cc5a51c0d4b9d4d414d809d2ffe33ef098d 100644 --- a/src/Appli/Fappli_Axpy.v +++ b/src/Appli/Fappli_Axpy.v @@ -152,7 +152,7 @@ Admitted. -Variable choice : R -> bool. +Variable choice : Z -> bool. Variable a1 x1 y1 a x y:R. diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 2c65e8cfae60489a455ac1f0e940082660ad9237..f183a1a195930f48df409f9f2af28c12885c6fd6 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/src/Core/Fcore_generic_fmt.v @@ -1113,12 +1113,12 @@ End not_FTZ. Section Znearest. (** Roundings to nearest: when in the middle, use the choice function *) -Variable choice : R -> bool. +Variable choice : Z -> bool. Definition Znearest x := match Rcompare (x - Z2R (Zfloor x)) (/2) with | Lt => Zfloor x - | Eq => if choice x then Zceil x else Zfloor x + | Eq => if choice (Zfloor x) then Zceil x else Zfloor x | Gt => Zceil x end. @@ -1144,7 +1144,7 @@ intros x. unfold Znearest. case Rcompare_spec ; intros _. now left. -case (choice x). +case choice. now right. now left. now right. @@ -1218,7 +1218,7 @@ rewrite 2!(Rplus_comm (- (Z2R (Zfloor x)))). change (x - Z2R (Zfloor x) = y - Z2R (Zfloor x))%R. now rewrite Hy. apply Zle_trans with (Zceil x). -case (choice x). +case choice. apply Zle_refl. apply le_Z2R. apply Rle_trans with x. @@ -1408,7 +1408,7 @@ apply Rle_0_minus. apply Zfloor_lb. case Rcompare_spec ; intros Hm'. now rewrite Rabs_minus_sym. -case (choice mx). +case choice. rewrite <- Hm'. exact H. now rewrite Rabs_minus_sym. @@ -1430,7 +1430,7 @@ Qed. Theorem round_N_middle : forall x, (x - round rndDN x = round rndUP x - x)%R -> - round rndN x = if choice (scaled_mantissa x) then round rndUP x else round rndDN x. + round rndN x = if choice (Zfloor (scaled_mantissa x)) then round rndUP x else round rndDN x. Proof. intros x. pattern x at 1 4 ; rewrite <- scaled_mantissa_bpow. @@ -1441,12 +1441,12 @@ intros _. rewrite <- Fx. rewrite Zceil_Z2R, Zfloor_Z2R. set (m := Zfloor (scaled_mantissa x)). -now case (Rcompare (Z2R m - Z2R m) (/ 2)) ; case (choice (Z2R m)). +now case (Rcompare (Z2R m - Z2R m) (/ 2)) ; case (choice m). (* *) intros H. rewrite Rcompare_floor_ceil_mid with (1 := Fx). rewrite Rcompare_Eq. -now case (choice (scaled_mantissa x)). +now case choice. apply Rmult_eq_reg_r with (bpow (canonic_exponent x)). now rewrite 2!Rmult_minus_distr_r. apply Rgt_not_eq. @@ -1457,14 +1457,14 @@ End Znearest. Section rndNA. -Definition rndNA := rndN (Rle_bool 0). +Definition rndNA := rndN (Zle_bool 0). Theorem generic_NA_pt : forall x, Rnd_NA_pt generic_format x (round rndNA x). Proof. intros x. -generalize (generic_N_pt (Rle_bool 0) x). +generalize (generic_N_pt (Zle_bool 0) x). fold rndNA. set (f := round rndNA x). intros Rxf. @@ -1479,8 +1479,9 @@ rewrite Rabs_pos_eq with (1 := Hx). rewrite Rabs_pos_eq. unfold f, rndNA. rewrite round_N_middle with (1 := Hm). -rewrite Rle_bool_true. +rewrite Zle_bool_true. apply (generic_UP_pt x). +apply Zfloor_lub. apply Rmult_le_pos with (1 := Hx). apply bpow_ge_0. apply Rnd_N_pt_pos with (2 := Hx) (3 := Rxf). @@ -1491,8 +1492,12 @@ rewrite Rabs_left1. apply Ropp_le_contravar. unfold f, rndNA. rewrite round_N_middle with (1 := Hm). -rewrite Rle_bool_false. +rewrite Zle_bool_false. apply (generic_DN_pt x). +apply lt_Z2R. +apply Rle_lt_trans with (scaled_mantissa x). +apply Zfloor_lb. +simpl. rewrite <- (Rmult_0_l (bpow (- canonic_exponent x))). apply Rmult_lt_compat_r with (2 := Hx). apply bpow_gt_0. @@ -1515,7 +1520,7 @@ Section rndN_opp. Theorem Znearest_opp : forall choice x, - Znearest choice (- x) = (- Znearest (fun t => negb (choice (-t)%R)) x)%Z. + Znearest choice (- x) = (- Znearest (fun t => negb (choice (- (t + 1))%Z)) x)%Z. Proof. intros choice x. destruct (Req_dec (Z2R (Zfloor x)) x) as [Hx|Hx]. @@ -1527,13 +1532,13 @@ replace (- x - Z2R (Zfloor (-x)))%R with (Z2R (Zceil x) - x)%R. rewrite Rcompare_ceil_floor_mid with (1 := Hx). rewrite Rcompare_floor_ceil_mid with (1 := Hx). rewrite Rcompare_sym. +rewrite <- Zceil_floor_neq with (1 := Hx). unfold Zceil. rewrite Ropp_involutive. -case Rcompare_spec ; simpl ; trivial. -intros H. -case (choice (-x)%R); simpl; trivial. +case Rcompare ; simpl ; trivial. +rewrite Zopp_involutive. +case (choice (Zfloor (- x))) ; simpl ; trivial. now rewrite Zopp_involutive. -intros _. now rewrite Zopp_involutive. unfold Zceil. rewrite Z2R_opp. @@ -1543,7 +1548,7 @@ Qed. Theorem round_N_opp : forall choice, forall x, - round (rndN choice) (-x) = (- round (rndN (fun t => negb (choice (-t)%R))) x)%R. + round (rndN choice) (-x) = (- round (rndN (fun t => negb (choice (- (t + 1))%Z))) x)%R. Proof. intros choice x. unfold round, F2R. simpl. diff --git a/src/Core/Fcore_rnd_ne.v b/src/Core/Fcore_rnd_ne.v index b123154ee1271024233b169d26fafea2b1e95852..336bed6830ecac9c30a4a32fa00deeb2ad1975ce 100644 --- a/src/Core/Fcore_rnd_ne.v +++ b/src/Core/Fcore_rnd_ne.v @@ -332,7 +332,7 @@ apply Rnd_NE_pt_total. apply Rnd_NE_pt_monotone. Qed. -Definition rndNE := rndN (fun x => negb (Zeven (Zfloor x))). +Definition rndNE := rndN (fun x => negb (Zeven x)). Theorem generic_NE_pt_pos : forall x, @@ -483,24 +483,20 @@ Theorem round_NE_opp : forall x, round beta fexp rndNE (-x) = (- round beta fexp rndNE x)%R. Proof. -intros x; unfold rndNE. -rewrite round_N_opp. -unfold round. -apply f_equal; apply f_equal; apply f_equal2; trivial. -unfold Zrnd; simpl. -generalize ((scaled_mantissa beta fexp x)); clear x; intros x. -unfold Znearest; case Rcompare_spec ; simpl ; trivial. -intros. -replace (negb (Zeven (Zfloor (- x)))) with (Zeven (Zfloor x)); trivial. -rewrite <- (Zopp_involutive (Zfloor (- x))). -fold (Zceil x). +intros x. +unfold rndNE, round. simpl. +rewrite scaled_mantissa_opp, canonic_exponent_opp. +rewrite Znearest_opp. +rewrite opp_F2R. +apply (f_equal (fun v => F2R (Float beta (-v) _))). +set (m := scaled_mantissa beta fexp x). +unfold Znearest. +case Rcompare ; trivial. +apply (f_equal (fun (b : bool) => if b then Zceil m else Zfloor m)). +rewrite Bool.negb_involutive. rewrite Zeven_opp. -rewrite Zceil_floor_neq. rewrite Zeven_plus. -now case (Zeven (Zfloor x)). -intros H1; contradict H. -rewrite H1; ring_simplify (x-x)%R. -apply sym_not_eq; apply Rinv_neq_0_compat; replace 2%R with (INR 2); auto with real. +now rewrite eqb_sym. Qed. Theorem generic_NE_pt : diff --git a/src/Prop/Fprop_div_sqrt_error.v b/src/Prop/Fprop_div_sqrt_error.v index 97ba1b219aadeb9449f62003d7582f22204de348..d025bbede6be3c6f490ce85e134c572075844824 100644 --- a/src/Prop/Fprop_div_sqrt_error.v +++ b/src/Prop/Fprop_div_sqrt_error.v @@ -33,7 +33,7 @@ Variable Hp : Zlt 0 prec. Notation format := (generic_format beta (FLX_exp prec)). Notation cexp := (canonic_exponent beta (FLX_exp prec)). -Variable choice : R -> bool. +Variable choice : Z -> bool. Theorem format_add: forall x y (fx fy: float beta), (x = F2R fx)%R -> (y = F2R fy)%R -> (Rabs (x+y) < bpow (prec+Fexp fx))%R -> (Rabs (x+y) < bpow (prec+Fexp fy))%R diff --git a/src/Prop/Fprop_plus_error.v b/src/Prop/Fprop_plus_error.v index b9700585adeb10eed9f458502df9355921ae0878..1847944671e244f4f8279bd40723a92a5820f7d1 100644 --- a/src/Prop/Fprop_plus_error.v +++ b/src/Prop/Fprop_plus_error.v @@ -67,7 +67,7 @@ Qed. Hypothesis monotone_exp : forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z. Notation format := (generic_format beta fexp). -Variable choice : R -> bool. +Variable choice : Z -> bool. Lemma plus_error_aux : forall x y, diff --git a/src/Prop/Fprop_relative.v b/src/Prop/Fprop_relative.v index 6f8df3ccd55a2b79c8458bec1600517cb41b127f..8b66f9151bd546cd6eaf7774da20d4c85edde034 100644 --- a/src/Prop/Fprop_relative.v +++ b/src/Prop/Fprop_relative.v @@ -217,7 +217,7 @@ rewrite F2R_0, <- abs_F2R. now apply Rabs_pos_lt. Qed. -Variable choice : R -> bool. +Variable choice : Z -> bool. Theorem generic_relative_error_N : forall x, @@ -443,7 +443,7 @@ apply bpow_gt_0. now apply relative_error_FLT. Qed. -Variable choice : R -> bool. +Variable choice : Z -> bool. Theorem relative_error_N_FLT : forall x, @@ -642,7 +642,7 @@ exact Hp. apply He. Qed. -Variable choice : R -> bool. +Variable choice : Z -> bool. Theorem relative_error_N_FLX : forall x,