Added a typeclass for exponent validity.

src/Appli/Fappli_IEEE.v

@@ -51,7 +51,7 @@ Hypothesis Hmax : (prec < emax)%Z.
 
 Let emin := (3 - emax - prec)%Z.
 Let fexp := FLT_exp emin prec.
-Let fexp_correct : valid_exp fexp := FLT_exp_correct _ _ Hprec.
+Instance fexp_correct : Valid_exp fexp := FLT_exp_valid _ _ Hprec.
 
 Definition bounded_prec m e :=
   Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e.
@@ -497,7 +497,7 @@ now apply F2R_ge_0_compat.
 exact (proj1 (inbetween_float_bounds _ _ _ _ _ Hx)).
 case_eq (shr (shr_record_of_loc m l) e (fexp (digits radix2 m + e) - e)).
 intros mrs e'' H3 H4 H1.
-generalize (truncate_correct radix2 _ fexp_correct x m e l Hx0 Hx (or_introl _ He)).
+generalize (truncate_correct radix2 _ x m e l Hx0 Hx (or_introl _ He)).
 rewrite H1.
 intros (H2,_).
 rewrite <- Hp, H3.
@@ -576,8 +576,8 @@ Proof.
 intros m x mx ex lx Bx Ex.
 unfold binary_round_sign.
 rewrite shr_truncate. 2: easy.
-refine (_ (round_trunc_sign_any_correct _ _ fexp_correct (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))).
-refine (_ (truncate_correct_partial _ _ fexp_correct _ _ _ _ _ Bx Ex)).
+refine (_ (round_trunc_sign_any_correct _ _ (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))).
+refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Bx Ex)).
 destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1).
 rewrite loc_of_shr_record_of_loc, shr_m_shr_record_of_loc.
 set (m1' := choice_mode m (Rlt_bool x 0) m1 l1).
@@ -635,7 +635,7 @@ apply Rlt_not_eq.
 now apply F2R_lt_0_compat.
 apply Rgt_not_eq.
 now apply F2R_gt_0_compat.
-refine (_ (truncate_correct_partial _ _ fexp_correct _ _ _ _ _ Br He)).
+refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)).
 2: now rewrite Hr ; apply F2R_gt_0_compat.
 refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)).
 2: discriminate.
@@ -1045,7 +1045,7 @@ elim Rle_not_lt with (1 := Bz).
 generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy).
 intros Bx By (Hx',_) (Hy',_).
 generalize (canonic_bounded_prec sx _ _ Hx') (canonic_bounded_prec sy _ _ Hy').
-clear -Bx By Hs fexp_correct.
+clear -Bx By Hs.
 intros Cx Cy.
 destruct sx.
 (* ... *)

src/Appli/Fappli_sqrt_FLT_ne.v

@@ -65,7 +65,7 @@ generalize (Fsqrt_core_correct beta prec mx ex (Zgt_lt _ _ Hm)).
 destruct (Fsqrt_core beta prec mx ex) as ((ms, es), ls).
 intros (H1, H2).
 assert (Hp : (0 < prec)%Z) by omega.
-generalize (round_trunc_NE_correct beta _ (FLT_exp_correct emin prec Hp) (sqrt (F2R (Float beta mx ex))) ms es ls).
+generalize (@round_trunc_NE_correct beta _  (FLT_exp_valid emin prec Hp) (sqrt (F2R (Float beta mx ex))) ms es ls).
 destruct (truncate beta (FLT_exp emin prec) (ms, es, ls)) as ((mr, er), lr).
 intros Hr. apply Hr. clear Hr.
 apply sqrt_ge_0.

src/Calc/Fcalc_round.v

@@ -31,7 +31,7 @@ Notation bpow e := (bpow beta e).
 Section Fcalc_round_fexp.
 
 Variable fexp : Z -> Z.
-Hypothesis prop_exp : valid_exp fexp.
+Context { valid_exp : Valid_exp fexp }.
 Notation format := (generic_format beta fexp).
 
 (** Relates location and rounding. *)
@@ -719,7 +719,7 @@ ring_simplify.
 rewrite <- Hm'.
 simpl.
 apply sym_eq.
-apply (proj2 (prop_exp e)).
+apply valid_exp.
 exact H2.
 apply Zle_trans with e.
 eapply bpow_lt_bpow.

src/Core/Fcore_FIX.v

@@ -40,7 +40,8 @@ Definition FIX_format (x : R) :=
 Definition FIX_exp (e : Z) := emin.
 
 (** Properties of the FIX format *)
-Theorem FIX_exp_correct : valid_exp FIX_exp.
+
+Global Instance FIX_exp_valid : Valid_exp FIX_exp.
 Proof.
 intros k.
 unfold FIX_exp.
@@ -68,18 +69,17 @@ Qed.
 Theorem FIX_format_satisfies_any :
   satisfies_any FIX_format.
 Proof.
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp _)).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).
 intros x.
 apply iff_sym.
 apply FIX_format_generic.
-exact FIX_exp_correct.
 Qed.
 
 Theorem Rnd_NE_pt_FIX :
   round_pred (Rnd_NE_pt beta FIX_exp).
 Proof.
 apply Rnd_NE_pt_round.
-apply FIX_exp_correct.
+apply FIX_exp_valid.
 right.
 split ; easy.
 Qed.

src/Core/Fcore_FLT.v

@@ -44,7 +44,7 @@ Definition FLT_format (x : R) :=
 Definition FLT_exp e := Zmax (e - prec) emin.
 
 (** Properties of the FLT format *)
-Theorem FLT_exp_correct : valid_exp FLT_exp.
+Global Instance FLT_exp_valid : Valid_exp FLT_exp.
 Proof.
 intros k.
 unfold FLT_exp.
@@ -124,11 +124,10 @@ Qed.
 Theorem FLT_format_satisfies_any :
   satisfies_any FLT_format.
 Proof.
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp _)).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
 intros x.
 apply iff_sym.
 apply FLT_format_generic.
-exact FLT_exp_correct.
 Qed.
 
 Theorem FLT_canonic_FLX :
@@ -278,7 +277,7 @@ Theorem FLT_not_FTZ :
   not_FTZ_prop FLT_exp.
 Proof.
 apply monotone_exp_not_FTZ.
-apply FLT_exp_correct.
+apply FLT_exp_valid.
 apply FLT_exp_monotone.
 Qed.
 
@@ -309,7 +308,7 @@ Theorem round_NE_pt_FLT :
 Proof.
 intros x.
 apply round_NE_pt.
-apply FLT_exp_correct.
+apply FLT_exp_valid.
 apply NE_ex_prop_FLT.
 Qed.
 
@@ -317,7 +316,7 @@ Theorem Rnd_NE_pt_FLT :
   round_pred (Rnd_NE_pt beta FLT_exp).
 Proof.
 apply Rnd_NE_pt_round.
-apply FLT_exp_correct.
+apply FLT_exp_valid.
 apply NE_ex_prop_FLT.
 Qed.
 

src/Core/Fcore_FLX.v

@@ -43,7 +43,8 @@ Definition FLX_format (x : R) :=
 Definition FLX_exp (e : Z) := (e - prec)%Z.
 
 (** Properties of the FLX format *)
-Theorem FLX_exp_correct : valid_exp FLX_exp.
+
+Global Instance FLX_exp_valid : Valid_exp FLX_exp.
 Proof.
 intros k.
 unfold FLX_exp.
@@ -136,11 +137,10 @@ Qed.
 Theorem FLX_format_satisfies_any :
   satisfies_any FLX_format.
 Proof.
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
 intros x.
 apply iff_sym.
 apply FLX_format_generic.
-exact FLX_exp_correct.
 Qed.
 
 (** unbounded floating-point format with normal mantissas *)
@@ -227,13 +227,12 @@ Qed.
 Theorem FLXN_format_satisfies_any :
   satisfies_any FLXN_format.
 Proof.
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
 split ; intros H.
 apply -> FLX_format_FLXN.
 now apply <- FLX_format_generic.
 apply -> FLX_format_generic.
 now apply <- FLX_format_FLXN.
-exact FLX_exp_correct.
 Qed.
 
 (** FLX is a nice format: it has a monotone exponent... *)
@@ -249,7 +248,7 @@ Theorem FLX_not_FTZ :
   not_FTZ_prop FLX_exp.
 Proof.
 apply monotone_exp_not_FTZ.
-apply FLX_exp_correct.
+apply FLX_exp_valid.
 apply FLX_exp_monotone.
 Qed.
 
@@ -272,7 +271,7 @@ Theorem round_NE_pt_FLX :
 Proof.
 intros x.
 apply round_NE_pt.
-apply FLX_exp_correct.
+apply FLX_exp_valid.
 apply NE_ex_prop_FLX.
 Qed.
 
@@ -280,7 +279,7 @@ Theorem Rnd_NE_pt_FLX :
   round_pred (Rnd_NE_pt beta FLX_exp).
 Proof.
 apply Rnd_NE_pt_round.
-apply FLX_exp_correct.
+apply FLX_exp_valid.
 apply NE_ex_prop_FLX.
 Qed.
 

src/Core/Fcore_FTZ.v

@@ -43,7 +43,7 @@ Definition FTZ_format (x : R) :=
 Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.
 
 (** Properties of the FTZ format *)
-Theorem FTZ_exp_correct : valid_exp FTZ_exp.
+Global Instance FTZ_exp_valid : Valid_exp FTZ_exp.
 Proof.
 intros k.
 unfold FTZ_exp.
@@ -173,11 +173,10 @@ Qed.
 Theorem FTZ_format_satisfies_any :
   satisfies_any FTZ_format.
 Proof.
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp _)).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp)).
 intros x.
 apply iff_sym.
 apply FTZ_format_generic.
-exact FTZ_exp_correct.
 Qed.
 
 Theorem FTZ_format_FLXN :

src/Core/Fcore_generic_fmt.v

@@ -32,14 +32,16 @@ Notation bpow e := (bpow beta e).
 Variable fexp : Z -> Z.
 
 (** To be a good fexp *)
-Definition valid_exp :=
+
+Class Valid_exp :=
+  valid_exp :
   forall k : Z,
   ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
   ( (k <= fexp k)%Z ->
     (fexp (fexp k + 1) <= fexp k)%Z /\
     forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ).
 
-Variable prop_exp : valid_exp.
+Context { valid_exp_ : Valid_exp }.
 
 Definition canonic_exponent x :=
   fexp (ln_beta beta x).
@@ -286,7 +288,7 @@ assert (ex' <= fexp ex)%Z.
 apply Zle_trans with (2 := He).
 apply bpow_lt_bpow with beta.
 now apply Rle_lt_trans with (2 := Ex).
-now rewrite (proj2 (proj2 (prop_exp _) He)).
+now rewrite (proj2 (proj2 (valid_exp _) He)).
 Qed.
 
 Theorem mantissa_DN_small_pos :
@@ -390,11 +392,10 @@ Theorem generic_format_bpow_inv :
 Proof.
 intros e He.
 apply Znot_gt_le; intros He2.
-unfold valid_exp in prop_exp.
 assert (e+1 <= fexp (e+1))%Z.
 replace (fexp (e+1)) with (fexp e).
 omega.
-destruct (prop_exp e) as (Y1,Y2).
+destruct (valid_exp e) as (Y1,Y2).
 apply sym_eq; apply Y2; omega.
 absurd (bpow e=0)%R.
 apply sym_not_eq; apply Rlt_not_eq.
@@ -479,7 +480,7 @@ apply Rle_lt_trans with (1 := proj1 Hex).
 apply Rle_lt_trans with (1 := Hxy).
 apply Hey.
 destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
-rewrite (proj2 (proj2 (prop_exp ey) Hy1) ex).
+rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex).
 apply F2R_le_compat.
 apply Zrnd_monotone.
 apply Rmult_le_compat_r.
@@ -488,7 +489,7 @@ exact Hxy.
 now apply Zle_trans with ey.
 destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
 destruct (Zle_or_lt ey (fexp ex)) as [Hx2|Hx2].
-rewrite (proj2 (proj2 (prop_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
+rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
 apply F2R_le_compat.
 apply Zrnd_monotone.
 apply Rmult_le_compat_r.
@@ -661,14 +662,14 @@ destruct (Zle_or_lt ex (fexp ex)) as [He|He].
 destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr.
 apply generic_format_0.
 apply generic_format_bpow.
-now apply (proj2 (prop_exp ex)).
+now apply valid_exp.
 (* large *)
 generalize (round_bounded_large_pos _ _ He Hex).
 intros (Hr1, Hr2).
 destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
 rewrite <- (Rle_antisym _ _ Hr Hr2).
 apply generic_format_bpow.
-now apply (proj1 (prop_exp ex)).
+now apply valid_exp.
 assert (Hr' := conj Hr1 Hr).
 unfold generic_format, scaled_mantissa.
 rewrite (canonic_exponent_fexp_pos _ _ Hr').
@@ -1114,7 +1115,7 @@ apply Z2R_Zpower.
 unfold canonic_exponent.
 set (ex := ln_beta beta x).
 generalize (not_FTZ ex).
-generalize (proj2 (proj2 (prop_exp _) He) (fexp ex + 1)%Z).
+generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z).
 omega.
 rewrite <- H.
 rewrite <- Z2R_mult, Ztrunc_Z2R.
@@ -1139,7 +1140,7 @@ 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).
+now apply valid_exp.
 Qed.
 
 Theorem canonic_exponent_round :

src/Core/Fcore_rnd_ne.v

@@ -33,7 +33,7 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 
-Variable prop_exp : valid_exp fexp.
+Context { valid_exp : Valid_exp fexp }.
 
 Notation format := (generic_format beta fexp).
 Notation canonic := (canonic beta fexp).
@@ -124,21 +124,21 @@ apply canonic_unicity with (1 := Hu).
 apply (f_equal fexp).
 rewrite <- F2R_change_exp.
 now rewrite F2R_bpow, ln_beta_bpow.
-now eapply prop_exp.
+now apply valid_exp.
 rewrite <- F2R_change_exp.
 rewrite F2R_bpow.
 apply sym_eq.
 rewrite Hxu.
 apply sym_eq.
 apply round_UP_small_pos with (1 := Hex) (2 := Hxe).
-now eapply prop_exp.
+now apply valid_exp.
 rewrite Hd3, Hu3.
 rewrite Zmult_1_l.
 simpl.
 destruct strong_fexp as [H|H].
 apply Zeven_Zpower_odd with (2 := H).
 apply Zle_minus_le_0.
-now eapply prop_exp.
+now apply valid_exp.
 rewrite (proj2 (H ex)).
 now rewrite Zminus_diag.
 exact Hxe.
@@ -147,18 +147,18 @@ assert (Hd4: (bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R).
 rewrite Rabs_pos_eq.
 rewrite Hxd.
 split.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 apply generic_format_bpow.
 ring_simplify (ex - 1 + 1)%Z.
 omega.
 apply Hex.
 apply Rle_lt_trans with (2 := proj2 Hex).
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 rewrite Hxd.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 apply generic_format_0.
 now apply Rlt_le.
-assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply prop_exp.
+assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp.
 assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R).
 rewrite Hxu, Hxd.
 now apply ulp_DN_UP.
@@ -173,7 +173,7 @@ apply canonic_unicity with (1 := Hu).
 apply (f_equal fexp).
 rewrite <- F2R_change_exp.
 now rewrite F2R_bpow, ln_beta_bpow.
-now eapply prop_exp.
+now apply valid_exp.
 rewrite <- Hu2.
 apply sym_eq.
 rewrite <- F2R_change_exp.
@@ -242,12 +242,12 @@ rewrite Rabs_pos_eq.
 split.
 apply Rle_trans with (1 := proj1 Hex).
 rewrite Hxu.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 exact Hu2.
 apply Rlt_le.
 apply Rlt_le_trans with (1 := H0x).
 rewrite Hxu.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 Qed.
 
 Theorem DN_UP_parity_generic :
@@ -350,11 +350,11 @@ destruct (Req_dec (mx - Z2R (Zfloor mx)) (/2)) as [Hm|Hm].
 left.
 exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (canonic_exponent beta fexp xr)).
 split.
-apply (generic_N_pt beta fexp prop_exp _ x).
+apply (generic_N_pt beta fexp _ x).
 split.
 unfold Fcore_generic_fmt.canonic. simpl.
 apply f_equal.
-apply (generic_N_pt beta fexp prop_exp _ x).
+apply (generic_N_pt beta fexp _ x).
 simpl.
 unfold xr, round, Zrnd. simpl.
 unfold Znearest.
@@ -436,7 +436,7 @@ pattern (fexp ex) ; rewrite <- canonic_exponent_fexp_pos with (1 := Hex).
 now apply sym_eq.
 apply Rgt_not_eq.
 apply bpow_gt_0.
-generalize (proj1 (prop_exp ex) He).
+generalize (proj1 (valid_exp ex) He).
 omega.
 (* .. small pos *)
 assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx.

src/Core/Fcore_ulp.v

@@ -32,11 +32,11 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 
-Variable prop_exp : valid_exp fexp.
+Context { valid_exp : Valid_exp fexp }.
 
 Definition ulp x := bpow (canonic_exponent beta fexp x).
 
-Definition F := generic_format beta fexp.
+Notation F := (generic_format beta fexp).
 
 Theorem ulp_opp :
   forall x, ulp (- x) = ulp x.
@@ -98,8 +98,7 @@ rewrite Z2R_plus. simpl.
 ring.
 intros H.
 apply Fx.
-unfold F, generic_format.
-unfold F2R. simpl.
+unfold generic_format, F2R. simpl.
 rewrite <- H.
 rewrite Ztrunc_Z2R.
 rewrite H.
@@ -215,8 +214,7 @@ specialize (Ex (Rgt_not_eq _ _ Zx)).
 assert (Ex' := Ex).
 rewrite Rabs_pos_eq in Ex'.
 destruct (succ_le_bpow x ex) ; try easy.
-unfold F, generic_format.
-unfold scaled_mantissa, canonic_exponent.
+unfold generic_format, scaled_mantissa, canonic_exponent.
 rewrite ln_beta_unique with beta (x + ulp x)%R ex.
 pattern x at 1 3 ; rewrite Fx.
 unfold ulp, scaled_mantissa.
@@ -243,7 +241,7 @@ now apply Rlt_le.
 apply bpow_ge_0.
 rewrite H.
 apply generic_format_bpow.
-apply (prop_exp ex).
+apply valid_exp.
 destruct (Zle_or_lt ex (fexp ex)) ; trivial.
 elim Rlt_not_le with (1 := Zx).
 rewrite Fx.
@@ -316,7 +314,7 @@ Theorem ulp_error :
   (Rabs (round beta fexp Zrnd x - x) < ulp x)%R.
 Proof.
 intros Zrnd x.
-destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx].
+destruct (generic_format_EM beta fexp x) as [Hx|Hx].
 (* x = rnd x *)
 rewrite round_generic with (1 := Hx).
 unfold Rminus.
@@ -331,28 +329,28 @@ apply Rplus_lt_reg_r with (round beta fexp rndDN x).
 rewrite <- ulp_DN_UP with (1 := Hx).
 ring_simplify.
 assert (Hu: (x <= round beta fexp rndUP x)%R).
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 destruct Hu as [Hu|Hu].
 exact Hu.
 elim Hx.
 rewrite Hu.
 now apply generic_format_round.
 apply Rle_minus.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 (* . *)
 rewrite Rabs_pos_eq.
 rewrite ulp_DN_UP with (1 := Hx).
 apply Rplus_lt_reg_r with (x - ulp x)%R.
 ring_simplify.
 assert (Hd: (round beta fexp rndDN x <= x)%R).
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 destruct Hd as [Hd|Hd].
 exact Hd.
 elim Hx.
 rewrite <- Hd.
 now apply generic_format_round.
 apply Rle_0_minus.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 Qed.
 
 Theorem ulp_half_error :
@@ -360,7 +358,7 @@ Theorem ulp_half_error :
   (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp x)%R.
 Proof.
 intros choice x.
-destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx].
+destruct (generic_format_EM beta fexp x) as [Hx|Hx].
 (* x = rnd x *)
 rewrite round_generic.
 unfold Rminus.
@@ -373,12 +371,12 @@ apply bpow_ge_0.
 exact Hx.
 (* x <> rnd x *)
 set (d := round beta fexp rndDN x).
-destruct (generic_N_pt beta fexp prop_exp choice x) as (Hr1, Hr2).
+destruct (generic_N_pt beta fexp choice x) as (Hr1, Hr2).
 destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
 (* . rnd(x) = rndd(x) *)
 apply Rle_trans with (Rabs (d - x)).
 apply Hr2.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 rewrite Rabs_left1.
 rewrite Ropp_minus_distr.
 apply Rmult_le_reg_r with 2%R.
@@ -388,7 +386,7 @@ ring_simplify.
 apply Rle_trans with (1 := H).
 right. field.
 apply Rle_minus.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 (* . rnd(x) = rndu(x) *)
 assert (Hu: (d + ulp x)%R = round beta fexp rndUP x).
 unfold d.
@@ -396,7 +394,7 @@ now rewrite <- ulp_DN_UP.
 apply Rle_trans with (Rabs (d + ulp x - x)).
 apply Hr2.
 rewrite Hu.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 rewrite Rabs_pos_eq.
 apply Rmult_le_reg_r with 2%R.
 now apply (Z2R_lt 0 2).
@@ -407,7 +405,7 @@ apply Rlt_le_trans with (1 := H).
 right. field.
 apply Rle_0_minus.
 rewrite Hu.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 Qed.
 
 Theorem ulp_monotone :
@@ -473,7 +471,7 @@ apply Rle_not_lt.
 apply round_monotone_l; trivial.
 apply generic_format_0.
 apply Ropp_le_contravar; rewrite Hx.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 (* *)
 rewrite Hx; case (Rle_or_lt 0 (round beta fexp rndUP x)).
 intros H; destruct H.
@@ -484,7 +482,7 @@ intros H1; contradict H.
 apply Rle_not_lt.
 apply round_monotone_r; trivial.
 apply generic_format_0.
-apply (round_UP_pt beta fexp prop_exp x).
+apply (round_UP_pt beta fexp x).
 rewrite Hx in Hfx; contradict Hfx; auto with real.
 intros H.
 rewrite <- (ulp_opp (round beta fexp rndUP x)).
@@ -525,7 +523,7 @@ apply Rle_not_lt.
 apply round_monotone_l; trivial.
 apply generic_format_0.
 apply Ropp_le_contravar; rewrite Hx.
-apply (round_DN_pt beta fexp prop_exp x).
+apply (round_DN_pt beta fexp x).
 (* *)
 case (Rle_or_lt 0 (round beta fexp rndUP x)).
 intros H; destruct H.
@@ -538,7 +536,7 @@ intros H1; contradict H.
 apply Rle_not_lt.
 apply round_monotone_r; trivial.
 apply generic_format_0.
-rewrite Hx; apply (round_UP_pt beta fexp prop_exp x).
+rewrite Hx; apply (round_UP_pt beta fexp x).
 rewrite Hx in Hfx; contradict Hfx; auto with real.
 intros H.
 rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp rndUP x)).
@@ -607,8 +605,7 @@ rewrite Rabs_pos_eq in Ex.
 destruct Ex as (H,H'); destruct H; split; trivial.
 contradict Hx; easy.
 now apply Rlt_le.
-unfold F, generic_format.
-unfold scaled_mantissa, canonic_exponent.
+unfold generic_format, scaled_mantissa, canonic_exponent.
 rewrite ln_beta_unique with beta (x - ulp x)%R ex.
 pattern x at 1 3 ; rewrite Fx.
 unfold ulp, scaled_mantissa.
@@ -963,7 +960,7 @@ apply Hey.
 now apply Rgt_not_eq.
 case (Zle_lt_or_eq _ _ H2); intros Hexy.
 assert (fexp ex = fexp (ey-1))%Z.
-apply (proj2 (prop_exp (ey-1)%Z)).
+apply valid_exp.