Added typeclasses for monotone and not_FTZ exponents.

src/Core/Fcore_FIX.v

@@ -84,10 +84,9 @@ right.
 split ; easy.
 Qed.
 
-Theorem FIX_not_FTZ :
-  not_FTZ_prop FIX_exp.
+Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
 Proof.
-intros e.
+intros ex ey H.
 apply Zle_refl.
 Qed.
 

src/Core/Fcore_FLT.v

@@ -262,8 +262,7 @@ now apply FIX_format_generic.
 Qed.
 
 (** FLT is a nice format: it has a monotone exponent... *)
-Theorem FLT_exp_monotone :
-  monotone_exp_prop FLT_exp.
+Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
 Proof.
 intros ex ey.
 clear Hp.
@@ -272,15 +271,6 @@ generalize (Zmax_spec (ex - prec) emin) (Zmax_spec (ey - prec) emin).
 omega.
 Qed.
 
-(** it has subnormal numbers... *)
-Theorem FLT_not_FTZ :
-  not_FTZ_prop FLT_exp.
-Proof.
-apply monotone_exp_not_FTZ.
-apply FLT_exp_valid.
-apply FLT_exp_monotone.
-Qed.
-
 (** and it allows a rounding to nearest, ties to even. *)
 Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
 

src/Core/Fcore_FLX.v

@@ -236,22 +236,12 @@ now apply <- FLX_format_FLXN.
 Qed.
 
 (** FLX is a nice format: it has a monotone exponent... *)
-Theorem FLX_exp_monotone :
-  monotone_exp_prop FLX_exp.
+Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
 Proof.
 intros ex ey Hxy.
 now apply Zplus_le_compat_r.
 Qed.
 
-(** it has normal numbers infinitely close to zero... *)
-Theorem FLX_not_FTZ :
-  not_FTZ_prop FLX_exp.
-Proof.
-apply monotone_exp_not_FTZ.
-apply FLX_exp_valid.
-apply FLX_exp_monotone.
-Qed.
-
 (** and it allows a rounding to nearest, ties to even. *)
 Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
 

src/Core/Fcore_generic_fmt.v

@@ -1097,8 +1097,10 @@ Qed.
 
 Section not_FTZ.
 
-Definition not_FTZ_prop := forall e, (fexp (fexp e + 1) <= fexp e)%Z.
-Hypothesis not_FTZ : not_FTZ_prop.
+Class Exp_not_FTZ :=
+  exp_not_FTZ : forall e, (fexp (fexp e + 1) <= fexp e)%Z.
+
+Context { exp_not_FTZ_ : Exp_not_FTZ }.
 
 Theorem subnormal_exponent :
   forall e x,
@@ -1114,7 +1116,7 @@ assert (H: Z2R (Zpower beta (canonic_exponent x + - fexp e)) = bpow (canonic_exp
 apply Z2R_Zpower.
 unfold canonic_exponent.
 set (ex := ln_beta beta x).
-generalize (not_FTZ ex).
+generalize (exp_not_FTZ ex).
 generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z).
 omega.
 rewrite <- H.
@@ -1130,30 +1132,30 @@ End not_FTZ.
 
 Section monotone_exp.
 
-Definition monotone_exp_prop := forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
+Class Monotone_exp :=
+  monotone_exp : forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
+
+Context { monotone_exp_ : Monotone_exp }.
 
-Theorem monotone_exp_not_FTZ :
-  monotone_exp_prop ->
-  not_FTZ_prop.
+Global Instance monotone_exp_not_FTZ : Exp_not_FTZ.
 Proof.
-intros Hm e.
+intros e.
 destruct (Z_lt_le_dec (fexp e) e) as [He|He].
-apply Hm.
+apply monotone_exp.
 now apply Zlt_le_succ.
 now apply valid_exp.
 Qed.
 
 Theorem canonic_exponent_round :
   forall rnd x,
-  monotone_exp_prop ->
   round rnd x <> R0 ->
   (canonic_exponent x <= canonic_exponent (round rnd x))%Z.
 Proof.
-intros rnd x Hm Zr.
+intros rnd x Zr.
 destruct (total_order_T x 0) as [[Hx|Hx]|Hx].
 (* x < 0 *)
 destruct (round_DN_or_UP rnd x) as [Hd|Hu].
-apply Hm.
+apply monotone_exp.
 apply ln_beta_monotone_abs.
 apply Rlt_not_eq with (1 := Hx).
 rewrite Hd.
@@ -1197,7 +1199,7 @@ apply Rle_antisym with (1 := Zr).
 apply round_monotone_l.
 apply generic_format_0.
 now apply Rlt_le.
-apply Hm.
+apply monotone_exp.
 apply ln_beta_monotone with (1 := Hx).
 rewrite Hu.
 eapply round_UP_pt.

src/Core/Fcore_ulp.v

@@ -409,7 +409,7 @@ apply (round_UP_pt beta fexp x).
 Qed.
 
 Theorem ulp_monotone :
-  monotone_exp_prop fexp ->
+  forall { Hm : Monotone_exp fexp },
   forall x y: R,
   (0 < x)%R -> (x <= y)%R ->
   (ulp x <= ulp y)%R.
@@ -446,12 +446,12 @@ now rewrite canonic_exponent_DN with (2 := Hd).
 Qed.
 
 Theorem ulp_error_f :
-  monotone_exp_prop fexp ->
+  forall { Hm : Monotone_exp 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.
 Proof.
-intros Hf Zrnd x Hfx.
+intros Hm Zrnd x Hfx.
 case (round_DN_or_UP beta fexp Zrnd x); intros Hx.
 (* *)
 case (Rle_or_lt 0 (round beta fexp rndDN x)).
@@ -496,12 +496,12 @@ rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
 Qed.
 
 Theorem ulp_half_error_f : 
-  monotone_exp_prop fexp ->
+  forall { Hm : Monotone_exp 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.
 Proof.
-intros Hf choice x Hfx.
+intros Hm choice x Hfx.
 case (round_DN_or_UP beta fexp (rndN choice) x); intros Hx.
 (* *)
 case (Rle_or_lt 0 (round beta fexp rndDN x)).

src/Prop/Fprop_Sterbenz.v

@@ -31,7 +31,7 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 Context { valid_exp : Valid_exp fexp }.
-Hypothesis monotone_exp : monotone_exp_prop fexp.
+Context { monotone_exp : Monotone_exp fexp }.
 Notation format := (generic_format beta fexp).
 
 Theorem generic_format_plus :

src/Prop/Fprop_plus_error.v

@@ -64,7 +64,7 @@ apply (f_equal (fun v => _ * bpow v)%R).
 ring.
 Qed.
 
-Hypothesis monotone_exp : monotone_exp_prop fexp.
+Context { monotone_exp : Monotone_exp fexp }.
 Notation format := (generic_format beta fexp).
 
 Variable choice : Z -> bool.
@@ -138,10 +138,9 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 Context { valid_exp : Valid_exp fexp }.
+Context { exp_not_FTZ : Exp_not_FTZ fexp }.
 Notation format := (generic_format beta fexp).
 
-Hypothesis not_FTZ : not_FTZ_prop fexp.
-
 Lemma round_plus_eq_zero_aux :
   forall rnd x y,
   (canonic_exponent beta fexp x <= canonic_exponent beta fexp y)%Z ->
@@ -160,8 +159,8 @@ destruct (Zle_or_lt exy (fexp exy)) as [He'|He'].
 (* . *)
 assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) +
   Ztrunc (y * bpow (- fexp exy)) * Zpower beta (fexp exy - fexp exy)) (fexp exy))).
-rewrite (subnormal_exponent beta fexp not_FTZ exy x He' Hx) at 1.
-rewrite (subnormal_exponent beta fexp not_FTZ exy y He' Hy) at 1.
+rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1.
+rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1.
 rewrite <- plus_F2R.
 unfold Fplus. simpl.
 now rewrite Zle_bool_refl.