Used Z -> bool for choice function of rounding to nearest.

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.
 

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.

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 :

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

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,

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,