Factored monotonicity of fexp.

src/Core/Fcore_generic_fmt.v

@@ -1110,6 +1110,23 @@ Qed.
 
 End not_FTZ.
 
+Section monotone_exp.
+
+Definition monotone_exp_prop := forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
+
+Theorem monotone_not_FTZ :
+  monotone_exp_prop ->
+  not_FTZ_prop.
+Proof.
+intros Hm e.
+destruct (Z_lt_le_dec (fexp e) e) as [He|He].
+apply Hm.
+now apply Zlt_le_succ.
+apply (proj2 (prop_exp e) He).
+Qed.
+
+End monotone_exp.
+
 Section Znearest.
 
 (** Roundings to nearest: when in the middle, use the choice function *)

src/Core/Fcore_ulp.v

@@ -411,7 +411,7 @@ apply (round_UP_pt beta fexp prop_exp x).
 Qed.
 
 Theorem ulp_monotone :
-  ( forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) ->
+  monotone_exp_prop fexp ->
   forall x y: R,
   (0 < x)%R -> (x <= y)%R ->
   (ulp x <= ulp y)%R.
@@ -447,9 +447,8 @@ unfold ulp.
 now rewrite canonic_exponent_DN with (2 := Hd).
 Qed.
 
-
 Theorem ulp_error_f :
-  (forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) ->
+  monotone_exp_prop fexp ->
   forall Zrnd x,
   (round beta fexp Zrnd x <> 0)%R ->
   (Rabs (round beta fexp Zrnd x - x) < ulp (round beta fexp Zrnd x))%R.
@@ -499,7 +498,7 @@ rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
 Qed.
 
 Theorem ulp_half_error_f : 
-  (forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) ->
+  monotone_exp_prop fexp ->
   forall choice x,
   (round beta fexp (rndN choice) x <> 0)%R ->
   (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp (round beta fexp (rndN choice) x))%R.

src/Prop/Fprop_Sterbenz.v

@@ -31,7 +31,7 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 Hypothesis prop_exp : valid_exp fexp.
-Hypothesis monotone_exp : forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
+Hypothesis monotone_exp : monotone_exp_prop fexp.
 Notation format := (generic_format beta fexp).
 
 Theorem generic_format_plus :

src/Prop/Fprop_div_sqrt_error.v

@@ -134,7 +134,7 @@ replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
 rewrite <- Hr1.
 apply ulp_error_f.
 now apply FLX_exp_correct.
-clear; intros; unfold FLX_exp; omega.
+clear; unfold monotone_exp_prop; intros; unfold FLX_exp; omega.
 exact Hr.
 unfold ulp; apply f_equal.
 now rewrite Hr2, <- Hr1.
@@ -248,7 +248,7 @@ apply Rle_trans with (/2*ulp beta  (FLX_exp prec) (F2R fr))%R.
 rewrite <- Hr1.
 apply ulp_half_error_f; trivial.
 now apply FLX_exp_correct.
-clear; intros; unfold FLX_exp; omega.
+clear; unfold monotone_exp_prop; intros; unfold FLX_exp; omega.
 right; unfold ulp; apply f_equal.
 rewrite Hr2, <- Hr1; trivial. 
 rewrite Rmult_assoc, Rmult_comm.

src/Prop/Fprop_plus_error.v

@@ -64,7 +64,7 @@ apply (f_equal (fun v => _ * bpow v)%R).
 ring.
 Qed.
 
-Hypothesis monotone_exp : forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
+Hypothesis monotone_exp : monotone_exp_prop fexp.
 Notation format := (generic_format beta fexp).
 
 Variable choice : Z -> bool.